 Timestamp:
 May 10, 2012, 10:35:18 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1931 r1932 1342 1342 ] (refl … z) 1343 1343 ].*) 1344 1344 1345 1345 1346 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ) … … 1353 1354 (jump_in_policy program x)) 1354 1355 (policy_isize_sum program (create_label_map program) x)) 1356 1355 1357 (\fst x < 2^16) 1356 1358 ]) ≝ … … 1799 1801 (* the actual computation of the fixpoint *) 1800 1802 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.l < 2^16). 1801 Σp:option ppc_pc_map.∃n.∀k.n < k → 1802 policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p. 1803 Σp:option ppc_pc_map. 1804 And (match p with 1805 [ None ⇒ True 1806  Some pol ⇒ And (And (And (And ( 1807 (out_of_program_none program pol)) 1808 (jump_in_policy program pol)) 1809 (policy_isize_sum program (create_label_map program) pol)) 1810 (policy_safe program (create_label_map program) pol)) 1811 (policy_compact program (create_label_map program) pol) 1812 ]) 1813 (∃n.∀k.n < k → 1814 policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p). 1803 1815 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*program)))) 1804 1805 1816 cases daemon 1806 1817 … … 1938 1949 definition jump_expansion': 1939 1950 ∀program:preamble × (Σl:list labelled_instruction.l < 2^16). 1940 ℕ → ℕ × (option jump_length) ≝ 1941 λprogram.λppc:ℕ. 1951 Σf:ℕ → ℕ × (option jump_length). 1952 ∀ppc.match je_fixpoint (\snd program) with 1953 [ None ⇒ True 1954  Some pol ⇒ \fst (f ppc) + 1955 (instruction_size_sigma (create_label_map (\snd program)) pol (bitvector_of_nat ? (\fst (f ppc))) 1956 (\snd (nth ppc ? (\snd program) 〈None ?, Comment []〉))) 1957 = \fst (f (S ppc)) 1958 ] ≝ 1959 λprogram.λppc:ℕ. 1942 1960 let policy ≝ pi1 … (je_fixpoint (\snd program)) in 1943 1961 match policy with … … 1945 1963  Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉 1946 1964 ]. 1965 cases daemon 1966 qed.
Note: See TracChangeset
for help on using the changeset viewer.