Changeset 3096 for src/ASM/Interpret2.ma

Timestamp:

Apr 5, 2013, 6:04:14 PM (7 years ago)

Author:

tranquil

Message:

preliminary work on closing correctness.ma

File:

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

src/ASM/Interpret2.ma

@@ -157 +157 @@
    (λst. return (execute_1_pseudo_instruction' … addr_of_label addr_of_symbol sigma policy st))
    (initialise_status … c).
+
+definition ASM_status:
+ ∀prog:pseudo_assembly_program.
+ ∀sigma,policy.abstract_status ≝
+  λc,sigma,policy.
+  let label_map ≝ \fst (create_label_cost_map (code … c)) in
+  let symbol_map ≝ construct_datalabels (preamble … c) in
+  let addr_of_label ≝ λx.bitvector_of_nat ? (lookup_def … label_map x 0) in
+  let addr_of_symbol ≝ λx.lookup_def … symbol_map x (addr_of_label x) in
+  ASM_abstract_status c addr_of_label addr_of_symbol sigma policy.
+