Changeset 2139 for src/ASM/AssemblyProofSplitSplit.ma

Timestamp:

Jun 28, 2012, 5:42:22 PM (8 years ago)

Author:

mulligan

Message:

Changes to get the main lemma compiling again. Changes pushed into
the first half of the proof of the main theorem, too.

File:

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

src/ASM/AssemblyProofSplitSplit.ma

@@ -134 +134 @@
       ]
     |1: (* Instruction *)
-      #instr #_ #EQP #EQnext #fetch_many_assm
-      @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
-        ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
-        EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
+      #instr #pi_refl #EQP #EQnext #fetch_many_assm
+      @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
+        ps ppc ? ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
+        EQnewppc instr ? (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
         (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
         (refl …) ? (refl …))
-      [1,2,3: try assumption try %] >assembly_refl assumption
+      [1,2:
+        assumption
+      |3:
+        %
+      |4:
+        >fetch_pseudo_refl @pi_refl
+      |5:
+        <EQP %
+      |6:
+        >assembly_refl assumption
+      ]
     |4: (* Jmp *)
       #arg1 #pi_refl
@@ -199 +209 @@
           >(andb_true_l … sj_possible_refl) @I
         ]
-        @(is_well_labelled_witness … fetch_pseudo_refl)
+        whd in is_well_labelled_witness;
+        @(is_well_labelled_witness ? ppc ppc_in_bounds pi)
+        try (>fetch_pseudo_refl %)
         >pi_refl %
       |2:
@@ -256 +268 @@
           @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl normalize nodelta
           <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
-          #relevant >fst_5_rest_refl
+          #relevant
           lapply pc_bu_bl_refl' -pc_bu_bl_refl'
           >program_counter_set_8051_sfr >set_clock_set_program_counter
@@ -278 +290 @@
               <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f
             ]
-          ]
+          ] *)
         |4:
           >set_program_counter_mk_Status_commutation in ⊢ (???%);