Changeset 1942 for src/ASM/Policy.ma
 Timestamp:
 May 14, 2012, 6:02:20 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.