- Timestamp:
- Jul 23, 2012, 10:46:06 PM (8 years ago)
- File:
-
- 1 edited
-
src/ASM/PolicyStep.ma (modified) (12 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/PolicyStep.ma
r2225 r2236 103 103 qed. 104 104 105 (* 105 lemma destination_of_None_to_is_jump_false: 106 ∀instr. destination_of instr = None … → is_jump' instr = false. 107 * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs) 108 qed. 109 110 lemma destination_of_Some_to_is_jump_true: 111 ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true. 112 #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs 113 destruct(abs) 114 qed. 115 106 116 lemma jump_expansion_step3: 107 (* 108 program : 109 (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l) 110 labels : 111 (Σlm:label_map 112 .(∀l:identifier ASMTag 117 ∀program.(* : 118 (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*) 119 ∀labels : 120 label_map(*Σlm:label_map 121 .∀l:identifier ASMTag 113 122 .occurs_exactly_once ASMTag pseudo_instruction l program 114 123 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 115 =address_of_word_labels_code_mem program l) )*)124 =address_of_word_labels_code_mem program l).*). 116 125 ∀old_sigma : 117 126 Σpolicy:ppc_pc_map 118 . True(*not_jump_default program policy119 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy)127 .not_jump_default program policy 128 (*∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 120 129 〈O,short_jump〉) 121 130 =O … … 125 134 ∧sigma_compact_unsafe program labels policy 126 135 ∧\fst policy≤ 2 \sup 16*). 127 ∀prefix : list (option Identifier×pseudo_instruction). (*128 x : (option Identifier×pseudo_instruction)129 tl : (list (option Identifier×pseudo_instruction))130 prf : (program=prefix@[x]@tl)136 ∀prefix : list (option Identifier×pseudo_instruction). 137 ∀x : option Identifier×pseudo_instruction. 138 ∀tl : list (option Identifier×pseudo_instruction). 139 ∀prf : program=prefix@[x]@tl.(* 131 140 acc : 132 141 (Σx0:ℕ×ppc_pc_map … … 149 158 (\snd old_sigma) 〈O,short_jump〉) 150 159 +added 151 ∧sigma_safe prefix labels added old_sigma policy)) 152 inc_added : ℕ153 inc_pc_sigma : ppc_pc_map160 ∧sigma_safe prefix labels added old_sigma policy))*) 161 ∀inc_added : ℕ. 162 ∀inc_pc_sigma : ppc_pc_map. (* 154 163 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 155 164 ∀label : option Identifier. 156 ∀instr : pseudo_instruction. (*157 p1 : (x≃〈label,instr〉)165 ∀instr : pseudo_instruction. 166 ∀p1 : x≃〈label,instr〉.(* 158 167 add_instr ≝ 159 168 match instr … … 172 181 Some jump_length 173 182 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 174 |Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 175 inc_pc : ℕ176 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)177 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 178 old_pc : ℕ179 old_length : jump_length180 Holdeq :181 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma)183 |Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length]*) 184 ∀inc_pc : ℕ. 185 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).(* 186 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*) 187 ∀old_pc : ℕ. 188 ∀old_length : jump_length. 189 ∀Holdeq : 190 lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) 182 191 〈O,short_jump〉 183 =〈old_pc,old_length〉 )184 Hpolicy :185 ( not_jump_default prefix 〈inc_pc,inc_sigma〉192 =〈old_pc,old_length〉. 193 ∀Hpolicy : 194 (*not_jump_default prefix 〈inc_pc,inc_sigma〉 186 195 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 187 196 〈O,short_jump〉) … … 190 199 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma 191 200 〈O,short_jump〉) 192 ∧ jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉201 ∧*)jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉(* 193 202 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 194 203 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) … … 198 207 〈O,short_jump〉) 199 208 =old_pc+inc_added 200 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉) 201 added : ℕ*)209 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*). 210 (* added : ℕ*) 202 211 ∀policy : ppc_pc_map. 203 (*new_length : jump_length204 isize : ℕ205 Heq1 :206 (match212 ∀new_length : jump_length. 213 ∀isize : ℕ. 214 ∀Heq1 : 215 match 207 216 match instr 208 217 in pseudo_instruction … … 220 229 Some jump_length 221 230 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 222 |Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length]231 |Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length] 223 232 in option 224 return λ_ 0:(option jump_length).(jump_length×ℕ)233 return λ_:(option jump_length).(jump_length×ℕ) 225 234 with 226 235 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 … … 228 237 〈max_length old_length pl, 229 238 instruction_size_jmplen (max_length old_length pl) instr〉] 230 =〈new_length,isize〉 )231 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )232 prefix_ok : (|prefix|< 2 \sup 16 )239 =〈new_length,isize〉. 240 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16. 241 ∀prefix_ok : |prefix|< 2 \sup 16.(* 233 242 Heq2a : 234 243 (match … … 255 264 |Some (x0:jump_length)⇒ 256 265 inc_added+(isize-instruction_size_jmplen old_length instr)] 257 =added) 258 Heq2b :259 (〈inc_pc+isize,266 =added)*) 267 ∀Heq2b : 268 〈inc_pc+isize, 260 269 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|))) 261 270 〈inc_pc+isize, … … 264 273 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 265 274 〈inc_pc,new_length〉 inc_sigma)〉 266 =policy )*)275 =policy. 267 276 jump_increase (prefix@[〈label,instr〉]) old_sigma policy. 268 #old_sigma #prefix #label #instr #policy 277 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label 278 #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy #policy #new_length 279 #isize #Heq1 #prefix_ok1 #prefix_ok #Heq2 269 280 #i >append_length >commutative_plus #Hi normalize in Hi; 270 281 cases (le_to_or_lt_eq … Hi) -Hi; #Hi 271 282 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 272 283 [ (* USE[pass]: jump_increase *) 273 lapply ( proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))i (le_S_to_le … Hi))274 < (proj2 ?? (pair_destruct ?????? Heq2))284 lapply (Hpolicy i (le_S_to_le … Hi)) 285 <Heq2 275 286 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 276 287 [ >lookup_insert_miss … … 278 289 | @bitvector_of_nat_abs 279 290 [ @(transitive_lt ??? Hi) ] 280 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 281 @le_S_S @le_plus_n_r 291 [1,2: assumption 282 292 | @lt_to_not_eq @Hi 283 293 ] … … 285 295 | @bitvector_of_nat_abs 286 296 [ @(transitive_lt ??? Hi) @le_S_to_le ] 287 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 288 >append_length @le_S_S <plus_n_Sm @le_plus_n_r 297 [1,2: assumption 289 298 | @lt_to_not_eq @le_S @Hi 290 299 ] 291 300 ] 292 | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta 301 | >Hi <Heq2 >Holdeq normalize nodelta 302 cut (|prefix| < |program|) 303 [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program 293 304 >lookup_insert_miss 294 [ >lookup_insert_hit cases (dec_is_jump instr)305 [ >lookup_insert_hit inversion (is_jump instr) normalize nodelta 295 306 [ cases instr in Heq1; normalize nodelta 296 [ #pi cases pi 297 [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: 298 [1,2,3,6,7,24,25: #x #y 299 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj 300 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 301 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 302 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) 303 @jmpleq_max_length 304 ] 305 |2,3,6: #x [3: #y] #_ #Hj cases Hj 307 [ #pi whd in match jump_expansion_step_instruction; normalize nodelta 308 lapply (destination_of_None_to_is_jump_false pi) 309 cases (destination_of ?) normalize nodelta 310 [ #abs #_ whd in match is_jump; normalize nodelta >abs try % #abs' 311 destruct(abs') 312 | #tgt #_ #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 313 ] 314 |2,3,6: #x [3: #y] #_ #Hj normalize in Hj; destruct(Hj) 306 315 |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 307 316 ] 308 | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta 309 [ #pi cases pi 310 [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: 311 [1,2,3,6,7,24,25: #x #y 312 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 313 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 314 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 315 (* USE: not_jump_default (from old_sigma) *) 316 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??) 317 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 318 >prf >nth_append_second 319 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 320 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 321 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 322 @le_n 323 ] 324 |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 325 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 326 |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 327 >Holdeq #EQ2 >EQ2 %2 @refl 317 | lapply Heq1 -Heq1; inversion instr normalize nodelta 318 [ 4,5: #x #_ #_ #abs @⊥ normalize in abs; destruct(abs) 319 | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta 320 lapply (destination_of_Some_to_is_jump_true pi) 321 cases (destination_of pi) normalize nodelta 322 [2: #tgt #abs #_ whd in match is_jump; normalize nodelta >abs try % 323 #abs' destruct(abs')] 324 #_ 325 |*: #x [3: #y] #Heqi ] 326 #Hj #Hx <(proj1 ?? (pair_destruct ?????? Hj)) 327 lapply (pi2 ?? old_sigma (|prefix|) ??) 328 [1,4,7,10: >prf >nth_append_second 329 [1,3,5,7: <minus_n_n whd in match (nth ????); >p1 >Heqi >Hj try % >Hx % 330 |*: @le_n 328 331 ] 329 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 330 #_ #_ #abs @⊥ @(absurd ? I abs) 331 ] 332 |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 333 (* USE: not_jump_default (from old_sigma) *) 334 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??) 335 [1,4,7: >prf >nth_append_second 336 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj 337 |2,4,6: @le_n 338 ] 339 |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 340 |3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl 341 ] 342 |4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs) 343 ] 344 ] 332 |2,5,8,11: @lt_prefix_program 333 |*: >Holdeq #EQ2 >EQ2 %2 @refl]] 345 334 | @bitvector_of_nat_abs 346 335 [ @le_S_to_le ] 347 [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf 348 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 336 [1,2: assumption 349 337 | @lt_to_not_eq @le_n 350 338 ] 351 339 ] 352 340 ] 353 | < (proj2 ?? (pair_destruct ?????? Heq2))>Hi >lookup_insert_hit341 | <Heq2 >Hi >lookup_insert_hit 354 342 normalize nodelta 355 343 cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉) 356 344 #a #b normalize nodelta %2 @refl 357 345 ] 358 ] 359 qed.*) 346 qed. 360 347 361 348 (* One step in the search for a jump expansion fixpoint. *)
Note: See TracChangeset
for help on using the changeset viewer.
