From 17b3c7a49f0ce7b7aaac4e63992c4d53c1cbab30 Mon Sep 17 00:00:00 2001
From: Scott Owens <sowens@fb.com>
Date: Fri, 27 Sep 2019 02:15:22 -0700
Subject: [PATCH] [sledge sem] Add top-level llair semantics

Summary:
Give the llair semantics observable side effects (writes to global
variables) and a semantic function mirroring the LLVM semantics. Start
sketching out the LLVM/llair translation equivalence proof in a top-down
way from the obvious statement of equality of the semantics.

Reviewed By: jberdine

Differential Revision: D17399654

fbshipit-source-id: 2170678a8
---
 sledge/semantics/Holmakefile                  |   2 +-
 sledge/semantics/llairScript.sml              |  85 +++--
 sledge/semantics/llair_propScript.sml         |  18 +-
 sledge/semantics/llvmScript.sml               |  16 -
 sledge/semantics/llvm_liveScript.sml          |   2 +-
 sledge/semantics/llvm_propScript.sml          |  12 -
 sledge/semantics/llvm_to_llairScript.sml      |   4 +-
 sledge/semantics/llvm_to_llair_propScript.sml | 302 +++++++++++++++---
 sledge/semantics/miscScript.sml               |  52 ++-
 9 files changed, 385 insertions(+), 108 deletions(-)

diff --git a/sledge/semantics/Holmakefile b/sledge/semantics/Holmakefile
index b5926bceb..59b9f184b 100644
--- a/sledge/semantics/Holmakefile
+++ b/sledge/semantics/Holmakefile
@@ -7,7 +7,7 @@ all: $(DEFAULT_TARGETS)
 
 HOLHEAP = heap
 EXTRA_CLEANS = heap
-OBJNAMES = wordsLib.uo intLib.uo stringLib.uo integer_wordLib.uo finite_mapLib.uo alistLib.uo
+OBJNAMES = wordsLib.uo intLib.uo stringLib.uo integer_wordLib.uo finite_mapLib.uo alistLib.uo pathTheory.uo
 DEPS = $(patsubst %,$(dprot $(SIGOBJ)/%),$(OBJNAMES))
 $(HOLHEAP): $(DEPS)
 	$(protect $(HOLDIR)/bin/buildheap) -o $@ $(OBJNAMES)
diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index 090c75056..254fc96d9 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -94,6 +94,7 @@ Datatype:
   | Return exp
   | Throw exp
   | Unreachable
+  | Exit
 End
 
 Datatype:
@@ -116,7 +117,7 @@ Datatype:
 End
 
 Datatype:
-  llair = <| globals : global list; functions : (string, func) alist |>
+  llair = <| glob_init : global list; functions : (string, func) alist |>
 End
 
 (* ----- Semantic states ----- *)
@@ -139,10 +140,11 @@ End
 Datatype:
   state =
     <| bp : label; (* Pointer to the next block to execute *)
-       globals : var |-> word64;
+       glob_addrs : var |-> num;
        locals : var |-> v;
        stack : frame list;
-       heap : unit heap |>
+       heap : unit heap;
+       status : trace_type |>
 End
 
 (* Assume that all pointers can fit in 64 bits *)
@@ -344,12 +346,17 @@ Definition update_results_def:
   update_results xvs s = s with locals := s.locals |++ xvs
 End
 
+Inductive get_obs:
+  (∀s ptr bytes x. flookup s.glob_addrs x = Some ptr ⇒ get_obs s ptr bytes (W x bytes)) ∧
+  (∀s ptr bytes. ptr ∉ FRANGE s.glob_addrs ⇒ get_obs s ptr bytes Tau)
+End
+
 Inductive step_inst:
   (∀s ves rs.
     list_rel (eval_exp s) (map snd ves) rs
     ⇒
     step_inst s
-    (Move ves)
+    (Move ves) Tau
     (update_results (map (λ(v,r). (v, r)) (zip (map fst ves, rs))) s)) ∧
 
   (∀s x t e size ptr freeable interval bytes.
@@ -359,19 +366,20 @@ Inductive step_inst:
    bytes = map snd (get_bytes s.heap interval)
    ⇒
    step_inst s
-    (Load (Var_name x t) e size)
+    (Load (Var_name x t) e size) Tau
     (update_results [(Var_name x t, fst (bytes_to_llair_value t bytes))] s)) ∧
 
-  (∀s e1 e2 size ptr bytes freeable interval r.
+  (∀s e1 e2 size ptr bytes freeable interval r obs.
    eval_exp s e1 (FlatV ptr) ∧
    eval_exp s e2 r ∧
    interval = Interval freeable (i2n ptr) (i2n ptr + size) ∧
    is_allocated interval s.heap ∧
    bytes = llair_value_to_bytes r ∧
-   length bytes = size
+   length bytes = size ∧
+   get_obs s (i2n ptr) bytes obs
    ⇒
    step_inst s
-     (Store e1 e2 size)
+     (Store e1 e2 size) obs
      (s with heap := set_bytes () bytes (i2n ptr) s.heap)) ∧
 
   (* TODO memset *)
@@ -387,7 +395,7 @@ Inductive step_inst:
    bytes = map snd (get_bytes s.heap src_interval)
    ⇒
    step_inst s
-    (Memcpy e1 e2 e3)
+    (Memcpy e1 e2 e3) Tau
     (s with heap := set_bytes () bytes (i2n dest_ptr) s.heap)) ∧
 
   (* TODO memmove *)
@@ -399,21 +407,21 @@ Inductive step_inst:
    nfits ptr pointer_size
    ⇒
    step_inst s
-     (Alloc v e1 e2)
+     (Alloc v e1 e2) Tau
      (update_results [(v, FlatV (n2i ptr pointer_size))] (s with heap := new_h))) ∧
 
   (∀s e ptr.
    eval_exp s e (FlatV ptr)
    ⇒
    step_inst s
-     (Free e)
+     (Free e) Tau
      (s with heap := deallocate [A (i2n ptr)] s.heap)) ∧
 
   (∀s x t nondet.
    value_type t nondet
    ⇒
    step_inst s
-     (NondetI (Var_name x t))
+     (NondetI (Var_name x t)) Tau
      (update_results [(Var_name x t, nondet)] s))
 
 End
@@ -445,7 +453,7 @@ Inductive step_term:
    step_term prog s
      (Call v (Lab_name fname bname) es t ret1 ret2)
      <| bp := Lab_name fname bname;
-        globals := s.globals;
+        glob_addrs := s.glob_addrs;
         locals := alist_to_fmap (zip (f.params, vals));
         stack :=
           <| ret := ret1;
@@ -461,11 +469,12 @@ Inductive step_term:
    step_term prog s
      (Return e)
      <| bp := top.ret;
-        globals := s.globals;
+        glob_addrs := s.glob_addrs;
         locals := top.saved_locals |+ (top.ret_var, r);
         stack := rest;
-        heap := s.heap |>)
+        heap := s.heap |>) ∧
 
+  (∀prog s. step_term prog s Exit (s with status := Complete))
   (* TODO Throw *)
 
 End
@@ -477,24 +486,46 @@ Inductive step_block:
   (∀prog s1 t s2.
    step_term prog s1 t s2
    ⇒
-   step_block prog s1 [] t s2) ∧
+   step_block prog s1 [] [] t s2) ∧
+
 
-  (∀prog s1 i is t s2 s3.
-   step_inst s1 i s2 ∧
-   step_block prog s2 is t s3
+  (∀prog s1 i1 i2 l1 is t s2.
+   step_inst s1 i1 l1 s2 ∧
+   (¬?l2 s3. step_inst s2 i2 l2 s3)
    ⇒
-   step_block prog s1 (i::is) t s3)
+   step_block prog s1 (i1::i2::is) [l1] t (s2 with status := Stuck)) ∧
+
+  (∀prog s1 i l is ls t s2 s3.
+   step_inst s1 i l s2 ∧
+   step_block prog s2 is ls t s3
+   ⇒
+   step_block prog s1 (i::is) (l::ls) t s3)
+
+End
 
+Inductive get_block:
+  ∀prog bp fname bname f b.
+    bp = Lab_name fname bname ∧
+    alookup prog.functions fname = Some f ∧
+    alookup f.cfg bp = Some b
+    ⇒
+    get_block prog bp b
 End
 
 Inductive step:
-  (∀prog s fname bname f b s'.
-   s.bp = Lab_name fname bname ∧
-   alookup prog.functions fname = Some f ∧
-   alookup f.cfg s.bp = Some b ∧
-   step_block prog s b.cmnd b.term s'
-   ⇒
-   step prog s s')
+  ∀prog s b ls s'.
+    get_block prog s.bp b ∧
+    step_block prog s b.cmnd ls b.term s' ∧
+    s.status = Partial
+    ⇒
+    step prog s ls s'
+End
+
+Definition sem_def:
+  sem p s1 =
+    { l1 | ∃path l2. l1 ∈ observation_prefixes ((last path).status, flat l2) ∧
+           toList (labels path) = Some l2 ∧
+           finite path ∧ okpath (step p) path ∧ first path = s1 }
 End
 
 export_theory ();
diff --git a/sledge/semantics/llair_propScript.sml b/sledge/semantics/llair_propScript.sml
index 456d92251..9f1b738fc 100644
--- a/sledge/semantics/llair_propScript.sml
+++ b/sledge/semantics/llair_propScript.sml
@@ -8,7 +8,7 @@
 (* Properties of the llair model *)
 
 open HolKernel boolLib bossLib Parse;
-open arithmeticTheory integerTheory integer_wordTheory wordsTheory;
+open arithmeticTheory integerTheory integer_wordTheory wordsTheory listTheory;
 open settingsTheory miscTheory llairTheory;
 
 new_theory "llair_prop";
@@ -138,4 +138,20 @@ Proof
     rw [w2i_n2w_pos])
 QED
 
+Theorem eval_exp_ignores_lem:
+  ∀s1 e v. eval_exp s1 e v ⇒ ∀s2. s1.locals = s2.locals ⇒ eval_exp s2 e v
+Proof
+  ho_match_mp_tac eval_exp_ind >>
+  rw [] >> simp [Once eval_exp_cases] >>
+  TRY (qexists_tac `vals` >> rw [] >> fs [LIST_REL_EL_EQN] >> NO_TAC) >>
+  TRY (fs [LIST_REL_EL_EQN] >> NO_TAC) >>
+  metis_tac []
+QED
+
+Theorem eval_exp_ignores:
+  ∀s1 e v s2. s1.locals = s2.locals ⇒ (eval_exp s1 e v ⇔ eval_exp s2 e v)
+Proof
+  metis_tac [eval_exp_ignores_lem]
+QED
+
 export_theory ();
diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 09f8484f2..6fc3d9244 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -178,15 +178,6 @@ Datatype:
        heap : bool heap |>
 End
 
-(* Labels for the transitions to make externally observable behaviours apparent.
- * For now, we'll consider this to be writes to global variables.
- * *)
-Datatype:
-  obs =
-  | Tau
-  | W glob_var (word8 list)
-End
-
 (* ----- Things about types ----- *)
 
 (* Given a number n that fits into pointer_size number of bytes, create the
@@ -671,13 +662,6 @@ Inductive step:
   step p s l s'
 End
 
-Datatype:
-  trace_type =
-  | Stuck
-  | Complete
-  | Partial
-End
-
 Definition get_observation_def:
   get_observation prog last_s =
     if get_instr prog last_s.ip Exit then
diff --git a/sledge/semantics/llvm_liveScript.sml b/sledge/semantics/llvm_liveScript.sml
index 1db0d44fd..76a9d069d 100644
--- a/sledge/semantics/llvm_liveScript.sml
+++ b/sledge/semantics/llvm_liveScript.sml
@@ -20,7 +20,7 @@ Definition inc_pc_def:
 End
 
 (* The set of program counters the given instruction and starting point can
- * immediately reach, withing a function *)
+ * immediately reach, within a function *)
 Definition next_ips_def:
   (next_ips (Ret _) ip = {}) ∧
   (next_ips (Br _ l1 l2) ip =
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 46ce3fed8..895453b61 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -483,9 +483,6 @@ QED
 
 
 (* ----- A bigger-step semantics ----- *)
-Definition stuck_def:
-  stuck p s1 ⇔ ¬get_instr p s1.ip Exit ∧ ¬∃l s2. step p s1 l s2
-End
 
 Definition last_step_def:
   last_step p s1 l s2 ⇔
@@ -512,15 +509,6 @@ Inductive multi_step:
    multi_step p s1 (l::ls) s3)
 End
 
-Inductive observation_prefixes:
-  (∀l. observation_prefixes (Complete, l) (Complete, filter (\x. x ≠ Tau) l)) ∧
-  (∀l. observation_prefixes (Stuck, l) (Stuck, filter (\x. x ≠ Tau) l)) ∧
-  (∀l1 l2 x.
-    l2 ≼ l1 ∧ (l2 = l1 ⇒ x = Partial)
-    ⇒
-    observation_prefixes (x, l1) (Partial, filter (\x. x ≠ Tau) l2))
-End
-
 Definition multi_step_sem_def:
   multi_step_sem p s1 =
     { l1 | ∃path l2. l1 ∈ observation_prefixes (get_observation p (last path), flat l2) ∧
diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml
index 2d573bc55..3b21f0702 100644
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@@ -180,7 +180,7 @@ End
 (* TODO *)
 Definition translate_instr_to_inst_def:
   (translate_instr_to_inst emap (llvm$Store (t1, a1) (t2, a2)) =
-    llair$Store (translate_arg emap a1) (translate_arg emap a2) (sizeof t2)) ∧
+    llair$Store (translate_arg emap a2) (translate_arg emap a1) (sizeof t1)) ∧
   (translate_instr_to_inst emap (Load r t (t1, a1)) =
     Load (translate_reg r t) (translate_arg emap a1) (sizeof t))
 End
@@ -402,7 +402,7 @@ End
 
 Definition translate_prog_def:
   translate_prog p =
-    <| globals := ARB;
+    <| glob_init := ARB;
        functions := map (\(fname, d). (dest_fn fname, translate_def (dest_fn fname) d)) p |>
 End
 
diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml
index 9efdfb781..e3964b6d7 100644
--- a/sledge/semantics/llvm_to_llair_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@@ -9,14 +9,18 @@
 
 open HolKernel boolLib bossLib Parse;
 open listTheory arithmeticTheory pred_setTheory finite_mapTheory wordsTheory integer_wordTheory;
-open settingsTheory miscTheory llvmTheory llairTheory llair_propTheory llvm_to_llairTheory;
+open rich_listTheory pathTheory;
+open settingsTheory miscTheory memory_modelTheory;
+open llvmTheory llvm_propTheory llvm_liveTheory llairTheory llair_propTheory llvm_to_llairTheory;
 
 new_theory "llvm_to_llair_prop";
 
+set_grammar_ancestry ["llvm", "llair", "llvm_to_llair", "llvm_live"];
+
 numLib.prefer_num ();
 
 Inductive v_rel:
-  (∀w. v_rel (FlatV (PtrV w)) (FlatV (IntV (w2i w) pointer_size))) ∧
+  (∀w. v_rel (FlatV (PtrV w)) (FlatV (IntV (w2i w) llair$pointer_size))) ∧
   (∀w. v_rel (FlatV (W1V w)) (FlatV (IntV (w2i w) 1))) ∧
   (∀w. v_rel (FlatV (W8V w)) (FlatV (IntV (w2i w) 8))) ∧
   (∀w. v_rel (FlatV (W32V w)) (FlatV (IntV (w2i w) 32))) ∧
@@ -28,52 +32,52 @@ Inductive v_rel:
 End
 
 (* Define when an LLVM state is related to a llair one. Parameterised over a
- * relation on program counters, which chould be generated by the
+ * relation on program counters, which should be generated by the
  * transformation. It is not trivial because the translation cuts up blocks at
- * function calls and for remiving phi nodes.
+ * function calls and adds blocks for removing phi nodes.
  *
  * Also parameterised on a map for locals relating LLVM registers to llair
  * expressions that compute the value in that register. This corresponds to part
  * of the translation's state.
  *)
 Definition state_rel_def:
-  state_rel pc_rel emap (s:llvm$state) (s':llair$state) ⇔
+  state_rel prog pc_rel emap (s:llvm$state) (s':llair$state) ⇔
     pc_rel s.ip s'.bp ∧
-    (* Unmapped registers in LLVM are unmapped in llair too *)
-    (∀r. flookup s.locals r = None ⇒ flookup emap r = None) ∧
-    (* Mapped LLVM registers have a related value in the emap (after
-     * evaluating) *)
-    (∀r v. flookup s.locals r = Some v ⇒
-      ∃v' e.
+    (* Live LLVM registers are mapped and have a related value in the emap
+     * (after evaluating) *)
+    (∀r. r ∈ live prog s.ip ⇒
+      ∃v v' e.
         v_rel v.value v' ∧
+        flookup s.locals r = Some v ∧
         flookup emap r = Some e ∧ eval_exp s' e v') ∧
-    erase_tags s.heap = s'.heap
+    erase_tags s.heap = s'.heap ∧
+    s'.status = get_observation prog s
 End
 
-Theorem translate_arg_correct:
-  ∀s a v pc_rel emap s'.
-  state_rel pc_rel emap s s' ∧
-  eval s a = Some v
-  ⇒
-  ∃v'. eval_exp s' (translate_arg emap a) v' ∧ v_rel v.value v'
+Theorem v_rel_bytes:
+  ∀v v'. v_rel v v' ⇒ llvm_value_to_bytes v = llair_value_to_bytes v'
 Proof
-  Cases_on `a` >> rw [eval_def, translate_arg_def]
-  >- cheat >>
-  CASE_TAC >> fs [PULL_EXISTS, state_rel_def] >>
-  res_tac >> rfs [] >> metis_tac []
+  ho_match_mp_tac v_rel_ind >>
+  rw [v_rel_cases, llvm_value_to_bytes_def, llair_value_to_bytes_def] >>
+  rw [value_to_bytes_def, llvmTheory.unconvert_value_def, w2n_i2n,
+      llairTheory.unconvert_value_def, llairTheory.pointer_size_def,
+      llvmTheory.pointer_size_def] >>
+  pop_assum mp_tac >>
+  qid_spec_tac `vs1` >>
+  Induct_on `vs2` >> rw [] >> rw []
 QED
 
 Theorem translate_constant_correct_lem:
-  (∀c s pc_rel emap s' (g : glob_var |-> β # word64).
-   state_rel pc_rel emap s s'
+  (∀c s prog pc_rel emap s' (g : glob_var |-> β # word64).
+   state_rel prog pc_rel emap s s'
    ⇒
    ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v') ∧
-  (∀(cs : (ty # const) list) s pc_rel emap s' (g : glob_var |-> β # word64).
-   state_rel pc_rel emap s s'
+  (∀(cs : (ty # const) list) s prog pc_rel emap s' (g : glob_var |-> β # word64).
+   state_rel prog pc_rel emap s s'
    ⇒
    ∃v'. list_rel (eval_exp s') (map (translate_const o snd) cs) v' ∧ list_rel v_rel (map (eval_const g o snd) cs) v') ∧
-  (∀(tc : ty # const) s pc_rel emap s' (g : glob_var |-> β # word64).
-   state_rel pc_rel emap s s'
+  (∀(tc : ty # const) s prog pc_rel emap s' (g : glob_var |-> β # word64).
+   state_rel prog pc_rel emap s s'
    ⇒
    ∃v'. eval_exp s' (translate_const (snd tc)) v' ∧ v_rel (eval_const g (snd tc)) v')
 Proof
@@ -97,14 +101,38 @@ Proof
 QED
 
 Theorem translate_constant_correct:
-  ∀c s pc_rel emap s' g.
-   state_rel pc_rel emap s s'
+  ∀c s prog pc_rel emap s' g.
+   state_rel prog pc_rel emap s s'
    ⇒
    ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v'
 Proof
   metis_tac [translate_constant_correct_lem]
 QED
 
+Theorem translate_arg_correct:
+  ∀s a v prog pc_rel emap s'.
+  state_rel prog pc_rel emap s s' ∧
+  eval s a = Some v ∧
+  arg_to_regs a ⊆ live prog s.ip
+  ⇒
+  ∃v'. eval_exp s' (translate_arg emap a) v' ∧ v_rel v.value v'
+Proof
+  Cases_on `a` >> rw [eval_def, translate_arg_def] >> rw []
+  >- metis_tac [translate_constant_correct] >>
+  CASE_TAC >> fs [PULL_EXISTS, state_rel_def, arg_to_regs_def] >>
+  res_tac >> rfs [] >> metis_tac []
+QED
+
+Theorem is_allocated_state_rel:
+  ∀prog pc_rel emap s1 s1'.
+    state_rel prog pc_rel emap s1 s1'
+    ⇒
+    (∀i. is_allocated i s1.heap ⇔ is_allocated i s1'.heap)
+Proof
+  rw [state_rel_def, is_allocated_def, erase_tags_def] >>
+  pop_assum mp_tac >> pop_assum (mp_tac o GSYM) >> rw []
+QED
+
 Theorem restricted_i2w_11:
   ∀i (w:'a word). INT_MIN (:'a) ≤ i ∧ i ≤ INT_MAX (:'a) ⇒ (i2w i : 'a word) = i2w (w2i w) ⇒ i = w2i w
 Proof
@@ -132,8 +160,8 @@ Proof
 QED
 
 Theorem translate_extract_correct:
-  ∀pc_rel emap s1 s1' a v v1' e1' cs ns result.
-    state_rel pc_rel emap s1 s1' ∧
+  ∀prog pc_rel emap s1 s1' a v v1' e1' cs ns result.
+    state_rel prog pc_rel emap s1 s1' ∧
     map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧
     extract_value v ns = Some result ∧
     eval_exp s1' e1' v1' ∧
@@ -166,8 +194,8 @@ Proof
 QED
 
 Theorem translate_update_correct:
-  ∀pc_rel emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result.
-    state_rel pc_rel emap s1 s1' ∧
+  ∀prog pc_rel emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result.
+    state_rel prog pc_rel emap s1 s1' ∧
     map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧
     insert_value v1 v2 ns = Some result ∧
     eval_exp s1' e1' v1' ∧
@@ -205,26 +233,29 @@ Proof
   metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN]
 QED
 
+(*
 Theorem translate_instr_to_exp_correct:
-  ∀emap instr r t s1 s1'.
+  ∀emap instr r t s1 s1' s2 prog pc_rel.
     classify_instr instr = Exp r t ∧
-    state_rel pc_rel emap s1 s1'
-    ⇒
-    (∀s2. step_instr prog s1 instr s2 ⇒
-      (∃v pv. eval_exp s1' (translate_instr_to_exp emap instr) v ∧
-              flookup s2.locals r = Some pv ∧ v_rel pv.value v))
+    state_rel prog pc_rel emap s1 s1' ∧
+    get_instr prog s1.ip instr ∧
+    step_instr prog s1 instr s2 ⇒
+    ∃v pv.
+      eval_exp s1' (translate_instr_to_exp emap instr) v ∧
+      flookup s2.locals r = Some pv ∧ v_rel pv.value v
 Proof
   recInduct translate_instr_to_exp_ind >>
   simp [translate_instr_to_exp_def, classify_instr_def] >>
   conj_tac
   >- ( (* Sub *)
     rw [step_instr_cases, Once eval_exp_cases, do_sub_def, PULL_EXISTS] >>
-    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
+    simp [llvmTheory.inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
     simp [v_rel_cases, PULL_EXISTS] >>
     first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
     disch_then drule >>
     first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
     disch_then drule >>
+    drule get_instr_live >> simp [uses_def] >> strip_tac >>
     BasicProvers.EVERY_CASE_TAC >> fs [translate_ty_def, translate_size_def] >>
     rfs [v_rel_cases] >>
     pairarg_tac >> fs [] >>
@@ -263,16 +294,193 @@ Proof
       metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:64)``,
                  SIMP_CONV (srw_ss()) [] ``INT_MAX (:64)``])) >>
   conj_tac
-  >- (
+  >- ( (* Extractvalue *)
     rw [step_instr_cases] >>
-    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
-    metis_tac [translate_arg_correct, translate_extract_correct]) >>
+    simp [llvmTheory.inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
+    metis_tac [uses_def, get_instr_live, translate_arg_correct, translate_extract_correct]) >>
   conj_tac
-  >- (
+  >- ( (* Updatevalue *)
     rw [step_instr_cases] >>
-    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
-    metis_tac [translate_arg_correct, translate_update_correct]) >>
+    simp [llvmTheory.inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
+    drule get_instr_live >> simp [uses_def] >>
+    metis_tac [get_instr_live, translate_arg_correct, translate_update_correct]) >>
+  cheat
+QED
+
+Triviality eval_exp_help:
+  (s1 with heap := h).locals = s1.locals
+Proof
+  rw []
+QED
+
+Theorem erase_tags_set_bytes:
+  ∀p v l h. erase_tags (set_bytes p v l h) = set_bytes () v l (erase_tags h)
+Proof
+  Induct_on `v` >> rw [set_bytes_def] >>
+  irule (METIS_PROVE [] ``x = y ⇒ f a b c x = f a b c y``) >>
+  rw [erase_tags_def]
+QED
+
+Theorem translate_instr_to_inst_correct:
+  ∀prog pc_rel emap instr s1 s1' s2.
+    classify_instr instr = Non_exp ∧
+    state_rel prog pc_rel emap s1 s1' ∧
+    get_instr prog s1.ip instr ∧
+    step_instr prog s1 instr s2 ⇒
+    ∃s2'.
+      step_inst s1' (translate_instr_to_inst emap instr) s2' ∧
+      state_rel prog pc_rel emap s2 s2'
+
+Proof
+
+  rw [step_instr_cases] >>
+  fs [classify_instr_def, translate_instr_to_inst_def]
+  >- ( (* Load *)
+    cheat)
+  >- ( (* Store *)
+    simp [step_inst_cases, PULL_EXISTS] >>
+    drule get_instr_live >> rw [uses_def] >>
+    drule translate_arg_correct >> disch_then drule >> disch_then drule >>
+    qpat_x_assum `eval _ _ = Some _` mp_tac >>
+    drule translate_arg_correct >> disch_then drule >> disch_then drule >>
+    rw [] >>
+    qpat_x_assum `v_rel (FlatV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
+    HINT_EXISTS_TAC >> rw [] >>
+    qexists_tac `freeable` >> rw [] >>
+    HINT_EXISTS_TAC >> rw []
+    >- metis_tac [v_rel_bytes]
+    >- (
+      fs [w2n_i2n, pointer_size_def] >>
+      metis_tac [v_rel_bytes, is_allocated_state_rel, ADD_COMM]) >>
+    fs [state_rel_def] >>
+    rw []
+    >- cheat
+    >- (
+      fs [llvmTheory.inc_pc_def] >>
+      `r ∈ live prog s1.ip`
+      by (
+        drule live_gen_kill >>
+        rw [next_ips_def, assigns_def, uses_def, inc_pc_def]) >>
+      first_x_assum drule >> rw [] >>
+      metis_tac [eval_exp_ignores, eval_exp_help])
+    >- (
+      rw [llvmTheory.inc_pc_def, w2n_i2n, pointer_size_def, erase_tags_set_bytes] >>
+      metis_tac[v_rel_bytes]))
+  >- cheat
+  >- cheat
+  >- cheat
+QED
+
+
+    simp [step_inst_cases, PULL_EXISTS] >>
+    Cases_on `r` >> simp [translate_reg_def] >>
+    drule get_instr_live >> rw [uses_def] >>
+    drule translate_arg_correct >> disch_then drule >> disch_then drule >>
+    simp [Once v_rel_cases] >> rw [] >>
+    qexists_tac `IntV (w2i w) pointer_size` >> rw [] >>
+    qexists_tac `freeable` >> rw []
+    >- (fs [w2n_i2n, pointer_size_def] >> metis_tac [is_allocated_state_rel]) >>
+    fs [state_rel_def] >> rw []
+    >- cheat
+    >- (
+      fs [llvmTheory.inc_pc_def, update_results_def, update_result_def] >>
+      rw [] >> fs [FLOOKUP_UPDATE] >> rw []
+      >- (
+        cheat)
+      >- (
+        `r ∈ live prog s1.ip`
+        by (
+          drule live_gen_kill >>
+          rw [next_ips_def, assigns_def, uses_def, inc_pc_def]) >>
+        first_x_assum drule >> rw [] >>
+        qexists_tac `v` >>
+        qexists_tac `v'` >>
+        qexists_tac `e` >>
+        rw []
+        metis_tac [eval_exp_ignores, eval_exp_help])
+
+
+    >- fs [update_results_def, llvmTheory.inc_pc_def, update_result_def]
+
+*)
+
+Definition translate_trace_def:
+  (translate_trace types Tau = Tau ) ∧
+  (translate_trace types (W gv bytes) = W (translate_glob_var gv (types gv)) bytes)
+End
+
+Theorem multi_step_to_step_block:
+  ∀prog s1 s1' tr s2.
+    state_rel prog pc_rel emap s1 s1' ∧
+    multi_step prog s1 tr s2
+    ⇒
+    ∃s2' b.
+      get_block (translate_prog prog) s1'.bp b ∧
+      step_block (translate_prog prog) s1' b.cmnd (map (translate_trace types) tr) b.term s2' ∧
+      state_rel prog pc_rel emap s2 s2'
+Proof
   cheat
 QED
 
+Theorem trans_trace_not_tau:
+  ∀types. (λx. x ≠ Tau) ∘ translate_trace types = (λx. x ≠ Tau)
+Proof
+  rw [FUN_EQ_THM] >> eq_tac >> rw [translate_trace_def] >>
+  Cases_on `x` >> fs [translate_trace_def]
+QED
+
+Theorem translate_prog_correct_lem1:
+  ∀path.
+    okpath (multi_step prog) path ∧ finite path
+    ⇒
+    ∀s1'.
+    state_rel prog pc_rel emap (first path) s1'
+    ⇒
+    ∃path'.
+      finite path' ∧
+      okpath (step (translate_prog prog)) path' ∧
+      first path' = s1' ∧
+      labels path' = LMAP (map (translate_trace types)) (labels path) ∧
+      state_rel prog pc_rel emap (last path) (last path')
+Proof
+  ho_match_mp_tac finite_okpath_ind >> rw []
+  >- (qexists_tac `stopped_at s1'` >> rw []) >>
+  drule multi_step_to_step_block >> disch_then drule >>
+  disch_then (qspec_then `types` mp_tac) >> rw [] >>
+  first_x_assum drule >> rw [] >>
+  qexists_tac `pcons s1' (map (translate_trace types) r) path'` >> rw [] >>
+  simp [step_cases] >> qexists_tac `b` >> simp [] >>
+  fs [state_rel_def] >> simp [get_observation_def] >>
+  fs [Once multi_step_cases, last_step_def] >> rw [] >>
+  metis_tac [get_instr_func, exit_no_step]
+QED
+
+Theorem translate_prog_correct:
+  ∀prog s1 s1'.
+    state_rel prog pc_rel emap s1 s1'
+    ⇒
+    image (I ## map (translate_trace types)) (multi_step_sem prog s1) = sem (translate_prog prog) s1'
+Proof
+  rw [sem_def, multi_step_sem_def, EXTENSION] >> eq_tac >> rw []
+  >- (
+    drule translate_prog_correct_lem1 >> disch_then drule >> disch_then drule >>
+    disch_then (qspec_then `types` mp_tac) >> rw [] >>
+    qexists_tac `path'` >> rw [] >>
+    fs [IN_DEF, observation_prefixes_cases, toList_some] >> rw [] >>
+    rfs [lmap_fromList] >>
+    rw [GSYM MAP_FLAT, FILTER_MAP, trans_trace_not_tau]
+    >- fs [state_rel_def]
+    >- fs [state_rel_def] >>
+    qexists_tac `map (translate_trace types) l2'` >>
+    simp [GSYM MAP_FLAT, FILTER_MAP, trans_trace_not_tau] >>
+    `INJ (translate_trace types) (set l2' ∪ set (flat l2)) UNIV`
+    by (
+      simp [INJ_DEF] >> rpt gen_tac >>
+      Cases_on `x` >> Cases_on `y` >> simp [translate_trace_def] >>
+      Cases_on `a` >> Cases_on `a'` >> simp [translate_glob_var_def]) >>
+    fs [INJ_MAP_EQ_IFF, inj_map_prefix_iff] >> rw [] >>
+    fs [state_rel_def])
+  >- cheat
+QED
+
 export_theory ();
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index 7e69f889f..18515eff3 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -10,7 +10,7 @@
 
 open HolKernel boolLib bossLib Parse;
 open listTheory rich_listTheory arithmeticTheory integerTheory llistTheory pathTheory;
-open integer_wordTheory wordsTheory;
+open integer_wordTheory wordsTheory pred_setTheory;
 open finite_mapTheory open logrootTheory numposrepTheory;
 open settingsTheory;
 
@@ -18,6 +18,31 @@ new_theory "misc";
 
 numLib.prefer_num ();
 
+(* Labels for the transitions to make externally observable behaviours apparent.
+ * For now, we'll consider this to be writes to global variables.
+ * *)
+Datatype:
+  obs =
+  | Tau
+  | W 'a (word8 list)
+End
+
+Datatype:
+  trace_type =
+  | Stuck
+  | Complete
+  | Partial
+End
+
+Inductive observation_prefixes:
+  (∀l. observation_prefixes (Complete, l) (Complete, filter (\x. x ≠ Tau) l)) ∧
+  (∀l. observation_prefixes (Stuck, l) (Stuck, filter (\x. x ≠ Tau) l)) ∧
+  (∀l1 l2 x.
+    l2 ≼ l1 ∧ (l2 = l1 ⇒ x = Partial)
+    ⇒
+    observation_prefixes (x, l1) (Partial, filter (\x. x ≠ Tau) l2))
+End
+
 (* ----- Theorems about list library functions ----- *)
 
 Theorem dropWhile_map:
@@ -85,6 +110,19 @@ Proof
   rw [FDIFF_def, FLOOKUP_DRESTRICT] >> fs []
 QED
 
+Theorem inj_map_prefix_iff:
+  ∀f l1 l2. INJ f (set l1 ∪ set l2) UNIV ⇒ (map f l1 ≼ map f l2 ⇔ l1 ≼ l2)
+Proof
+  Induct_on `l1` >> rw [] >>
+  Cases_on `l2` >> rw [] >>
+  `INJ f (set l1 ∪ set t) UNIV`
+  by (
+    irule INJ_SUBSET >> qexists_tac `(h INSERT set l1) ∪ (set (h'::t))` >>
+    simp [SUBSET_DEF] >> fs [] >>
+    metis_tac []) >>
+  fs [INJ_IFF] >> metis_tac []
+QED
+
 (* ----- Theorems about log ----- *)
 
 Theorem mul_div_bound:
@@ -251,6 +289,18 @@ Proof
   metis_tac []
 QED
 
+Theorem lmap_fromList:
+  !f l. LMAP f (fromList l) = fromList (map f l)
+Proof
+  Induct_on `l` >> rw []
+QED
+
+Theorem fromList_11[simp]:
+  !l1 l2. fromList l1 = fromList l2 ⇔ l1 = l2
+Proof
+  Induct >> rw [] >>
+  Cases_on `l2` >> fs []
+QED
 
 (* ----- Theorems about labelled transition system paths ----- *)