Changeset 935


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

changes to status and assembly proof

Location:
src/ASM
Files:
2 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 
  • src/ASM/Status.ma

    r911 r935  
    498498  λac: option Bit.
    499499  λov: Bit.
    500     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_PSW) in
    501     let old_cy ≝ get_index_v… nu O ? in
    502     let old_ac ≝ get_index_v… nu 1 ? in
    503     let old_fo ≝ get_index_v… nu 2 ? in
    504     let old_rs1 ≝ get_index_v… nu 3 ? in
    505     let old_rs0 ≝ get_index_v… nl O ? in
    506     let old_ov ≝ get_index_v… nl 1 ? in
    507     let old_ud ≝ get_index_v… nl 2 ? in
    508     let old_p ≝ get_index_v… nl 3 ? in
     500    let old_cy ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) O ? in
     501    let old_ac ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 1 ? in
     502    let old_fo ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 2 ? in
     503    let old_rs1 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 3 ? in
     504    let old_rs0 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 4 ? in
     505    let old_ov ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 5 ? in
     506    let old_ud ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 6 ? in
     507    let old_p ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 7 ? in
    509508    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
    510509    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
Note: See TracChangeset for help on using the changeset viewer.