Changeset 1955 for src/ASM/AssemblyProof.ma

Timestamp:

May 16, 2012, 3:03:52 PM (9 years ago)

Author:

mulligan

Message:

Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some small changes to the statement

File:

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

src/ASM/AssemblyProof.ma

@@ -17 +17 @@
       bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)
   ].
-  [1:
-    applyS prefix
-  |2:
-    letin res ≝ (bit ::: prefix)
-    <minus_S_S >minus_Sn_m
-    try assumption @res
-  |3:
-    @le_S_to_le
-    assumption
-  ]
+  try applyS prefix
+  try (@le_S_to_le assumption)
+  letin res ≝ (bit ::: prefix)
+  <minus_S_S >minus_Sn_m
+  assumption
 qed.
 
@@ -33 +28 @@
   λP: BitVector n → Prop.
     bitvector_elim_prop_internal n P n ? ?.
-  [ @(le_n ?)
-  | <(minus_n_n ?)
-    @[[ ]]
-  ]
+  try @le_n
+  <minus_n_n @[[ ]]
 qed.
 
@@ -60 +53 @@
   | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
   ].
-  [1:
-    applyS prefix
-  |2:
-    letin res ≝ (bit ::: prefix)
-    <(minus_S_S ? ?) >(minus_Sn_m ? ?)
-    try @prf2 @res
-  |3:
-    /2/
-  ].
+  /2/
 qed.
 
@@ -1284 +1269 @@
   ].
 
+axiom add_commutative:
+  ∀n: nat.
+  ∀l, r: BitVector n.
+    add n l r = add n r l.
+
 axiom add_bitvector_of_nat_Sm:
   ∀n, m: nat.
@@ -1321 +1311 @@
 qed.
 
-axiom bitvector_3_cases:
+lemma destruct_bug_fix:
+  3 = 0 → False.
+  #absurd destruct(absurd)
+qed.
+
+definition bitvector_3_cases:
   ∀b: BitVector 3.
-  ∃l, c, r: bool.
-    b = [[l; c; r]].
+    ∃l, c, r: bool.
+      b ≃ [[l; c; r]] ≝ ?.
+  #b
+  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
+  [1:
+    #absurd @⊥ @destruct_bug_fix
+    >absurd %
+  |2:
+    #n #hd #tl #_ #_ #_ %{hd}
+    cases daemon
+  ]
+qed.
 
 lemma bitvector_3_elim_prop:
@@ -2187 +2192 @@
 qed.
 
+definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
+  λpseudo_instruction.
+    match pseudo_instruction with
+    [ Comment c ⇒ False
+    | Cost c ⇒ False
+    | _ ⇒ True
+    ].
+    
 (*CSC: ???*)
 lemma snd_assembly_1_pseudoinstruction_ok:
@@ -2194 +2207 @@
   ∀ppc: Word.
   ∀pi.
+  ∀present_in_machine_code_image_witness: is_present_in_machine_code_image_p pi.
   ∀lookup_labels.
   ∀lookup_datalabels.
@@ -2199 +2213 @@
     lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
     \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
-    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (sigma ppc) lookup_datalabels  pi) in
+    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) 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: !!! *)
+  #program #sigma #policy #ppc #pi #is_present_in_machine_code_image_witness
+  #lookup_labels #lookup_datalabels #lookup_labels_refl #lookup_datalabels_refl
+  #fetch_pseudo_refl
+  normalize nodelta
+  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
+  generalize in match is_present_in_machine_code_image_witness; -is_present_in_machine_code_image_witness
+  cases pi
+  [1:
+    #preinstruction #_
+  |2,3:
+    (* XXX: bug in original statement here, to prove: sigma (ppc + 1) = sigma ppc *)
+    #cost_or_comment normalize in ⊢ (% → ?); #absurd cases absurd
+  |4,5:
+    #identifier #_
+  |6:
+    #dptr #identifier #_
+  ]
+  #fetch_pseudo_refl
+  letin assembled ≝ (\fst (assembly program sigma policy))
+  letin costs ≝ (\snd (assembly program sigma policy))
+  lapply (assembly_ok program sigma policy assembled costs)
+  @pair_elim #labels #costs' #create_label_cost_map_refl
+  <eq_pair_fst_snd #H cases (H (refl …)) -H #costs_refl #H
+  lapply (H ppc) -H
+  @pair_elim #pi' #newppc #fetch_pseudo_refl'
+  @pair_elim #len #assembled #assembly1_refl #H cases H
+  #encoding_check_assm #sigma_newppc_refl
+  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
+  >pi_refl' in assembly1_refl; #assembly1_refl
+  >lookup_labels_refl >lookup_datalabels_refl >assembly1_refl
+  <sigma_newppc_refl
+  generalize in match fetch_pseudo_refl';
+  whd in match (fetch_pseudo_instruction ??);
+  @pair_elim #lbl #instr #nth_refl normalize nodelta
+  #G destruct %
 qed.