Changeset 2215


Ignore:
Timestamp:
Jul 19, 2012, 5:12:50 PM (5 years ago)
Author:
sacerdot
Message:

Some speed up.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2211 r2215  
    33include alias "arithmetics/nat.ma".
    44include alias "basics/logic.ma".
     5
     6lemma jump_expansion_step1:
     7 ∀program : Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l.
     8 ∀prefix,x,tl. pi1 … program=prefix@[x]@tl →
     9 ∀labels: label_map.
     10 ∀old_sigma : ppc_pc_map.
     11 ∀inc_added : ℕ.
     12 ∀inc_pc_sigma : ppc_pc_map.
     13 ∀label : (option Identifier).
     14 ∀instr : pseudo_instruction.
     15 ∀inc_pc : ℕ.
     16 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
     17 ∀old_length : jump_length.
     18 ∀Hpolicy : not_jump_default prefix 〈inc_pc,inc_sigma〉.
     19 ∀policy : ppc_pc_map.
     20 ∀new_length : jump_length.
     21 ∀isize : ℕ.
     22 let add_instr ≝ match instr with
     23  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     24  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     25  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     26  | _             ⇒ None ?
     27  ] in
     28 ∀Heq1 :
     29  match add_instr with 
     30   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     31   |Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉]
     32   =〈new_length,isize〉.
     33 ∀Heq2 :
     34   〈inc_pc+isize,
     35     insert … (bitvector_of_nat … (S (|prefix|)))
     36      〈inc_pc+isize, \snd  (lookup … (bitvector_of_nat … (S (|prefix|))) (\snd  old_sigma) 〈O,short_jump〉)〉
     37      (insert … (bitvector_of_nat … (|prefix|)) 〈inc_pc,new_length〉 inc_sigma)〉
     38   = policy.
     39  not_jump_default (prefix@[〈label,instr〉]) policy.
     40 #program #prefix #x #tl #prf #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
     41 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2
     42 #i >append_length <commutative_plus #Hi normalize in Hi;
     43 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     44 [ <Heq2 >lookup_insert_miss
     45   [ >lookup_insert_miss
     46     [ >(nth_append_first ? i prefix ?? Hi)
     47       @(Hpolicy i Hi)
     48     | @bitvector_of_nat_abs
     49       [ @(transitive_lt ??? Hi) ]
     50       [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
     51         @le_plus_n_r
     52       | @lt_to_not_eq @Hi
     53       ]
     54     ]
     55   | @bitvector_of_nat_abs
     56     [ @(transitive_lt ??? Hi) @le_S_to_le ]
     57     [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
     58       <plus_n_Sm @le_S_S @le_plus_n_r
     59     | @lt_to_not_eq @le_S @Hi
     60     ]
     61   ]
     62 | <Heq2 >Hi >lookup_insert_miss
     63   [ >lookup_insert_hit cases instr in Heq1;
     64     [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
     65     |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
     66       [1,3: <minus_n_n whd in match (nth ????); %
     67       |2,4: @le_n
     68       ]
     69     |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
     70       [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:
     71         [1,2,3,6,7,24,25: #x #y
     72         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
     73         <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
     74       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
     75         #_ #H @⊥ cases H #H2 @H2 %
     76       ]
     77     ]
     78   | @bitvector_of_nat_abs
     79     [ @le_S_to_le ]
     80     [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S
     81       >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     82     | @lt_to_not_eq @le_n
     83     ]
     84   ]
     85 ]
     86qed.
    587
    688(* One step in the search for a jump expansion fixpoint. *)
     
    97179    else
    98180      〈eqb final_added 0, Some ? final_policy〉.
    99 [ normalize nodelta @nmk #Habs lapply p generalize in match (foldl_strong ?????); *
     181[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
    100182  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
    101183  (* USE: inc_pc = fst of policy (from fold) *)
     
    129211    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
    130212  ]
    131 | normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
     213| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
    132214  >H2 in H; normalize nodelta -H2 -x #H @conj
    133215  [ @conj [ @conj
     
    153235  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    154236   * commented out for full proofs, but this needs a lot of memory and time *)
    155   [ (* not_jump_default *) cases daemon
    156     (* #i >append_length <commutative_plus #Hi normalize in Hi;
    157     cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    158     [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    159       [ >lookup_insert_miss
    160         [ >(nth_append_first ? i prefix ?? Hi)
    161           (* USE[pass]: not_jump_default *)
    162           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)
    163         | @bitvector_of_nat_abs
    164           [ @(transitive_lt ??? Hi) ]
    165           [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    166             @le_plus_n_r
    167           | @lt_to_not_eq @Hi
    168           ]
    169         ]
    170       | @bitvector_of_nat_abs
    171         [ @(transitive_lt ??? Hi) @le_S_to_le ]
    172         [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
    173           <plus_n_Sm @le_S_S @le_plus_n_r
    174         | @lt_to_not_eq @le_S @Hi
    175         ]
    176       ]
    177     | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
    178       [ >lookup_insert_hit cases instr in Heq1;
    179         [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    180         |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
    181           [1,3: <minus_n_n whd in match (nth ????); / by I/
    182           |2,4: @le_n
    183           ]
    184         |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
    185           [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:
    186             [1,2,3,6,7,24,25: #x #y
    187             |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
    188             <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    189           |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
    190             #_ #H @⊥ cases H #H2 @H2 / by I/
    191           ]
    192         ]
    193       | @bitvector_of_nat_abs
    194         [ @le_S_to_le ]
    195         [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S
    196           >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    197         | @lt_to_not_eq @le_n
    198         ]
    199       ]
    200     ] *)
    201   | (* 0 ↦ 0 *) cases daemon
    202     (* <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     237  [ (* not_jump_default *)
     238    cases (pair_destruct ?????? Heq2) -Heq2 #_ #Heq2
     239    @(jump_expansion_step1 … prf … Heq1 Heq2)
     240    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
     241  | (* 0 ↦ 0 *)
     242    <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    203243    [ cases (decidable_eq_nat 0 (|prefix|))
    204244      [ #Heq <Heq >lookup_insert_hit
     
    215255      ]
    216256    | @bitvector_of_nat_abs
    217       [3: @lt_to_not_eq / by / ]
     257      [3: @lt_to_not_eq @lt_O_S ]
    218258    ]
    219     [1,3: / by /
     259    [1,3: @lt_O_S
    220260    |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    221261      [2: <plus_n_Sm @le_S_S]
    222262      @le_plus_n_r
    223     ] *)
     263    ]
    224264  ]
    225265  | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
Note: See TracChangeset for help on using the changeset viewer.