Changeset 935 for src

Timestamp:

Jun 10, 2011, 1:15:11 PM (10 years ago)

Author:

mulligan

Message:

changes to status and assembly proof

Location:

src/ASM

Files:

• AssemblyProof.ma (modified) (6 diffs)
• Status.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -1844 +1844 @@
 qed.
 
+lemma set_arg_8_set_program_counter:
+  ∀n.∀l:Vector addressing_mode_tag (S n). ¬(is_in ? l ACC_PC) →
+  ∀T,s.∀pc:Word.∀b:l.
+   set_arg_8 T (set_program_counter … s pc) b = set_arg_8 … s b.
+ [2,3: cases b; *; normalize //]
+ #n #l #prf #T #s #pc #b * *; 
+qed.
+
 lemma get_arg_8_set_code_memory:
  ∀T1,T2,s,code_mem,b,arg.
@@ -1854 +1862 @@
   set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
    set_flags … (set_code_memory … s code_mem) f1 f2 f3.
- #T1 #T2 #s #f1 #f2 #f3 #code_mem whd in ⊢ (??(???%?)%)
- cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl %
+ #T1 #T2 #s #f1 #f2 #f3 #code_mem %
 qed.
 
@@ -1862 +1869 @@
   set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
    set_flags … (set_program_counter … s pc) f1 f2 f3.
- #T1 #s #f1 #f2 #f3 #pc whd in ⊢ (??(??%?)%)
- cases (split bool 4 4 (get_8051_sfr T1 s SFR_PSW)) #nu #nl %
+ #T1 #s #f1 #f2 #f3 #pc  %
 qed.
 
@@ -1869 +1875 @@
  ∀T1,s,f1,f2,f3.
   program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
- #T1 #s #f1 #f2 #f3 whd in ⊢ (??(??%)?) cases (split ????) #nu #nl %
+ #T1 #s #f1 #f2 #f3 %
 qed.
 
 axiom ignore_clock: ∀T,ps,x.set_clock T ps x = ps.
+
+lemma eq_rect_Type1_r:
+  ∀A: Type[1].
+  ∀a:A.
+  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
+  #A #a #P #H #x #p
+  generalize in match H
+  generalize in match P
+  cases p
+  //
+qed.
 
 lemma main_thm:
@@ -1935 +1952 @@
        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
        #result #flags
-       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
-       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
+       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; %
     | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
        normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
@@ -1952 +1968 @@
         #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
         [5: %
-        |
+        |1: >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
 
         XXX
-       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 
+          % 
   

src/ASM/Status.ma

@@ -498 +498 @@
   λac: option Bit.
   λov: Bit.
-    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_PSW) in
-    let old_cy ≝ get_index_v… nu O ? in
-    let old_ac ≝ get_index_v… nu 1 ? in
-    let old_fo ≝ get_index_v… nu 2 ? in
-    let old_rs1 ≝ get_index_v… nu 3 ? in
-    let old_rs0 ≝ get_index_v… nl O ? in
-    let old_ov ≝ get_index_v… nl 1 ? in
-    let old_ud ≝ get_index_v… nl 2 ? in
-    let old_p ≝ get_index_v… nl 3 ? in
+    let old_cy ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) O ? in
+    let old_ac ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 1 ? in
+    let old_fo ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 2 ? in
+    let old_rs1 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 3 ? in
+    let old_rs0 ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 4 ? in
+    let old_ov ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 5 ? in
+    let old_ud ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 6 ? in
+    let old_p ≝ get_index_v… (get_8051_sfr ? s SFR_PSW) 7 ? in
     let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
     let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;