 Timestamp:
 May 14, 2012, 6:02:20 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1934 r1942 1209 1209 qed. 1210 1210 1211 (*theorem build_maps_ok:1212 ∀pseudo_program .∀sigma:Word → Word.1213 let 〈labels, costs〉 ≝ build_maps pseudo_program sigmain1211 theorem create_label_cost_map_ok: 1212 ∀pseudo_program: pseudo_assembly_program. 1213 let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in 1214 1214 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 1215 lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id). 1216 #pseudo_program #sigma @(pi2 … (build_maps0 … sigma)) 1217 qed.*) 1215 bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id. 1216 #pseudo_program 1217 cases (create_label_cost_map (\snd pseudo_program)) * #label_map #cost_map 1218 normalize nodelta elim (\snd pseudo_program) 1219 [1: 1220 #_ #id #absurd normalize in absurd; cases absurd 1221 2: 1222 #hd #tl #inductive_hypothesis #H #id 1223 whd in match (occurs_exactly_once ????); 1224 whd in ⊢ (? → ???%); 1225 whd in match (index_of ???); 1226 inversion (instruction_matches_identifier ????) normalize nodelta 1227 [1: 1228 whd in ⊢ (??%? → ?); #G 1229 lapply (H 0 ? id ??) 1230 [1: 1231 normalize cases hd in G; #lbl #instr normalize 1232 cases lbl normalize try (#absurd destruct(absurd) @I) 1233 #id' change with (eq_identifier ??? = true → ?) 1234 @(eq_identifier_elim ? ? id id') #assm 1235 [1: 1236 // 1237 2: 1238 lapply (eq_identifier_false … assm) 1239 check eq_identifier 1240 #absurd1 >eq_identifier_sym >absurd1 #absurd2 destruct(absurd2) 1241 ] 1242 2: 1243 3: 1244 normalize @le_S_S // 1245 4: 1246 #H whd in match (lookup_def ?????); 1247 >H normalize nodelta #_ % 1248 ] 1249 2: 1250 1251 ] 1252 cases daemon 1253 qed. 1218 1254 1219 1255 definition assembly: 
src/ASM/Policy.ma
r1940 r1942 1665 1665 qed. 1666 1666 1667 include alias "arithmetics/nat.ma". 1668 include alias "basics/logic.ma". 1669 1670 check create_label_cost_map 1671 1667 1672 (* The glue between Policy and Assembly. *) 1668 1673 definition jump_expansion': 1669 1674 ∀program:preamble × (Σl:list labelled_instruction.l < 2^16). 1670 1675 option (Σsigma:Word → Word × bool. 1671 ∀ppc:ℕ. 1672 And (ppc ≤ (\snd program) → 1673 \snd 1674 (half_add ? 1675 (\fst (sigma (bitvector_of_nat 16 ppc))) 1676 (bitvector_of_nat ? 1677 (instruction_size 1678 (λid. bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) id 0)) 1679 sigma (bitvector_of_nat ? ppc) 1680 (\fst (fetch_pseudo_instruction (\snd program) (bitvector_of_nat ? ppc)))))) 1681 = (* \fst (sigma (\snd (half_add ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? 1)))) *) 1682 \fst (sigma (bitvector_of_nat ? (S ppc)))) 1683 (ppc < (\snd program) → 1684 Or (lt_u ? (\fst (sigma (bitvector_of_nat ? ppc))) (\fst (sigma (bitvector_of_nat ? (S ppc)))) = true) 1685 (And (S ppc = (\snd program)) (\fst (sigma (bitvector_of_nat ? (S ppc))) = (zero 16)))) 1686 ) 1687 ≝ λprogram.? (* 1688 let policy ≝ pi1 … (je_fixpoint (\snd program)) in 1689 match policy with 1690 [ None ⇒ None ? 1691  Some x ⇒ Some ? 1692 «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 1693 〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?» 1694 ]*). 1676 ∀ppc: Word. 1677 let pc ≝ \fst (sigma ppc) in 1678 let labels ≝ \fst (create_label_cost_map (\snd program)) in 1679 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in 1680 let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in 1681 let next_pc ≝ \fst (sigma (add … ppc (bitvector_of_nat ? 1))) in 1682 (nat_of_bitvector … ppc ≤ \snd program → 1683 next_pc = add … pc (bitvector_of_nat … (instruction_size lookup_labels sigma ppc instruction))) 1684 ∧ 1685 ((nat_of_bitvector … ppc < \snd program → 1686 nat_of_bitvector … pc < nat_of_bitvector … next_pc) 1687 ∨ 1688 (nat_of_bitvector … ppc = \snd program → next_pc = (zero …)))). 1695 1689 cases daemon 1696 1690 qed.
Note: See TracChangeset
for help on using the changeset viewer.