Changeset 840


Ignore:
Timestamp:
May 25, 2011, 1:57:55 PM (8 years ago)
Author:
sacerdot
Message:

sigma defined

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r837 r840  
    586586  λi.
    587587  match i with
    588   [ Comment comment ⇒ Some ? 〈program_counter, costs〉
    589   | Cost cost ⇒
     588  [ Cost cost ⇒
    590589    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    591590      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
  • src/ASM/AssemblyProof.ma

    r839 r840  
    11include "ASM/Assembly.ma".
    22include "ASM/Interpret.ma".
     3
     4(* This establishes the correspondence between pseudo program counters and
     5   program counters. It is at the heart of the proof. *)
     6(*CSC: code taken from build_maps *)
     7definition sigma: pseudo_assembly_program → option (Word → Word) ≝
     8 λinstr_list.
     9  let result ≝ foldl ?(*(option (nat × (nat × (BitVectorTrie Word 16))))*) ?
     10    (λt. λi.
     11       match t with
     12       [ None ⇒ None ?
     13       | Some ppc_pc_map ⇒
     14         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     15         let 〈program_counter, sigma_map〉 ≝ pc_map in
     16         let 〈label, i〉 ≝ i in
     17          match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
     18           [ None ⇒ None ?
     19           | Some pc_ignore ⇒
     20              let 〈pc,ignore〉 ≝ pc_ignore in
     21              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
     22       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list) in
     23  match result with
     24  [ None ⇒ None ?
     25  | Some result ⇒
     26    let 〈ppc,pc_sigma_map〉 ≝ result in
     27    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
     28      if gtb pc (2^16) then
     29        None ?
     30      else
     31        Some ? (λx.lookup ?? x sigma_map (zero …))
     32  ].
     33
    334
    435let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
Note: See TracChangeset for help on using the changeset viewer.