Ignore:
Timestamp:
Jun 14, 2012, 11:44:46 AM (8 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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.