Base Dead Code Elim on Subst01

Based on https://github.com/coq/coq/issues/8993#issuecomment-438572277,
I am guessing that DCE is currently memory-hungry.  This makes sense,
because every [var] is carrying around a full `PositiveSet.t` when
computing live variables.  Instead, we now adjust `subst01` to not
increment counts coming from dead variables, and use it to implement
DCE.  Hopefully this will be much faster and more efficient.

N.B. It was important to stop doing union of `PositiveMap.t`, and
instead add to them incrementally.

Before: p384_32.c (real: 406.78, user: 391.99, sys: 14.82, mem: 16896040 ko)
After:  p384_32.c (real: 201.11, user: 200.33, sys:  0.80, mem:  1039520 ko)

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
21m16.47s | Total                                                                | 24m45.69s || -3m29.22s | -14.08%
--------------------------------------------------------------------------------------------------------------------
3m20.33s  | p384_32.c                                                            | 6m31.99s  || -3m11.66s | -48.89%
0m14.08s  | secp256k1_32.c                                                       | 0m18.85s  || -0m04.77s | -25.30%
0m13.86s  | p256_32.c                                                            | 0m18.14s  || -0m04.28s | -23.59%
6m14.92s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo                | 6m17.66s  || -0m02.74s | -0.72%
4m37.51s  | Experiments/NewPipeline/Toplevel1.vo                                 | 4m39.20s  || -0m01.68s | -0.60%
0m06.46s  | p224_32.c                                                            | 0m07.85s  || -0m01.38s | -17.70%
0m02.49s  | Experiments/NewPipeline/MiscCompilerPassesProofs.vo                  | 0m03.85s  || -0m01.35s | -35.32%
1m32.10s  | Experiments/NewPipeline/Toplevel2.vo                                 | 1m31.75s  || +0m00.34s | +0.38%
0m42.06s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m42.17s  || -0m00.10s | -0.26%
0m39.54s  | p521_32.c                                                            | 0m39.37s  || +0m00.17s | +0.43%
0m39.45s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m39.51s  || -0m00.05s | -0.15%
0m32.87s  | p521_64.c                                                            | 0m32.94s  || -0m00.07s | -0.21%
0m25.29s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m25.26s  || +0m00.02s | +0.11%
0m23.06s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m23.20s  || -0m00.14s | -0.60%
0m18.73s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m19.01s  || -0m00.28s | -1.47%
0m14.93s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m15.04s  || -0m00.10s | -0.73%
0m10.58s  | p384_64.c                                                            | 0m11.21s  || -0m00.63s | -5.61%
0m09.12s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.90s  || +0m00.21s | +2.47%
0m05.94s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m06.06s  || -0m00.11s | -1.98%
0m05.78s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.76s  || +0m00.02s | +0.34%
0m04.36s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m04.37s  || -0m00.00s | -0.22%
0m04.23s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.24s  || -0m00.00s | -0.23%
0m03.47s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.68s  || -0m00.20s | -5.70%
0m02.38s  | curve25519_32.c                                                      | 0m02.39s  || -0m00.01s | -0.41%
0m02.04s  | secp256k1_64.c                                                       | 0m02.09s  || -0m00.04s | -2.39%
0m01.94s  | p224_64.c                                                            | 0m01.96s  || -0m00.02s | -1.02%
0m01.90s  | p256_64.c                                                            | 0m01.96s  || -0m00.06s | -3.06%
0m01.52s  | curve25519_64.c                                                      | 0m01.60s  || -0m00.08s | -5.00%
0m01.47s  | Experiments/NewPipeline/CLI.vo                                       | 0m01.44s  || +0m00.03s | +2.08%
0m01.22s  | Experiments/NewPipeline/StandaloneHaskellMain.vo                     | 0m01.26s  || -0m00.04s | -3.17%
0m01.21s  | Experiments/NewPipeline/StandaloneOCamlMain.vo                       | 0m01.27s  || -0m00.06s | -4.72%
0m00.97s  | Experiments/NewPipeline/CompilersTestCases.vo                        | 0m01.10s  || -0m00.13s | -11.81%
0m00.66s  | Experiments/NewPipeline/MiscCompilerPasses.vo                        | 0m00.62s  || +0m00.04s | +6.45%

3 files changed, 214 insertions, 259 deletions

diff --git a/src/Experiments/NewPipeline/MiscCompilerPasses.v b/src/Experiments/NewPipeline/MiscCompilerPasses.v
index 66dd7c09c..d04d4c742 100644
--- a/src/Experiments/NewPipeline/MiscCompilerPasses.v
+++ b/src/Experiments/NewPipeline/MiscCompilerPasses.v
@@ -11,137 +11,108 @@ Module Compilers.
   Import invert_expr.
   Import defaults.
 
-  Module DeadCodeElimination.
-    Section with_ident.
-      Context {base_type : Type}.
-      Local Notation type := (type.type base_type).
-      Context {ident : type -> Type}.
-      Local Notation expr := (@expr.expr base_type ident).
-      Fixpoint compute_live' {t} (e : @expr (fun _ => PositiveSet.t) t) (cur_idx : positive)
-        : positive * PositiveSet.t
-        := match e with
-           | expr.Var t v => (cur_idx, v)
-           | expr.App s d f x
-             => let '(idx, live1) := @compute_live' _ f cur_idx in
-                let '(idx, live2) := @compute_live' _ x idx in
-                (idx, PositiveSet.union live1 live2)
-           | expr.Abs s d f
-             => let '(_, live) := @compute_live' _ (f PositiveSet.empty) cur_idx in
-                (cur_idx, live)
-           | expr.LetIn tx tC ex eC
-             => let '(idx, live) := @compute_live' tx ex cur_idx in
-                let '(_, live) := @compute_live' tC (eC (PositiveSet.add idx live)) (Pos.succ idx) in
-                (Pos.succ idx, live)
-           | expr.Ident t idc => (cur_idx, PositiveSet.empty)
-           end.
-      Definition compute_live {t} e : PositiveSet.t := snd (@compute_live' t e 1).
-      Definition ComputeLive {t} (e : expr.Expr t) := compute_live (e _).
+  Module Subst01.
+    Section with_counter.
+      Context {t : Type}
+              (one : t)
+              (incr : t -> t).
 
-      Section with_var.
-        Context {var : type -> Type}
-                (live : PositiveSet.t).
-        Definition OUGHT_TO_BE_UNUSED {T1 T2} (v : T1) (v' : T2) := v.
-        Global Opaque OUGHT_TO_BE_UNUSED.
-        Fixpoint eliminate_dead' {t} (e : @expr (@expr var) t) (cur_idx : positive)
-          : positive * @expr var t
+      Local Notation PositiveMap_incr idx m
+        := (PositiveMap.add idx (match PositiveMap.find idx m with
+                                 | Some n => incr n
+                                 | None => one
+                                 end) m).
+
+      Section with_ident.
+        Context {base_type : Type}.
+        Local Notation type := (type.type base_type).
+        Context {ident : type -> Type}.
+        Local Notation expr := (@expr.expr base_type ident).
+        (** N.B. This does not work well when let-binders are not at top-level *)
+        Fixpoint compute_live_counts' {t} (e : @expr (fun _ => positive) t) (cur_idx : positive) (live : PositiveMap.t _)
+          : positive * PositiveMap.t _
           := match e with
-             | expr.Var t v => (cur_idx, v)
-             | expr.Ident t idc => (cur_idx, expr.Ident idc)
+             | expr.Var t v => (cur_idx, PositiveMap_incr v live)
+             | expr.Ident t idc => (cur_idx, live)
              | expr.App s d f x
-               => let '(idx, f') := @eliminate_dead' _ f cur_idx in
-                  let '(idx, x') := @eliminate_dead' _ x idx in
-                  (idx, expr.App f' x')
+               => let '(idx, live) := @compute_live_counts' _ f cur_idx live in
+                  let '(idx, live) := @compute_live_counts' _ x idx live in
+                  (idx, live)
              | expr.Abs s d f
-               => (cur_idx, expr.Abs (fun v => snd (@eliminate_dead' _ (f (expr.Var v)) cur_idx)))
+               => let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in
+                  (cur_idx, live)
              | expr.LetIn tx tC ex eC
-               => let '(idx, ex') := @eliminate_dead' tx ex cur_idx in
-                  let eC' := fun v => snd (@eliminate_dead' _ (eC v) (Pos.succ idx)) in
-                  if PositiveSet.mem idx live
-                  then (Pos.succ idx, expr.LetIn ex' (fun v => eC' (expr.Var v)))
-                  else (Pos.succ idx, eC' (OUGHT_TO_BE_UNUSED ex' (Pos.succ idx, PositiveSet.elements live)))
+               => let '(idx, live) := @compute_live_counts' tC (eC cur_idx) (Pos.succ cur_idx) live in
+                  if PositiveMap.mem cur_idx live
+                  then @compute_live_counts' tx ex idx live
+                  else (idx, live)
              end.
+        Definition compute_live_counts {t} e : PositiveMap.t _ := snd (@compute_live_counts' t e 1 (PositiveMap.empty _)).
+        Definition ComputeLiveCounts {t} (e : expr.Expr t) := compute_live_counts (e _).
 
-        Definition eliminate_dead {t} e : expr t
-          := snd (@eliminate_dead' t e 1).
-      End with_var.
+        Section with_var.
+          Context (doing_subst : forall T1 T2, T1 -> T2 -> T1)
+                  {var : type -> Type}
+                  (should_subst : t -> bool)
+                  (live : PositiveMap.t t).
+          Fixpoint subst0n' {t} (e : @expr (@expr var) t) (cur_idx : positive)
+            : positive * @expr var t
+            := match e with
+               | expr.Var t v => (cur_idx, v)
+               | expr.Ident t idc => (cur_idx, expr.Ident idc)
+               | expr.App s d f x
+                 => let '(idx, f') := @subst0n' _ f cur_idx in
+                    let '(idx, x') := @subst0n' _ x idx in
+                    (idx, expr.App f' x')
+               | expr.Abs s d f
+                 => (cur_idx, expr.Abs (fun v => snd (@subst0n' _ (f (expr.Var v)) (Pos.succ cur_idx))))
+               | expr.LetIn tx tC ex eC
+                 => let '(idx, ex') := @subst0n' tx ex cur_idx in
+                    let eC' := fun v => snd (@subst0n' tC (eC v) (Pos.succ cur_idx)) in
+                    if match PositiveMap.find cur_idx live with
+                       | Some n => should_subst n
+                       | None => true
+                       end
+                    then (Pos.succ cur_idx, eC' (doing_subst _ _ ex' (Pos.succ cur_idx, PositiveMap.elements live)))
+                    else (Pos.succ cur_idx, expr.LetIn ex' (fun v => eC' (expr.Var v)))
+               end.
 
-      Definition EliminateDead {t} (e : expr.Expr t) : expr.Expr t
-        := fun var => eliminate_dead (ComputeLive e) (e _).
-    End with_ident.
-  End DeadCodeElimination.
+          Definition subst0n {t} e : expr t
+            := snd (@subst0n' t e 1).
+        End with_var.
 
-  Module Subst01.
-    Local Notation PositiveMap_incr idx m
-      := (PositiveMap.add idx (match PositiveMap.find idx m with
-                               | Some n => S n
-                               | None => S O
-                               end) m).
-    Local Notation PositiveMap_union m1 m2
-      := (PositiveMap.map2
-            (fun c1 c2
-             => match c1, c2 with
-                | Some n1, Some n2 => Some (n1 + n2)%nat
-                | Some n, None
-                | None, Some n
-                  => Some n
-                | None, None => None
-                end) m1 m2).
+        Definition Subst0n (doing_subst : forall T1 T2, T1 -> T2 -> T1) (should_subst : t -> bool) {t} (e : expr.Expr t) : expr.Expr t
+          := fun var => subst0n doing_subst should_subst (ComputeLiveCounts e) (e _).
+      End with_ident.
+    End with_counter.
+
+    Section for_01.
+      Inductive one_or_more := one | more.
+      Local Notation t := one_or_more.
+      Let incr : t -> t := fun _ => more.
+      Let should_subst : t -> bool
+        := fun v => match v with
+                    | one => true
+                    | more => false
+                    end.
+
+      Definition Subst01 {base_type ident} {t} (e : expr.Expr t) : expr.Expr t
+        := @Subst0n _ one incr base_type ident (fun _ _ x _ => x) should_subst t e.
+    End for_01.
+  End Subst01.
+
+  Module DeadCodeElimination.
     Section with_ident.
       Context {base_type : Type}.
       Local Notation type := (type.type base_type).
       Context {ident : type -> Type}.
       Local Notation expr := (@expr.expr base_type ident).
-      Fixpoint compute_live_counts' {t} (e : @expr (fun _ => positive) t) (cur_idx : positive)
-        : positive * PositiveMap.t nat
-        := match e with
-           | expr.Var t v => (cur_idx, PositiveMap_incr v (PositiveMap.empty _))
-           | expr.Ident t idc => (cur_idx, PositiveMap.empty _)
-           | expr.App s d f x
-             => let '(idx, live1) := @compute_live_counts' _ f cur_idx in
-                let '(idx, live2) := @compute_live_counts' _ x idx in
-                (idx, PositiveMap_union live1 live2)
-           | expr.Abs s d f
-             => let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) in
-                (cur_idx, live)
-           | expr.LetIn tx tC ex eC
-             => let '(idx, live1) := @compute_live_counts' tx ex cur_idx in
-                let '(idx, live2) := @compute_live_counts' tC (eC idx) (Pos.succ idx) in
-                (idx, PositiveMap_union live1 live2)
-           end.
-      Definition compute_live_counts {t} e : PositiveMap.t _ := snd (@compute_live_counts' t e 1).
-      Definition ComputeLiveCounts {t} (e : expr.Expr t) := compute_live_counts (e _).
 
-      Section with_var.
-        Context {var : type -> Type}
-                (live : PositiveMap.t nat).
-        Fixpoint subst01' {t} (e : @expr (@expr var) t) (cur_idx : positive)
-          : positive * @expr var t
-          := match e with
-             | expr.Var t v => (cur_idx, v)
-             | expr.Ident t idc => (cur_idx, expr.Ident idc)
-             | expr.App s d f x
-               => let '(idx, f') := @subst01' _ f cur_idx in
-                  let '(idx, x') := @subst01' _ x idx in
-                  (idx, expr.App f' x')
-             | expr.Abs s d f
-               => (cur_idx, expr.Abs (fun v => snd (@subst01' _ (f (expr.Var v)) (Pos.succ cur_idx))))
-             | expr.LetIn tx tC ex eC
-               => let '(idx, ex') := @subst01' tx ex cur_idx in
-                  let eC' := fun v => snd (@subst01' tC (eC v) (Pos.succ idx)) in
-                  if match PositiveMap.find idx live with
-                     | Some n => (n <=? 1)%nat
-                     | None => true
-                     end
-                  then (Pos.succ idx, eC' ex')
-                  else (Pos.succ idx, expr.LetIn ex' (fun v => eC' (expr.Var v)))
-             end.
-
-        Definition subst01 {t} e : expr t
-          := snd (@subst01' t e 1).
-      End with_var.
+      Definition OUGHT_TO_BE_UNUSED {T1 T2} (v : T1) (v' : T2) := v.
+      Global Opaque OUGHT_TO_BE_UNUSED.
 
-      Definition Subst01 {t} (e : expr.Expr t) : expr.Expr t
-        := fun var => subst01 (ComputeLiveCounts e) (e _).
+      Definition EliminateDead {t} (e : expr.Expr t) : expr.Expr t
+        := @Subst01.Subst0n unit tt (fun _ => tt) base_type ident (@OUGHT_TO_BE_UNUSED) (fun _ => false) t e.
     End with_ident.
-  End Subst01.
+  End DeadCodeElimination.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v
index 52101023a..986bfaaa5 100644
--- a/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v
+++ b/src/Experiments/NewPipeline/MiscCompilerPassesProofs.v
@@ -24,22 +24,105 @@ Module Compilers.
   Import invert_expr.
   Import defaults.
 
-  Module DeadCodeElimination.
-    Import MiscCompilerPasses.Compilers.DeadCodeElimination.
-
-    (** Rather than proving correctness of the computation of live
-            variables and requiring something about [live], we instead
-            rely on the fact that DCE in fact just inlines code it
-            believes to be dead. *)
-    Local Transparent OUGHT_TO_BE_UNUSED.
-    Lemma OUGHT_TO_BE_UNUSED_id {T1 T2} (v : T1) (v' : T2) : OUGHT_TO_BE_UNUSED v v' = v.
-    Proof. exact eq_refl. Qed.
-    Local Opaque OUGHT_TO_BE_UNUSED.
+  Module Subst01.
+    Import MiscCompilerPasses.Compilers.Subst01.
 
     Local Ltac simplifier_t_step :=
       first [ progress cbn [fst snd] in *
-            | progress eta_expand
-            | rewrite OUGHT_TO_BE_UNUSED_id ].
+            | progress eta_expand ].
+
+    Section with_counter.
+      Context {T : Type}
+              (one : T)
+              (incr : T -> T).
+
+      Section with_ident.
+        Context {base_type : Type}.
+        Local Notation type := (type.type base_type).
+        Context {ident : type -> Type}.
+        Local Notation expr := (@expr.expr base_type ident).
+
+        Section with_var.
+          Context {doing_subst : forall T1 T2, T1 -> T2 -> T1}
+                  {should_subst : T -> bool}
+                  (Hdoing_subst : forall T1 T2 x y, doing_subst T1 T2 x y = x)
+                  {var1 var2 : type -> Type}
+                  (live : PositiveMap.t T).
+          Local Notation expr1 := (@expr.expr base_type ident var1).
+          Local Notation expr2 := (@expr.expr base_type ident var2).
+          Local Notation subst0n'1 := (@subst0n' T base_type ident doing_subst var1 should_subst live).
+          Local Notation subst0n'2 := (@subst0n' T base_type ident doing_subst var2 should_subst live).
+          Local Notation subst0n1 := (@subst0n T base_type ident doing_subst var1 should_subst live).
+          Local Notation subst0n2 := (@subst0n T base_type ident doing_subst var2 should_subst live).
+
+          Lemma wf_subst0n' G1 G2 t e1 e2 p
+                (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2)
+            : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (subst0n'1 e1 p)) (snd (subst0n'2 e2 p))
+                                         /\ fst (subst0n'1 e1 p) = fst (subst0n'2 e2 p).
+          Proof using Hdoing_subst.
+            intro Hwf; revert dependent G2; revert p; induction Hwf;
+              cbn [subst0n'];
+              repeat first [ progress wf_safe_t
+                           | simplifier_t_step
+                           | progress split_and
+                           | rewrite Hdoing_subst
+                           | apply conj
+                           | match goal with
+                             | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto
+                             end
+                           | break_innermost_match_step
+                           | solve [ wf_t ] ].
+          Qed.
+
+          Lemma wf_subst0n t e1 e2
+            : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst0n1 e1) (subst0n2 e2).
+          Proof using Hdoing_subst. clear -Hdoing_subst; intro Hwf; apply wf_subst0n' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed.
+        End with_var.
+
+        Lemma Wf_Subst0n
+              {doing_subst : forall T1 T2, T1 -> T2 -> T1}
+              {should_subst : T -> bool}
+              (Hdoing_subst : forall T1 T2 x y, doing_subst T1 T2 x y = x)
+              {t} (e : @expr.Expr base_type ident t)
+          : expr.Wf e -> expr.Wf (Subst0n one incr doing_subst should_subst e).
+        Proof using Type. intros Hwf var1 var2; eapply wf_subst0n, Hwf; assumption. Qed.
+
+        Section interp.
+          Context {base_interp : base_type -> Type}
+                  {interp_ident : forall t, ident t -> type.interp base_interp t}
+                  {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}.
+
+          Section with_doing_subst.
+            Context {doing_subst : forall T1 T2, T1 -> T2 -> T1}
+                    {should_subst : T -> bool}
+                    (Hdoing_subst : forall T1 T2 x y, doing_subst T1 T2 x y = x).
+
+            Lemma interp_subst0n'_gen (live : PositiveMap.t T) G t (e1 e2 : expr t)
+                  (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2)
+                  (Hwf : expr.wf G e1 e2)
+                  p
+              : expr.interp interp_ident (snd (subst0n' doing_subst should_subst live e1 p)) == expr.interp interp_ident e2.
+            Proof using Hdoing_subst interp_ident_Proper.
+              revert p; induction Hwf; cbn [subst0n']; cbv [Proper respectful] in *;
+                repeat first [ progress interp_safe_t
+                             | simplifier_t_step
+                             | rewrite Hdoing_subst
+                             | break_innermost_match_step
+                             | interp_unsafe_t_step ].
+            Qed.
+
+            Lemma interp_subst0n live t (e1 e2 : expr t)
+                  (Hwf : expr.wf nil e1 e2)
+              : expr.interp interp_ident (subst0n doing_subst should_subst live e1) == expr.interp interp_ident e2.
+            Proof using Hdoing_subst interp_ident_Proper. clear -Hwf Hdoing_subst interp_ident_Proper. apply interp_subst0n'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed.
+
+            Lemma Interp_Subst0n {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e)
+              : expr.Interp interp_ident (Subst0n one incr doing_subst should_subst e) == expr.Interp interp_ident e.
+            Proof using Hdoing_subst interp_ident_Proper. apply interp_subst0n, Hwf. Qed.
+          End with_doing_subst.
+        End interp.
+      End with_ident.
+    End with_counter.
 
     Section with_ident.
       Context {base_type : Type}.
@@ -47,82 +130,35 @@ Module Compilers.
       Context {ident : type -> Type}.
       Local Notation expr := (@expr.expr base_type ident).
 
-      Section with_var.
-        Context {var1 var2 : type -> Type}
-                (live : PositiveSet.t).
-        Local Notation expr1 := (@expr.expr base_type ident var1).
-        Local Notation expr2 := (@expr.expr base_type ident var2).
-        Local Notation eliminate_dead'1 := (@eliminate_dead' base_type ident var1 live).
-        Local Notation eliminate_dead'2 := (@eliminate_dead' base_type ident var2 live).
-        Local Notation eliminate_dead1 := (@eliminate_dead base_type ident var1 live).
-        Local Notation eliminate_dead2 := (@eliminate_dead base_type ident var2 live).
-
-        Lemma wf_eliminate_dead' G1 G2 t e1 e2 p
-              (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2)
-          : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (eliminate_dead'1 e1 p)) (snd (eliminate_dead'2 e2 p))
-                                      /\ fst (eliminate_dead'1 e1 p) = fst (eliminate_dead'2 e2 p).
-        Proof.
-          intro Hwf; revert dependent G2; revert p; induction Hwf;
-            cbn [eliminate_dead'];
-            repeat first [ progress wf_safe_t
-                         | simplifier_t_step
-                         | progress split_and
-                         | apply conj
-                         | match goal with
-                           | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto
-                           end
-                         | break_innermost_match_step
-                         | solve [ wf_t ] ].
-        Qed.
-
-        Lemma wf_eliminate_dead t e1 e2
-          : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (eliminate_dead1 e1) (eliminate_dead2 e2).
-        Proof. intro Hwf; apply wf_eliminate_dead' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed.
-      End with_var.
-
-      Lemma Wf_EliminateDead {t} (e : @expr.Expr base_type ident t)
-        : expr.Wf e -> expr.Wf (EliminateDead e).
-      Proof. intros Hwf var1 var2; eapply wf_eliminate_dead, Hwf. Qed.
+      Lemma Wf_Subst01 {t} (e : @expr.Expr base_type ident t)
+        : expr.Wf e -> expr.Wf (Subst01 e).
+      Proof using Type. eapply Wf_Subst0n; reflexivity. Qed.
 
       Section interp.
         Context {base_interp : base_type -> Type}
                 {interp_ident : forall t, ident t -> type.interp base_interp t}
                 {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}.
-
-        Lemma interp_eliminate_dead'_gen (live : PositiveSet.t) G t (e1 e2 : expr t)
-              (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2)
-              (Hwf : expr.wf G e1 e2)
-              p
-          : expr.interp interp_ident (snd (eliminate_dead' live e1 p)) == expr.interp interp_ident e2.
-        Proof.
-          revert p; induction Hwf; cbn [eliminate_dead']; cbv [Proper respectful] in *;
-            repeat first [ progress interp_safe_t
-                         | simplifier_t_step
-                         | break_innermost_match_step
-                         | interp_unsafe_t_step ].
-        Qed.
-
-        Lemma interp_eliminate_dead live t (e1 e2 : expr t)
-              (Hwf : expr.wf nil e1 e2)
-          : expr.interp interp_ident (eliminate_dead live e1) == expr.interp interp_ident e2.
-        Proof. apply interp_eliminate_dead'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed.
-
-        Lemma Interp_EliminateDead {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e)
-          : expr.Interp interp_ident (EliminateDead e) == expr.Interp interp_ident e.
-        Proof. apply interp_eliminate_dead, Hwf. Qed.
+        Lemma Interp_Subst01 {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e)
+          : expr.Interp interp_ident (Subst01 e) == expr.Interp interp_ident e.
+        Proof using interp_ident_Proper. apply Interp_Subst0n, Hwf; auto. Qed.
       End interp.
     End with_ident.
-  End DeadCodeElimination.
+  End Subst01.
 
-  Hint Resolve DeadCodeElimination.Wf_EliminateDead : wf.
-  Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp.
+  Hint Resolve Subst01.Wf_Subst01 : wf.
+  Hint Rewrite @Subst01.Interp_Subst01 : interp.
 
-  Module Subst01.
-    Import MiscCompilerPasses.Compilers.Subst01.
+  Module DeadCodeElimination.
+    Import MiscCompilerPasses.Compilers.DeadCodeElimination.
 
-    Local Ltac simplifier_t_step :=
-      first [ progress cbn [fst snd] in *
-            | progress eta_expand ].
+    (** Rather than proving correctness of the computation of live
+            variables and requiring something about [live], we instead
+            rely on the fact that DCE in fact just inlines code it
+            believes to be dead. *)
+    Local Transparent OUGHT_TO_BE_UNUSED.
+    Lemma OUGHT_TO_BE_UNUSED_id {T1 T2} (v : T1) (v' : T2) : OUGHT_TO_BE_UNUSED v v' = v.
+    Proof. exact eq_refl. Qed.
+    Local Opaque OUGHT_TO_BE_UNUSED.
 
     Section with_ident.
       Context {base_type : Type}.
@@ -130,73 +166,22 @@ Module Compilers.
       Context {ident : type -> Type}.
       Local Notation expr := (@expr.expr base_type ident).
 
-      Section with_var.
-        Context {var1 var2 : type -> Type}
-                (live : PositiveMap.t nat).
-        Local Notation expr1 := (@expr.expr base_type ident var1).
-        Local Notation expr2 := (@expr.expr base_type ident var2).
-        Local Notation subst01'1 := (@subst01' base_type ident var1 live).
-        Local Notation subst01'2 := (@subst01' base_type ident var2 live).
-        Local Notation subst011 := (@subst01 base_type ident var1 live).
-        Local Notation subst012 := (@subst01 base_type ident var2 live).
-
-        Lemma wf_subst01' G1 G2 t e1 e2 p
-              (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2)
-          : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (subst01'1 e1 p)) (snd (subst01'2 e2 p))
-                                      /\ fst (subst01'1 e1 p) = fst (subst01'2 e2 p).
-        Proof.
-          intro Hwf; revert dependent G2; revert p; induction Hwf;
-            cbn [subst01'];
-            repeat first [ progress wf_safe_t
-                         | simplifier_t_step
-                         | progress split_and
-                         | apply conj
-                         | match goal with
-                           | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto
-                           end
-                         | break_innermost_match_step
-                         | solve [ wf_t ] ].
-        Qed.
-
-        Lemma wf_subst01 t e1 e2
-          : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst011 e1) (subst012 e2).
-        Proof. intro Hwf; apply wf_subst01' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed.
-      End with_var.
-
-      Lemma Wf_Subst01 {t} (e : @expr.Expr base_type ident t)
-        : expr.Wf e -> expr.Wf (Subst01 e).
-      Proof. intros Hwf var1 var2; eapply wf_subst01, Hwf. Qed.
+      Lemma Wf_EliminateDead {t} (e : @expr.Expr base_type ident t)
+        : expr.Wf e -> expr.Wf (EliminateDead e).
+      Proof using Type. apply Subst01.Wf_Subst0n, @OUGHT_TO_BE_UNUSED_id. Qed.
 
       Section interp.
         Context {base_interp : base_type -> Type}
                 {interp_ident : forall t, ident t -> type.interp base_interp t}
                 {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}.
 
-        Lemma interp_subst01'_gen (live : PositiveMap.t nat) G t (e1 e2 : expr t)
-              (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2)
-              (Hwf : expr.wf G e1 e2)
-              p
-          : expr.interp interp_ident (snd (subst01' live e1 p)) == expr.interp interp_ident e2.
-        Proof.
-          revert p; induction Hwf; cbn [subst01']; cbv [Proper respectful] in *;
-            repeat first [ progress interp_safe_t
-                         | simplifier_t_step
-                         | break_innermost_match_step
-                         | interp_unsafe_t_step ].
-        Qed.
-
-        Lemma interp_subst01 live t (e1 e2 : expr t)
-              (Hwf : expr.wf nil e1 e2)
-          : expr.interp interp_ident (subst01 live e1) == expr.interp interp_ident e2.
-        Proof. apply interp_subst01'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed.
-
-        Lemma Interp_Subst01 {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e)
-          : expr.Interp interp_ident (Subst01 e) == expr.Interp interp_ident e.
-        Proof. apply interp_subst01, Hwf. Qed.
+        Lemma Interp_EliminateDead {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e)
+          : expr.Interp interp_ident (EliminateDead e) == expr.Interp interp_ident e.
+        Proof using interp_ident_Proper. apply Subst01.Interp_Subst0n, Hwf; auto using @OUGHT_TO_BE_UNUSED_id. Qed.
       End interp.
     End with_ident.
-  End Subst01.
+  End DeadCodeElimination.
 
-  Hint Resolve Subst01.Wf_Subst01 : wf.
-  Hint Rewrite @Subst01.Interp_Subst01 : interp.
+  Hint Resolve DeadCodeElimination.Wf_EliminateDead : wf.
+  Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index b1bf23019..8cf5687e6 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -688,10 +688,9 @@ Module Pipeline.
           first *)
        dlet_nd e := ToFlat E in
        let E := FromFlat e in
-       let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in
-       dlet_nd e := ToFlat E in
-       let E := FromFlat e in
-       let E := if with_subst01 then Subst01.Subst01 E else E in
+       let E := if with_subst01 then Subst01.Subst01 E
+                else if with_dead_code_elimination then DeadCodeElimination.EliminateDead E
+                     else E in
        let E := UnderLets.LetBindReturn E in
        let E := DoRewrite E in (* after inlining, see if any new rewrite redexes are available *)
        dlet_nd e := ToFlat E in