Changeset 1934 for src/ASM/Policy.ma
 Timestamp:
 May 10, 2012, 3:37:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1933 r1934 14 14 (* Internal types *) 15 15 16 (* label_map: identifier ↦ pseudo program counter *)17 definition label_map ≝ identifier_map ASMTag ℕ.18 19 16 (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *) 20 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × (option jump_length)) 16).17 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × bool) 16). 21 18 22 19 (* The different properties that we want/need to prove at some point *) … … 72 69 ]. 73 70 74 definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝71 (*definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝ 75 72 λprefix.λsigma. 76 73 ∀i:ℕ.i < prefix → 77 74 iff (is_jump (nth i ? prefix 〈None ?, Comment []〉)) 78 75 (∃x:jump_length. 79 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x). 76 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).*) 80 77 81 78 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *) … … 111 108 λprogram.λop.λp. 112 109 ∀i.i < program → 113 let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0, None ?〉 in114 let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0, None ?〉 in115 opc ≤ pc ∧116 match ox with110 let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,false〉 in 111 let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,false〉 in 112 opc ≤ pc. 113 (*∧ match ox with 117 114 [ Some oj ⇒ 118 115 match x with … … 121 118 ] 122 119  _ ⇒ True 123 ]. 120 ].*) 121 122 (* 124 123 125 124 (* Policy safety *) 126 definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝125 (*definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ 127 126 λprogram.λlabels.λsigma. 128 127 ∀i.i < program → 129 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0, None ?〉 in128 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,false〉 in 130 129 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in 131 130 ∀dest.is_jump_to instr dest → 132 131 let paddr ≝ lookup_def … labels dest 0 in 133 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0, None ?〉) in132 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,false〉) in 134 133 match j with 135 134 [ None ⇒ True … … 147 146  long_jump ⇒ True 148 147 ] 149 ]. 148 ].*) 150 149 151 150 (* this is the instruction size as determined by the distance from origin to destination *) … … 291 290 %2 @nmk #H destruct (H) 292 291 qed. 293 294 (* Labels *)295 definition is_label ≝296 λx:labelled_instruction.λl:Identifier.297 let 〈lbl,instr〉 ≝ x in298 match lbl with299 [ Some l' ⇒ l' = l300  _ ⇒ False301 ].302 303 lemma label_does_not_occur:304 ∀i:ℕ.∀p:list labelled_instruction.∀l:Identifier.305 is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.306 #i #p #l generalize in match i; elim p307 [ #i >nth_nil #H cases H308  #h #t #IH #i cases i i309 [ cases h #hi #hp cases hi310 [ normalize #H cases H311  #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);312 whd in Heq; >Heq313 >eq_identifier_refl / by refl/314 ]315  #i #H whd in match (does_not_occur ????);316 whd in match (instruction_matches_identifier ????);317 cases h #hi #hp cases hi normalize nodelta318 [ @(IH i) @H319  #l' @eq_identifier_elim320 [ normalize / by /321  normalize #_ @(IH i) @H322 ]323 ]324 ]325 ]326 qed.327 292 328 293 definition policy_isize_sum ≝ … … 343 308 lookup ?? labels l = Some ? i 344 309 ) ≝ 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 / 370 ] 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 376  @le_n 377 ] 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 389 ] 310 λprogram. 311 390 312 qed. 391 313 … … 1946 1868 ] *) 1947 1869 qed. 1870 *) 1948 1871 1949 1872 (* The glue between Policy and Assembly. *) 1950 1873 definition jump_expansion': 1951 1874 ∀program:preamble × (Σl:list labelled_instruction.l < 2^16). 1952 Σf:ℕ → ℕ × (option jump_length). 1953 ∀ppc.match je_fixpoint (\snd program) with 1954 [ None ⇒ True 1955  Some pol ⇒ \fst (f ppc) + 1956 (instruction_size_sigma (create_label_map (\snd program)) pol (bitvector_of_nat ? (\fst (f ppc))) 1957 (\snd (nth ppc ? (\snd program) 〈None ?, Comment []〉))) 1958 = \fst (f (S ppc)) 1959 ] ≝ 1875 option (Σsigma:Word → Word × bool. 1876 ∀ppc. 1877 \snd 1878 (half_add ? 1879 (\fst (sigma ppc)) 1880 (bitvector_of_nat ? 1881 (instruction_size 1882 (λid. bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) id 0)) 1883 sigma ppc (\fst (fetch_pseudo_instruction (\snd program) ppc))))) 1884 = \fst (sigma (\snd (half_add ? ppc (bitvector_of_nat ? 1))))) 1885 ≝ ?. 1886 (* 1960 1887 λprogram.λppc:ℕ. 1961 1888 let policy ≝ pi1 … (je_fixpoint (\snd program)) in … … 1963 1890 [ None ⇒ 〈0, Some ? long_jump〉 1964 1891  Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉 1965 ]. 1892 ].*) 1966 1893 cases daemon 1967 1894 qed.
Note: See TracChangeset
for help on using the changeset viewer.