Changeset 2078


Ignore:
Timestamp:
Jun 14, 2012, 11:44:46 AM (5 years ago)
Author:
sacerdot
Message:

sigma_policy_specification has been
1) strengthened
2) made nicer to see
3) moved to Assembly.ma
4) used into Policy

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2073 r2078  
    768768 #lbl #instr normalize nodelta >add_associative %
    769769qed.
     770
     771definition sigma_policy_specification ≝
     772  λprogram: pseudo_assembly_program.
     773  λsigma: Word → Word.
     774  λpolicy: Word → bool.
     775  ∀ppc: Word. ∀ppc_ok.
     776    let instr_list ≝ \snd program in
     777    let pc ≝ sigma ppc in
     778    let labels ≝ \fst (create_label_cost_map instr_list) in
     779    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
     780    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
     781    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
     782     sigma (zero …) = zero …
     783     ∧
     784      (nat_of_bitvector … ppc ≤ |instr_list| →
     785       next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction)))
     786     ∧       
     787      (  (nat_of_bitvector … ppc < |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc)
     788       ∨ (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
    770789
    771790definition assembly:
  • src/ASM/AssemblyProof.ma

    r2075 r2078  
    14791479    ].
    14801480
    1481 definition sigma_policy_specification ≝
    1482   λprogram: pseudo_assembly_program.
    1483   λsigma: Word → Word.
    1484   λpolicy: Word → bool.
    1485   ∀ppc: Word. ∀ppc_ok.
    1486     let instr_list ≝ \snd program in
    1487     let pc ≝ sigma ppc in
    1488     let labels ≝ \fst (create_label_cost_map instr_list) in
    1489     let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    1490     let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    1491     let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
    1492       And (nat_of_bitvector … ppc ≤ |instr_list| →
    1493         next_pc = add 16 pc (bitvector_of_nat …
    1494           (instruction_size lookup_labels sigma policy ppc instruction)))
    1495        (Or (nat_of_bitvector … ppc < |instr_list| →
    1496          nat_of_bitvector … pc < nat_of_bitvector … next_pc)
    1497         (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
    1498 
    14991481(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
    15001482   function that load the code in memory is correct. The latter is based
  • src/ASM/Policy.ma

    r2059 r2078  
    628628
    629629(* The glue between Policy and Assembly. *)
     630(*CSC: modified to really use the specification in Assembly.ma.
     631  I have modified all that follows in vi without testing it in Matita.
     632  Jaap, please repair it *)
    630633definition jump_expansion':
    631634∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
    632  option (Σsigma:Word → Word × bool.
    633    ∀ppc: Word. ∀ppc_ok.
    634    let pc ≝ \fst (sigma ppc) in
    635    let labels ≝ \fst (create_label_cost_map (\snd program)) in
    636    let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in
    637    let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
    638    let next_pc ≝ \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
    639      And (nat_of_bitvector … ppc ≤ |\snd program| →
    640        next_pc = add ? pc (bitvector_of_nat …
    641          (instruction_size lookup_labels (λx.\fst (sigma x)) (λx.\snd (sigma x)) ppc instruction)))
    642       (Or (nat_of_bitvector … ppc < |\snd program| →
    643         nat_of_bitvector … pc < nat_of_bitvector … next_pc)
    644        (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))) ≝
     635 option (Σsigma_policy:(Word → Word) × (Word → bool).
     636   let 〈sigma,policy〉≝ sigma_policy in
     637   sigma_policy_specification program sigma policy
     638
    645639 λprogram.
    646640  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
     
    648642  [ None ⇒ None ?
    649643  | Some x ⇒ Some ?
    650       «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
    651         〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?»
     644      «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
     645          bitvector_of_nat 16 pc),
     646         (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
     647          jmpeqb jl long_jump)〉,?»
    652648  ].
    653649 #ppc normalize nodelta cases daemon
Note: See TracChangeset for help on using the changeset viewer.