 Timestamp:
 May 9, 2012, 7:23:37 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1632 r1931 143 143  Stub _ ⇒ λ_.None ? 144 144 ]) b. 145 146 alias id "bvt_lookup_opt" = "cic:/matita/cerco/ASM/BitVectorTrie/lookup_opt.fix(0,3,2)". 145 147 146 148 definition member ≝ 
src/ASM/Policy.ma
r1886 r1931 3 3 include "ASM/Fetch.ma". 4 4 include "ASM/Status.ma". 5 include alias "basics/logic.ma".6 include alias "arithmetics/nat.ma".7 5 include "utilities/extralib.ma". 8 6 include "ASM/Assembly.ma". 9 7 8 (*include alias "common/Identifiers.ma". 9 include alias "ASM/BitVector.ma".*) 10 include alias "basics/lists/list.ma". 11 include alias "arithmetics/nat.ma". 12 include alias "basics/logic.ma". 13 10 14 (* Internal types *) 11 15 12 (* label_map: identifier ↦ 〈instruction number, address〉*)13 definition label_map ≝ identifier_map ASMTag (ℕ × ℕ).14 15 (* jump_expansion_policy: instruction number ↦ 〈pc, [addr, jump_length]〉*)16 definition jump_expansion_policy ≝ ℕ × (BitVectorTrie (ℕ × ℕ × jump_length) 16).16 (* label_map: identifier ↦ pseudo program counter *) 17 definition label_map ≝ identifier_map ASMTag ℕ. 18 19 (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *) 20 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × (option jump_length)) 16). 17 21 18 22 (* The different properties that we want/need to prove at some point *) 19 23 (* Anything that's not in the program doesn't end up in the policy *) 20 definition out_of_program_none: list labelled_instruction → jump_expansion_policy→ Prop ≝21 λprefix.λ policy.22 ∀i .i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) (\snd policy) = None ?.24 definition out_of_program_none: list labelled_instruction → ppc_pc_map → Prop ≝ 25 λprefix.λsigma. 26 ∀i:ℕ.i ≥ prefix → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?. 23 27 24 28 (* If instruction i is a jump, then there will be something in the policy at … … 49 53 ]. 50 54 51 definition jump_in_policy: list labelled_instruction → jump_expansion_policy → Prop ≝ 52 λprefix.λpolicy. 55 definition is_jump_to ≝ 56 λx:pseudo_instruction.λd:Identifier. 57 match x with 58 [ Instruction i ⇒ match i with 59 [ JC j ⇒ d = j 60  JNC j ⇒ d = j 61  JZ j ⇒ d = j 62  JNZ j ⇒ d = j 63  JB _ j ⇒ d = j 64  JNB _ j ⇒ d = j 65  CJNE _ j ⇒ d = j 66  DJNZ _ j ⇒ d = j 67  _ ⇒ False 68 ] 69  Call c ⇒ d = c 70  Jmp j ⇒ d = j 71  _ ⇒ False 72 ]. 73 74 definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝ 75 λprefix.λsigma. 53 76 ∀i:ℕ.i < prefix → 54 77 iff (is_jump (nth i ? prefix 〈None ?, Comment []〉)) 55 (∃p:ℕ.∃a:ℕ.∃j:jump_length. 56 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈p,a,j〉). 57 58 definition labels_okay: label_map → jump_expansion_policy → Prop ≝ 59 λlabels.λpolicy. 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 63 ). 78 (∃x:jump_length. 79 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x). 80 81 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *) 82 (* definition labels_okay: label_map → ppc_pc_map → Prop ≝ 83 λlabels.λsigma. 84 bvt_forall ?? (\snd sigma) (λn.λx. 85 let 〈pc,addr_nat〉 ≝ x in 86 ∃id:Identifier.lookup_def … labels id 0 = addr_nat 87 ). *) 64 88 65 89 (* Between two policies, jumps cannot decrease *) … … 83 107 λj1.λj2.jmple j1 j2 ∨ j1 = j2. 84 108 85 definition policy_increase: list labelled_instruction → jump_expansion_policy→86 jump_expansion_policy→ Prop ≝109 definition policy_increase: list labelled_instruction → ppc_pc_map → 110 ppc_pc_map → Prop ≝ 87 111 λprogram.λop.λp. 88 (∀i:ℕ.i < program → 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 ). 112 ∀i.i < program → 113 let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,None ?〉 in 114 let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,None ?〉 in 115 opc ≤ pc ∧ 116 match ox with 117 [ Some oj ⇒ 118 match x with 119 [ Some j ⇒ jmpleq oj j 120  _ ⇒ True 121 ] 122  _ ⇒ True 123 ]. 93 124 94 125 (* Policy safety *) 95 definition policy_safe: jump_expansion_policy → Prop ≝ 96 λpolicy. 97 bvt_forall ?? (\snd policy) (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in 98 match jmp_len with 99 [ short_jump ⇒ if leb pc_nat addr_nat 100 then le (addr_nat  pc_nat) 126 101 else le (pc_nat  addr_nat) 129 102  medium_jump ⇒ 103 let addr ≝ bitvector_of_nat 16 addr_nat in 104 let pc ≝ bitvector_of_nat 16 pc_nat in 105 let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in 106 let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in 107 eq_bv 5 fst_5_addr fst_5_pc = true 108  long_jump ⇒ True 109 ] 110 ). 126 definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ 127 λprogram.λlabels.λsigma. 128 ∀i.i < program → 129 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉 in 130 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in 131 ∀dest.is_jump_to instr dest → 132 let paddr ≝ lookup_def … labels dest 0 in 133 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,None ?〉) in 134 match j with 135 [ None ⇒ True 136  Some j ⇒ match j with 137 [ short_jump ⇒ 138 if leb pc addr 139 then le (addr  pc) 126 140 else le (pc  addr) 129 141  medium_jump ⇒ 142 let a ≝ bitvector_of_nat 16 addr in 143 let p ≝ bitvector_of_nat 16 pc in 144 let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 a in 145 let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 p in 146 eq_bv 5 fst_5_addr fst_5_pc = true 147  long_jump ⇒ True 148 ] 149 ]. 150 151 (* this is the instruction size as determined by the distance from origin to destination *) 152 definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝ 153 λlabels.λsigma.λpc.λi. 154 \fst (assembly_1_pseudoinstruction 155 (λid.bitvector_of_nat 16 (lookup_def … labels id 0)) 156 (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0,None ?〉))) pc 157 (λx.zero 16) i). 158 159 (* this is the instruction size as determined by the jump length given *) 160 definition expand_relative_jump_internal_unsafe: 161 jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝ 162 λjmp_len:jump_length.λi. 163 match jmp_len with 164 [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ] 165  medium_jump ⇒ [ ] (* XXX this should not happen *) 166  long_jump ⇒ 167 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); 168 SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) 169 LJMP (ADDR16 (zero 16)) 170 ] 171 ]. 172 @I 173 qed. 174 175 definition expand_relative_jump_unsafe: 176 jump_length → preinstruction Identifier → list instruction ≝ 177 λjmp_len:jump_length.λi. 178 match i with 179 [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?) 180  JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?) 181  JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr) 182  JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?) 183  JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?) 184  JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr) 185  JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr) 186  CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr) 187  DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr) 188  ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ] 189  ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ] 190  SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ] 191  INC arg ⇒ [ INC ? arg ] 192  DEC arg ⇒ [ DEC ? arg ] 193  MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ] 194  DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ] 195  DA arg ⇒ [ DA ? arg ] 196  ANL arg ⇒ [ ANL ? arg ] 197  ORL arg ⇒ [ ORL ? arg ] 198  XRL arg ⇒ [ XRL ? arg ] 199  CLR arg ⇒ [ CLR ? arg ] 200  CPL arg ⇒ [ CPL ? arg ] 201  RL arg ⇒ [ RL ? arg ] 202  RR arg ⇒ [ RR ? arg ] 203  RLC arg ⇒ [ RLC ? arg ] 204  RRC arg ⇒ [ RRC ? arg ] 205  SWAP arg ⇒ [ SWAP ? arg ] 206  MOV arg ⇒ [ MOV ? arg ] 207  MOVX arg ⇒ [ MOVX ? arg ] 208  SETB arg ⇒ [ SETB ? arg ] 209  PUSH arg ⇒ [ PUSH ? arg ] 210  POP arg ⇒ [ POP ? arg ] 211  XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ] 212  XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ] 213  RET ⇒ [ RET ? ] 214  RETI ⇒ [ RETI ? ] 215  NOP ⇒ [ RealInstruction (NOP ?) ] 216 ]. 217 218 definition instruction_size_jmplen: 219 jump_length → pseudo_instruction → ℕ ≝ 220 λjmp_len. 221 λi. 222 let pseudos ≝ match i with 223 [ Cost cost ⇒ [ ] 224  Comment comment ⇒ [ ] 225  Call call ⇒ 226 match jmp_len with 227 [ short_jump ⇒ [ ] (* XXX this should not happen *) 228  medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ] 229  long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ] 230 ] 231  Mov d trgt ⇒ 232 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))] 233  Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr 234  Jmp jmp ⇒ 235 match jmp_len with 236 [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ] 237  medium_jump ⇒ [ AJMP (ADDR11 (zero 11)) ] 238  long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ] 239 ] 240 ] in 241 let mapped ≝ map ? ? assembly1 pseudos in 242 let flattened ≝ flatten ? mapped in 243 let pc_len ≝ length ? flattened in 244 pc_len. 245 @I. 246 qed. 247 248 (* new safety condition: policy corresponds to program and resulting program is compact *) 249 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ 250 λprogram.λlabels.λsigma. 251 ∀n:ℕ.S n < program → 252 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with 253 [ None ⇒ False 254  Some x ⇒ let 〈pc,j〉 ≝ x in 255 match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with 256 [ None ⇒ False 257  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 258 pc1 = instruction_size_sigma labels sigma (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉)) 259 ] 260 ]. 111 261 112 262 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) … … 127 277 ]. 128 278 129 lemma dec_jmple: ∀x,y:jump_length. jmple x y + ¬(jmple x y).279 lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)). 130 280 #x #y cases x cases y /3 by inl, inr, nmk, I/ 131 281 qed. … … 137 287 qed. 138 288 139 lemma dec_eq_jump_length: ∀a,b:jump_length. (a = b) +(a ≠ b).289 lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b). 140 290 #a #b cases a cases b /2/ 141 291 %2 @nmk #H destruct (H) … … 155 305 is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false. 156 306 #i #p #l generalize in match i; elim p 157 [ #i >nth_nil #H @⊥ @H307 [ #i >nth_nil #H cases H 158 308  #h #t #IH #i cases i i 159 309 [ cases h #hi #hp cases hi 160 [ normalize #H @⊥ @H310 [ normalize #H cases H 161 311  #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????); 162 312 whd in Heq; >Heq … … 175 325 ] 176 326 qed. 177 178 definition expand_relative_jump_internal_unsafe:179 jump_length → ([[relative]] → preinstruction [[relative]]) → option (list instruction) ≝180 λjmp_len:jump_length.λi.181 match jmp_len with182 [ 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 @I191 qed.192 193 definition expand_relative_jump_unsafe:194 jump_length → preinstruction Identifier → option (list instruction) ≝195 λjmp_len:jump_length.λi.196 match i with197 [ 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 with241 [ Cost cost ⇒ Some ? [ ]242  Comment comment ⇒ Some ? [ ]243  Call call ⇒244 match jmp_len with245 [ 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 instr252  Jmp jmp ⇒253 match jmp_len with254 [ 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 @I260 qed.261 262 definition instruction_size: (* ℕ → *) jump_length → pseudo_instruction → ℕ ≝263 λjmp_len.λinstr.264 let ilist ≝ expand_pseudo_instruction_unsafe jmp_len instr in265 let bv: list (BitVector 8) ≝ match ilist with266 [ None ⇒ (* this shouldn't happen *) [ ]267  Some l ⇒ flatten … (map … assembly1 l)268 ] in269 bv.270 327 271 328 definition policy_isize_sum ≝ 272 λprefix:list labelled_instruction.λ policy:jump_expansion_policy.273 (\fst policy) = foldl_strong (option Identifier × pseudo_instruction)329 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. 330 (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction) 274 331 (λacc.ℕ) 275 332 prefix 276 333 (λ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))) 334 acc + (instruction_size_sigma labels sigma (bitvector_of_nat 16 (\fst sigma)) (\snd x))) 279 335 0. 280 336 281 337 (* The function that creates the labeltoaddress map *) 282 338 definition create_label_map: ∀program:list labelled_instruction. 283 ∀policy:jump_expansion_policy.284 339 (Σlabels:label_map. 285 340 ∀i:ℕ.lt i (program) → 286 341 ∀l.occurs_exactly_once ?? l program → 287 342 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 288 ∃a.lookup … labels l = Some ? 〈i,a〉343 lookup ?? labels l = Some ? i 289 344 ) ≝ 290 λprogram.λpolicy. 291 let 〈final_pc, final_labels〉 ≝ 292 foldl_strong (option Identifier × pseudo_instruction) 293 (λprefix.ℕ × (Σlabels. 294 ∀i:ℕ.lt i (prefix) → 295 ∀l.occurs_exactly_once ?? l prefix → 296 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 297 ∃a.lookup … labels l = Some ? 〈i,a〉) 298 ) 299 program 300 (λprefix.λx.λtl.λprf.λacc. 301 let 〈pc,labels〉 ≝ acc in 302 let 〈label,instr〉 ≝ x in 303 let new_labels ≝ 304 match label with 305 [ None ⇒ labels 306  Some l ⇒ add ? (ℕ×ℕ) labels l 〈prefix, pc〉 307 ] in 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〉 311 ) 〈0, empty_map …〉 in 312 final_labels. 313 [#i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 314 [ #Hi #l normalize nodelta; cases label normalize nodelta 315 [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl 316 lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 317 % [ @addr  @Haddr ] 318  #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) Hocc; 319 @eq_identifier_elim #Heq #Hocc 320 [ normalize in Hocc; 321 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 322 @⊥ @(absurd … Hocc) 323  normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?) 324 [ #addr #Haddr % [ @addr  <Haddr @lookup_add_miss /2/ ] 325  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / by / 345 λprogram. 346 foldl_strong (option Identifier × pseudo_instruction) 347 (λprefix.Σlabels:label_map. 348 ∀i:ℕ.lt i (prefix) → 349 ∀l.occurs_exactly_once ?? l prefix → 350 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 351 lookup … labels l = Some ? i 352 ) 353 program 354 (λprefix.λx.λtl.λprf.λlabels. 355 let 〈label,instr〉 ≝ x in 356 match label with 357 [ None ⇒ labels 358  Some l ⇒ add … labels l (prefix) 359 ] 360 ) (empty_map …). 361 [1,2: #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 362 [ #Hi #lbl #Hocc #Hlbl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) Hocc 363 @eq_identifier_elim 364 [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl 365 @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/ 366  #Heq #Hocc normalize in Hocc; >lookup_add_miss 367 [ @(pi2 … labels i (le_S_S_to_le … Hi)) 368 [ @Hocc 369  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by / 326 370 ] 327 ] 328 >(label_does_not_occur i … Hl) normalize nodelta @nmk / by / 329 ] 330  #Hi #l #Hocc >(injective_S … Hi) >nth_append_second 331 [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl; 332 [ normalize nodelta #H @⊥ @H 333  #l' normalize nodelta #Heq % [ @pc  <Heq normalize nodelta @lookup_add_hit ] 334 ] 371  @sym_neq @Heq 372 ] 373 ] 374  #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second 375 [ <minus_n_n #Hl normalize in Hl; >Hl @lookup_add_hit 335 376  @le_n 336 377 ] 337 ] 338  #i #Hi #l #Hl @⊥ @Hl 378  #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl 379 @(pi2 … labels i (le_S_S_to_le … Hi)) 380 [ @Hocc 381  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by / 382 ] 383  #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second 384 [ <minus_n_n #Hl cases Hl 385  @le_n 386 ] 387 ] 388  #i #Hi #l #Hl cases Hl 339 389 ] 340 390 qed. 341 391 342 definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝ 343 λlabels.λpc.λlbl. 344 let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in 345 if leb pc addr (* forward jump *) 346 then if leb (addr  pc) 126 347 then 〈addr, short_jump〉 348 else 〈addr, long_jump〉 349 else if leb (pc  addr) 129 350 then 〈addr, short_jump〉 351 else 〈addr, long_jump〉. 352 353 definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝ 354 λlabels.λpc_nat.λlbl. 355 let pc ≝ bitvector_of_nat 16 pc_nat in 356 let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in 357 let addr ≝ bitvector_of_nat 16 addr_nat in 358 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in 359 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 392 definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → 393 Identifier → jump_length ≝ 394 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. 395 let paddr ≝ lookup_def … labels lbl 0 in 396 if leb ppc paddr (* forward jump *) 397 then 398 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,None ?〉) 399 + added in 400 if leb (addr  \fst inc_sigma) 126 401 then short_jump 402 else long_jump 403 else 404 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,None ?〉) in 405 if leb (\fst inc_sigma  addr) 129 406 then short_jump 407 else long_jump. 408 409 definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → 410 Identifier → jump_length ≝ 411 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. 412 let paddr ≝ lookup_def ? ? labels lbl 0 in 413 let addr ≝ 414 if leb ppc paddr (* forward jump *) 415 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,None ?〉) 416 + added 417 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,None ?〉) in 418 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (bitvector_of_nat ? addr) in 419 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in 360 420 if eq_bv ? fst_5_addr fst_5_pc 361 then 〈addr_nat, medium_jump〉362 else 〈addr_nat, long_jump〉.421 then medium_jump 422 else long_jump. 363 423 364 definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝ 365 λlabels.λpc.λlbl. 366 let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in 367 if leb pc addr 368 then if leb (addr  pc) 126 369 then 〈addr, short_jump〉 370 else select_call_length labels pc lbl 371 else if leb (pc  addr) 129 372 then 〈addr, short_jump〉 373 else select_call_length labels pc lbl. 424 definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → 425 Identifier → jump_length ≝ 426 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. 427 let paddr ≝ lookup_def … labels lbl 0 in 428 if leb ppc paddr (* forward jump *) 429 then 430 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,None ?〉) 431 + added in 432 if leb (addr  \fst inc_sigma) 126 433 then short_jump 434 else select_call_length labels old_sigma inc_sigma added ppc lbl 435 else 436 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,None ?〉) in 437 if leb (\fst inc_sigma  addr) 129 438 then short_jump 439 else select_call_length labels old_sigma inc_sigma added ppc lbl. 374 440 375 definition jump_expansion_step_instruction: label_map → ℕ→376 preinstruction Identifier → option (ℕ × jump_length)≝377 λlabels.λ pc.λi.441 definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → 442 ℕ → ℕ → preinstruction Identifier → option jump_length ≝ 443 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi. 378 444 match i with 379 [ JC j ⇒ Some ? (select_reljump_length labels pc j)380  JNC j ⇒ Some ? (select_reljump_length labels pc j)381  JZ j ⇒ Some ? (select_reljump_length labels pc j)382  JNZ j ⇒ Some ? (select_reljump_length labels pc j)383  JB _ j ⇒ Some ? (select_reljump_length labels pc j)384  JBC _ j ⇒ Some ? (select_reljump_length labels pc j)385  JNB _ j ⇒ Some ? (select_reljump_length labels pc j)386  CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)387  DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)445 [ JC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 446  JNC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 447  JZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 448  JNZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 449  JB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 450  JBC _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 451  JNB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 452  CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 453  DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 388 454  _ ⇒ None ? 389 455 ]. 390 456 391 lemma dec_is_jump: ∀x. (is_jump x) +(¬is_jump x).457 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x). 392 458 #x cases x #l #i cases i 393 459 [#id cases id … … 407 473 408 474 lemma jump_not_in_policy: ∀prefix:list labelled_instruction. 409 ∀policy:(Σp: jump_expansion_policy.475 ∀policy:(Σp:ppc_pc_map. 410 476 out_of_program_none prefix p ∧ jump_in_policy prefix p). 411 477 ∀i:ℕ.i < prefix → 412 478 iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉)) 413 ( lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = None ?).479 (\snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) = None ?). 414 480 #prefix #policy #i #Hi @conj 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))) 481 [ #Hnotjmp lapply (refl ? (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉)) 482 cases (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) in ⊢ (???% → ?); 483 #pc #j cases j 484 [ #H >H @refl 485  #x #H >H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi)) 486 >H @(ex_intro ?? x ?) / by / 420 487 ] 421 488  #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)489 #H elim H H; #x #H >H in Hnone; #abs destruct (abs) 423 490 ] 424 491 qed. … … 440 507 definition jump_expansion_start: 441 508 ∀program:(Σl:list labelled_instruction.l < 2^16). 442 Σpolicy:jump_expansion_policy. 443 And (And (out_of_program_none (pi1 ?? program) policy) 444 (jump_in_policy (pi1 ?? program) policy)) 445 (∀i.i < pi1 ?? program → is_jump (nth i ? (pi1 ?? program) 〈None ?, Comment []〉) → 446 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉) ≝ 447 λprogram. 509 ∀labels:label_map. 510 Σpolicy:ppc_pc_map. 511 And (out_of_program_none (pi1 ?? program) policy) 512 (jump_in_policy (pi1 ?? program) policy) ≝ 513 λprogram.λlabels. 448 514 foldl_strong (option Identifier × pseudo_instruction) 449 (λprefix.Σpolicy:jump_expansion_policy. 450 And (And (out_of_program_none prefix policy) 451 (jump_in_policy prefix policy)) 452 (∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 453 lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉)) 515 (λprefix.Σpolicy:ppc_pc_map. 516 (And (out_of_program_none prefix policy) 517 (jump_in_policy prefix policy))) 454 518 program 455 519 (λprefix.λx.λtl.λprf.λp. 456 let 〈pc, policy〉 ≝ p in520 let 〈pc,sigma〉 ≝ p in 457 521 let 〈label,instr〉 ≝ x in 458 〈pc + instruction_size short_jump instr,match instr with 522 let isize ≝ instruction_size_jmplen short_jump instr in 523 〈pc + isize, 524 match instr with 459 525 [ Instruction i ⇒ match i with 460 [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,0,short_jump〉 policy461  JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy462  JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy463  JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy464  JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy465  JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy466  JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy467  CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy468  DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy469  _ ⇒ policy526 [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 527  JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 528  JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 529  JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 530  JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 531  JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 532  JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 533  CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 534  DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 535  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,None ?〉 sigma 470 536 ] 471  Call c ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy472  Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈 0,0,short_jump〉 policy473  _ ⇒ policy537  Call c ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 538  Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,Some ? short_jump〉 sigma 539  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,None ?〉 sigma 474 540 ]〉 475 541 ) 〈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 542 [ @conj #i >append_length <commutative_plus #Hi normalize in Hi; 543 [ #Hi2 544 cases (le_to_or_lt_eq … Hi) Hi #Hi 545 cases p p #p cases p p #pc #p #Hp cases x x #l #pi cases pi 481 546 [1,7: #id cases id normalize nodelta 482 547 [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 548 [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 549 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_opt_insert_miss 550 [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: 551 @bitvector_of_nat_abs 552 [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: 553 @Hi2 554 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: 555 @(transitive_lt … Hi2) @le_S_to_le @Hi 556 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: 557 @sym_neq @lt_to_not_eq @le_S_to_le @Hi 558 ] 559 ] 560 @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi 486 561 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 562 [1,2,3,6,7,24,25: #x #y 488 563 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))) ?) 564 >lookup_opt_insert_miss 565 [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: 566 @bitvector_of_nat_abs 567 [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: 568 @Hi2 569 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: 570 @(transitive_lt … Hi2) <Hi @le_n 571 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: 572 @sym_neq @lt_to_not_eq <Hi @le_n 573 ] 574 ] 575 <Hi @(proj1 ?? Hp (S (prefix)) (le_S ?? (le_n (prefix))) ?) 490 576 >Hi @Hi2 491 577 9,10,11,12,13,14,15,16,17: … … 497 583 ] 498 584 1,3,5,7,9,11,13,15,17: 499 @(proj1 ?? (proj1 ?? Hp)i ? Hi2) @le_S_to_le @le_S_to_le @Hi585 @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi 500 586 ] 501 587 46,47,48,49,50,51,52,53,54: … … 507 593 ] 508 594 1,3,5,7,9,11,13,15,17: 509 @(proj1 ?? (proj1 ?? Hp)i ? Hi2) <Hi @le_S @le_n595 @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n 510 596 ] 511 597 ] 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 598 2,3,6,8,9,12: [3,6: #w] #z >lookup_opt_insert_miss 599 [2,4,6,8,10,12: @bitvector_of_nat_abs 600 [1,4,7,10,13,16: @Hi2 601 2,8,11: @(transitive_lt … Hi2) @le_S_to_le @Hi 602 5,14,17: @(transitive_lt … Hi2) <Hi @le_n 603 3,9,12: @sym_neq @lt_to_not_eq @le_S_to_le @Hi 604 6,15,18: <Hi @sym_neq @lt_to_not_eq @le_n 605 ] 606 ] 607 [1,3,4: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi 514 608 2,5,6: 515 <Hi @(proj1 ?? (proj1 ?? Hp)(S (prefix)) (le_S ?? (le_n (prefix))) ?)609 <Hi @(proj1 ?? Hp (S (prefix)) (le_S ?? (le_n (prefix))) ?) 516 610 >Hi @Hi2 517 611 ] … … 524 618 9,12: @sym_neq @lt_to_not_eq <Hi @le_n 525 619 ] 526 1,3: @(proj1 ?? (proj1 ?? Hp)i ? Hi2) @le_S_to_le @le_S_to_le @Hi527 5,7: @(proj1 ?? (proj1 ?? Hp)i ? Hi2) <Hi @le_S @le_n620 1,3: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi 621 5,7: @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n 528 622 ] 529 623 ] 530 624  cases (le_to_or_lt_eq … Hi) Hi #Hi 531 625 [ >(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 626 [ #Hj cases p p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta 534 627 [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 628 [1,2,3,6,7,33,34,35,36,37: [1,2,3,4,5,6,7: #x #y] >lookup_insert_miss 629 [2,4,6,8,10,12,14,16,18,20: @bitvector_of_nat_abs 630 [1,4,7,10,13,16,19,22,25,28: @(transitive_lt … (pi2 ?? program)) >prf 631 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 632 @le_S_S_to_le @le_plus_n_r 633 2,5,8,11,14,17,20,23,26,29: @(transitive_lt … (pi2 ?? program)) >prf 634 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 635 3,6,9,12,15,18,21,24,27,30: @lt_to_not_eq @(le_S_S_to_le … Hi) 636 ] 637 ] 638 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x >lookup_insert_miss 639 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36: @bitvector_of_nat_abs 640 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52: 641 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm 642 @le_S_to_le @(transitive_le … Hi) @le_S_S_to_le @le_plus_n_r 643 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53: 644 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm 645 @le_S_S_to_le @le_plus_n_r 646 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54: 647 @lt_to_not_eq @(le_S_S_to_le … Hi) 648 ] 649 ] 537 650 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_miss651 [1,2,6,7: #x  3,4,5,8,9: #x #id] >lookup_insert_miss 539 652 [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 540 653 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf … … 546 659 ] 547 660 ] 661 ] 662 2,3: #x >lookup_insert_miss 663 [2,4: @bitvector_of_nat_abs 664 [1,4: @(transitive_lt … (pi2 ?? program)) >prf 665 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 666 @le_S_S_to_le @le_plus_n_r 667 2,5: @(transitive_lt … (pi2 ?? program)) >prf 668 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 669 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 670 ] 548 671 ] 549 2,3: #x 550 4,5: #id >lookup_opt_insert_miss 672 4,5: #id >lookup_insert_miss 551 673 [2,4: @bitvector_of_nat_abs 552 674 [1,4: @(transitive_lt … (pi2 ?? program)) >prf … … 558 680 ] 559 681 ] 560 6: #x #id 682 6: #x #id >lookup_insert_miss 683 [2: @bitvector_of_nat_abs 684 [ @(transitive_lt … (pi2 ?? program)) >prf 685 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 686 @le_S_S_to_le @le_plus_n_r 687  @(transitive_lt … (pi2 ?? program)) >prf 688 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 689  @lt_to_not_eq @(le_S_S_to_le … Hi) 690 ] 691 ] 561 692 ] 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 ] 693 @(proj1 ?? (proj2 ?? Hp i (le_S_S_to_le … Hi)) Hj) 694  #H @(proj2 ?? (proj2 ?? (pi2 ?? p) i (le_S_S_to_le … Hi))) 695 cases p in H; p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta 696 [1: #id cases id 697 [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: 698 [1,2,3,6,7,24,25: #x #y 699 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 700 normalize nodelta >lookup_insert_miss 701 [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: 702 @bitvector_of_nat_abs 703 [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: 704 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm 705 @le_S_to_le @(transitive_le … Hi) @le_S_S_to_le @le_plus_n_r 706 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: 707 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm 708 @le_S_S_to_le @le_plus_n_r 709 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: 710 @lt_to_not_eq @(le_S_S_to_le … Hi) 711 ] 712 ] / by / 713 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #x #id] 714 normalize nodelta >lookup_insert_miss 715 [1,3,5,7,9,11,13,15,17: / by / 716 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 717 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 718 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 719 @le_S_S_to_le @le_plus_n_r 720 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 721 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 722 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi) 582 723 ] 583 724 ] 584 2,3: #x / by /585 4,5: #id >lookup_opt_insert_miss586 587 588 589 590 591 592 593 725 ] 726 2,3: #x >lookup_insert_miss 727 [2,4: @bitvector_of_nat_abs 728 [1,4: @(transitive_lt … (pi2 ?? program)) >prf 729 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 730 @le_S_S_to_le @le_plus_n_r 731 2,5: @(transitive_lt … (pi2 ?? program)) >prf 732 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 733 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 734 ] 594 735 1,3: / by / 736 ] 737 4,5: #id >lookup_insert_miss 738 [2,4: @bitvector_of_nat_abs 739 [1,4: @(transitive_lt … (pi2 ?? program)) >prf 740 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 741 @le_S_S_to_le @le_plus_n_r 742 2,5: @(transitive_lt … (pi2 ?? program)) >prf 743 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 744 3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 595 745 ] 596  6: #x #id/ by /746 1,3: / by / 597 747 ] 748 6: #x #id >lookup_insert_miss 749 [2: @bitvector_of_nat_abs 750 [@(transitive_lt … (pi2 ?? program)) >prf 751 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi) 752 @le_S_S_to_le @le_plus_n_r 753 @(transitive_lt … (pi2 ?? program)) >prf 754 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 755 @lt_to_not_eq @(le_S_S_to_le … Hi) 756 ] 757 ] 758 / by / 598 759 ] 599 760 ] 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 ] 761  >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (prefix))) 762 <minus_n_n whd in match (nth ????); cases x #l #ins cases ins 763 [1: #pi cases pi 764 [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: 765 [1,2,3,6,7,24,25: #x #y 766 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 767 @conj 768 [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: 769 #H cases H in ⊢ ?; 770 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: 771 cases p p #p cases p p #pc #pol #Hp #H elim H H #p 772 normalize nodelta >lookup_insert_hit #H destruct (H) 628 773 ] 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 ] 774 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x  3,4,5,8,9: #x #id] 775 @conj normalize nodelta 776 [(*1: #_ @(ex_intro ?? (zero ?) (ex_intro ?? (bitvector_of_nat ? (lookup_def … labels x 0)) ?))*) 777 1,3,5,7,9,11,13,15,17: #_ @(ex_intro ?? short_jump ?) 778 2,4,6,8,10,12,14,16,18: #_ / by I/ 638 779 ] 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/ 780 cases p p #p cases p p #pc #pol #Hp >lookup_insert_hit @refl 643 781 ] 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) 782 2,3,6: #x [3: #id] @conj 783 [1,3,5: #H @⊥ @H 784 2,4,6: 785 cases p p #p cases p p #pc #pol #Hp #H elim H H #p 786 normalize nodelta >lookup_insert_hit #H destruct (H) 787 (* [1,3,5: #_ #H destruct (H) 788 2,4,6: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm 663 789 @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 ] 790 ] *) 668 791 ] 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) 792 4,5: #x @conj 793 [1,3: #_ @(ex_intro ?? (short_jump) ?) 794 cases p p #p cases p p #pc #pol #Hp normalize nodelta >lookup_insert_hit @refl 795 2,4: #_ / by I/ 681 796 ] 682 797 ] 683 798 ] 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 / 799 ] 800  @conj 801 [ #i #_ #Hi2 / by refl/ 802  #i #_ @conj 803 [ >nth_nil #H @⊥ @H 804  #H elim H H #p >lookup_stub #H destruct (H) 696 805 ] 697 806 ] 698 807 ] 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 ] 709 ] 710 qed. 711 712 definition policy_equal_int ≝ 713 λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy. 714 ∀n:ℕ.n < program → 715 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 717 j1 = j2. 808 qed. 809 810 definition policy_equal ≝ 811 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 812 (* \fst p1 = \fst p2 ∧ *) 813 (∀n:ℕ.n < program → 814 let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,None ?〉 in 815 let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,None ?〉 in 816 pc1 = pc2). 718 817 719 definition nec_plus_ultra ≝720 λprogram:list labelled_instruction.λp: jump_expansion_policy.721 ¬(∀i.i < program → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). 818 (*definition nec_plus_ultra ≝ 819 λprogram:list labelled_instruction.λp:ppc_pc_mapjump_expansion_policy. 820 ¬(∀i.i < program → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). *) 722 821 723 822 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a. … … 725 824 qed. 726 825 727 (*lemma foldl_strong_eq: 728 ∀A: Type[0]. 729 ∀P: list A → Type[0]. 730 ∀l: list A. 731 ∀H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]). 732 ∀acc: P [ ]. 733 foldl_strong_internal A P l H [ ] l acc (refl …).*) 826 include alias "common/Identifiers.ma". 827 include alias "ASM/BitVector.ma". 828 include alias "basics/lists/list.ma". 829 include alias "arithmetics/nat.ma". 830 include alias "basics/logic.ma". 734 831 735 832 736 833 (* One step in the search for a jump expansion fixpoint. *) 834 (* Takes a horrible amount of time to typecheck. I suspect disambiguation problems. *) 737 835 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 738 ∀labels:(Σlm:label_map.∀i:ℕ.lt i (pi1 ?? program) → 739 ∀l.occurs_exactly_once ?? l (pi1 ?? program) → 740 is_label (nth i ? (pi1 ?? program) 〈None ?, Comment [ ]〉) l → 741 ∃a.lookup … lm l = Some ? 〈i,a〉). 742 ∀old_policy:(Σpolicy:jump_expansion_policy. 743 out_of_program_none (pi1 ?? program) policy ∧ 744 jump_in_policy (pi1 ?? program) policy ∧ (\fst policy < 2^16) ∧ 745 policy_isize_sum (pi1 ?? program) policy). 746 (Σx:bool × (option jump_expansion_policy). 747 let 〈ch,y〉 ≝ x in 836 ∀labels:(Σlm:label_map. ∀i:ℕ.lt i (program) → 837 ∀l.occurs_exactly_once ?? l program → 838 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 839 lookup … lm l = Some ? i). 840 ∀old_policy:(Σpolicy:ppc_pc_map. 841 And (And (And (out_of_program_none program policy) 842 (jump_in_policy program policy)) 843 (policy_isize_sum program labels policy)) 844 (\fst policy < 2^16)). 845 (Σx:bool × (option ppc_pc_map). 846 let 〈no_ch,y〉 ≝ x in 748 847 match y with 749 [ None ⇒ nec_plus_ultra program old_policy 750  Some p ⇒ out_of_program_none (pi1 ?? program) p ∧ labels_okay labels p ∧ 751 jump_in_policy (pi1 ?? program) p ∧ 752 policy_increase (pi1 ?? program) old_policy p ∧ policy_safe p ∧ 753 (ch = false → policy_equal_int (pi1 ?? program) old_policy p) ∧ 754 policy_isize_sum (pi1 ?? program) p ∧ \fst p < 2^16 848 [ None ⇒ (* nec_plus_ultra program old_policy *) True 849  Some p ⇒ And (And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p) (* labels_okay labels p ∧*) 850 (jump_in_policy program p)) 851 (policy_isize_sum program labels p)) 852 (policy_increase program old_policy p)) 853 (policy_safe program labels p)) 854 (policy_compact program labels p)) 855 (no_ch = true → policy_equal program old_policy p)) 856 (\fst p < 2^16) 755 857 ]) 756 ≝ 757 λprogram.λlabels.λold_ policy.758 let 〈final_ changed, final_policy〉 ≝858 ≝ 859 λprogram.λlabels.λold_sigma. 860 let 〈final_added, final_policy〉 ≝ 759 861 foldl_strong (option Identifier × pseudo_instruction) 760 (λprefix.Σx:bool × jump_expansion_policy. 761 let 〈changed,policy〉 ≝ x in 762 out_of_program_none prefix policy ∧ labels_okay labels policy ∧ 763 jump_in_policy prefix policy ∧ 764 policy_increase prefix old_policy policy ∧ 765 policy_safe policy ∧ 766 (changed = false → policy_equal_int prefix old_policy policy) ∧ 767 policy_isize_sum prefix policy) 862 (λprefix.Σx:ℕ × ppc_pc_map. 863 let 〈added,policy〉 ≝ x in 864 And (And (And (And (And (And (out_of_program_none prefix policy) 865 (jump_in_policy prefix policy)) 866 (policy_isize_sum prefix labels policy)) 867 (policy_increase prefix old_sigma policy)) 868 (policy_safe prefix labels policy)) 869 (policy_compact prefix labels policy)) 870 (added = 0 → policy_equal prefix old_sigma policy)) 768 871 program 769 872 (λprefix.λx.λtl.λprf.λacc. 770 let 〈changed, pol〉 ≝ acc in 771 (* let 〈pc,pol〉 ≝ p in *) 873 let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in 772 874 let 〈label,instr〉 ≝ x in 773 let add_instr ≝ 774 match instr with 775 [ Instruction i ⇒ jump_expansion_step_instruction labels (\fst pol) i 776  Call c ⇒ Some ? (select_call_length labels (\fst pol) c) 777  Jmp j ⇒ Some ? (select_jump_length labels (\fst pol) j) 778  _ ⇒ None ? 875 (* Now, we must add the current ppc and its pc translation. 876 * Three possibilities: 877 *  Instruction is not a jump; i.e. constant size whatever the sigma we use; 878 *  Instruction is a backward jump; we can use the sigma we're constructing, 879 * since it will already know the translation of its destination; 880 *  Instruction is a forward jump; we must use the old sigma (the new sigma 881 * does not know the translation yet), but compensate for the jumps we 882 * have lengthened. 883 *) 884 let add_instr ≝ match instr with 885 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 886  Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 887  Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (prefix) i 888  _ ⇒ None ? 889 ] in 890 let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in 891 let 〈old_pc, old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,None ?〉 in 892 match add_instr with 893 [ None ⇒ 894 let isize ≝ instruction_size_jmplen short_jump instr in 895 (* instruction is not a jump: nothing changes *) 896 〈inc_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat 16 (prefix)) 〈inc_pc, None ?〉 inc_sigma〉〉 897  Some proj_length ⇒ 898 let x ≝ match old_length with 899 [ None ⇒ (* this should not happen! *) short_jump 900  Some y ⇒ y 779 901 ] in 780 let old_length ≝ \snd (bvt_lookup … (bitvector_of_nat 16 (prefix)) (\snd old_policy) 〈0,0,short_jump〉) in 781 match add_instr with 782 [ None ⇒ (* i.e. it's not a jump *) 783 let isize ≝ instruction_size short_jump instr in 784 〈changed, 〈(\fst pol) + isize, (\snd pol)〉〉 785  Some z ⇒ let 〈addr,ai〉 ≝ z in 786 let new_length ≝ max_length old_length ai in 787 let isize ≝ instruction_size new_length instr in 788 〈match dec_eq_jump_length new_length old_length with 789 [ inl _ ⇒ changed 790  inr _ ⇒ true], 〈(\fst pol) + isize, 791 insert … (bitvector_of_nat 16 (prefix)) 〈(\fst pol), addr, new_length〉 (\snd pol)〉〉 792 ] 793 ) 〈false, 〈0, Stub ? ?〉〉 in 902 let new_length ≝ max_length x proj_length in 903 let old_size ≝ instruction_size_jmplen x instr in 904 let isize ≝ instruction_size_jmplen new_length instr in 905 〈plus inc_added (minus isize old_size), 〈plus inc_pc isize, 906 bvt_insert … (bitvector_of_nat 16 (prefix)) 〈inc_pc, Some ? new_length〉 inc_sigma〉〉 907 ] 908 ) 〈0, 〈0, Stub ??〉〉 in 794 909 if geb (\fst final_policy) 2^16 then 795 〈 final_changed,None ?〉910 〈eqb final_added 0, None ?〉 796 911 else 797 〈final_changed,Some ? final_policy〉. 798 [ @pair_elim #fch #x #Heq <(pair_eq2 ?????? Heq) normalize nodelta 799 @nmk #Hfull lapply p generalize in match (foldl_strong ?????); * #x #H #H2 800 >H2 in H; normalize nodelta H2 x #H 801 @(absurd ((\fst final_policy) ≥ 2^16)) 802 [ @leb_true_to_le <geb_to_leb @p1 803  @lt_to_not_le @(le_to_lt_to_lt … (proj2 ?? (proj1 ?? (pi2 ?? old_policy)))) 804 >(proj2 ?? H) >(proj2 ?? (pi2 ?? old_policy)) cases daemon (* XXX *) 805 ] 912 〈eqb final_added 0, Some ? final_policy〉. 913 [ / by I/ 806 914  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 807 >H2 in H; normalize nodelta #H @conj 808 [ @H 915 >H2 in H; normalize nodelta H2 x #H @conj 916 [ @conj 917 [ @(proj1 ?? H) 918  #H2 @(proj2 ?? H) @eqb_true_to_eq @H2 919 ] 809 920  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 810 921 ] 811  lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy; 922  (* XXX complicated proof *) cases daemon 923  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj 924 [ #i #Hi / by refl/ 925  #i #Hi @conj [ >nth_nil #H @⊥ @H  #H elim H #x H #H 926 normalize in Hi; @⊥ @(absurd ? Hi) @not_le_Sn_O ] 927 ] 928  / by refl/ 929 ]]]]] 930 [4: #_] 931 #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 932 ] 933 qed. 934 935 (* old proof  lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy; 812 936 cases (dec_eq_jump_length new_length old_length) #Hlength normalize nodelta 813 937 @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj … … 1179 1303 ] 1180 1304 ] 1181 qed. 1305 qed.*) 1182 1306 1183 1307 (* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *) … … 1220 1344 1221 1345 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ) 1222 on n:(Σx:bool × (option jump_expansion_policy).1346 on n:(Σx:bool × (option ppc_pc_map). 1223 1347 let 〈c,pol〉 ≝ x in 1224 1348 match pol with 1225 1349 [ None ⇒ True 1226  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) 1350  Some x ⇒ 1351 And (And (And 1352 (out_of_program_none program x) 1353 (jump_in_policy program x)) 1354 (policy_isize_sum program (create_label_map program) x)) 1355 (\fst x < 2^16) 1227 1356 ]) ≝ 1357 let labels ≝ create_label_map program in 1228 1358 match n with 1229 [ O ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program ))〉1359 [ O ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program labels))〉 1230 1360  S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 1231 match z return λx. z=x → Σa:bool × (option jump_expansion_policy).? with1361 match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with 1232 1362 [ None ⇒ λp2.〈false,None ?〉 1233 1363  Some op ⇒ λp2.if ch 1234 then pi1 ?? (jump_expansion_step program (create_label_map program op)«op,?»)1364 then pi1 ?? (jump_expansion_step program labels «op,?») 1235 1365 else (jump_expansion_internal program m) 1236 1366 ] (refl … z) … … 1238 1368 [ normalize nodelta @conj 1239 1369 [ @conj 1240 [ @(p roj1 ?? (pi2 ?? (jump_expansion_startprogram)))1370 [ @(pi2 ?? (jump_expansion_start program (create_label_map program))) 1241 1371  (* XXX *) cases daemon 1242 1372 ] … … 1245 1375  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 1246 1376  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 1247  normalize nodelta cases (jump_expansion_step program (create_label_map program op)«op,?»)1377  normalize nodelta cases (jump_expansion_step program labels «op,?») 1248 1378 #p cases p p #p #r cases r normalize nodelta 1249 1379 [ #H / by I/ … … 1252 1382 [ @conj 1253 1383 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))) 1254  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))1384  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))) 1255 1385 ] 1256  @(proj2 ?? H)1257 ] 1258  @(proj2 ?? (proj1 ?? H))1386  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 1387 ] 1388  @(proj2 ?? H) 1259 1389 ] 1260 1390 ] … … 1262 1392 qed. 1263 1393 1264 lemma pe_int_refl: ∀program.reflexive ? (policy_equal _intprogram).1394 lemma pe_int_refl: ∀program.reflexive ? (policy_equal program). 1265 1395 #program whd #x whd #n #Hn 1266 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0, 0,short_jump〉)1267 #y cases y y #y#z normalize nodelta @refl1268 qed. 1269 1270 lemma pe_int_sym: ∀program.symmetric ? (policy_equal _intprogram).1396 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,None ?〉) 1397 #y #z normalize nodelta @refl 1398 qed. 1399 1400 lemma pe_int_sym: ∀program.symmetric ? (policy_equal program). 1271 1401 #program whd #x #y #Hxy whd #n #Hn 1272 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0, 0,short_jump〉)1273 # z cases z z #x1 #x2 #x31274 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0, 0,short_jump〉)1275 # z cases z z #y1 #y2 #y3normalize nodelta //1402 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,None ?〉) 1403 #x1 #x2 1404 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,None ?〉) 1405 #y1 #y2 normalize nodelta // 1276 1406 qed. 1277 1407 1278 lemma pe_int_trans: ∀program.transitive ? (policy_equal_int program). 1279 #program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?); 1280 whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy 1281 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉) 1282 #z cases z z #x1 #x2 #x3 1283 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉) #z cases z z 1284 #y1 #y2 #y3 1285 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,0,short_jump〉) #z cases z z 1286 #z1 #z2 #z3 normalize nodelta // 1287 qed. 1288 1289 definition policy_equal ≝ 1290 λprogram:list labelled_instruction.λp1,p2:option jump_expansion_policy. 1408 lemma pe_int_trans: ∀program.transitive ? (policy_equal program). 1409 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?); 1410 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy 1411 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,None ?〉) 1412 #x1 #x2 1413 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,None ?〉) #y1 #y2 1414 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,None ?〉) #z1 #z2 1415 normalize nodelta // 1416 qed. 1417 1418 definition policy_equal_opt ≝ 1419 λprogram:list labelled_instruction.λp1,p2:option ppc_pc_map. 1291 1420 match p1 with 1292 1421 [ Some x1 ⇒ match p2 with 1293 [ Some x2 ⇒ policy_equal _intprogram x1 x21422 [ Some x2 ⇒ policy_equal program x1 x2 1294 1423  _ ⇒ False 1295 1424 ] … … 1297 1426 ]. 1298 1427 1299 lemma pe_refl: ∀program.reflexive ? (policy_equal program).1428 lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program). 1300 1429 #program whd #x whd cases x 1301 1430 [ // … … 1304 1433 qed. 1305 1434 1306 lemma pe_sym: ∀program.symmetric ? (policy_equal program).1435 lemma pe_sym: ∀program.symmetric ? (policy_equal_opt program). 1307 1436 #program whd #x #y #Hxy whd cases y in Hxy; 1308 1437 [ cases x … … 1311 1440 ] 1312 1441  #y' cases x 1313 [ #H @⊥ @(absurd ? H) whd in match (policy_equal ???); @nmk #H destruct (H)1442 [ #H @⊥ @(absurd ? H) whd in match (policy_equal_opt ???); @nmk #H destruct (H) 1314 1443  #x' #H @pe_int_sym @H 1315 1444 ] … … 1317 1446 qed. 1318 1447 1319 lemma pe_trans: ∀program.transitive ? (policy_equal program).1448 lemma pe_trans: ∀program.transitive ? (policy_equal_opt program). 1320 1449 #program whd #x #y #z cases x 1321 1450 [ #Hxy #Hyz >Hxy in Hyz; // … … 1350 1479 1351 1480 lemma pe_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 1352 ∀n.policy_equal program (\snd (pi1 ?? (jump_expansion_internal program n)))1481 ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n))) 1353 1482 (\snd (pi1 ?? (jump_expansion_internal program (S n)))) → 1354 policy_equal program (\snd (pi1 ?? (jump_expansion_internal program (S n))))1483 policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n)))) 1355 1484 (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))). 1356 1485 #program #n #Heq … … 1363 1492 1364 1493 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.l < 2^16).∀n:ℕ. 1365 policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))1494 policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n))) 1366 1495 (\snd (pi1 … (jump_expansion_internal program (S n)))) → 1367 ∀k.k ≥ n → policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))1496 ∀k.k ≥ n → policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n))) 1368 1497 (\snd (pi1 … (jump_expansion_internal program k))). 1369 1498 #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H H Hk k; … … 1379 1508 1380 1509 (* this number monotonically increases over iterations, maximum 2*program *) 1381 let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)1510 let rec measure_int (program: list labelled_instruction) (policy: ppc_pc_map) (acc: ℕ) 1382 1511 on program: ℕ ≝ 1383 1512 match program with 1384 1513 [ nil ⇒ acc 1385  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,00 1386 ,short_jump〉)) with 1387 [ long_jump ⇒ measure_int t policy (acc + 2) 1388  medium_jump ⇒ measure_int t policy (acc + 1) 1389  _ ⇒ measure_int t policy acc 1514  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉)) with 1515 [ None ⇒ measure_int t policy acc 1516  Some j ⇒ match j with 1517 [ long_jump ⇒ measure_int t policy (acc + 2) 1518  medium_jump ⇒ measure_int t policy (acc + 1) 1519  _ ⇒ measure_int t policy acc 1520 ] 1390 1521 ] 1391 1522 ]. … … 1398 1529 [ / by refl/ 1399 1530  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1400 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0, 0,short_jump〉))1531 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉)) 1401 1532 [ normalize nodelta @Hd 1402 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus 1403 @Hd 1533  #x cases x 1534 [ normalize nodelta @Hd 1535 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus 1536 @Hd 1537 ] 1404 1538 ] 1405 1539 ] … … 1412 1546 [ normalize @le_n 1413 1547  #h #t #Hind whd in match (measure_int ???); 1414 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0, 0,short_jump〉))1548 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉)) 1415 1549 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1416 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) 1417 @le_plus [1,3: @Hind 2,4: / by le_n/ ] 1550  #x cases x 1551 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1552 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) 1553 @le_plus [1,3: @Hind 2,4: / by le_n/ ] 1554 ] 1418 1555 ] 1419 1556 ] … … 1421 1558 1422 1559 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.l<2^16. 1423 ∀policy:Σp:jump_expansion_policy. 1424 out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p. 1560 ∀policy:Σp:ppc_pc_map. 1561 out_of_program_none program p ∧ jump_in_policy program p ∧ 1562 policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16. 1425 1563 ∀l.l ≤ program → ∀acc:ℕ. 1426 match \snd (jump_expansion_step program (create_label_map program policy) policy) with1564 match \snd (jump_expansion_step program (create_label_map program) policy) with 1427 1565 [ None ⇒ True 1428 1566  Some p ⇒ measure_int l policy acc ≤ measure_int l p acc … … 1431 1569 [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q pi1; cases q [ //  #x #_ @le_n ] 1432 1570  #h #t #Hind #Hp #acc 1433 lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy))1571 lapply (refl ? (jump_expansion_step program (create_label_map program) policy)) 1434 1572 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 pi1 #c #r cases r 1435 1573 [ / by I/ 1436 1574  #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (t) Hp) 1437 1575 whd in match (measure_int ???); whd in match (measure_int ? x ?); 1438 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,0,short_jump〉) 1439 #z cases z z #x1 #x2 #x3 1440 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,0,short_jump〉) 1441 #z cases z z #y1 #y2 #y3 1442 normalize nodelta #Hj cases Hj 1443 [ cases x3 cases y3 1444 [1,4,5,7,8,9: #H @⊥ @H 1445 2,3,6: #_ normalize nodelta 1446 [1,2: @(transitive_le ? (measure_int t x acc)) 1447 3: @(transitive_le ? (measure_int t x (acc+1))) 1448 ] 1449 [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/] 1450 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1451 ] 1452  #Heq >Heq cases y3 normalize nodelta 1453 [2,3: >measure_plus >measure_plus @le_plus / by le_n/] 1454 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1455 ] 1456 ] 1457 ] 1576 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) 1577 [ #Hj 1578 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (t) ?) Hj) 1579 [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (t) ?) Hj) 1580 [ #j1 normalize nodelta 1581 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉) 1582 #x1 #x2 1583 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,None ?〉) 1584 #y1 #y2 normalize nodelta #Hx #Hy >Hx >Hy normalize nodelta 1585 #Hblerp cases (proj2 ?? Hblerp) cases j1 cases j2 1586 [1,4,5,7,8,9: #H cases H 1587 2,3,6: #_ normalize nodelta 1588 [1,2: @(transitive_le ? (measure_int t x acc)) 1589 3: @(transitive_le ? (measure_int t x (acc+1))) 1590 ] 1591 [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/] 1592 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1593 11,12,13,15,16,17: #H destruct (H) 1594 10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1595 ] 1596  @(transitive_le … Hp) @le_n 1597 ] 1598  @(transitive_le … Hp) @le_n 1599 ] 1600  #Hnj 1601 lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (t) ?) Hnj) 1602 [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) x (t) ?) Hnj) 1603 [3: cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉) 1604 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,None ?〉) 1605 #y1 #y2 #Hy #Hx >Hx >Hy normalize nodelta 1606 #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1607 1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) 1608 2: @(transitive_le … Hp) @le_n 1609 ] 1610 1: @(proj1 ?? (proj1 ?? (pi2 ?? policy))) 1611 2: @(transitive_le … Hp) @le_n 1612 ] 1613 ] 1614 ] 1458 1615 qed. 1459 1616 … … 1475 1632 lemma measure_full: ∀program.∀policy. 1476 1633 measure_int program policy 0 = 2*program → ∀i.i<program → 1477 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,0,short_jump〉)) = long_jump. 1478 #program #policy elim program 1634 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = None ? ∨ 1635 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = Some ? long_jump. 1636 #program #policy elim program 1479 1637 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1480 1638  #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*t) 1481 1639 [ whd in match (measure_int ???) in Hm; 1482 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0, 0,short_jump〉)) in Hm;1640 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉)) in Hm; 1483 1641 normalize nodelta 1484 1642 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ 1485  >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) 1486 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize 1487 >(commutative_plus (t) 0) <plus_O_n <minus_n_O 1488 >plus_n_Sm @le_n 1489  >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) // 1643  #j cases j normalize nodelta 1644 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ 1645  >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) 1646 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize 1647 >(commutative_plus (t) 0) <plus_O_n <minus_n_O 1648 >plus_n_Sm @le_n 1649  >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) // 1650 ] 1490 1651 ] 1491 1652  #Hmt cases (le_to_or_lt_eq … Hi) Hi; 1492 1653 [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi)) 1493 1654  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1494 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0, 0,short_jump〉)) in Hm;1655 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉)) in Hm; 1495 1656 normalize nodelta 1496 [ >Hmt normalize <plus_n_O >(commutative_plus (t) (S (t))) 1497 >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s 1498  >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize 1499 #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s 1500  #_ // 1657 [ #_ %1 @refl 1658  #j cases j normalize nodelta 1659 [ >Hmt normalize <plus_n_O >(commutative_plus (t) (S (t))) 1660 >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s 1661  >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize 1662 #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s 1663  #_ %2 @refl 1664 ] 1501 1665 ] 1502 1666 ]] … … 1505 1669 1506 1670 lemma measure_special: ∀program:(Σl:list labelled_instruction.l < 2^16). 1507 ∀policy:Σp: jump_expansion_policy.1508 out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p.1509 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with1671 ∀policy:Σp:ppc_pc_map. 1672 out_of_program_none program p ∧ jump_in_policy program p ∧ policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16. 1673 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with 1510 1674 [ None ⇒ True 1511  Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal _intprogram policy p ].1512 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy)))1513 cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %);1675  Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal program policy p ]. 1676 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) 1677 cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %); 1514 1678 #p cases p p #ch #pol normalize nodelta cases pol 1515 1679 [ / by I/ … … 1517 1681 @(list_ind ? (λx.x ≤ pi1 ?? program → 1518 1682 measure_int x policy 0 = measure_int x p 0 → 1519 policy_equal _intx policy p) ?? (pi1 ?? program))1683 policy_equal x policy p) ?? (pi1 ?? program)) 1520 1684 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 1521 1685  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) Hi; … … 1523 1687 [ @(transitive_le … Hp) / by / 1524 1688  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 1525 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) 1526 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in Hm; 1527 #x cases x x #x1 #x2 #x3 1528 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉); 1529 #y cases y y #y1 #y2 #y3 1530 cases x3 cases y3 normalize nodelta 1531 [1: #H #_ @H 1532 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1533 lapply (measure_incr_or_equal program policy t ? 0) 1534 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1535 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 1536 5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) 1537 #H #_ @(injective_plus_r … H) 1538 6: >measure_plus >measure_plus 1539 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 1540 #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1541 lapply (measure_incr_or_equal program policy t ? 0) 1542 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1543 9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) 1544 #H #_ @(injective_plus_r … H) 1545 ] 1546  @(le_S_S_to_le … Hi) 1689 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) #Hinc 1690 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) 1691 [ #Hj elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (t) ?) Hj) 1692 [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (t) ?) Hj) 1693 [ #j1 normalize nodelta 1694 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,None ?〉) in Hm Hinc; #x1 #x2 1695 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,None ?〉); #y1 #y2 1696 #Hm #Hinc #Hx #Hy lapply Hm Hm; lapply Hinc Hinc; >Hx >Hy normalize nodelta 1697 cases j1 cases j2 normalize nodelta 1698 [1: / by / 1699 2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1700 lapply (measure_incr_or_equal program policy t ? 0) 1701 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1702 4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 2,4,6: destruct (H2) ] 1703 5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) 1704 #_ #H @(injective_plus_r … H) 1705 6: >measure_plus >measure_plus 1706 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 1707 #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1708 lapply (measure_incr_or_equal program policy t ? 0) 1709 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1710 9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) 1711 #_ #H @(injective_plus_r … H) 1712 ] 1713  @(transitive_le … Hp) @le_n 1714 ] 1715  @(transitive_le … Hp) @le_n 1716 ] 1717  #Hnj lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (t) ?) Hnj) 1718 [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) p (t) ?) Hnj) 1719 [3: cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉) in Hm Hinc; 1720 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd p) 〈0,None ?〉) 1721 #y1 #y2 #Hm #Hinc #Hy #Hx lapply Hm Hm; lapply Hinc Hinc; >Hx >Hy normalize nodelta 1722 #_ / by / 1723 1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) 1724 2: @(transitive_le … Hp) @le_n 1725 ] 1726 1: @(proj1 ?? (proj1 ?? (pi2 ?? policy))) 1727 2: @(transitive_le … Hp) @le_n 1728 ] 1729 ] 1730  @(le_S_S_to_le … Hi) 1547 1731 ] 1548 1732  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1549 1733 whd in match (measure_int ? p ?) in Hm; 1550 1734 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) 1735 (* XXX *) cases daemon 1736 (* change proof for not_jump 1551 1737 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in 1552 1738 Hm; … … 1564 1750 #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1565 1751 lapply (measure_incr_or_equal program policy t ? 0) 1566 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1567 ] 1752 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1753 ] *) 1568 1754 ] 1569 1755 ] … … 1586 1772 1587 1773 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.l < 2^16. 1588 l ≤ program → measure_int l (jump_expansion_start program ) 0 = 0.1774 l ≤ program → measure_int l (jump_expansion_start program (create_label_map program)) 0 = 0. 1589 1775 #l #program elim l 1590 1776 [ // 1591  #h #t #Hind #Hp whd in match (measure_int ???); 1777  #h #t #Hind #Hp cases daemon 1778 1779 (* old proof whd in match (measure_int ???); 1780 cases daemo 1592 1781 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) #Hj 1593 [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (t) ? Hj) 〈0,0,short_jump〉) 1782 [ lapply 1783 (proj1 ?? (pi2 ?? 1784 (jump_expansion_start program (create_label_map program))))) 〈0,None ?〉) 1594 1785 [ normalize nodelta @Hind @le_S_to_le ] 1595 1786 @Hp … … 1602 1793 ] 1603 1794 ] 1604 ] 1795 ]*) 1605 1796 ] 1606 1797 qed. … … 1608 1799 (* the actual computation of the fixpoint *) 1609 1800 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.l < 2^16). 1610 Σp:option jump_expansion_policy.∃n.∀k.n < k →1611 policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p.1801 Σp:option ppc_pc_map.∃n.∀k.n < k → 1802 policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p. 1612 1803 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*program)))) 1804 1805 cases daemon 1806 1807 (* old proof 1613 1808 cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program) 1614 1809 (\snd (pi1 ?? (jump_expansion_internal program k))) 1615 1810 (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*program)) 1811 cases daemon 1616 1812 [ #Hex elim Hex Hex #x #Hx @(ex_intro … x) #k #Hk 1617 1813 @pe_trans … … 1736 1932 @dec_eq_jump_length 1737 1933 ] 1738 ] 1739 qed. 1740 1741 (* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into 1742 * a map from pc to jump_length. This cannot be done earlier because the pc 1743 * changes between iterations. *) 1744 let rec transform_policy (n: nat) (policy: jump_expansion_policy) (acc: BitVectorTrie jump_length 16) on n: 1745 BitVectorTrie jump_length 16 ≝ 1746 match n with 1747 [ O ⇒ acc 1748  S n' ⇒ 1749 match lookup_opt … (bitvector_of_nat 16 n') (\snd policy) with 1750 [ None ⇒ transform_policy n' policy acc 1751  Some x ⇒ let 〈pc,addr,length〉 ≝ x in 1752 transform_policy n' policy (insert … (bitvector_of_nat 16 pc) length acc) 1753 ] 1754 ]. 1934 ] *) 1935 qed. 1755 1936 1756 1937 (* The glue between Policy and Assembly. *) 1757 1938 definition jump_expansion': 1758 1939 ∀program:preamble × (Σl:list labelled_instruction.l < 2^16). 1759 ∀lookup_labels.policy_type lookup_labels≝1760 λprogram.λ lookup_labels.λpc.1761 let policy ≝ 1762 transform_policy (\snd program) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in1763 «bvt_lookup ? ? pc policy long_jump,?».1764 cases daemon (* XXX later *)1765 qed.1940 ℕ → ℕ × (option jump_length) ≝ 1941 λprogram.λppc:ℕ. 1942 let policy ≝ pi1 … (je_fixpoint (\snd program)) in 1943 match policy with 1944 [ None ⇒ 〈0, Some ? long_jump〉 1945  Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉 1946 ].
Note: See TracChangeset
for help on using the changeset viewer.