From c065a274d9f3085527261172c9820f8eafc6893e Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@kevix.co>
Date: Fri, 15 Jun 2018 16:30:25 -0400
Subject: [PATCH 1/7] io experiment using explicit stacks

---
 src/ExprImp.v | 105 +++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 78 insertions(+), 27 deletions(-)

diff --git a/src/ExprImp.v b/src/ExprImp.v
index c6db6512..c95a3577 100644
--- a/src/ExprImp.v
+++ b/src/ExprImp.v
@@ -22,7 +22,7 @@ Section ExprImp1.
   Notation func := (@name FName).
 
 
-  Context {state: Type}.
+  Context {state: Set}.
   Context {stateMap: Map state var (word wXLEN)}.
   Context {vars: Type}.
   Context {varset: set vars var}.
@@ -43,7 +43,8 @@ Section ExprImp1.
     | SWhile(cond: expr)(body: stmt): stmt
     | SSeq(s1 s2: stmt): stmt
     | SSkip: stmt
-    | SCall(binds: list var)(f: func)(args: list expr).
+    | SCall(binds: list var)(f: func)(args: list expr)
+    | SExtern.
 
   Fixpoint eval_expr(st: state)(e: expr): option (word wXLEN) :=
     match e with
@@ -55,50 +56,99 @@ Section ExprImp1.
         Return (eval_binop op v1 v2)
     end.
 
+  Inductive cont: Set :=
+    | CLoad(x: var)(addr: expr): cont
+    | CStore(addr val: expr): cont
+    | CSet(x: var)(e: expr): cont
+    | CIf(cond: expr)(bThen bElse: cont): cont
+    | CWhile(cond: expr)(body: cont): cont
+    | CSeq(s1 s2: cont): cont
+    | CSkip: cont
+    | CCall(binds: list var)(f: func)(args: list expr)
+    | CExtern
+    | CStack(st: state)(c: cont)(binds rets: list var).
+
+  Fixpoint cont_of_stmt (s:stmt) :=
+    match s with
+    | SLoad x a => CLoad x a
+    | SStore a v => CStore a v
+    | SSet x e => CSet x e
+    | SIf c t e => CIf c (cont_of_stmt t) (cont_of_stmt e)
+    | SWhile c b => CWhile c (cont_of_stmt b)
+    | SSeq s1 s2 => CSeq (cont_of_stmt s1) (cont_of_stmt s2)
+    | SSkip => CSkip
+    | SExtern => CExtern
+    | SCall b f a => CCall b f a
+    end.
+
   Section WithEnv.
     Context {env} {funcMap: Map env func (list var * list var * stmt)} (e:env).
-    Fixpoint eval_stmt(f: nat)(st: state)(m: mem)(s: stmt): option (state * mem) :=
+    Fixpoint eval_cont(f: nat)(st: state)(m: mem)(s: cont): option (state*mem*option cont) :=
       match f with
       | 0 => None (* out of fuel *)
       | S f => match s with
-        | SLoad x a =>
+        | CLoad x a =>
             a <- eval_expr st a;
             v <- read_mem a m;
-            Return (put st x v, m)
-        | SStore a v =>
+            Return (put st x v, m, None)
+        | CStore a v =>
             a <- eval_expr st a;
             v <- eval_expr st v;
             m <- write_mem a v m;
-            Return (st, m)
-        | SSet x e =>
+            Return (st, m, None)
+        | CSet x e =>
             v <- eval_expr st e;
-            Return (put st x v, m)
-        | SIf cond bThen bElse =>
+            Return (put st x v, m, None)
+        | CIf cond bThen bElse =>
             v <- eval_expr st cond;
-            eval_stmt f st m (if weq v $0 then bElse else bThen)
-        | SWhile cond body =>
+            eval_cont f st m (if weq v $0 then bElse else bThen)
+        | CWhile cond body =>
             v <- eval_expr st cond;
-            if weq v $0 then Return (st, m) else
-              p <- eval_stmt f st m body;
-              let '(st, m) := p in
-              eval_stmt f st m (SWhile cond body)
-        | SSeq s1 s2 =>
-            p <- eval_stmt f st m s1;
-            let '(st, m) := p in
-            eval_stmt f st m s2
-        | SSkip => Return (st, m)
-        | SCall binds fname args =>
+            if weq v $0 then Return (st, m, None) else
+              p <- eval_cont f st m body;
+              let '(st, m, c) := p in
+              match c with
+              | Some c => Return (st, m, Some (CSeq c s))
+              | None => eval_cont f st m (CWhile cond body)
+              end
+        | CSeq s1 s2 =>
+            p <- eval_cont f st m s1;
+            let '(st, m, c) := p in
+            match c with
+            | Some c => Return (st, m, Some (CSeq c s2))
+            | None => eval_cont f st m s2
+            end
+        | CSkip => Return (st, m, None)
+        | CCall binds fname args =>
           fimpl <- get e fname;
           let '(params, rets, fbody) := fimpl in
+          let fbody := cont_of_stmt fbody in
           argvs <- option_all (map (eval_expr st) args);
           st0 <- putmany params argvs empty;
-          st1m' <- eval_stmt f st0 m fbody;
-          let '(st1, m') := st1m' in
-          retvs <- option_all (map (get st1) rets);
-          st' <- putmany binds retvs st;
-          Return (st', m')
+          st1m' <- eval_cont f st0 m fbody;
+          let '(st1, m', c) := st1m' in
+          match c with
+          | Some c => Return (st, m', Some (CStack st1 c binds rets))
+          | None => 
+            retvs <- option_all (map (get st1) rets);
+            st' <- putmany binds retvs st;
+            Return (st', m', None)
+          end
+        | CExtern => Return (st, m, Some CSkip)
+        | CStack stf cf binds rets =>
+          stf'm' <- eval_cont f stf m cf;
+          let '(stf', m', c) := stf'm' in
+          match c with
+          | Some c => Return (st, m', Some (CStack stf' c binds rets))
+          | None => 
+            retvs <- option_all (map (get stf') rets);
+            st' <- putmany binds retvs st;
+            Return (st', m', None)
+          end
         end
       end.
+    Definition eval_stmt(f: nat)(st: state)(m: mem)(s: stmt)
+      := eval_cont f st m (cont_of_stmt s).
 
     Fixpoint expr_size(e: expr): nat :=
       match e with
@@ -118,6 +168,7 @@ Section ExprImp1.
       | SSkip => 1
       | SCall binds f args =>
           S (length binds + length args + List.fold_right Nat.add O (List.map expr_size args))
+      | SExtern => 1 (* TODO *)
       end.
 
     Local Ltac inversion_lemma :=

From f53c5f9c31342b11842cde5e3cd802e9d956ec4e Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@kevix.co>
Date: Wed, 20 Jun 2018 13:56:03 -0400
Subject: [PATCH 2/7] factor stmt and cont

---
 src/ExprImp.v | 83 +++++++++++++++++++++++++--------------------------
 1 file changed, 40 insertions(+), 43 deletions(-)

diff --git a/src/ExprImp.v b/src/ExprImp.v
index c95a3577..26b0c904 100644
--- a/src/ExprImp.v
+++ b/src/ExprImp.v
@@ -44,7 +44,7 @@ Section ExprImp1.
     | SSeq(s1 s2: stmt): stmt
     | SSkip: stmt
     | SCall(binds: list var)(f: func)(args: list expr)
-    | SExtern.
+    | SExtern(binds: list var)(io : nat)(args: list expr).
 
   Fixpoint eval_expr(st: state)(e: expr): option (word wXLEN) :=
     match e with
@@ -56,76 +56,58 @@ Section ExprImp1.
         Return (eval_binop op v1 v2)
     end.
 
-  Inductive cont: Set :=
-    | CLoad(x: var)(addr: expr): cont
-    | CStore(addr val: expr): cont
-    | CSet(x: var)(e: expr): cont
-    | CIf(cond: expr)(bThen bElse: cont): cont
-    | CWhile(cond: expr)(body: cont): cont
-    | CSeq(s1 s2: cont): cont
-    | CSkip: cont
-    | CCall(binds: list var)(f: func)(args: list expr)
-    | CExtern
+  Section cont.
+    Context {T : Set}.
+    Inductive cont : Set :=
+    | CSuspended (_:T)
+    | CSeq(s1:cont) (s2: stmt)
     | CStack(st: state)(c: cont)(binds rets: list var).
-
-  Fixpoint cont_of_stmt (s:stmt) :=
-    match s with
-    | SLoad x a => CLoad x a
-    | SStore a v => CStore a v
-    | SSet x e => CSet x e
-    | SIf c t e => CIf c (cont_of_stmt t) (cont_of_stmt e)
-    | SWhile c b => CWhile c (cont_of_stmt b)
-    | SSeq s1 s2 => CSeq (cont_of_stmt s1) (cont_of_stmt s2)
-    | SSkip => CSkip
-    | SExtern => CExtern
-    | SCall b f a => CCall b f a
-    end.
+  End cont. Arguments cont : clear implicits.
 
   Section WithEnv.
     Context {env} {funcMap: Map env func (list var * list var * stmt)} (e:env).
-    Fixpoint eval_cont(f: nat)(st: state)(m: mem)(s: cont): option (state*mem*option cont) :=
+    Fixpoint eval_stmt(f: nat)(st: state)(m: mem)(s: stmt): option (state*mem*option (cont unit)) :=
       match f with
       | 0 => None (* out of fuel *)
       | S f => match s with
-        | CLoad x a =>
+        | SLoad x a =>
             a <- eval_expr st a;
             v <- read_mem a m;
             Return (put st x v, m, None)
-        | CStore a v =>
+        | SStore a v =>
             a <- eval_expr st a;
             v <- eval_expr st v;
             m <- write_mem a v m;
             Return (st, m, None)
-        | CSet x e =>
+        | SSet x e =>
             v <- eval_expr st e;
             Return (put st x v, m, None)
-        | CIf cond bThen bElse =>
+        | SIf cond bThen bElse =>
             v <- eval_expr st cond;
-            eval_cont f st m (if weq v $0 then bElse else bThen)
-        | CWhile cond body =>
+            eval_stmt f st m (if weq v $0 then bElse else bThen)
+        | SWhile cond body =>
             v <- eval_expr st cond;
             if weq v $0 then Return (st, m, None) else
-              p <- eval_cont f st m body;
+              p <- eval_stmt f st m body;
               let '(st, m, c) := p in
               match c with
-              | Some c => Return (st, m, Some (CSeq c s))
-              | None => eval_cont f st m (CWhile cond body)
+              | Some c => Return (st, m, Some (CSeq c (SWhile cond body)))
+              | None => eval_stmt f st m (SWhile cond body)
               end
-        | CSeq s1 s2 =>
-            p <- eval_cont f st m s1;
+        | SSeq s1 s2 =>
+            p <- eval_stmt f st m s1;
             let '(st, m, c) := p in
             match c with
             | Some c => Return (st, m, Some (CSeq c s2))
-            | None => eval_cont f st m s2
+            | None => eval_stmt f st m s2
             end
-        | CSkip => Return (st, m, None)
-        | CCall binds fname args =>
+        | SSkip => Return (st, m, None)
+        | SCall binds fname args =>
           fimpl <- get e fname;
           let '(params, rets, fbody) := fimpl in
-          let fbody := cont_of_stmt fbody in
           argvs <- option_all (map (eval_expr st) args);
           st0 <- putmany params argvs empty;
-          st1m' <- eval_cont f st0 m fbody;
+          st1m' <- eval_stmt f st0 m fbody;
           let '(st1, m', c) := st1m' in
           match c with
           | Some c => Return (st, m', Some (CStack st1 c binds rets))
@@ -134,7 +116,22 @@ Section ExprImp1.
             st' <- putmany binds retvs st;
             Return (st', m', None)
           end
-        | CExtern => Return (st, m, Some CSkip)
+        | SExtern _ _ _ => Return (st, m, Some (CSuspended tt))
+        end
+      end.
+
+    Fixpoint eval_cont(f: nat)(st: state)(m: mem)(s: cont stmt): option (state*mem*option (cont unit)) :=
+      match f with
+      | 0 => None (* out of fuel *)
+      | S f => match s with
+        | CSuspended s => eval_stmt f st m s
+        | CSeq c1 s2 =>
+            p <- eval_cont f st m c1;
+            let '(st, m, c) := p in
+            match c with
+            | Some c => Return (st, m, Some (CSeq c s2))
+            | None => eval_cont f st m (CSuspended s2)
+            end
         | CStack stf cf binds rets =>
           stf'm' <- eval_cont f stf m cf;
           let '(stf', m', c) := stf'm' in
@@ -148,7 +145,7 @@ Section ExprImp1.
         end
       end.
     Definition eval_stmt(f: nat)(st: state)(m: mem)(s: stmt)
-      := eval_cont f st m (cont_of_stmt s).
+      := eval_cont f st m (CSuspended s).
 
     Fixpoint expr_size(e: expr): nat :=
       match e with

From 6e7b3b125917a01551181ee3816e5e2ee54efc96 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@kevix.co>
Date: Wed, 20 Jun 2018 14:08:10 -0400
Subject: [PATCH 3/7] cleanup

---
 src/ExprImp.v | 36 ++++++++++++++++++++----------------
 1 file changed, 20 insertions(+), 16 deletions(-)

diff --git a/src/ExprImp.v b/src/ExprImp.v
index 26b0c904..de3b1d68 100644
--- a/src/ExprImp.v
+++ b/src/ExprImp.v
@@ -20,6 +20,7 @@ Section ExprImp1.
   Existing Instance eq_name_dec.
   Context {FName : NameWithEq}.
   Notation func := (@name FName).
+  Context (ioaction : Set).
 
 
   Context {state: Set}.
@@ -44,7 +45,7 @@ Section ExprImp1.
     | SSeq(s1 s2: stmt): stmt
     | SSkip: stmt
     | SCall(binds: list var)(f: func)(args: list expr)
-    | SExtern(binds: list var)(io : nat)(args: list expr).
+    | SIO(binds: list var)(io : ioaction)(args: list expr).
 
   Fixpoint eval_expr(st: state)(e: expr): option (word wXLEN) :=
     match e with
@@ -64,9 +65,11 @@ Section ExprImp1.
     | CStack(st: state)(c: cont)(binds rets: list var).
   End cont. Arguments cont : clear implicits.
 
+  Definition ioact : Set := (list var * ioaction * list (word (wXLEN))).
+  Definition ioret : Set := (list var * list (word wXLEN)).
   Section WithEnv.
     Context {env} {funcMap: Map env func (list var * list var * stmt)} (e:env).
-    Fixpoint eval_stmt(f: nat)(st: state)(m: mem)(s: stmt): option (state*mem*option (cont unit)) :=
+    Fixpoint eval_stmt(f: nat)(st: state)(m: mem)(s: stmt): option (state*mem*option(cont ioact)) :=
       match f with
       | 0 => None (* out of fuel *)
       | S f => match s with
@@ -116,26 +119,30 @@ Section ExprImp1.
             st' <- putmany binds retvs st;
             Return (st', m', None)
           end
-        | SExtern _ _ _ => Return (st, m, Some (CSuspended tt))
+        | SIO binds ionum args =>
+          argvs <- option_all (map (eval_expr st) args);
+          Return (st, m, Some (CSuspended (binds, ionum, argvs)))
         end
       end.
 
-    Fixpoint eval_cont(f: nat)(st: state)(m: mem)(s: cont stmt): option (state*mem*option (cont unit)) :=
+    Fixpoint eval_cont(f: nat)(st: state)(m: mem)(s: cont ioret): option (state*mem*option(cont ioact)) :=
       match f with
       | 0 => None (* out of fuel *)
       | S f => match s with
-        | CSuspended s => eval_stmt f st m s
-        | CSeq c1 s2 =>
-            p <- eval_cont f st m c1;
-            let '(st, m, c) := p in
-            match c with
+        | CSuspended (binds, retvs) =>
+            st' <- putmany binds retvs st;
+            Return (st', m, None)
+        | CSeq c s2 =>
+            p <- eval_cont f st m c;
+            let '(st, m, oc) := p in
+            match oc with
             | Some c => Return (st, m, Some (CSeq c s2))
-            | None => eval_cont f st m (CSuspended s2)
+            | None => eval_stmt f st m s2
             end
         | CStack stf cf binds rets =>
           stf'm' <- eval_cont f stf m cf;
-          let '(stf', m', c) := stf'm' in
-          match c with
+          let '(stf', m', oc) := stf'm' in
+          match oc with
           | Some c => Return (st, m', Some (CStack stf' c binds rets))
           | None => 
             retvs <- option_all (map (get stf') rets);
@@ -144,8 +151,6 @@ Section ExprImp1.
           end
         end
       end.
-    Definition eval_stmt(f: nat)(st: state)(m: mem)(s: stmt)
-      := eval_cont f st m (CSuspended s).
 
     Fixpoint expr_size(e: expr): nat :=
       match e with
@@ -163,9 +168,8 @@ Section ExprImp1.
       | SWhile cond body => S (expr_size cond + stmt_size body)
       | SSeq s1 s2 => S (stmt_size s1 + stmt_size s2)
       | SSkip => 1
-      | SCall binds f args =>
+      | SCall binds _ args | SIO binds _ args =>
           S (length binds + length args + List.fold_right Nat.add O (List.map expr_size args))
-      | SExtern => 1 (* TODO *)
       end.
 
     Local Ltac inversion_lemma :=

From 7906d2023d7dfb5cbe242782a6b169d5619f5617 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@kevix.co>
Date: Wed, 20 Jun 2018 14:17:52 -0400
Subject: [PATCH 4/7] relations on suspended continuations

---
 src/ExprImp.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/ExprImp.v b/src/ExprImp.v
index de3b1d68..76734408 100644
--- a/src/ExprImp.v
+++ b/src/ExprImp.v
@@ -64,6 +64,17 @@ Section ExprImp1.
     | CSeq(s1:cont) (s2: stmt)
     | CStack(st: state)(c: cont)(binds rets: list var).
   End cont. Arguments cont : clear implicits.
+  Lemma cont_uninhabited (T:Set) (_:T -> False) (X : cont T) : False. Proof. induction X; eauto. Qed.
+  Fixpoint lift_cont {A B : Set} (P : A -> B -> Prop) (a : cont A) (b : cont B) {struct a} :=
+    match a, b with
+    | CSuspended a, CSuspended b =>
+      P a b
+    | CSeq a sa, CSeq b sb =>
+      lift_cont P a b /\ sa = sb
+    | CStack sta a ba ra, CStack stb b bb rb =>
+      (forall vss, agree_on sta vss stb) /\ lift_cont P a b /\ ba = bb /\ ra = rb
+    | _, _ => False
+    end.
 
   Definition ioact : Set := (list var * ioaction * list (word (wXLEN))).
   Definition ioret : Set := (list var * list (word wXLEN)).

From d4ab29a0a4e405a98503d836926a193a8baf91c6 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@kevix.co>
Date: Wed, 20 Jun 2018 17:10:51 -0400
Subject: [PATCH 5/7] refactor...

---
 src/ExprImp.v | 201 ++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 196 insertions(+), 5 deletions(-)

diff --git a/src/ExprImp.v b/src/ExprImp.v
index 76734408..560e4d60 100644
--- a/src/ExprImp.v
+++ b/src/ExprImp.v
@@ -1,8 +1,203 @@
+Set Universe Polymorphism.
+Unset Universe Minimization ToSet.
+
+Require compiler.Common.
+
+Local Notation "'bind_Some' x <- a ; f" :=
+  (match a with
+   | Some x => f
+   | None => None
+   end)
+    (right associativity, at level 60, x pattern).
+
+Record LanguageParameters :=
+  {
+    mword : Type;
+    mword_nonzero : mword -> bool;
+
+    varname : Type;
+    funname : Type;
+    actname : Type;
+    bopname : Type;
+    mem : Type;
+
+    varmap : Type;
+    varmap_operations : Common.Map varmap varname mword;
+
+    eval_binop : bopname -> mword -> mword -> mword;
+    load : mword -> mem -> option mword;
+    store : mword -> mword -> mem -> option mem;
+  }.
+
+Section Language.
+  Context (p : LanguageParameters).
+  (* RecordImport p (* COQBUG(https://github.com/coq/coq/issues/7808) *) *)
+  Local Notation mword := p.(mword).
+  Local Notation mword_nonzero := p.(mword_nonzero).
+  Local Notation varname := p.(varname).
+  Local Notation funname := p.(funname).
+  Local Notation actname := p.(actname).
+  Local Notation bopname := p.(bopname).
+  Local Notation varmap := p.(varmap).
+  Local Notation mem := p.(mem).
+  Local Definition varmap_operations_ : Common.Map _ _ _ := p.(varmap_operations). Local Existing Instance varmap_operations_.
+  Local Notation eval_binop := p.(eval_binop).
+  Local Notation load := p.(load).
+  Local Notation store := p.(store).
+
+  Inductive expr :=
+  | ELit(v: mword)
+  | EVar(x: varname)
+  | EOp(op: bopname) (e1 e2: expr).
+
+  Inductive stmt :=
+  | SLoad(x: varname) (addr: expr)
+  | SStore(addr val: expr)
+  | SSet(x: varname)(e: expr)
+  | SIf(cond: expr)(bThen bElse: stmt)
+  | SWhile(cond: expr)(body: stmt)
+  | SSeq(s1 s2: stmt)
+  | SSkip
+  | SCall(binds: list varname)(f: funname)(args: list expr)
+  | SIO(binds: list varname)(io : actname)(args: list expr).
+
+  Fixpoint eval_expr(st: varmap)(e: expr): option (mword) :=
+    match e with
+    | ELit v => Some v
+    | EVar x => Common.get st x
+    | EOp op e1 e2 =>
+        bind_Some v1 <- eval_expr st e1;
+        bind_Some v2 <- eval_expr st e2;
+        Some (eval_binop op v1 v2)
+    end.
+
+  Section cont.
+    Context {T : Type}.
+    Inductive cont : Type :=
+    | CSuspended(_:T)
+    | CSeq(s1:cont) (s2: stmt)
+    | CStack(st: varmap)(c: cont)(binds rets: list varname).
+  End cont. Arguments cont : clear implicits.
+  Lemma cont_uninhabited (T:Set) (_:T -> False) (X : cont T) : False. Proof. induction X; auto 2. Qed.
+  Fixpoint lift_cont {A B : Set} (P : A -> B -> Prop) (a : cont A) (b : cont B) {struct a} :=
+    match a, b with
+    | CSuspended a, CSuspended b =>
+      P a b
+    | CSeq a sa, CSeq b sb =>
+      lift_cont P a b /\ sa = sb
+    | CStack sta a ba ra, CStack stb b bb rb =>
+      (forall v, Common.get sta v = Common.get stb v) /\ lift_cont P a b /\ ba = bb /\ ra = rb
+    | _, _ => False
+    end.
+
+  Definition ioact : Type := (list varname * actname * list mword).
+  Definition ioret : Type := (list varname * list mword).
+  
+  Section WithFunctions.
+    Context (lookupFunction : funname -> option (list varname * list varname * stmt)).
+    Fixpoint eval_stmt(f: nat)(st: varmap)(m: mem)(s: stmt): option (varmap*mem*option(cont ioact)) :=
+      match f with
+      | 0 => None (* out of fuel *)
+      | S f => match s with
+        | SLoad x a =>
+            bind_Some a <- eval_expr st a;
+            bind_Some v <- load a m;
+            Some (Common.put st x v, m, None)
+        | SStore a v =>
+            bind_Some a <- eval_expr st a;
+            bind_Some v <- eval_expr st v;
+            bind_Some m <- store a v m;
+            Some (st, m, None)
+        | SSet x e =>
+            bind_Some v <- eval_expr st e;
+            Some (Common.put st x v, m, None)
+        | SIf cond bThen bElse =>
+            bind_Some v <- eval_expr st cond;
+            eval_stmt f st m (if mword_nonzero v then bThen else bElse)
+        | SWhile cond body =>
+            bind_Some v <- eval_expr st cond;
+            if mword_nonzero v
+            then
+              bind_Some (st, m, c) <- eval_stmt f st m body;
+              match c with
+              | Some c => Some (st, m, Some (CSeq c (SWhile cond body)))
+              | None => eval_stmt f st m (SWhile cond body)
+              end
+            else Some (st, m, None)
+        | SSeq s1 s2 =>
+            bind_Some (st, m, c) <- eval_stmt f st m s1;
+            match c with
+            | Some c => Some (st, m, Some (CSeq c s2))
+            | None => eval_stmt f st m s2
+            end
+        | SSkip => Some (st, m, None)
+        | SCall binds fname args =>
+          bind_Some (params, rets, fbody) <- lookupFunction fname;
+          bind_Some argvs <- Common.option_all (List.map (eval_expr st) args);
+          bind_Some st0 <- Common.putmany params argvs Common.empty;
+          bind_Some (st1, m', oc) <- eval_stmt f st0 m fbody;
+          match oc with
+          | Some c => Some (st, m', Some (CStack st1 c binds rets))
+          | None => 
+            bind_Some retvs <- Common.option_all (List.map (Common.get st1) rets);
+            bind_Some st' <- Common.putmany binds retvs st;
+            Some (st', m', None)
+          end
+        | SIO binds ionum args =>
+          bind_Some argvs <- Common.option_all (List.map (eval_expr st) args);
+          Some (st, m, Some (CSuspended (binds, ionum, argvs)))
+        end
+      end.
+
+    Fixpoint eval_cont(f: nat)(st: varmap)(m: mem)(s: cont ioret): option (varmap*mem*option(cont ioact)) :=
+      match f with
+      | 0 => None (* out of fuel *)
+      | S f => match s with
+        | CSuspended (binds, retvs) =>
+            bind_Some st' <- Common.putmany binds retvs st;
+            Some (st', m, None)
+        | CSeq c s2 =>
+            bind_Some (st, m, oc) <- eval_cont f st m c;
+            match oc with
+            | Some c => Some (st, m, Some (CSeq c s2))
+            | None => eval_stmt f st m s2
+            end
+        | CStack stf cf binds rets =>
+          bind_Some (stf', m', oc) <- eval_cont f stf m cf;
+          match oc with
+          | Some c => Some (st, m', Some (CStack stf' c binds rets))
+          | None => 
+            bind_Some retvs <- Common.option_all (List.map (Common.get stf') rets);
+            bind_Some st' <- Common.putmany binds retvs st;
+            Some (st', m', None)
+          end
+        end
+      end.
+  End WithFunctions.
+End Language.
+
+
+
+
+
+
+
+
+
+
+(* TODO: refactor below here *)
+
+
+
+
+
+
+
+      
 Require Import Coq.Lists.List.
 Import ListNotations.
 Require Import lib.LibTacticsMin.
 Require Import riscv.util.BitWidths.
-Require Import compiler.Common.
 Require Import compiler.Tactics.
 Require Import compiler.Op.
 Require Import compiler.StateCalculus.
@@ -12,17 +207,13 @@ Require Import Coq.Program.Tactics.
 Require Import compiler.Memory.
 
 Section ExprImp1.
-
   Context {Bw: BitWidths}. (* bit width *)
-
   Context {Name: NameWithEq}.
   Notation var := (@name Name).
   Existing Instance eq_name_dec.
   Context {FName : NameWithEq}.
   Notation func := (@name FName).
   Context (ioaction : Set).
-
-
   Context {state: Set}.
   Context {stateMap: Map state var (word wXLEN)}.
   Context {vars: Type}.

From cc007a6e15ada3255d002b4d4d495a3190d5e062 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@kevix.co>
Date: Thu, 21 Jun 2018 11:24:10 -0400
Subject: [PATCH 6/7] refactor...

---
 src/Common.v  |   5 +-
 src/ExprImp.v | 573 +++++++++++++++++++++++---------------------------
 2 files changed, 265 insertions(+), 313 deletions(-)

diff --git a/src/Common.v b/src/Common.v
index 3fc59625..763a1844 100644
--- a/src/Common.v
+++ b/src/Common.v
@@ -1,7 +1,6 @@
 Require Export Coq.omega.Omega.
 Require Export Coq.Lists.List.
 Require Export bbv.Word.
-Require Export riscv.util.Monads.
 Require Export compiler.Decidable.
 Require Export compiler.Tactics.
 Require Export compiler.Set.
@@ -56,8 +55,8 @@ Section WithMap.
   Context {T} {K V} {TMap:Map T K V}.
   Fixpoint putmany (keys : list K) (values : list V) (init : T) {struct keys} : option T :=
     match keys, values with
-    | nil, nil => Return init
-    | b::binders, v::values => t <- putmany binders values init; Return (put t b v)
+    | nil, nil => Some init
+    | b::binders, v::values => match putmany binders values init with None => None | Some t => Some (put t b v) end
     | _, _ => None
     end.
 
diff --git a/src/ExprImp.v b/src/ExprImp.v
index 560e4d60..95cae88c 100644
--- a/src/ExprImp.v
+++ b/src/ExprImp.v
@@ -1,5 +1,10 @@
 Set Universe Polymorphism.
 Unset Universe Minimization ToSet.
+(* TODO: should we do this?
+Set Primitive Projections.
+Unset Printing Primitive Projection Parameters.
+*)
+Set Printing Projections.
 
 Require compiler.Common.
 
@@ -10,7 +15,9 @@ Local Notation "'bind_Some' x <- a ; f" :=
    end)
     (right associativity, at level 60, x pattern).
 
-Record LanguageParameters :=
+Module Imp. (* TODO: file *)
+
+Record ImpParameters :=
   {
     mword : Type;
     mword_nonzero : mword -> bool;
@@ -24,13 +31,13 @@ Record LanguageParameters :=
     varmap : Type;
     varmap_operations : Common.Map varmap varname mword;
 
-    eval_binop : bopname -> mword -> mword -> mword;
+    interp_binop : bopname -> mword -> mword -> mword;
     load : mword -> mem -> option mword;
     store : mword -> mword -> mem -> option mem;
   }.
 
-Section Language.
-  Context (p : LanguageParameters).
+Section Imp.
+  Context {p : ImpParameters}.
   (* RecordImport p (* COQBUG(https://github.com/coq/coq/issues/7808) *) *)
   Local Notation mword := p.(mword).
   Local Notation mword_nonzero := p.(mword_nonzero).
@@ -41,16 +48,16 @@ Section Language.
   Local Notation varmap := p.(varmap).
   Local Notation mem := p.(mem).
   Local Definition varmap_operations_ : Common.Map _ _ _ := p.(varmap_operations). Local Existing Instance varmap_operations_.
-  Local Notation eval_binop := p.(eval_binop).
+  Local Notation interp_binop := p.(interp_binop).
   Local Notation load := p.(load).
   Local Notation store := p.(store).
 
-  Inductive expr :=
+  Local Inductive expr :=
   | ELit(v: mword)
   | EVar(x: varname)
   | EOp(op: bopname) (e1 e2: expr).
 
-  Inductive stmt :=
+  Local Inductive stmt :=
   | SLoad(x: varname) (addr: expr)
   | SStore(addr val: expr)
   | SSet(x: varname)(e: expr)
@@ -61,81 +68,70 @@ Section Language.
   | SCall(binds: list varname)(f: funname)(args: list expr)
   | SIO(binds: list varname)(io : actname)(args: list expr).
 
-  Fixpoint eval_expr(st: varmap)(e: expr): option (mword) :=
+  Local Fixpoint interp_expr(st: varmap)(e: expr): option (mword) :=
     match e with
     | ELit v => Some v
     | EVar x => Common.get st x
     | EOp op e1 e2 =>
-        bind_Some v1 <- eval_expr st e1;
-        bind_Some v2 <- eval_expr st e2;
-        Some (eval_binop op v1 v2)
+        bind_Some v1 <- interp_expr st e1;
+        bind_Some v2 <- interp_expr st e2;
+        Some (interp_binop op v1 v2)
     end.
 
   Section cont.
     Context {T : Type}.
-    Inductive cont : Type :=
+    Local Inductive cont : Type :=
     | CSuspended(_:T)
     | CSeq(s1:cont) (s2: stmt)
     | CStack(st: varmap)(c: cont)(binds rets: list varname).
   End cont. Arguments cont : clear implicits.
-  Lemma cont_uninhabited (T:Set) (_:T -> False) (X : cont T) : False. Proof. induction X; auto 2. Qed.
-  Fixpoint lift_cont {A B : Set} (P : A -> B -> Prop) (a : cont A) (b : cont B) {struct a} :=
-    match a, b with
-    | CSuspended a, CSuspended b =>
-      P a b
-    | CSeq a sa, CSeq b sb =>
-      lift_cont P a b /\ sa = sb
-    | CStack sta a ba ra, CStack stb b bb rb =>
-      (forall v, Common.get sta v = Common.get stb v) /\ lift_cont P a b /\ ba = bb /\ ra = rb
-    | _, _ => False
-    end.
 
-  Definition ioact : Type := (list varname * actname * list mword).
-  Definition ioret : Type := (list varname * list mword).
+  Local Definition ioact : Type := (list varname * actname * list mword).
+  Local Definition ioret : Type := (list varname * list mword).
   
   Section WithFunctions.
     Context (lookupFunction : funname -> option (list varname * list varname * stmt)).
-    Fixpoint eval_stmt(f: nat)(st: varmap)(m: mem)(s: stmt): option (varmap*mem*option(cont ioact)) :=
+    Local Fixpoint interp_stmt(f: nat)(st: varmap)(m: mem)(s: stmt): option (varmap*mem*option(cont ioact)) :=
       match f with
       | 0 => None (* out of fuel *)
       | S f => match s with
         | SLoad x a =>
-            bind_Some a <- eval_expr st a;
+            bind_Some a <- interp_expr st a;
             bind_Some v <- load a m;
             Some (Common.put st x v, m, None)
         | SStore a v =>
-            bind_Some a <- eval_expr st a;
-            bind_Some v <- eval_expr st v;
+            bind_Some a <- interp_expr st a;
+            bind_Some v <- interp_expr st v;
             bind_Some m <- store a v m;
             Some (st, m, None)
         | SSet x e =>
-            bind_Some v <- eval_expr st e;
+            bind_Some v <- interp_expr st e;
             Some (Common.put st x v, m, None)
         | SIf cond bThen bElse =>
-            bind_Some v <- eval_expr st cond;
-            eval_stmt f st m (if mword_nonzero v then bThen else bElse)
+            bind_Some v <- interp_expr st cond;
+            interp_stmt f st m (if mword_nonzero v then bThen else bElse)
         | SWhile cond body =>
-            bind_Some v <- eval_expr st cond;
+            bind_Some v <- interp_expr st cond;
             if mword_nonzero v
             then
-              bind_Some (st, m, c) <- eval_stmt f st m body;
+              bind_Some (st, m, c) <- interp_stmt f st m body;
               match c with
               | Some c => Some (st, m, Some (CSeq c (SWhile cond body)))
-              | None => eval_stmt f st m (SWhile cond body)
+              | None => interp_stmt f st m (SWhile cond body)
               end
             else Some (st, m, None)
         | SSeq s1 s2 =>
-            bind_Some (st, m, c) <- eval_stmt f st m s1;
+            bind_Some (st, m, c) <- interp_stmt f st m s1;
             match c with
             | Some c => Some (st, m, Some (CSeq c s2))
-            | None => eval_stmt f st m s2
+            | None => interp_stmt f st m s2
             end
         | SSkip => Some (st, m, None)
         | SCall binds fname args =>
           bind_Some (params, rets, fbody) <- lookupFunction fname;
-          bind_Some argvs <- Common.option_all (List.map (eval_expr st) args);
+          bind_Some argvs <- Common.option_all (List.map (interp_expr st) args);
           bind_Some st0 <- Common.putmany params argvs Common.empty;
-          bind_Some (st1, m', oc) <- eval_stmt f st0 m fbody;
+          bind_Some (st1, m', oc) <- interp_stmt f st0 m fbody;
           match oc with
           | Some c => Some (st, m', Some (CStack st1 c binds rets))
           | None => 
@@ -144,12 +140,12 @@ Section Language.
             Some (st', m', None)
           end
         | SIO binds ionum args =>
-          bind_Some argvs <- Common.option_all (List.map (eval_expr st) args);
+          bind_Some argvs <- Common.option_all (List.map (interp_expr st) args);
           Some (st, m, Some (CSuspended (binds, ionum, argvs)))
         end
       end.
 
-    Fixpoint eval_cont(f: nat)(st: varmap)(m: mem)(s: cont ioret): option (varmap*mem*option(cont ioact)) :=
+    Local Fixpoint interp_cont(f: nat)(st: varmap)(m: mem)(s: cont ioret): option (varmap*mem*option(cont ioact)) :=
       match f with
       | 0 => None (* out of fuel *)
       | S f => match s with
@@ -157,13 +153,13 @@ Section Language.
             bind_Some st' <- Common.putmany binds retvs st;
             Some (st', m, None)
         | CSeq c s2 =>
-            bind_Some (st, m, oc) <- eval_cont f st m c;
+            bind_Some (st, m, oc) <- interp_cont f st m c;
             match oc with
             | Some c => Some (st, m, Some (CSeq c s2))
-            | None => eval_stmt f st m s2
+            | None => interp_stmt f st m s2
             end
         | CStack stf cf binds rets =>
-          bind_Some (stf', m', oc) <- eval_cont f stf m cf;
+          bind_Some (stf', m', oc) <- interp_cont f stf m cf;
           match oc with
           | Some c => Some (st, m', Some (CStack stf' c binds rets))
           | None => 
@@ -173,27 +169,80 @@ Section Language.
           end
         end
       end.
-  End WithFunctions.
-End Language.
-
-
-
-
-
 
+  End WithFunctions.
+  Record ImpType :=
+    {
+      _expr : Type;
+      _stmt : Type;
+      _cont : Type -> Type;
+      _interp_expr : forall (st: varmap)(e: expr), option (mword);
+      _interp_stmt : forall (lookupFunction : funname -> option (list varname * list varname * stmt))(f: nat)(st: varmap)(m: mem)(s: stmt),       option (varmap*mem*option(cont ioact));
+      _interp_cont : forall (lookupFunction : funname -> option (list varname * list varname * stmt))(f: nat)(st: varmap)(m: mem)(s: cont ioret), option (varmap*mem*option(cont ioact));
+    }.
+  Definition Imp : ImpType := Build_ImpType expr stmt cont interp_expr interp_stmt interp_cont.
+End Imp.
+Arguments ImpType : clear implicits.
+Arguments Imp : clear implicits.
 
+End Imp. (* TODO: file *)
 
 
 
-(* TODO: refactor below here *)
+Require riscv.util.BitWidths.
+Require compiler.Memory.
+Require compiler.Op.
 
+Module RISCVImp. (* TODO: file *)
 
+Record RISCVImpParameters :=
+  {
+    bw : riscv.util.BitWidths.BitWidths;
+    varname : Type;
+    funname : Type;
+    actname : Type;
+    varmap : Type;
+    varmap_operations : Common.Map varmap varname (bbv.Word.word (riscv.util.BitWidths.wXLEN));
+  }.
 
+Definition ImpParameters_of_RISCVImpParameters (p:RISCVImpParameters): Imp.ImpParameters :=
+  {|
+    Imp.mword := bbv.Word.word (@riscv.util.BitWidths.wXLEN p.(bw));
+    Imp.mword_nonzero := fun v => if bbv.Word.weq v (bbv.Word.wzero _) then false else true;
+    Imp.varname := p.(varname);
+    Imp.funname := p.(funname);
+    Imp.actname := p.(actname);
+    Imp.bopname := compiler.Op.binop;
+    Imp.mem := compiler.Memory.mem;
+
+    Imp.interp_binop := compiler.Op.eval_binop;
+    Imp.load := Memory.read_mem;
+    Imp.store := Memory.write_mem;
+
+    Imp.varmap := p.(varmap);
+    Imp.varmap_operations := p.(varmap_operations);
+  |}.
+Definition RISCVImp (p:RISCVImpParameters) : Imp.ImpType (ImpParameters_of_RISCVImpParameters p)
+  := Imp.Imp (ImpParameters_of_RISCVImpParameters p).
 
+(*
+Eval cbv [RISCVImp ImpParameters_of_RISCVImpParameters
+                   RISCVImp.bw
+                   RISCVImp.varname
+                   RISCVImp.funname
+                   RISCVImp.actname
+                   RISCVImp.varmap
+                   RISCVImp.varmap_operations
+         ] in
+    fun bw varname funnname actname varmap varmap_operations =>
+      RISCVImp (Build_RISCVImpParameters bw varname funnname actname varmap varmap_operations).
+*)
 
+End RISCVImp. (* TODO: file *)
 
 
-      
+(* TODO: file*)
+Require Import compiler.Common.
 Require Import Coq.Lists.List.
 Import ListNotations.
 Require Import lib.LibTacticsMin.
@@ -206,56 +255,33 @@ Require Import compiler.NameWithEq.
 Require Import Coq.Program.Tactics.
 Require Import compiler.Memory.
 
-Section ExprImp1.
-  Context {Bw: BitWidths}. (* bit width *)
-  Context {Name: NameWithEq}.
-  Notation var := (@name Name).
-  Existing Instance eq_name_dec.
-  Context {FName : NameWithEq}.
-  Notation func := (@name FName).
-  Context (ioaction : Set).
-  Context {state: Set}.
-  Context {stateMap: Map state var (word wXLEN)}.
-  Context {vars: Type}.
-  Context {varset: set vars var}.
-
-  Ltac state_calc := state_calc_generic (@name Name) (word wXLEN).
-  Ltac set_solver := set_solver_generic (@name Name).
-
-  Inductive expr: Set :=
-    | ELit(v: word wXLEN): expr
-    | EVar(x: var): expr
-    | EOp(op: binop)(e1 e2: expr): expr.
-
-  Inductive stmt: Set :=
-    | SLoad(x: var)(addr: expr): stmt
-    | SStore(addr val: expr): stmt
-    | SSet(x: var)(e: expr): stmt
-    | SIf(cond: expr)(bThen bElse: stmt): stmt
-    | SWhile(cond: expr)(body: stmt): stmt
-    | SSeq(s1 s2: stmt): stmt
-    | SSkip: stmt
-    | SCall(binds: list var)(f: func)(args: list expr)
-    | SIO(binds: list var)(io : ioaction)(args: list expr).
-
-  Fixpoint eval_expr(st: state)(e: expr): option (word wXLEN) :=
-    match e with
-    | ELit v => Return v
-    | EVar x => get st x
-    | EOp op e1 e2 =>
-        v1 <- eval_expr st e1;
-        v2 <- eval_expr st e2;
-        Return (eval_binop op v1 v2)
-    end.
-
-  Section cont.
-    Context {T : Set}.
-    Inductive cont : Set :=
-    | CSuspended (_:T)
-    | CSeq(s1:cont) (s2: stmt)
-    | CStack(st: state)(c: cont)(binds rets: list var).
-  End cont. Arguments cont : clear implicits.
-  Lemma cont_uninhabited (T:Set) (_:T -> False) (X : cont T) : False. Proof. induction X; eauto. Qed.
+Module ImpProperties.
+Section ImpProperties.
+  Import Imp.
+  Context (p:ImpParameters).
+  Let Imp : Imp.ImpType p := Imp.Imp p.
+  (* RecordImport p (* COQBUG(https://github.com/coq/coq/issues/7808) *) *)
+  Local Notation mword := p.(mword).
+  Local Notation mword_nonzero := p.(mword_nonzero).
+  Local Notation varname := p.(varname).
+  Local Notation funname := p.(funname).
+  Local Notation actname := p.(actname).
+  Local Notation bopname := p.(bopname).
+  Local Notation varmap := p.(varmap).
+  Local Notation mem := p.(mem).
+  Local Definition varmap_operations_ : Common.Map _ _ _ := p.(varmap_operations). Local Existing Instance varmap_operations_.
+  Local Notation interp_binop := p.(interp_binop).
+  Local Notation load := p.(load).
+  Local Notation store := p.(store).
+  (* RecordImport Imp (* COQBUG(https://github.com/coq/coq/issues/7808) *) *)
+  Local Notation expr := Imp.(_expr).
+  Local Notation stmt := Imp.(_stmt).
+  Local Notation cont := Imp.(_cont).
+  Local Notation interp_expr := Imp.(_interp_expr).
+  Local Notation interp_stmt := Imp.(_interp_stmt).
+  Local Notation interp_cont := Imp.(_interp_cont).
+  
+  Lemma cont_uninhabited (T:Set) (_:T -> False) (X : cont T) : False. Proof. induction X; auto 2. Qed.
   Fixpoint lift_cont {A B : Set} (P : A -> B -> Prop) (a : cont A) (b : cont B) {struct a} :=
     match a, b with
     | CSuspended a, CSuspended b =>
@@ -263,193 +289,113 @@ Section ExprImp1.
     | CSeq a sa, CSeq b sb =>
       lift_cont P a b /\ sa = sb
     | CStack sta a ba ra, CStack stb b bb rb =>
-      (forall vss, agree_on sta vss stb) /\ lift_cont P a b /\ ba = bb /\ ra = rb
+      (forall v, Common.get sta v = Common.get stb v) /\ lift_cont P a b /\ ba = bb /\ ra = rb
     | _, _ => False
     end.
 
-  Definition ioact : Set := (list var * ioaction * list (word (wXLEN))).
-  Definition ioret : Set := (list var * list (word wXLEN)).
-  Section WithEnv.
-    Context {env} {funcMap: Map env func (list var * list var * stmt)} (e:env).
-    Fixpoint eval_stmt(f: nat)(st: state)(m: mem)(s: stmt): option (state*mem*option(cont ioact)) :=
-      match f with
-      | 0 => None (* out of fuel *)
-      | S f => match s with
-        | SLoad x a =>
-            a <- eval_expr st a;
-            v <- read_mem a m;
-            Return (put st x v, m, None)
-        | SStore a v =>
-            a <- eval_expr st a;
-            v <- eval_expr st v;
-            m <- write_mem a v m;
-            Return (st, m, None)
-        | SSet x e =>
-            v <- eval_expr st e;
-            Return (put st x v, m, None)
-        | SIf cond bThen bElse =>
-            v <- eval_expr st cond;
-            eval_stmt f st m (if weq v $0 then bElse else bThen)
-        | SWhile cond body =>
-            v <- eval_expr st cond;
-            if weq v $0 then Return (st, m, None) else
-              p <- eval_stmt f st m body;
-              let '(st, m, c) := p in
-              match c with
-              | Some c => Return (st, m, Some (CSeq c (SWhile cond body)))
-              | None => eval_stmt f st m (SWhile cond body)
-              end
-        | SSeq s1 s2 =>
-            p <- eval_stmt f st m s1;
-            let '(st, m, c) := p in
-            match c with
-            | Some c => Return (st, m, Some (CSeq c s2))
-            | None => eval_stmt f st m s2
-            end
-        | SSkip => Return (st, m, None)
-        | SCall binds fname args =>
-          fimpl <- get e fname;
-          let '(params, rets, fbody) := fimpl in
-          argvs <- option_all (map (eval_expr st) args);
-          st0 <- putmany params argvs empty;
-          st1m' <- eval_stmt f st0 m fbody;
-          let '(st1, m', c) := st1m' in
-          match c with
-          | Some c => Return (st, m', Some (CStack st1 c binds rets))
-          | None => 
-            retvs <- option_all (map (get st1) rets);
-            st' <- putmany binds retvs st;
-            Return (st', m', None)
-          end
-        | SIO binds ionum args =>
-          argvs <- option_all (map (eval_expr st) args);
-          Return (st, m, Some (CSuspended (binds, ionum, argvs)))
-        end
-      end.
-
-    Fixpoint eval_cont(f: nat)(st: state)(m: mem)(s: cont ioret): option (state*mem*option(cont ioact)) :=
-      match f with
-      | 0 => None (* out of fuel *)
-      | S f => match s with
-        | CSuspended (binds, retvs) =>
-            st' <- putmany binds retvs st;
-            Return (st', m, None)
-        | CSeq c s2 =>
-            p <- eval_cont f st m c;
-            let '(st, m, oc) := p in
-            match oc with
-            | Some c => Return (st, m, Some (CSeq c s2))
-            | None => eval_stmt f st m s2
-            end
-        | CStack stf cf binds rets =>
-          stf'm' <- eval_cont f stf m cf;
-          let '(stf', m', oc) := stf'm' in
-          match oc with
-          | Some c => Return (st, m', Some (CStack stf' c binds rets))
-          | None => 
-            retvs <- option_all (map (get stf') rets);
-            st' <- putmany binds retvs st;
-            Return (st', m', None)
-          end
-        end
-      end.
-
-    Fixpoint expr_size(e: expr): nat :=
-      match e with
-      | ELit _ => 8
-      | EVar _ => 1
-      | EOp op e1 e2 => S (S (expr_size e1 + expr_size e2))
-      end.
+  Fixpoint expr_size(e: expr): nat :=
+    match e with
+    | ELit _ => 8
+    | EVar _ => 1
+    | EOp op e1 e2 => S (S (expr_size e1 + expr_size e2))
+    end.
 
-    Fixpoint stmt_size(s: stmt): nat :=
-      match s with
-      | SLoad x a => S (expr_size a)
-      | SStore a v => S (expr_size a + expr_size v)
-      | SSet x e => S (expr_size e)
-      | SIf cond bThen bElse => S (expr_size cond + stmt_size bThen + stmt_size bElse)
-      | SWhile cond body => S (expr_size cond + stmt_size body)
-      | SSeq s1 s2 => S (stmt_size s1 + stmt_size s2)
-      | SSkip => 1
-      | SCall binds _ args | SIO binds _ args =>
-          S (length binds + length args + List.fold_right Nat.add O (List.map expr_size args))
-      end.
+  Fixpoint stmt_size(s: stmt): nat :=
+    match s with
+    | SLoad x a => S (expr_size a)
+    | SStore a v => S (expr_size a + expr_size v)
+    | SSet x e => S (expr_size e)
+    | SIf cond bThen bElse => S (expr_size cond + stmt_size bThen + stmt_size bElse)
+    | SWhile cond body => S (expr_size cond + stmt_size body)
+    | SSeq s1 s2 => S (stmt_size s1 + stmt_size s2)
+    | SSkip => 1
+    | SCall binds _ args | SIO binds _ args =>
+                           S (length binds + length args + List.fold_right Nat.add O (List.map expr_size args))
+    end.
 
-    Local Ltac inversion_lemma :=
-      intros;
-      simpl in *;
-      repeat (destruct_one_match_hyp; try discriminate);
-      inversionss;
-      eauto 16.
-
-    Lemma invert_eval_SLoad: forall fuel initialSt initialM x e final,
-      eval_stmt (S fuel) initialSt initialM (SLoad x e) = Some final ->
-      exists a v, eval_expr initialSt e = Some a /\
-                  read_mem a initialM = Some v /\
-                  final = (put initialSt x v, initialM).
-    Proof. inversion_lemma. Qed.
-
-    Lemma invert_eval_SStore: forall fuel initialSt initialM a v final,
-      eval_stmt (S fuel) initialSt initialM (SStore a v) = Some final ->
-      exists av vv finalM, eval_expr initialSt a = Some av /\
-                           eval_expr initialSt v = Some vv /\
-                           write_mem av vv initialM = Some finalM /\
-                           final = (initialSt, finalM).
-    Proof. inversion_lemma. Qed.
-
-    Lemma invert_eval_SSet: forall f st1 m1 p2 x e,
-      eval_stmt (S f) st1 m1 (SSet x e) = Some p2 ->
-      exists v, eval_expr st1 e = Some v /\ p2 = (put st1 x v, m1).
-    Proof. inversion_lemma. Qed.
-
-    Lemma invert_eval_SIf: forall f st1 m1 p2 cond bThen bElse,
-      eval_stmt (S f) st1 m1 (SIf cond bThen bElse) = Some p2 ->
-      exists cv,
-        eval_expr st1 cond = Some cv /\ 
-        (cv <> $0 /\ eval_stmt f st1 m1 bThen = Some p2 \/
-         cv = $0  /\ eval_stmt f st1 m1 bElse = Some p2).
-    Proof. inversion_lemma. Qed.
-
-    Lemma invert_eval_SWhile: forall st1 m1 p3 f cond body,
-      eval_stmt (S f) st1 m1 (SWhile cond body) = Some p3 ->
-      exists cv,
-        eval_expr st1 cond = Some cv /\
-        (cv <> $0 /\ (exists st2 m2, eval_stmt f st1 m1 body = Some (st2, m2) /\ 
-                                     eval_stmt f st2 m2 (SWhile cond body) = Some p3) \/
-         cv = $0  /\ p3 = (st1, m1)).
-    Proof. inversion_lemma. Qed.
-
-    Lemma invert_eval_SSeq: forall st1 m1 p3 f s1 s2,
-      eval_stmt (S f) st1 m1 (SSeq s1 s2) = Some p3 ->
-      exists st2 m2, eval_stmt f st1 m1 s1 = Some (st2, m2) /\ eval_stmt f st2 m2 s2 = Some p3.
-    Proof. inversion_lemma. Qed.
-
-    Lemma invert_eval_SSkip: forall st1 m1 p2 f,
-      eval_stmt (S f) st1 m1 SSkip = Some p2 ->
-      p2 = (st1, m1).
-    Proof. inversion_lemma. Qed.
-
-    Lemma invert_eval_SCall : forall st m1 p2 f binds fname args,
-      eval_stmt (S f) st m1 (SCall binds fname args) = Some p2 ->
-      exists params rets fbody argvs st0 st1 m' retvs st',
-        get e fname = Some (params, rets, fbody) /\
-        option_all (map (eval_expr st) args) = Some argvs /\
-        putmany params argvs empty = Some st0 /\
-        eval_stmt f st0 m1 fbody = Some (st1, m') /\
-        option_all (map (get st1) rets) = Some retvs /\
-        putmany binds retvs st = Some st' /\
-        p2 = (st', m').
-    Proof. inversion_lemma. Qed.
-  End WithEnv.
+  Local Ltac inversion_lemma :=
+    intros;
+    simpl in *;
+    repeat (destruct_one_match_hyp; try discriminate);
+    inversionss;
+    eauto 99.
+
+  Lemma invert_interp_SLoad: forall env fuel initialSt initialM x e final,
+      interp_stmt env (S fuel) initialSt initialM (SLoad x e) = Some final ->
+      exists a v, interp_expr initialSt e = Some a /\
+                  load a initialM = Some v /\
+                  final = (put initialSt x v, initialM, None).
+  Proof. inversion_lemma. Qed.
+
+  Lemma invert_interp_SStore: forall env fuel initialSt initialM a v final,
+    interp_stmt env (S fuel) initialSt initialM (SStore a v) = Some final ->
+    exists av vv finalM, interp_expr initialSt a = Some av /\
+                         interp_expr initialSt v = Some vv /\
+                         store av vv initialM = Some finalM /\
+                         final = (initialSt, finalM, None).
+  Proof. inversion_lemma. Qed.
+
+  Lemma invert_interp_SSet: forall env f st1 m1 p2 x e,
+    interp_stmt env (S f) st1 m1 (SSet x e) = Some p2 ->
+    exists v, interp_expr st1 e = Some v /\ p2 = (put st1 x v, m1, None).
+  Proof. inversion_lemma. Qed.
+
+  Lemma invert_interp_SIf: forall env f st1 m1 p2 cond bThen bElse,
+    interp_stmt env (S f) st1 m1 (SIf cond bThen bElse) = Some p2 ->
+    exists cv,
+      interp_expr st1 cond = Some cv /\ 
+      (mword_nonzero cv = true /\ interp_stmt env f st1 m1 bThen = Some p2 \/
+       mword_nonzero cv = false /\ interp_stmt env f st1 m1 bElse = Some p2).
+  Proof. inversion_lemma. Qed.
+
+  Lemma invert_interp_SSkip: forall env st1 m1 p2 f,
+    interp_stmt env (S f) st1 m1 SSkip = Some p2 ->
+    p2 = (st1, m1, None).
+  Proof. inversion_lemma. Qed.
+
+  Lemma invert_interp_SSeq: forall env st1 m1 p3 f s1 s2,
+    interp_stmt env (S f) st1 m1 (SSeq s1 s2) = Some p3 ->
+    exists st2 m2 oc, interp_stmt env f st1 m1 s1 = Some (st2, m2, oc) /\ (
+        (oc = None /\ interp_stmt env f st2 m2 s2 = Some p3)
+     \/ (exists c, oc = Some c /\ p3 = (st2, m2, Some (CSeq c s2)))).
+  Proof. inversion_lemma. Qed.
+
+  Lemma invert_interp_SWhile: forall env st1 m1 p3 f cond body,
+    interp_stmt env (S f) st1 m1 (SWhile cond body) = Some p3 ->
+    exists cv,
+      interp_expr st1 cond = Some cv /\
+      (mword_nonzero cv = true /\
+       (exists st2 m2 oc, interp_stmt env f st1 m1 body = Some (st2, m2, oc) /\
+              ( oc = None /\ interp_stmt env f st2 m2 (SWhile cond body) = Some p3)
+           \/ ( exists c, oc = Some c /\ p3 = (st2, m2, Some (CSeq c (SWhile cond body)))))
+       \/ mword_nonzero cv = false /\ p3 = (st1, m1, None)).
+  Proof. inversion_lemma. Qed.
+
+  Lemma invert_interp_SCall : forall env st m1 p2 f binds fname args,
+    interp_stmt env (S f) st m1 (SCall binds fname args) = Some p2 ->
+    exists params rets fbody argvs st0 st1 m' oc,
+      env fname = Some (params, rets, fbody) /\
+      option_all (map (interp_expr st) args) = Some argvs /\
+      putmany params argvs empty = Some st0 /\
+      interp_stmt env f st0 m1 fbody = Some (st1, m', oc) /\ (
+       ( oc = None /\ exists retvs st',
+         option_all (map (get st1) rets) = Some retvs /\
+         putmany binds retvs st = Some st' /\
+         p2 = (st', m', None)
+       ) \/
+       ( exists c, oc = Some c /\
+         p2 = (st, m', Some (CStack st1 c binds rets)) ) ).
+  Proof. inversion_lemma. Qed.
 
   (* Returns a list to make it obvious that it's a finite set. *)
-  Fixpoint allVars_expr(e: expr): list var :=
+  Fixpoint allVars_expr(e: expr): list varname :=
     match e with
     | ELit v => []
     | EVar x => [x]
     | EOp op e1 e2 => (allVars_expr e1) ++ (allVars_expr e2)
     end.
 
-  Fixpoint allVars_stmt(s: stmt): list var := 
+  Fixpoint allVars_stmt(s: stmt): list varname := 
     match s with
     | SLoad v e => v :: allVars_expr e
     | SStore a e => (allVars_expr a) ++ (allVars_expr e)
@@ -458,12 +404,15 @@ Section ExprImp1.
     | SWhile c body => (allVars_expr c) ++ (allVars_stmt body)
     | SSeq s1 s2 => (allVars_stmt s1) ++ (allVars_stmt s2)
     | SSkip => []
-    | SCall binds _ args => binds ++ List.fold_right (@List.app _) nil (List.map allVars_expr args)
+    | SCall binds _ args | SIO binds _ args => binds ++ List.fold_right (@List.app _) nil (List.map allVars_expr args)
     end.
 
+  Context {set_varname: Type}.
+  Context {varset: set set_varname varname}.
+
   (* Returns a static approximation of the set of modified vars.
      The returned set might be too big, but is guaranteed to include all modified vars. *)
-  Fixpoint modVars(s: stmt): vars := 
+  Fixpoint modVars(s: stmt): set_varname := 
     match s with
     | SLoad v _ => singleton_set v
     | SStore _ _ => empty_set
@@ -472,48 +421,49 @@ Section ExprImp1.
     | SWhile _ body => modVars body
     | SSeq s1 s2 => union (modVars s1) (modVars s2)
     | SSkip => empty_set
-    | SCall binds _ _ => of_list binds
+    | SCall binds _ _ | SIO binds _ _ => of_list binds
     end.
 
+  Ltac set_solver := set_solver_generic constr:(varname).
+  Ltac state_calc := state_calc_generic constr:(varname) (word wXLEN).
+  
   Lemma modVars_subset_allVars: forall x s,
     x \in modVars s ->
     In x (allVars_stmt s).
   Proof.
     intros.
     induction s; simpl in *.
-    - set_solver.
-    - set_solver.
-    - apply singleton_set_spec in H. auto.
-    - apply union_spec in H.
+    { set_solver. }
+    { set_solver. }
+    { apply singleton_set_spec in H. auto. }
+    { apply union_spec in H.
       apply in_or_app. right. apply in_or_app.
-      destruct H as [H|H]; auto.
-    - apply in_or_app. right. auto.
-    - apply union_spec in H.
+      destruct H as [H|H]; auto. }
+    { apply in_or_app. right. auto. }
+    { apply union_spec in H.
       apply in_or_app.
-      destruct H as [H|H]; auto.
-    - eapply empty_set_spec. eassumption.
-    - generalize dependent binds; induction binds; intros H; cbn in *.
-      + apply empty_set_spec in H; destruct H.
-      + apply union_spec in H; destruct H.
-        * left. apply singleton_set_spec in H. auto.
-        * right. auto.
+      destruct H as [H|H]; auto. }
+    { eapply empty_set_spec. eassumption. }
+    1,2 : generalize dependent binds; induction binds; intros H; cbn in *;
+      [ apply empty_set_spec in H; destruct H
+      | apply union_spec in H; destruct H;
+        [ left; apply singleton_set_spec in H; auto
+        | right; auto ] ].
   Qed.
+End ImpProperties.
 
-End ExprImp1.
-
-
-Ltac invert_eval_stmt :=
+Ltac invert_interp_stmt :=
   lazymatch goal with
-  | E: eval_stmt _ (S ?fuel) _ _ ?s = Some _ |- _ =>
+  | E: Imp.interp_stmt _ (S ?fuel) _ _ ?s = Some _ |- _ =>
     destruct s;
-    [ apply invert_eval_SLoad in E
-    | apply invert_eval_SStore in E
-    | apply invert_eval_SSet in E
-    | apply invert_eval_SIf in E
-    | apply invert_eval_SWhile in E
-    | apply invert_eval_SSeq in E
-    | apply invert_eval_SSkip in E
-    | apply invert_eval_SCall in E
+    [ apply invert_interp_SLoad in E
+    | apply invert_interp_SStore in E
+    | apply invert_interp_SSet in E
+    | apply invert_interp_SIf in E
+    | apply invert_interp_SWhile in E
+    | apply invert_interp_SSeq in E
+    | apply invert_interp_SSkip in E
+    | apply invert_interp_SCall in E
     ];
     deep_destruct E;
     [ let x := fresh "Case_SLoad" in pose proof tt as x; move x at top
@@ -529,6 +479,9 @@ Ltac invert_eval_stmt :=
     ]
   end.
 
+End ImpProperties. (* TODO: file *)
+
+
 
 Section ExprImp2.
 
@@ -548,12 +501,12 @@ Section ExprImp2.
   Ltac state_calc := state_calc_generic (@name Name) (word wXLEN).
 
   Lemma modVarsSound: forall env fuel s initialS initialM finalS finalM,
-    eval_stmt env fuel initialS initialM s = Some (finalS, finalM) ->
+    interp_stmt env fuel initialS initialM s = Some (finalS, finalM) ->
     only_differ initialS (modVars s) finalS.
   Proof.
     induction fuel; introv Ev.
     - discriminate.
-    - invert_eval_stmt; simpl in *; inversionss;
+    - invert_interp_stmt; simpl in *; inversionss;
       repeat match goal with
       | IH: _, H: _ |- _ =>
           let IH' := fresh IH in pose proof IH as IH';
@@ -610,7 +563,7 @@ Definition isRight(x y z: word 32) :=
                                (EOp OTimes (EVar _c) (EVar _c)))).
 
 Definition run_isRight(x y z: word 32): option (word 32) :=
-  final <- (eval_stmt empty 10 empty no_mem (isRight x y z));
+  final <- (interp_stmt empty 10 empty no_mem (isRight x y z));
   let '(finalSt, finalM) := final in
   get finalSt _isRight.
 

From 2f41000821c54839b797d9915bcbf5cbc095a9cf Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@kevix.co>
Date: Thu, 21 Jun 2018 13:30:31 -0400
Subject: [PATCH 7/7] build ExprImp excluding example

---
 src/ExprImp.v | 135 ++++++++++++++++++++++++++------------------------
 1 file changed, 70 insertions(+), 65 deletions(-)

diff --git a/src/ExprImp.v b/src/ExprImp.v
index 95cae88c..adfc695d 100644
--- a/src/ExprImp.v
+++ b/src/ExprImp.v
@@ -47,7 +47,7 @@ Section Imp.
   Local Notation bopname := p.(bopname).
   Local Notation varmap := p.(varmap).
   Local Notation mem := p.(mem).
-  Local Definition varmap_operations_ : Common.Map _ _ _ := p.(varmap_operations). Local Existing Instance varmap_operations_.
+  Local Definition varmap_operations_ : Common.Map _ _ _ := p.(varmap_operations). Global Existing Instance varmap_operations_.
   Local Notation interp_binop := p.(interp_binop).
   Local Notation load := p.(load).
   Local Notation store := p.(store).
@@ -241,7 +241,7 @@ Eval cbv [RISCVImp ImpParameters_of_RISCVImpParameters
 End RISCVImp. (* TODO: file *)
 
 
-(* TODO: file*)
+
 Require Import compiler.Common.
 Require Import Coq.Lists.List.
 Import ListNotations.
@@ -255,8 +255,8 @@ Require Import compiler.NameWithEq.
 Require Import Coq.Program.Tactics.
 Require Import compiler.Memory.
 
-Module ImpProperties.
-Section ImpProperties.
+Module ImpInversion. (* TODO: file*)
+Section ImpInversion.
   Import Imp.
   Context (p:ImpParameters).
   Let Imp : Imp.ImpType p := Imp.Imp p.
@@ -269,7 +269,6 @@ Section ImpProperties.
   Local Notation bopname := p.(bopname).
   Local Notation varmap := p.(varmap).
   Local Notation mem := p.(mem).
-  Local Definition varmap_operations_ : Common.Map _ _ _ := p.(varmap_operations). Local Existing Instance varmap_operations_.
   Local Notation interp_binop := p.(interp_binop).
   Local Notation load := p.(load).
   Local Notation store := p.(store).
@@ -365,9 +364,9 @@ Section ImpProperties.
     exists cv,
       interp_expr st1 cond = Some cv /\
       (mword_nonzero cv = true /\
-       (exists st2 m2 oc, interp_stmt env f st1 m1 body = Some (st2, m2, oc) /\
+       (exists st2 m2 oc, interp_stmt env f st1 m1 body = Some (st2, m2, oc) /\ (
               ( oc = None /\ interp_stmt env f st2 m2 (SWhile cond body) = Some p3)
-           \/ ( exists c, oc = Some c /\ p3 = (st2, m2, Some (CSeq c (SWhile cond body)))))
+           \/ ( exists c, oc = Some c /\ p3 = (st2, m2, Some (CSeq c (SWhile cond body))))))
        \/ mword_nonzero cv = false /\ p3 = (st1, m1, None)).
   Proof. inversion_lemma. Qed.
 
@@ -387,6 +386,59 @@ Section ImpProperties.
          p2 = (st, m', Some (CStack st1 c binds rets)) ) ).
   Proof. inversion_lemma. Qed.
 
+  Lemma invert_interp_SIO : forall env st m1 p2 f binds ioname args,
+    interp_stmt env (S f) st m1 (SIO binds ioname args) = Some p2 ->
+    exists argvs, option_all (map (Imp.interp_expr st) args) = Some argvs /\
+                  p2 = (st, m1, Some (CSuspended (binds, ioname, argvs))).
+  Proof. inversion_lemma. Qed.
+End ImpInversion.
+
+Local Tactic Notation "marker" ident(s) := let x := fresh s in pose proof tt as x; move x at top.
+Ltac invert_interp_stmt :=
+  lazymatch goal with
+  | E: Imp._interp_stmt _ _ (S ?fuel) _ _ ?s = Some _ |- _ =>
+    destruct s;
+    [ apply invert_interp_SLoad in E; deep_destruct E; marker SLoad
+    | apply invert_interp_SStore in E; deep_destruct E; marker SStore
+    | apply invert_interp_SSet in E; deep_destruct E; marker SSet
+    | apply invert_interp_SIf in E; deep_destruct E; [marker SIf_true | marker SIf_false]
+    | apply invert_interp_SWhile in E; deep_destruct E; [marker SWhile_true | marker SWhile_blocked | marker SWhile_false ]
+    | apply invert_interp_SSeq in E; deep_destruct E; [marker SSeq | marker SSeq_blocked ]
+    | apply invert_interp_SSkip in E; deep_destruct E; marker SSkip
+    | apply invert_interp_SCall in E; deep_destruct E; [marker SCall | marker SCall_blocked]
+    | apply invert_interp_SIO in E; deep_destruct E; [marker SIO ]
+    ] end.
+End ImpInversion. (* TODO: file *)
+
+Module ImpVars. (* TODO: file *)
+Import ImpInversion.
+Section ImpVars.
+  Import Imp.
+  Context {p:ImpParameters}.
+  Let Imp : Imp.ImpType p := Imp.Imp p.
+  (* RecordImport p (* COQBUG(https://github.com/coq/coq/issues/7808) *) *)
+  Local Notation mword := p.(mword).
+  Local Notation mword_nonzero := p.(mword_nonzero).
+  Local Notation varname := p.(varname).
+  Local Notation funname := p.(funname).
+  Local Notation actname := p.(actname).
+  Local Notation bopname := p.(bopname).
+  Local Notation varmap := p.(varmap).
+  Local Notation mem := p.(mem).
+  Local Notation interp_binop := p.(interp_binop).
+  Local Notation load := p.(load).
+  Local Notation store := p.(store).
+  (* RecordImport Imp (* COQBUG(https://github.com/coq/coq/issues/7808) *) *)
+  Local Notation expr := Imp.(_expr).
+  Local Notation stmt := Imp.(_stmt).
+  Local Notation cont := Imp.(_cont).
+  Local Notation interp_expr := Imp.(_interp_expr).
+  Local Notation interp_stmt := Imp.(_interp_stmt).
+  Local Notation interp_cont := Imp.(_interp_cont).
+
+  (* TODO: record ImpParametersOK *)
+  Context {mword_eq_dec : DecidableRel (@eq (Imp.varname p))}.
+
   (* Returns a list to make it obvious that it's a finite set. *)
   Fixpoint allVars_expr(e: expr): list varname :=
     match e with
@@ -425,7 +477,6 @@ Section ImpProperties.
     end.
 
   Ltac set_solver := set_solver_generic constr:(varname).
-  Ltac state_calc := state_calc_generic constr:(varname) (word wXLEN).
   
   Lemma modVars_subset_allVars: forall x s,
     x \in modVars s ->
@@ -450,75 +501,29 @@ Section ImpProperties.
         [ left; apply singleton_set_spec in H; auto
         | right; auto ] ].
   Qed.
-End ImpProperties.
 
-Ltac invert_interp_stmt :=
-  lazymatch goal with
-  | E: Imp.interp_stmt _ (S ?fuel) _ _ ?s = Some _ |- _ =>
-    destruct s;
-    [ apply invert_interp_SLoad in E
-    | apply invert_interp_SStore in E
-    | apply invert_interp_SSet in E
-    | apply invert_interp_SIf in E
-    | apply invert_interp_SWhile in E
-    | apply invert_interp_SSeq in E
-    | apply invert_interp_SSkip in E
-    | apply invert_interp_SCall in E
-    ];
-    deep_destruct E;
-    [ let x := fresh "Case_SLoad" in pose proof tt as x; move x at top
-    | let x := fresh "Case_SStore" in pose proof tt as x; move x at top
-    | let x := fresh "Case_SSet" in pose proof tt as x; move x at top
-    | let x := fresh "Case_SIf_Then" in pose proof tt as x; move x at top
-    | let x := fresh "Case_SIf_Else" in pose proof tt as x; move x at top
-    | let x := fresh "Case_SWhile_Done" in pose proof tt as x; move x at top
-    | let x := fresh "Case_SWhile_NotDone" in pose proof tt as x; move x at top
-    | let x := fresh "Case_SSeq" in pose proof tt as x; move x at top
-    | let x := fresh "Case_SSkip" in pose proof tt as x; move x at top 
-    | let x := fresh "Case_SCall" in pose proof tt as x; move x at top
-    ]
-  end.
-
-End ImpProperties. (* TODO: file *)
-
-
-
-Section ExprImp2.
-
-  Context {Bw: BitWidths}. (* bit width *)
-
-  Context {Name: NameWithEq}.
-  Notation var := (@name Name).
-  Existing Instance eq_name_dec.
-  Context {FName: NameWithEq}.
-  Notation func := (@name FName).
-
-  Context {state: Type}.
-  Context {stateMap: Map state var (word wXLEN)}.
-  Context {vars: Type}.
-  Context {varset: set vars var}.
-
-  Ltac state_calc := state_calc_generic (@name Name) (word wXLEN).
-
-  Lemma modVarsSound: forall env fuel s initialS initialM finalS finalM,
-    interp_stmt env fuel initialS initialM s = Some (finalS, finalM) ->
+  Ltac state_calc := state_calc_generic constr:(varname) constr:(mword).
+
+  Lemma modVarsSound: forall env fuel s initialS initialM finalS finalM oc,
+    interp_stmt env fuel initialS initialM s = Some (finalS, finalM, oc) ->
     only_differ initialS (modVars s) finalS.
   Proof.
     induction fuel; introv Ev.
     - discriminate.
-    - invert_interp_stmt; simpl in *; inversionss;
+    - invert_interp_stmt; cbn [modVars] in *; inversionss;
       repeat match goal with
       | IH: _, H: _ |- _ =>
           let IH' := fresh IH in pose proof IH as IH';
           specialize IH' with (1 := H);
-          simpl in IH';
+          cbn [modVars] in IH';
           ensure_new IH'
-      end;
-      state_calc.
+      end; state_calc.
+      (* SCall *)
       refine (only_differ_putmany _ _ _ _ _ _); eassumption.
   Qed.
 
-End ExprImp2.
+End ImpVars.
+End ImpVars. (* TODO: file *)
 
 
 Require riscv.util.BitWidth32.
@@ -574,4 +579,4 @@ Goal run_isRight $5 $3 $5 = Some $0. reflexivity. Qed.
 Goal run_isRight $5 $3 $4 = Some $1. reflexivity. Qed.
 Goal run_isRight $12 $13 $5 = Some $1. reflexivity. Qed.
 
-End TestExprImp.
+End TestExprImp.
\ No newline at end of file