Changeset 1879 for src/ASM/Policy.ma
 Timestamp:
 Apr 5, 2012, 6:13:26 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1810 r1879 13 13 definition label_map ≝ identifier_map ASMTag (ℕ × ℕ). 14 14 15 (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)16 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.15 (* jump_expansion_policy: instruction number ↦ 〈pc, [addr, jump_length]〉 *) 16 definition jump_expansion_policy ≝ ℕ × (BitVectorTrie (ℕ × ℕ × jump_length) 16). 17 17 18 18 (* The different properties that we want/need to prove at some point *) … … 20 20 definition out_of_program_none ≝ 21 21 λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. 22 ∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy= None ?.22 ∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) (\snd policy) = None ?. 23 23 24 24 (* If instruction i is a jump, then there will be something in the policy at … … 53 53 ∀i:ℕ.i < prefix → 54 54 (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔ 55 ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉). 55 ∃p:ℕ.∃a:ℕ.∃j:jump_length. 56 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈p,a,j〉). 56 57 57 58 definition labels_okay ≝ 58 59 λlabels:label_map.λpolicy:jump_expansion_policy. 59 bvt_forall ?? policy (λn.λx.let 〈pc,addr_nat,i〉 ≝ x in60 ∃id:Identifier.61 60 bvt_forall ?? (\snd policy) (λn.λx. 61 let 〈pc,addr_nat,j〉 ≝ x in 62 ∃id:Identifier.\snd (lookup_def … labels id 〈0,pc〉) = addr_nat 62 63 ). 63 64 … … 86 87 λprogram.λop.λp. 87 88 (∀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). 89 let 〈pc1,i1,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) (\snd op) 〈0,0,short_jump〉 in 90 let 〈pc2,i2,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) (\snd p) 〈0,0,short_jump〉 in 91 jmpleq oj j 92 ). 91 93 92 94 (* Policy safety *) 93 95 definition policy_safe: jump_expansion_policy → Prop ≝ 94 96 λpolicy. 95 bvt_forall ?? policy(λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in97 bvt_forall ?? (\snd policy) (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in 96 98 match jmp_len with 97 99 [ short_jump ⇒ if leb pc_nat addr_nat 98 100 then le (addr_nat  pc_nat) 126 99 101 else le (pc_nat  addr_nat) 129 100  medium_jump ⇒ 102  medium_jump ⇒ 101 103 let addr ≝ bitvector_of_nat 16 addr_nat in 102 104 let pc ≝ bitvector_of_nat 16 pc_nat in … … 174 176 qed. 175 177 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 178 definition expand_relative_jump_internal_unsafe: 179 jump_length → ([[relative]] → preinstruction [[relative]]) → option (list instruction) ≝ 180 λjmp_len,i. 181 match jmp_len with 182 [ short_jump ⇒ Some ? [ RealInstruction (i (RELATIVE (zero 8))) ] 183  medium_jump ⇒ None … 184  long_jump ⇒ Some ? 185 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); 186 SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) 187 LJMP (ADDR16 (zero 16)) 188 ] 189 ]. 190 @I 191 qed. 192 193 definition expand_relative_jump_unsafe: 194 jump_length → preinstruction Identifier → option (list instruction) ≝ 195 λjmp_len,i. 196 match i with 197 [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?) 198  JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?) 199  JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr) 200  JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?) 201  JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?) 202  JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr) 203  JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr) 204  CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr) 205  DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr) 206  ADD arg1 arg2 ⇒ Some … [ ADD ? arg1 arg2 ] 207  ADDC arg1 arg2 ⇒ Some … [ ADDC ? arg1 arg2 ] 208  SUBB arg1 arg2 ⇒ Some … [ SUBB ? arg1 arg2 ] 209  INC arg ⇒ Some … [ INC ? arg ] 210  DEC arg ⇒ Some … [ DEC ? arg ] 211  MUL arg1 arg2 ⇒ Some … [ MUL ? arg1 arg2 ] 212  DIV arg1 arg2 ⇒ Some … [ DIV ? arg1 arg2 ] 213  DA arg ⇒ Some … [ DA ? arg ] 214  ANL arg ⇒ Some … [ ANL ? arg ] 215  ORL arg ⇒ Some … [ ORL ? arg ] 216  XRL arg ⇒ Some … [ XRL ? arg ] 217  CLR arg ⇒ Some … [ CLR ? arg ] 218  CPL arg ⇒ Some … [ CPL ? arg ] 219  RL arg ⇒ Some … [ RL ? arg ] 220  RR arg ⇒ Some … [ RR ? arg ] 221  RLC arg ⇒ Some … [ RLC ? arg ] 222  RRC arg ⇒ Some … [ RRC ? arg ] 223  SWAP arg ⇒ Some … [ SWAP ? arg ] 224  MOV arg ⇒ Some … [ MOV ? arg ] 225  MOVX arg ⇒ Some … [ MOVX ? arg ] 226  SETB arg ⇒ Some … [ SETB ? arg ] 227  PUSH arg ⇒ Some … [ PUSH ? arg ] 228  POP arg ⇒ Some … [ POP ? arg ] 229  XCH arg1 arg2 ⇒ Some … [ XCH ? arg1 arg2 ] 230  XCHD arg1 arg2 ⇒ Some … [ XCHD ? arg1 arg2 ] 231  RET ⇒ Some … [ RET ? ] 232  RETI ⇒ Some … [ RETI ? ] 233  NOP ⇒ Some … [ RealInstruction (NOP ?) ] 234 ]. 235 236 definition expand_pseudo_instruction_unsafe: 237 jump_length → pseudo_instruction → option (list instruction) ≝ 238 λjmp_len. 239 λi. 240 match i with 241 [ Cost cost ⇒ Some ? [ ] 242  Comment comment ⇒ Some ? [ ] 243  Call call ⇒ 244 match jmp_len with 245 [ short_jump ⇒ None ? 246  medium_jump ⇒ Some ? [ ACALL (ADDR11 (zero 11)) ] 247  long_jump ⇒ Some ? [ LCALL (ADDR16 (zero 16)) ] 248 ] 249  Mov d trgt ⇒ 250 Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))] 251  Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr 252  Jmp jmp ⇒ 253 match jmp_len with 254 [ short_jump ⇒ Some ? [ SJMP (RELATIVE (zero 8)) ] 255  medium_jump ⇒ Some ? ([ AJMP (ADDR11 (zero 11)) ]) 256  long_jump ⇒ Some ? [ LJMP (ADDR16 (zero 16)) ] 257 ] 258 ]. 259 @I 260 qed. 261 262 definition instruction_size: (* ℕ → *) jump_length → pseudo_instruction → ℕ ≝ 263 λjmp_len.λinstr. 264 let ilist ≝ expand_pseudo_instruction_unsafe jmp_len instr in 180 265 let bv: list (BitVector 8) ≝ match ilist with 181 266 [ None ⇒ (* this shouldn't happen *) [ ] 182 267  Some l ⇒ flatten … (map … assembly1 l) 183 268 ] in 184 pc + (bv). 185 @(λx.bv_pc) 186 qed. 269 bv. 270 271 definition policy_isize_sum ≝ 272 λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. 273 (\fst policy) = foldl_strong (option Identifier × pseudo_instruction) 274 (λacc.ℕ) 275 prefix 276 (λhd.λx.λtl.λp.λacc. 277 let 〈i1,i2,jl〉 ≝ bvt_lookup … (bitvector_of_nat ? (hd)) (\snd policy) 〈0,0,short_jump〉 in 278 acc + (instruction_size jl (\snd x))) 279 0. 187 280 188 281 (* The function that creates the labeltoaddress map *) … … 213 306  Some l ⇒ add … labels l 〈prefix, pc〉 214 307 ] in 215 let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (prefix)) policy 〈0, 0, long_jump〉 in 216 〈add_instruction_size pc jmp_len instr, new_labels〉 308 let 〈i1,i2,jmp_len〉 ≝ 309 bvt_lookup ?? (bitvector_of_nat 16 (prefix)) (\snd policy) 〈0,0,short_jump〉 in 310 〈pc + (instruction_size jmp_len instr), new_labels〉 217 311 ) 〈0, empty_map …〉 in 218 312 final_labels. 219 [ 313 [#i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 220 314 [ #Hi #l normalize nodelta; cases label normalize nodelta 221 315 [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl … … 226 320 [ normalize in Hocc; 227 321 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 228 @⊥ @(absurd … Hocc) 322 @⊥ @(absurd … Hocc) 229 323  normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?) 230 324 [ #addr #Haddr % [ @addr  <Haddr @lookup_add_miss /2/ ] … … 312 406 qed. 313 407 314 (* these should be moved to BitVector at some point, and proven *)315 lemma bitvector_of_nat_ok: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.317 #n elim n n318 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl319  #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)320 ]321 qed.322 323 lemma bitvector_of_nat_abs:324 ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).325 #n #x #y #Hx #Hy #Heq @notb_elim326 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))327 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);328 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/329  #H / by I/330 ]331 qed.332 333 408 lemma jump_not_in_policy: ∀prefix:list labelled_instruction. 334 409 ∀policy:(Σp:jump_expansion_policy. … … 336 411 ∀i:ℕ.i < prefix → 337 412 iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉)) 338 (lookup_opt … (bitvector_of_nat 16 i) policy= None ?).413 (lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = None ?). 339 414 #prefix #policy #i #Hi @conj 340 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))341 cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);342 343  #x cases x x #x #z cases x x #x #y#H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))344 345 346 347 #H elim H H; #x #H elim H H; #y #H elim H H;#z #H >H in Hnone; #abs destruct (abs)348 415 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) (\snd policy))) 416 cases (lookup_opt … (bitvector_of_nat 16 i) (\snd policy)) in ⊢ (???% → ?); 417 [ #H @H 418  #x cases x x #x cases x x #x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi)) 419 @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H))) 420 ] 421  #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj) 422 #H elim H H; #x #H elim H H; #y #H elim H H #z #H >H in Hnone; #abs destruct (abs) 423 ] 349 424 qed. 350 425 … … 369 444 jump_in_policy program policy ∧ 370 445 ∀i.i < program → is_jump (nth i ? program 〈None ?, Comment []〉) → 371 lookup_opt … (bitvector_of_nat 16 i) policy= Some ? 〈0,0,short_jump〉 ≝446 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉 ≝ 372 447 λprogram. 373 448 foldl_strong (option Identifier × pseudo_instruction) … … 376 451 jump_in_policy prefix policy ∧ 377 452 ∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 378 lookup_opt … (bitvector_of_nat 16 i) policy= Some ? 〈0,0,short_jump〉)453 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉) 379 454 program 380 (λprefix.λx.λtl.λprf.λpolicy. 455 (λprefix.λx.λtl.λprf.λp. 456 let 〈pc,policy〉 ≝ p in 381 457 let 〈label,instr〉 ≝ x in 382 match instr with458 〈pc + instruction_size short_jump instr,match instr with 383 459 [ Instruction i ⇒ match i with 384 460 [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,0,short_jump〉 policy … … 391 467  CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,0,short_jump〉 policy 392 468  DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,0,short_jump〉 policy 393  _ ⇒ (pi1 … policy)469  _ ⇒ policy 394 470 ] 395  Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16(bitvector_of_nat 16 (prefix)) 〈0,0,short_jump〉 policy471  Call c ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,0,short_jump〉 policy 396 472  Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,0,short_jump〉 policy 397  _ ⇒ (pi1 ?? policy) 398 ] 399 ) (Stub ? ?). 400 [1,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,35,36,37,38,39,40,41,42: 401 @conj 402 [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: 403 @conj 404 #i >append_length <commutative_plus #Hi normalize in Hi; 405 [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: 406 #Hi2 cases (le_to_or_lt_eq … Hi) Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i) 407 [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121: 408 @le_S_to_le @le_S_to_le @Hi 409 2,6,10,14,18,22,26,30,34,38,42,46,50,54,58,62,66,70,74,78,82,86,90,94,98,102,106,110,114,118,122: 410 @Hi2 411 3,7,11,15,19,23,27,31,35,39,43,47,51,55,59,63,67,71,75,79,83,87,91,95,99,103,107,111,115,119,123: 412 <Hi @le_n_Sn 413 4,8,12,16,20,24,28,32,36,40,44,48,52,56,60,64,68,72,76,80,84,88,92,96,100,104,108,112,116,120,124: 414 @Hi2 415 ] 416 ] 417 cases (le_to_or_lt_eq … Hi) Hi; #Hi 418 [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: 419 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) 420 @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 421 ] 422 @conj >(injective_S … Hi) 423 [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: 424 >(nth_append_second ? ? prefix ? ? (le_n (prefix))) <minus_n_n #H @⊥ @H 425 ] 426 #H elim H; H; #t1 #H elim H; H #t2 #H elim H; H; #t3 #H 427 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) in H; 428 [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: 429 #H destruct (H) 430 ] 431 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S 432 @le_plus_n_r 433 ] 434 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 435 Hi; #Hi 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: 437 #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi)) 438 >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; / by / 439 ] 440 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n 441 #H @⊥ @H 442 2,3,26,27,28,29,30,31,32,33,34: @conj 443 [1,3,5,7,9,11,13,15,17,19,21: @conj 444 [1,3,5,7,9,11,13,15,17,19,21: 445 #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss 446 [1,3,5,7,9,11,13,15,17,19,21: 447 @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) 448 ] 449 >eq_bv_sym @bitvector_of_nat_abs 450 [1,4,7,10,13,16,19,22,25,28,31: 451 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S 452 @le_plus_n_r 453 2,5,8,11,14,17,20,23,26,29,32: @Hi2 454 3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi 455 ] 456 ] 457 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 458 Hi #Hi 459 [1,3,5,7,9,11,13,15,17,19,21: 460 >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss 461 [1,3,5,7,9,11,13,15,17,19,21: 462 @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 463 ] 464 @bitvector_of_nat_abs 465 [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi)) 466 1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 467 ] 468 @(transitive_lt … (pi2 ?? program)) 469 >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 470 ] 471 @conj >(injective_S … Hi) #H 472 [2,4,6,8,10,12,14,16,18,20,22: 473 >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n / by I/ 474 ] 475 @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy)))) 476 ] 477 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 478 Hi #Hi 479 [1,3,5,7,9,11,13,15,17,19,21: 480 >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss 481 [1,3,5,7,9,11,13,15,17,19,21: 482 @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj) 483 ] 484 @bitvector_of_nat_abs 485 [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi)) 486 1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 487 ] 488 @(transitive_lt … (pi2 ?? program)) 489 >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 490 ] 491 #_ >(injective_S … Hi) @lookup_opt_insert_hit 492 @conj 493 [@conj 494 [ #i #Hi / by refl/ 495  whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?)) 496 ] 497  #i #Hi >nth_nil #Hj @⊥ @Hj 473  _ ⇒ policy 474 ]〉 475 ) 〈0, Stub ? ?〉. 476 [ @conj 477 [ @conj 478 #i >append_length <commutative_plus #Hi normalize in Hi; 479 [ #Hi2 cases (le_to_or_lt_eq … Hi) Hi #Hi 480 cases p p #p cases p p #pc #p #Hp cases x x #l #pi cases pi 481 [1,7: #id cases id normalize nodelta 482 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 483 [1,2,3,6,7,24,25: #x #y 484 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 485 @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 486 38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74: 487 [1,2,3,6,7,24,25: #x #y 488 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 489 <Hi @(proj1 ?? (proj1 ?? Hp) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 490 >Hi @Hi2 491 9,10,11,12,13,14,15,16,17: 492 [1,2,6,7: #x 3,4,5,8,9: #x #id] >lookup_opt_insert_miss 493 [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 494 [1,4,7,10,13,16,19,22,25: @Hi2 495 2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) @le_S_to_le @Hi 496 3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq @le_S_to_le @Hi 497 ] 498 1,3,5,7,9,11,13,15,17: 499 @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 500 ] 501 46,47,48,49,50,51,52,53,54: 502 [1,2,6,7: #x 3,4,5,8,9: #x #id] >lookup_opt_insert_miss 503 [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 504 [1,4,7,10,13,16,19,22,25: @Hi2 505 2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) <Hi @le_n 506 3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq <Hi @le_n 507 ] 508 1,3,5,7,9,11,13,15,17: 509 @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n 510 ] 511 ] 512 2,3,6,8,9,12: [3,6: #w] #z normalize nodelta 513 [1,3,4: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 514 2,5,6: 515 <Hi @(proj1 ?? (proj1 ?? Hp) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 516 >Hi @Hi2 517 ] 518 4,5,10,11: #dst normalize nodelta >lookup_opt_insert_miss 519 [2,4,6,8: @bitvector_of_nat_abs 520 [1,4,7,10: @Hi2 521 2,5: @(transitive_lt … Hi2) @le_S_to_le @Hi 522 8,11: @(transitive_lt … Hi2) <Hi @le_n 523 3,6: @sym_neq @lt_to_not_eq @le_S_to_le @Hi 524 9,12: @sym_neq @lt_to_not_eq <Hi @le_n 525 ] 526 1,3: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 527 5,7: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n 528 ] 529 ] 530  cases (le_to_or_lt_eq … Hi) Hi #Hi 531 [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) @conj 532 [ #Hj @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?))) 533 cases p p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta 534 [1: #pi cases pi normalize nodelta 535 [1,2,3,6,7,33,34: #x #y 536 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x 537 9,10,11,12,13,14,15,16,17: 538 [1,2,6,7: #x  3,4,5,8,9: #x #id] >lookup_opt_insert_miss 539 [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 540 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 541 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 542 @le_S_S_to_le @le_plus_n_r 543 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 544 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 545 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi) 546 ] 547 ] 548 ] 549 2,3: #x 550 4,5: #id >lookup_opt_insert_miss 551 [2,4: @bitvector_of_nat_abs 552 [1,4: @(transitive_lt … (pi2 ?? program)) >prf 553 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 554 @le_S_S_to_le @le_plus_n_r 555 2,5: @(transitive_lt … (pi2 ?? program)) >prf 556 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 557 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 558 ] 559 ] 560 6: #x #id 561 ] 562 @((proj2 ?? Hp) i (le_S_S_to_le … Hi) Hj) 563  #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i ?)) 564 [ @(le_S_S_to_le … Hi) 565  cases p in H; p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta 566 [1: #id cases id 567 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 568 [1,2,3,6,7,24,25: #x #y 569 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 570 normalize nodelta / by / 571 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #x #id] 572 normalize nodelta >lookup_opt_insert_miss 573 [1,3,5,7,9,11,13,15,17: / by / 574 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 575 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 576 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 577 @le_S_S_to_le @le_plus_n_r 578 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 579 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 580 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi) 581 ] 582 ] 583 ] 584 2,3: #x / by / 585 4,5: #id >lookup_opt_insert_miss 586 [2,4: @bitvector_of_nat_abs 587 [1,4: @(transitive_lt … (pi2 ?? program)) >prf 588 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 589 @le_S_S_to_le @le_plus_n_r 590 2,5: @(transitive_lt … (pi2 ?? program)) >prf 591 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 592 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 593 ] 594 1,3: / by / 595 ] 596 6: #x #id / by / 597 ] 598 ] 599 ] 600  >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (prefix))) 601 <minus_n_n whd in match (nth ????); 602 cases x #l #ins cases ins 603 [1: #pi cases pi 604 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 605 [1,2,3,6,7,24,25: #x #y 606 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 607 @conj 608 [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: 609 #H @⊥ @H 610 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 611 cases p p #p cases p p #pc #pol #Hp #H elim H H #p #H elim H H #a #H elim H H #j 612 normalize nodelta >(proj1 ?? (proj1 ?? Hp) (prefix) (le_n (prefix)) ?) 613 [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: 614 #H destruct (H) 615 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 616 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm 617 @le_S_S_to_le @le_plus_n_r 618 ] 619 ] 620 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x  3,4,5,8,9: #x #id] 621 @conj 622 [1,3,5,7,9,11,13,15,17: 623 #_ @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?))) 624 cases p p #p cases p p #pc #pol #Hp @lookup_opt_insert_hit 625 2,4,6,8,10,12,14,16,18: 626 #_ / by I/ 627 ] 628 ] 629 2,3,6: #x [3: #id] @conj 630 [1,3,5: #H @⊥ @H 631 2,4,6: 632 cases p p #p cases p p #pc #pol #Hp #H elim H H #p #H elim H H #a #H elim H H #j 633 normalize nodelta >(proj1 ?? (proj1 ?? Hp) (prefix) (le_n (prefix)) ?) 634 [1,3,5: #H destruct (H) 635 2,4,6: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm 636 @le_S_S_to_le @le_plus_n_r 637 ] 638 ] 639 4,5: #x @conj 640 [1,3: #_ @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?))) 641 cases p p #p cases p p #pc #pol #Hp @lookup_opt_insert_hit 642 2,4: #_ / by I/ 643 ] 644 ] 645 ] 646 ] 647  #i >append_length <commutative_plus #Hi normalize in Hi; 648 elim (le_to_or_lt_eq … Hi) Hi #Hi 649 [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #H 650 cases p p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta 651 [1: #pi cases pi 652 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 653 [1,2,3,6,7,24,25: #x #y 654 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 655 normalize nodelta 656 @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H) 657 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x  3,4,5,8,9: #x #id] 658 normalize nodelta >lookup_opt_insert_miss 659 [1,3,5,7,9,11,13,15,17: @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H) 660 2,4,6,8,10,12,14,16,18,20: @bitvector_of_nat_abs 661 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 662 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 663 @le_S_S_to_le @le_plus_n_r 664 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 665 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 666 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi) 667 ] 668 ] 669 ] 670 2,3,6: #x [3: #id] 671 normalize nodelta @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H) 672 4,5: #x >lookup_opt_insert_miss 673 [1,3: @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H) 674 2,4: @bitvector_of_nat_abs 675 [1,4: @(transitive_lt … (pi2 ?? program)) >prf 676 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 677 @le_S_S_to_le @le_plus_n_r 678 2,5: @(transitive_lt … (pi2 ?? program)) >prf 679 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 680 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 681 ] 682 ] 683 ] 684  >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (prefix))) 685 <minus_n_n whd in match (nth ????); cases x #l #ins cases ins 686 [1: #pi cases pi 687 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 688 [1,2,3,6,7,24,25: #x #y 689 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 690 #H @⊥ @H 691 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x  3,4,5,8,9: #x #id] 692 #_ cases p p #p cases p p #pc #pol #Hp >lookup_opt_insert_hit / by / 693 ] 694 2,3,6: #x [3: #id] #H @⊥ @H 695 4,5: #id #_ cases p p #p cases p p #pc #pol #Hp >lookup_opt_insert_hit / by / 696 ] 697 ] 698 ] 699  @conj 700 [ @conj 701 [ #i #_ #Hi2 / by refl/ 702  #i #_ @conj 703 [ >nth_nil #H @⊥ @H 704  #H elim H H #p #H elim H H #a #H elim H H #j #H normalize in H; destruct (H) 705 ] 706 ] 707  #i #Hi >nth_nil #H @⊥ @H 708 ] 498 709 ] 499 710 qed. … … 502 713 λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy. 503 714 ∀n:ℕ.n < program → 504 let 〈 i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1〈0,0,short_jump〉 in505 let 〈 i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2〈0,0,short_jump〉 in715 let 〈pc1,i1,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,0,short_jump〉 in 716 let 〈pc2,i2,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,0,short_jump〉 in 506 717 j1 = j2. 507 718 508 719 definition nec_plus_ultra ≝ 509 720 λprogram:list labelled_instruction.λp:jump_expansion_policy. 510 ¬(∀i.i < program → \snd (bvt_lookup … (bitvector_of_nat 16 i) p〈0,0,short_jump〉) = long_jump).721 ¬(∀i.i < program → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). 511 722 723 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a. 724 #a #b / by refl/ 725 qed. 726 512 727 (* One step in the search for a jump expansion fixpoint. *) 513 728 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.l < 2^16). … … 516 731 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 517 732 ∃a.lookup … lm l = Some ? 〈i,a〉). 518 ∀old_policy:(Σpolicy. 519 out_of_program_none program policy ∧ jump_in_policy program policy). 520 (Σx:bool × ℕ × (option jump_expansion_policy). 521 let 〈changed,pc,y〉 ≝ x in 733 ∀old_policy:(Σpolicy:jump_expansion_policy. 734 out_of_program_none program policy ∧ jump_in_policy program policy ∧ (\fst policy < 2^16) ∧ 735 policy_isize_sum program policy). 736 (Σx:bool × (option jump_expansion_policy). 737 let 〈ch,y〉 ≝ x in 522 738 match y with 523 [ None ⇒ pc > 2^16 ∧nec_plus_ultra program old_policy739 [ None ⇒ nec_plus_ultra program old_policy 524 740  Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧ 525 741 jump_in_policy program p ∧ 526 policy_increase program old_policy p ∧ 527 policy_safe p∧528 (changed = false → policy_equal_int program old_policy p)742 policy_increase program old_policy p ∧ policy_safe p ∧ 743 (ch = false → policy_equal_int program old_policy p (*sic!*)) ∧ 744 policy_isize_sum program p ∧ \fst p < 2^16 529 745 ]) 530 746 ≝ 531 747 λprogram.λlabels.λold_policy. 532 let 〈final_changed, final_p c, final_policy〉 ≝748 let 〈final_changed, final_policy〉 ≝ 533 749 foldl_strong (option Identifier × pseudo_instruction) 534 (λprefix.Σx:bool × ℕ ×jump_expansion_policy.535 let 〈changed,p c,policy〉 ≝ x in750 (λprefix.Σx:bool × jump_expansion_policy. 751 let 〈changed,policy〉 ≝ x in 536 752 out_of_program_none prefix policy ∧ labels_okay labels policy ∧ 537 753 jump_in_policy prefix policy ∧ 538 754 policy_increase prefix old_policy policy ∧ 539 755 policy_safe policy ∧ 540 (changed = false → policy_equal_int prefix old_policy policy)) 756 (changed = false → policy_equal_int prefix old_policy policy) ∧ 757 policy_isize_sum prefix policy) 541 758 program 542 759 (λprefix.λx.λtl.λprf.λacc. 543 let 〈changed, pc, policy〉 ≝ acc in 760 let 〈changed, pol〉 ≝ acc in 761 (* let 〈pc,pol〉 ≝ p in *) 544 762 let 〈label,instr〉 ≝ x in 545 (* let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (prefix)) old_policy in *)546 763 let add_instr ≝ 547 764 match instr with 548 [ Instruction i ⇒ jump_expansion_step_instruction labels pci549  Call c ⇒ Some ? (select_call_length labels pcc)550  Jmp j ⇒ Some ? (select_jump_length labels pcj)765 [ Instruction i ⇒ jump_expansion_step_instruction labels (\fst pol) i 766  Call c ⇒ Some ? (select_call_length labels (\fst pol) c) 767  Jmp j ⇒ Some ? (select_jump_length labels (\fst pol) j) 551 768  _ ⇒ None ? 552 769 ] in 553 let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (prefix)) old_policy 〈0, 0, short_jump〉 in 554 match add_instr with 555 [ None ⇒ (* i.e. it's not a jump *) 556 〈changed, add_instruction_size pc long_jump instr, policy〉 557  Some z ⇒ let 〈addr,ai〉 ≝ z in 558 let new_length ≝ max_length old_length ai in 559 〈match dec_eq_jump_length new_length old_length with 560 [ inl _ ⇒ changed 561  inr _ ⇒ true], add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (prefix)) 〈pc, addr, new_length〉 policy〉 562 ] 563 ) 〈false, 0, Stub ? ?〉 in 564 if geb final_pc 2^16 then 565 〈final_changed,final_pc,None ?〉 770 let old_length ≝ \snd (bvt_lookup … (bitvector_of_nat 16 (prefix)) (\snd old_policy) 〈0,0,short_jump〉) in 771 match add_instr with 772 [ None ⇒ (* i.e. it's not a jump *) 773 let isize ≝ instruction_size short_jump instr in 774 〈changed, 〈(\fst pol) + isize, (\snd pol)〉〉 775  Some z ⇒ let 〈addr,ai〉 ≝ z in 776 let new_length ≝ max_length old_length ai in 777 let isize ≝ instruction_size new_length instr in 778 〈match dec_eq_jump_length new_length old_length with 779 [ inl _ ⇒ changed 780  inr _ ⇒ true], 〈(\fst pol) + isize, 781 insert … (bitvector_of_nat 16 (prefix)) 〈(\fst pol), addr, new_length〉 (\snd pol)〉〉 782 ] 783 ) 〈false, 〈0, Stub ? ?〉〉 in 784 if geb (\fst final_policy) 2^16 then 785 〈final_changed,None ?〉 566 786 else 567 〈final_changed,final_pc,Some jump_expansion_policy final_policy〉. 568 [ normalize nodelta @conj 569 [ @leb_true_to_le @p2 570  @nmk #Hfull (* XXX *) cases daemon 787 〈final_changed,Some ? final_policy〉. 788 [ @pair_elim #fch #x #Heq <(pair_eq2 ?????? Heq) normalize nodelta 789 @nmk #Hfull lapply p generalize in match (foldl_strong ?????); * #x #H #H2 790 >H2 in H; normalize nodelta H2 x #H 791 @(absurd ((\fst final_policy) ≥ 2^16)) 792 [ @leb_true_to_le <geb_to_leb @p1 793  @lt_to_not_le @(le_to_lt_to_lt … (proj2 ?? (proj1 ?? (pi2 ?? old_policy)))) 794 >(proj2 ?? H) >(proj2 ?? (pi2 ?? old_policy)) 795 cases daemon (* XXX *) 571 796 ] 572 797  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 573 >H2 in H; >p1 normalize nodelta // 574  lapply (pi2 ?? acc) >p >p1 normalize nodelta #Hpolicy 575 @conj [ @conj [ @conj [ @conj [ @conj 576 [ (* out_of_policy_none *) 798 >H2 in H; normalize nodelta #H @conj 799 [ @H 800  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 801 ] 802  lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy; 803 cases (dec_eq_jump_length new_length old_length) #Hlength normalize nodelta 804 @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj 805 [1,3: (* out_of_policy_none *) 577 806 #i >append_length <commutative_plus #Hi normalize in Hi; 578 807 #Hi2 >lookup_opt_insert_miss 579 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) @Hi2580  >eq_bv_sym @bitvector_of_nat_abs581 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm808 [1,3: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi)) @Hi2 809 2,4: >eq_bv_sym @bitvector_of_nat_abs 810 [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 582 811 @le_S_S @le_plus_n_r 583  @Hi2 584  @lt_to_not_eq @Hi 585 ] 586 ] 587  (* labels_okay *) 588 @lookup_forall #i cases i i #i cases i i #p #a #j #n (*lapply (refl ? add_instr) 589 cases (lookup ??? old_policy ?); #x cases x x #p1 #p2 #p3 590 cases add_instr in ⊢ (???% → %); 591 [ #Hai normalize nodelta #Hl 592 elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl) 812 2,5: @Hi2 813 3,6: @lt_to_not_eq @Hi 814 ] 815 ] 816 2,4: (* labels_okay *) 817 @lookup_forall #i cases i i #i cases i i #p #a #j #n #Hl 818 elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) Hl #Hl 819 [1,3: elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? n Hl) 593 820 #i #Hi @(ex_intro ?? i Hi) 594  #x cases x x #np #nl #Hai normalize nodelta *) #Hl 595 elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) Hl #Hl 596 [ elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl) 597 #i #Hi @(ex_intro ?? i Hi) 598  (*whd in match add_instr in Hai; cases instr in Hai;*) normalize nodelta 599 normalize nodelta in p4; cases instr in p4; 600 [2,3: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 601 6: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 602 1: #pi cases pi 603 [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 604 1,2,3,6,7,33,34: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) 605 #H destruct (H) 606 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #abs normalize in abs; 607 lapply (jmeq_to_eq ??? abs) #H destruct (H) 608 9,10,14,15: #id normalize nodelta whd in match (jump_expansion_step_instruction ???); 609 whd in match (select_reljump_length ???); >p5 610 lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) 611 cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 612 normalize nodelta #H 613 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 614 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) 615 cases (leb pc q2) in ⊢ (???% → %); #Hle1 616 [1,3,5,7: lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %); 617 2,4,6,8: lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %); 618 ] 619 #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H 620 <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl 621 11,12,13,16,17: #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???); 622 whd in match (select_reljump_length ???); >p5 623 lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) 624 cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 625 normalize nodelta #H 626 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 627 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2)) 628 cases (leb pc q2) in ⊢ (???% → %); #Hle1 629 [1,3,5,7,9: lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %); 630 2,4,6,8,10: lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %); 631 ] 632 #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H 633 <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl 821 2,4: normalize nodelta normalize nodelta in p2; cases instr in p2; 822 [2,3,8,9: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 823 6,12: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 824 1,7: #pi cases pi 825 [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 826 1,2,3,6,7,33,34,38,39,40,43,44,70,71: 827 #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 828 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: 829 #x #abs normalize in abs;lapply (jmeq_to_eq ??? abs) #H destruct (H) 830 9,10,14,15,46,47,51,52: 831 #id normalize nodelta whd in match (jump_expansion_step_instruction ???); 832 whd in match (select_reljump_length ???); >p3 833 lapply (refl ? (lookup_def ?? (pi1 ?? labels) id 〈0,\fst pol〉)) 834 cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 835 normalize nodelta #H 836 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 837 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) 838 cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 839 [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 840 2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 634 841 ] 635 4,5: #id normalize nodelta whd in match (select_jump_length ???); 636 whd in match (select_call_length ???); >p5 637 lapply (refl ? (lookup_def ?? labels id 〈0,pc〉)) 638 cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 639 normalize nodelta #H 640 [1: cases (leb pc q2) 641 [ cases (leb (q2pc) 126)  cases (leb (pcq2) 129) ] 642 [1,3: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; 643 #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl) 644 #H >(pair_eq1 ?????? (pair_eq1 ?????? H)) 645 >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl] 646 ] 647 cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2 648 cases (split ? 5 11 (bitvector_of_nat 16 pc)) #m1 #m2 649 normalize nodelta cases (eq_bv ? n1 m1) 650 normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H 651 @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2 652 >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2)) 653 >H @refl 654 ] 655 ] 656 ] 657  (* jump_in_policy *) 842 #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H 843 <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl 844 11,12,13,16,17,48,49,50,53,54: 845 #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???); 846 whd in match (select_reljump_length ???); >p3 847 lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉)) 848 cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 849 normalize nodelta #H 850 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 851 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) 852 cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 853 [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 854 2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 855 ] 856 #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H 857 <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl 858 ] 859 4,5,10,11: #id normalize nodelta whd in match (select_jump_length ???); 860 whd in match (select_call_length ???); >p3 861 lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉)) 862 cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 863 normalize nodelta #H 864 [1,3: cases (leb (\fst pol) q2) 865 [1,3: cases (leb (q2\fst pol) 126) 2,4: cases (leb (\fst polq2) 129) ] 866 [1,3,5,7: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; 867 #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl) 868 #H >(pair_eq1 ?????? (pair_eq1 ?????? H)) 869 >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl] 870 ] 871 cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2 872 cases (split ? 5 11 (bitvector_of_nat 16 (\fst pol))) #m1 #m2 873 normalize nodelta cases (eq_bv ? n1 m1) 874 normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H 875 @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2 876 >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2)) 877 >H @refl 878 ] 879 ] 880 ] 881 2,4: (* jump_in_policy *) 658 882 #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 659 [ >append_length <commutative_plus #Hi normalize in Hi;883 [1,3: >append_length <commutative_plus #Hi normalize in Hi; 660 884 >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj 661 [ #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))885 [1,3: #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi)) 662 886 #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n n #n #H elim H H #j #Hj 663 887 @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???); 664 >lookup_opt_insert_miss [ @Hj @bitvector_of_nat_abs ]665 [3 : @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi)666 1 : @(transitive_lt ??? (le_S_S_to_le ?? Hi))888 >lookup_opt_insert_miss [1,3: @Hj 2,4: @bitvector_of_nat_abs ] 889 [3,6: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 890 1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 667 891 ] 668 892 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 669 893 @le_S_S @le_plus_n_r 670  lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) #Hacc671 #H elim H H; #h #H elim H H; #n #H elim H H #j672 #Hl@(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))894 2,4: lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi)) 895 #Hacc #H elim H H; #h #H elim H H; #n #H elim H H #j #Hl 896 @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) 673 897 <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs 674 [3 : @lt_to_not_eq @(le_S_S_to_le … Hi)675 1 : @(transitive_lt ??? (le_S_S_to_le ?? Hi))898 [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 899 1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 676 900 ] 677 901 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 678 902 @le_S_S @le_plus_n_r 679 903 ] 680  >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi)904 2,4: >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi) 681 905 >(nth_append_second ?? prefix ?? (le_n (prefix))) 682 <minus_n_n whd in match (nth ????); normalize nodelta in p 4; cases instr in p4;683 [1 : #pi  2,3: #x  4,5: #id  6: #x #y] #Hinstr @conj normalize nodelta684 [ 3,5,11: #H @⊥ @H (* instr is not a jump *)685  4,6,12: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr)906 <minus_n_n whd in match (nth ????); normalize nodelta in p2; cases instr in p2; 907 [1,7: #pi  2,3,8,9: #x  4,5,10,11: #id  6,12: #x #y] #Hinstr @conj normalize nodelta 908 [5,7,9,11,21,23: #H @⊥ @H (* instr is not a jump *) 909 6,8,10,12,22,24: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr) 686 910 #H destruct (H) 687  7,9: (* instr is a jump *) #_ @(ex_intro ?? pc)911 13,15,17,19: (* instr is a jump *) #_ @(ex_intro ?? (\fst pol)) 688 912 @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 689 913 @lookup_opt_insert_hit 690 8,10: #_ / by I/ 691 1,2: cases pi in Hinstr; 692 [35,36,37: #Hinstr #H @⊥ @H 693 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hinstr #H @⊥ @H 694 1,2,3,6,7,33,34: #x #y #Hinstr #H @⊥ @H 695 9,10,14,15: #id #Hinstr #_ 696 @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 914 14,16,18,20: #_ / by I/ 915 1,2,3,4: cases pi in Hinstr; 916 [35,36,37,109,110,111: #Hinstr #H @⊥ @H 917 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,78,79,82,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106: 918 #x #Hinstr #H @⊥ @H 919 1,2,3,6,7,33,34,75,76,77,80,81,107,108: #x #y #Hinstr #H @⊥ @H 920 9,10,14,15,83,84,88,89: #id #Hinstr #_ 921 @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 697 922 @lookup_opt_insert_hit 698 11,12,13,16,17 : #x #id #Hinstr #_699 @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))923 11,12,13,16,17,85,86,87,90,91: #x #id #Hinstr #_ 924 @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 700 925 @lookup_opt_insert_hit 701 72,73,74 : #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)702 41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69 : #x #Hinstr703 lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)704 38,39,40,43,44,70,71 : #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H926 72,73,74,146,147,148: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) 927 41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,115,116,119,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143: 928 #x #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) 929 38,39,40,43,44,70,71,112,113,114,117,118,144,145: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H 705 930 normalize in H; destruct (H) 706 46,47,51,52 : #id #Hinstr #_ / by I/707 48,49,50,53,54 : #x #id #Hinstr #_ / by I/931 46,47,51,52,120,121,125,126: #id #Hinstr #_ / by I/ 932 48,49,50,53,54,122,123,124,127,128: #x #id #Hinstr #_ / by I/ 708 933 ] 709 934 ] 710 935 ] 711 936 ] 712  (* policy increase *)937 2,4: (* policy increase *) 713 938 #i >append_length >commutative_plus #Hi normalize in Hi; 714 939 cases (le_to_or_lt_eq … Hi) Hi; #Hi 715 [ >lookup_insert_miss716 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))717  @bitvector_of_nat_abs718 [3 : @lt_to_not_eq @(le_S_S_to_le … Hi)719 1 : @(transitive_lt ??? (le_S_S_to_le … Hi))940 [1,3: >lookup_insert_miss 941 [1,3: @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) 942 2,4: @bitvector_of_nat_abs 943 [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 944 1,4: @(transitive_lt ??? (le_S_S_to_le … Hi)) 720 945 ] 721 946 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 722 947 @le_S_S @le_plus_n_r 723 948 ] 724  >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta 725 @pair_elim #x #y #_ @jmpleq_max_length 949 2: >(injective_S … Hi) normalize nodelta in Hlength; >lookup_insert_hit normalize nodelta 950 >Hlength @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy 951 >Hl %2 @refl 952 4: cases daemon (* XXX get rest of proof done first *) 726 953 ] 727 954 ] 728  (* policy_safe *)955 2,4: (* policy_safe *) 729 956 @lookup_forall #x cases x x #x cases x x #p #a #j #n normalize nodelta #Hl 730 957 elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) Hl #Hl 731 [ @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)732  normalize nodelta in p4; cases instr in p4;733 [2,3 : #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)734 6 : #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)735 1 : #pi cases pi normalize nodelta736 [35,36,37 : #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)737 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32 :738 #x #abs @⊥normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)739 1,2,3,6,7,33,34 : #x #y #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H740 destruct (H)741 9,10,14,15 : #id >p5whd in match (jump_expansion_step_instruction ???);958 [1,3: @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl) 959 2,4: normalize nodelta in p2; cases instr in p2; 960 [2,3,8,9: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 961 6,12: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 962 1,7: #pi cases pi normalize nodelta 963 [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 964 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: 965 #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 966 1,2,3,6,7,33,34,38,39,40,43,44,70,71: 967 #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 968 9,10,14,15,46,47,51,52: #id >p3 whd in match (jump_expansion_step_instruction ???); 742 969 whd in match (select_reljump_length ???); 743 cases (lookup_def ?? labels id 〈0, pc〉) #q1 #q2 normalize nodelta970 cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta 744 971 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 745 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pcq2))746 cases (leb pcq2) in ⊢ (???% → %); #Hle1747 [1,3,5,7 : lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %);748 2,4,6,8 : lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %);972 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) 973 cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 974 [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 975 2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 749 976 ] 750 977 #Hle2 normalize nodelta #Hli 751 978 <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 752 979 >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli)) 753 cases old_length754 [1,7,13,19,25,31,37,43 : @(leb_true_to_le … Hle2)980 cases (\snd (lookup ?? (bitvector_of_nat ? (prefix)) (\snd old_policy) ?)) 981 [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91: @(leb_true_to_le … Hle2) 755 982 ] normalize @I (* much faster than / by I/, strangely enough *) 756 11,12,13,16,17 : #x #id >p5whd in match (jump_expansion_step_instruction ???);983 11,12,13,16,17,48,49,50,53,54: #x #id >p3 whd in match (jump_expansion_step_instruction ???); 757 984 whd in match (select_reljump_length ???); 758 cases (lookup_def ?? labels id 〈0, pc〉) #q1 #q2 normalize nodelta985 cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta 759 986 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 760 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pcq2))761 cases (leb pcq2) in ⊢ (???% → %); #Hle1762 [1,3,5,7,9 : lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %);763 2,4,6,8,10 : lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %);987 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) 988 cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 989 [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 990 2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 764 991 ] 765 992 #Hle2 normalize nodelta #Hli 766 993 <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl)) 767 994 <(pair_eq2 ?????? (Some_eq ??? Hli)) 768 cases old_length769 [1,7,13,19,25,31,37,43,49,55 : @(leb_true_to_le … Hle2)995 cases (\snd (lookup ?? (bitvector_of_nat ? (prefix)) (\snd old_policy) ?)) 996 [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91,97,103,109,115: @(leb_true_to_le … Hle2) 770 997 ] normalize @I (* vide supra *) 771 998 ] 772 4,5 : #id >p5normalize nodelta whd in match (select_jump_length ???);773 whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0, pc〉)999 4,5,10,11: #id >p3 normalize nodelta whd in match (select_jump_length ???); 1000 whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,\fst pol〉) 774 1001 #q1 #q2 normalize nodelta 775 1002 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 776 1003 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 777 [1 : lapply (refl ? (leb pc q2)) cases (leb pcq2) in ⊢ (???% → %); #Hle1778 [ lapply (refl ? (leb (q2pc) 126)) cases (leb (q2pc) 126) in ⊢ (???% → %);779  lapply (refl ? (leb (pcq2) 129)) cases (leb (pcq2) 129) in ⊢ (???% → %);1004 [1,3: lapply (refl ? (leb (\fst pol) q2)) cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 1005 [1,3: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 1006 2,4: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 780 1007 ] 781 1008 #Hle2 normalize nodelta 782 1009 ] 783 [2,4, 5: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2)))1010 [2,4,6,8,9,10: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2))) 784 1011 cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3 785 lapply (refl ? (split ? 5 11 (bitvector_of_nat ? pc)))786 cases (split ??? (bitvector_of_nat ? pc)) in ⊢ (???% → %); #y1 #y2 #Hle41012 lapply (refl ? (split ? 5 11 (bitvector_of_nat ? (\fst pol)))) 1013 cases (split ??? (bitvector_of_nat ? (\fst pol))) in ⊢ (???% → %); #y1 #y2 #Hle4 787 1014 normalize nodelta lapply (refl ? (eq_bv 5 x1 y1)) 788 1015 cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5 … … 790 1017 #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl)) 791 1018 <(pair_eq2 ?????? (Some_eq ??? Hli)) 792 cases old_length793 [2,8,14 : >Hle3 @Hle5794  19,22: >Hle1 @(leb_true_to_le … Hle2)1019 cases (\snd (lookup ?? (bitvector_of_nat ? (prefix)) (\snd old_policy) ?)) 1020 [2,8,14,20,26,32: >Hle3 @Hle5 1021 37,40,43,46: >Hle1 @(leb_true_to_le … Hle2) 795 1022 ] normalize @I (* here too *) 796 1023 ] 797 1024 ] 798 1025 ] 799  (* changed *) 800 cases (dec_eq_jump_length (max_length old_length ai) old_length) normalize nodelta 801 [ #Hml #Hc #i #Hi cases (le_to_or_lt_eq … Hi) Hi >append_length >commutative_plus #Hi 802 normalize in Hi; 803 [ >lookup_insert_miss 804 [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) 805  @bitvector_of_nat_abs 806 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 807 1: @(transitive_lt ??? (le_S_S_to_le … Hi)) 808 ] 809 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 810 @le_S_S @le_plus_n_r 811 ] 812  >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta 813 @pair_elim #x #y #_ @(sym_eq ??? Hml) 814 ] 815  #_ #H destruct (H) 816 ] 1026 2,4: (* changed *) 1027 normalize nodelta #Hc [2: destruct (Hc)] #i #Hi cases (le_to_or_lt_eq … Hi) Hi 1028 >append_length >commutative_plus #Hi 1029 normalize in Hi; 1030 [ >lookup_insert_miss 1031 [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) 1032  @bitvector_of_nat_abs 1033 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 1034 1: @(transitive_lt ??? (le_S_S_to_le … Hi)) 1035 ] 1036 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1037 @le_S_S @le_plus_n_r 1038 ] 1039  >(injective_S … Hi) >lookup_insert_hit normalize nodelta in Hlength; >Hlength 1040 normalize nodelta @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy >Hl @refl 1041 ] 817 1042 ] 1043 2,4: (* policy_isize_sum XXX *) cases daemon 1044 ] 818 1045  (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1 819 1046 normalize nodelta #Hpolicy 820 @conj [ @conj [ @conj [ @conj [ @conj 1047 @conj [ @conj [ @conj [ @conj [ @conj [ @conj 821 1048 [ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi; 822 #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le ?? Hi) Hi2)1049 #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le ?? Hi) Hi2) 823 1050  (* labels_okay *) @lookup_forall #x cases x x #x cases x #p #a #j #lbl #Hl normalize nodelta 824 elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? lbl Hl)1051 elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? lbl Hl) 825 1052 #id #Hid @(ex_intro … id Hid) 826 1053 ] … … 828 1055 elim (le_to_or_lt_eq … Hi) Hi #Hi 829 1056 [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) 830 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le ?? Hi))1057 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le ?? Hi)) 831 1058  >(injective_S … Hi) @conj 832 1059 [ >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n whd in match (nth ????); 833 normalize nodelta in p 4; cases instr in p4;1060 normalize nodelta in p2; cases instr in p2; 834 1061 [ #pi cases pi 835 1062 [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H … … 848 1075 ] 849 1076  #H elim H H #p #H elim H H #a #H elim H H #j #H 850 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (prefix) (le_n (prefix)) ?) in H;1077 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (prefix) (le_n (prefix)) ?) in H; 851 1078 [ #H destruct (H) 852 1079  @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm … … 858 1085  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 859 1086 elim (le_to_or_lt_eq … Hi) Hi #Hi 860 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))1087 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) 861 1088  >(injective_S … Hi) >lookup_opt_lookup_miss 862 1089 [ >lookup_opt_lookup_miss 863 1090 [ normalize nodelta %2 @refl 864  @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (prefix) (le_n (prefix)) ?)1091  @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (prefix) (le_n (prefix)) ?) 865 1092 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 866 1093 @le_S_S @le_plus_n_r 867 1094 ] 868  @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy(prefix) ?)) >prf1095  @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (prefix) ?)) >prf 869 1096 [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 870  >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n >p 2871 whd in match (nth ????); normalize nodelta in p 4; cases instr in p4;1097  >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n >p1 1098 whd in match (nth ????); normalize nodelta in p2; cases instr in p2; 872 1099 [ #pi cases pi 873 1100 [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ … … 890 1117 ] 891 1118  (* policy_safe *) @lookup_forall #x cases x x #x cases x x #p #a #j #n #Hl 892 @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)1119 @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl) 893 1120 ] 894 1121  (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi; 895 1122 elim (le_to_or_lt_eq … Hi) Hi #Hi 896 [ @( (proj2?? Hpolicy) Hc i (le_S_S_to_le … Hi))1123 [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) 897 1124  >(injective_S … Hi) >lookup_opt_lookup_miss 898 1125 [ >lookup_opt_lookup_miss 899 1126 [ normalize nodelta @refl 900  @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (prefix) (le_n (prefix)) ?)1127  @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (prefix) (le_n (prefix)) ?) 901 1128 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 902 1129 @le_S_S @le_plus_n_r 903 1130 ] 904  @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy(prefix) ?)) >prf1131  @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (prefix) ?)) >prf 905 1132 [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 906  >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n >p 2907 whd in match (nth ????); normalize nodelta in p 4; cases instr in p4;1133  >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n >p1 1134 whd in match (nth ????); normalize nodelta in p2; cases instr in p2; 908 1135 [ #pi cases pi 909 1136 [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ … … 924 1151 ] 925 1152 ] 926 ] 927  @conj [ @conj [ @conj [ @conj [ @conj 928 [ #i #Hi // 929  // 1153 ] 1154  (* XXX policy_isize_sum *) cases daemon 1155 ] 1156  @conj [ @conj [ @conj [ @conj [ @conj [ @conj 1157 [ #i #Hi / by refl/ 1158  / by I/ 930 1159 ] 931 1160  #i #Hi @conj [ >nth_nil #H @⊥ @H  #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3 … … 934 1163  #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 935 1164 ] 936  / /1165  / by I/ 937 1166 ] 938 1167  #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi  @not_le_Sn_O ] 939 1168 ] 1169  / by refl/ 1170 ] 1171 ] 940 1172 qed. 941 1173 … … 979 1211 980 1212 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (l) 2^16) (n: ℕ) 981 on n:(Σx:bool × ℕ ×(option jump_expansion_policy).982 let 〈c,p c,y〉 ≝ x in983 match ywith984 [ None ⇒ pc > 2^16985  Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)1213 on n:(Σx:bool × (option jump_expansion_policy). 1214 let 〈c,pol〉 ≝ x in 1215 match pol with 1216 [ None ⇒ True 1217  Some x ⇒ And (And (And (out_of_program_none program x) (jump_in_policy program x)) (\fst x < 2^16)) (policy_isize_sum program x) 986 1218 ]) ≝ 987 1219 match n with 988 [ O ⇒ 〈true, 0,Some ? (pi1 ?? (jump_expansion_start program))〉989  S m ⇒ let 〈ch, pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in990 match z return λx. z=x → Σa:bool × ℕ ×(option jump_expansion_policy).? with991 [ None ⇒ λp2.〈false, pc,None ?〉1220 [ O ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program))〉 1221  S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 1222 match z return λx. z=x → Σa:bool × (option jump_expansion_policy).? with 1223 [ None ⇒ λp2.〈false,None ?〉 992 1224  Some op ⇒ λp2.if ch 993 1225 then pi1 ?? (jump_expansion_step program (create_label_map program op) «op,?») … … 995 1227 ] (refl … z) 996 1228 ]. 997 [ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program))) 1229 [ normalize nodelta @conj 1230 [ @conj 1231 [ @(proj1 ?? (pi2 ?? (jump_expansion_start program))) 1232  (* XXX *) cases daemon 1233 ] 1234  (* XXX *) cases daemon 1235 ] 998 1236  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 999  3: lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /1237  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 1000 1238  normalize nodelta cases (jump_expansion_step program (create_label_map program op) «op,?») 1001 #p cases p p #p cases p p #p #q#r cases r normalize nodelta1002 [ #H @(proj1 ?? H)1239 #p cases p p #p #r cases r normalize nodelta 1240 [ #H / by I/ 1003 1241  #j #H @conj 1004 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1005  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 1242 [ @conj 1243 [ @conj 1244 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))) 1245  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 1246 ] 1247  @(proj2 ?? H) 1248 ] 1249  @(proj2 ?? (proj1 ?? H)) 1006 1250 ] 1007 1251 ] … … 1011 1255 lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program). 1012 1256 #program whd #x whd #n #Hn 1013 cases (bvt_lookup … (bitvector_of_nat ? n) x〈0,0,short_jump〉)1257 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,0,short_jump〉) 1014 1258 #y cases y y #y #z normalize nodelta @refl 1015 1259 qed. … … 1017 1261 lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program). 1018 1262 #program whd #x #y #Hxy whd #n #Hn 1019 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x〈0,0,short_jump〉)1263 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉) 1020 1264 #z cases z z #x1 #x2 #x3 1021 cases (bvt_lookup … (bitvector_of_nat ? n) y〈0,0,short_jump〉)1265 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉) 1022 1266 #z cases z z #y1 #y2 #y3 normalize nodelta // 1023 1267 qed. … … 1026 1270 #program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?); 1027 1271 whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy 1028 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) x〈0,0,short_jump〉)1272 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉) 1029 1273 #z cases z z #x1 #x2 #x3 1030 cases (bvt_lookup … (bitvector_of_nat ? n) y〈0,0,short_jump〉) #z cases z z1274 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉) #z cases z z 1031 1275 #y1 #y2 #y3 1032 cases (bvt_lookup … (bitvector_of_nat ? n) z〈0,0,short_jump〉) #z cases z z1276 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,0,short_jump〉) #z cases z z 1033 1277 #z1 #z2 #z3 normalize nodelta // 1034 1278 qed. … … 1087 1331 lapply (refl ? (jump_expansion_internal program (n+k'))) 1088 1332 cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %); 1089 #x2 cases x2 x2 # x2 cases x2 x2 #c2 #p2 #j2 normalize nodelta #H #Heqj21090 cases j2 in H Heqj2;1333 #x2 cases x2 x2 #c2 #p2 normalize nodelta #H #Heqj2 1334 cases p2 in H Heqj2; 1091 1335 [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??); 1092 1336 >Heqj2 normalize nodelta @refl … … 1130 1374 match program with 1131 1375 [ nil ⇒ acc 1132  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy〈0,001376  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,00 1133 1377 ,short_jump〉)) with 1134 1378 [ long_jump ⇒ measure_int t policy (acc + 2) … … 1145 1389 [ / by refl/ 1146 1390  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1147 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy〈0,0,short_jump〉))1391 cases (\snd (lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) 1148 1392 [ normalize nodelta @Hd 1149 1393 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus … … 1159 1403 [ normalize @le_n 1160 1404  #h #t #Hind whd in match (measure_int ???); 1161 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) policy〈0,0,short_jump〉))1405 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) 1162 1406 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1163 1407 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) 1164 @le_plus [1,3: @Hind 2,4: / / ]1408 @le_plus [1,3: @Hind 2,4: / by le_n/ ] 1165 1409 ] 1166 1410 ] … … 1169 1413 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.l<2^16. 1170 1414 ∀policy:Σp:jump_expansion_policy. 1171 out_of_program_none program p ∧ jump_in_policy program p .1415 out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p. 1172 1416 ∀l.l ≤ program → ∀acc:ℕ. 1173 1417 match \snd (jump_expansion_step program (create_label_map program policy) policy) with … … 1179 1423  #h #t #Hind #Hp #acc 1180 1424 lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy)) 1181 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 pi1 #pi1 cases pi1 1182 #p #q #r pi1; cases r 1183 [ // 1184  #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? Hx)) (t) Hp) 1425 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 pi1 #c #r cases r 1426 [ / by I/ 1427  #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (t) Hp) 1185 1428 whd in match (measure_int ???); whd in match (measure_int ? x ?); 1186 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) policy〈0,0,short_jump〉)1429 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉) 1187 1430 #z cases z z #x1 #x2 #x3 1188 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) x〈0,0,short_jump〉)1431 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,0,short_jump〉) 1189 1432 #z cases z z #y1 #y2 #y3 1190 1433 normalize nodelta #Hj cases Hj … … 1223 1466 lemma measure_full: ∀program.∀policy. 1224 1467 measure_int program policy 0 = 2*program → ∀i.i<program → 1225 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy〈0,0,short_jump〉)) = long_jump.1468 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,0,short_jump〉)) = long_jump. 1226 1469 #program #policy elim program 1227 1470 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1228 1471  #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*t) 1229 1472 [ whd in match (measure_int ???) in Hm; 1230 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy〈0,0,short_jump〉)) in Hm;1473 cases (\snd (lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) in Hm; 1231 1474 normalize nodelta 1232 1475 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ … … 1240 1483 [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi)) 1241 1484  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1242 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy〈0,0,short_jump〉)) in Hm;1485 cases (\snd (lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉)) in Hm; 1243 1486 normalize nodelta 1244 1487 [ >Hmt normalize <plus_n_O >(commutative_plus (t) (S (t))) … … 1254 1497 lemma measure_special: ∀program:(Σl:list labelled_instruction.l < 2^16). 1255 1498 ∀policy:Σp:jump_expansion_policy. 1256 out_of_program_none program p ∧ jump_in_policy program p .1499 out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p. 1257 1500 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with 1258 1501 [ None ⇒ True … … 1260 1503 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) 1261 1504 cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %); 1262 #p cases p p # p cases p p #ch #pc#pol normalize nodelta cases pol1263 [ / /1505 #p cases p p #ch #pol normalize nodelta cases pol 1506 [ / by I/ 1264 1507  #p normalize nodelta #Hpol #eqpol lapply (le_n (program)) 1265 1508 @(list_ind ? (λx.x ≤ pi1 ?? program → … … 1269 1512  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 1270 1513 [ #Hi @Hind 1271 [ @(transitive_le … Hp) / /1514 [ @(transitive_le … Hp) / by / 1272 1515  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 1273 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (t) Hp)1516 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) 1274 1517 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in Hm; 1275 1518 #x cases x x #x1 #x2 #x3 … … 1296 1539  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1297 1540 whd in match (measure_int ? p ?) in Hm; 1298 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (t) Hp)1541 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) 1299 1542 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in 1300 1543 Hm; … … 1378 1621 [ lapply (refl ? (jump_expansion_internal program (2*program))) 1379 1622 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → %); 1380 #x cases x x # x cases x #Fch #Fpc #Fpol normalize nodelta #HFpol cases Fpol in HFpol;1623 #x cases x x #Fch #Fpol normalize nodelta #HFpol cases Fpol in HFpol; normalize nodelta 1381 1624 [ (* if we're at None in 2*program, we're at None in S 2*program too *) 1382 1625 #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ 1383 normalize nodelta / /1626 normalize nodelta / by / 1384 1627  #Fp #HFp #EQ whd in match (jump_expansion_internal ??); 1385 1628 >EQ normalize nodelta … … 1389 1632 [ @le_to_le_to_eq 1390 1633 [ @measure_le 1391  (* XXX *) cases daemon 1634  cut (∀x:ℕ.x ≤ 2*program → 1635 ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ 1636 x ≤ measure_int program p 0)) 1637 [ #x elim x 1638 [ #Hx @(ex_intro ?? (jump_expansion_start program)) @conj 1639 [ whd in match (jump_expansion_internal ??); @refl 1640  @le_O_n 1641 ] 1642  x #x #Hind #Hx 1643 lapply (refl ? (jump_expansion_internal program (S x))) 1644 cases (jump_expansion_internal program (S x)) in ⊢ (???% → %); 1645 #z cases z z #Sxch #Sxpol cases Sxpol Sxpol normalize nodelta 1646 [ #H #HeqSxpol @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk 1647 @(absurd … (step_none program (S x) ? k)) 1648 [ >HeqSxpol / by / 1649  <Hk >EQ @nmk #H destruct (H) 1650 ] 1651  #Sxpol #HSxpol #HeqSxpol @(ex_intro ?? Sxpol) @conj 1652 [ @refl 1653  elim (Hind (transitive_le … (le_n_Sn x) Hx)) 1654 #xpol #Hxpol @(le_to_lt_to_lt … (proj2 ?? Hxpol)) 1655 lapply (measure_incr_or_equal program xpol program (le_n (program)) 0) 1656 [ cases (jump_expansion_internal program x) in Hxpol; 1657 #z cases z z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H; 1658 normalize nodelta / by / 1659  lapply (Hfa x Hx) lapply HeqSxpol HeqSxpol 1660 whd in match (jump_expansion_internal program (S x)); 1661 lapply (refl ? (jump_expansion_internal program x)) 1662 lapply Hxpol Hxpol cases (jump_expansion_internal program x) in ⊢ (% → ???% → %); 1663 #z cases z z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H; 1664 #H #Heq cases xch in Heq; #Heq normalize nodelta 1665 [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»)) 1666 cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 1667 normalize nodelta cases c normalize nodelta 1668 [ #H1 #Heq #H2 destruct (H2) 1669  #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2) 1670 [ / by / 1671  #H3 lapply (measure_special program «xpol,H») >Heq 1672 normalize nodelta #H4 @⊥ 1673 @(absurd … (H4 H3)) 1674 @Hfull 1675 ] 1676 ] 1677  lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»)) 1678 cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 1679 normalize nodelta cases c normalize nodelta 1680 [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl 1681  #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl 1682 ] 1683 ] 1684 ] 1685 ] 1686 ] 1687 ] 1688  #H elim (H (2*program) (le_n ?)) #plp >EQ #Hplp 1689 >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp) 1690 ] 1392 1691 ] 1393 1692  #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %); 1394 #x cases x x # x cases x x #Gch #Gpc#Gpol cases Gpol normalize nodelta1395 [ #H #EQ2 @⊥ @(absurd ?? (proj2 ?? H)) @Hfull1693 #x cases x x #Gch #Gpol cases Gpol normalize nodelta 1694 [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull 1396 1695  #Gp #HGp #EQ2 cases Fch 1397 1696 [ normalize nodelta #i #Hi 1398 lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) Fp〈0,0,short_jump〉))1399 cases (lookup ?? (bitvector_of_nat 16 i) Fp〈0,0,short_jump〉) in ⊢ (???% → %);1697 lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉)) 1698 cases (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉) in ⊢ (???% → %); 1400 1699 #x cases x x #p #a #j normalize nodelta #H 1401 lapply (proj2 ?? (proj1 ?? (proj1 ?? HGp)) i Hi) lapply (Hfull i Hi) >H1402 #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) Gp 〈0,0,short_jump\rangle)1700 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) lapply (Hfull i Hi) >H 1701 #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) (\snd Gp) 〈0,0,short_jump〉) 1403 1702 #x cases x x #p #a #j' cases j' normalize nodelta #H elim H H #H 1404 1703 [1,3: @⊥ @H … … 1415 1714 ] 1416 1715  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 1417 #x cases x x # x cases x x #nch #npc#npol normalize nodelta #Hnpol1418 #x cases x x # x cases x x #Sch #Scp#Spol normalize nodelta #HSpol1716 #x cases x x #nch #npol normalize nodelta #Hnpol 1717 #x cases x x #Sch #Spol normalize nodelta #HSpol 1419 1718 cases npol in Hnpol; cases Spol in HSpol; 1420 1719 [ #Hnpol #HSpol %1 // … … 1434 1733 * a map from pc to jump_length. This cannot be done earlier because the pc 1435 1734 * changes between iterations. *) 1436 let rec transform_policy (n: nat) policy(acc: BitVectorTrie jump_length 16) on n:1735 let rec transform_policy (n: nat) (policy: jump_expansion_policy) (acc: BitVectorTrie jump_length 16) on n: 1437 1736 BitVectorTrie jump_length 16 ≝ 1438 1737 match n with 1439 1738 [ O ⇒ acc 1440 1739  S n' ⇒ 1441 match lookup_opt … (bitvector_of_nat 16 n') policywith1740 match lookup_opt … (bitvector_of_nat 16 n') (\snd policy) with 1442 1741 [ None ⇒ transform_policy n' policy acc 1443  Some x ⇒ let 〈pc, length〉 ≝ x in1444 transform_policy n' policy (insert … pclength acc)1742  Some x ⇒ let 〈pc,addr,length〉 ≝ x in 1743 transform_policy n' policy (insert … (bitvector_of_nat 16 pc) length acc) 1445 1744 ] 1446 1745 ]. … … 1453 1752 let policy ≝ 1454 1753 transform_policy (\snd program) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in 1455 (* here we must use jump_length_ok *) 1456 bvt_lookup ? ? pc policy long_jump. 1457 /2 by Stub, mk_Sig/ 1458 qed. 1754 «bvt_lookup ? ? pc policy long_jump,?». 1755 cases daemon (* XXX later *) 1756 qed.
Note: See TracChangeset
for help on using the changeset viewer.