 Timestamp:
 Dec 14, 2011, 1:50:23 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 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))) 
src/ASM/AssemblyProof.ma
r1484 r1607 1314 1314 ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2. 1315 1315 1316 1317 notation < "❰ x ❱" with precedence 90 for @{'dp $x $y }.1318 interpretation "dp" 'dp x y = (dp x y).1319 1320 1316 lemma fetch_assembly_pseudo': 1321 1317 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
Note: See TracChangeset
for help on using the changeset viewer.