diff --git a/bedrock2/src/bedrock2/FE310CSemantics.v b/bedrock2/src/bedrock2/FE310CSemantics.v
index 37d965de5..57cbb6b49 100644
--- a/bedrock2/src/bedrock2/FE310CSemantics.v
+++ b/bedrock2/src/bedrock2/FE310CSemantics.v
@@ -1,5 +1,6 @@
 Require Import Coq.ZArith.ZArith.
-Require Import bedrock2.Syntax bedrock2.Semantics bedrock2.LeakageSemantics bedrock2.MetricLeakageSemantics.
+Require Import bedrock2.Syntax bedrock2.Semantics bedrock2.LeakageSemantics.
+Require Import bedrock2.SemanticsRelations.
 Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString.
 Require Import coqutil.Word.Interface.
 Require Export coqutil.Word.Bitwidth32.
diff --git a/bedrock2/src/bedrock2/LeakageProgramLogic.v b/bedrock2/src/bedrock2/LeakageProgramLogic.v
index cfe1c9c1f..e754cdcb0 100644
--- a/bedrock2/src/bedrock2/LeakageProgramLogic.v
+++ b/bedrock2/src/bedrock2/LeakageProgramLogic.v
@@ -6,9 +6,10 @@ Require Import bedrock2.LeakageWeakestPrecondition.
 Require Import bedrock2.LeakageWeakestPreconditionProperties.
 Require Import bedrock2.LeakageLoops.
 Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars.
+Require bedrock2.ProgramLogic.
+Require Import bedrock2.SemanticsRelations.
 
-Definition spec_of (procname:String.string) := Semantics.env -> Prop.
-Existing Class spec_of.
+Notation spec_of := bedrock2.ProgramLogic.spec_of.
 
 Module Import Coercions.
   Import Map.Interface Word.Interface BinInt.
@@ -388,7 +389,6 @@ Ltac straightline_call_noex :=
   | |- LeakageWeakestPrecondition.call ?functions ?callee _ _ _ _ _ =>
     let callee_spec := lazymatch constr:(_:spec_of callee) with ?s => s end in
     let Hcall := lazymatch goal with H: callee_spec functions |- _ => H end in
-    repeat destruct Hcall as [?f Hcall]; 
     eapply LeakageWeakestPreconditionProperties.Proper_call; cycle -1;
       [ eapply Hcall | try eabstract (solve [Morphisms.solve_proper]) .. ];
       [ .. | intros ? ? ? ?]
@@ -406,8 +406,19 @@ Ltac straightline_call_ex :=
         [ .. | intros ? ? ? ? ]
   end.
 
+(*for use when the spec of callee has been written using Semantics, not LeakageSemantics*)
+Ltac straightline_call_from_plain :=
+  lazymatch goal with
+  | |- LeakageWeakestPrecondition.call ?functions ?callee _ _ _ _ _ =>
+    let callee_spec := lazymatch constr:(_:spec_of callee) with ?s => s end in
+    let Hcall := lazymatch goal with H: callee_spec functions |- _ => H end in
+    eapply LeakageWeakestPreconditionProperties.Proper_call; cycle -1;
+      [ eapply leakage_to_plain_call; eapply Hcall | try eabstract (solve [Morphisms.solve_proper]) .. ];
+      [ .. | intros ? ? ? ?]
+  end.
+
 (* TODO: once we can automatically prove some calls, include the success-only version of this in [straightline] *)
-Ltac straightline_call := straightline_call_noex || straightline_call_ex.
+Ltac straightline_call := straightline_call_noex || straightline_call_ex || straightline_call_from_plain.
 
 Ltac current_trace_mem_locals :=
   lazymatch goal with
diff --git a/bedrock2/src/bedrock2/MetricLeakageSemantics.v b/bedrock2/src/bedrock2/MetricLeakageSemantics.v
index adfb2c376..420aa9848 100644
--- a/bedrock2/src/bedrock2/MetricLeakageSemantics.v
+++ b/bedrock2/src/bedrock2/MetricLeakageSemantics.v
@@ -6,10 +6,8 @@ Require Import coqutil.Z.Lia.
 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 Coq.Lists.List.
 Require Import bedrock2.MetricLogging.
 Require Import bedrock2.MetricCosts.
-Require Import bedrock2.MetricSemantics.
 Require Import bedrock2.Semantics.
 Require Import bedrock2.LeakageSemantics.
 Require Import Coq.Lists.List.
@@ -546,173 +544,4 @@ Section WithParams.
     - eassumption.
     - eapply exec.extend_env; eassumption.
   Qed.
-
-  Lemma to_plain_eval_expr: forall m l e v,
-      Semantics.eval_expr m l e = Some v ->
-      forall k mc, exists k' mc', eval_expr m l e k mc = Some (v, k', mc').
-  Proof.
-    induction e; cbn; intros;
-      repeat match goal with
-        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
-        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
-        | IH: forall _ _, Semantics.eval_expr _ _ _ = Some _ -> _ |- _ =>
-            specialize (IH _ _ ltac:(eassumption))
-        | IH: forall _: leakage, forall _: MetricLog, exists _: leakage, exists _: MetricLog,
-            eval_expr ?m ?l ?e _ _ = Some _
-          |- context[eval_expr ?m ?l ?e ?k ?mc] => specialize (IH k mc)
-        | |- _ => progress fwd
-        | |- _ => Tactics.destruct_one_match
-        end;
-      eauto.
-  Qed.
-
-  Lemma to_metric_eval_expr: forall m l e mc v mc',
-      MetricSemantics.eval_expr m l e mc = Some (v, mc') ->
-      forall k, exists k', eval_expr m l e k mc = Some (v, k', mc').
-  Proof.
-    induction e; cbn; intros;
-      repeat match goal with
-        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
-        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
-        | IH: forall _ _ _, MetricSemantics.eval_expr _ _ _ _ = Some _ -> _ |- _
-          => specialize (IH _ _ _ ltac:(eassumption))
-        | IH: forall _: leakage, exists _: leakage, eval_expr ?m ?l ?e _ _ = Some _
-          |- context[eval_expr ?m ?l ?e ?k ?mc] => specialize (IH k)
-        | |- _ => progress fwd
-        | |- _ => Tactics.destruct_one_match
-        end;
-      eauto.
-  Qed.
-
-  Lemma to_leakage_eval_expr: forall m l e k v k',
-      LeakageSemantics.eval_expr m l e k = Some (v, k') ->
-      forall mc, exists mc', eval_expr m l e k mc = Some (v, k', mc').
-  Proof.
-    induction e; cbn; intros;
-      repeat match goal with
-        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
-        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
-        | IH: forall _ _ _, LeakageSemantics.eval_expr _ _ _ _ = Some _ -> _ |- _
-          => specialize (IH _ _ _ ltac:(eassumption))
-        | IH: forall _: MetricLog, exists _: MetricLog, eval_expr ?m ?l ?e _ _ = Some _
-          |- context[eval_expr ?m ?l ?e ?k ?mc] => specialize (IH mc)
-        | |- _ => progress fwd
-        | |- _ => Tactics.destruct_one_match
-        end;
-      eauto.
-  Qed.
-
-  Lemma to_plain_eval_call_args: forall m l arges args,
-      Semantics.eval_call_args m l arges = Some args ->
-      forall k mc, exists k' mc', eval_call_args m l arges k mc = Some (args, k', mc').
-  Proof.
-    induction arges; cbn; intros.
-    - eapply Option.eq_of_eq_Some in H. subst. eauto.
-    - fwd.
-      eapply to_plain_eval_expr in E. destruct E as (k' & mc' & E). rewrite E.
-      specialize IHarges with (1 := eq_refl). specialize (IHarges k' mc').
-      destruct IHarges as (k'' & mc'' & IH). rewrite IH. eauto.
-  Qed.
-
-  Lemma to_metric_eval_call_args: forall m l arges mc args mc',
-      MetricSemantics.eval_call_args m l arges mc = Some (args, mc') ->
-      forall k, exists k', eval_call_args m l arges k mc = Some (args, k', mc').
-  Proof.
-    induction arges; cbn; intros.
-    - inversion H. subst. eauto.
-    - fwd.
-      eapply to_metric_eval_expr in E. destruct E as (k' & E). rewrite E.
-      specialize (IHarges _ _ _ ltac:(eassumption) k').
-      destruct IHarges as (k'' & IH). rewrite IH. eauto.
-  Qed.
-
-  Lemma to_leakage_eval_call_args: forall m l arges k args k',
-      LeakageSemantics.eval_call_args m l arges k = Some (args, k') ->
-      forall mc, exists mc', eval_call_args m l arges k mc = Some (args, k', mc').
-  Proof.
-    induction arges; cbn; intros.
-    - inversion H. subst. eauto.
-    - fwd.
-      eapply to_leakage_eval_expr in E. destruct E as (mc' & E). rewrite E.
-      specialize (IHarges _ _ _ ltac:(eassumption) mc').
-      destruct IHarges as (mc'' & IH). rewrite IH. eauto.
-  Qed.
-
-  Definition deleakaged_ext_spec : Semantics.ExtSpec :=
-    fun t mGive a args post => ext_spec t mGive a args (fun mReceive resvals klist => post mReceive resvals).
-  
-  Lemma deleakaged_ext_spec_ok {ext_spec_ok: ext_spec.ok ext_spec}:
-    Semantics.ext_spec.ok deleakaged_ext_spec.
-  Proof.
-    destruct ext_spec_ok. cbv [deleakaged_ext_spec]. constructor; eauto.
-    intros. cbv [Morphisms.Proper Morphisms.respectful Morphisms.pointwise_relation Basics.impl] in *.
-    intros. eapply weaken; eauto. intros. apply H. simpl in *. assumption.
-  Qed.    
-
-  Context (e: env).
-  Existing Instance deleakaged_ext_spec.
-  Existing Instance deleakaged_ext_spec_ok.
-
-  Lemma to_plain_exec: forall c t m l post,
-      Semantics.exec e c t m l post ->
-      forall k mc, exec e c k t m l mc (fun _ t' m' l' _ => post t' m' l').
-  Proof.
-    induction 1; intros;
-      repeat match reverse goal with
-        | H: Semantics.eval_expr _ _ _ = Some _ |- _ =>
-            eapply to_plain_eval_expr in H; destruct H as (? & ? & H)
-        | H: Semantics.eval_call_args _ _ _ = Some _ |- _ =>
-            eapply to_plain_eval_call_args in H; destruct H as (? & ? & H)
-        end;
-      try solve [econstructor; eauto].
-  Qed.
-
-  Lemma to_metric_exec: forall c t m l mc post,
-      MetricSemantics.exec e c t m l mc post ->
-      forall k, exec e c k t m l mc (fun _ t' m' l' mc' => post t' m' l' mc').
-  Proof.
-    induction 1; intros;
-      repeat match reverse goal with
-        | H: MetricSemantics.eval_expr _ _ _ _ = Some _ |- _ =>
-            eapply to_metric_eval_expr in H; destruct H as (? & H)
-        | H: MetricSemantics.eval_call_args _ _ _ _ = Some _ |- _ =>
-            eapply to_metric_eval_call_args in H; destruct H as (? & H)
-        end;
-      try solve [econstructor; eauto].
-  Qed.
-
-  Lemma to_leakage_exec: forall c t m l k post,
-      LeakageSemantics.exec e c k t m l post ->
-      forall mc, exec e c k t m l mc (fun k' t' m' l' _ => post k' t' m' l').
-  Proof.
-    induction 1; intros;
-      repeat match reverse goal with
-        | H: LeakageSemantics.eval_expr _ _ _ _ = Some _ |- _ =>
-            eapply to_leakage_eval_expr in H; destruct H as (? & H)
-        | H: LeakageSemantics.eval_call_args _ _ _ _ = Some _ |- _ =>
-            eapply to_leakage_eval_call_args in H; destruct H as (? & H)
-        end;
-      try solve [econstructor; eauto].
-  Qed.
-
-  Lemma to_plain_call: forall f t m args post,
-      Semantics.call e f t m args post ->
-      forall k mc, call e f k t m args mc (fun _ t' m' rets _ => post t' m' rets).
-  Proof.
-    unfold call, Semantics.call. intros. fwd. eauto 10 using to_plain_exec.
-  Qed.
-
-  Lemma to_metric_call: forall f t m args mc post,
-      MetricSemantics.call e f t m args mc post ->
-      forall k, call e f k t m args mc (fun _ t' m' rets mc' => post t' m' rets mc').
-  Proof.
-    unfold call, MetricSemantics.call. intros. fwd. eauto 10 using to_metric_exec.
-  Qed.
-
-  Lemma to_leakage_call: forall f k t m args post,
-      LeakageSemantics.call e f k t m args post ->
-      forall mc, call e f k t m args mc (fun k' t' m' rets _ => post k' t' m' rets).
-  Proof.
-    unfold call, LeakageSemantics.call. intros. fwd. eauto 10 using to_leakage_exec.
-  Qed.
 End WithParams.
diff --git a/bedrock2/src/bedrock2/SemanticsRelations.v b/bedrock2/src/bedrock2/SemanticsRelations.v
new file mode 100644
index 000000000..6f923beed
--- /dev/null
+++ b/bedrock2/src/bedrock2/SemanticsRelations.v
@@ -0,0 +1,490 @@
+Require Import coqutil.sanity coqutil.Byte.
+Require Import coqutil.Tactics.fwd.
+Require Import coqutil.Z.Lia.
+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.MetricLogging.
+Require Import bedrock2.Semantics.
+Require Import bedrock2.LeakageSemantics.
+Require Import bedrock2.MetricSemantics.
+Require Import bedrock2.MetricLeakageSemantics.
+
+Section MetricLeakageToSomething.
+  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}.
+
+  Lemma metricleakage_to_plain_eval_expr: forall m l e v,
+      Semantics.eval_expr m l e = Some v ->
+      forall k mc, exists k' mc', MetricLeakageSemantics.eval_expr m l e k mc = Some (v, k', mc').
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _ _, Semantics.eval_expr _ _ _ = Some _ -> _ |- _ =>
+            specialize (IH _ _ ltac:(eassumption))
+        | IH: forall _: leakage, forall _: MetricLog, exists _: leakage, exists _: MetricLog,
+            MetricLeakageSemantics.eval_expr ?m ?l ?e _ _ = Some _
+          |- context[MetricLeakageSemantics.eval_expr ?m ?l ?e ?k ?mc] => specialize (IH k mc)
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma metricleakage_to_metric_eval_expr: forall m l e mc v mc',
+      MetricSemantics.eval_expr m l e mc = Some (v, mc') ->
+      forall k, exists k', MetricLeakageSemantics.eval_expr m l e k mc = Some (v, k', mc').
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _ _ _, MetricSemantics.eval_expr _ _ _ _ = Some _ -> _ |- _
+          => specialize (IH _ _ _ ltac:(eassumption))
+        | IH: forall _: leakage, exists _: leakage, MetricLeakageSemantics.eval_expr ?m ?l ?e _ _ = Some _
+          |- context[MetricLeakageSemantics.eval_expr ?m ?l ?e ?k ?mc] => specialize (IH k)
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma metricleakage_to_leakage_eval_expr: forall m l e k v k',
+      LeakageSemantics.eval_expr m l e k = Some (v, k') ->
+      forall mc, exists mc', MetricLeakageSemantics.eval_expr m l e k mc = Some (v, k', mc').
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _ _ _, LeakageSemantics.eval_expr _ _ _ _ = Some _ -> _ |- _
+          => specialize (IH _ _ _ ltac:(eassumption))
+        | IH: forall _: MetricLog, exists _: MetricLog, MetricLeakageSemantics.eval_expr ?m ?l ?e _ _ = Some _
+          |- context[MetricLeakageSemantics.eval_expr ?m ?l ?e ?k ?mc] => specialize (IH mc)
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma metricleakage_to_plain_eval_call_args: forall m l arges args,
+      Semantics.eval_call_args m l arges = Some args ->
+      forall k mc, exists k' mc', eval_call_args m l arges k mc = Some (args, k', mc').
+  Proof.
+    induction arges; cbn; intros.
+    - eapply Option.eq_of_eq_Some in H. subst. eauto.
+    - fwd.
+      eapply metricleakage_to_plain_eval_expr in E. destruct E as (k' & mc' & E). rewrite E.
+      specialize IHarges with (1 := eq_refl). specialize (IHarges k' mc').
+      destruct IHarges as (k'' & mc'' & IH). rewrite IH. eauto.
+  Qed.
+
+  Lemma metricleakage_to_metric_eval_call_args: forall m l arges mc args mc',
+      MetricSemantics.eval_call_args m l arges mc = Some (args, mc') ->
+      forall k, exists k', eval_call_args m l arges k mc = Some (args, k', mc').
+  Proof.
+    induction arges; cbn; intros.
+    - inversion H. subst. eauto.
+    - fwd.
+      eapply metricleakage_to_metric_eval_expr in E. destruct E as (k' & E). rewrite E.
+      specialize (IHarges _ _ _ ltac:(eassumption) k').
+      destruct IHarges as (k'' & IH). rewrite IH. eauto.
+  Qed.
+
+  Lemma metricleakage_to_leakage_eval_call_args: forall m l arges k args k',
+      LeakageSemantics.eval_call_args m l arges k = Some (args, k') ->
+      forall mc, exists mc', eval_call_args m l arges k mc = Some (args, k', mc').
+  Proof.
+    induction arges; cbn; intros.
+    - inversion H. subst. eauto.
+    - fwd.
+      eapply metricleakage_to_leakage_eval_expr in E. destruct E as (mc' & E). rewrite E.
+      specialize (IHarges _ _ _ ltac:(eassumption) mc').
+      destruct IHarges as (mc'' & IH). rewrite IH. eauto.
+  Qed.
+
+  Definition deleakaged_ext_spec : Semantics.ExtSpec :=
+    fun t mGive a args post => ext_spec t mGive a args (fun mReceive resvals klist => post mReceive resvals).
+  
+  Lemma deleakaged_ext_spec_ok {ext_spec_ok: ext_spec.ok ext_spec}:
+    Semantics.ext_spec.ok deleakaged_ext_spec.
+  Proof.
+    destruct ext_spec_ok. cbv [deleakaged_ext_spec]. constructor; eauto.
+    intros. cbv [Morphisms.Proper Morphisms.respectful Morphisms.pointwise_relation Basics.impl] in *.
+    intros. eapply weaken; eauto. intros. apply H. simpl in *. assumption.
+  Qed.    
+
+  Context (e: env).
+  Existing Instance deleakaged_ext_spec.
+  Existing Instance deleakaged_ext_spec_ok.
+
+  Lemma metricleakage_to_plain_exec: forall c t m l post,
+      Semantics.exec e c t m l post ->
+      forall k mc, MetricLeakageSemantics.exec e c k t m l mc (fun _ t' m' l' _ => post t' m' l').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: Semantics.eval_expr _ _ _ = Some _ |- _ =>
+            eapply metricleakage_to_plain_eval_expr in H; destruct H as (? & ? & H)
+        | H: Semantics.eval_call_args _ _ _ = Some _ |- _ =>
+            eapply metricleakage_to_plain_eval_call_args in H; destruct H as (? & ? & H)
+        end;
+      try solve [econstructor; eauto].
+  Qed.
+
+  Lemma metricleakage_to_metric_exec: forall c t m l mc post,
+      MetricSemantics.exec e c t m l mc post ->
+      forall k, MetricLeakageSemantics.exec e c k t m l mc (fun _ t' m' l' mc' => post t' m' l' mc').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: MetricSemantics.eval_expr _ _ _ _ = Some _ |- _ =>
+            eapply metricleakage_to_metric_eval_expr in H; destruct H as (? & H)
+        | H: MetricSemantics.eval_call_args _ _ _ _ = Some _ |- _ =>
+            eapply metricleakage_to_metric_eval_call_args in H; destruct H as (? & H)
+        end;
+      try solve [econstructor; eauto].
+  Qed.
+
+  Lemma metricleakage_to_leakage_exec: forall c t m l k post,
+      LeakageSemantics.exec e c k t m l post ->
+      forall mc, MetricLeakageSemantics.exec e c k t m l mc (fun k' t' m' l' _ => post k' t' m' l').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: LeakageSemantics.eval_expr _ _ _ _ = Some _ |- _ =>
+            eapply metricleakage_to_leakage_eval_expr in H; destruct H as (? & H)
+        | H: LeakageSemantics.eval_call_args _ _ _ _ = Some _ |- _ =>
+            eapply metricleakage_to_leakage_eval_call_args in H; destruct H as (? & H)
+        end;
+      try solve [econstructor; eauto].
+  Qed.
+
+  Lemma metricleakage_to_plain_call: forall f t m args post,
+      Semantics.call e f t m args post ->
+      forall k mc, MetricLeakageSemantics.call e f k t m args mc (fun _ t' m' rets _ => post t' m' rets).
+  Proof.
+    unfold MetricLeakageSemantics.call, Semantics.call. intros. fwd. eauto 10 using metricleakage_to_plain_exec.
+  Qed.
+
+  Lemma metricleakage_to_metric_call: forall f t m args mc post,
+      MetricSemantics.call e f t m args mc post ->
+      forall k, MetricLeakageSemantics.call e f k t m args mc (fun _ t' m' rets mc' => post t' m' rets mc').
+  Proof.
+    unfold MetricLeakageSemantics.call, MetricSemantics.call. intros. fwd. eauto 10 using metricleakage_to_metric_exec.
+  Qed.
+
+  Lemma metricleakage_to_leakage_call: forall f k t m args post,
+      LeakageSemantics.call e f k t m args post ->
+      forall mc, MetricLeakageSemantics.call e f k t m args mc (fun k' t' m' rets _ => post k' t' m' rets).
+  Proof.
+    unfold MetricLeakageSemantics.call, LeakageSemantics.call. intros. fwd. eauto 10 using metricleakage_to_leakage_exec.
+  Qed.
+End MetricLeakageToSomething.
+
+Section LeakageToSomething.
+  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}.
+
+  Lemma leakage_to_plain_eval_expr: forall m l e v,
+      Semantics.eval_expr m l e = Some v ->
+      forall k, exists k', LeakageSemantics.eval_expr m l e k = Some (v, k').
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _, Semantics.eval_expr _ _ _ = Some _ -> _ |- _ =>
+            specialize (IH _ ltac:(eassumption))
+        | IH: forall _: leakage, exists _: leakage,
+            LeakageSemantics.eval_expr ?m ?l ?e _ = Some _
+          |- context[LeakageSemantics.eval_expr ?m ?l ?e ?k] => specialize (IH k)
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma leakage_to_metric_eval_expr: forall m l e mc v mc',
+      MetricSemantics.eval_expr m l e mc = Some (v, mc') ->
+      forall k, exists k', LeakageSemantics.eval_expr m l e k = Some (v, k').
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _ _ _, MetricSemantics.eval_expr _ _ _ _ = Some _ -> _ |- _
+          => specialize (IH _ _ _ ltac:(eassumption))
+        | IH: forall _: leakage, exists _: leakage, LeakageSemantics.eval_expr ?m ?l ?e _ = Some _
+          |- context[LeakageSemantics.eval_expr ?m ?l ?e ?k] => specialize (IH k)
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma leakage_to_metricleakage_eval_expr: forall m l e k v k' mc mc',
+      MetricLeakageSemantics.eval_expr m l e k mc = Some (v, k', mc') ->
+      LeakageSemantics.eval_expr m l e k = Some (v, k').
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _ _ _ _ _, MetricLeakageSemantics.eval_expr _ _ _ _ _ = Some _ -> _ |- _
+          => specialize (IH _ _ _ _ _ ltac:(eassumption))
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma leakage_to_plain_eval_call_args: forall m l arges args,
+      Semantics.eval_call_args m l arges = Some args ->
+      forall k, exists k', LeakageSemantics.eval_call_args m l arges k = Some (args, k').
+  Proof.
+    induction arges; cbn; intros.
+    - eapply Option.eq_of_eq_Some in H. subst. eauto.
+    - fwd.
+      eapply leakage_to_plain_eval_expr in E. destruct E as (k' & E). rewrite E.
+      specialize IHarges with (1 := eq_refl). specialize (IHarges k').
+      destruct IHarges as (k'' & IH). rewrite IH. eauto.
+  Qed.
+
+  Lemma leakage_to_metric_eval_call_args: forall m l arges mc args mc',
+      MetricSemantics.eval_call_args m l arges mc = Some (args, mc') ->
+      forall k, exists k', LeakageSemantics.eval_call_args m l arges k = Some (args, k').
+  Proof.
+    induction arges; cbn; intros.
+    - inversion H. subst. eauto.
+    - fwd.
+      eapply leakage_to_metric_eval_expr in E. destruct E as (k' & E). rewrite E.
+      specialize (IHarges _ _ _ ltac:(eassumption) k').
+      destruct IHarges as (k'' & IH). rewrite IH. eauto.
+  Qed.
+
+  Lemma leakage_to_metricleakage_eval_call_args: forall m l arges k mc args k' mc',
+      MetricLeakageSemantics.eval_call_args m l arges k mc = Some (args, k', mc') ->
+      LeakageSemantics.eval_call_args m l arges k = Some (args, k').
+  Proof.
+    induction arges; cbn; intros.
+    - inversion H. subst. eauto.
+    - fwd.
+      eapply leakage_to_metricleakage_eval_expr in E. rewrite E.
+      specialize (IHarges _ _ _ _ _ ltac:(eassumption)).
+      rewrite IHarges. eauto.
+  Qed.
+
+  Context (e: env).
+  Existing Instance deleakaged_ext_spec.
+  Existing Instance deleakaged_ext_spec_ok.
+
+  Lemma leakage_to_plain_exec: forall c t m l post,
+      Semantics.exec e c t m l post ->
+      forall k, LeakageSemantics.exec e c k t m l (fun _ t' m' l' => post t' m' l').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: Semantics.eval_expr _ _ _ = Some _ |- _ =>
+            eapply leakage_to_plain_eval_expr in H; destruct H as (? & H)
+        | H: Semantics.eval_call_args _ _ _ = Some _ |- _ =>
+            eapply leakage_to_plain_eval_call_args in H; destruct H as (? & H)
+        end;
+      try solve [econstructor; eauto].
+  Qed.
+
+  Lemma leakage_to_metric_exec: forall c t m l mc post,
+      MetricSemantics.exec e c t m l mc post ->
+      forall k, LeakageSemantics.exec e c k t m l (fun _ t' m' l' => exists mc', post t' m' l' mc').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: MetricSemantics.eval_expr _ _ _ _ = Some _ |- _ =>
+            eapply leakage_to_metric_eval_expr in H; destruct H as (? & H)
+        | H: MetricSemantics.eval_call_args _ _ _ _ = Some _ |- _ =>
+            eapply leakage_to_metric_eval_call_args in H; destruct H as (? & H)
+        end;
+      try solve [econstructor; eauto].
+    all: try solve [econstructor; eauto; simpl; intros; fwd; eauto].
+    - econstructor; eauto. intros. eapply LeakageSemantics.exec.weaken.
+      1: eapply H1; solve[eauto]. simpl. intros. fwd. eexists. eexists. eauto.
+    - econstructor; eauto. simpl. intros. fwd. apply H3 in H4. fwd. eauto 10.
+    - econstructor; eauto. simpl. intros. apply H2 in H3. fwd. eauto.
+  Qed.
+
+  Lemma leakage_to_metricleakage_exec: forall c t m l k mc post,
+      MetricLeakageSemantics.exec e c k t m l mc post ->
+      LeakageSemantics.exec e c k t m l (fun k' t' m' l' => exists mc', post k' t' m' l' mc').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: MetricLeakageSemantics.eval_expr _ _ _ _ _ = Some _ |- _ =>
+            eapply leakage_to_metricleakage_eval_expr in H
+        | H: MetricLeakageSemantics.eval_call_args _ _ _ _ _ = Some _ |- _ =>
+            eapply leakage_to_metricleakage_eval_call_args in H
+        end;
+      try solve [econstructor; eauto].
+    all: try solve [econstructor; eauto; simpl; intros; fwd; eauto].
+    - econstructor; eauto. intros. eapply LeakageSemantics.exec.weaken.
+      1: eapply H1; solve[eauto]. simpl. intros. fwd. eexists. eexists. eauto.
+    - econstructor; eauto. simpl. intros. fwd. apply H3 in H4. fwd. eauto 10.
+    - econstructor; eauto. simpl. intros. apply H2 in H3. fwd. eauto.
+  Qed.
+
+  Lemma leakage_to_plain_call: forall f t m args post,
+      Semantics.call e f t m args post ->
+      forall k, LeakageSemantics.call e f k t m args (fun _ t' m' rets => post t' m' rets).
+  Proof.
+    unfold LeakageSemantics.call, Semantics.call. intros. fwd. eauto 10 using leakage_to_plain_exec.
+  Qed.
+
+  Lemma leakage_to_metric_call: forall f t m args mc post,
+      MetricSemantics.call e f t m args mc post ->
+      forall k, LeakageSemantics.call e f k t m args (fun _ t' m' rets => exists mc', post t' m' rets mc').
+  Proof.
+    unfold LeakageSemantics.call, MetricSemantics.call. intros. fwd. do 3 eexists.
+    intuition eauto. eexists. intuition eauto. eapply LeakageSemantics.exec.weaken.
+    - eauto 10 using leakage_to_metric_exec.
+    - simpl. intros. fwd. eauto.
+  Qed.
+
+  Lemma leakage_to_metricleakage_call: forall f k t m args mc post,
+      MetricLeakageSemantics.call e f k t m args mc post ->
+      LeakageSemantics.call e f k t m args (fun k' t' m' rets => exists mc', post k' t' m' rets mc').
+  Proof.
+    unfold LeakageSemantics.call, MetricLeakageSemantics.call. intros. fwd.
+    do 3 eexists. intuition eauto. eexists. intuition eauto.
+    eapply LeakageSemantics.exec.weaken.
+    - eauto 10 using leakage_to_metricleakage_exec.
+    - simpl. intros. fwd. eauto.
+  Qed.
+End LeakageToSomething.
+
+Section MetricToSomething.
+  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: Semantics.ExtSpec}.
+
+  Lemma metric_to_plain_eval_expr: forall (m : mem) l e v,
+      Semantics.eval_expr m l e = Some v ->
+      forall mc, exists mc', MetricSemantics.eval_expr m l e mc = Some (v, mc').
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _, Semantics.eval_expr _ _ _ = Some _ -> _ |- _ =>
+            specialize (IH _ ltac:(eassumption))
+        | IH: forall _: MetricLog, exists _: MetricLog,
+            MetricSemantics.eval_expr ?m ?l ?e _ = Some _
+          |- context[MetricSemantics.eval_expr ?m ?l ?e ?mc] => specialize (IH mc)
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma metric_to_plain_eval_call_args: forall (m : mem) l arges args,
+      Semantics.eval_call_args m l arges = Some args ->
+      forall mc, exists mc', MetricSemantics.eval_call_args m l arges mc = Some (args, mc').
+  Proof.
+    induction arges; cbn; intros.
+    - eapply Option.eq_of_eq_Some in H. subst. eauto.
+    - fwd.
+      eapply metric_to_plain_eval_expr in E. destruct E as (mc' & E). rewrite E.
+      specialize IHarges with (1 := eq_refl). specialize (IHarges mc').
+      destruct IHarges as (mc'' & IH). rewrite IH. eauto.
+  Qed.
+
+  Context (e: env).
+
+  Lemma metric_to_plain_exec: forall c t (m : mem) l post,
+      Semantics.exec e c t m l post ->
+      forall mc, MetricSemantics.exec e c t m l mc (fun t' m' l' _ => post t' m' l').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: Semantics.eval_expr _ _ _ = Some _ |- _ =>
+            eapply metric_to_plain_eval_expr in H; destruct H as (? & H)
+        | H: Semantics.eval_call_args _ _ _ = Some _ |- _ =>
+            eapply metric_to_plain_eval_call_args in H; destruct H as (? & H)
+        end;
+      try solve [econstructor; eauto].
+  Qed.
+  
+  Lemma metric_to_plain_call: forall f t m args post,
+      Semantics.call e f t m args post ->
+      forall mc, MetricSemantics.call e f t m args mc (fun t' m' rets _ => post t' m' rets).
+  Proof.
+    unfold MetricSemantics.call, Semantics.call. intros. fwd. eauto 10 using metric_to_plain_exec.
+  Qed.
+End MetricToSomething.
+
+Section PlainToSomething.
+  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: Semantics.ExtSpec}.
+
+  Lemma plain_to_metric_eval_expr: forall (m : mem) l e mc v mc',
+      MetricSemantics.eval_expr m l e mc = Some (v, mc') ->
+      Semantics.eval_expr m l e = Some v.
+  Proof.
+    induction e; cbn; intros;
+      repeat match goal with
+        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
+        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
+        | IH: forall _ _ _, MetricSemantics.eval_expr _ _ _ _ = Some _ -> _ |- _ =>
+            specialize (IH _ _ _ ltac:(eassumption))
+        | |- _ => progress fwd
+        | |- _ => Tactics.destruct_one_match
+        end;
+      eauto.
+  Qed.
+
+  Lemma plain_to_metric_eval_call_args: forall (m : mem) l arges mc args mc',
+      MetricSemantics.eval_call_args m l arges mc = Some (args, mc') ->
+      Semantics.eval_call_args m l arges = Some args.
+  Proof.
+    induction arges; cbn; intros.
+    - eapply Option.eq_of_eq_Some in H. inversion H. subst. eauto.
+    - fwd.
+      eapply plain_to_metric_eval_expr in E. rewrite E.
+      apply IHarges in E0. rewrite E0. reflexivity.
+  Qed.
+
+  Context (e: env).
+
+  Lemma plain_to_metric_exec: forall c t (m : mem) l mc post,
+      MetricSemantics.exec e c t m l mc post ->
+      Semantics.exec e c t m l (fun t' m' l' => exists mc', post t' m' l' mc').
+  Proof.
+    induction 1; intros;
+      repeat match reverse goal with
+        | H: MetricSemantics.eval_expr _ _ _ _ = Some _ |- _ =>
+            eapply plain_to_metric_eval_expr in H
+        | H: MetricSemantics.eval_call_args _ _ _ _ = Some _ |- _ =>
+            eapply plain_to_metric_eval_call_args in H
+        end;
+      try solve [econstructor; eauto].
+    all: try solve [econstructor; eauto; simpl; intros; fwd; eauto].
+    - econstructor; eauto. intros. eapply Semantics.exec.weaken.
+      1: eapply H1; solve[eauto]. simpl. intros. fwd. eexists. eexists. eauto.
+    - econstructor; eauto. simpl. intros. fwd. apply H3 in H4. fwd. eauto 10.
+    - econstructor; eauto. simpl. intros. apply H2 in H3. fwd. eauto.
+  Qed.
+
+  Lemma plain_to_metric_call: forall f t m args mc post,
+      MetricSemantics.call e f t m args mc post ->
+      Semantics.call e f t m args (fun t' m' rets => exists mc', post t' m' rets mc').
+  Proof.
+    unfold MetricSemantics.call, Semantics.call. intros. fwd.
+    do 3 eexists. intuition eauto. eexists. intuition eauto.
+    eapply Semantics.exec.weaken.
+    - eauto 10 using plain_to_metric_exec.
+    - simpl. intros. fwd. eauto.
+  Qed.
+End PlainToSomething.
diff --git a/bedrock2/src/bedrock2/memory_mapped_ext_spec.v b/bedrock2/src/bedrock2/memory_mapped_ext_spec.v
index 2067585d7..63890e2f9 100644
--- a/bedrock2/src/bedrock2/memory_mapped_ext_spec.v
+++ b/bedrock2/src/bedrock2/memory_mapped_ext_spec.v
@@ -10,7 +10,8 @@ Require coqutil.Datatypes.String.
 Require Import coqutil.Map.Interface coqutil.Map.Domain.
 Require Import coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import coqutil.Word.Properties.
-Require Import bedrock2.Semantics bedrock2.LeakageSemantics bedrock2.MetricLeakageSemantics.
+Require Import bedrock2.Semantics bedrock2.LeakageSemantics.
+Require Import bedrock2.SemanticsRelations.
 Require Import bedrock2.TraceInspection.
 Local Open Scope string_scope.
 
diff --git a/compiler/src/compilerExamples/memequal.v b/compiler/src/compilerExamples/memequal.v
index 436fdb6c0..2baf3c2e6 100644
--- a/compiler/src/compilerExamples/memequal.v
+++ b/compiler/src/compilerExamples/memequal.v
@@ -128,7 +128,7 @@ Proof.
   { subst. cbv [fname_memequal]. move spec at bottom.
     specialize (spec x y n xs ys Rx Ry [] (initial.(getLog)) m ltac:(intuition eauto)).
     eapply MetricLeakageSemantics.weaken_call.
-    { eapply MetricLeakageSemantics.to_leakage_call. exact spec. }
+    { eapply SemanticsRelations.metricleakage_to_leakage_call. exact spec. }
     cbv beta. intros. fwd. split; [|reflexivity]. reflexivity. }
   { reflexivity. }
   { reflexivity. }
diff --git a/end2end/src/end2end/End2EndPipeline.v b/end2end/src/end2end/End2EndPipeline.v
index 3bd216db8..3bbdc33c2 100644
--- a/end2end/src/end2end/End2EndPipeline.v
+++ b/end2end/src/end2end/End2EndPipeline.v
@@ -362,13 +362,13 @@ Section Connect.
                rewrite heap_start_agree in H;
                rewrite heap_pastend_agree in H
              end.
-             eapply MetricLeakageSemantics.to_plain_exec.
+             eapply SemanticsRelations.metricleakage_to_plain_exec.
              eapply WeakestPreconditionProperties.sound_cmd; eauto.
           -- simpl. clear. intros. unfold bedrock2Inv in *. eauto.
         * exact GetLoop.
         * intros. unfold bedrock2Inv in *.
           eapply MetricLeakageSemantics.exec.weaken.
-          -- eapply MetricLeakageSemantics.to_plain_exec.
+          -- eapply SemanticsRelations.metricleakage_to_plain_exec.
              eapply WeakestPreconditionProperties.sound_cmd; eauto.
           -- simpl. clear. intros. eauto.
       + assumption.