Changeset 2024 for src/ASM/AssemblyProofSplit.ma

Timestamp:

Jun 7, 2012, 3:20:53 PM (8 years ago)

Author:

mulligan

Message:

Updated AssemblyProof? to fix mismatch in definition of lookup_labels between that file and AssemblyProofSplit?. Noticed the precondition we need on fetch_assembly_pseudo2 (that ppc <= |instr_list|) is precisely what we need to remove the cases not_implemented in fetch_assembly_pseudo. Small amount of work, getting everything typechecking, on main theorem in AssemblyProofSplit?.ma.

File:

• src/ASM/AssemblyProofSplit.ma (modified) (5 diffs)

src/ASM/AssemblyProofSplit.ma

@@ -1394 +1394 @@
 
 theorem main_thm:
-  ∀M.
-  ∀M'.
+  ∀M, M': internal_pseudo_address_map.
   ∀program: pseudo_assembly_program.
   ∀sigma: Word → Word.
@@ -1408 +1407 @@
   change with (next_internal_pseudo_address_map0 ????? = ? → ?)
   @(pose … (program_counter ?? ps)) #ppc #EQppc
+  check fetch_assembly_pseudo2
   generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
   @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
@@ -1459 +1459 @@
     >EQassembled in fetch_many_assm;
     cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
-    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
+    #eq_instr
     #fetch_many_assm whd in fetch_many_assm;
     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
-    >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
+    destruct whd in ⊢ (??%?);
     (* XXX: now we start to work on the mk_PreStatus equality *)
     (* XXX: lhs *)
@@ -1470 +1470 @@
     >set_arg_16_mk_Status_commutation
     (* XXX: rhs *)
-    change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
+    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
     >set_program_counter_mk_Status_commutation
     >set_clock_mk_Status_commutation
@@ -1480 +1480 @@
     |2:
       @special_function_registers_8051_set_arg_16
-      [2: >EQlookup_datalabels %
+      [2: %
       |1: //
       ]
     ]
   |1: (* Instruction *) -pi; #instr
-    @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
+    @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy
+        sigma_policy_witness ps ppc EQppc labels costs create_label_cost_refl ? lookup_datalabels)
+    check (main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
       … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels …
       EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))