Changeset 1607 for src/ASM


Ignore:
Timestamp:
Dec 14, 2011, 1:50:23 PM (8 years ago)
Author:
sacerdot
Message:

Porting to new library.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1606 r1607  
    11351135          ]
    11361136        ]
    1137       | >(proj1 ?? (jump_not_in_policy (eject … program) old_policy (|prefix|) ?))
     1137      | >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?))
    11381138        [ //
    11391139        | >prf >p1 >nth_append_second [ <minus_n_n
     
    12481248   [ >lookup_opt_lookup_miss
    12491249     [ @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))
    12511251       [ @(proj1 ?? (pi2 … (jump_expansion_step program p2)))
    12521252       | @Hnotjmp
    12531253       ]
    12541254     ]
    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))
    12561256     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1)))
    12571257     | @Hnotjmp
     
    13121312lemma stupid:
    13131313  ∀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)).
    13161316 //
    13171317qed.
     
    14451445  policy_equal program policy (jump_expansion_step program policy).
    14461446#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)))
    14491449   ?? program)
    14501450 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
     
    15131513definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    15141514  Σ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|)))
    15161516 @(ex_intro … (2*|program|)) #k #Hk
    15171517 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
     
    15841584 λprogram.λpc.
    15851585  let policy ≝
    1586     transform_policy (|\snd program|) (eject … (je_fixpoint (\snd program))) (Stub ??) in
     1586    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
    15871587  lookup ? ? pc policy long_jump.
    1588 /2 by Stub, dp/
     1588/2 by Stub, mk_Sig/
    15891589qed.
    15901590
     
    16911691
    16921692lemma eject_policy: ∀p. policy p → policy_type.
    1693  #p #pol @(eject … pol)
     1693 #p #pol @(pi1 … pol)
    16941694qed.
    16951695
     
    16981698definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
    16991699 λp,policy.
    1700   match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
     1700  match sigma_safe p (pi1 … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    17011701   [ None ⇒ λabs. ⊥
    17021702   | Some r ⇒ λ_.r] (pi2 … policy).
     
    18661866
    18671867definition 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).
    18691869
    18701870(*
     
    19801980              And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
    19811981                (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'〉)) (*∧*)
    19831983                (∀id. occurs_exactly_once id pre →
    19841984                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
  • src/ASM/AssemblyProof.ma

    r1484 r1607  
    13141314  ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
    13151315               
    1316 
    1317 notation < "❰ x ❱" with precedence 90 for @{'dp $x $y }.
    1318 interpretation "dp" 'dp x y = (dp x y).
    1319 
    13201316lemma fetch_assembly_pseudo':
    13211317 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
Note: See TracChangeset for help on using the changeset viewer.