Changeset 2131 for src/ASM/AssemblyProofSplitSplit.ma

Timestamp:

Jun 28, 2012, 12:55:05 AM (8 years ago)

Author:

sacerdot

Message:

No more need for functional extensionality.

File:

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

src/ASM/AssemblyProofSplitSplit.ma

@@ -63 +63 @@
     lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
     @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
-    @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
+    @(pose … (λx. bitvector_of_nat ? (lookup_def … labels x 0))) #lookup_labels #EQlookup_labels
     @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
     whd in match execute_1_pseudo_instruction; normalize nodelta
     whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
     lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
-    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
-    [1: >fetch_pseudo_refl % |2: skip |3: assumption ]
+    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels)
+    [1: assumption |2: assumption] >create_label_cost_refl
+    #X lapply (X EQlookup_labels EQlookup_datalabels ?) -X
+    [1: >fetch_pseudo_refl %]
     #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
     generalize in match assm1; -assm1 -assm2 -assm3
     normalize nodelta
     inversion pi
-    [(*2,3:
+    [2,3:
       #arg #_
       (* XXX: we first work on sigma_increment_commutation *)
@@ -138 +140 @@
         (λ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 …))
-      try assumption try % >assembly_refl assumption
+      [1,2,3: try assumption try %] >assembly_refl assumption
     |4: (* Jmp *)
       #arg1 #pi_refl
@@ -182 +184 @@
           >EQnewpc
           inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
-          @sym_eq >address_of_word_labels_assm
-          [1:
-            >EQlookup_labels in mjc_refl; #mjc_refl
-            @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
-            >(andb_true_l … mj_possible_refl) @I
-          ]
+          @sym_eq
+          >EQlookup_labels in mjc_refl; #mjc_refl
+          @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
+          >(andb_true_l … mj_possible_refl) @I
         |3:
-          >EQlookup_labels normalize nodelta
-          >address_of_word_labels_assm try %
+          >EQlookup_labels normalize nodelta %
         |5:
           >EQnewpc
           inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
-          @sym_eq >address_of_word_labels_assm
-          [1:
-            >EQlookup_labels in sjc_refl; #sjc_refl
-            >(pair_destruct_2 ????? (sym_eq … half_add_refl))
-            @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
-            >(andb_true_l … sj_possible_refl) @I
-          ]
+          @sym_eq
+          >EQlookup_labels in sjc_refl; #sjc_refl
+          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
+          @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
+          >(andb_true_l … sj_possible_refl) @I
         ]
         @(is_well_labelled_witness … fetch_pseudo_refl)
@@ -212 +209 @@
         @commutative_plus
       ]
-    |*)5: (* Call *)
+    |5: (* Call *)
       #arg1 #pi_refl
       (* XXX: we first work on sigma_increment_commutation *)
@@ -249 +246 @@
         @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
         try /demod nohyps/ [1: %]
-        @pair_elim #thr #eig #thr_eig_refl
         @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
         @split_eq_status try /demod nohyps/ try %
@@ -256 +252 @@
           cases daemon
         |3:
-          >program_counter_set_program_counter
           whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
           >EQlookup_labels normalize nodelta
@@ -262 +257 @@
           <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
           #relevant >fst_5_rest_refl
-          check absolute_jump_cond
-          <(vsplit_ok ?????? (sym_eq … thr_eig_refl))
           lapply pc_bu_bl_refl' -pc_bu_bl_refl'
           >program_counter_set_8051_sfr >set_clock_set_program_counter