Changeset 1953

Timestamp:

May 16, 2012, 10:29:22 AM (8 years ago)

Author:

mulligan

Message:

Commit to avoid conflicts.

File:

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

src/ASM/AssemblyProof.ma

@@ -1850 +1850 @@
   λpolicy.
   λppc: Word.
-  λfetched. ?.
-cases daemon(*
+  λfetched.
     match fetched with
     [ Instruction instr ⇒
       match instr with
-      [ JC lbl ⇒
+      [ JC lbl ⇒ ? (*
         match pol lookup_labels ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
-      | JNC lbl ⇒
+        ] *)
+      | JNC lbl ⇒ ? (*
         match pol lookup_labels ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
-      | JB bit lbl ⇒
+        ] *)
+      | JB bit lbl ⇒ ? (*
         match pol lookup_labels ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
-      | JNB bit lbl ⇒
+        ] *)
+      | JNB bit lbl ⇒ ? (*
         match pol lookup_labels ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
-      | JBC bit lbl ⇒
+        ] *)
+      | JBC bit lbl ⇒ ? (*
         match pol lookup_labels ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
-      | JZ lbl ⇒
+        ] *)
+      | JZ lbl ⇒ ? (*
         match pol lookup_labels ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
-      | JNZ lbl ⇒
+        ] *)
+      | JNZ lbl ⇒ ? (*
         match pol lookup_labels  ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
-      | CJNE arg lbl ⇒
+        ] *)
+      | CJNE arg lbl ⇒ ? (*
         match pol lookup_labels ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
-      | DJNZ arg lbl ⇒
+        ] *)
+      | DJNZ arg lbl ⇒ ? (*
         match pol lookup_labels ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
         | long_jump ⇒ 〈4, 4〉
-        ]
+        ] *)
       | ADD arg1 arg2 ⇒
         let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
@@ -2000 +1999 @@
     | Mov dptr tgt ⇒ 〈2, 2〉
     ].
-  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
-*)qed.
+    cases daemon
+qed.
 
 definition ticks_of:
@@ -2032 +2031 @@
       v = v' ∧ q = q'.
 
-axiom split_vector_singleton:
+lemma split_vector_singleton:
   ∀A: Type[0].
   ∀n: nat.
@@ -2038 +2037 @@
   ∀rest: Vector A n.
   ∀s: Vector A 1.
-  ∀prf.
     v = s @@ rest →
-    ((get_index_v A ? v 0 prf) ::: rest) = v.
+    ((get_index_v A ? v 0 ?) ::: rest) = v.
+  [1:
+    #A #n #v cases daemon (* XXX: !!! *)
+  |2:
+    @le_S_S @le_O_n
+  ]
+qed.
 
 example sub_minus_one_seven_eight:
@@ -2121 +2125 @@
 
 axiom low_internal_ram_write_at_stack_pointer:
- ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
+ ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
+ ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
   get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
   low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
   sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
   sp2 = add ? sp1 (bitvector_of_nat 8 1) →
-  bu@@bl = \fst (sigma (pbu@@pbl)) →
+  bu@@bl = sigma (pbu@@pbl) →
    low_internal_ram T1 cm1
      (write_at_stack_pointer …
@@ -2146 +2151 @@
         pbu)).
 
-axiom high_internal_ram_write_at_stack_pointer:
- ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
+lemma high_internal_ram_write_at_stack_pointer:
+ ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
+ ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
   get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
   high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
   sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
   sp2 = add ? sp1 (bitvector_of_nat 8 1) →
-  bu@@bl = \fst (sigma (pbu@@pbl)) →
+  bu@@bl = sigma (pbu@@pbl) →
    high_internal_ram T1 cm1
      (write_at_stack_pointer …
@@ -2171 +2177 @@
           SFR_SP sp2)
         pbu)).
+  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
+  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
+  cases daemon (* XXX: !!! *)
+qed.
 
 lemma Some_Some_elim:
@@ -2178 +2188 @@
 
 (*CSC: ???*)
-axiom snd_assembly_1_pseudoinstruction_ok:
+lemma snd_assembly_1_pseudoinstruction_ok:
   ∀program: pseudo_assembly_program.
   ∀sigma: Word → Word.
@@ -2191 +2201 @@
     let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (sigma ppc) lookup_datalabels  pi) in
       sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
+  #program #sigma #policy #ppc #pi #lookup_labels #lookup_datalabels
+  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
+  normalize nodelta cases daemon (* XXX: !!! *)
+qed.
 
 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.