Changeset 840 for src/ASM/AssemblyProof.ma

Timestamp:

May 25, 2011, 1:57:55 PM (10 years ago)

Author:

sacerdot

Message:

sigma defined

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -1 +1 @@
 include "ASM/Assembly.ma".
 include "ASM/Interpret.ma".
+
+(* This establishes the correspondence between pseudo program counters and
+   program counters. It is at the heart of the proof. *)
+(*CSC: code taken from build_maps *)
+definition sigma: pseudo_assembly_program → option (Word → Word) ≝
+ λinstr_list.
+  let result ≝ foldl ?(*(option (nat × (nat × (BitVectorTrie Word 16))))*) ?
+    (λt. λi.
+       match t with
+       [ None ⇒ None ?
+       | Some ppc_pc_map ⇒
+         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
+         let 〈program_counter, sigma_map〉 ≝ pc_map in
+         let 〈label, i〉 ≝ i in
+          match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
+           [ None ⇒ None ?
+           | Some pc_ignore ⇒
+              let 〈pc,ignore〉 ≝ pc_ignore in
+              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
+       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list) in
+  match result with
+  [ None ⇒ None ?
+  | Some result ⇒
+    let 〈ppc,pc_sigma_map〉 ≝ result in
+    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
+      if gtb pc (2^16) then
+        None ?
+      else
+        Some ? (λx.lookup ?? x sigma_map (zero …))
+  ].
+
 
 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)