Changeset 2266 for src/ASM/AssemblyProofSplitSplit.ma

Timestamp:

Jul 26, 2012, 10:43:55 AM (7 years ago)

Author:

sacerdot

Message:

All daemons closed in Jmp case.

File:

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

src/ASM/AssemblyProofSplitSplit.ma

@@ -37 +37 @@
   <(vsplit_ok … (sym_eq … vsplit_v2_refl))
   >(eq_bv_eq … relevant) %
+qed. 
+
+lemma ticks_of_instruction_AJMP:
+ ∀address. ticks_of_instruction (AJMP (ADDR11 address)) = 2.
+try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ
+@(bitvector_3_elim_prop … vl) %
+qed.
+
+lemma ticks_of_instruction_ACALL:
+ ∀address. ticks_of_instruction (ACALL (ADDR11 address)) = 2.
+try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ
+@(bitvector_3_elim_prop … vl) %
 qed.
 
@@ -144 +156 @@
       whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
       whd in match (expand_pseudo_instruction ??????);
+      whd in match (ticks_of0 ??????);
       inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
       inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
@@ -165 +178 @@
       >EQassembled in fetch_refl; #fetch_refl <fetch_refl
       lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
-      whd in ⊢ (??%%);
-      (* XXX: now we start to work on the mk_PreStatus equality *)
-      (* XXX: lhs *)
-      (* XXX: rhs *)
-      (* here we are *)
-      @split_eq_status try % /demod nohyps/
-      [1,3,4:
-        change with (add ???) in match (\snd (half_add ???));
-        whd in match execute_1_pseudo_instruction0; normalize nodelta
-        /demod nohyps/ >set_clock_set_program_counter
-        >program_counter_set_program_counter
-        whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
-        lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
-        normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
-        [1:
-          >EQnewpc
-          inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
-          @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 %
-        |5:
-          >EQnewpc
-          inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
-          @sym_eq
+      change with (set_program_counter ???? =
+       status_of_pseudo_status ?? (set_program_counter ????) ??)
+       @set_program_counter_status_of_pseudo_status
+       [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
+         [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
+                 @sigma_increment_commutation
+         | @eq_f2 try % @ticks_of_instruction_AJMP ]]
+       whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
+       normalize nodelta
+       [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
+         >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
+         @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
+         [2: >(andb_true_l … mj_possible_refl) %
+         | <vsplit_refl @eq_f <EQnewpc % ]
+       | >EQlookup_labels >create_label_cost_refl %
+       |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
+          >create_label_cost_refl
           >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
-        ]
-        whd in is_well_labelled_witness;
-        @(is_well_labelled_witness ? ppc ppc_in_bounds pi)
-        try (>fetch_pseudo_refl %)
-        >pi_refl %
-      |2:
-        whd in ⊢ (??(?%%)%);
-        cases (bitvector_11_cases address)
-        * * * * * * #b4 * #b5
-        * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
-        normalize in match (fetch ??); <plus_n_Sm @eq_f
-        @commutative_plus
+          >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
+          [2: >(andb_true_l … sj_possible_refl) %
+          | >EQnewpc % ]]
+    |5: (* Call *)
+      #arg1 #pi_refl
+      (* XXX: we first work on sigma_increment_commutation *)
+      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
+      whd in match (expand_pseudo_instruction ??????);
+      whd in match (ticks_of0 ??????);
+      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
+      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
+      [2:
+        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
+        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
       ]
-    |5: (* Call *)
+      #sigma_increment_commutation
+      normalize in sigma_increment_commutation:(???(???(??%)));
+      (* XXX: we work on the maps *)
+      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
+      (* XXX: we assume the fetch_many hypothesis *)
+      * #fetch_refl #fetch_many_assm
+      (* XXX: we give the existential *)
+      %{1}
+      (* XXX: work on the left hand side of the equality *)
+      whd in ⊢ (??%?); whd in match (program_counter ???);
+      (* XXX: execute fetches some more *)
+      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
+      whd in fetch_many_assm;
+      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
+      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
+      change with (set_program_counter ???? =
+       status_of_pseudo_status ?? (set_program_counter ????) ??)
+       @set_program_counter_status_of_pseudo_status
+       [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
+         [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
+                 @sigma_increment_commutation
+         | @eq_f2 try % @ticks_of_instruction_AJMP ]]
+       whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
+       normalize nodelta
+       [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
+         >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
+         @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
+         [2: >(andb_true_l … mj_possible_refl) %
+         | <vsplit_refl @eq_f <EQnewpc % ]
+       | >EQlookup_labels >create_label_cost_refl %
+       |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
+          >create_label_cost_refl
+          >EQlookup_labels in sjc_refl; #sjc_refl
+          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
+          >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
+          [2: >(andb_true_l … sj_possible_refl) %
+          | >EQnewpc % ]]
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
       #arg1 #pi_refl
       (* XXX: we first work on sigma_increment_commutation *)