Changeset 2316 for src/ASM/PolicyFront.ma
 Timestamp:
 Sep 3, 2012, 9:03:24 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2273 r2316 17 17 ∀i.i < 2^16 → (i > prefix ↔ bvt_lookup_opt … (bitvector_of_nat ? i) (\snd sigma) = None ?). 18 18 19 (* If instruction i is a jump, then there will be something in the policy at20 * position i *)21 definition is_jump' ≝22 λx:preinstruction Identifier.23 match x with24 [ JC _ ⇒ true25  JNC _ ⇒ true26  JZ _ ⇒ true27  JNZ _ ⇒ true28  JB _ _ ⇒ true29  JNB _ _ ⇒ true30  JBC _ _ ⇒ true31  CJNE _ _ ⇒ true32  DJNZ _ _ ⇒ true33  _ ⇒ false34 ].35 36 definition is_relative_jump ≝37 λinstr:pseudo_instruction.38 match instr with39 [ Instruction i ⇒ is_jump' i40  _ ⇒ false41 ].42 43 definition is_jump ≝44 λinstr:pseudo_instruction.45 match instr with46 [ Instruction i ⇒ is_jump' i47  Call _ ⇒ true48  Jmp _ ⇒ true49  _ ⇒ false50 ].51 52 definition is_call ≝53 λinstr:pseudo_instruction.54 match instr with55 [ Call _ ⇒ true56  _ ⇒ false57 ].58 59 definition is_jump_to ≝60 λx:pseudo_instruction.λd:Identifier.61 match x with62 [ Instruction i ⇒ match i with63 [ JC j ⇒ d = j64  JNC j ⇒ d = j65  JZ j ⇒ d = j66  JNZ j ⇒ d = j67  JB _ j ⇒ d = j68  JNB _ j ⇒ d = j69  JBC _ j ⇒ d = j70  CJNE _ j ⇒ d = j71  DJNZ _ j ⇒ d = j72  _ ⇒ False73 ]74  Call c ⇒ d = c75  Jmp j ⇒ d = j76  _ ⇒ False77 ].78 79 19 definition not_jump_default ≝ 80 20 λprefix:list labelled_instruction.λsigma:ppc_pc_map. … … 250 190  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 251 191 pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) 192 (λx.zero ?) 252 193 (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) 253 194 (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) … … 258 199 (* jumps are of the proper size *) 259 200 definition sigma_safe ≝ 260 λprefix:list labelled_instruction.λlabels:label_map. λadded:ℕ.201 λprefix:list labelled_instruction.λlabels:label_map. 261 202 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. 262 203 ∀i.i < prefix → 263 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in264 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in265 204 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in 266 205 ∀dest.is_jump_to instr dest → 267 let paddr ≝ lookup_def … labels dest 0 in 268 let addr ≝ bitvector_of_nat ? (if leb paddr (prefix) (* jump to address already known *) 269 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉) 270 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 206 let paddr ≝ lookup_def … labels dest 0 in 207 let 〈j,src,dest〉 ≝ 208 if leb paddr i then (* backward jump *) 209 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in 210 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in 211 let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in 212 〈j,pc_plus_jmp_length,addr〉 213 else 214 let 〈pc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉 in 215 let 〈npc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in 216 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd old_sigma) 〈0,short_jump〉)) in 217 let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)) in 218 〈j,pc_plus_jmp_length,addr〉 in 271 219 match j with 272 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ 273 bool_to_Prop (¬is_call instr) 274  absolute_jump ⇒ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧ 275 \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 276 bool_to_Prop (¬is_relative_jump instr) 277  long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 278 \fst (absolute_jump_cond pc_plus_jmp_length addr) = false 220 [ short_jump ⇒ \fst (short_jump_cond src dest) = true 221  absolute_jump ⇒ \fst (absolute_jump_cond src dest) = true (*∧ 222 \fst (short_jump_cond src dest) = false*) 223  long_jump ⇒ True (* do not talk about long jump *) 279 224 ]. 225 226 definition sigma_jumps ≝ 227 λprefix:list labelled_instruction.λsigma:ppc_pc_map. 228 ∀i.i < prefix → 229 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment []〉 in 230 (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump → 231 bool_to_Prop (¬is_call instr)) ∧ 232 (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = absolute_jump → 233 bool_to_Prop (¬is_relative_jump instr)). 280 234 281 235 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) … … 326 280 (* General note on jump length selection: the jump displacement is added/replaced 327 281 * AFTER the fetch (and attendant PC increase), but we calculate before the 328 * fetch, which means that in the case of a short and medium jump we are 2 329 * bytes off and have to compensate. 330 * For the long jump we don't care, because the PC gets replaced integrally anyway. *) 331 definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → 332 Identifier → jump_length ≝ 333 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. 334 let pc ≝ \fst inc_sigma in 335 let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in 336 let paddr ≝ lookup_def … labels lbl 0 in 337 let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) 338 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) 339 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 340 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in 282 * fetch, which means that we are [jump_length] bytes off and have to compensate. *) 283 definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → 284 Identifier → ℕ → jump_length ≝ 285 λlabels.λold_sigma.λinc_sigma.λppc.λlbl.λins_len. 286 let paddr ≝ lookup_def ?? labels lbl 0 in 287 let 〈src,dest〉 ≝ 288 if leb paddr ppc then (* backward jump *) 289 let pc ≝ \fst inc_sigma in 290 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in 291 〈bitvector_of_nat ? (pc+ins_len), bitvector_of_nat ? addr〉 292 else 293 let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in 294 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in 295 〈bitvector_of_nat ? (pc+ins_len), bitvector_of_nat ? addr〉 in 296 let 〈sj_possible, disp〉 ≝ short_jump_cond src dest in 341 297 if sj_possible 342 298 then short_jump 343 299 else long_jump. 344 300 345 definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →301 definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → 346 302 Identifier → jump_length ≝ 347 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. 348 let pc ≝ \fst inc_sigma in 349 let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in 350 let paddr ≝ lookup_def ? ? labels lbl 0 in 351 let addr ≝ bitvector_of_nat ? 352 (if leb paddr ppc (* jump to address already known *) 353 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) 354 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 355 let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in 303 λlabels.λold_sigma.λinc_sigma.λppc.λlbl. 304 let paddr ≝ lookup_def ?? labels lbl 0 in 305 let 〈src,dest〉 ≝ 306 if leb paddr ppc then (* backward jump *) 307 let pc ≝ \fst inc_sigma in 308 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in 309 〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 310 else 311 let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in 312 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in 313 〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 in 314 let 〈aj_possible, disp〉 ≝ absolute_jump_cond src dest in 356 315 if aj_possible 357 316 then absolute_jump 358 317 else long_jump. 359 318 360 definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →319 definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → 361 320 Identifier → jump_length ≝ 362 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. 363 let pc ≝ \fst inc_sigma in 364 let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in 365 let paddr ≝ lookup_def … labels lbl 0 in 366 let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) 367 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) 368 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 369 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in 321 λlabels.λold_sigma.λinc_sigma.λppc.λlbl. 322 let paddr ≝ lookup_def ?? labels lbl 0 in 323 let 〈src,dest〉 ≝ 324 if leb paddr ppc then (* backward jump *) 325 let pc ≝ \fst inc_sigma in 326 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in 327 〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 328 else 329 let pc ≝ \fst (bvt_lookup … (bitvector_of_nat ? ppc) (\snd old_sigma) 〈0,short_jump〉) in 330 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) in 331 〈bitvector_of_nat ? (pc+2), bitvector_of_nat ? addr〉 in 332 let 〈sj_possible, disp〉 ≝ short_jump_cond src dest in 370 333 if sj_possible 371 334 then short_jump 372 else select_call_length labels old_sigma inc_sigma addedppc lbl.335 else select_call_length labels old_sigma inc_sigma ppc lbl. 373 336 374 337 definition destination_of: preinstruction Identifier → option Identifier ≝ … … 387 350 ]. 388 351 352 definition length_of: preinstruction Identifier → ℕ ≝ 353 λi. 354 match i with 355 [ JC j ⇒ 2 356  JNC j ⇒ 2 357  JZ j ⇒ 2 358  JNZ j ⇒ 2 359  JB _ j ⇒ 3 360  JBC _ j ⇒ 3 361  JNB _ j ⇒ 3 362  CJNE _ j ⇒ 3 363  DJNZ x j ⇒ match x with [ REGISTER _ ⇒ 2  _ ⇒ 3 ] 364  _ ⇒ 0 365 ]. 366 389 367 definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → 390 ℕ → ℕ → preinstruction Identifier → option jump_length ≝ 391 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi. 368 ℕ → preinstruction Identifier → option jump_length ≝ 369 λlabels.λold_sigma.λinc_sigma.λppc.λi. 370 let ins_len ≝ length_of i in 392 371 match destination_of i with 393 [ Some j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)372 [ Some j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma ppc j ins_len) 394 373  None ⇒ None ? 395 374 ]. … … 470 449 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 471 450  @bitvector_of_nat_abs 472 [ / by /451 [ @ltb_true_to_lt / by refl/ 473 452  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm 474 453 @le_S_S @le_plus_n_r 475  @lt_to_not_eq / by /454  @lt_to_not_eq @ltb_true_to_lt / by refl/ 476 455 ] 477 456 ] … … 617 596 #a #b #i cases i 618 597 [2,3,6: #x [3: #y] #H cases H 619 4,5: #id #_ cases a cases b / by le_n/598 4,5: #id #_ cases a cases b @leb_true_to_le / by refl/ 620 599 1: #pi cases pi 621 600 try (#x #y #H) try (#x #H) try (#H) cases H … … 630 609 ∀old_sigma.∀sigma. 631 610 sigma_pc_equal program old_sigma sigma → 632 sigma_safe program (create_label_map program) 0 old_sigma sigma → 611 sigma_jump_equal program old_sigma sigma → 612 sigma_jumps program old_sigma → 613 sigma_safe program (create_label_map program) old_sigma sigma → 633 614 sigma_compact_unsafe program (create_label_map program) sigma → 634 615 sigma_compact program (create_label_map program) sigma. 635 #program cases program program #program #Hprogram #old_sigma #sigma #Hequal636 #H safe #Hcp_unsafe #i #Hi637 lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)616 #program cases program program #program #Hprogram #old_sigma #sigma 617 #Hpc_equal #Hjump_equal #Hjumps #Hsafe #Hcp_unsafe #i #Hi 618 lapply (Hcp_unsafe i Hi) Hcp_unsafe lapply (Hsafe i Hi) Hsafe 638 619 inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) 639 620 [ / by / 640  #x cases x x # x1 #x2#EQ641 cases(lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma))621  #x cases x x #pc #jl #EQ 622 inversion (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma)) 642 623 [ / by / 643  # y cases y y #y1 #y2 normalize nodelta #H #H2624  #x cases x x #Spc #Sjl #SEQ normalize nodelta #Hsafe #Hcp_unsafe 644 625 (*CSC: make a lemma here; to shorten the proof, reimplement the 645 626 safe case so that it also does a pattern matching on the jump_length 646 627 type *) 647 cut (instruction_size_jmplen x2628 cut (instruction_size_jmplen jl 648 629 (\snd (nth i ? program 〈None ?, Comment []〉)) = 649 630 instruction_size … (bitvector_of_nat ? i) 650 631 (\snd (nth i ? program 〈None ?, Comment []〉))) 651 [ 5: #H3 <H3 @H2652  4: whd in match (instruction_size_jmplen ??);653 whd in match (instruction_size …); 632 [6: #H <H @Hcp_unsafe 633 5: whd in match (instruction_size_jmplen ??); 634 whd in match (instruction_size …); 654 635 whd in match (assembly_1_pseudoinstruction …); 655 636 whd in match (expand_pseudo_instruction …); 656 normalize nodelta whd in match (append …) in H; lapply H 657 inversion (nth i ? program 〈None ?,Comment []〉) 637 normalize nodelta inversion (nth i ? program 〈None ?,Comment []〉) in Hsafe; 658 638 #lbl #instr cases instr 659 [2,3,6: #x [3: #y] normalize nodelta #H #_ % 660 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Heq #Hj 661 lapply (Hj x (refl ? x)) Hj normalize nodelta 639 [1: #pi normalize nodelta cases pi 640 try (#x #id #Hnth_eq #Hsafe) try (#id #Hnth_eq #Hsafe) try (#Hnth_eq #Hsafe) 641 try % lapply Hsafe Hsafe lapply Hnth_eq Hnth_eq lapply id id 642 2,3,6: #x [3: #y] normalize nodelta #Hnth_eq #_ %] 643 #id lapply (Hpc_equal i (le_S_to_le … Hi)) 644 lapply (Hpc_equal (S i) Hi) 645 lapply (Hjump_equal i Hi) 646 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #jeq #OSeq #Oeq #Hnth_eq #Hsafe 647 lapply (Hsafe id (refl ? id)) Hsafe normalize nodelta 648 whd in match expand_relative_jump; 649 whd in match expand_relative_jump_internal; normalize nodelta 662 650 >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O 663 cases x2 normalize nodelta 664 [1,4: whd in match short_jump_cond; normalize nodelta 665 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 666 [1,3: cases (create_label_map program) #clm #Hclm 667 @le_S_to_le @(Hclm x ?) 668 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 669 2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] 670 [1,4: >nat_of_bitvector_bitvector_of_nat_inverse 671 [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 672 2,5: whd in match fetch_pseudo_instruction; normalize nodelta 673 >nth_safe_nth 674 [1,3: >nat_of_bitvector_bitvector_of_nat_inverse 675 [1,3: >Heq / by refl/ 676 2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 677 ] 678 ] 679 3,6: / by / 651 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) in OSeq; #OSeq >Hcp_unsafe 652 inversion (leb (lookup_def … (create_label_map program) id 0) i) #Hli 653 normalize nodelta 654 [1,3,5,7,9,11,13,15,17,19,21: (* JC JNC JB JNB JBC JZ JNZ CJNE DJNZ Jmp Call *) 655 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 656 cases jl in jeq; normalize nodelta #jeq 657 [2,5,8,11,14,17,20,23,26: lapply (Hjumps i Hi) >Hnth_eq >jeq normalize nodelta #abs 658 cases ((proj2 ?? abs) (refl ? absolute_jump)) (* no absolute reljmps *) 659 31: lapply (Hjumps i Hi) >Hnth_eq >jeq normalize nodelta #abs 660 cases ((proj1 ?? abs) (refl ? short_jump)) (* no short calls *) 661 28: >Hnth_eq #Hold cases (short_jump_cond ??) in Hold; 662 #sj_poss #disp #Hold normalize nodelta >Hold normalize nodelta % 663 1,4,7,10,13,16,19,22,25: >Hnth_eq #Hold cases (short_jump_cond ??) in Hold; 664 #sj_poss #disp #Hold normalize nodelta >Hold 665 try % try (@(subaddressing_mode_elim … x) #w %) 666 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % 667 @(subaddressing_mode_elim … a1) #w % 668 3,6,9,12,15,18,21,24,27: >Hnth_eq #_ whd in match (jmpeqb ??); 669 cases (short_jump_cond ??); #sj_poss #disp normalize nodelta 670 cases sj_poss normalize nodelta try % try (@(subaddressing_mode_elim … x) #w %) 671 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % 672 @(subaddressing_mode_elim … a1) #w % 673 29,32: >Hnth_eq #Hold cases (absolute_jump_cond ??) in Hold; 674 #aj_poss #disp #Hold >Hold normalize nodelta 675 cases (short_jump_cond ??); 676 [1,2: #sj_poss #disp2 normalize nodelta cases sj_poss % 677 3,4: @(zero 16) 680 678 ] 681 2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 682 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 683 #result #flags normalize nodelta 684 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 685 cases (get_index' bool 2 0 flags) normalize nodelta 686 [3,4: #H cases (proj2 ?? H) 687 1,2: cases (eq_bv 9 upper ?) 688 [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3) 689 1,3: #_ normalize nodelta @refl 679 30,33: >Hnth_eq #_ whd in match (jmpeqb ??); cases (absolute_jump_cond ??); 680 #mj_poss #disp2 normalize nodelta cases (short_jump_cond ??); 681 [1,2: #sj_poss #disp normalize nodelta cases sj_poss cases mj_poss % 682 3,4: @(zero 16) (* where does this come from? *) 690 683 ] 691 684 ] 685 *: cases (lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) in Oeq jeq; 686 #opc #ojl #Oeq #jeq normalize nodelta 687 cases (lookup … (bitvector_of_nat ? (S i)) (\snd old_sigma) 〈0,short_jump〉) in OSeq; 688 #oSpc #oSjl #OSeq normalize nodelta >jeq 689 >OSeq >Hcp_unsafe Hcp_unsafe >Hnth_eq lapply (Hpc_equal (lookup_def … (create_label_map program) id 0) ?) 690 [1,3,5,7,9,11,13,15,17,19,21: 691 @(le_S_to_le … (pi2 ?? (create_label_map program) id ?)) 692 cut (i < 2^16) 693 [1,3,5,7,9,11,13,15,17,19,21: 694 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ] #Hi2 695 @(proj2 ?? ((proj2 ?? Hprogram) id (bitvector_of_nat ? i) ???)) 696 [1,5,9,13,17,21,25,29,33,37,41: 697 whd in match fetch_pseudo_instruction; normalize nodelta 698 >(nth_safe_nth … 〈None ?, Comment []〉) >nat_of_bitvector_bitvector_of_nat_inverse 699 [1: >Hnth_eq in ⊢ (??%?); 700 3: >Hnth_eq in ⊢ (??%?); 701 5: >Hnth_eq in ⊢ (??%?); 702 7: >Hnth_eq in ⊢ (??%?); 703 9: >Hnth_eq in ⊢ (??%?); 704 11: >Hnth_eq in ⊢ (??%?); 705 13: >Hnth_eq in ⊢ (??%?); 706 15: >Hnth_eq in ⊢ (??%?); 707 17: >Hnth_eq in ⊢ (??%?); 708 19: >Hnth_eq in ⊢ (??%?); 709 21: >Hnth_eq in ⊢ (??%?); ] 710 [1,2,3,4,5,6,7,8,9,10,11: % 711 *: assumption] 712 3,7,11,15,19,23,27,31,35,39,43: 713 >nat_of_bitvector_bitvector_of_nat_inverse assumption 714 4,8,12,16,20,24,28,32,36,40,44: % 715 ] 716 *: #Hpc lapply (Hjumps i Hi) >Hnth_eq >(Hjump_equal i Hi) 717 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 718 cases jl normalize nodelta 719 [31: #abs cases ((proj1 ?? abs) (refl ? short_jump)) (* no short calls *) 720 2,5,8,11,14,17,20,23,26: #abs cases ((proj2 ?? abs) (refl ? absolute_jump)) (* no absolute RJs *) 721 1,4,7,10,13,16,19,22,25,28: 722 >Hpc cases (short_jump_cond ??); #sj_poss #disp #_ #H normalize nodelta 723 >H normalize nodelta try % try (@(subaddressing_mode_elim … x) #w %) 724 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % 725 @(subaddressing_mode_elim … a1) #w % 726 3,6,9,12,15,18,21,24,27: >Hpc #_ #_ cases (short_jump_cond ??); 727 #sj_poss #disp normalize nodelta normalize nodelta 728 whd in match (jmpeqb ??); cases sj_poss 729 try % try (@(subaddressing_mode_elim … x) #w %) 730 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % 731 @(subaddressing_mode_elim … a1) #w % 732 29,32: >Hpc #_ #Hold cases (absolute_jump_cond ??) in Hold; 733 #aj_poss #disp #Hold >Hold normalize nodelta cases (short_jump_cond ??) 734 [1,2: #sj_poss #disp2 cases sj_poss normalize nodelta % 735 3,4: @(zero 16) 736 ] 737 30,33: >Hnth_eq #_ #_ whd in match (jmpeqb ??); cases (absolute_jump_cond ??); 738 #mj_poss #disp2 normalize nodelta cases (short_jump_cond ??); 739 [1,2: #sj_poss #disp normalize nodelta cases sj_poss cases mj_poss % 740 3,4: @(zero 16) 741 ] 742 ] 692 743 ] 693 2,3,5,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 694 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 695 [1,3,5,7: cases (create_label_map program) #clm #Hclm 696 @le_S_to_le @(Hclm x ?) 697 [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 698 3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] 699 [1,4,7,10: >nat_of_bitvector_bitvector_of_nat_inverse 700 [2,4,6,8: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 701 2,5,8,11: whd in match fetch_pseudo_instruction; normalize nodelta 702 >nth_safe_nth 703 [1,3,5,7: >nat_of_bitvector_bitvector_of_nat_inverse 704 [1,3,5,7: >Heq / by refl/ 705 *: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 706 ] 707 ] 708 *: / by / 709 ] 710 *: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 711 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 712 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 713 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 714 #result #flags normalize nodelta 715 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 716 cases (get_index' bool 2 0 flags) normalize nodelta 717 #H 718 [1,2,5,6: >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 719 *: >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 720 ]]] 721 1: normalize nodelta 722 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 723 [#A #B * / by refl/] #fst_foo 724 cut (∀x. 725 instruction_has_label x (\snd (nth i labelled_instruction program 〈None (identifier ASMTag),Comment []〉)) → 726 lookup_def ?? (create_label_map program) x 0 ≤ (program)) 727 [#x #Heq cases (create_label_map program) #clm #Hclm 728 @le_S_to_le @(Hclm x ?) 729 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 730 [ >nat_of_bitvector_bitvector_of_nat_inverse 731 [2: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 732  whd in match fetch_pseudo_instruction; normalize nodelta 733 >nth_safe_nth 734 [ >nat_of_bitvector_bitvector_of_nat_inverse 735 [ @pair_elim // ] 736 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ] 737  assumption ]] #lookup_in_program 738 H #pi cases pi 739 try (#y #x #Heq #H) try (#x #Heq #H) try (#Heq #H) try % lapply H H 740 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 741 #Hj lapply (Hj x (refl ? x)) Hj 742 whd in match expand_relative_jump; normalize nodelta 743 whd in match expand_relative_jump_internal; normalize nodelta 744 whd in match expand_relative_jump_unsafe; normalize nodelta 745 whd in match expand_relative_jump_internal_unsafe; 746 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 747 <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta 748 [1,4,7,10,13,16,19,22,25: 749 >fst_foo @pair_elim #sj_possible #disp #H #H2 750 @(pair_replace ?????????? (eq_to_jmeq … H)) 751 [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …)) 752 try % >Heq % ] 753 >(proj1 ?? H2) try (@refl) normalize nodelta 754 [1,2,3,5: @(subaddressing_mode_elim … y) #w % 755  cases y * #sth #sth2 @(subaddressing_mode_elim … sth) 756 @(subaddressing_mode_elim … sth2) #x [3,4: #x2] % 757 ] 758 2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs 759 ] 760 * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H 761 @(pair_replace ?????????? (eq_to_jmeq … H)) 762 [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …)) 763 try % >Heq % ] 764 #H2 >H2 try (@refl) normalize nodelta 765 [1,2,3,5: @(subaddressing_mode_elim … y) #w % 766  cases y * #sth #sth2 @(subaddressing_mode_elim … sth2) #w 767 [1,2: %] whd in match (map ????); whd in match (flatten ??); 768 whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%); 769 >length_append >length_append %]]]]] 744 ] 745 ] 746 ] 747 ] 770 748 qed. 771 749
Note: See TracChangeset
for help on using the changeset viewer.