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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2211 r2215 3 3 include alias "arithmetics/nat.ma". 4 4 include alias "basics/logic.ma". 5 6 lemma 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 ] 86 qed. 5 87 6 88 (* One step in the search for a jump expansion fixpoint. *) … … 97 179 else 98 180 〈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.?) ???) 100 182 #x #H #Heq >Heq in H; normalize nodelta Heq x #Hind 101 183 (* USE: inc_pc = fst of policy (from fold) *) … … 129 211 @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge 130 212 ] 131  normalize nodelta lapply p generalize in match (foldl_strong ?????); *#x #H #H2213  normalize nodelta lapply p p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2 132 214 >H2 in H; normalize nodelta H2 x #H @conj 133 215 [ @conj [ @conj … … 153 235 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 154 236 * 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 203 243 [ cases (decidable_eq_nat 0 (prefix)) 204 244 [ #Heq <Heq >lookup_insert_hit … … 215 255 ] 216 256  @bitvector_of_nat_abs 217 [3: @lt_to_not_eq / by /]257 [3: @lt_to_not_eq @lt_O_S ] 218 258 ] 219 [1,3: / by /259 [1,3: @lt_O_S 220 260 2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 221 261 [2: <plus_n_Sm @le_S_S] 222 262 @le_plus_n_r 223 ] *)263 ] 224 264 ] 225 265  (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
Note: See TracChangeset
for help on using the changeset viewer.