Changeset 2278 for src/ASM/AssemblyProofSplit.ma

Timestamp:

Jul 30, 2012, 6:33:11 PM (9 years ago)

Author:

mulligan

Message:

Half of JC case complete

File:

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

src/ASM/AssemblyProofSplit.ma

@@ -10 +10 @@
   ∀i: instruction.
     fetch_many code_memory final_pc start_pc [i] →
-      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory
-start_pc.
+      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
   #code_memory #final_pc #start_pc #i * #new_pc
   #fetch_many_assm whd in fetch_many_assm;
@@ -68 +67 @@
  #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status
  try assumption %
+qed.
+
+lemma short_jump_cond_ok:
+  ∀v1, v1', v2, v2': Word.
+  ∀is_possible, offset.
+    v1 = v1' → v2 = v2' →
+    〈is_possible, offset〉 = short_jump_cond v1 v2 →
+      is_possible → v2' = add 16 v1' (sign_extension offset).
+  #v1 #v1' #v2 #v2' #is_possible #offset #v1_refl #v2_refl <v1_refl <v2_refl
+  whd in match short_jump_cond; normalize nodelta
+  @pair_elim #result #flags #sub16_refl
+  @pair_elim #upper #lower #vsplit_refl
+  inversion (get_index' bool ???) #get_index_refl normalize nodelta
+  #relevant destruct(relevant) #relevant
+  [1:
+    @(sub_16_to_add_16_8_1 … flags)
+  |2:
+    @(sub_16_to_add_16_8_0 … flags)
+  ]
+  try assumption >sub16_refl
+  <(eq_bv_eq … relevant)
+  >(vsplit_ok … (sym_eq … vsplit_refl)) %
 qed.
 
@@ -1139 +1160 @@
       ]
     ]
-  |12: (* JC *)
+  |*)12: (* JC *)
     >EQP -P normalize nodelta
+    whd in match assembly_1_pseudoinstruction; normalize nodelta
     whd in match expand_pseudo_instruction; normalize nodelta
     whd in match expand_relative_jump; normalize nodelta
     whd in match expand_relative_jump_internal; normalize nodelta
+    >EQppc in ⊢ (% → ?);
     @pair_elim #sj_possible #disp #sj_possible_disp_refl
     inversion sj_possible #sj_possible_refl normalize nodelta
@@ -1156 +1179 @@
       >EQs >EQticks <instr_refl normalize nodelta
       [1:
-        @(get_cy_flag_status_of_pseudo_status M') %
-      |2:
-        @sym_eq @set_program_counter_status_of_pseudo_status
-        [1:
-        |2:
-          @sym_eq @set_clock_status_of_pseudo_status try %
+        @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
+      |2:
+        @set_program_counter_status_of_pseudo_status
+        [1:
+          >EQaddr_of normalize nodelta
+          whd in match addr_of_relative; normalize nodelta
+          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
+          [1:
+            @sym_eq whd in ⊢ (??%?); >EQppc %
+          |2:
+            >EQlookup_labels %
+          |3:
+            >sj_possible_refl @I
+          ]
+        |2:
+          @set_clock_status_of_pseudo_status try %
           whd in match ticks_of0; normalize nodelta
           @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
           [1:
-            @eq_f2 try %
-            >sigma_increment_commutation
-            lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta
-            * #sigma_zero_assm #relevant cases (relevant ppc ?)
-            [1:
-              -relevant
-              [2:
-                >EQcm assumption
-              |1:
-                #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f
-                >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2
-              ]
-            |2:
-            ]
+            >EQppc %
           |2:
             >sj_possible_refl %
@@ -1184 +1204 @@
         ]
       |3:
-      ]
+        @set_clock_status_of_pseudo_status try % @eq_f2 try %
+        whd in match ticks_of0; normalize nodelta
+        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
+        [1:
+          >EQppc %
+        |2:
+          >sj_possible_refl %
+        ]
+      ]
+    |2:
+      #sigma_increment_commutation #maps_assm
+      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
+      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
+      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
+      @(if_then_else_replace ???????? p) try % normalize nodelta
+      change with (execute_1 ?? = ?) destruct
+      whd in ⊢ (??%?); >EQs >EQticks <instr_refl
+      change with (set_program_counter ???? = ?)
     ]
     cases daemon