Changeset 1809
 Timestamp:
 Mar 7, 2012, 1:27:17 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1615 r1809 8 8 include "ASM/Assembly.ma". 9 9 10 definition max_length: jump_length → jump_length → jump_length ≝ 11 λj1.λj2. 12 match j1 with 13 [ long_jump ⇒ long_jump 14  medium_jump ⇒ 15 match j2 with 16 [ long_jump ⇒ long_jump 17  _ ⇒ medium_jump 18 ] 19  short_jump ⇒ j2 10 (* Internal types *) 11 12 (* label_map: identifier ↦ 〈instruction number, address〉 *) 13 definition label_map ≝ identifier_map ASMTag (ℕ × ℕ). 14 15 (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *) 16 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16. 17 18 (* The different properties that we want/need to prove at some point *) 19 (* Anything that's not in the program doesn't end up in the policy *) 20 definition out_of_program_none ≝ 21 λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. 22 ∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?. 23 24 (* If instruction i is a jump, then there will be something in the policy at 25 * position i *) 26 definition is_jump' ≝ 27 λx:preinstruction Identifier. 28 match x with 29 [ JC _ ⇒ True 30  JNC _ ⇒ True 31  JZ _ ⇒ True 32  JNZ _ ⇒ True 33  JB _ _ ⇒ True 34  JNB _ _ ⇒ True 35  JBC _ _ ⇒ True 36  CJNE _ _ ⇒ True 37  DJNZ _ _ ⇒ True 38  _ ⇒ False 20 39 ]. 21 40 41 definition is_jump ≝ 42 λx:labelled_instruction. 43 let 〈label,instr〉 ≝ x in 44 match instr with 45 [ Instruction i ⇒ is_jump' i 46  Call _ ⇒ True 47  Jmp _ ⇒ True 48  _ ⇒ False 49 ]. 50 51 definition jump_in_policy ≝ 52 λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. 53 ∀i:ℕ.i < prefix → 54 (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔ 55 ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉). 56 57 definition labels_okay ≝ 58 λlabels:label_map.λpolicy:jump_expansion_policy. 59 bvt_forall ?? policy (λn.λx.let 〈pc,addr_nat,i〉 ≝ x in 60 ∃id:Identifier. 61 \snd (lookup_def … labels id 〈0,pc〉) = addr_nat 62 ). 63 64 (* Between two policies, jumps cannot decrease *) 22 65 definition jmple: jump_length → jump_length → Prop ≝ 23 66 λj1.λj2. … … 39 82 λj1.λj2.jmple j1 j2 ∨ j1 = j2. 40 83 84 definition policy_increase: list labelled_instruction → jump_expansion_policy → 85 jump_expansion_policy → Prop ≝ 86 λprogram.λop.λp. 87 (∀i:ℕ.i < program → 88 let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in 89 let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in 90 jmpleq oj j). 91 92 (* Policy safety *) 93 definition policy_safe: jump_expansion_policy → Prop ≝ 94 λpolicy. 95 bvt_forall ?? policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in 96 match jmp_len with 97 [ short_jump ⇒ if leb pc_nat addr_nat 98 then le (addr_nat  pc_nat) 126 99 else le (pc_nat  addr_nat) 129 100  medium_jump ⇒ 101 let addr ≝ bitvector_of_nat 16 addr_nat in 102 let pc ≝ bitvector_of_nat 16 pc_nat in 103 let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in 104 let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in 105 eq_bv 5 fst_5_addr fst_5_pc = true 106  long_jump ⇒ True 107 ] 108 ). 109 110 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) 111 definition max_length: jump_length → jump_length → jump_length ≝ 112 λj1.λj2. 113 match j1 with 114 [ long_jump ⇒ long_jump 115  medium_jump ⇒ 116 match j2 with 117 [ medium_jump ⇒ medium_jump 118  _ ⇒ long_jump 119 ] 120  short_jump ⇒ 121 match j2 with 122 [ short_jump ⇒ short_jump 123  _ ⇒ long_jump 124 ] 125 ]. 126 41 127 lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y). 42 128 #x #y cases x cases y /3 by inl, inr, nmk, I/ … … 54 140 qed. 55 141 56 57 (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *) 58 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16. 59 60 (* label_map: identifier ↦ 〈instruction number, address〉 *) 61 definition label_map ≝ identifier_map ASMTag (nat × nat). 62 142 (* Labels *) 63 143 definition is_label ≝ 64 144 λx:labelled_instruction.λl:Identifier. … … 68 148  _ ⇒ False 69 149 ]. 70 71 definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝72 λpc.λjmp_len.λinstr.73 let bv_pc ≝ bitvector_of_nat 16 pc in74 let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in75 let bv: list (BitVector 8) ≝ match ilist with76 [ None ⇒ (* this shouldn't happen *) [ ]77  Some l ⇒ flatten … (map … assembly1 l)78 ] in79 pc + (bv).80 150 81 151 lemma label_does_not_occur: … … 89 159  #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??); 90 160 whd in Heq; >Heq 91 >eq_identifier_refl / /161 >eq_identifier_refl / by refl/ 92 162 ] 93 163  #i #H whd in match (does_not_occur ??); … … 96 166 [ @(IH i) @H 97 167  #l' @eq_identifier_elim 98 [ normalize / /168 [ normalize / by / 99 169  normalize #_ @(IH i) @H 100 170 ] … … 102 172 ] 103 173 ] 104 qed. 105 174 qed. 175 176 definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝ 177 λpc.λjmp_len.λinstr. 178 let bv_pc ≝ bitvector_of_nat 16 pc in 179 let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) bv_pc jmp_len ? instr in 180 let bv: list (BitVector 8) ≝ match ilist with 181 [ None ⇒ (* this shouldn't happen *) [ ] 182  Some l ⇒ flatten … (map … assembly1 l) 183 ] in 184 pc + (bv). 185 @(λx.bv_pc) 186 qed. 187 188 (* The function that creates the labeltoaddress map *) 106 189 definition create_label_map: ∀program:list labelled_instruction. 107 190 ∀policy:jump_expansion_policy. … … 146 229  normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?) 147 230 [ #addr #Haddr % [ @addr  <Haddr @lookup_add_miss /2/ ] 148  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / /231  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / by / 149 232 ] 150 233 ] 151 >(label_does_not_occur i … Hl) normalize nodelta @nmk / /234 >(label_does_not_occur i … Hl) normalize nodelta @nmk / by / 152 235 ] 153 236  #Hi #l #Hocc >(injective_S … Hi) >nth_append_second … … 212 295 ]. 213 296 214 definition is_jump' ≝215 λx:preinstruction Identifier.216 match x with217 [ JC _ ⇒ True218  JNC _ ⇒ True219  JZ _ ⇒ True220  JNZ _ ⇒ True221  JB _ _ ⇒ True222  JNB _ _ ⇒ True223  JBC _ _ ⇒ True224  CJNE _ _ ⇒ True225  DJNZ _ _ ⇒ True226  _ ⇒ False227 ].228 229 definition is_jump ≝230 λx:labelled_instruction.231 let 〈label,instr〉 ≝ x in232 match instr with233 [ Instruction i ⇒ is_jump' i234  Call _ ⇒ True235  Jmp _ ⇒ True236  _ ⇒ False237 ].238 239 297 lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x). 240 298 #x cases x #l #i cases i … … 245 303 #x %2 whd in match (is_jump ?); /2 by nmk/ 246 304 35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ 247 9,10,14,15: #x %1 / /248 11,12,13,16,17: #x #y %1 / /305 9,10,14,15: #x %1 / by I/ 306 11,12,13,16,17: #x #y %1 / by I/ 249 307 ] 250 308 2,3: #x %2 /2 by nmk/ 251 4,5: #x %1 / /309 4,5: #x %1 / by I/ 252 310 6: #x #y %2 /2 by nmk/ 253 311 ] 254 312 qed. 255 256 257 definition jump_in_policy ≝ 258 λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. 259 ∀i:ℕ.i < prefix → 260 (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔ 261 ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉). 262 263 (* these should be moved to BitVector at some point *) 313 314 (* these should be moved to BitVector at some point, and proven *) 264 315 lemma bitvector_of_nat_ok: 265 316 ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y. … … 275 326 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y))) 276 327 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %); 277 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / /278  #H / /328 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/ 329  #H / by I/ 279 330 ] 280 331 qed. … … 282 333 lemma jump_not_in_policy: ∀prefix:list labelled_instruction. 283 334 ∀policy:(Σp:jump_expansion_policy. 284 (∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 285 jump_in_policy prefix p). 335 out_of_program_none prefix p ∧ jump_in_policy prefix p). 286 336 ∀i:ℕ.i < prefix → 287 337 iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉)) … … 299 349 qed. 300 350 351 (* these two obviously belong somewhere else *) 352 lemma pi1_eq: ∀A:Type[0].∀P:A>Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2. 353 s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2). 354 #A #P #s1 #s2 / by / 355 qed. 356 357 lemma Some_eq: 358 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y. 359 #T #x #y #H @option_destruct_Some @H 360 qed. 361 362 (* The first step of the jump expansion: everything to short. 363 * The third condition of the dependent type implies jump_in_policy; 364 * I've left it in for convenience of typechecking. *) 301 365 definition jump_expansion_start: 302 366 ∀program:(Σl:list labelled_instruction.l < 2^16). 303 367 Σpolicy:jump_expansion_policy. 304 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?)∧368 out_of_program_none program policy ∧ 305 369 jump_in_policy program policy ∧ 306 370 ∀i.i < program → is_jump (nth i ? program 〈None ?, Comment []〉) → … … 309 373 foldl_strong (option Identifier × pseudo_instruction) 310 374 (λprefix.Σpolicy:jump_expansion_policy. 311 (∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?)∧375 out_of_program_none prefix policy ∧ 312 376 jump_in_policy prefix policy ∧ 313 377 ∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → … … 372 436 [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,57,59,61: 373 437 #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi)) 374 >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; / /438 >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; / by / 375 439 ] 376 440 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n … … 407 471 @conj >(injective_S … Hi) #H 408 472 [2,4,6,8,10,12,14,16,18,20,22: 409 >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n / /473 >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n / by I/ 410 474 ] 411 475 @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy)))) … … 428 492 @conj 429 493 [@conj 430 [ #i #Hi / /494 [ #i #Hi / by refl/ 431 495  whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?)) 432 496 ] … … 435 499 qed. 436 500 437 definition policy_increase: list labelled_instruction → jump_expansion_policy → 438 jump_expansion_policy → Prop ≝ 439 λprogram.λop.λp. 440 (∀i:ℕ.i < program → 441 let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in 442 let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in 443 jmpleq oj j). 444 445 definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝ 446 (*λlabels.*)λpolicy. 447 bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in 448 match jmp_len with 449 [ short_jump ⇒ if leb pc_nat addr_nat 450 then le (addr_nat  pc_nat) 126 451 else le (pc_nat  addr_nat) 129 452  medium_jump ⇒ 453 let addr ≝ bitvector_of_nat 16 addr_nat in 454 let pc ≝ bitvector_of_nat 16 pc_nat in 455 let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in 456 let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in 457 eq_bv 5 fst_5_addr fst_5_pc = true 458  long_jump ⇒ True 459 ] 460 ). 461 501 definition policy_equal_int ≝ 502 λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy. 503 ∀n:ℕ.n < program → 504 let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in 505 let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in 506 j1 = j2. 507 508 (* One step in the search for a jump expansion fixpoint. *) 462 509 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 463 510 ∀labels:(Σlm:label_map.∀i:ℕ.lt i (program) → … … 466 513 ∃a.lookup … lm l = Some ? 〈i,a〉). 467 514 ∀old_policy:(Σpolicy. 468 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 469 jump_in_policy program policy). 470 (Σpolicy. 471 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 472 jump_in_policy program policy ∧ 473 policy_increase program old_policy policy) 515 out_of_program_none program policy ∧ jump_in_policy program policy). 516 (Σx:bool × ℕ × (option jump_expansion_policy). 517 let 〈changed,pc,y〉 ≝ x in 518 match y with 519 [ None ⇒ pc > 2^16 520  Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧ 521 jump_in_policy program p ∧ 522 policy_increase program old_policy p ∧ 523 policy_safe p ∧ 524 (changed = false → policy_equal_int program old_policy p) 525 ]) 474 526 ≝ 475 527 λprogram.λlabels.λold_policy. 476 let 〈final_ pc, final_policy〉 ≝528 let 〈final_changed, final_pc, final_policy〉 ≝ 477 529 foldl_strong (option Identifier × pseudo_instruction) 478 (λprefix.ℕ × Σpolicy. 479 (∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 480 jump_in_policy prefix policy ∧ 481 policy_increase prefix old_policy policy 482 ) 530 (λprefix.Σx:bool × ℕ × jump_expansion_policy. 531 let 〈changed,pc,policy〉 ≝ x in 532 out_of_program_none prefix policy ∧ labels_okay labels policy ∧ 533 jump_in_policy prefix policy ∧ 534 policy_increase prefix old_policy policy ∧ 535 policy_safe policy ∧ 536 (changed = false → policy_equal_int prefix old_policy policy)) 483 537 program 484 538 (λprefix.λx.λtl.λprf.λacc. 485 let 〈 pc, policy〉 ≝ acc in539 let 〈changed, pc, policy〉 ≝ acc in 486 540 let 〈label,instr〉 ≝ x in 487 let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (prefix)) old_policy in 541 (* let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (prefix)) old_policy in *) 488 542 let add_instr ≝ 489 543 match instr with … … 493 547  _ ⇒ None ? 494 548 ] in 495 let 〈new_pc, new_policy〉 ≝496 549 let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (prefix)) old_policy 〈0, 0, short_jump〉 in 497 550 match add_instr with 498 551 [ None ⇒ (* i.e. it's not a jump *) 499 〈 add_instruction_size pc long_jump instr, policy〉552 〈changed, add_instruction_size pc long_jump instr, policy〉 500 553  Some z ⇒ let 〈addr,ai〉 ≝ z in 501 554 let new_length ≝ max_length old_length ai in 502 〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (prefix)) 〈pc, addr, new_length〉 policy〉 503 ] in 504 〈new_pc, new_policy〉 505 ) 〈0, Stub ? ?〉 in 506 final_policy. 507 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi; 508 [ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr 509 [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) 510  #z cases z z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss 511 [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) 512  >eq_bv_sym @bitvector_of_nat_abs 513 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 514 @le_S_S @le_plus_n_r 515  @Hi2 516  @lt_to_not_eq @Hi 517 ] 518 ] 519 ] 520  cases (le_to_or_lt_eq … Hi) Hi; 521 [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj 522 [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc 523 cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y 524 [ @(proj1 ?? Hacc Hj) 525  #z cases z z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n n #n #H elim H H #j #Hj 526 @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???); 527 >lookup_opt_insert_miss [ @Hj  @bitvector_of_nat_abs ] 528 [3: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 529 1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 555 〈match dec_eq_jump_length new_length old_length with 556 [ inl _ ⇒ changed 557  inr _ ⇒ true], add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (prefix)) 〈pc, addr, new_length〉 policy〉 530 558 ] 531 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 532 @le_S_S @le_plus_n_r 533 ] 534  lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc 535 #H elim H H; #h #H elim H H; #n #H elim H H #j cases add_instr cases (lookup ??? old_policy ?) 536 normalize nodelta #x #y [2: #z] 559 ) 〈false, 0, Stub ? ?〉 in 560 if geb final_pc 2^16 then 561 〈final_changed,final_pc,None ?〉 562 else 563 〈final_changed,final_pc,Some jump_expansion_policy final_policy〉. 564 [ normalize nodelta @leb_true_to_le @p2 565  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 566 >H2 in H; >p1 normalize nodelta // 567  lapply (pi2 ?? acc) >p >p1 normalize nodelta #Hpolicy 568 @conj [ @conj [ @conj [ @conj [ @conj 569 [ (* out_of_policy_none *) 570 #i >append_length <commutative_plus #Hi normalize in Hi; 571 #Hi2 >lookup_opt_insert_miss 572 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) @Hi2 573  >eq_bv_sym @bitvector_of_nat_abs 574 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 575 @le_S_S @le_plus_n_r 576  @Hi2 577  @lt_to_not_eq @Hi 578 ] 579 ] 580  (* labels_okay *) 581 @lookup_forall #i cases i i #i cases i i #p #a #j #n (*lapply (refl ? add_instr) 582 cases (lookup ??? old_policy ?); #x cases x x #p1 #p2 #p3 583 cases add_instr in ⊢ (???% → %); 584 [ #Hai normalize nodelta #Hl 585 elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl) 586 #i #Hi @(ex_intro ?? i Hi) 587  #x cases x x #np #nl #Hai normalize nodelta *) #Hl 588 elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) Hl #Hl 589 [ elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl) 590 #i #Hi @(ex_intro ?? i Hi) 591  (*whd in match add_instr in Hai; cases instr in Hai;*) normalize nodelta 592 normalize nodelta in p4; cases instr in p4; 593 [2,3: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 594 6: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 595 1: #pi cases pi 596 [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 597 1,2,3,6,7,33,34: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) 598 #H destruct (H) 599 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #abs normalize in abs; 600 lapply (jmeq_to_eq ??? abs) #H destruct (H) 601 9,10,14,15: #id normalize nodelta whd in match (jump_expansion_step_instruction ???); 602 whd in match (select_reljump_length ???); >p5 603 lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) 604 cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 605 normalize nodelta #H 606 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 607 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) 608 cases (leb pc q2) in ⊢ (???% → %); #Hle1 609 [1,3,5,7: lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %); 610 2,4,6,8: lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %); 611 ] 612 #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H 613 <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl 614 11,12,13,16,17: #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???); 615 whd in match (select_reljump_length ???); >p5 616 lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) 617 cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 618 normalize nodelta #H 619 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 620 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) 621 cases (leb pc q2) in ⊢ (???% → %); #Hle1 622 [1,3,5,7,9: lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %); 623 2,4,6,8,10: lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %); 624 ] 625 #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H 626 <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl 627 ] 628 4,5: #id normalize nodelta whd in match (select_jump_length ???); 629 whd in match (select_call_length ???); >p5 630 lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) 631 cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 632 normalize nodelta #H 633 [1: cases (leb pc q2) 634 [ cases (leb (q2pc) 126)  cases (leb (pcq2) 129) ] 635 [1,3: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; 636 #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl) 637 #H >(pair_eq1 ?????? (pair_eq1 ?????? H)) 638 >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl] 639 ] 640 cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2 641 cases (split ? 5 11 (bitvector_of_nat 16 pc)) #m1 #m2 642 normalize nodelta cases (eq_bv ? n1 m1) 643 normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H 644 @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2 645 >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2)) 646 >H @refl 647 ] 648 ] 649 ] 650  (* jump_in_policy *) 651 #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 652 [ >append_length <commutative_plus #Hi normalize in Hi; 653 >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj 654 [ #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) 655 #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n n #n #H elim H H #j #Hj 656 @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???); 657 >lookup_opt_insert_miss [ @Hj  @bitvector_of_nat_abs ] 658 [3: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 659 1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 660 ] 661 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 662 @le_S_S @le_plus_n_r 663  lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) #Hacc 664 #H elim H H; #h #H elim H H; #n #H elim H H #j 537 665 #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) 538 [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs 539 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 540 1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 541 ] 542 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 543 @le_S_S @le_plus_n_r 544  @Hl 545 ] 546 ] 547  #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (prefix))) 548 <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr 549 [1: #pi  2,3: #x  4,5: #id  6: #x #y] @conj normalize nodelta 666 <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs 667 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 668 1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 669 ] 670 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 671 @le_S_S @le_plus_n_r 672 ] 673  >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi) 674 >(nth_append_second ?? prefix ?? (le_n (prefix))) 675 <minus_n_n whd in match (nth ????); normalize nodelta in p4; cases instr in p4; 676 [1: #pi  2,3: #x  4,5: #id  6: #x #y] #Hinstr @conj normalize nodelta 550 677 [3,5,11: #H @⊥ @H (* instr is not a jump *) 551 4,6,12: #H elim H H; #h #H elim H H #n #H elim H H #j cases (lookup ??? old_policy ?) 552 #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 553 [1,3,5: #H destruct (H)] 554 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 555 @le_S_S @le_plus_n_r 556 7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j 557 whd in match (snd ???); @(ex_intro ?? pc) 558 [ @(ex_intro ?? (\fst (select_jump_length labels pc id))) 559 @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id)))) 560 cases (select_jump_length labels pc id) 561  @(ex_intro ?? (\fst (select_call_length labels pc id))) 562 @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id)))) 563 cases (select_call_length labels pc id) 564 ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit 565 8,10: #_ // 566 1,2: cases pi 567 [35,36,37: #H @⊥ @H 568 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H 569 1,2,3,6,7,33,34: #x #y #H @⊥ @H 570 9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j 571 whd in match (snd ???); @(ex_intro ?? pc) 572 @(ex_intro ?? (\fst (select_reljump_length labels pc id))) 573 @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id)))) 574 normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta 678 4,6,12: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr) 679 #H destruct (H) 680 7,9: (* instr is a jump *) #_ @(ex_intro ?? pc) 681 @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 682 @lookup_opt_insert_hit 683 8,10: #_ / by I/ 684 1,2: cases pi in Hinstr; 685 [35,36,37: #Hinstr #H @⊥ @H 686 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hinstr #H @⊥ @H 687 1,2,3,6,7,33,34: #x #y #Hinstr #H @⊥ @H 688 9,10,14,15: #id #Hinstr #_ 689 @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 575 690 @lookup_opt_insert_hit 576 11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j 577 whd in match (snd ???); @(ex_intro ?? pc) 578 @(ex_intro ?? (\fst (select_reljump_length labels pc id))) 579 @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id)))) 580 normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta 691 11,12,13,16,17: #x #id #Hinstr #_ 692 @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 581 693 @lookup_opt_insert_hit 582 72,73,74: #H elim H H; #h #H elim H H #n #H elim H H #j cases (lookup ??? old_policy ?) 583 #z cases z z #x #y #z normalize nodelta 584 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 585 [1,3,5: #H destruct (H)] 586 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 587 @le_S_S @le_plus_n_r 588 41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x 589 #H elim H H; #h #H elim H H #n #H elim H H #j cases (lookup ??? old_policy ?) 590 #z cases z z #x #y #z normalize nodelta 591 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 592 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)] 593 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 594 @le_S_S @le_plus_n_r 595 38,39,40,43,44,70,71: #x #y #H elim H H; #h #H elim H H #n #H elim H H #j 596 cases (lookup ??? old_policy ?) #z cases z z #x #y #z normalize nodelta 597 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 598 [1,3,5,7,9,11,13: #H destruct (H)] 599 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 600 @le_S_S @le_plus_n_r 601 46,47,51,52: #id #_ // 602 48,49,50,53,54: #x #id #_ // 694 72,73,74: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) 695 41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x #Hinstr 696 lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) 697 38,39,40,43,44,70,71: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H 698 normalize in H; destruct (H) 699 46,47,51,52: #id #Hinstr #_ / by I/ 700 48,49,50,53,54: #x #id #Hinstr #_ / by I/ 603 701 ] 604 702 ] 605 703 ] 606 ] 607  lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %); 608 [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi; 609 cases (le_to_or_lt_eq … Hi) Hi; #Hi 610 [ cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,0,short_jump〉) 611 #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 612  normalize nodelta >(injective_S … Hi) 613 >lookup_opt_lookup_miss 614 [ >lookup_opt_lookup_miss 615 [ // 616  cases (lookup ?? (bitvector_of_nat ? (prefix)) old_policy 〈0,0,short_jump〉) 617 #x #y normalize nodelta 618 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 619 [ // 620  @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 621 @le_S_S @le_plus_n_r 622 ] 704 ] 705  (* policy increase *) 706 #i >append_length >commutative_plus #Hi normalize in Hi; 707 cases (le_to_or_lt_eq … Hi) Hi; #Hi 708 [ >lookup_insert_miss 709 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi)) 710  @bitvector_of_nat_abs 711 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 712 1: @(transitive_lt ??? (le_S_S_to_le … Hi)) 713 ] 714 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 715 @le_S_S @le_plus_n_r 716 ] 717  >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta 718 @pair_elim #x #y #_ @jmpleq_max_length 719 ] 720 ] 721  (* policy_safe *) 722 @lookup_forall #x cases x x #x cases x x #p #a #j #n normalize nodelta #Hl 723 elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) Hl #Hl 724 [ @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl) 725  normalize nodelta in p4; cases instr in p4; 726 [2,3: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 727 6: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 728 1: #pi cases pi normalize nodelta 729 [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 730 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: 731 #x #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 732 1,2,3,6,7,33,34: #x #y #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H 733 destruct (H) 734 9,10,14,15: #id >p5 whd in match (jump_expansion_step_instruction ???); 735 whd in match (select_reljump_length ???); 736 cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta 737 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 738 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) 739 cases (leb pc q2) in ⊢ (???% → %); #Hle1 740 [1,3,5,7: lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %); 741 2,4,6,8: lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %); 742 ] 743 #Hle2 normalize nodelta #Hli 744 <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 745 >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli)) 746 cases old_length 747 [1,7,13,19,25,31,37,43: @(leb_true_to_le … Hle2) 748 ] normalize @I (* much faster than / by I/, strangely enough *) 749 11,12,13,16,17: #x #id >p5 whd in match (jump_expansion_step_instruction ???); 750 whd in match (select_reljump_length ???); 751 cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta 752 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 753 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) 754 cases (leb pc q2) in ⊢ (???% → %); #Hle1 755 [1,3,5,7,9: lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %); 756 2,4,6,8,10: lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %); 757 ] 758 #Hle2 normalize nodelta #Hli 759 <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl)) 760 <(pair_eq2 ?????? (Some_eq ??? Hli)) 761 cases old_length 762 [1,7,13,19,25,31,37,43,49,55: @(leb_true_to_le … Hle2) 763 ] normalize @I (* vide supra *) 764 ] 765 4,5: #id >p5 normalize nodelta whd in match (select_jump_length ???); 766 whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,pc〉) 767 #q1 #q2 normalize nodelta 768 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 769 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 770 [1: lapply (refl ? (leb pc q2)) cases (leb pc q2) in ⊢ (???% → %); #Hle1 771 [ lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %); 772  lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %); 623 773 ] 624  >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (prefix) ?)) 625 [ // 626  >prf >p1 >nth_append_second [ <minus_n_n 627 generalize in match Ha; normalize nodelta cases instr normalize nodelta 628 [1: #pi cases pi 629 [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/ 630 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/ 631 35,36,37: #H normalize /2 by nmk/ 632 9,10,14,15: #id whd in match (jump_expansion_step_instruction ???); 633 #H destruct (H) 634 11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???); 635 #H destruct (H) 636 ] 637 2,3: #x #H normalize /2 by nmk/ 638 6: #x #y #H normalize /2 by nmk/ 639 4,5: #id #H destruct (H) 640 ]  @le_n ] 641  >prf >append_length normalize <plus_n_Sm @le_plus_n_r 642 ] 643 ] 644 ] 645  #x cases x x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi; 646 cases (le_to_or_lt_eq … Hi) Hi; #Hi 647 [ cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,0,short_jump〉) 648 #y cases y y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss 649 [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 650  @bitvector_of_nat_abs 774 #Hle2 normalize nodelta 775 ] 776 [2,4,5: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2))) 777 cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3 778 lapply (refl ? (split ? 5 11 (bitvector_of_nat ? pc))) 779 cases (split ??? (bitvector_of_nat ? pc)) in ⊢ (???% → %); #y1 #y2 #Hle4 780 normalize nodelta lapply (refl ? (eq_bv 5 x1 y1)) 781 cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5 782 ] 783 #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl)) 784 <(pair_eq2 ?????? (Some_eq ??? Hli)) 785 cases old_length 786 [2,8,14: >Hle3 @Hle5 787 19,22: >Hle1 @(leb_true_to_le … Hle2) 788 ] normalize @I (* here too *) 789 ] 790 ] 791 ] 792  (* changed *) 793 cases (dec_eq_jump_length (max_length old_length ai) old_length) normalize nodelta 794 [ #Hml #Hc #i #Hi cases (le_to_or_lt_eq … Hi) Hi >append_length >commutative_plus #Hi 795 normalize in Hi; 796 [ >lookup_insert_miss 797 [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) 798  @bitvector_of_nat_abs 651 799 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 652 800 1: @(transitive_lt ??? (le_S_S_to_le … Hi)) … … 655 803 @le_S_S @le_plus_n_r 656 804 ] 657  >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (prefix) ?) ?) 658 [ #a #H elim H H; #b #H elim H H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H) 659 normalize nodelta >lookup_insert_hit @jmpleq_max_length 660  >prf >p1 >nth_append_second 661 [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta 662 [1: #pi cases pi 663 [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H) 664 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H) 665 35,36,37: #H normalize in H; destruct (H) 666 9,10,14,15: #id #H // 667 11,12,13,16,17: #x #id #H // 668 ] 669 2,3: #x #H normalize in H; destruct (H) 670 6: #x #y #H normalize in H; destruct (H) 671 4,5: #id #H // 805  >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta 806 @pair_elim #x #y #_ @(sym_eq ??? Hml) 807 ] 808  #_ #H destruct (H) 809 ] 810 ] 811  (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1 812 normalize nodelta #Hpolicy 813 @conj [ @conj [ @conj [ @conj [ @conj 814 [ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi; 815 #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le ?? Hi) Hi2) 816  (* labels_okay *) @lookup_forall #x cases x x #x cases x #p #a #j #lbl #Hl normalize nodelta 817 elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? lbl Hl) 818 #id #Hid @(ex_intro … id Hid) 819 ] 820  (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi; 821 elim (le_to_or_lt_eq … Hi) Hi #Hi 822 [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) 823 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le ?? Hi)) 824  >(injective_S … Hi) @conj 825 [ >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n whd in match (nth ????); 826 normalize nodelta in p4; cases instr in p4; 827 [ #pi cases pi 828 [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H 829 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H 830 9,10,14,15: #id (* normalize segfaults here *) normalize nodelta 831 whd in match (jump_expansion_step_instruction ???); 832 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 833 11,12,13,16,17: #x #id normalize nodelta 834 whd in match (jump_expansion_step_instruction ???); 835 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 836 35,36,37: #_ #H @⊥ @H 837 ] 838 2,3: #x #_ #H @⊥ @H 839 4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 840 6: #x #id #_ #H @⊥ @H 841 ] 842  #H elim H H #p #H elim H H #a #H elim H H #j #H 843 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (prefix) (le_n (prefix)) ?) in H; 844 [ #H destruct (H) 845  @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 846 @le_S_S @le_plus_n_r 847 ] 848 ] 849 ] 850 ] 851  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 852 elim (le_to_or_lt_eq … Hi) Hi #Hi 853 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi)) 854  >(injective_S … Hi) >lookup_opt_lookup_miss 855 [ >lookup_opt_lookup_miss 856 [ normalize nodelta %2 @refl 857  @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (prefix) (le_n (prefix)) ?) 858 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 859 @le_S_S @le_plus_n_r 860 ] 861  @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (prefix) ?)) >prf 862 [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 863  >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n >p2 864 whd in match (nth ????); normalize nodelta in p4; cases instr in p4; 865 [ #pi cases pi 866 [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ 867 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/ 868 9,10,14,15: #id (* normalize segfaults here *) normalize nodelta 869 whd in match (jump_expansion_step_instruction ???); 870 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 871 11,12,13,16,17: #x #id normalize nodelta 872 whd in match (jump_expansion_step_instruction ???); 873 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 874 35,36,37: #_ normalize /2 by nmk/ 672 875 ] 673  @le_n ] 674  >prf >append_length normalize <plus_n_Sm @le_plus_n_r 675 ] 676 ] 677 ] ] 678  @conj [ @conj 876 2,3: #x #_ normalize /2 by nmk/ 877 4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 878 6: #x #id #_ normalize /2 by nmk/ 879 ] 880 ] 881 ] 882 ] 883 ] 884  (* policy_safe *) @lookup_forall #x cases x x #x cases x x #p #a #j #n #Hl 885 @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl) 886 ] 887  (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi; 888 elim (le_to_or_lt_eq … Hi) Hi #Hi 889 [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) 890  >(injective_S … Hi) >lookup_opt_lookup_miss 891 [ >lookup_opt_lookup_miss 892 [ normalize nodelta @refl 893  @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (prefix) (le_n (prefix)) ?) 894 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 895 @le_S_S @le_plus_n_r 896 ] 897  @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (prefix) ?)) >prf 898 [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 899  >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n >p2 900 whd in match (nth ????); normalize nodelta in p4; cases instr in p4; 901 [ #pi cases pi 902 [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ 903 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/ 904 9,10,14,15: #id (* normalize segfaults here *) normalize nodelta 905 whd in match (jump_expansion_step_instruction ???); 906 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 907 11,12,13,16,17: #x #id normalize nodelta 908 whd in match (jump_expansion_step_instruction ???); 909 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 910 35,36,37: #_ normalize /2 by nmk/ 911 ] 912 2,3: #x #_ normalize /2 by nmk/ 913 4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 914 6: #x #id #_ normalize /2 by nmk/ 915 ] 916 ] 917 ] 918 ] 919 ] 920  @conj [ @conj [ @conj [ @conj [ @conj 679 921 [ #i #Hi // 922  // 923 ] 680 924  #i #Hi @conj [ >nth_nil #H @⊥ @H  #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3 681 925 normalize in H3; destruct (H3) ] 682 926 ] 683 927  #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 928 ] 929  // 930 ] 931  #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi  @not_le_Sn_O ] 932 ] 933 qed. 934 935 (* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *) 936 (* definition weaken_policy: 937 ∀program,op. 938 option (Σp:jump_expansion_policy. 939 And (And (And (And (out_of_program_none program p) 940 (labels_okay (create_label_map program op) p)) 941 (jump_in_policy program p)) (policy_increase program op p)) 942 (policy_safe p)) → 943 option (Σp:jump_expansion_policy.And (out_of_program_none program p) 944 (jump_in_policy program p)) ≝ 945 λprogram.λop.λx. 946 match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with 947 [ None ⇒ None ? 948  Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?) 949 ]. 950 @conj 951 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))) 952  @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))) 684 953 ] 954 qed. *) 955 956 (* This function executes n steps from the starting point. *) 957 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (l) 2^16) 958 (n: ℕ) on n:(Σx:ℕ × (option jump_expansion_policy). 959 let 〈pc,y〉 ≝ x in 960 match y with 961 [ None ⇒ pc > 2^16 962  Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p) 963 ]) ≝ 964 match n with 965 [ O ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉 966  S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 967 match z return λx. z=x → Σa:ℕ × (option jump_expansion_policy).? with 968 [ None ⇒ λp2.〈pc,None ?〉 969  Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?») 970 ] (refl … z) 971 ]. 972 [ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program))) 973  normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m)) 974 <p1 >p2 / by / 975 4: cases (jump_expansion_step program (create_label_map program op) «op,?») 976 #p cases p #q #r cases r normalize nodelta 977 [ / by / 978  #j #H @conj 979 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 980  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 981 ] 982 ] 983  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 / by / 984 ] 685 985 qed. 686 986 687 let rec jump_expansion_internal (program: Σl:list labelled_instruction.l < 2^16) 688 (n: ℕ) on n: (Σpolicy:jump_expansion_policy. 689 And 690 (∀i:ℕ.i ≥ program → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?) 691 (jump_in_policy program policy)) ≝ 692 match n with 693 [ O ⇒ jump_expansion_start program 694  S m ⇒ let old_policy ≝ jump_expansion_internal program m in 695 jump_expansion_step program (create_label_map program old_policy) old_policy 987 lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program). 988 #program whd #x whd #n #Hn 989 cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) 990 #y cases y y #y #z normalize nodelta @refl 991 qed. 992 993 lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program). 994 #program whd #x #y #Hxy whd #n #Hn 995 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) 996 #z cases z z #x1 #x2 #x3 997 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) 998 #z cases z z #y1 #y2 #y3 normalize nodelta // 999 qed. 1000 1001 lemma pe_int_trans: ∀program.transitive ? (policy_equal_int program). 1002 #program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?); 1003 whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy 1004 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) 1005 #z cases z z #x1 #x2 #x3 1006 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z z 1007 #y1 #y2 #y3 1008 cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z z 1009 #z1 #z2 #z3 normalize nodelta // 1010 qed. 1011 1012 definition policy_equal ≝ 1013 λprogram:list labelled_instruction.λp1,p2:option jump_expansion_policy. 1014 match p1 with 1015 [ Some x1 ⇒ match p2 with 1016 [ Some x2 ⇒ policy_equal_int program x1 x2 1017  _ ⇒ False 1018 ] 1019  None ⇒ p2 = None ? 696 1020 ]. 697 [ @(proj1 ?? (pi2 ?? (jump_expansion_start program))) 698  @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy))) 1021 1022 lemma pe_refl: ∀program.reflexive ? (policy_equal program). 1023 #program whd #x whd cases x 1024 [ // 1025  #y @pe_int_refl 699 1026 ] 700 1027 qed. 701 1028 702 definition policy_equal ≝ 703 λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy. 704 ∀n:ℕ.n < program → 705 let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in 706 let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in 707 j1 = j2. 708 709 lemma pe_refl: 710 ∀program.reflexive ? (policy_equal program). 711 #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) 712 #y cases y y #y #z normalize nodelta @refl 713 qed. 714 715 lemma pe_sym: 716 ∀program.symmetric ? (policy_equal program). 717 #program whd #x #y #Hxy whd #n #Hn 718 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) 719 #z cases z z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) 720 #z cases z z #y1 #y2 #y3 normalize nodelta // 721 qed. 722 723 lemma pe_trans: 724 ∀program.transitive ? (policy_equal program). 725 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?); 726 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn 727 lapply (Hxy n Hn) Hxy lapply (Hyz n Hn) Hyz 728 cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z z #x1 #x2 #x3 729 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z z #y1 #y2 #y3 730 cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z z #z1 #z2 #z3 731 normalize nodelta // 1029 lemma pe_sym: ∀program.symmetric ? (policy_equal program). 1030 #program whd #x #y #Hxy whd cases y in Hxy; 1031 [ cases x 1032 [ // 1033  #x' #H @⊥ @(absurd ? H) /2 by nmk/ 1034 ] 1035  #y' cases x 1036 [ #H @⊥ @(absurd ? H) whd in match (policy_equal ???); @nmk #H destruct (H) 1037  #x' #H @pe_int_sym @H 1038 ] 1039 ] 1040 qed. 1041 1042 lemma pe_trans: ∀program.transitive ? (policy_equal program). 1043 #program whd #x #y #z cases x 1044 [ #Hxy #Hyz >Hxy in Hyz; // 1045  #x' cases y 1046 [ #H @⊥ @(absurd ? H) /2 by nmk/ 1047  #y' cases z 1048 [ #_ #H @⊥ @(absurd ? H) /2 by nmk/ 1049  #z' @pe_int_trans 1050 ] 1051 ] 1052 ] 1053 qed. 1054 1055 definition step_none: ∀program.∀n. 1056 (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? → 1057 ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?. 1058 #program #n lapply (refl ? (jump_expansion_internal program n)) 1059 cases (jump_expansion_internal program n) in ⊢ (???% → %); 1060 #x1 cases x1 #p1 #j1 x1; #H1 #Heqj #Hj #k elim k 1061 [ <plus_n_O >Heqj @Hj 1062  #k' k <plus_n_Sm lapply (refl ? (jump_expansion_internal program (n+k'))) 1063 cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %); 1064 #x2 cases x2 #p2 #j2 x2; normalize nodelta #H #Heqj2 1065 cases j2 in H Heqj2; 1066 [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??); 1067 >Heqj2 normalize nodelta @refl 1068  #x #H #Heqj2 #abs destruct (abs) 1069 ] 1070 ] 732 1071 qed. 733 1072 734 1073 lemma pe_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 735 ∀p1,p2:Σpolicy. 736 (∀i:ℕ.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?) 737 ∧jump_in_policy program policy. 738 policy_equal program p1 p2 → 739 policy_equal program (jump_expansion_step program (create_label_map program p1) p1) 740 (jump_expansion_step program (create_label_map program p2) p2). 741 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H 742 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1)) 743 cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?); 744 [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl) 745 #Hnotjmp >lookup_opt_lookup_miss 746 [ >lookup_opt_lookup_miss 747 [ @refl 748  @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn)) 749 [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2))) 750  @Hnotjmp 751 ] 752 ] 753  @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn)) 754 [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1))) 755  @Hnotjmp 756 ] 757 ] 758  #x #Hl cases daemon (* XXX *) 759 ] 1074 ∀n.policy_equal program (\snd (pi1 ?? (jump_expansion_internal program n))) 1075 (\snd (pi1 ?? (jump_expansion_internal program (S n)))) → 1076 policy_equal program (\snd (pi1 ?? (jump_expansion_internal program (S n)))) 1077 (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))). 1078 #program #n #Heq 1079 cases daemon (* XXX *) 760 1080 qed. 761 1081 … … 763 1083 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n. 764 1084 #n (elim n) normalize /2 by S_pred/ qed. 765 1085 766 1086 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.l < 2^16).∀n:ℕ. 767 policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) → 768 ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k). 769 #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H H Hk k; 770 lapply Heq Heq; lapply n n; elim z z; 771 [ #n #Heq <plus_n_O @pe_refl 772  #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n))) 773 [ @Heq 774  @pe_step @Hind @Heq 775 ] 776 ] 777 qed. 778 779 lemma thingie: 780 ∀A:Prop.(A + ¬A) → (¬¬A) → A. 781 #A #Adec #nnA cases Adec 782 [ // 783  #H @⊥ @(absurd (¬A) H nnA) 784 ] 785 qed. 786 787 lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.l<2^16). 788 ∀policy:(Σp:jump_expansion_policy. 789 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 790 jump_in_policy program p). 791 ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) → 792 ∃n:ℕ.n < (program) ∧ jmple 793 (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉)) 794 (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)). 795 #program #policy #Hp 796 cases (dec_bounded_exists (λn.jmple 797 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉)) 798 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (program)) 799 [ #H elim H; H #i #Hi @(ex_intro ?? i) @Hi 800  #abs @⊥ @(absurd ?? Hp) #n #Hn 801 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn) 802 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉)) 803 cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %); 804 #z cases z z #x1 #x2 #x3 #Hx 805 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)) 806 cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %); 807 #z cases z z #y1 #y2 #y3 #Hy 808 normalize nodelta #Hj cases Hj 809 [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn  >Hx >Hy @Hj ] 810  // 811 ] 812  #n @dec_jmple 813 ] 814 qed. 815 816 lemma stupid: 817 ∀program,n. 818 pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) = 819 pi1 … (jump_expansion_internal program (S n)). 820 // 821 qed. 822 1087 policy_equal program (\snd (pi1 … (jump_expansion_internal program n))) 1088 (\snd (pi1 … (jump_expansion_internal program (S n)))) → 1089 ∀k.k ≥ n → policy_equal program (\snd (pi1 … (jump_expansion_internal program n))) 1090 (\snd (pi1 … (jump_expansion_internal program k))). 1091 #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H H Hk k; 1092 lapply Heq Heq; lapply n n; elim z z; 1093 [ #n #Heq <plus_n_O @pe_refl 1094  #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); 1095 @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n))))) 1096 [ @Heq 1097  @Hind @pe_step @Heq 1098 ] 1099 ] 1100 qed. 1101 1102 (* this number monotonically increases over iterations, maximum 2*program *) 823 1103 let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ) 824 1104 on program: ℕ ≝ 825 1105 match program with 826 1106 [ nil ⇒ acc 827  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉)) with 1107  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,00 1108 ,short_jump〉)) with 828 1109 [ long_jump ⇒ measure_int t policy (acc + 2) 829 1110  medium_jump ⇒ measure_int t policy (acc + 1) … … 832 1113 ]. 833 1114 834 (* definition measure ≝835 λprogram.λpolicy.measure_int program policy 0. *)836 837 1115 lemma measure_plus: ∀program.∀policy.∀x,d:ℕ. 838 measure_int program policy (x+d) = measure_int program policy x + d. 839 #program #policy #x #d generalize in match x; x elim d 840 [ // 841  d; #d #Hind elim program 842 [ // 843  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 844 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉)) 845 [ normalize nodelta @Hd 846 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus 847 @Hd 848 ] 849 ] 850 ] 851 qed. 852 1116 measure_int program policy (x+d) = measure_int program policy x + d. 1117 #program #policy #x #d generalize in match x; x elim d 1118 [ // 1119  d; #d #Hind elim program 1120 [ / by refl/ 1121  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1122 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉)) 1123 [ normalize nodelta @Hd 1124 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus 1125 @Hd 1126 ] 1127 ] 1128 ] 1129 qed. 1130 1131 lemma measure_le: ∀program.∀policy. 1132 measure_int program policy 0 ≤ 2*program. 1133 #program #policy elim program 1134 [ normalize @le_n 1135  #h #t #Hind whd in match (measure_int ???); 1136 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉)) 1137 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1138 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) 1139 @le_plus [1,3: @Hind 2,4: // ] 1140 ] 1141 ] 1142 qed. 1143 853 1144 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.l<2^16. 854 1145 ∀policy:Σp:jump_expansion_policy. 855 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 856 jump_in_policy program p.∀l.l ≤ program → ∀acc:ℕ. 857 measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc. 1146 out_of_program_none program p ∧ jump_in_policy program p. 1147 ∀l.l ≤ program → ∀acc:ℕ. 1148 match \snd (jump_expansion_step program (create_label_map program policy) policy) with 1149 [ None ⇒ True 1150  Some p ⇒ measure_int l policy acc ≤ measure_int l p acc 1151 ]. 858 1152 #program #policy #l elim l l; 859 [ #Hp #acc normalize @le_n 860  #h #t #Hind #Hp #acc 861 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (t) Hp) 862 whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?); 863 cases (bvt_lookup … (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉) #z cases z z #x1 #x2 #x3 864 cases (bvt_lookup … (bitvector_of_nat ? (t)) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) #z cases z z #y1 #y2 #y3 1153 [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q pi1; cases q [ //  #x #_ @le_n ] 1154  #h #t #Hind #Hp #acc 1155 lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy)) 1156 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 #p #q pi1; cases q 1157 [ // 1158  #x #Hx #Hjeq normalize nodelta lapply (proj2 ?? (proj1 ?? Hx) (t) Hp) 1159 whd in match (measure_int ???); whd in match (measure_int ? x ?); 1160 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉) 1161 #z cases z z #x1 #x2 #x3 1162 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) x 〈0,0,short_jump〉) 1163 #z cases z z #y1 #y2 #y3 865 1164 normalize nodelta #Hj cases Hj 866 1165 [ cases x3 cases y3 867 1166 [1,4,5,7,8,9: #H @⊥ @H 868 1167 2,3,6: #_ normalize nodelta 869 [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy)acc))870 3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy)(acc+1)))1168 [1,2: @(transitive_le ? (measure_int t x acc)) 1169 3: @(transitive_le ? (measure_int t x (acc+1))) 871 1170 ] 872 [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn 873 2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n  //] 874 ] 875 ] 876  #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn 877 ] 878 ] 879 qed. 880 881 lemma measure_le: ∀program.∀policy. 882 measure_int program policy 0 ≤ 2*program. 883 #program #policy elim program 884 [ normalize @le_n 885  #h #t #Hind whd in match (measure_int ???); 886 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉)) 887 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 888 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) 889 @le_plus [1,3: @Hind 2,4: // ] 890 ] 891 ] 1171 [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus //] 1172 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1173 ] 1174  #Heq >Heq cases y3 normalize nodelta 1175 [2,3: >measure_plus >measure_plus @le_plus //] 1176 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1177 ] 1178 ] 1179 ] 892 1180 qed. 893 1181 … … 895 1183 lemma bla: ∀a,b:ℕ.a + a = b + b → a = b. 896 1184 #a elim a 897 [ normalize #b // 1185 [ normalize #b // 898 1186  a #a #Hind #b cases b [ /2 by le_n_O_to_eq/  b #b normalize 899 1187 <plus_n_Sm <plus_n_Sm #H … … 906 1194 [ //  #y // ] 907 1195 qed. 908 1196 909 1197 lemma measure_full: ∀program.∀policy. 910 1198 measure_int program policy 0 = 2*program → ∀i.i<program → 911 1199 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump. 912 913 914 915 916 917 918 919 920 921 >(commutative_plus (t) 0) <plus_O_n <minus_n_O922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 1200 #program #policy elim program 1201 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1202  #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*t) 1203 [ whd in match (measure_int ???) in Hm; 1204 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉)) in Hm; 1205 normalize nodelta 1206 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ 1207  >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) 1208 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize 1209 >(commutative_plus (t) 0) <plus_O_n <minus_n_O 1210 >plus_n_Sm @le_n 1211  >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) // 1212 ] 1213  #Hmt cases (le_to_or_lt_eq … Hi) Hi; 1214 [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi)) 1215  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1216 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉)) in Hm; 1217 normalize nodelta 1218 [ >Hmt normalize <plus_n_O >(commutative_plus (t) (S (t))) 1219 >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s 1220  >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize 1221 #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s 1222  #_ // 1223 ] 1224 ]] 1225 ] 938 1226 qed. 939 1227 940 1228 lemma measure_special: ∀program:(Σl:list labelled_instruction.l < 2^16). 941 1229 ∀policy:Σp:jump_expansion_policy. 942 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 943 jump_in_policy program p. 944 measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 → 945 policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy). 946 #program #policy lapply (le_n (program)) @(list_ind ? 947 (λx.x ≤ program → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 → 948 policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy))) 949 ?? program) 950 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 1230 out_of_program_none program p ∧ jump_in_policy program p. 1231 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with 1232 [ None ⇒ True 1233  Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal_int program policy p ]. 1234 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) 1235 cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %); 1236 #p cases p #pc #pol normalize nodelta cases pol 1237 [ // 1238  #p normalize nodelta #Hpol #eqpol lapply (le_n (program)) 1239 @(list_ind ? (λx.x ≤ pi1 ?? program → 1240 measure_int x policy 0 = measure_int x p 0 → 1241 policy_equal_int x policy p) ?? (pi1 ?? program)) 1242 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 951 1243  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 952 1244 [ #Hi @Hind 953 1245 [ @(transitive_le … Hp) // 954  whd in match (measure_int ???) in Hm; whd in match (measure_int ? (jump_expansion_step ???)?) in Hm;955 lapply (proj2 ?? (p i2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (t) ?)956 [ @(lt_to_le_to_lt … (h::t)) [ //  @Hp ]957  cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in Hm;958 #x cases x x #x1 #x2 #x3959 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉);960 #y cases y y #y1 #y2 #y3961 normalize nodelta cases x3 cases y3 normalize nodelta962 [1: #H #_ @H963 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt964 @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn965 966 967 968 969 970 971 @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn972 9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)973 #H #_ @(injective_plus_r … H)974 ]1246  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 1247 lapply (proj2 ?? (proj1 ?? Hpol) (t) Hp) 1248 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in Hm; 1249 #x cases x x #x1 #x2 #x3 1250 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉); 1251 #y cases y y #y1 #y2 #y3 1252 cases x3 cases y3 normalize nodelta 1253 [1: #H #_ @H 1254 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1255 lapply (measure_incr_or_equal program policy t ? 0) 1256 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol // 1257 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 1258 5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) 1259 #H #_ @(injective_plus_r … H) 1260 6: >measure_plus >measure_plus 1261 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 1262 #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1263 lapply (measure_incr_or_equal program policy t ? 0) 1264 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol // 1265 9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) 1266 #H #_ @(injective_plus_r … H) 975 1267 ] 976 1268  @(le_S_S_to_le … Hi) 977 1269 ] 978  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 979 whd in match (measure_int ?(jump_expansion_step ???)?) in Hm; 980 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (t) ?) 981 [ @(lt_to_le_to_lt … (h::t)) [ //  @Hp ] 982  cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in Hm; 983 #x cases x x #x1 #x2 #x3 984 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉); 985 #y cases y y #y1 #y2 #y3 986 normalize nodelta cases x3 cases y3 normalize nodelta 987 [1,5,9: #_ #_ // 988 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 989 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 990 @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn 991 6: >measure_plus >measure_plus 992 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 993 #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 994 @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn 995 ] 1270  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1271 whd in match (measure_int ? p ?) in Hm; 1272 lapply (proj2 ?? (proj1 ?? Hpol) (t) Hp) 1273 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in 1274 Hm; 1275 #x cases x x #x1 #x2 #x3 1276 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉); 1277 #y cases y y #y1 #y2 #y3 1278 normalize nodelta cases x3 cases y3 normalize nodelta 1279 [1,5,9: #_ #_ // 1280 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 1281 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1282 lapply (measure_incr_or_equal program policy t ? 0) 1283 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1284 6: >measure_plus >measure_plus 1285 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 1286 #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1287 lapply (measure_incr_or_equal program policy t ? 0) 1288 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 996 1289 ] 997 1290 ] 998 ] 1291 ] 1292 qed. 1293 1294 lemma le_to_eq_plus: ∀n,z. 1295 n ≤ z → ∃k.z = n + k. 1296 #n #z elim z 1297 [ #H cases (le_to_or_lt_eq … H) 1298 [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O 1299  #H2 @(ex_intro … 0) >H2 // 1300 ] 1301  #z' #Hind #H cases (le_to_or_lt_eq … H) 1302 [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k')) 1303 >H2 >plus_n_Sm // 1304  #H' @(ex_intro … 0) >H' // 1305 ] 1306 ] 999 1307 qed. 1000 1308 1001 1309 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.l < 2^16. 1002 l ≤ program → measure_int l (jump_expansion_ internal program 0) 0 = 0.1003 #l #program elim l 1310 l ≤ program → measure_int l (jump_expansion_start program) 0 = 0. 1311 #l #program elim l 1004 1312 [ // 1005 1313  #h #t #Hind #Hp whd in match (measure_int ???); … … 1008 1316 [ normalize nodelta @Hind @le_S_to_le ] 1009 1317 @Hp 1010  >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (t) ?) Hj) 〈0,0,short_jump〉) 1011 [ normalize nodelta @Hind @le_S_to_le ] 1012 @Hp 1013 ] 1014 ] 1015 qed. 1016 1017 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.l < 2^16). 1018 Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p. 1019 #program @(mk_Sig … (jump_expansion_internal program (2*program))) 1020 @(ex_intro … (2*program)) #k #Hk 1021 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k) 1022 (jump_expansion_internal program (S k))) ? (2*program)) 1023 [ #H elim H H #x #Hx @pe_trans 1024 [ @(jump_expansion_internal program x) 1025  @pe_sym @equal_remains_equal 1026 [ @(proj2 ?? Hx) 1027  @(transitive_le ? (2*program)) 1028 [ @le_S_S_to_le @le_S @(proj1 ?? Hx) 1029  @le_S_S_to_le @le_S @Hk 1318  >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (t) ?) Hj) 〈0,0,short_jump〉) 1319 [ normalize nodelta @Hind @le_S_to_le @Hp 1320  @Hp 1321  % 1322 [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program)))) 1323  @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program)))) 1030 1324 ] 1031 1325 ] 1032  @equal_remains_equal 1033 [ @(proj2 ?? Hx) 1034  @le_S_S_to_le @le_S @(proj1 ?? Hx) 1035 ] 1036 ] 1037  #Hnex lapply (not_exists_forall … Hnex) Hnex; #Hfa @pe_sym @equal_remains_equal 1038 [ lapply (measure_full program (jump_expansion_internal program (2*program))) 1039 #Hfull #i #Hi 1040 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program (jump_expansion_internal program (2*program))) (jump_expansion_internal program (2*program)))) i Hi) 1041 lapply (Hfull ? i Hi) 1042 [ i @le_to_le_to_eq 1043 [ @measure_le 1044  lapply (le_n (2*program)) elim (2*program) in ⊢ (?%? → %); 1045 [ #_ >measure_zero @le_n 1046  #x #Hind #Hx 1047 cut (measure_int program (jump_expansion_internal program x) 0 < 1048 measure_int program (jump_expansion_internal program (S x)) 0) 1049 [ elim (le_to_or_lt_eq … 1050 (measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (program)) 0)) 1051 [ // 1052  #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H 1053 ] 1054  #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2 1055 ] 1056 ] 1057 ] 1058  Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*program)) 〈0,0,short_jump〉) 1059 #x cases x x #x1 #x2 #x3 normalize nodelta #Hfull 1060 >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉) 1061 #y cases y y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta 1062 [1,2: #H elim H #H2 [1,3: @⊥ @H2 2,4: destruct (H2) ] 1063  #_ // 1064 ] 1065 ] 1066  @le_S_to_le @Hk 1067 ] 1068  #n @dec_bounded_forall #m 1069 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉) 1070 #x cases x x #x1 #x2 #x3 1071 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉) 1072 #y cases y y #y1 #y2 #y3 normalize nodelta 1073 @dec_eq_jump_length 1074 ] 1075 qed. 1076 1326 ] 1327 ] 1328 qed. 1329 1330 (* the actual computation of the fixpoint *) 1331 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.l < 2^16). 1332 Σp:option jump_expansion_policy.∃n.∀k.n < k → 1333 policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p. 1334 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*program)))) 1335 (*@(ex_intro … (2*program)) #k #Hk*) 1336 cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program) 1337 (\snd (pi1 ?? (jump_expansion_internal program k))) 1338 (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*program)) 1339 [ #Hex elim Hex Hex #x #Hx @(ex_intro … x) #k @pe_trans 1340 [ @(\snd (pi1 ?? (jump_expansion_internal program x))) 1341  @pe_sym @equal_remains_equal 1342 [ @(proj2 ?? Hx) 1343  @(transitive_le ? (2*program)) 1344 [ @le_S_S_to_le @le_S @(proj1 ?? Hx) 1345  @le_S_S_to_le @le_S @Hk 1346 ] 1347 ] 1348  @equal_remains_equal 1349 [ @(proj2 ?? Hx) 1350  @le_S_S_to_le @le_S @(proj1 ?? Hx) 1351 ] 1352 ] 1353  #Hnex lapply (not_exists_forall … Hnex) Hnex; #Hfa @pe_sym @equal_remains_equal 1354 [ lapply (refl ? (jump_expansion_internal program (2*program))) 1355 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → %); 1356 #jep cases jep #pc #x jep cases x normalize nodelta 1357 [ #Hjep #Heqx >Heqx lapply (step_none program (2*pi1 ?? program) ? 1) 1358 [ >Heqx //  <plus_n_Sm <plus_n_O #H >H // ] 1359  #pol_2prog #H2prog #Heq2prog lapply (measure_full (pi1 ?? program) pol_2prog) #Hfull 1360 whd in match (policy_equal ???); lapply Heq2prog Heq2prog; 1361 lapply (refl ? (jump_expansion_internal program (2*program))) 1362 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → % → %); 1363 #z cases z #fpc #pol z cases pol normalize nodelta 1364 [ #Heq2prog #Hjep #Hploq destruct (Hploq) 1365  #p #Heq2prog #Hjep #Hploq whd in match (jump_expansion_internal ??); 1366 >Hjep normalize nodelta 1367 lapply (refl ? (jump_expansion_step program (create_label_map program p) «p,?»)) 1368 [2: cases (jump_expansion_step program (create_label_map program p) «p,?») in ⊢ (???% → %); 1369 #x cases x #Spc #Spol x cases Spol normalize nodelta 1370 [ #Hy #Hgnarf cases daemon (* XXX *) 1371  #y #Hy #Hgnarf #i #Hi lapply (proj2 ?? (proj1 ?? Hy) i Hi) 1372 lapply (Hfull ? i Hi) 1373 [2: lapply (sym_eq ??? (proj1 ?? Hpy)) #Hblp >(Some_eq ??? Hblp) 1374 >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq))) 1375 cases (bvt_lookup ?? (bitvector_of_nat 16 i) pol_2prog 〈0,0,short_jump〉) 1376 #blp cases blp #a #b #c blp #EQ >EQ normalize nodelta 1377 cases (bvt_lookup ?? (bitvector_of_nat 16 i) y 〈0,0,short_jump〉) 1378 #blp cases blp #d #e #f blp normalize nodelta cases f 1379 [1,2: #H elim H #H2 [1,3: @⊥ @H2 2,4: destruct (H2) ] 1380  #_ // 1381 ] 1382  @le_to_le_to_eq 1383 [ @measure_le 1384  cut (∀x.x ≤ (2*pi1 ?? program) → 1385 ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ 1386 x ≤ measure_int program p 0)) 1387 [ #n elim n 1388 [ #_ whd in match (jump_expansion_internal program 0); 1389 @(ex_intro … (jump_expansion_start program)) % [ @refl  1390 >measure_zero @le_n ] 1391  n #n' #Hind #Hn' elim (le_to_or_lt_eq … Hn') 1392 [ #H2n' elim (Hind ?) 1393 [ Hgnarf #pn' lapply (refl ? (jump_expansion_internal program (S n'))) 1394 cases (jump_expansion_internal program (S n')) in ⊢ (???% → %); 1395 #x cases x x #npc #npol cases npol normalize nodelta 1396 [ #Hbla #Hnone #Hsome lapply (step_none program (S n')) 1397 >Hnone normalize nodelta #Ht elim (le_to_eq_plus ?? Hn') 1398 #k #Hk lapply (Ht ? k) [ //  <Hk >Hjep #H destruct (H) ] 1399  #Spol #Hbla #HSpol #H3 @(ex_intro ?? Spol) @conj [ @refl  1400 lapply (measure_incr_or_equal program pn' program) 1401 lapply (pi2 ?? (jump_expansion_internal program n')) 1402 >(proj1 ?? H3) 1403 lapply (refl ? (jump_expansion_internal program n')) 1404 lapply H3 H3 1405 cases (jump_expansion_internal program n') in ⊢ (% → ???% → %); 1406 #x cases x x #npc #npol normalize nodelta #Hbli #H3 #EQ 1407 >(proj1 ?? H3) in Hbli EQ; #Hbli #EQ 1408 whd in match (jump_expansion_internal program (S n')) in HSpol; 1409 >EQ in HSpol; normalize nodelta 1410 ] ] 1411 1412 1413 1414  1415 ] 1416  1417 ] 1418 ] 1419 1420  #gloeirks elim (gloeirks (2*program) (le_n ?)) #q 1421 >Hjep >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq))) 1422 #H >(Some_eq ??? (proj1 ?? H)) @(proj2 ?? H) 1423 ] 1424 ] 1425 ] 1426 ] 1427 ]] 1428 ] 1429 ] 1430  @le_S_to_le @Hk 1431 ] 1432  (* TO BE CHANGED *) 1433 #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 1434 [ %1 // 1435 2,3: #x %2 @nmk whd in match (policy_equal ???); [2: //] 1436 whd in match (eject_policy_opt ???); #H destruct (H) 1437 4: #p1 #p2 whd in match (policy_equal ???); @dec_bounded_forall #m 1438 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉) 1439 #x cases x x #x1 #x2 #x3 1440 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉) 1441 #y cases y y #y1 #y2 #y3 normalize nodelta 1442 @dec_eq_jump_length 1443 ] 1444 ] 1445 1446 (* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into 1447 * a map from pc to jump_length. This cannot be done earlier because the pc 1448 * changes between iterations. *) 1077 1449 let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n: 1078 1450 BitVectorTrie jump_length 16 ≝ … … 1087 1459 ]. 1088 1460 1461 (* The glue between Policy and Assembly. *) 1089 1462 definition jump_expansion': 1090 1463 ∀program:preamble × (Σl:list labelled_instruction.l < 2^16).
Note: See TracChangeset
for help on using the changeset viewer.