Ignore:
Timestamp:
Jun 10, 2011, 1:15:11 PM (9 years ago)
Author:
mulligan
Message:

changes to status and assembly proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r934 r935  
    18441844qed.
    18451845
     1846lemma set_arg_8_set_program_counter:
     1847  ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
     1848  ∀T,s.∀pc:Word.∀b:l.
     1849   set_arg_8 T (set_program_counter … s pc) b = set_arg_8 … s b.
     1850 [2,3: cases b; *; normalize //]
     1851 #n #l #prf #T #s #pc #b * *;
     1852qed.
     1853
    18461854lemma get_arg_8_set_code_memory:
    18471855 ∀T1,T2,s,code_mem,b,arg.
     
    18541862  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
    18551863   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
    1856  #T1 #T2 #s #f1 #f2 #f3 #code_mem whd in ⊢ (??(???%?)%)
    1857  cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl %
     1864 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
    18581865qed.
    18591866
     
    18621869  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
    18631870   set_flags … (set_program_counter … s pc) f1 f2 f3.
    1864  #T1 #s #f1 #f2 #f3 #pc whd in ⊢ (??(??%?)%)
    1865  cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl %
     1871 #T1 #s #f1 #f2 #f3 #pc  %
    18661872qed.
    18671873
     
    18691875 ∀T1,s,f1,f2,f3.
    18701876  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
    1871  #T1 #s #f1 #f2 #f3 whd in ⊢ (??(??%)?) cases (split ????) #nu #nl %
     1877 #T1 #s #f1 #f2 #f3 %
    18721878qed.
    18731879
    18741880axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps.
     1881
     1882lemma eq_rect_Type1_r:
     1883  ∀A: Type[1].
     1884  ∀a:A.
     1885  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
     1886  #A #a #P #H #x #p
     1887  generalize in match H
     1888  generalize in match P
     1889  cases p
     1890  //
     1891qed.
    18751892
    18761893lemma main_thm:
     
    19351952       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    19361953       #result #flags
    1937        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
    1938        >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
     1954       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; %
    19391955    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
    19401956       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     
    19521968        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
    19531969        [5: %
    1954         |
     1970        |1: >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
    19551971
    19561972        XXX
    1957        >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
     1973         %
    19581974 
Note: See TracChangeset for help on using the changeset viewer.