 Timestamp:
 Jun 8, 2012, 5:16:22 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2032 r2034 1 include "ASM/ASM.ma". 2 include "ASM/Arithmetic.ma". 3 include "ASM/Fetch.ma". 4 include "ASM/Status.ma". 5 include "utilities/extralib.ma". 6 include "ASM/Assembly.ma". 1 include "ASM/PolicyStep.ma". 7 2 8 3 include alias "basics/lists/list.ma". … … 10 5 include alias "basics/logic.ma". 11 6 12 (* Internal types *)13 14 (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *)15 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16).16 17 (* The different properties that we want/need to prove at some point *)18 (* Anything that's not in the program doesn't end up in the policy *)19 definition out_of_program_none: list labelled_instruction → ppc_pc_map → Prop ≝20 λprefix.λsigma.21 ∀i:ℕ.i > prefix → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?.22 23 (* If instruction i is a jump, then there will be something in the policy at24 * position i *)25 definition is_jump' ≝26 λx:preinstruction Identifier.27 match x with28 [ JC _ ⇒ True29  JNC _ ⇒ True30  JZ _ ⇒ True31  JNZ _ ⇒ True32  JB _ _ ⇒ True33  JNB _ _ ⇒ True34  JBC _ _ ⇒ True35  CJNE _ _ ⇒ True36  DJNZ _ _ ⇒ True37  _ ⇒ False38 ].39 40 definition is_jump ≝41 λinstr:pseudo_instruction.42 match instr with43 [ Instruction i ⇒ is_jump' i44  Call _ ⇒ True45  Jmp _ ⇒ True46  _ ⇒ False47 ].48 49 definition is_jump_to ≝50 λx:pseudo_instruction.λd:Identifier.51 match x with52 [ Instruction i ⇒ match i with53 [ JC j ⇒ d = j54  JNC j ⇒ d = j55  JZ j ⇒ d = j56  JNZ j ⇒ d = j57  JB _ j ⇒ d = j58  JNB _ j ⇒ d = j59  CJNE _ j ⇒ d = j60  DJNZ _ j ⇒ d = j61  _ ⇒ False62 ]63  Call c ⇒ d = c64  Jmp j ⇒ d = j65  _ ⇒ False66 ].67 68 definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝69 λprefix.λsigma.70 ∀i:ℕ.i < prefix →71 ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) →72 \snd (bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd sigma) 〈0,short_jump〉) = short_jump.73 74 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)75 (* definition labels_okay: label_map → ppc_pc_map → Prop ≝76 λlabels.λsigma.77 bvt_forall ?? (\snd sigma) (λn.λx.78 let 〈pc,addr_nat〉 ≝ x in79 ∃id:Identifier.lookup_def … labels id 0 = addr_nat80 ). *)81 82 (* Between two policies, jumps cannot decrease *)83 definition jmpeqb: jump_length → jump_length → bool ≝84 λj1.λj2.85 match j1 with86 [ short_jump ⇒ match j2 with [ short_jump ⇒ true  _ ⇒ false ]87  medium_jump ⇒ match j2 with [ medium_jump ⇒ true  _ ⇒ false ]88  long_jump ⇒ match j2 with [ long_jump ⇒ true  _ ⇒ false ]89 ].90 91 lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2.92 #j1 #j2 cases j1 cases j293 [1,5,9: / by /]94 #H cases H95 qed.96 97 definition jmple: jump_length → jump_length → Prop ≝98 λj1.λj2.99 match j1 with100 [ short_jump ⇒101 match j2 with102 [ short_jump ⇒ False103  _ ⇒ True104 ]105  medium_jump ⇒106 match j2 with107 [ long_jump ⇒ True108  _ ⇒ False109 ]110  long_jump ⇒ False111 ].112 113 definition jmpleq: jump_length → jump_length → Prop ≝114 λj1.λj2.jmple j1 j2 ∨ j1 = j2.115 116 definition policy_increase: list labelled_instruction → ppc_pc_map →117 ppc_pc_map → Prop ≝118 λprogram.λop.λp.119 ∀i.i < program →120 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd op) 〈0,short_jump〉 in121 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd p) 〈0,short_jump〉 in122 (*opc ≤ pc ∧*) jmpleq oj j.123 124 (* Policy safety *)125 (*definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝126 λprogram.λlabels.λsigma.127 ∀i.i < program →128 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,false〉 in129 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in130 ∀dest.is_jump_to instr dest →131 let paddr ≝ lookup_def … labels dest 0 in132 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,false〉) in133 match j with134 [ None ⇒ True135  Some j ⇒ match j with136 [ short_jump ⇒137 if leb pc addr138 then le (addr  pc) 126139 else le (pc  addr) 129140  medium_jump ⇒141 let a ≝ bitvector_of_nat 16 addr in142 let p ≝ bitvector_of_nat 16 pc in143 let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 a in144 let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 p in145 eq_bv 5 fst_5_addr fst_5_pc = true146  long_jump ⇒ True147 ]148 ].*)149 150 (* this is the instruction size as determined by the distance from origin to destination *)151 (*definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝152 λlabels.λsigma.λpc.λi.153 \fst (assembly_1_pseudoinstruction154 (λid.bitvector_of_nat 16 (lookup_def … labels id 0))155 (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0,false〉))) pc156 (λx.zero 16) i).*)157 158 (* this is the instruction size as determined by the jump length given *)159 definition expand_relative_jump_internal_unsafe:160 jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝161 λjmp_len:jump_length.λi.162 match jmp_len with163 [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ]164  medium_jump ⇒ [ ] (* this should not happen *)165  long_jump ⇒166 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));167 SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)168 LJMP (ADDR16 (zero 16))169 ]170 ].171 @I172 qed.173 174 definition expand_relative_jump_unsafe:175 jump_length → preinstruction Identifier → list instruction ≝176 λjmp_len:jump_length.λi.177 match i with178 [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)179  JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?)180  JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr)181  JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?)182  JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?)183  JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr)184  JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr)185  CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr)186  DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr)187  ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]188  ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]189  SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ]190  INC arg ⇒ [ INC ? arg ]191  DEC arg ⇒ [ DEC ? arg ]192  MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ]193  DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ]194  DA arg ⇒ [ DA ? arg ]195  ANL arg ⇒ [ ANL ? arg ]196  ORL arg ⇒ [ ORL ? arg ]197  XRL arg ⇒ [ XRL ? arg ]198  CLR arg ⇒ [ CLR ? arg ]199  CPL arg ⇒ [ CPL ? arg ]200  RL arg ⇒ [ RL ? arg ]201  RR arg ⇒ [ RR ? arg ]202  RLC arg ⇒ [ RLC ? arg ]203  RRC arg ⇒ [ RRC ? arg ]204  SWAP arg ⇒ [ SWAP ? arg ]205  MOV arg ⇒ [ MOV ? arg ]206  MOVX arg ⇒ [ MOVX ? arg ]207  SETB arg ⇒ [ SETB ? arg ]208  PUSH arg ⇒ [ PUSH ? arg ]209  POP arg ⇒ [ POP ? arg ]210  XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ]211  XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ]212  RET ⇒ [ RET ? ]213  RETI ⇒ [ RETI ? ]214  NOP ⇒ [ RealInstruction (NOP ?) ]215 ].216 217 definition instruction_size_jmplen:218 jump_length → pseudo_instruction → ℕ ≝219 λjmp_len.220 λi.221 let pseudos ≝ match i with222 [ Cost cost ⇒ [ ]223  Comment comment ⇒ [ ]224  Call call ⇒225 match jmp_len with226 [ short_jump ⇒ [ ] (* this should not happen *)227  medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]228  long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ]229 ]230  Mov d trgt ⇒231 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]232  Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr233  Jmp jmp ⇒234 match jmp_len with235 [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ]236  medium_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]237  long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ]238 ]239 ] in240 let mapped ≝ map ? ? assembly1 pseudos in241 let flattened ≝ flatten ? mapped in242 let pc_len ≝ length ? flattened in243 pc_len.244 @I.245 qed.246 247 definition policy_compact_unsafe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝248 λprogram.λlabels.λsigma.249 ∀n:ℕ.n < program →250 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with251 [ None ⇒ False252  Some x ⇒ let 〈pc,j〉 ≝ x in253 match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with254 [ None ⇒ False255  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in256 pc1 = pc + instruction_size_jmplen j (\snd (nth n ? program 〈None ?, Comment []〉))257 ]258 ].259 260 (* new safety condition: policy corresponds to program and resulting program is compact *)261 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝262 λprogram.λlabels.λsigma.263 ∀n:ℕ.n < program →264 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with265 [ None ⇒ False266  Some x ⇒ let 〈pc,j〉 ≝ x in267 match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with268 [ None ⇒ False269  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in270 pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))271 (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))272 (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))273 (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉))274 ]275 ].276 277 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *)278 definition max_length: jump_length → jump_length → jump_length ≝279 λj1.λj2.280 match j1 with281 [ long_jump ⇒ long_jump282  medium_jump ⇒283 match j2 with284 [ medium_jump ⇒ medium_jump285  _ ⇒ long_jump286 ]287  short_jump ⇒288 match j2 with289 [ short_jump ⇒ short_jump290  _ ⇒ long_jump291 ]292 ].293 294 lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)).295 #x #y cases x cases y /3 by inl, inr, nmk, I/296 qed.297 298 lemma jmpleq_max_length: ∀ol,nl.299 jmpleq ol (max_length ol nl).300 #ol #nl cases ol cases nl301 /2 by or_introl, or_intror, I/302 qed.303 304 lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b).305 #a #b cases a cases b /2/306 %2 @nmk #H destruct (H)307 qed.308 309 (* definition policy_isize_sum ≝310 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.311 (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction)312 (λacc.ℕ)313 prefix314 (λhd.λx.λtl.λp.λacc.315 acc + (instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))316 (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))317 (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))318 (bitvector_of_nat 16 (\fst sigma)) (\snd x)))319 0. *)320 321 (* The function that creates the labeltoaddress map *)322 definition create_label_map: ∀program:list labelled_instruction.323 (Σlabels:label_map.324 ∀l.occurs_exactly_once ?? l program →325 bitvector_of_nat ? (lookup_def ?? labels l 0) =326 address_of_word_labels_code_mem program l327 ) ≝328 λprogram.329 \fst (create_label_cost_map program).330 #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim331 #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map;332 normalize nodelta >EQ @(H l Hl)333 qed.334 335 definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →336 Identifier → jump_length ≝337 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.338 let paddr ≝ lookup_def … labels lbl 0 in339 if leb ppc paddr (* forward jump *)340 then341 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)342 + added in343 if leb (addr  \fst inc_sigma) 129344 then short_jump345 else long_jump346 else347 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in348 if leb (\fst inc_sigma  addr) 125349 then short_jump350 else long_jump.351 352 definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →353 Identifier → jump_length ≝354 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.355 let paddr ≝ lookup_def ? ? labels lbl 0 in356 let addr ≝357 if leb ppc paddr (* forward jump *)358 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)359 + added360 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in361 let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? addr) in362 let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in363 if eq_bv ? fst_5_addr fst_5_pc364 then medium_jump365 else long_jump.366 367 definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →368 Identifier → jump_length ≝369 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.370 let paddr ≝ lookup_def … labels lbl 0 in371 if leb ppc paddr (* forward jump *)372 then373 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)374 + added in375 if leb (addr  \fst inc_sigma) 126376 then short_jump377 else select_call_length labels old_sigma inc_sigma added ppc lbl378 else379 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in380 if leb (\fst inc_sigma  addr) 129381 then short_jump382 else select_call_length labels old_sigma inc_sigma added ppc lbl.383 384 definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map →385 ℕ → ℕ → preinstruction Identifier → option jump_length ≝386 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.387 match i with388 [ JC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)389  JNC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)390  JZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)391  JNZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)392  JB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)393  JBC _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)394  JNB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)395  CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)396  DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)397  _ ⇒ None ?398 ].399 400 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x).401 #i cases i402 [#id cases id403 [1,2,3,6,7,33,34:404 #x #y %2 whd in match (is_jump ?); /2 by nmk/405 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:406 #x %2 whd in match (is_jump ?); /2 by nmk/407 35,36,37: %2 whd in match (is_jump ?); /2 by nmk/408 9,10,14,15: #x %1 / by I/409 11,12,13,16,17: #x #y %1 / by I/410 ]411 2,3: #x %2 /2 by nmk/412 4,5: #x %1 / by I/413 6: #x #y %2 /2 by nmk/414 ]415 qed.416 417 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.418 #a #b / by refl/419 qed.420 421 lemma nth_last: ∀A,a,l.422 nth (l) A l a = a.423 #A #a #l elim l424 [ / by /425  #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind426 ]427 qed.428 429 (* The first step of the jump expansion: everything to short. *)430 definition jump_expansion_start:431 ∀program:(Σl:list labelled_instruction.S (l) < 2^16).432 ∀labels:label_map.433 Σpolicy:option ppc_pc_map.434 match policy with435 [ None ⇒ True436  Some p ⇒437 And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p)438 (jump_not_in_policy (pi1 ?? program) p))439 (policy_compact_unsafe program labels p))440 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉))441 (∀i.i ≤ program → ∃pc.442 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))443 (bvt_lookup_opt … (bitvector_of_nat ? (program)) (\snd p) =444 Some ? 〈\fst p,short_jump〉))445 (\fst p < 2^16)446 ] ≝447 λprogram.λlabels.448 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)449 (λprefix.Σpolicy:ppc_pc_map.450 And (And (And (And (And (out_of_program_none prefix policy)451 (jump_not_in_policy prefix policy))452 (policy_compact_unsafe prefix labels policy))453 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))454 (∀i.i ≤ prefix → ∃pc.455 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))456 (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd policy) =457 Some ? 〈\fst policy,short_jump〉))458 program459 (λprefix.λx.λtl.λprf.λp.460 let 〈pc,sigma〉 ≝ pi1 ?? p in461 let 〈label,instr〉 ≝ x in462 let isize ≝ instruction_size_jmplen short_jump instr in463 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (prefix))) 〈pc+isize,short_jump〉 sigma〉464 ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in465 if geb (\fst (pi1 ?? final_policy)) 2^16 then466 None ?467 else468 Some ? (pi1 ?? final_policy).469 [ / by I/470  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg471 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]472  @conj [ @conj [ @conj [ @conj [ @conj473 [ (* out_of_program_none *)474 #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2475 cases (le_to_or_lt_eq … Hi) Hi #Hi476 cases p p #p cases p p #pc #p #Hp cases x x #l #pi477 [ >lookup_opt_insert_miss478 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i ? Hi2)479 @le_S_to_le @le_S_to_le @Hi480  @bitvector_of_nat_abs481 [ @Hi2482  @(transitive_lt … Hi2) @le_S_to_le @Hi483  @sym_neq @lt_to_not_eq @le_S_to_le @Hi484 ]485 ]486  >lookup_opt_insert_miss487 [ <Hi @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (prefix))) ?)488 [ @le_S @le_n489  >Hi @Hi2490 ]491  @bitvector_of_nat_abs492 [ @Hi2493  @(transitive_lt … Hi2) <Hi @le_n494  @sym_neq @lt_to_not_eq <Hi @le_n495 ]496 ]497 ]498  (* jump_not_in_policy *) cases p p #p cases p p #pc #sigma #Hp499 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi500 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi501 [ >lookup_insert_miss502 [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i ?)503 [ @Hi504  >nth_append_first505 [ #H #H2 @H @H2506  @Hi507 ]508 ]509  @bitvector_of_nat_abs510 [ @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <commutative_plus @le_S511 @le_plus_a @Hi512  @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S513 @le_plus_n_r514  @lt_to_not_eq @le_S_S @Hi515 ]516 ]517  >Hi >lookup_insert_hit #_ @refl518 ]519 ]520  (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;521 cases p p #p cases p p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta522 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi523 [ >lookup_opt_insert_miss524 [ >lookup_opt_insert_miss525 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)526 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))527 cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);528 [ #_ normalize nodelta / by /529  #x cases x x #pci #ji #EQi530 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma))531 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %);532 [ #_ normalize nodelta / by /533  #x cases x x #pcSi #jSi #EQSi normalize nodelta >nth_append_first534 [ / by /535  @Hi536 ]537 ]538 ]539 ]540 ]541 [2: lapply (le_S_to_le … Hi) Hi #Hi]542 @bitvector_of_nat_abs543 [1,4: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <commutative_plus544 @le_plus_a @Hi545 2,5: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm546 @le_S_S @le_plus_n_r547 3,6: @lt_to_not_eq @le_S_S @Hi548 ]549  >lookup_opt_insert_miss550 [ >Hi >lookup_opt_insert_hit normalize nodelta551 >(proj2 ?? Hp) normalize nodelta >nth_append_second552 [ <minus_n_n whd in match (nth ????); @refl553  @le_n554 ]555  @bitvector_of_nat_abs556 [ @(transitive_lt … (pi2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus557 @le_plus_a @le_n558  @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm559 @le_S_S @le_plus_n_r560  @lt_to_not_eq @le_S_S >Hi @le_n561 ]562 ]563 ]564 ]565  (* lookup 0 = 0 *)566 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta567 >lookup_opt_insert_miss568 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hp)))569  @bitvector_of_nat_abs570 [ / by /571  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm572 @le_S_S @le_plus_n_r573  @lt_to_not_eq / by /574 ]575 ]576 ]577  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;578 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta579 cases (le_to_or_lt_eq … Hi) Hi #Hi580 [ >lookup_opt_insert_miss581 [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi))582  @bitvector_of_nat_abs583 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus584 @le_plus_a @le_S_S_to_le @Hi585  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S586 @le_S_S @le_plus_n_r587  @lt_to_not_eq @Hi588 ]589 ]590  >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr))591 @refl592 ]593 ]594  (* lookup at the end *) cases p p #p cases p p #pc #sigma #Hp cases x595 #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit596 / by refl/597 ]598  @conj [ @conj [ @conj [ @conj [ @conj599 [ #i cases i600 [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /601  i #i #Hi #Hi2 >lookup_opt_insert_miss602 [ / by refl/603  @bitvector_of_nat_abs604 [ @Hi2605  / by /606  @sym_neq @lt_to_not_eq / by /607 ]608 ]609 ]610  #i cases i611 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O612  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O613 ]614 ]615  #i cases i616 [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n617  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O618 ]619 ]620  >lookup_opt_insert_hit @refl621 ]622  #i cases i623 [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl624  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O625 ]626 ]627  >lookup_opt_insert_hit @refl628 ]629 ]630 qed.631 632 definition policy_equal ≝633 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.634 (* \fst p1 = \fst p2 ∧ *)635 (∀n:ℕ.n ≤ program →636 let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in637 let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in638 \snd pc1 = \snd pc2).639 640 definition nec_plus_ultra ≝641 λprogram:list labelled_instruction.λp:ppc_pc_map.642 ¬(∀i.i < program → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →643 \snd (bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd p) 〈0,short_jump〉) = long_jump).644 645 (*include alias "common/Identifiers.ma".*)646 include alias "ASM/BitVector.ma".647 include alias "basics/lists/list.ma".648 include alias "arithmetics/nat.ma".649 include alias "basics/logic.ma".650 651 lemma blerpque: ∀a,b,i.652 is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →653 (max_length a b) = a.654 #a #b #i cases i655 [1: #pi cases pi656 [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:657 try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H658 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %)659 try (#abs normalize in abs; destruct (abs) @I)660 cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I)661 try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I)662 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w663 try ( #abs normalize in abs; destruct (abs) @I)664 @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs)665 ]666 2,3,6: #x [3: #y] #H cases H667 4,5: #id #_ cases a cases b668 [2,3,4,6,11,12,13,15: normalize #H destruct (H)669 1,5,7,8,9,10,14,16,17,18: #H / by refl/670 ]671 ]672 qed.673 674 lemma etblorp: ∀a,b,i.is_jump i →675 instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.676 #a #b #i cases i677 [2,3,6: #x [3: #y] #H cases H678 4,5: #id #_ cases a cases b / by le_n/679 1: #pi cases pi680 [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:681 [1,2,3,6,7,24,25: #x #y682 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]683 #H cases H684 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]685 #_ cases a cases b686 [2,3: cases x #ad cases ad687 [15,34: #b #Hb / by le_n/688 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb689 1,4,5,6,7,8,9: / by le_n/690 11,12: cases x #ad cases ad691 [15,34: #b #Hb / by le_n/692 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb693 10,13,14,15,16,17,18: / by le_n/694 20,21: cases x #ad cases ad695 [15,34: #b #Hb / by le_n/696 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb697 19,22,23,24,25,26,27: / by le_n/698 29,30: cases x #ad cases ad #a1 #a2699 [1,3: cases a2 #ad2 cases ad2700 [1,8,20,27: #b #Hb / by le_n/701 2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb702 2,4: cases a1 #ad1 cases ad1703 [2,4,21,23: #b #Hb / by le_n/704 1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb705 ]706 28,31,32,33,34,35,36: / by le_n/707 38,39: cases x #ad cases ad708 [1,4,20,23: #b #Hb / by le_n/709 2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb710 37,40,41,42,43,44,45: / by le_n/711 46,47,48,49,50,51,52,53,54: / by le_n/712 55,56,57,58,59,60,61,62,63: / by le_n/713 64,65,66,67,68,69,70,71,72: / by le_n/714 73,74,75,76,77,78,79,80,81: / by le_n/715 ]716 ]717 ]718 qed.719 720 lemma minus_zero_to_le: ∀n,m:ℕ.n  m = 0 → n ≤ m.721 #n722 elim n723 [ #m #_ @le_O_n724  #n' #Hind #m cases m725 [ #H n whd in match (minus ??) in H; >H @le_n726  #m' m #H whd in match (minus ??) in H; @le_S_S @Hind @H727 ]728 ]729 qed.730 731 lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.732 #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r733 qed.734 735 (* One step in the search for a jump expansion fixpoint. *)736 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (l) < 2^16).737 ∀labels:(Σlm:label_map.∀l.738 occurs_exactly_once ?? l program →739 bitvector_of_nat ? (lookup_def … lm l 0) =740 address_of_word_labels_code_mem program l).741 ∀old_policy:(Σpolicy:ppc_pc_map.742 And (And (And (out_of_program_none program policy)743 (jump_not_in_policy program policy))744 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))745 (\fst policy < 2^16)).746 (Σx:bool × (option ppc_pc_map).747 let 〈no_ch,y〉 ≝ x in748 match y with749 [ None ⇒ nec_plus_ultra program old_policy750  Some p ⇒ And (And (And (And (And (And (out_of_program_none program p)751 (jump_not_in_policy program p))752 (policy_increase program old_policy p))753 (policy_compact program labels p))754 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉))755 (no_ch = true → policy_equal program old_policy p))756 (\fst p < 2^16)757 ])758 ≝759 λprogram.λlabels.λold_sigma.760 let 〈final_added, final_policy〉 ≝761 pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)762 (λprefix.Σx:ℕ × ppc_pc_map.763 let 〈added,policy〉 ≝ x in764 And (And (And (And (And (out_of_program_none prefix policy)765 (jump_not_in_policy prefix policy))766 (policy_increase prefix old_sigma policy))767 (policy_compact_unsafe prefix labels policy))768 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))769 (added = 0 → policy_equal prefix old_sigma policy))770 program771 (λprefix.λx.λtl.λprf.λacc.772 let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in773 let 〈label,instr〉 ≝ x in774 (* Now, we must add the current ppc and its pc translation.775 * Three possibilities:776 *  Instruction is not a jump; i.e. constant size whatever the sigma we use;777 *  Instruction is a backward jump; we can use the sigma we're constructing,778 * since it will already know the translation of its destination;779 *  Instruction is a forward jump; we must use the old sigma (the new sigma780 * does not know the translation yet), but compensate for the jumps we781 * have lengthened.782 *)783 let add_instr ≝ match instr with784 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j)785  Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c)786  Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (prefix) i787  _ ⇒ None ?788 ] in789 let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in790 let 〈old_pc,old_length〉 ≝791 bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉 in792 let old_size ≝ instruction_size_jmplen old_length instr in793 let 〈new_length, isize〉 ≝ match add_instr with794 [ None ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉795  Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉796 ] in797 let new_added ≝ match add_instr with798 [ None ⇒ inc_added799  Some x ⇒ plus inc_added (minus isize old_size)800 ] in801 〈new_added, 〈plus inc_pc isize,802 bvt_insert … (bitvector_of_nat ? (S (prefix))) 〈inc_pc+isize, new_length〉 inc_sigma〉〉803 ) 〈0, 〈0, bvt_insert … (bitvector_of_nat 16 0) 〈0, short_jump〉 (Stub ??)〉〉) in804 if geb (\fst final_policy) 2^16 then805 〈eqb final_added 0, None ?〉806 else807 〈eqb final_added 0, Some ? final_policy〉.808 [ normalize nodelta cases daemon (* XXX nec_plus_ultra *)809  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2810 >H2 in H; normalize nodelta H2 x #H @conj811 [ @conj812 [ @conj813 [ @conj814 [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))815  cases daemon (* XXX policy_compact_unsafe → policy_compact *)816 ]817  @(proj2 ?? (proj1 ?? H))818 ]819  #H2 @(proj2 ?? H) @eqb_true_to_eq @H2820 ]821  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1822 ]823 4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma824 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))825 cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);826 #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta827 @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2828 @conj [ @conj [ @conj [ @conj [ @conj829 [ (* out_of_program_none *) #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2830 cases instr in Heq2; normalize nodelta831 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss832 [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ? Hi2)833 @le_S_to_le @Hi834 2,4,6,8,10,12: @bitvector_of_nat_abs835 [1,4,7,10,13,16: @Hi2836 2,5,8,11,14,17: @(transitive_lt … Hi2) @Hi837 3,6,9,12,15,18: @sym_neq @lt_to_not_eq @Hi838 ]839 ]840  (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi;841 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi842 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss843 [ >(nth_append_first ? i prefix ?? Hi)844 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i Hi)845  @bitvector_of_nat_abs846 [ @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length >commutative_plus847 @le_plus_a @Hi848  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm849 @le_plus_n_r850  @lt_to_not_eq @le_S_S @Hi851 ]852 ]853  <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit854 cases instr in Heq1;855 [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl856 4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second857 [1,3: <minus_n_n whd in match (nth ????); / by I/858 2,4: @le_n859 ]860 1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi861 [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:862 [1,2,3,6,7,24,25: #x #y863 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1864 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl865 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta866 #_ #H @⊥ cases H #H2 @H2 / by I/867 ]868 ]869 ]870 ]871  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;872 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi; #Hi873 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)874 <(proj2 ?? (pair_destruct ?????? Heq2))875 @pair_elim #opc #oj #EQ1 >lookup_insert_miss876 [ @pair_elim #pc #j #EQ2 / by /877  @bitvector_of_nat_abs878 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus879 @le_plus_a @Hi880  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r881  @lt_to_not_eq @le_S_S @Hi882 ]883 ]884  >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit885 cases (dec_is_jump instr)886 [ cases instr in Heq1; normalize nodelta887 [ #pi cases pi888 [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:889 [1,2,3,6,7,24,25: #x #y890 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj891 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]892 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1893 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta894 @jmpleq_max_length895 ]896 2,3,6: #x [3: #y] #_ #Hj cases Hj897 4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta898 @jmpleq_max_length899 ]900  lapply Heq1 Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta901 [ #pi cases pi902 [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:903 [1,2,3,6,7,24,25: #x #y904 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]905 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1906 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))907 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??)908 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:909 >prf >nth_append_second910 [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:911 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj912 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:913 @le_n914 ]915 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:916 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r917 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:918 cases (lookup ?? (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)919 #a #b #H >H normalize nodelta %2 @refl920 ]921 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]922 #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/923 ]924 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))925 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??)926 [1,4,7: >prf >nth_append_second927 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj928 2,4,6: @le_n929 ]930 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r931 3,6,9: cases (lookup ?? (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)932 #a #b #H >H normalize nodelta %2 @refl933 ]934 4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/935 ]936 ]937 ]938 ]939  (* policy_compact_unsafe *) (*XXX*) cases daemon940 ]941  (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_opt_insert_miss942 [ @(proj2 ?? (proj1 ?? Hpolicy))943  @bitvector_of_nat_abs944 [ / by /945  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm946 @le_S_S @le_plus_n_r947  @lt_to_not_eq / by /948 ]949 ]950 ]951  (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy)952 lapply Heq2 Heq2 lapply Heq1 Heq1 lapply (refl ? instr)953 cases instr in ⊢ (???% → % → % → %); normalize nodelta954 [ #pi cases pi normalize nodelta955 [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:956 [1,2,3,6,7,24,25: #x #y957 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]958 #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded959 #i >append_length >commutative_plus #Hi normalize in Hi;960 cases (le_to_or_lt_eq … Hi) Hi #Hi961 [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:962 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss963 [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:964 @(Hold Hadded i (le_S_S_to_le … Hi))965 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:966 @bitvector_of_nat_abs967 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:968 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus969 @le_S_S @le_plus_a @le_S_S_to_le @Hi970 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:971 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_S_S972 @le_plus_n_r973 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:974 @lt_to_not_eq @Hi975 ]976 ]977 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:978 <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit979 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??)980 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:981 >prf >nth_append_second982 [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:983 <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H984 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:985 @le_n986 ]987 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:988 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r989 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:990 cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)991 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl992 ]993 ]994 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold995 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))996 #H #i >append_length >commutative_plus #Hi normalize in Hi;997 cases (le_to_or_lt_eq … Hi) Hi #Hi998 [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))999 >lookup_insert_miss1000 [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_S_to_le … Hi))1001 [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]1002 ]1003 @bitvector_of_nat_abs1004 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf1005 >append_length >commutative_plus @le_S_S @le_plus_a @le_S_S_to_le @Hi1006 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf1007 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r1008 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi1009 ]1010 2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi1011 >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))1012 >Holdeq normalize nodelta @sym_eq @blerpque1013 [3,6,9,12,15,18,21,24,27:1014 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))1015 [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp1016 2,4,6,8,10,12,14,16,18: #H @H1017 ]1018 / by I/1019 2,5,8,11,14,17,20,23,26: / by I/1020 ]1021 ]1022 ]1023 2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))1024 #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;1025 cases (le_to_or_lt_eq …Hi) Hi #Hi1026 [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss1027 [1,3,5: @(Hold Hadded i (le_S_S_to_le … Hi))1028 2,4,6: @bitvector_of_nat_abs1029 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus1030 @le_S_S @le_plus_a @le_S_S_to_le @Hi1031 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm1032 @le_S_S @le_plus_n_r1033 3,6,9: @lt_to_not_eq @Hi1034 ]1035 ]1036 2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit1037 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??)1038 [1,4,7: >prf >nth_append_second1039 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H1040 2,4,6: @le_n1041 ]1042 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r1043 3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)1044 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl1045 ]1046 ]1047 4,5: #x #Hins #Heq1 #Heq2 #Hold1048 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))1049 #H #i >append_length >commutative_plus #Hi normalize in Hi;1050 cases (le_to_or_lt_eq … Hi) Hi #Hi1051 [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss1052 [1,3: @(Hold ? i (le_S_S_to_le … Hi))1053 [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]1054 ]1055 @bitvector_of_nat_abs1056 [1,4: @(transitive_lt … (pi2 ?? program)) >prf1057 >append_length >commutative_plus @le_S_S @le_plus_a @le_S_S_to_le @Hi1058 2,5: @(transitive_lt … (pi2 ?? program)) >prf1059 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r1060 3,6: @lt_to_not_eq @Hi1061 ]1062 2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit1063 <(proj1 ?? (pair_destruct ?????? Heq1))>Holdeq normalize nodelta1064 @sym_eq @blerpque1065 [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))1066 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp1067 2,4: #H @H1068 ]1069 / by I/1070 2,5: / by I/1071 ]1072 ]1073 ]1074 ]1075  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj1076 [ #i cases i1077 [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /1078  i #i #Hi #Hi2 >lookup_opt_insert_miss1079 [ / by refl/1080  @bitvector_of_nat_abs1081 [ @Hi21082  / by /1083  @sym_neq @lt_to_not_eq / by /1084 ]1085 ]1086 ]1087  #i cases i1088 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O1089  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O1090 ]1091 ]1092  #i cases i1093 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O1094  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O1095 ]1096 ]1097  #i cases i1098 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O1099  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O1100 ]1101 ]1102  >lookup_opt_insert_hit @refl1103 ]1104  #_ #i cases i1105 [ #Hi >lookup_insert_hit1106 >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? (pi2 ?? old_sigma))) 〈0,short_jump〉)1107 @refl1108  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O1109 ]1110 ]1111 ]1112 qed.1113 1114 7 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (l)) 2^16) (n: ℕ) 1115 8 on n:(Σx:bool × (option ppc_pc_map). 1116 9 let 〈c,pol〉 ≝ x in 1117 match pol with 10 And 11 (match pol with 1118 12 [ None ⇒ True 1119 13  Some x ⇒ … … 1122 16 (jump_not_in_policy program x)) 1123 17 (n > 0 → policy_compact program (create_label_map program) x)) 1124 ( bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd x) = Some ? 〈0,short_jump〉))18 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0)) 1125 19 (\fst x < 2^16) 1126 ]) ≝20 ]) (n = 0 → c = true)) ≝ 1127 21 let labels ≝ create_label_map program in 1128 match n with1129 [ O ⇒ 〈true,pi1 ?? (jump_expansion_start program labels)〉1130  S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in22 match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with 23 [ O ⇒ λp.〈true,pi1 ?? (jump_expansion_start program labels)〉 24  S m ⇒ λp.let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 1131 25 match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with 1132 26 [ None ⇒ λp2.〈false,None ?〉 1133 27  Some op ⇒ λp2.if ch 1134 28 then pi1 ?? (jump_expansion_step program labels «op,?») 1135 else (jump_expansion_internal program m)29 else pi1 ?? (jump_expansion_internal program m) 1136 30 ] (refl … z) 1137 ] .31 ] (refl … n). 1138 32 [ normalize nodelta cases (jump_expansion_start program (create_label_map program)) 1139 #x cases x x 1140 [ / by I/1141  #sigma normalize nodelta #H @conj [ @conj [ @conj 33 #x cases x x 34 [ #H @conj / by I/ 35  #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj 1142 36 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1143  #H @⊥ @(absurd ? H) @le_to_not_lt @le_n37  >p #H @⊥ @(absurd ? H) @le_to_not_lt @le_n 1144 38 ] 1145 39  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 1146 40 ] 1147  @(proj2 ?? H) ] 1148 ] 1149  cases daemon 1150  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 1151  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta 1152 #H @conj [ @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))  @(proj2 ?? (proj1 ?? H)) ]  @(proj2 ?? H) ] 1153  normalize nodelta cases (jump_expansion_step program labels «op,?») 41  @(proj2 ?? H) 42 ] 43  / by / 44 ] 45 ] 46  normalize nodelta @conj [ / by I/  >p #H destruct (H) ] 47  cases ch in p1; #p1 48 [ normalize nodelta 49 cases (jump_expansion_step program (create_label_map program) «op,?») 50 #x cases x x #ch2 #z2 cases z2 normalize nodelta 51 [ #_ @conj [ / by I/  >p #H2 destruct (H2) ] 52  #j2 #H2 @conj [ @conj [ @conj [ @conj 53 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))) 54  #_ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))) 55 ] 56  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) 57 ] 58  @(proj2 ?? H2) 59 ] 60  >p #H3 destruct (H3) 61 ] 62 ] 63  normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m)) 64 <p1 >p2 normalize nodelta #H @conj [ @conj [ @conj [ @conj 65 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 66  >p #Hm cases (le_to_or_lt_eq … Hm) Hm #Hm 67 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @(le_S_S_to_le … Hm) 68  lapply ((proj2 ?? H) (sym_eq … (injective_S … Hm))) #H2 destruct (H2) 69 ] 70 ] 71  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 72 ] 73  @(proj2 ?? (proj1 ?? H)) 74 ] 75  >p #H2 destruct (H2) 76 ] 77 ] 78  cases (jump_expansion_internal program m) in p1; 1154 79 #p cases p p #p #r cases r normalize nodelta 1155 [ #H / by I/ 1156  #j #H @conj 1157 [ @conj 1158 [ @conj 1159 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1160  cases daemon 1161 ] 1162  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 1163 ] 1164  @(proj2 ?? H) 80 [ #_ >p2 #ABS destruct (ABS) 81  #map >p2 normalize nodelta 82 #H #eq destruct (eq) @conj [ @conj 83 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 84  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 85 ] 86  @(proj2 ?? (proj1 ?? H)) 1165 87 ] 1166 88 ] … … 1242 164 #x1 cases x1 #p1 #j1 x1; #H1 #Heqj #Hj #k elim k 1243 165 [ <plus_n_O >Heqj @Hj 1244  #k' k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k')));166  #k' k <plus_n_Sm (*whd in match (jump_expansion_internal program (S (n+k')));*) 1245 167 lapply (refl ? (jump_expansion_internal program (n+k'))) 1246 cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);168 cases (jump_expansion_internal program (n+k')) in ⊢ (???% → %); 1247 169 #x2 cases x2 x2 #c2 #p2 normalize nodelta #H #Heqj2 1248 170 cases p2 in H Heqj2; … … 1288 210 match program with 1289 211 [ nil ⇒ acc 1290  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? ( S (t))) (\snd policy) 〈0,short_jump〉)) with212  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) with 1291 213 [ long_jump ⇒ measure_int t policy (acc + 2) 1292 214  medium_jump ⇒ measure_int t policy (acc + 1) … … 1302 224 [ / by refl/ 1303 225  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1304 cases (\snd (bvt_lookup … (bitvector_of_nat ? ( S (t))) (\snd policy) 〈0,short_jump〉))226 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) 1305 227 [ normalize nodelta @Hd 1306 228 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus … … 1316 238 [ normalize @le_n 1317 239  #h #t #Hind whd in match (measure_int ???); 1318 cases (\snd (lookup ?? (bitvector_of_nat ? ( S (t))) (\snd policy) 〈0,short_jump〉))240 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) 1319 241 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1320 242 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) … … 1329 251 out_of_program_none program p ∧ 1330 252 jump_not_in_policy program p ∧ 1331 lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉∧253 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 1332 254 \fst p < 2^16. 1333 255 ∀l.l ≤ program → ∀acc:ℕ. … … 1343 265 [ / by I/ 1344 266  #x normalize nodelta #Hx #Hjeq 1345 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (t) Hp)267 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))))) (t) Hp) 1346 268 whd in match (measure_int ???); whd in match (measure_int ? x ?); 1347 cases (bvt_lookup ?? (bitvector_of_nat ? ( S (t))) (\snd (pi1 ?? policy)) 〈0,short_jump〉)1348 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? ( S (t))) (\snd x) 〈0,short_jump〉)269 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd (pi1 ?? policy)) 〈0,short_jump〉) 270 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,short_jump〉) 1349 271 #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2 1350 272 [1,4,5,7,8,9: #H cases H … … 1380 302 measure_int program policy 0 = 2*program → ∀i.i<program → 1381 303 is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) → 1382 (\snd (bvt_lookup ?? (bitvector_of_nat ? (S i)) (\snd policy) 〈0,short_jump〉)) = long_jump.304 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump. 1383 305 #program #policy elim program in ⊢ (% → ∀i.% → ? → %); 1384 306 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 1387 309 [ #Hi @Hind 1388 310 [ whd in match (measure_int ???) in Hm; 1389 cases (\snd (bvt_lookup … (bitvector_of_nat ? ( S (t))) (\snd policy) 〈0,short_jump〉)) in Hm;311 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) in Hm; 1390 312 normalize nodelta 1391 313 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ … … 1398 320 ] 1399 321  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1400 cases (\snd (bvt_lookup … (bitvector_of_nat ? ( S (t))) (\snd policy) 〈0,short_jump〉)) in Hm;322 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) in Hm; 1401 323 normalize nodelta 1402 324 [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/ … … 1413 335 ∀policy:Σp:ppc_pc_map. 1414 336 out_of_program_none program p ∧ jump_not_in_policy program p ∧ 1415 bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉∧337 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 1416 338 \fst p < 2^16. 1417 339 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with … … 1426 348 measure_int x policy 0 = measure_int x p 0 → 1427 349 policy_equal x policy p) ?? (pi1 ?? program)) 1428 [ #_ #_ #i #Hi <(le_n_O_to_eq … Hi) 1429 >(lookup_opt_lookup_hit … 〈0,short_jump〉 (proj2 ?? (proj1 ?? (proj1 ?? Hpol)))) 1430 >(lookup_opt_lookup_hit … 〈0,short_jump〉 (proj2 ?? (proj1 ?? (pi2 ?? policy)))) 1431 / by refl/ 1432  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 1433 [ #Hi @Hind 350 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n 351  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 352 [ @Hind 1434 353 [ @(transitive_le … Hp) / by / 1435 354  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 1436 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) #Hinc1437 cases (bvt_lookup ?? (bitvector_of_nat ? ( S (t))) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x21438 cases (bvt_lookup ?? (bitvector_of_nat ? ( S (t))) ? 〈0,short_jump〉); #y1 #y2355 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (t) Hp) #Hinc 356 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2 357 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉); #y1 #y2 1439 358 #Hm #Hinc lapply Hm Hm; lapply Hinc Hinc; normalize nodelta 1440 359 cases x2 cases y2 normalize nodelta … … 1454 373 #_ #H @(injective_plus_r … H) 1455 374 ] 1456  @ (le_S_S_to_le … Hi)375  @Hi 1457 376 ] 1458  #Hi >Hi whd in match (measure_int ???) in Hm; 1459 whd in match (measure_int ? p ?) in Hm; 1460 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) 1461 cases (bvt_lookup ?? (bitvector_of_nat ? (S (t))) ? 〈0,short_jump〉) in Hm; 377  >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 378 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (t) Hp) 379 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm; 1462 380 #x1 #x2 1463 cases (bvt_lookup ?? (bitvector_of_nat ? (S (t))) ? 〈0,short_jump〉); 1464 #y1 #y2 381 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉); #y1 #y2 1465 382 normalize nodelta cases x2 cases y2 normalize nodelta 1466 383 [1,5,9: #_ #_ @refl … … 1506 423 [ / by refl/ 1507 424  #h #t #Hind #Hp whd in match (measure_int ???); 1508 elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) ( S (t)) Hp)425 elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) (t) (le_S_to_le … Hp)) 1509 426 #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind 1510 427 @(transitive_le … Hp) @le_n_Sn 1511 428 ] 1512 ] 429 ] 1513 430 qed. 1514 431 … … 1528 445 #c #pol #Hp cases pol 1529 446 [ normalize nodelta // 1530  #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))1531  #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? H))) cases (pi1 ?? program) in Hneq;447  #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 448  #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) cases (pi1 ?? program) in Hneq; 1532 449 [ #H cases H #H @⊥ @H @refl 1533 450  #h #t #_ / by / … … 1561 478 lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»)) 1562 479 [ @conj [ @conj 1563 [ @(proj1 ?? (proj1 ?? (proj1 ?? HFp))) 480 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) 481  @(proj2 ?? (proj1 ?? (proj1 ?? HFp))) ] 1564 482  @(proj2 ?? (proj1 ?? HFp)) ] 1565  @(proj2 ?? HFp) ]1566 483  lapply (measure_full program Fp ?) 1567 484 [ @le_to_le_to_eq 1568 485 [ @measure_le 1569 486  cut (∀x:ℕ.x ≤ 2*program → 1570 ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ 487 ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ 1571 488 x ≤ measure_int program p 0)) 1572 489 [ #x elim x … … 1601 518 #z cases z z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H; 1602 519 normalize nodelta #H @conj [ @conj 1603 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 520 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 521  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 1604 522  @(proj2 ?? (proj1 ?? H)) ] 1605  @(proj2 ?? H) ]1606 523  lapply (Hfa x (le_S_to_le … Hx)) lapply HeqSxpol HeqSxpol 1607 whd in match (jump_expansion_internal program (S x));1608 524 lapply (refl ? (jump_expansion_internal program x)) 1609 lapply Hxpol Hxpol cases (jump_expansion_internal program x) in ⊢ (% → ???% → %); 525 lapply Hxpol Hxpol 526 whd in match (jump_expansion_internal program (S x)); 527 cases (jump_expansion_internal program x) in ⊢ (% → ???% → %); 1610 528 #z cases z z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H; 1611 #H #Heq cases xch in Heq; #Heqnormalize nodelta529 #H #Heq2 cases xch in H Heq2; #H #Heq2 normalize nodelta 1612 530 [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 1613 531 [ @conj [ @conj 1614 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 532 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 533  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 1615 534  @(proj2 ?? (proj1 ?? H)) ] 1616  @(proj2 ?? H) ]1617 535  cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 1618 536 normalize nodelta cases c normalize nodelta … … 1621 539 [ / by / 1622 540  #H3 lapply (measure_special program «xpol,?») 1623 [ @conj [ @conj 1624 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 541 [ @conj [ @conj 542 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 543  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 1625 544  @(proj2 ?? (proj1 ?? H)) ] 1626  @(proj2 ?? H) ]1627 545  >Heq normalize nodelta #H4 @⊥ @(absurd … (H4 H3)) @Hfull 1628 546 ] … … 1632 550  lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 1633 551 [ @conj [ @conj 1634 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 552 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 553  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 1635 554  @(proj2 ?? (proj1 ?? H)) ] 1636  @(proj2 ?? H) ]1637 555  cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 1638 556 normalize nodelta cases c normalize nodelta … … 1654 572 [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull 1655 573  #Gp #HGp #EQ2 cases Fch 1656 [ normalize nodelta #i cases i 1657 [ #_ >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? HFp)) 〈0,short_jump〉) 1658 >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? (proj1 ?? HGp))) 〈0,short_jump〉) 1659 / by refl/ 1660  i #i #Hi 1661 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj 1662 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) 1663 lapply (Hfull i Hi Hj) 1664 cases (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd Fp) 〈0,short_jump〉) 1665 #fp #fj #Hfj >Hfj normalize nodelta 1666 cases (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd Gp) 〈0,short_jump〉) 1667 #gp #gj cases gj normalize nodelta 1668 [1,2: #H cases H #H2 cases H2 destruct (H2) 1669 3: #_ @refl 1670 ] 1671  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi Hj) 1672 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl 574 [ normalize nodelta #i #Hi 575 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj 576 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi) 577 lapply (Hfull i Hi Hj) 578 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 579 #fp #fj #Hfj >Hfj normalize nodelta 580 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Gp) 〈0,short_jump〉) 581 #gp #gj cases gj normalize nodelta 582 [1,2: #H cases H #H2 cases H2 destruct (H2) 583 3: #_ @refl 1673 584 ] 585  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i Hi Hj) 586 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl 1674 587 ] 1675 588  normalize nodelta /2 by pe_int_refl/ … … 1688 601 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); // 1689 602 #H destruct (H) 1690 4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m 1691 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 1692 #x1 #x2 1693 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 1694 #y1 #y2 normalize nodelta 1695 @dec_eq_jump_length 603 4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); cases program #p #_ cases p 604 [ %1 #m #Hm @⊥ @(absurd ? Hm) @le_to_not_lt @le_O_n 605  #h #t elim (dec_bounded_forall ?? (t)) 606 [1: #Hyp %1 #m #Hm @(Hyp m) @(le_S_S_to_le … Hm) 607 2: #Hyp %2 @nmk #H @(absurd ?? Hyp) #m #Hm @(H m) @(le_S_S … Hm) 608  #m cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 609 #x1 #x2 610 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 611 #y1 #y2 normalize nodelta 612 @dec_eq_jump_length 613 ] 614 615 ] 1696 616 ] 1697 617 ]
Note: See TracChangeset
for help on using the changeset viewer.