Changeset 959 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 15, 2011, 2:22:59 PM (10 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/AssemblyProof.ma (modified) (4 diffs)

src/ASM/AssemblyProof.ma

@@ -2209 +2209 @@
 qed.
 
+lemma program_counter_set_8051_sfr:
+ ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
+ //
+qed.
+
 lemma eq_rect_Type1_r:
   ∀A: Type[1].
@@ -2229 +2234 @@
  //
 qed.
+
+axiom pair_elim':
+  ∀A,B,C: Type[0].
+  ∀T: A → B → C.
+  ∀p.
+  ∀P: A×B → C → Prop.
+    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
+      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
+
+axiom pair_elim'':
+  ∀A,B,C,C': Type[0].
+  ∀T: A → B → C.
+  ∀T': A → B → C'.
+  ∀p.
+  ∀P: A×B → C → C' → Prop.
+    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
+      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
 
 axiom split_elim':
@@ -2370 +2392 @@
     #abs @⊥ normalize in abs; destruct (abs) ]
  * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
- generalize in match (refl … (code_memory … ps))
- cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
+ generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
  generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
   [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
@@ -2509 +2530 @@
               >clock_write_at_stack_pointer %]
        | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
-         generalize in match
-          (refl …
-            (split … 5 11 (sigma 〈preamble,instr_list〉 (address_of_word_labels_code_mem instr_list label))))
-         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
-         generalize in match
-          (refl …
-            (split … 5 11 (sigma 〈preamble,instr_list〉 (program_counter … ps))))
-         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
+         @pair_elim' #fst_5_addr #rest_addr #EQ1
+         @pair_elim' #fst_5_pc #rest_pc #EQ2
          generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
          cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
          generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
          change in ⊢ (? →??%?) with (execute_1_0 ??)
-           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
-           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
-           >H2b >(eq_instruction_to_eq … H2a)
-           generalize in match EQ; -EQ;
-           whd in ⊢ (???% → ?);
-           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
+         @pair_elim' * #instr #newppc' #ticks #EQn
+          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
+          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
+          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
+          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
+          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
+          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
+          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
+          >get_8051_sfr_set_8051_sfr
+          
+          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
            change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
            generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))