diff --git a/bedrock2/src/bedrock2/LeakageSemantics.v b/bedrock2/src/bedrock2/LeakageSemantics.v
new file mode 100644
index 000000000..47591bcae
--- /dev/null
+++ b/bedrock2/src/bedrock2/LeakageSemantics.v
@@ -0,0 +1,372 @@
+Require Import coqutil.sanity coqutil.Byte.
+Require Import coqutil.Tactics.fwd.
+Require Import coqutil.Map.Properties.
+Require coqutil.Map.SortedListString.
+Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
+Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
+Require Export bedrock2.Memory.
+Require Import bedrock2.Semantics.
+Require Import Coq.Lists.List.
+
+Inductive leakage_event {width: Z}{BW: Bitwidth width}{word: word.word width} : Type :=
+| leak_unit
+| leak_bool (b : bool)
+| leak_word (w : word)
+| leak_list (l : list word).
+(* ^sometimes it's convenient that one io call leaks only one event
+   See Interact case of spilling transform_trace function for an example. *)
+Definition leakage {width: Z}{BW: Bitwidth width}{word: word.word width} : Type :=
+  list leakage_event.
+
+Definition ExtSpec{width: Z}{BW: Bitwidth width}{word: word.word width}{mem: map.map word byte} :=
+  (* Given a trace of what happened so far,
+     the given-away memory, an action label and a list of function call arguments, *)
+  trace -> mem -> String.string -> list word ->
+  (* and a postcondition on the received memory, function call results, and leakage trace, *)
+  (mem -> list word -> list word -> Prop) ->
+  (* tells if this postcondition will hold *)
+  Prop.
+
+Existing Class ExtSpec.
+
+Module ext_spec.
+  Class ok{width: Z}{BW: Bitwidth width}{word: word.word width}{mem: map.map word byte}
+          {ext_spec: ExtSpec}: Prop :=
+  {
+    (* Given a trace of previous interactions, the action name and arguments
+       uniquely determine what chunk of memory the ext_spec will chop off from
+       the whole memory m *)
+    mGive_unique: forall t m mGive1 mKeep1 mGive2 mKeep2 a args post1 post2,
+      map.split m mKeep1 mGive1 ->
+      map.split m mKeep2 mGive2 ->
+      ext_spec t mGive1 a args post1 ->
+      ext_spec t mGive2 a args post2 ->
+      mGive1 = mGive2;
+
+    #[global] weaken :: forall t mGive act args,
+        Morphisms.Proper
+          (Morphisms.respectful
+             (Morphisms.pointwise_relation Interface.map.rep
+                (Morphisms.pointwise_relation (list word)
+                   (Morphisms.pointwise_relation (list word) Basics.impl))) Basics.impl)
+             (ext_spec t mGive act args);
+
+    intersect: forall t mGive a args
+                      (post1 post2: mem -> list word -> list word -> Prop),
+        ext_spec t mGive a args post1 ->
+        ext_spec t mGive a args post2 ->
+        ext_spec t mGive a args (fun mReceive resvals klist =>
+                                   post1 mReceive resvals klist /\ post2 mReceive resvals klist);
+  }.
+End ext_spec.
+Arguments ext_spec.ok {_ _ _ _} _.
+
+Definition PickSp {width: Z}{BW: Bitwidth width}{word: word.word width} : Type :=
+  leakage -> word.
+Existing Class PickSp.
+
+Section binops.
+  Context {width : Z} {BW : Bitwidth width} {word : Word.Interface.word width}.
+  Definition leak_binop (bop : bopname) (x1 : word) (x2 : word) (k : leakage) : leakage :=
+    match bop with
+    | bopname.divu | bopname.remu => cons (leak_word x2) (cons (leak_word x1) nil)
+    | bopname.sru | bopname.slu | bopname.srs => cons (leak_word x2) nil
+    | _ => nil
+    end.
+End binops.
+
+Section semantics.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
+  Context {locals: map.map String.string word}.
+  Context {ext_spec: ExtSpec}.
+
+  Section WithMemAndLocals.
+    Context (m : mem) (l : locals).
+
+    Local Notation "' x <- a ; f" := (match a with Some x => f | None => None end)
+      (right associativity, at level 70, x pattern).
+
+    Fixpoint eval_expr (e : expr) (k : leakage) : option (word * leakage) :=
+      match e with
+      | expr.literal v => Some (word.of_Z v, k)
+      | expr.var x => 'v <- map.get l x; Some (v, k)
+      | expr.inlinetable aSize t index =>
+          '(index', k') <- eval_expr index k;
+          'v <- load aSize (map.of_list_word t) index';
+          Some (v, leak_word index' :: k')
+      | expr.load aSize a =>
+          '(a', k') <- eval_expr a k;
+          'v <- load aSize m a';
+          Some (v, leak_word a' :: k')
+      | expr.op op e1 e2 =>
+          '(v1, k') <- eval_expr e1 k;
+          '(v2, k'') <- eval_expr e2 k';
+          Some (interp_binop op v1 v2, leak_binop op v1 v2 k'')
+      | expr.ite c e1 e2 =>
+          '(vc, k') <- eval_expr c k;
+          let b := word.eqb vc (word.of_Z 0) in
+          eval_expr (if b then e2 else e1) (leak_bool b :: k')
+      end.
+
+    Fixpoint eval_call_args (arges : list expr) (k : leakage) :=
+      match arges with
+      | e :: tl =>
+        '(v, k') <- eval_expr e k;
+        '(args, k'') <- eval_call_args tl k';
+        Some (v :: args, k'')
+      | _ => Some (nil, k)
+      end.
+
+  End WithMemAndLocals.
+End semantics.
+
+Module exec. Section WithParams.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
+  Context {locals: map.map String.string word}.
+  Context {ext_spec: ExtSpec} {pick_sp: PickSp}.
+  Section WithEnv.
+  Context (e: env).
+
+  Implicit Types post : leakage -> trace -> mem -> locals -> Prop. (* COQBUG: unification finds Type instead of Prop and fails to downgrade *)
+  Inductive exec: cmd -> leakage -> trace -> mem -> locals ->
+                  (leakage -> trace -> mem -> locals -> Prop) -> Prop :=
+  | skip: forall k t m l post,
+      post k t m l ->
+      exec cmd.skip k t m l post
+  | set: forall x e k t m l post v k',
+      eval_expr m l e k = Some (v, k') ->
+      post k' t m (map.put l x v) ->
+      exec (cmd.set x e) k t m l post
+  | unset: forall x k t m l post,
+      post k t m (map.remove l x) ->
+      exec (cmd.unset x) k t m l post
+  | store: forall sz ea ev k t m l post a k' v k'' m',
+      eval_expr m l ea k = Some (a, k') ->
+      eval_expr m l ev k' = Some (v, k'') ->
+      store sz m a v = Some m' ->
+      post (leak_word a :: k'') t m' l ->
+      exec (cmd.store sz ea ev) k t m l post
+  | stackalloc: forall x n body k t mSmall l post,
+      Z.modulo n (bytes_per_word width) = 0 ->
+      (forall mStack mCombined,
+        let a := pick_sp k in
+        anybytes a n mStack ->
+        map.split mCombined mSmall mStack ->
+        exec body (leak_unit :: k) t mCombined (map.put l x a)
+          (fun k' t' mCombined' l' =>
+            exists mSmall' mStack',
+              anybytes a n mStack' /\
+              map.split mCombined' mSmall' mStack' /\
+              post k' t' mSmall' l')) ->
+      exec (cmd.stackalloc x n body) k t mSmall l post
+  | if_true: forall k t m l e c1 c2 post v k',
+      eval_expr m l e k = Some (v, k') ->
+      word.unsigned v <> 0 ->
+      exec c1 (leak_bool true :: k') t m l post ->
+      exec (cmd.cond e c1 c2) k t m l post
+  | if_false: forall e c1 c2 k t m l post v k',
+      eval_expr m l e k = Some (v, k') ->
+      word.unsigned v = 0 ->
+      exec c2 (leak_bool false :: k') t m l post ->
+      exec (cmd.cond e c1 c2) k t m l post
+  | seq: forall c1 c2 k t m l post mid,
+      exec c1 k t m l mid ->
+      (forall k' t' m' l', mid k' t' m' l' -> exec c2 k' t' m' l' post) ->
+      exec (cmd.seq c1 c2) k t m l post
+  | while_false: forall e c k t m l post v k',
+      eval_expr m l e k = Some (v, k') ->
+      word.unsigned v = 0 ->
+      post (leak_bool false :: k') t m l ->
+      exec (cmd.while e c) k t m l post
+  | while_true: forall e c k t m l post v k' mid,
+      eval_expr m l e k = Some (v, k') ->
+      word.unsigned v <> 0 ->
+      exec c (leak_bool true :: k') t m l mid ->
+      (forall k'' t' m' l', mid k'' t' m' l' -> exec (cmd.while e c) k'' t' m' l' post) ->
+      exec (cmd.while e c) k t m l post
+  | call: forall binds fname arges k t m l post params rets fbody args k' lf mid,
+      map.get e fname = Some (params, rets, fbody) ->
+      eval_call_args m l arges k = Some (args, k') ->
+      map.of_list_zip params args = Some lf ->
+      exec fbody (leak_unit :: k') t m lf mid ->
+      (forall k'' t' m' st1, mid k'' t' m' st1 ->
+          exists retvs, map.getmany_of_list st1 rets = Some retvs /\
+          exists l', map.putmany_of_list_zip binds retvs l = Some l' /\
+          post k'' t' m' l') ->
+      exec (cmd.call binds fname arges) k t m l post
+  | interact: forall binds action arges args k' k t m l post mKeep mGive mid,
+      map.split m mKeep mGive ->
+      eval_call_args m l arges k = Some (args, k') ->
+      ext_spec t mGive action args mid ->
+      (forall mReceive resvals klist, mid mReceive resvals klist ->
+          exists l', map.putmany_of_list_zip binds resvals l = Some l' /\
+          forall m', map.split m' mKeep mReceive ->
+          post (leak_list klist :: k') (cons ((mGive, action, args), (mReceive, resvals)) t) m' l') ->
+      exec (cmd.interact binds action arges) k t m l post.
+
+  Context {word_ok: word.ok word} {mem_ok: map.ok mem} {ext_spec_ok: ext_spec.ok ext_spec}.
+
+  Lemma interact_cps: forall binds action arges args k' k t m l post mKeep mGive,
+      map.split m mKeep mGive ->
+      eval_call_args m l arges k = Some (args, k') ->
+      ext_spec t mGive action args (fun mReceive resvals klist =>
+          exists l', map.putmany_of_list_zip binds resvals l = Some l' /\
+          forall m', map.split m' mKeep mReceive ->
+          post (leak_list klist :: k') (cons ((mGive, action, args), (mReceive, resvals)) t) m' l') ->
+      exec (cmd.interact binds action arges) k t m l post.
+  Proof. intros. eauto using interact. Qed.
+
+  Lemma seq_cps: forall c1 c2 k t m l post,
+      exec c1 k t m l (fun k' t' m' l' => exec c2 k' t' m' l' post) ->
+      exec (cmd.seq c1 c2) k t m l post.
+  Proof. intros. eauto using seq. Qed.
+
+  Lemma weaken: forall k t l m s post1,
+      exec s k t m l post1 ->
+      forall post2,
+        (forall k' t' m' l', post1 k' t' m' l' -> post2 k' t' m' l') ->
+        exec s k t m l post2.
+  Proof.
+    induction 1; intros; try solve [econstructor; eauto].
+    - eapply stackalloc. 1: assumption.
+      intros.
+      eapply H1; eauto.
+      intros. fwd. eauto 10.
+    - eapply call.
+      4: eapply IHexec.
+      all: eauto.
+      intros.
+      edestruct H3 as (? & ? & ? & ? & ?); [eassumption|].
+      eauto 10.
+    - eapply interact; try eassumption.
+      intros.
+      edestruct H2 as (? & ? & ?); [eassumption|].
+      eauto 10.
+  Qed.
+
+  Lemma intersect: forall k t l m s post1,
+      exec s k t m l post1 ->
+      forall post2,
+        exec s k t m l post2 ->
+        exec s k t m l (fun k' t' m' l' => post1 k' t' m' l' /\ post2 k' t' m' l').
+  Proof.
+    induction 1;
+      intros;
+      match goal with
+      | H: exec _ _ _ _ _ _ |- _ => inversion H; subst; clear H
+      end;
+      try match goal with
+      | H1: ?e = Some (?x1, ?y1, ?z1), H2: ?e = Some (?x2, ?y2, ?z2) |- _ =>
+        replace x2 with x1 in * by congruence;
+          replace y2 with y1 in * by congruence;
+          replace z2 with z1 in * by congruence;
+          clear x2 y2 z2 H2
+      end;
+      repeat match goal with
+             | H1: ?e = Some (?v1, ?k1), H2: ?e = Some (?v2, ?k2) |- _ =>
+                 replace v2 with v1 in * by congruence;
+                 replace k2 with k1 in * by congruence;
+                 clear H2
+             end;
+      repeat match goal with
+             | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
+               replace v2 with v1 in * by congruence; clear H2
+             end;
+      try solve [econstructor; eauto | exfalso; congruence].
+
+    - econstructor. 1: eassumption.
+      intros.
+      rename H0 into Ex1, H12 into Ex2.
+      eapply weaken. 1: eapply H1. 1,2: eassumption.
+      1: eapply Ex2. 1,2: eassumption.
+      cbv beta.
+      intros. fwd.
+      lazymatch goal with
+      | A: map.split _ _ _, B: map.split _ _ _ |- _ =>
+        specialize @map.split_diff with (4 := A) (5 := B) as P
+      end.
+      edestruct P; try typeclasses eauto. 2: subst; eauto 10.
+      eapply anybytes_unique_domain; eassumption.
+    - econstructor.
+      + eapply IHexec. exact H5. (* not H *)
+      + simpl. intros *. intros [? ?]. eauto.
+    - eapply while_true. 1, 2: eassumption.
+      + eapply IHexec. exact H9. (* not H1 *)
+      + simpl. intros *. intros [? ?]. eauto.
+    - eapply call. 1, 2, 3: eassumption.
+      + eapply IHexec. exact H16. (* not H2 *)
+      + simpl. intros *. intros [? ?].
+        edestruct H3 as (? & ? & ? & ? & ?); [eassumption|].
+        edestruct H17 as (? & ? & ? & ? & ?); [eassumption|].
+        repeat match goal with
+               | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
+                 replace v2 with v1 in * by congruence; clear H2
+               end.
+        eauto 10.
+    - pose proof ext_spec.mGive_unique as P.
+      specialize P with (1 := H) (2 := H7) (3 := H1) (4 := H14).
+      subst mGive0.
+      destruct (map.split_diff (map.same_domain_refl mGive) H H7) as (? & _).
+      subst mKeep0.
+      eapply interact. 1,2: eassumption.
+      + eapply ext_spec.intersect; [ exact H1 | exact H14 ].
+      + simpl. intros *. intros [? ?].
+        edestruct H2 as (? & ? & ?); [eassumption|].
+        edestruct H15 as (? & ? & ?); [eassumption|].
+        repeat match goal with
+               | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
+                 replace v2 with v1 in * by congruence; clear H2
+               end.
+        eauto 10.
+  Qed.
+
+  End WithEnv.
+
+  Lemma extend_env: forall e1 e2,
+      map.extends e2 e1 ->
+      forall c k t m l post,
+      exec e1 c k t m l post ->
+      exec e2 c k t m l post.
+  Proof. induction 2; try solve [econstructor; eauto]. Qed.
+
+  End WithParams.
+End exec. Notation exec := exec.exec.
+
+Section WithParams.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
+  Context {locals: map.map String.string word}.
+  Context {ext_spec: ExtSpec} {pick_sp : PickSp}.
+
+  Implicit Types (l: locals) (m: mem) (post: leakage -> trace -> mem -> list word -> Prop).
+
+  Definition call e fname k t m args post :=
+    exists argnames retnames body,
+      map.get e fname = Some (argnames, retnames, body) /\
+      exists l, map.of_list_zip argnames args = Some l /\
+        exec e body k t m l (fun k' t' m' l' => exists rets,
+          map.getmany_of_list l' retnames = Some rets /\ post k' t' m' rets).
+
+  Lemma weaken_call: forall e fname k t m args post1,
+      call e fname k t m args post1 ->
+      forall post2, (forall k' t' m' rets, post1 k' t' m' rets -> post2 k' t' m' rets) ->
+      call e fname k t m args post2.
+  Proof.
+    unfold call. intros. fwd.
+    do 4 eexists. 1: eassumption.
+    do 2 eexists. 1: eassumption.
+    eapply exec.weaken. 1: eassumption.
+    cbv beta. clear -H0. intros. fwd. eauto.
+  Qed.
+
+  Lemma extend_env_call: forall e1 e2,
+      map.extends e2 e1 ->
+      forall f k t m rets post,
+      call e1 f k t m rets post ->
+      call e2 f k t m rets post.
+  Proof.
+    unfold call. intros. fwd. repeat eexists.
+    - eapply H. eassumption.
+    - eassumption.
+    - eapply exec.extend_env; eassumption.
+  Qed.
+End WithParams.
diff --git a/bedrock2/src/bedrock2/Semantics.v b/bedrock2/src/bedrock2/Semantics.v
index c5e878df5..0fe39044e 100644
--- a/bedrock2/src/bedrock2/Semantics.v
+++ b/bedrock2/src/bedrock2/Semantics.v
@@ -14,22 +14,12 @@ Definition LogItem{width: Z}{BW: Bitwidth width}{word: word.word width}{mem: map
 Definition trace{width: Z}{BW: Bitwidth width}{word: word.word width}{mem: map.map word byte} :=
   list LogItem.
 
-Inductive event {width: Z}{BW: Bitwidth width}{word: word.word width} : Type :=
-| leak_unit
-| leak_bool (b : bool)
-| leak_word (w : word)
-| leak_list (l : list word).
-(* sometimes it's convenient that one io call leaks only one event
-   See Interact case of spilling transform_trace function for an example. *)
-Definition ltrace {width: Z}{BW: Bitwidth width}{word: word.word width} : Type :=
-  list event.
-
 Definition ExtSpec{width: Z}{BW: Bitwidth width}{word: word.word width}{mem: map.map word byte} :=
   (* Given a trace of what happened so far,
      the given-away memory, an action label and a list of function call arguments, *)
   trace -> mem -> String.string -> list word ->
-  (* and a postcondition on the received memory, function call results, and leakage trace, *)
-  (mem -> list word -> list word -> Prop) ->
+  (* and a postcondition on the received memory and function call results, *)
+  (mem -> list word -> Prop) ->
   (* tells if this postcondition will hold *)
   Prop.
 
@@ -53,26 +43,21 @@ Module ext_spec.
         Morphisms.Proper
           (Morphisms.respectful
              (Morphisms.pointwise_relation Interface.map.rep
-                (Morphisms.pointwise_relation (list word)
-                   (Morphisms.pointwise_relation (list word) Basics.impl))) Basics.impl)
-             (ext_spec t mGive act args);
+               (Morphisms.pointwise_relation (list word) Basics.impl)) Basics.impl)
+          (ext_spec t mGive act args);
 
     intersect: forall t mGive a args
-                      (post1 post2: mem -> list word -> list word -> Prop),
+                      (post1 post2: mem -> list word -> Prop),
         ext_spec t mGive a args post1 ->
         ext_spec t mGive a args post2 ->
-        ext_spec t mGive a args (fun mReceive resvals klist =>
-                                   post1 mReceive resvals klist /\ post2 mReceive resvals klist);
+        ext_spec t mGive a args (fun mReceive resvals =>
+                                   post1 mReceive resvals /\ post2 mReceive resvals);
   }.
 End ext_spec.
 Arguments ext_spec.ok {_ _ _ _} _.
 
-Definition PickSp {width: Z}{BW: Bitwidth width}{word: word.word width} : Type :=
-  ltrace -> word.
-Existing Class PickSp.
-
 Section binops.
-  Context {width : Z} {BW : Bitwidth width} {word : Word.Interface.word width}.
+  Context {width : Z} {word : Word.Interface.word width}.
   Definition interp_binop (bop : bopname) : word -> word -> word :=
     match bop with
     | bopname.add => word.add
@@ -94,12 +79,6 @@ Section binops.
     | bopname.eq => fun a b =>
       if word.eqb a b then word.of_Z 1 else word.of_Z 0
     end.
-  Definition leak_binop (bop : bopname) (x1 : word) (x2 : word) (k : ltrace) : ltrace :=
-    match bop with
-    | bopname.divu | bopname.remu => cons (leak_word x2) (cons (leak_word x1) nil)
-    | bopname.sru | bopname.slu | bopname.srs => cons (leak_word x2) nil
-    | _ => nil
-    end.
 End binops.
 
 Definition env: map.map String.string Syntax.func := SortedListString.map _.
@@ -114,38 +93,35 @@ Section semantics.
   Section WithMemAndLocals.
     Context (m : mem) (l : locals).
 
-    Local Notation "' x <- a ; f" := (match a with Some x => f | None => None end)
-      (right associativity, at level 70, x pattern).
+    Local Notation "x <- a ; f" := (match a with Some x => f | None => None end)
+      (right associativity, at level 70).
 
-    Fixpoint eval_expr (e : expr) (k : ltrace) : option (word * ltrace) :=
+    Fixpoint eval_expr (e : expr) : option word :=
       match e with
-      | expr.literal v => Some (word.of_Z v, k)
-      | expr.var x => 'v <- map.get l x; Some (v, k)
+      | expr.literal v => Some (word.of_Z v)
+      | expr.var x => map.get l x
       | expr.inlinetable aSize t index =>
-          '(index', k') <- eval_expr index k;
-          'v <- load aSize (map.of_list_word t) index';
-          Some (v, leak_word index' :: k')
+          index' <- eval_expr index;
+          load aSize (map.of_list_word t) index'
       | expr.load aSize a =>
-          '(a', k') <- eval_expr a k;
-          'v <- load aSize m a';
-          Some (v, leak_word a' :: k')
+          a' <- eval_expr a;
+          load aSize m a'
       | expr.op op e1 e2 =>
-          '(v1, k') <- eval_expr e1 k;
-          '(v2, k'') <- eval_expr e2 k';
-          Some (interp_binop op v1 v2, leak_binop op v1 v2 k'')
+          v1 <- eval_expr e1;
+          v2 <- eval_expr e2;
+          Some (interp_binop op v1 v2)
       | expr.ite c e1 e2 =>
-          '(vc, k') <- eval_expr c k;
-          let b := word.eqb vc (word.of_Z 0) in
-          eval_expr (if b then e2 else e1) (leak_bool b :: k')
+          vc <- eval_expr c;
+          eval_expr (if word.eqb vc (word.of_Z 0) then e2 else e1)
       end.
 
-    Fixpoint eval_call_args (arges : list expr) (k : ltrace) :=
+    Fixpoint eval_call_args (arges : list expr) :=
       match arges with
       | e :: tl =>
-        '(v, k') <- eval_expr e k;
-        '(args, k'') <- eval_call_args tl k';
-        Some (v :: args, k'')
-      | _ => Some (nil, k)
+        v <- eval_expr e;
+        args <- eval_call_args tl;
+        Some (v :: args)
+      | _ => Some nil
       end.
 
   End WithMemAndLocals.
@@ -154,109 +130,108 @@ End semantics.
 Module exec. Section WithParams.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {ext_spec: ExtSpec} {pick_sp: PickSp}.
+  Context {ext_spec: ExtSpec}.
   Section WithEnv.
   Context (e: env).
 
-  Implicit Types post : ltrace -> trace -> mem -> locals -> Prop. (* COQBUG: unification finds Type instead of Prop and fails to downgrade *)
-  Inductive exec: cmd -> ltrace -> trace -> mem -> locals ->
-                  (ltrace -> trace -> mem -> locals -> Prop) -> Prop :=
-  | skip: forall k t m l post,
-      post k t m l ->
-      exec cmd.skip k t m l post
-  | set: forall x e k t m l post v k',
-      eval_expr m l e k = Some (v, k') ->
-      post k' t m (map.put l x v) ->
-      exec (cmd.set x e) k t m l post
-  | unset: forall x k t m l post,
-      post k t m (map.remove l x) ->
-      exec (cmd.unset x) k t m l post
-  | store: forall sz ea ev k t m l post a k' v k'' m',
-      eval_expr m l ea k = Some (a, k') ->
-      eval_expr m l ev k' = Some (v, k'') ->
+  Implicit Types post : trace -> mem -> locals -> Prop. (* COQBUG: unification finds Type instead of Prop and fails to downgrade *)
+  Inductive exec: cmd -> trace -> mem -> locals ->
+                  (trace -> mem -> locals -> Prop) -> Prop :=
+  | skip: forall t m l post,
+      post t m l ->
+      exec cmd.skip t m l post
+  | set: forall x e t m l post v,
+      eval_expr m l e = Some v ->
+      post t m (map.put l x v) ->
+      exec (cmd.set x e) t m l post
+  | unset: forall x t m l post,
+      post t m (map.remove l x) ->
+      exec (cmd.unset x) t m l post
+  | store: forall sz ea ev t m l post a v m',
+      eval_expr m l ea = Some a ->
+      eval_expr m l ev = Some v ->
       store sz m a v = Some m' ->
-      post (leak_word a :: k'') t m' l ->
-      exec (cmd.store sz ea ev) k t m l post
-  | stackalloc: forall x n body k t mSmall l post,
+      post t m' l ->
+      exec (cmd.store sz ea ev) t m l post
+  | stackalloc: forall x n body t mSmall l post,
       Z.modulo n (bytes_per_word width) = 0 ->
-      (forall mStack mCombined,
-        let a := pick_sp k in
+      (forall a mStack mCombined,
         anybytes a n mStack ->
         map.split mCombined mSmall mStack ->
-        exec body (leak_unit :: k) t mCombined (map.put l x a)
-          (fun k' t' mCombined' l' =>
+        exec body t mCombined (map.put l x a)
+          (fun t' mCombined' l' =>
             exists mSmall' mStack',
               anybytes a n mStack' /\
               map.split mCombined' mSmall' mStack' /\
-              post k' t' mSmall' l')) ->
-      exec (cmd.stackalloc x n body) k t mSmall l post
-  | if_true: forall k t m l e c1 c2 post v k',
-      eval_expr m l e k = Some (v, k') ->
+              post t' mSmall' l')) ->
+      exec (cmd.stackalloc x n body) t mSmall l post
+  | if_true: forall t m l e c1 c2 post v,
+      eval_expr m l e = Some v ->
       word.unsigned v <> 0 ->
-      exec c1 (leak_bool true :: k') t m l post ->
-      exec (cmd.cond e c1 c2) k t m l post
-  | if_false: forall e c1 c2 k t m l post v k',
-      eval_expr m l e k = Some (v, k') ->
+      exec c1 t m l post ->
+      exec (cmd.cond e c1 c2) t m l post
+  | if_false: forall e c1 c2 t m l post v,
+      eval_expr m l e = Some v ->
       word.unsigned v = 0 ->
-      exec c2 (leak_bool false :: k') t m l post ->
-      exec (cmd.cond e c1 c2) k t m l post
-  | seq: forall c1 c2 k t m l post mid,
-      exec c1 k t m l mid ->
-      (forall k' t' m' l', mid k' t' m' l' -> exec c2 k' t' m' l' post) ->
-      exec (cmd.seq c1 c2) k t m l post
-  | while_false: forall e c k t m l post v k',
-      eval_expr m l e k = Some (v, k') ->
+      exec c2 t m l post ->
+      exec (cmd.cond e c1 c2) t m l post
+  | seq: forall c1 c2 t m l post mid,
+      exec c1 t m l mid ->
+      (forall t' m' l', mid t' m' l' -> exec c2 t' m' l' post) ->
+      exec (cmd.seq c1 c2) t m l post
+  | while_false: forall e c t m l post v,
+      eval_expr m l e = Some v ->
       word.unsigned v = 0 ->
-      post (leak_bool false :: k') t m l ->
-      exec (cmd.while e c) k t m l post
-  | while_true: forall e c k t m l post v k' mid,
-      eval_expr m l e k = Some (v, k') ->
+      post t m l ->
+      exec (cmd.while e c) t m l post
+  | while_true: forall e c t m l post v mid,
+      eval_expr m l e = Some v ->
       word.unsigned v <> 0 ->
-      exec c (leak_bool true :: k') t m l mid ->
-      (forall k'' t' m' l', mid k'' t' m' l' -> exec (cmd.while e c) k'' t' m' l' post) ->
-      exec (cmd.while e c) k t m l post
-  | call: forall binds fname arges k t m l post params rets fbody args k' lf mid,
+      exec c t m l mid ->
+      (forall t' m' l', mid t' m' l' -> exec (cmd.while e c) t' m' l' post) ->
+      exec (cmd.while e c) t m l post
+  | call: forall binds fname arges t m l post params rets fbody args lf mid,
       map.get e fname = Some (params, rets, fbody) ->
-      eval_call_args m l arges k = Some (args, k') ->
+      eval_call_args m l arges = Some args ->
       map.of_list_zip params args = Some lf ->
-      exec fbody (leak_unit :: k') t m lf mid ->
-      (forall k'' t' m' st1, mid k'' t' m' st1 ->
+      exec fbody t m lf mid ->
+      (forall t' m' st1, mid t' m' st1 ->
           exists retvs, map.getmany_of_list st1 rets = Some retvs /\
           exists l', map.putmany_of_list_zip binds retvs l = Some l' /\
-          post k'' t' m' l') ->
-      exec (cmd.call binds fname arges) k t m l post
-  | interact: forall binds action arges args k' k t m l post mKeep mGive mid,
+          post t' m' l') ->
+      exec (cmd.call binds fname arges) t m l post
+  | interact: forall binds action arges args t m l post mKeep mGive mid,
       map.split m mKeep mGive ->
-      eval_call_args m l arges k = Some (args, k') ->
+      eval_call_args m l arges = Some args ->
       ext_spec t mGive action args mid ->
-      (forall mReceive resvals klist, mid mReceive resvals klist ->
+      (forall mReceive resvals, mid mReceive resvals ->
           exists l', map.putmany_of_list_zip binds resvals l = Some l' /\
           forall m', map.split m' mKeep mReceive ->
-          post (leak_list klist :: k') (cons ((mGive, action, args), (mReceive, resvals)) t) m' l') ->
-      exec (cmd.interact binds action arges) k t m l post.
+          post (cons ((mGive, action, args), (mReceive, resvals)) t) m' l') ->
+      exec (cmd.interact binds action arges) t m l post.
 
   Context {word_ok: word.ok word} {mem_ok: map.ok mem} {ext_spec_ok: ext_spec.ok ext_spec}.
 
-  Lemma interact_cps: forall binds action arges args k' k t m l post mKeep mGive,
+  Lemma interact_cps: forall binds action arges args t m l post mKeep mGive,
       map.split m mKeep mGive ->
-      eval_call_args m l arges k = Some (args, k') ->
-      ext_spec t mGive action args (fun mReceive resvals klist =>
+      eval_call_args m l arges = Some args ->
+      ext_spec t mGive action args (fun mReceive resvals =>
           exists l', map.putmany_of_list_zip binds resvals l = Some l' /\
           forall m', map.split m' mKeep mReceive ->
-          post (leak_list klist :: k') (cons ((mGive, action, args), (mReceive, resvals)) t) m' l') ->
-      exec (cmd.interact binds action arges) k t m l post.
+          post (cons ((mGive, action, args), (mReceive, resvals)) t) m' l') ->
+      exec (cmd.interact binds action arges) t m l post.
   Proof. intros. eauto using interact. Qed.
 
-  Lemma seq_cps: forall c1 c2 k t m l post,
-      exec c1 k t m l (fun k' t' m' l' => exec c2 k' t' m' l' post) ->
-      exec (cmd.seq c1 c2) k t m l post.
+  Lemma seq_cps: forall c1 c2 t m l post,
+      exec c1 t m l (fun t' m' l' => exec c2 t' m' l' post) ->
+      exec (cmd.seq c1 c2) t m l post.
   Proof. intros. eauto using seq. Qed.
 
-  Lemma weaken: forall k t l m s post1,
-      exec s k t m l post1 ->
+  Lemma weaken: forall t l m s post1,
+      exec s t m l post1 ->
       forall post2,
-        (forall k' t' m' l', post1 k' t' m' l' -> post2 k' t' m' l') ->
-        exec s k t m l post2.
+        (forall t' m' l', post1 t' m' l' -> post2 t' m' l') ->
+        exec s t m l post2.
   Proof.
     induction 1; intros; try solve [econstructor; eauto].
     - eapply stackalloc. 1: assumption.
@@ -275,16 +250,16 @@ Module exec. Section WithParams.
       eauto 10.
   Qed.
 
-  Lemma intersect: forall k t l m s post1,
-      exec s k t m l post1 ->
+  Lemma intersect: forall t l m s post1,
+      exec s t m l post1 ->
       forall post2,
-        exec s k t m l post2 ->
-        exec s k t m l (fun k' t' m' l' => post1 k' t' m' l' /\ post2 k' t' m' l').
+        exec s t m l post2 ->
+        exec s t m l (fun t' m' l' => post1 t' m' l' /\ post2 t' m' l').
   Proof.
     induction 1;
       intros;
       match goal with
-      | H: exec _ _ _ _ _ _ |- _ => inversion H; subst; clear H
+      | H: exec _ _ _ _ _ |- _ => inversion H; subst; clear H
       end;
       try match goal with
       | H1: ?e = Some (?x1, ?y1, ?z1), H2: ?e = Some (?x2, ?y2, ?z2) |- _ =>
@@ -294,10 +269,8 @@ Module exec. Section WithParams.
           clear x2 y2 z2 H2
       end;
       repeat match goal with
-             | H1: ?e = Some (?v1, ?k1), H2: ?e = Some (?v2, ?k2) |- _ =>
-                 replace v2 with v1 in * by congruence;
-                 replace k2 with k1 in * by congruence;
-                 clear H2
+             | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
+               replace v2 with v1 in * by congruence; clear H2
              end;
       repeat match goal with
              | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
@@ -307,7 +280,7 @@ Module exec. Section WithParams.
 
     - econstructor. 1: eassumption.
       intros.
-      rename H0 into Ex1, H12 into Ex2.
+      rename H0 into Ex1, H11 into Ex2.
       eapply weaken. 1: eapply H1. 1,2: eassumption.
       1: eapply Ex2. 1,2: eassumption.
       cbv beta.
@@ -325,25 +298,25 @@ Module exec. Section WithParams.
       + eapply IHexec. exact H9. (* not H1 *)
       + simpl. intros *. intros [? ?]. eauto.
     - eapply call. 1, 2, 3: eassumption.
-      + eapply IHexec. exact H16. (* not H2 *)
+      + eapply IHexec. exact H15. (* not H2 *)
       + simpl. intros *. intros [? ?].
         edestruct H3 as (? & ? & ? & ? & ?); [eassumption|].
-        edestruct H17 as (? & ? & ? & ? & ?); [eassumption|].
+        edestruct H16 as (? & ? & ? & ? & ?); [eassumption|].
         repeat match goal with
                | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
                  replace v2 with v1 in * by congruence; clear H2
                end.
         eauto 10.
     - pose proof ext_spec.mGive_unique as P.
-      specialize P with (1 := H) (2 := H7) (3 := H1) (4 := H14).
+      specialize P with (1 := H) (2 := H7) (3 := H1) (4 := H13).
       subst mGive0.
       destruct (map.split_diff (map.same_domain_refl mGive) H H7) as (? & _).
       subst mKeep0.
       eapply interact. 1,2: eassumption.
-      + eapply ext_spec.intersect; [ exact H1 | exact H14 ].
+      + eapply ext_spec.intersect; [ exact H1 | exact H13 ].
       + simpl. intros *. intros [? ?].
         edestruct H2 as (? & ? & ?); [eassumption|].
-        edestruct H15 as (? & ? & ?); [eassumption|].
+        edestruct H14 as (? & ? & ?); [eassumption|].
         repeat match goal with
                | H1: ?e = Some ?v1, H2: ?e = Some ?v2 |- _ =>
                  replace v2 with v1 in * by congruence; clear H2
@@ -355,9 +328,9 @@ Module exec. Section WithParams.
 
   Lemma extend_env: forall e1 e2,
       map.extends e2 e1 ->
-      forall c k t m l post,
-      exec e1 c k t m l post ->
-      exec e2 c k t m l post.
+      forall c t m l post,
+      exec e1 c t m l post ->
+      exec e2 c t m l post.
   Proof. induction 2; try solve [econstructor; eauto]. Qed.
 
   End WithParams.
@@ -366,21 +339,21 @@ End exec. Notation exec := exec.exec.
 Section WithParams.
   Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.
   Context {locals: map.map String.string word}.
-  Context {ext_spec: ExtSpec} {pick_sp : PickSp}.
+  Context {ext_spec: ExtSpec}.
 
-  Implicit Types (l: locals) (m: mem) (post: ltrace -> trace -> mem -> list word -> Prop).
+  Implicit Types (l: locals) (m: mem) (post: trace -> mem -> list word -> Prop).
 
-  Definition call e fname k t m args post :=
+  Definition call e fname t m args post :=
     exists argnames retnames body,
       map.get e fname = Some (argnames, retnames, body) /\
       exists l, map.of_list_zip argnames args = Some l /\
-        exec e body k t m l (fun k' t' m' l' => exists rets,
-          map.getmany_of_list l' retnames = Some rets /\ post k' t' m' rets).
+        exec e body t m l (fun t' m' l' => exists rets,
+          map.getmany_of_list l' retnames = Some rets /\ post t' m' rets).
 
-  Lemma weaken_call: forall e fname k t m args post1,
-      call e fname k t m args post1 ->
-      forall post2, (forall k' t' m' rets, post1 k' t' m' rets -> post2 k' t' m' rets) ->
-      call e fname k t m args post2.
+  Lemma weaken_call: forall e fname t m args post1,
+      call e fname t m args post1 ->
+      forall post2, (forall t' m' rets, post1 t' m' rets -> post2 t' m' rets) ->
+      call e fname t m args post2.
   Proof.
     unfold call. intros. fwd.
     do 4 eexists. 1: eassumption.
@@ -391,9 +364,9 @@ Section WithParams.
 
   Lemma extend_env_call: forall e1 e2,
       map.extends e2 e1 ->
-      forall f k t m rets post,
-      call e1 f k t m rets post ->
-      call e2 f k t m rets post.
+      forall f t m rets post,
+      call e1 f t m rets post ->
+      call e2 f t m rets post.
   Proof.
     unfold call. intros. fwd. repeat eexists.
     - eapply H. eassumption.