Changeset 2140 for src/ASM

Timestamp:

Jun 28, 2012, 6:47:26 PM (7 years ago)

Author:

mulligan

Message:

Done the hardest cases in the main theorem. Just got a few daemons to close...

Location:

src/ASM

Files:

• AssemblyProofSplit.ma (modified) (1 diff)
• AssemblyProofSplitSplit.ma (modified) (3 diffs)

src/ASM/AssemblyProofSplit.ma

@@ -403 +403 @@
                       status_of_pseudo_status M' cm s sigma policy).
     P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
+  (* XXX: takes about 45 minutes to type check! *)
   #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
   #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels

src/ASM/AssemblyProofSplitSplit.ma

@@ -150 +150 @@
       |6:
         >assembly_refl assumption
+      |7:
+        <EQassembled assumption
       ]
     |4: (* Jmp *)
@@ -264 +266 @@
           cases daemon
         |3:
-          whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
-          >EQlookup_labels normalize nodelta
-          @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
-          lapply pc_bu_bl_refl' -pc_bu_bl_refl'
-          >program_counter_set_8051_sfr >set_clock_set_program_counter
-          >program_counter_set_program_counter >fst_5_rest_pc_refl
-          cut(fst_5_addr = fst_5_pc)
-          [1:
-            cases daemon (* XXX: !! *)
-          |2:
-            #relevant2 >relevant2
+          lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
+          change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
+          #relevant <(relevant arg1)
+          [2:
+            @(is_well_labelled_witness … ppc_in_bounds pi)
+            [1:
+              >fetch_pseudo_refl %
+            |2:
+              >pi_refl %
+            ]
+          |1:
+            whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
+            >EQlookup_labels normalize nodelta
+            @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
+            >fst_5_rest_refl normalize nodelta
+            @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
+            #pair_true_refl destruct(pair_true_refl)
+            <EQnewpc in fst_5_rest_pc_refl;
+            lapply pc_bu_bl_refl' -pc_bu_bl_refl'
+            >program_counter_set_8051_sfr >set_clock_set_program_counter
+            >program_counter_set_program_counter #relevant2
+            <(vsplit_ok ?????? (sym_eq … relevant2))
             <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
-            #relevant3
-            lapply(vsplit_ok ?????? (sym_eq … relevant3))
-            >(vector_associative_append bool 5 3 8) #relevant4
-            cut(fiv = fst_5_pc ∧ thr'@@pc_bl' = rest_pc)
+            >(vector_associative_append bool 5 3 8) #relevant3
+            >(? : fiv = fst_5_addr)
             [1:
-              cases daemon (* XXX: !! *)
+              %
             |2:
-              * #relevant5 #relevant6 >relevant5
-              >(vector_associative_append bool 5 3 8) @eq_f
-              destruct(relevant)
-              <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f
+              cases daemon
             ]
-          ] *)
+          ]
         |4:
           >set_program_counter_mk_Status_commutation in ⊢ (???%);
@@ -308 +314 @@
           [1: //
           |2:
-            normalize in match (assembly1 ?); >thr_eig_refl
-            @(bitvector_3_elim_prop … thr) %
+            normalize in match (assembly1 ?);
+            @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 offset))) %
           |3:
             #fetch_2_refl >fetch_2_refl >commutative_plus %
           ]
+        ]
+      |2:
+        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
+        try /demod nohyps/ [1: %]
+        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
+        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
+        try /demod nohyps/ [1: %]
+        @split_eq_status try /demod nohyps/ try %
+        [1:
+          cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
+          [1:
+            >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) /demod nohyps/
+            >set_clock_set_program_counter >program_counter_set_program_counter
+            >add_commutative >EQnewpc @eq_f @sym_eq @(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
+          |2:
+            #relevant cases daemon
+            (* XXX: need axioms *)
+          ]
         |2:
+          cases daemon (* XXX: need axioms from assembly.ma *)
+        |3:
+          change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
+          lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
+          #relevant <(relevant arg1)
+          [1:
+            >EQlookup_labels %
+          |2:
+            @(is_well_labelled_witness … ppc_in_bounds pi)
+            [1:
+              >fetch_pseudo_refl %
+            |2:
+              >pi_refl %
+            ]
+          ]
+        |4:
+          >set_program_counter_mk_Status_commutation in ⊢ (???%);
+          >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
+          (* XXX: require set_8051_sfr_write_at_stack_pointer and
+                          special_function_registers_8051_set_8051_sfr
+          *)
+          cases daemon
+        |5,6,7:
+          >set_program_counter_mk_Status_commutation in ⊢ (???%);
+          (* XXX: similar to above but for 8052
+          *)
+          cases daemon
         ]
       ]
     ]
-  ]
 qed.