Changeset 2215

Timestamp:

Jul 19, 2012, 5:12:50 PM (7 years ago)

Author:

sacerdot

Message:

Some speed up.

File:

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

src/ASM/PolicyStep.ma

@@ -3 +3 @@
 include alias "arithmetics/nat.ma".
 include alias "basics/logic.ma".
+
+lemma jump_expansion_step1:
+ ∀program : Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l.
+ ∀prefix,x,tl. pi1 … program=prefix@[x]@tl →
+ ∀labels: label_map.
+ ∀old_sigma : ppc_pc_map.
+ ∀inc_added : ℕ.
+ ∀inc_pc_sigma : ppc_pc_map.
+ ∀label : (option Identifier).
+ ∀instr : pseudo_instruction.
+ ∀inc_pc : ℕ.
+ ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
+ ∀old_length : jump_length.
+ ∀Hpolicy : not_jump_default prefix 〈inc_pc,inc_sigma〉.
+ ∀policy : ppc_pc_map.
+ ∀new_length : jump_length.
+ ∀isize : ℕ.
+ let add_instr ≝ match instr with
+  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
+  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
+  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
+  | _             ⇒ None ? 
+  ] in
+ ∀Heq1 :
+  match add_instr with 
+   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
+   |Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉]
+   =〈new_length,isize〉.
+ ∀Heq2 :
+   〈inc_pc+isize,
+     insert … (bitvector_of_nat … (S (|prefix|)))
+      〈inc_pc+isize, \snd  (lookup … (bitvector_of_nat … (S (|prefix|))) (\snd  old_sigma) 〈O,short_jump〉)〉
+      (insert … (bitvector_of_nat … (|prefix|)) 〈inc_pc,new_length〉 inc_sigma)〉
+   = policy.
+  not_jump_default (prefix@[〈label,instr〉]) policy.
+ #program #prefix #x #tl #prf #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
+ #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2 
+ #i >append_length <commutative_plus #Hi normalize in Hi;
+ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+ [ <Heq2 >lookup_insert_miss
+   [ >lookup_insert_miss
+     [ >(nth_append_first ? i prefix ?? Hi)
+       @(Hpolicy i Hi)
+     | @bitvector_of_nat_abs
+       [ @(transitive_lt ??? Hi) ]
+       [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 
+         @le_plus_n_r
+       | @lt_to_not_eq @Hi
+       ]
+     ]
+   | @bitvector_of_nat_abs
+     [ @(transitive_lt ??? Hi) @le_S_to_le ]
+     [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
+       <plus_n_Sm @le_S_S @le_plus_n_r
+     | @lt_to_not_eq @le_S @Hi
+     ]
+   ]
+ | <Heq2 >Hi >lookup_insert_miss
+   [ >lookup_insert_hit cases instr in Heq1;
+     [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
+     |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
+       [1,3: <minus_n_n whd in match (nth ????); %
+       |2,4: @le_n 
+       ]
+     |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
+       [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+         [1,2,3,6,7,24,25: #x #y
+         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
+         <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 
+       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
+         #_ #H @⊥ cases H #H2 @H2 %
+       ]
+     ]
+   | @bitvector_of_nat_abs
+     [ @le_S_to_le ]
+     [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S
+       >append_length <plus_n_Sm @le_S_S @le_plus_n_r
+     | @lt_to_not_eq @le_n
+     ]
+   ]
+ ]
+qed.
 
 (* One step in the search for a jump expansion fixpoint. *)
@@ -97 +179 @@
     else
       〈eqb final_added 0, Some ? final_policy〉.
-[ normalize nodelta @nmk #Habs lapply p generalize in match (foldl_strong ?????); *
+[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
   #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
   (* USE: inc_pc = fst of policy (from fold) *)
@@ -129 +211 @@
     @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
   ]
-| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
+| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
   >H2 in H; normalize nodelta -H2 -x #H @conj
   [ @conj [ @conj 
@@ -153 +235 @@
   (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    * commented out for full proofs, but this needs a lot of memory and time *)
-  [ (* not_jump_default *) cases daemon 
-    (* #i >append_length <commutative_plus #Hi normalize in Hi;
-    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
-    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
-      [ >lookup_insert_miss
-        [ >(nth_append_first ? i prefix ?? Hi)
-          (* USE[pass]: not_jump_default *)
-          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)
-        | @bitvector_of_nat_abs
-          [ @(transitive_lt ??? Hi) ]
-          [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 
-            @le_plus_n_r
-          | @lt_to_not_eq @Hi
-          ]
-        ]
-      | @bitvector_of_nat_abs
-        [ @(transitive_lt ??? Hi) @le_S_to_le ]
-        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
-          <plus_n_Sm @le_S_S @le_plus_n_r
-        | @lt_to_not_eq @le_S @Hi
-        ]
-      ]
-    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
-      [ >lookup_insert_hit cases instr in Heq1;
-        [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
-        |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
-          [1,3: <minus_n_n whd in match (nth ????); / by I/
-          |2,4: @le_n 
-          ]
-        |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
-          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
-            [1,2,3,6,7,24,25: #x #y
-            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
-            <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 
-          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
-            #_ #H @⊥ cases H #H2 @H2 / by I/
-          ]
-        ]
-      | @bitvector_of_nat_abs
-        [ @le_S_to_le ]
-        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S
-          >append_length <plus_n_Sm @le_S_S @le_plus_n_r
-        | @lt_to_not_eq @le_n
-        ]
-      ]
-    ] *)
-  | (* 0 ↦ 0 *) cases daemon
-    (* <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
+  [ (* not_jump_default *)
+    cases (pair_destruct ?????? Heq2) -Heq2 #_ #Heq2
+    @(jump_expansion_step1 … prf … Heq1 Heq2)
+    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
+  | (* 0 ↦ 0 *)
+    <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     [ cases (decidable_eq_nat 0 (|prefix|))
       [ #Heq <Heq >lookup_insert_hit
@@ -215 +255 @@
       ]
     | @bitvector_of_nat_abs
-      [3: @lt_to_not_eq / by / ]
+      [3: @lt_to_not_eq @lt_O_S ]
     ]
-    [1,3: / by /
+    [1,3: @lt_O_S
     |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
       [2: <plus_n_Sm @le_S_S]
       @le_plus_n_r
-    ] *)
+    ]
   ]
   | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))