Changeset 987 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 16, 2011, 6:08:12 PM (8 years ago)
Author:
sacerdot
Message:

Real parameterization over the policy.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r985 r987  
    656656    jump_expansion_policy_internal program old_labels old_policy in
    657657    jump_expansion_internal n' program new_labels new_policy ].
    658          
    659 definition jump_expansion ≝
    660  λpc.λprogram.
     658
     659definition policy_type ≝ Word → jump_length.
     660
     661definition jump_expansion': pseudo_assembly_program → policy_type ≝
     662 λprogram.λpc.
    661663  let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
    662664  lookup ? ? pc policy long_jump.
     
    664666definition assembly_1_pseudoinstruction ≝
    665667  λprogram: pseudo_assembly_program.
     668  λjump_expansion: policy_type.
    666669  λppc: Word.
    667670  λpc: Word.
     
    669672  λlookup_datalabels.
    670673  λi.
    671   let expansion ≝ jump_expansion ppc program in
     674  let expansion ≝ jump_expansion ppc in
    672675    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
    673676    [ None ⇒ None ?
     
    681684definition construct_costs ≝
    682685  λprogram.
     686  λjump_expansion: policy_type.
    683687  λpseudo_program_counter: nat.
    684688  λprogram_counter: nat.
     
    695699    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
    696700    let pc_delta_assembled ≝
    697       assembly_1_pseudoinstruction program ppc_bv pc_bv
     701      assembly_1_pseudoinstruction program jump_expansion ppc_bv pc_bv
    698702        lookup_labels lookup_datalabels i
    699703    in
     
    709713   program counters. It is at the heart of the proof. *)
    710714(*CSC: code taken from build_maps *)
    711 definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    712  λinstr_list.λl:list labelled_instruction.
     715definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     716 λinstr_list.
     717 λjump_expansion: policy_type.
     718 λl:list labelled_instruction.
    713719  foldl ??
    714720   (λt,i.
     
    719725         let 〈program_counter, sigma_map〉 ≝ pc_map in
    720726         let 〈label, i〉 ≝ i in
    721           match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
     727          match construct_costs instr_list jump_expansion ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
    722728           [ None ⇒ None ?
    723729           | Some pc_ignore ⇒
     
    726732       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
    727733
    728 definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
    729  ≝ λprog.sigma00 prog (\snd prog).
    730 
    731 definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
    732  λprogram,instr_list.
    733   match sigma00 program instr_list with
     734definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
     735 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
     736
     737definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
     738 λprogram,jump_expansion,instr_list.
     739  match sigma00 program jump_expansion instr_list with
    734740   [ None ⇒ None …
    735741   | Some result ⇒
     
    738744       Some … 〈ppc,pc〉 ].
    739745
    740 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝
    741  λinstr_list.
    742   match sigma0 instr_list with
     746definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
     747 λinstr_list,jump_expansion.
     748  match sigma0 instr_list jump_expansion with
    743749  [ None ⇒ None ?
    744750  | Some result ⇒
     
    752758(* stuff about policy *)
    753759
    754 axiom policy_ok: ∀p. sigma_safe p ≠ None ….
    755 
    756 definition sigma: pseudo_assembly_program → Word → Word ≝
    757  λp.
    758   match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
     760definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
     761
     762definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
     763
     764lemma eject_policy: ∀p. policy p → policy_type.
     765 #p #pol @(eject … pol)
     766qed.
     767
     768coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
     769
     770definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
     771 λp,policy.
     772  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    759773   [ None ⇒ λabs. ⊥
    760    | Some r ⇒ λ_.r] (policy_ok p).
     774   | Some r ⇒ λ_.r] (sig2 … policy).
    761775 cases abs //
    762776qed.
    763777
    764 example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
     778example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
    765779 cases daemon.
    766780qed.
    767781
    768782axiom construct_costs_sigma:
    769  ∀p,ppc,pc,pc',costs,costs',i.
    770   bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
    771    Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
    772     bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
     783 ∀p.∀pol:policy p.∀ppc,pc,pc',costs,costs',i.
     784  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
     785   Some … 〈pc',costs'〉 = construct_costs p pol ppc pc (λx.zero 16) (λx.zero 16) costs i →
     786    bitvector_of_nat ? pc' = sigma p pol (bitvector_of_nat 16 (S ppc)).
    773787
    774788axiom tech_pc_sigma00_append_Some:
    775  ∀program,prefix,costs,label,i,pc',code,ppc,pc.
    776   tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
    777    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
    778     tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
     789 ∀program.∀pol:policy program.∀prefix,costs,label,i,pc',code,ppc,pc.
     790  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
     791   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
     792    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
    779793
    780794axiom tech_pc_sigma00_append_None:
    781  ∀program,prefix,i,ppc,pc,costs.
    782   tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
    783    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     795 ∀program.∀pol:policy program.∀prefix,i,ppc,pc,costs.
     796  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
     797   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
    784798    → False.
    785799
    786800definition build_maps ≝
    787   λpseudo_program.
     801  λpseudo_program.λpol:policy pseudo_program.
    788802  let result ≝
    789803   foldl_strong
     
    793807      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    794808      let 〈pc',costs〉 ≝ pc_costs in
    795        bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
     809       bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc') ∧
    796810       ppc' = length … pre ∧
    797        tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
     811       tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉 ∧
    798812       ∀id. occurs_exactly_once id pre →
    799         lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
     813        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))
    800814    (\snd pseudo_program)
    801815    (λprefix,i,tl,prf,t.
     
    812826         ]
    813827       in
    814          match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
     828         match construct_costs pseudo_program pol ppc pc (λx. zero ?) (λx. zero ?) costs i' with
    815829         [ None ⇒
    816830            let dummy ≝ 〈labels,ppc_pc_costs〉 in
     
    858872*)
    859873
    860 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    861   λp.
     874definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
     875  λp,pol.
    862876    let 〈preamble, instr_list〉 ≝ p in
    863     let 〈labels,costs〉 ≝ build_maps p in
     877    let 〈labels,costs〉 ≝ build_maps p pol in
    864878    let datalabels ≝ construct_datalabels preamble in
    865879    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
     
    871885          let 〈pc, ppc_y〉 ≝ lst in
    872886          let 〈ppc, y〉 ≝ ppc_y in
    873           let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
     887          let x ≝ assembly_1_pseudoinstruction p pol ppc pc lookup_labels lookup_datalabels (\snd x) in
    874888          match x with
    875889          [ None ⇒ None ?
Note: See TracChangeset for help on using the changeset viewer.