Changeset 1607 for src/ASM/Assembly.ma
- Timestamp:
- Dec 14, 2011, 1:50:23 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r1606 r1607 1135 1135 ] 1136 1136 ] 1137 | >(proj1 ?? (jump_not_in_policy ( eject… program) old_policy (|prefix|) ?))1137 | >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) 1138 1138 [ // 1139 1139 | >prf >p1 >nth_append_second [ <minus_n_n … … 1248 1248 [ >lookup_opt_lookup_miss 1249 1249 [ @refl 1250 | @(proj1 ?? (jump_not_in_policy program ( eject… (jump_expansion_step program p2)) n Hn))1250 | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p2)) n Hn)) 1251 1251 [ @(proj1 ?? (pi2 … (jump_expansion_step program p2))) 1252 1252 | @Hnotjmp 1253 1253 ] 1254 1254 ] 1255 | @(proj1 ?? (jump_not_in_policy program ( eject… (jump_expansion_step program p1)) n Hn))1255 | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p1)) n Hn)) 1256 1256 [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1))) 1257 1257 | @Hnotjmp … … 1312 1312 lemma stupid: 1313 1313 ∀program,n. 1314 eject… (jump_expansion_step program (jump_expansion_internal program n)) =1315 eject… (jump_expansion_internal program (S n)).1314 pi1 … (jump_expansion_step program (jump_expansion_internal program n)) = 1315 pi1 … (jump_expansion_internal program (S n)). 1316 1316 // 1317 1317 qed. … … 1445 1445 policy_equal program policy (jump_expansion_step program policy). 1446 1446 #program #policy lapply (le_n (|program|)) @(list_ind ? 1447 (λx.|x| ≤ |program| → measure_int x ( eject … policy) 0 = measure_int x (eject… (jump_expansion_step program policy)) 0 →1448 policy_equal x ( eject … policy) (eject… (jump_expansion_step program policy)))1447 (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program policy)) 0 → 1448 policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program policy))) 1449 1449 ?? program) 1450 1450 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O … … 1513 1513 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16). 1514 1514 Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p. 1515 #program @( dp …(jump_expansion_internal program (2*|program|)))1515 #program @(mk_Sig …(jump_expansion_internal program (2*|program|))) 1516 1516 @(ex_intro … (2*|program|)) #k #Hk 1517 1517 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k) … … 1584 1584 λprogram.λpc. 1585 1585 let policy ≝ 1586 transform_policy (|\snd program|) ( eject… (je_fixpoint (\snd program))) (Stub ??) in1586 transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in 1587 1587 lookup ? ? pc policy long_jump. 1588 /2 by Stub, dp/1588 /2 by Stub, mk_Sig/ 1589 1589 qed. 1590 1590 … … 1691 1691 1692 1692 lemma eject_policy: ∀p. policy p → policy_type. 1693 #p #pol @( eject… pol)1693 #p #pol @(pi1 … pol) 1694 1694 qed. 1695 1695 … … 1698 1698 definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝ 1699 1699 λp,policy. 1700 match sigma_safe p ( eject… policy) return λr:option (Word → Word). r ≠ None … → Word → Word with1700 match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with 1701 1701 [ None ⇒ λabs. ⊥ 1702 1702 | Some r ⇒ λ_.r] (pi2 … policy). … … 1866 1866 1867 1867 definition construct_costs ≝ 1868 λprogram,pol,ppc,pc,costs,i. eject… (construct_costs' program pol ppc pc costs i).1868 λprogram,pol,ppc,pc,costs,i. pi1 … (construct_costs' program pol ppc pc costs i). 1869 1869 1870 1870 (* … … 1980 1980 And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*) 1981 1981 (ppc' = length … pre)) (*∧ *) 1982 (tech_pc_sigma00 pseudo_program ( eject… pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)1982 (tech_pc_sigma00 pseudo_program (pi1 … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*) 1983 1983 (∀id. occurs_exactly_once id pre → 1984 1984 lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
Note: See TracChangeset
for help on using the changeset viewer.