Changeset 2051 for src

Timestamp:

Jun 12, 2012, 5:49:02 PM (8 years ago)

Author:

mulligan

Message:

Finished the Jmp case in the main theorem.

Location:

src/ASM

Files:

• Assembly.ma (modified) (1 diff)
• AssemblyProofSplitSplit.ma (modified) (6 diffs)
• Interpret.ma (modified) (1 diff)

src/ASM/Assembly.ma

@@ -20 +20 @@
   λpc_plus_jmp_length.λaddr.(*λinstr.*)
   let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
-  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
+  let 〈upper, lower〉 ≝ vsplit ? 9 7 result in
     if get_index' ? 2 0 flags then
-      〈eq_bv 8 upper [[true;true;true;true;true;true;true;true]], lower〉
+      〈eq_bv 9 upper [[true;true;true;true;true;true;true;true;true]], true:::lower〉
     else
-      〈eq_bv 8 upper (zero 8), zero 8〉.
+      〈eq_bv 9 upper (zero …), false:::lower〉.
  
 definition medium_jump_cond: Word → Word → (*pseudo_instruction →*)

src/ASM/AssemblyProofSplitSplit.ma

@@ -1 +1 @@
 include "ASM/AssemblyProofSplit.ma".
 include "common/LabelledObjects.ma".
-
-check pseudo_instruction
 
 definition instruction_has_label ≝
@@ -35 +33 @@
         occurs_exactly_once ASMTag pseudo_instruction id instr_list.
 
+(*CSC: move elsewhere *)
+axiom sub_16_to_add_16_8_0:
+ ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
+  get_index' ? 2 0 flags = false →
+  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
+   v1 = add ? v2 (sign_extension (false:::v3)).
+
+(*CSC: move elsewhere *)
+axiom sub_16_to_add_16_8_1:
+ ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
+  get_index' ? 2 0 flags = true →
+  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
+   v1 = add ? v2 (sign_extension (true:::v3)).
+
+(*CSC: move elsewhere *)
+lemma vsplit_ok:
+  ∀A: Type[0].
+  ∀m, n: nat.
+  ∀v: Vector A (m + n).
+  ∀upper: Vector A m.
+  ∀lower: Vector A n.
+    〈upper, lower〉 = vsplit A m n v →
+      upper @@ lower = v.
+  #A #m #n #v #upper #lower
+  cases daemon
+qed.
+
+lemma short_jump_cond_ok:
+  ∀v1, v2: Word.
+  ∀is_possible, offset.
+    〈is_possible, offset〉 = short_jump_cond v1 v2 →
+      is_possible → v2 = add 16 v1 (sign_extension offset).
+  #v1 #v2 #is_possible #offset
+  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.
+
+lemma medium_jump_cond_ok:
+  ∀v1, v2: Word.
+  ∀is_possible, offset, v1_upper, v1_lower.
+    〈is_possible, offset〉 = medium_jump_cond v1 v2 →
+      〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 →
+        is_possible → v2 = v1_upper @@ offset.
+  #v1 #v2 #is_possible #offset #v1_upper #v1_lower
+  whd in match medium_jump_cond; normalize nodelta
+  @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl
+  @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl
+  #relevant destruct(relevant) normalize nodelta #relevant
+  destruct(relevant) #relevant
+  <(vsplit_ok … (sym_eq … vsplit_v2_refl))
+  >(eq_bv_eq … relevant) %
+qed.
+        
 theorem main_thm:
   ∀M, M': internal_pseudo_address_map.
@@ -81 +143 @@
     (* XXX: work on the left hand side of the equality *)
     whd in ⊢ (??%?);
-    @split_eq_status //
-    [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
+    @split_eq_status try %
+    /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *)
   |6: (* Mov *)
     #arg1 #arg2 #_
@@ -137 +199 @@
     whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
     whd in match (expand_pseudo_instruction ??????);
-(*    generalize in match (refl … (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels (Jmp arg1)));
-    whd in match (expand_pseudo_instruction ??????) in ⊢ (??%? → % → ?); *)
-    inversion (sub_16_with_carry ???) #result #flags #sub16_refl normalize nodelta
-    inversion (vsplit ????) #upper #lower #vsplit_refl normalize nodelta
-    inversion (eq_bv ??? ∧ ¬ policy ?) #eq_bv_policy_refl normalize nodelta
+    inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
+    inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
     [2:
-      inversion (vsplit ????) #fst_5_addr #rest_addr #addr_refl normalize nodelta
-      inversion (vsplit ????) #fst_5_pc #rest_pc #pc_refl normalize nodelta
-      cases (eq_bv ??? ∧ ¬ policy ?) normalize nodelta
+      inversion (medium_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
+      inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
     ]
     #sigma_increment_commutation
@@ -160 +218 @@
     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     whd in fetch_many_assm;
-    >EQassembled in fetch_refl; #fetch_refl <fetch_refl -fetch_refl
+    >EQassembled in fetch_refl; #fetch_refl <fetch_refl
     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     whd in ⊢ (??%%);
@@ -177 +235 @@
       normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
       [1:
-        -address_of_word_labels_assm >EQnewpc >pc_refl normalize nodelta
-        >(pair_destruct_2 ????? (sym_eq … addr_refl))
-        >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc
-        (* XXX: true but needs lemma about splitting *)
-        cases daemon
+        >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
+          @(medium_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
+          >(andb_true_l … mj_possible_refl) @I
+        ]
       |3:
-        >EQnewpc >pc_refl normalize nodelta
-        >(pair_destruct_2 ????? (sym_eq … addr_refl))
-        >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc
         >EQlookup_labels normalize nodelta
         >address_of_word_labels_assm try %
       |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
+        ]
       ]
       @(is_well_labelled_witness … fetch_pseudo_refl)
       >pi_refl %
     |2:
-      whd in match compute_target_of_unconditional_jump; normalize nodelta
-      >program_counter_set_program_counter
-      cases (vsplit ????) #pc_bu #pc_bl normalize nodelta
-      cases (vsplit ????) #nu #nl normalize nodelta
-      cases (vsplit ????) #relevant1 #relevant2 normalize nodelta
-      change with (add ???) in match (\snd (half_add ???)); >EQnewpc
-      cases daemon
-    |3:
-      whd in ⊢ (??%%);
-      /demod nohyps/
-      cases daemon
+      whd in ⊢ (??(?%%)%);
+      cut (∃b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11. address = [[b1;b2;b3;b4;b5;b6;b7;b8;b9;b10;b11]])
+      [1:
+        cases daemon (* XXX: easy but massive proof, move into separate lemma *)
+      |2:
+        * * * * * * * #b4 * #b5
+        * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
+        normalize in match (fetch ??); <plus_n_Sm @eq_f
+        @commutative_plus
+      ]
     ]
   |5: (* Call *)

src/ASM/Interpret.ma

@@ -1170 +1170 @@
 
 lemma execute_1_ok: ∀cm.∀s.
-  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
-    (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
+  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
+    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
       (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
         program_counter ? cm (execute_1 cm s) =