Changeset 950 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 14, 2011, 5:46:15 PM (10 years ago)

Author:

sacerdot

Message:

Horrible sub-proof finished :-)

File:

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

src/ASM/AssemblyProof.ma

@@ -1501 +1501 @@
 (* changed from add to sub *)
 axiom low_internal_ram_of_pseudo_internal_ram_miss:
- ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
+ ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7.
   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 
   let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
@@ -1513 +1513 @@
 
 definition addressing_mode_ok ≝
- λM:internal_pseudo_address_map.λs:PseudoStatus.
+ λT.λM:internal_pseudo_address_map.λs:PreStatus T.
   λaddr:addressing_mode.
    match addr with
@@ -1542 +1542 @@
     
 definition next_internal_pseudo_address_map0 ≝
+  λT.
   λfetched.
   λM: internal_pseudo_address_map.
-  λs: PseudoStatus.
+  λs: PreStatus T.
    match fetched with
     [ Comment _ ⇒ Some ? M
@@ -1555 +1556 @@
        match instr with
         [ ADD addr1 addr2 ⇒
-           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
+           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
             Some ? M
            else
             None ?
         | ADDC addr1 addr2 ⇒ 
-           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
+           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
             Some ? M
            else
             None ?
         | SUBB addr1 addr2 ⇒
-           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
+           if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then
             Some ? M
            else
@@ -1575 +1576 @@
  λM:internal_pseudo_address_map.
   λs:PseudoStatus.
-    next_internal_pseudo_address_map0 (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
+    next_internal_pseudo_address_map0 ?
+     (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
     
 definition status_of_pseudo_status:
@@ -2074 +2076 @@
 qed.
 
+axiom low_internal_ram_write_at_stack_pointer:
+ ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
+  get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP →
+  low_internal_ram ? s2 = low_internal_ram T2 s3 →
+  sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →
+  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
+  bu@@bl = sigma (code_memory … s2) (pbu@@pbl) →
+   low_internal_ram T1
+     (write_at_stack_pointer ?
+       (set_8051_sfr ?
+         (write_at_stack_pointer ?
+           (set_8051_sfr ?
+             (set_low_internal_ram ? s1
+               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2)))
+             SFR_SP sp1)
+          bl)
+        SFR_SP sp2)
+      bu)
+   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
+      (low_internal_ram ?
+       (write_at_stack_pointer ?
+         (set_8051_sfr ?
+           (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl)
+          SFR_SP sp2)
+        pbu)).
+        
 (*
-lemma low_internal_ram_write_at_stack_pointer:
- ∀T,s,x. low_internal_ram T (write_at_stack_pointer T s x) = low_internal_ram T s.
- #T #s #x whd in ⊢ (??(??%)?)
- cases (split ????) #nu #nl normalize nodelta;
- cases (get_index_v bool ????) normalize nodelta; // 
-qed.
-
 lemma high_internal_ram_write_at_stack_pointer:
  ∀T,s,x. high_internal_ram T (write_at_stack_pointer T s x) = high_internal_ram T s.
@@ -2089 +2110 @@
 qed.
 *)
+
+lemma set_program_counter_set_low_internal_ram:
+ ∀T,s,x,y.
+  set_program_counter T (set_low_internal_ram … s x) y =
+   set_low_internal_ram … (set_program_counter … s y) x.
+ //
+qed.
+
+lemma set_clock_set_low_internal_ram:
+ ∀T,s,x,y.
+  set_clock T (set_low_internal_ram … s x) y =
+   set_low_internal_ram … (set_clock … s y) x.
+ //
+qed.
 
 lemma external_ram_write_at_stack_pointer:
@@ -2125 +2160 @@
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
+qed.
+
+axiom get_index_v_set_index:
+ ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
+
+lemma get_8051_sfr_set_8051_sfr:
+ ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
+ #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
+ whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
 qed.
 
@@ -2191 +2235 @@
   \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
 
+lemma pair_destruct_1:
+ ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
+ #A #B #a #b *; /2/
+qed.
+
+lemma pair_destruct_2:
+ ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
+ #A #B #a #b *; /2/
+qed.
+
+(*
 lemma blah:
   ∀m: internal_pseudo_address_map.
@@ -2249 +2304 @@
   |
   ].
-  
+*)
 (*
 map_address0 ... (DIRECT arg) = Some .. →
@@ -2276 +2331 @@
   [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
     #abs @⊥ normalize in abs; destruct (abs) ]
- * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ?)
+ * #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;
@@ -2348 +2403 @@
            generalize in match EQ; -EQ;
            whd in ⊢ (???% → ??%?);
-           cases (half_add ???) #carry #new_sp normalize nodelta;
+           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
            >(eq_bv_to_eq … H2c)
            change with
@@ -2356 +2411 @@
            generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
            >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
-           cases (half_add ???) #carry' #new_sp' normalize nodelta;
+           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
+           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
            @split_eq_status;(* whd in ⊢ (??%%)*)
             [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
               >code_memory_write_at_stack_pointer %
-            | change with
-               (low_internal_ram ?
-                (write_at_stack_pointer ?
-                 (set_8051_sfr ?
-                  (write_at_stack_pointer ?
-                   (set_low_internal_ram ? ps
-                    (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? ps)))
-                  pc_bl) ??) pc_bu) = ?)
+            | >set_program_counter_set_low_internal_ram
+              >set_clock_set_low_internal_ram
+              @low_internal_ram_write_at_stack_pointer
+               [ % | %
+               | @(pair_destruct_2 … EQ1)
+               | @(pair_destruct_2 … EQ2)
+               | >(pair_destruct_1 ????? EQpc)
+                 >(pair_destruct_2 ????? EQpc)
+                 @split_elim #x #y #H <H -x y H;
+                 >(pair_destruct_1 ????? EQppc)
+                 >(pair_destruct_2 ????? EQppc)
+                 @split_elim #x #y #H <H -x y H;
+                 >EQ0 % ]
             |
             | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)