Merge pull request #84 from mit-plv/rsloan-phoas

Patching master with most of my Conversion refactors

10 files changed, 1036 insertions, 1515 deletions

diff --git a/src/Assembly/Bounded.v b/src/Assembly/Bounded.v
deleted file mode 100644
index aa4fd503b..000000000
--- a/src/Assembly/Bounded.v
+++ /dev/null
@@ -1,728 +0,0 @@
-Require Import Bedrock.Word Bedrock.Nomega.
-Require Import NPeano NArith PArith Ndigits ZArith Znat ZArith_dec Ndec.
-Require Import List Basics Bool Nsatz.
-
-Require Import Crypto.Assembly.QhasmUtil.
-Require Import Crypto.Assembly.WordizeUtil.
-Require Import Crypto.Assembly.Bounds.
-
-Import ListNotations.
-
-Section BoundedZ.
-
-  Section Trans4.
-    Definition min4 (a b c d: Z) :=
-      Z.min 0 (Z.min (Z.min a b) (Z.min c d)).
-
-    Definition max4 (a b c d: Z) :=
-      Z.max 0 (Z.max (Z.max a b) (Z.max c d)).
-
-    Ltac trans4min_tac := intros; unfold min4;
-      repeat match goal with
-      | [|- context[(Z.min ?x0 ?x1)%Z]] => is_var x1;
-        let A := fresh in let B := fresh in
-        destruct (Zmin_spec x0 x1)%Z as [A|A];
-        destruct A as [A B];
-        rewrite B; clear B
-      end; nomega.
-
-    Lemma trans4min_0: forall (x a b c d: Z),
-      (0 <= x)%Z -> (min4 a b c d <= x)%Z.
-    Proof. trans4min_tac. Qed.
-
-    Lemma trans4min_a: forall (x a b c d: Z),
-      (a <= x)%Z -> (min4 a b c d <= x)%Z.
-    Proof. trans4min_tac. Qed.
-
-    Lemma trans4min_b: forall (x a b c d: Z),
-      (b <= x)%Z -> (min4 a b c d <= x)%Z.
-    Proof. trans4min_tac. Qed.
-
-    Lemma trans4min_c: forall (x a b c d: Z),
-      (c <= x)%Z -> (min4 a b c d <= x)%Z.
-    Proof. trans4min_tac. Qed.
-
-    Lemma trans4min_d: forall (x a b c d: Z),
-      (d <= x)%Z -> (min4 a b c d <= x)%Z.
-    Proof. trans4min_tac. Qed.
-
-    Ltac trans4max_tac := intros; unfold max4;
-      repeat match goal with
-      | [|- context[(Z.max ?x0 ?x1)%Z]] => is_var x1;
-        let A := fresh in let B := fresh in
-        destruct (Zmax_spec x0 x1)%Z as [A|A];
-        destruct A as [A B];
-        rewrite B; clear B
-      end; try nomega.
-
-    Lemma trans4max_0: forall (x a b c d: Z),
-      (x <= 0)%Z -> (x <= max4 a b c d)%Z.
-    Proof. trans4max_tac. Qed.
-
-    Lemma trans4max_a: forall (x a b c d: Z),
-      (x <= a)%Z -> (x <= max4 a b c d)%Z.
-    Proof. trans4max_tac. Qed.
-
-    Lemma trans4max_b: forall (x a b c d: Z),
-      (x <= b)%Z -> (x <= max4 a b c d)%Z.
-    Proof. trans4max_tac. Qed.
-
-    Lemma trans4max_c: forall (x a b c d: Z),
-      (x <= c)%Z -> (x <= max4 a b c d)%Z.
-    Proof. trans4max_tac. Qed.
-
-    Lemma trans4max_d: forall (x a b c d: Z),
-      (x <= d)%Z -> (x <= max4 a b c d)%Z.
-    Proof. trans4max_tac. Qed.
-  End Trans4.
-
-  Section BoundedMul.
-    Lemma bZMul_min: forall (x0 low0 high0 x1 low1 high1: Z),
-      (low0 <= x0)%Z -> (x0 <= high0)%Z ->
-      (low1 <= x1)%Z -> (x1 <= high1)%Z ->
-      (min4 (low0 * low1) (low0 * high1)
-            (high0 * low1) (high0 * high1) <= x0 * x1)%Z.
-    Proof.
-      intros x0 low0 high0 x1 low1 high1
-        Hlow0 Hhigh0 Hlow1 Hhigh1.
-      destruct (Z_le_dec 0 x0), (Z_le_dec 0 x1).
-
-      - apply trans4min_0.
-        replace 0%Z with (0*0)%Z by nomega.
-        apply Z.mul_le_mono_nonneg; nomega.
-
-      - apply trans4min_c.
-        transitivity (x0 * low1)%Z.
-
-        + apply Z.mul_le_mono_nonpos_r; try nomega.
-        + apply Z.mul_le_mono_nonneg_l; try nomega.
-
-      - apply trans4min_b.
-        transitivity (x0 * high1)%Z.
-
-        + apply Z.mul_le_mono_nonneg_r; try nomega.
-        + apply Z.mul_le_mono_nonpos_l; try nomega.
-
-      - apply trans4min_0.
-        replace 0%Z with (0*0)%Z by nomega.
-        apply Z.mul_le_mono_nonpos; try nomega.
-    Qed.
-
-    Lemma bZMul_max: forall (x0 low0 high0 x1 low1 high1: Z),
-      (low0 <= x0)%Z -> (x0 <= high0)%Z ->
-      (low1 <= x1)%Z -> (x1 <= high1)%Z ->
-      (x0 * x1 <=
-      max4 (low0 * low1) (low0 * high1)
-           (high0 * low1) (high0 * high1))%Z.
-    Proof.
-      intros x0 low0 high0 x1 low1 high1
-        Hlow0 Hhigh0 Hlow1 Hhigh1.
-      destruct (Z_le_dec 0 x0), (Z_le_dec 0 x1).
-
-      - apply trans4max_d.
-        apply Z.mul_le_mono_nonneg; nomega.
-
-      - apply trans4max_0.
-        replace 0%Z with (0*0)%Z by nomega.
-        transitivity (x0 * 0)%Z.
-
-        + apply Z.mul_le_mono_nonneg_l; try nomega.
-        + apply Z.mul_le_mono_nonpos_r; try nomega.
-
-      - apply trans4max_0.
-        replace 0%Z with (0*0)%Z by nomega.
-        transitivity (x0 * 0)%Z.
-
-        + apply Z.mul_le_mono_nonpos_l; try nomega.
-        + apply Z.mul_le_mono_nonneg_r; try nomega.
-
-      - apply trans4max_a.
-        apply Z.mul_le_mono_nonpos; try nomega.
-    Qed.
-  End BoundedMul.
-
-  Inductive BoundedZ :=
-    | boundedZ: forall (x low high: Z),
-      (low <= x)%Z -> (x <= high)%Z -> BoundedZ.
-
-  Definition bprojZ (x: BoundedZ) :=
-    match x with
-    | boundedZ x0 low0 high0 plow0 phigh0 => x0
-    end.
-
-  Definition bZAdd (a b: BoundedZ): BoundedZ.
-    refine match a with
-    | boundedZ x0 low0 high0 plow0 phigh0 =>
-      match b with
-      | boundedZ x1 low1 high1 plow1 phigh1 =>
-        boundedZ (x0 + x1) (low0 + low1) (high0 + high1) _ _
-      end
-    end; abstract nomega.
-  Defined.
-
-  Definition bZSub (a b: BoundedZ): BoundedZ.
-    refine match a with
-    | boundedZ x0 low0 high0 plow0 phigh0 =>
-      match b with
-      | boundedZ x1 low1 high1 plow1 phigh1 =>
-        boundedZ (x0 - x1) (low0 - high1) (high0 - low1) _ _
-      end
-    end; abstract nomega.
-  Defined.
-
-  Definition bZMul (a b: BoundedZ): BoundedZ.
-    refine match a with
-    | boundedZ x0 low0 high0 plow0 phigh0 =>
-      match b with
-      | boundedZ x1 low1 high1 plow1 phigh1 =>
-        boundedZ (x0 * x1)
-          (min4 (low0 * low1) (low0 * high1)
-                (high0 * low1) (high0 * high1))
-          (max4 (low0 * low1) (low0 * high1)
-                (high0 * low1) (high0 * high1))
-          _ _
-      end
-    end; try apply bZMul_min; try apply bZMul_max; try assumption.
-  Defined.
-
-  Definition bZShiftr (a: BoundedZ) (k: nat): BoundedZ.
-    assert (forall k, 2 ^ (Z.of_nat k) > 0)%Z as H by abstract (
-      intro m;
-      rewrite <- two_p_equiv;
-      apply two_p_gt_ZERO;
-      induction m; try reflexivity;
-      rewrite Nat2Z.inj_succ;
-      nomega).
-
-    refine match a with
-    | boundedZ x low high plow phigh =>
-      boundedZ (Z.shiftr x (Z.of_nat k))
-               (Z.shiftr low (Z.of_nat k))
-               (Z.succ (Z.shiftr high (Z.of_nat k))) _ _
-    end.
-
-    - abstract (
-        repeat rewrite Z.shiftr_div_pow2;
-        try apply Nat2Z.is_nonneg;
-        apply Z_div_le; try assumption;
-        try apply H).
-
-    - abstract (
-        apply Z.lt_succ_r;
-        repeat rewrite Z.shiftr_div_pow2;
-        try apply Nat2Z.is_nonneg;
-        apply Z.lt_lt_succ_r;
-        apply Z.lt_succ_r;
-        apply Z_div_le;
-        try apply H;
-        try assumption).
-  Qed.
-
-  Definition bZMask (a: BoundedZ) (k: nat): BoundedZ.
-    assert (0 < 2 ^ Z.of_nat k)%Z as Hk by (
-      induction k;
-      try abstract (vm_compute; reflexivity);
-      rewrite Nat2Z.inj_succ;
-      rewrite <- two_p_equiv;
-      apply Z.gt_lt;
-      apply two_p_gt_ZERO;
-      apply Z.le_le_succ_r;
-      apply Nat2Z.is_nonneg).
-
-    refine match a with
-    | boundedZ x low high plow phigh =>
-      boundedZ (Z.land x (Z.ones (Z.of_nat k)))
-               (Z.of_N 0%N)
-               (Z.of_N (Npow2 k)) _ _
-    end.
-
-    - repeat rewrite Z.land_ones;
-        try apply Nat2Z.is_nonneg.
-
-      abstract (
-        apply (Z.mod_pos_bound x) in Hk; destruct Hk;
-        induction k; simpl in *; assumption).
-
-    - repeat rewrite Z.land_ones;
-        try apply Nat2Z.is_nonneg.
-
-      abstract (
-        rewrite Npow2_N;
-        rewrite N2Z.inj_pow; simpl;
-        apply (Z.mod_pos_bound x) in Hk; destruct Hk;
-        apply Z.lt_le_incl;
-        induction k; simpl in *; assumption).
-  Qed.
-End BoundedZ.
-
-Section BoundedN.
-
-  Inductive BoundedN :=
-    | boundedN: forall (x low high: N),
-      (low <= x)%N -> (x < high)%N -> BoundedN.
-
-  Definition bprojN (x: BoundedN) :=
-    match x with
-    | boundedN x0 low0 high0 plow0 phigh0 => x0
-    end.
-
-  Definition bNAdd (a b: BoundedN): BoundedN.
-    refine match a with
-    | boundedN x0 low0 high0 plow0 phigh0 =>
-      match b with
-      | boundedN x1 low1 high1 plow1 phigh1 =>
-        boundedN (x0 + x1) (low0 + low1) (high0 + high1) _ _
-      end
-    end.
-
-    - abstract (apply N.add_le_mono; assumption).
-    - abstract nomega.
-  Defined.
-
-  Definition bNSub (a b: BoundedN): BoundedN.
-    refine match a with
-    | boundedN x0 low0 high0 plow0 phigh0 =>
-      match b with
-      | boundedN x1 low1 high1 plow1 phigh1 =>
-        boundedN (x0 - x1) (low0 - high1) (N.succ (high0 - low1)) _ _
-      end
-    end.
-
-    - transitivity (x0 - high1)%N.
-
-      + apply N.sub_le_mono_r; assumption.
-      + apply N.sub_le_mono_l; apply N.lt_le_incl; assumption.
-
-    - apply N.lt_succ_r; transitivity (high0 - x1)%N.
-
-      + apply N.sub_le_mono_r; apply N.lt_le_incl; assumption.
-      + apply N.sub_le_mono_l; assumption.
-
-  Defined.
-
-  Definition bNMul (a b: BoundedN): BoundedN.
-    refine match a with
-    | boundedN x0 low0 high0 plow0 phigh0 =>
-      match b with
-      | boundedN x1 low1 high1 plow1 phigh1 =>
-        boundedN (x0 * x1)%N (low0 * low1)%N (high0 * high1)%N _ _
-      end
-    end; abstract (
-      try apply N.mul_le_mono_nonneg;
-      try apply N.mul_lt_mono_nonneg;
-        try assumption;
-        try apply N_ge_0).
-  Qed.
-
-  Definition bNShiftr (a: BoundedN) (k: nat): BoundedN.
-    assert (forall k, 2 ^ (N.of_nat k) > 0)%N as H by abstract (
-      intros;
-      rewrite <- Npow2_N;
-      apply N.lt_gt;
-      apply Npow2_gt0).
-
-    refine match a with
-    | boundedN x low high plow phigh =>
-      boundedN (N.shiftr x (N.of_nat k))
-               (N.shiftr low (N.of_nat k))
-               (N.succ (N.shiftr high (N.of_nat k))) _ _
-    end.
-
-    - repeat rewrite N.shiftr_div_pow2.
-      apply N.div_le_mono; try assumption.
-      pose proof (H k) as H0.
-      induction ((2 ^ N.of_nat k)%N);
-        [inversion H0; intuition |].
-      apply N.neq_0_lt_0; apply N.gt_lt; assumption.
-
-    - apply N.lt_succ_r.
-      repeat rewrite N.shiftr_div_pow2.
-      apply N.div_le_mono; [|apply N.lt_le_incl; assumption].
-      pose proof (H k) as H0.
-      induction ((2 ^ N.of_nat k)%N);
-        [inversion H0; intuition |].
-      apply N.neq_0_lt_0; apply N.gt_lt; assumption.
-  Defined.
-
-  Definition bNMask (a: BoundedN) (k: nat): BoundedN.
-    assert (forall k, 0 < 2 ^ (N.of_nat k))%N as H by abstract (
-      intros;
-      rewrite <- Npow2_N;
-      apply Npow2_gt0).
-
-    refine match a with
-    | boundedN x low high plow phigh =>
-      boundedN (N.land x (N.ones (N.of_nat k)))
-               0%N
-               (Npow2 k) _ _
-    end.
-
-    - repeat rewrite N.land_ones;
-        apply N_ge_0.
-
-    - repeat rewrite N.land_ones.
-
-      abstract (
-        rewrite Npow2_N;
-        pose proof (N.mod_bound_pos x (2 ^ N.of_nat k)%N (N_ge_0 _) (H k))
-          as H0; destruct H0;
-        assumption).
-  Defined.
-
-End BoundedN.
-
-Section BoundedWord.
-  Context {n: nat}.
-
-  Section BoundedSub.
-    Lemma NToWord_Npow2: wzero n = NToWord n (Npow2 n).
-    Proof.
-      induction n as [|n0].
-
-      + repeat rewrite shatter_word_0; reflexivity.
-
-      + unfold wzero in *; simpl in *.
-        rewrite IHn0; simpl.
-        induction (Npow2 n0); simpl; reflexivity.
-    Qed.
-
-    Lemma bWSub_lem0: forall (x0 x1: word n) (low0 high1: N),
-      (low0 <= wordToN x0)%N -> (wordToN x1 < high1)%N ->
-      (low0 - high1 <= & (x0 ^- x1))%N.
-    Proof.
-      intros.
-
-      destruct (Nge_dec (wordToN x1) 1)%N as [e|e].
-      destruct (Nge_dec (wordToN x1) (wordToN x0)).
-
-      - unfold wminus, wneg.
-        assert (low0 < high1)%N. {
-          apply (N.le_lt_trans _ (wordToN x0) _); [assumption|].
-          apply (N.le_lt_trans _ (wordToN x1) _); [apply N.ge_le|]; assumption.
-        }
-
-        replace (low0 - high1)%N with 0%N; [apply N_ge_0|].
-        symmetry.
-        apply N.sub_0_le.
-        apply N.lt_le_incl.
-        assumption.
-
-        - transitivity (wordToN x0 - wordToN x1)%N.
-
-          + transitivity (wordToN x0 - high1)%N.
-
-            * apply N.sub_le_mono_r; assumption.
-
-            * apply N.sub_le_mono_l; apply N.lt_le_incl; assumption.
-
-          + assert (& x0 - & x1 < Npow2 n)%N. {
-              transitivity (wordToN x0);
-                try apply word_size_bound;
-                apply N.sub_lt.
-
-              + apply N.lt_le_incl; assumption.
-
-              + nomega.
-            }
-
-            assert (& x0 - & x1 + & x1 < Npow2 n)%N. {
-              replace (wordToN x0 - wordToN x1 + wordToN x1)%N
-                with (wordToN x0) by nomega.
-              apply word_size_bound.
-            }
-
-            assert (x0 = NToWord n (wordToN x0 - wordToN x1) ^+ x1) as Hv. {
-              apply NToWord_equal.
-              rewrite <- wordize_plus; rewrite wordToN_NToWord;
-                try assumption.
-              nomega.
-            }
-
-            apply N.eq_le_incl.
-            rewrite Hv.
-            unfold wminus.
-            rewrite <- wplus_assoc.
-            rewrite wminus_inv.
-            rewrite (wplus_comm (NToWord n (wordToN x0 - wordToN x1)) (wzero n)).
-            rewrite wplus_unit.
-            rewrite <- wordize_plus; [nomega|].
-            rewrite wordToN_NToWord; assumption.
-
-      - unfold wminus, wneg.
-        assert (wordToN x1 = 0)%N as e' by nomega.
-        rewrite e'.
-        replace (Npow2 n - 0)%N with (Npow2 n) by nomega.
-        rewrite <- NToWord_Npow2.
-
-        erewrite <- wordize_plus;
-          try rewrite wordToN_zero;
-          replace (wordToN x0 + 0)%N with (wordToN x0)%N by nomega;
-          try apply word_size_bound.
-
-        transitivity low0; try assumption.
-        apply N.le_sub_le_add_r.
-        apply N.le_add_r.
-    Qed.
-
-    Lemma bWSub_lem1: forall (x0 x1: word n) (low1 high0: N),
-      (low1 <= wordToN x1)%N -> (wordToN x0 < high0)%N ->
-      (& (x0 ^- x1) < N.succ (high0 + Npow2 n - low1))%N.
-    Proof.
-      intros; unfold wminus.
-      destruct (Nge_dec (wordToN x1) 1)%N as [e|e].
-      destruct (Nge_dec (wordToN x0) (wordToN x1)).
-
-      - apply N.lt_succ_r.
-        assert (& x0 - & x1 < Npow2 n)%N. {
-          transitivity (wordToN x0);
-          try apply word_size_bound;
-          apply N.sub_lt.
-
-          + apply N.ge_le; assumption.
-
-          + nomega.
-        }
-
-        assert (& x0 - & x1 + & x1 < Npow2 n)%N. {
-          replace (wordToN x0 - wordToN x1 + wordToN x1)%N
-            with (wordToN x0) by nomega.
-          apply word_size_bound.
-        }
-
-        assert (x0 = NToWord n (wordToN x0 - wordToN x1) ^+ x1) as Hv. {
-          apply NToWord_equal.
-          rewrite <- wordize_plus; rewrite wordToN_NToWord;
-          try assumption.
-          nomega.
-        }
-
-        rewrite Hv.
-        rewrite <- wplus_assoc.
-        rewrite wminus_inv.
-        rewrite wplus_comm.
-        rewrite wplus_unit.
-        rewrite wordToN_NToWord.
-
-        + transitivity (wordToN x0 - low1)%N.
-
-          * apply N.sub_le_mono_l; assumption.
-
-          * apply N.sub_le_mono_r.
-            transitivity high0; [apply N.lt_le_incl; assumption|].
-            replace' high0 with (high0 + 0)%N at 1 by nomega.
-            apply N.add_le_mono_l.
-            apply N_ge_0.
-
-        + transitivity (wordToN x0); try apply word_size_bound.
-            nomega.
-
-      - rewrite <- wordize_plus; [apply N.lt_succ_r|].
-
-        + transitivity (high0 + (wordToN (wneg x1)))%N.
-
-          * apply N.add_le_mono_r; apply N.lt_le_incl; assumption.
-
-          * unfold wneg.
-            rewrite wordToN_NToWord; [|abstract (
-              apply N.sub_lt;
-              try apply N.lt_le_incl;
-              try apply word_size_bound;
-              nomega )].
-
-            rewrite N.add_sub_assoc; [|abstract (
-              try apply N.lt_le_incl;
-              try apply word_size_bound)].
-
-            apply N.sub_le_mono_l.
-            assumption.
-
-        + unfold wneg.
-
-          rewrite wordToN_NToWord; [|abstract (
-            apply N.sub_lt;
-            try apply N.lt_le_incl;
-            try apply word_size_bound;
-            nomega )].
-
-          replace (wordToN x0 + (Npow2 n - wordToN x1))%N
-            with (Npow2 n - (wordToN x1 - wordToN x0))%N.
-
-          * apply N.sub_lt; try nomega.
-            transitivity (wordToN x1); [apply N.le_sub_l|].
-            apply N.lt_le_incl.
-            apply word_size_bound.
-
-          * apply N.add_sub_eq_l.
-            rewrite <- N.add_sub_swap;
-                [|apply N.lt_le_incl; assumption].
-            rewrite (N.add_comm (wordToN x0)).
-            rewrite N.add_assoc.
-            rewrite N.add_sub_assoc;
-                [|apply N.lt_le_incl; apply word_size_bound].
-            rewrite N.add_sub.
-            rewrite N.add_comm.
-            rewrite N.add_sub.
-            reflexivity.
-
-      - apply N.lt_succ_r.
-        assert (wordToN x1 = 0)%N as e' by nomega.
-        assert (NToWord n (wordToN x1) = NToWord n 0%N) as E by
-            (rewrite e'; reflexivity).
-        rewrite NToWord_wordToN in E.
-        simpl in E; rewrite wzero'_def in E.
-        rewrite E.
-        unfold wneg.
-        rewrite wordToN_zero.
-        rewrite N.sub_0_r.
-        rewrite <- NToWord_Npow2.
-        rewrite wplus_comm.
-        rewrite wplus_unit.
-        transitivity high0.
-
-        + apply N.lt_le_incl.
-          assumption.
-
-        + rewrite <- N.add_sub_assoc.
-
-          * replace high0 with (high0 + 0)%N by nomega.
-            apply N.add_le_mono; [|apply N_ge_0].
-            apply N.eq_le_incl.
-            rewrite N.add_0_r.
-            reflexivity.
-
-          * transitivity (wordToN x1);
-            [ assumption
-            | apply N.lt_le_incl;
-                apply word_size_bound].
-
-    Qed.
-  End BoundedSub.
-
-  Inductive BoundedWord :=
-    | boundedWord: forall (x: word n) (low high: N) (overflowed: bool),
-      (low <= wordToN x)%N -> (wordToN x < high)%N -> BoundedWord.
-
-  Definition bprojW (x: BoundedWord) :=
-    match x with
-    | boundedWord x0 _ _ _ _ _ => x0
-    end.
-
-  Definition bWAdd (a b: BoundedWord): BoundedWord.
-    refine match a with
-    | boundedWord x0 low0 high0 o0 plow0 phigh0 =>
-      match b with
-      | boundedWord x1 low1 high1 o1 plow1 phigh1 =>
-        if (overflows n (high0 + high1))
-        then boundedWord (x0 ^+ x1) 0%N (high0 + high1) (orb o0 o1) _ _
-        else boundedWord (x0 ^+ x1) (low0 + low1) (high0 + high1) true _ _
-      end
-    end; try abstract (
-      apply (N.le_lt_trans _ (wordToN x0 + wordToN x1)%N _);
-        try apply plus_le;
-        abstract nomega).
-
-    - apply N_ge_0.
-
-    - erewrite <- wordize_plus';
-        try eassumption;
-        try abstract nomega.
-
-      + apply N.add_le_mono; assumption.
-
-      + abstract (apply N.lt_le_incl; nomega).
-  Qed.
-
-  Definition bWSub (a b: BoundedWord): BoundedWord.
-    refine match a with
-    | boundedWord x0 low0 high0 o0 plow0 phigh0 =>
-      match b with
-      | boundedWord x1 low1 high1 o1 plow1 phigh1 =>
-        let upper_bound :=
-          if (Nge_dec high0 (Npow2 n))
-          then Npow2 n
-          else if (Nge_dec high1 (Npow2 n))
-               then Npow2 n
-               else (N.succ (high0 + Npow2 n - low1)) in
-
-        if (Nge_dec low0 high1)
-        then boundedWord (x0 ^- x1) (low0 - high1)%N upper_bound (orb o0 o1) _ _
-        else boundedWord (x0 ^- x1) 0%N upper_bound (orb o0 o1) _ _
-      end
-    end; abstract (unfold upper_bound; try apply N_ge_0;
-      destruct (Nge_dec high0 (Npow2 n)), (Nge_dec high1 (Npow2 n));
-      repeat match goal with
-      | [|- (_ - ?x <= wordToN _)%N] => apply bWSub_lem0
-      | [|- (wordToN _ < N.succ (?x + _ - _))%N] => apply bWSub_lem1
-      | [|- (wordToN _ < Npow2 _)%N] => apply word_size_bound
-      | [|- (0 <= _)%N] => apply N_ge_0
-      end; assumption).
-  Qed.
-
-  Definition bWMul (a b: BoundedWord): BoundedWord.
-    refine match a with
-    | boundedWord x0 low0 high0 o0 plow0 phigh0 =>
-      match b with
-      | boundedWord x1 low1 high1 o1 plow1 phigh1 =>
-        if (overflows n (high0 * high1))
-        then boundedWord (x0 ^* x1)%N 0%N (high0 * high1)%N true _ _
-        else boundedWord (x0 ^* x1)%N (low0 * low1)%N (high0 * high1)%N (orb o0 o1) _ _
-      end
-    end.
-
-    - apply N_ge_0.
-
-    - apply (N.le_lt_trans _ (wordToN x0 * wordToN x1)%N _); [apply mult_le|].
-      apply N.mul_lt_mono; assumption.
-
-    - rewrite <- wordize_mult.
-
-      + apply N.mul_le_mono; assumption.
-
-      + transitivity (high0 * high1)%N; [|assumption].
-        apply N.mul_lt_mono; assumption.
-
-    - apply (N.le_lt_trans _ (wordToN x0 * wordToN x1)%N _); [apply mult_le|].
-      apply N.mul_lt_mono; assumption.
-  Qed.
-
-  Definition bWShiftr (a: BoundedWord) (k: nat): BoundedWord.
-    assert (forall k, 2 ^ (N.of_nat k) > 0)%N as H by abstract (
-      intros;
-      rewrite <- Npow2_N;
-      apply N.lt_gt;
-      apply Npow2_gt0).
-
-    refine match a with
-    | boundedWord x low high o plow phigh =>
-      boundedWord (extend (le_n _) (shiftr x k))
-        (N.shiftr low (N.of_nat k))
-        (N.succ (N.shiftr high (N.of_nat k))) o _ _
-           end.
-
-    - unfold extend; rewrite wordToN_convS.
-
-      rewrite wordToN_zext.
-      rewrite <- wordize_shiftr.
-      rewrite <- Nshiftr_equiv_nat.
-      repeat rewrite N.shiftr_div_pow2.
-      apply N.div_le_mono; try assumption.
-      pose proof (H k) as H0.
-      induction ((2 ^ N.of_nat k)%N);
-        [inversion H0; intuition |].
-      apply N.neq_0_lt_0; apply N.gt_lt; assumption.
-
-    - unfold extend; rewrite wordToN_convS.
-      rewrite wordToN_zext.
-      rewrite Nshiftr_equiv_nat.
-      eapply N.lt_le_trans; [apply shiftr_bound; eassumption|].
-      try apply N.eq_le_incl.
-      try eassumption; reflexivity.
-  Qed.
-
-  Definition bWMask (a: BoundedWord) (k: nat): BoundedWord.
-    refine match a with
-    | boundedWord x low high o plow phigh =>
-      boundedWord (mask k x) 0%N (Npow2 k) o _ _
-    end; [apply N_ge_0 | apply mask_bound].
-  Qed.
-End BoundedWord.
diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v
index 0aff52bcf..666cc65cc 100644
--- a/src/Assembly/Compile.v
+++ b/src/Assembly/Compile.v
@@ -12,31 +12,44 @@ Require Import Crypto.Assembly.Qhasm.
 Local Arguments LetIn.Let_In _ _ _ _ / .
 
 Module CompileHL.
-  Context {ivar : type -> Type}.
-  Context {ovar : Type}.
-
-  Fixpoint compile {t} (e:@HL.expr Z (@LL.arg Z Z) t) : @LL.expr Z Z t :=
-    match e with
-    | HL.Const n => LL.Return (LL.Const n)
-    | HL.Var _ arg => LL.Return arg
-    | HL.Binop t1 t2 t3 op e1 e2 =>
-       LL.under_lets (@compile _ e1) (fun arg1 =>
-          LL.under_lets (@compile _ e2) (fun arg2 =>
-            LL.LetBinop op arg1 arg2 (fun v =>
-              LL.Return v)))
-    | HL.Let _ ex _ eC =>
-       LL.under_lets (@compile _ ex) (fun arg => @compile _ (eC arg))
-    | HL.Pair t1 e1 t2 e2 =>
-       LL.under_lets (@compile _ e1) (fun arg1 =>
-          LL.under_lets (@compile _ e2) (fun arg2 =>
-             LL.Return (LL.Pair arg1 arg2)))
-    | HL.MatchPair _ _ ep _ eC =>
-        LL.under_lets (@compile _ ep) (fun arg =>
-          let (a1, a2) := LL.match_arg_Prod arg in @compile _ (eC a1 a2))
-    end.
+  Section Compilation.
+    Context {T: Type}.
+
+    Fixpoint compile {T t} (e:@HL.expr T (@LL.arg T T) t) : @LL.expr T T t :=
+        match e with
+        | HL.Const _ n => LL.Return (LL.Const n)
+
+        | HL.Var _ arg => LL.Return arg
+
+        | HL.Binop t1 t2 t3 op e1 e2 =>
+          LL.under_lets (compile e1) (fun arg1 =>
+            LL.under_lets (compile e2) (fun arg2 =>
+              LL.LetBinop op arg1 arg2 (fun v =>
+                LL.Return v)))
+
+        | HL.Let _ ex _ eC =>
+          LL.under_lets (compile ex) (fun arg =>
+            compile (eC arg))
+
+        | HL.Pair t1 e1 t2 e2 =>
+          LL.under_lets (compile e1) (fun arg1 =>
+            LL.under_lets (compile e2) (fun arg2 =>
+              LL.Return (LL.Pair arg1 arg2)))
+
+        | HL.MatchPair _ _ ep _ eC =>
+            LL.under_lets (compile ep) (fun arg =>
+              let (a1, a2) := LL.match_arg_Prod arg in
+              compile (eC a1 a2))
+        end.
+
+    Definition Compile {T t} (e:@HL.Expr T t) : @LL.expr T T t :=
+      compile (e (@LL.arg T T)).
+  End Compilation.
 
   Section Correctness.
-    Lemma compile_correct {_: Evaluable Z} {t} e1 e2 G (wf:HL.wf G e1 e2) :
+    Context {T: Type}.
+
+    Lemma compile_correct {_: Evaluable T} {t} e1 e2 G (wf:HL.wf G e1 e2) :
       List.Forall (fun v => let 'existT _ (x, a) := v in LL.interp_arg a = x) G ->
         LL.interp (compile e2) = HL.interp e1 :> interp_type t.
     Proof.
@@ -196,7 +209,7 @@ Module CompileLL.
       | Prod t0 t1 => fun a' =>
         match a' with
         | Pair _ _ a0 a1 => (vars a0) ++ (vars a1)
-        | _ => I (* dummy value *)
+        | _ => I (* dummy *)
         end
       end a.
 
@@ -242,7 +255,7 @@ Module CompileLL.
                 omap (getOutputSlot nextRegName op' x' y') (fun r =>
                   let var :=
                     match t3 as t3' return WArg t3' with
-                    | TT => Var (natToWord n r)
+                    | TT => Var (natToWord _ r)
                     | _ => zeros _
                     end in
 
@@ -269,14 +282,14 @@ Module CompileLL.
         (fun rt var op x y out => Some out)
         (fun t' a => Some (vars a)).
 
-    Fixpoint fillInputs t inputs (prog: NAry inputs (WArg TT) (WExpr t)) {struct inputs}: WExpr t :=
-      match inputs as inputs' return NAry inputs' (WArg TT) (WExpr t) -> NAry O (WArg TT) (WExpr t) with
+    Fixpoint fillInputs t inputs (prog: NAry inputs Z (WExpr t)) {struct inputs}: WExpr t :=
+      match inputs as inputs' return NAry inputs' Z (WExpr t) -> NAry O Z (WExpr t) with
       | O => fun p => p
-      | S inputs'' => fun p => @fillInputs _ _ (p (Var (natToWord _ inputs)))
+      | S inputs'' => fun p => @fillInputs _ _ (p (Z.of_nat inputs))
       end prog.
     Global Arguments fillInputs {t inputs} _.
 
-    Definition compile {t inputs} (p: NAry inputs (WArg TT) (WExpr t)): option (Program * list nat) :=
+    Definition compile {t inputs} (p: NAry inputs Z (WExpr t)): option (Program * list nat) :=
       let p' := fillInputs p in
 
       omap (getOuts _ (S inputs) p') (fun outs =>
diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v
index fa024c728..c7801c63a 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -17,6 +17,7 @@ Require Import Coq.ZArith.Znat.
 Require Import Coq.NArith.Nnat Coq.NArith.Ndigits.
 
 Require Import Coq.Bool.Sumbool.
+Require Import Coq.Program.Basics.
 
 Local Arguments LetIn.Let_In _ _ _ _ / .
 
@@ -30,29 +31,9 @@ Defined.
 Module HLConversions.
   Import HL.
 
-  Fixpoint mapVar {A: Type} {t V0 V1} (f: forall t, V0 t -> V1 t) (g: forall t, V1 t -> V0 t) (a: expr (T := A) (var := V0) t): expr (T := A) (var := V1) t :=
+  Fixpoint convertExpr {A B: Type} {EB: Evaluable B} {t v} (a: expr (T := A) (var := v) t): expr (T := B) (var := v) t :=
     match a with
-    | Const x => Const x
-    | Var t x => Var (f _ x)
-    | Binop t1 t2 t3 o e1 e2 => Binop o (mapVar f g e1) (mapVar f g e2)
-    | Let tx e tC h => Let (mapVar f g e) (fun x => mapVar f g (h (g _ x)))
-    | Pair t1 e1 t2 e2 => Pair (mapVar f g e1) (mapVar f g e2)
-    | MatchPair t1 t2 e tC h => MatchPair (mapVar f g e) (fun x y => mapVar f g (h (g _ x) (g _ y)))
-    end.
-
-  Definition convertVar {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: interp_type (T := A) t): interp_type (T := B) t.
-  Proof.
-    induction t as [| t3 IHt1 t4 IHt2].
-
-    - refine (@toT B EB (@fromT A EA _)); assumption.
-
-    - destruct a as [a1 a2]; constructor;
-        [exact (IHt1 a1) | exact (IHt2 a2)].
-  Defined.
-
-  Fixpoint convertExpr {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t v} (a: expr (T := A) (var := v) t): expr (T := B) (var := v) t :=
-    match a with
-    | Const x => Const (@toT B EB (@fromT A EA x))
+    | Const E x => Const (@toT B EB (@fromT A E x))
     | Var t x => @Var B _ t x
     | Binop t1 t2 t3 o e1 e2 =>
       @Binop B _ t1 t2 t3 o (convertExpr e1) (convertExpr e2)
@@ -62,354 +43,134 @@ Module HLConversions.
     | MatchPair t1 t2 e tC f => MatchPair (convertExpr e) (fun x y =>
         convertExpr (f x y))
     end.
-
-  Fixpoint convertExpr' {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: expr (T := A) (var := @interp_type A) t): expr (T := B) (var := @interp_type B) t :=
-    match a with
-    | Const x => Const (@toT B EB (@fromT A EA x))
-    | Var t x => @Var B _ t (convertVar x)
-    | Binop t1 t2 t3 o e1 e2 =>
-      @Binop B _ t1 t2 t3 o (convertExpr' e1) (convertExpr' e2)
-    | Let tx e tC f =>
-      Let (convertExpr' e) (fun x => convertExpr' (f (convertVar x)))
-    | Pair t1 e1 t2 e2 => Pair (convertExpr' e1) (convertExpr' e2)
-    | MatchPair t1 t2 e tC f => MatchPair (convertExpr' e) (fun x y =>
-        convertExpr' (f (convertVar x) (convertVar y)))
-    end.
-
-  Definition convertZToWord {t} n v a :=
-    @convertExpr Z (word n) ZEvaluable (@WordEvaluable n) t v a.
-
-  Definition convertZToBounded {t} n v a :=
-    @convertExpr Z (option (@BoundedWord n))
-                 ZEvaluable (@BoundedEvaluable n) t v a.
-
-  Definition ZToWord {t} n (a: @Expr Z t): @Expr (word n) t :=
-    fun v => convertZToWord n v (a v).
-
-  Definition ZToRange {t} n (a: @Expr Z t): @Expr (option (@BoundedWord n)) t :=
-    fun v => convertZToBounded n v (a v).
-
-  Definition BInterp {n t} E: @interp_type (option (@BoundedWord n)) t :=
-    @Interp (option (@BoundedWord n)) (@BoundedEvaluable n) t E.
-
-  Example example_Expr : Expr TT := fun var => (
-    Let (Const 7) (fun a =>
-      Let (Let (Binop OPadd (Var a) (Var a)) (fun b => Pair (Var b) (Var b))) (fun p =>
-        MatchPair (Var p) (fun x y =>
-          Binop OPadd (Var x) (Var y)))))%Z.
-
-  Example interp_example_range :
-    option_map high (BInterp (ZToRange 32 example_Expr)) = Some 28%N.
-  Proof. cbv; reflexivity. Qed.
 End HLConversions.
 
 Module LLConversions.
   Import LL.
 
-  Definition convertVar {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: interp_type (T := A) t): interp_type (T := B) t.
-  Proof.
-    induction t as [| t3 IHt1 t4 IHt2].
-
-    - refine (@toT B EB (@fromT A EA _)); assumption.
-
-    - destruct a as [a1 a2]; constructor;
-        [exact (IHt1 a1) | exact (IHt2 a2)].
-  Defined.
-
-  Fixpoint convertArg {A B: Type} {EA: Evaluable A} {EB: Evaluable B} t {struct t}: @arg A A t -> @arg B B t :=
-    match t as t' return @arg A A t' -> @arg B B t' with
-    | TT => fun x =>
-      match x with
-      | Const c => Const (convertVar (t := TT) c)
-      | Var v => Var (convertVar (t := TT) v)
-      end
-    | Prod t0 t1 => fun x =>
-      match (match_arg_Prod x) with
-      | (a, b) => Pair ((convertArg t0) a) ((convertArg t1) b)
-      end
-    end.
-
-  Arguments convertArg [_ _ _ _ _ _].
+  Section VarConv.
+    Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}.
 
-  Fixpoint convertExpr {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: expr (T := A) t): expr (T := B) t :=
-    match a with
-    | LetBinop _ _ out op a b _ eC =>
-      LetBinop (T := B) op (convertArg a) (convertArg b) (fun x: (arg out) => convertExpr (eC (convertArg x)))
-    | Return _ a => Return (convertArg a)
-    end.
-
-  Definition convertZToWord {t} n a :=
-    @convertExpr Z (word n) ZEvaluable (@WordEvaluable n) t a.
-
-  Definition convertZToBounded {t} n a :=
-    @convertExpr Z (option (@BoundedWord n)) ZEvaluable (@BoundedEvaluable n) t a.
-
-  Definition zinterp {t} E := @interp Z ZEvaluable t E.
-
-  Definition wordInterp {n t} E := @interp (word n) (@WordEvaluable n) t E.
-
-  Definition boundedInterp {n t} E: @interp_type (option (@BoundedWord n)) t :=
-    @interp (option (@BoundedWord n)) (@BoundedEvaluable n) t E.
-
-  Section Correctness.
-    (* Aliases to make the proofs easier to read. *)
-
-    Definition varZToBounded {n t} (v: @interp_type Z t): @interp_type (option (@BoundedWord n)) t :=
-      @convertVar Z (option (@BoundedWord n)) ZEvaluable BoundedEvaluable t v.
-
-    Definition varBoundedToZ {n t} (v: @interp_type _ t): @interp_type Z t :=
-      @convertVar (option (@BoundedWord n)) Z BoundedEvaluable ZEvaluable t v.
-
-    Definition varZToWord {n t} (v: @interp_type Z t): @interp_type (@word n) t :=
-      @convertVar Z (@word n) ZEvaluable (@WordEvaluable n) t v.
-
-    Definition varWordToZ {n t} (v: @interp_type (@word n) t): @interp_type Z t :=
-      @convertVar (word n) Z (@WordEvaluable n) ZEvaluable t v.
-
-    Definition zOp {tx ty tz: type} (op: binop tx ty tz)
-               (x: @interp_type Z tx) (y: @interp_type Z ty): @interp_type Z tz :=
-      @interp_binop Z ZEvaluable _ _ _ op x y.
-
-    Definition wOp {n} {tx ty tz: type} (op: binop tx ty tz)
-               (x: @interp_type _ tx) (y: @interp_type _ ty): @interp_type _ tz :=
-      @interp_binop (word n) (@WordEvaluable n) _ _ _ op x y.
-
-    Definition bOp {n} {tx ty tz: type} (op: binop tx ty tz)
-               (x: @interp_type _ tx) (y: @interp_type _ ty): @interp_type _ tz :=
-      @interp_binop (option (@BoundedWord n)) BoundedEvaluable _ _ _ op x y.
-
-    Definition boundedArg {n t} (x: @arg (option (@BoundedWord n)) (option (@BoundedWord n)) t) :=
-      @interp_arg _ _ x.
+    Definition convertVar {t} (a: interp_type (T := A) t): interp_type (T := B) t.
+    Proof.
+      induction t as [| t3 IHt1 t4 IHt2].
 
-    Definition wordArg {n t} (x: @arg (word n) (word n) t) := @interp_arg _ _ x.
+      - refine (@toT B EB (@fromT A EA _)); assumption.
 
-    (* BoundedWord-based Bounds-checking fixpoint *)
+      - destruct a as [a1 a2]; constructor;
+          [exact (IHt1 a1) | exact (IHt2 a2)].
+    Defined.
+  End VarConv.
 
-    Definition getBounds {n t} T (E: Evaluable T) (e : @expr T T t): @interp_type (option (@BoundedWord n)) t :=
-      interp (E := BoundedEvaluable) (@convertExpr T (option (@BoundedWord n)) E BoundedEvaluable t e).
+  Section ArgConv.
+    Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}.
 
-    Fixpoint bcheck' {n t} (x: @interp_type (option (@BoundedWord n)) t) :=
-      match t as t' return (interp_type t') -> bool with
-      | TT => fun x' =>
-        match x' with
-        | Some _ => true
-        | None => false
+    Fixpoint convertArg {V} t {struct t}: @arg A V t -> @arg B V t :=
+      match t as t' return @arg A V t' -> @arg B V t' with
+      | TT => fun x =>
+        match x with
+        | Const c => Const (convertVar (t := TT) c)
+        | Var v => Var v
         end
-      | Prod t0 t1 => fun x' =>
-        match x' with
-        | (x0, x1) => andb (bcheck' x0) (bcheck' x1)
+      | Prod t0 t1 => fun x =>
+        match (match_arg_Prod x) with
+        | (a, b) => Pair ((convertArg t0) a) ((convertArg t1) b)
         end
-      end x.
-
-    Definition bcheck {n t} T (E: Evaluable T) (e : @expr T T t): bool := bcheck' (n := n) (getBounds T E e).
-
-    (* Utility Lemmas *)
-
-    Lemma convertArg_interp: forall {A B t} {EA: Evaluable A} {EB: Evaluable B} (x: @arg A A t),
-        (interp_arg (@convertArg A B EA EB t x)) = @convertVar A B EA EB t (interp_arg x).
-    Proof.
-      induction x as [| |t0 t1 i0 i1]; [reflexivity|reflexivity|].
-      induction EA, EB; simpl; f_equal; assumption.
-    Qed.
-
-    Lemma convertArg_var: forall {A B EA EB t} (x: @interp_type A t),
-        @convertArg A B EA EB t (uninterp_arg x) = uninterp_arg (@convertVar A B EA EB t x).
-    Proof.
-      induction t as [|t0 IHt_0 t1 IHt_1]; simpl; intros; [reflexivity|].
-      induction x as [a b]; simpl; f_equal;
-        induction t0 as [|t0a IHt0_0 t0b IHt0_1],
-                  t1 as [|t1a IHt1_0]; simpl in *;
-        try rewrite IHt_0;
-        try rewrite IHt_1;
-        reflexivity.
-    Qed.
-
-    Ltac kill_just n :=
-      match goal with
-      | [|- context[just ?x] ] =>
-        let Hvalue := fresh in let Hvalue' := fresh in
-        let Hlow := fresh in let Hlow' := fresh in
-        let Hhigh := fresh in let Hhigh' := fresh in
-        let Hnone := fresh in let Hnone' := fresh in
-
-        let B := fresh in
-
-        pose proof (just_value_spec (n := n) x) as Hvalue;
-        pose proof (just_low_spec (n := n) x) as Hlow;
-        pose proof (just_high_spec (n := n) x) as Hhigh;
-        pose proof (just_None_spec (n := n) x) as Hnone;
-
-        destruct (just x);
-
-        try pose proof (Hlow _ eq_refl) as Hlow';
-        try pose proof (Hvalue _ eq_refl) as Hvalue';
-        try pose proof (Hhigh _ eq_refl) as Hhigh';
-        try pose proof (Hnone eq_refl) as Hnone';
-
-        clear Hlow Hhigh Hvalue Hnone
-      end.
-
-    Ltac kill_dec :=
-      repeat match goal with
-      | [|- context[Nge_dec ?a ?b] ] => destruct (Nge_dec a b)
-      | [H : context[Nge_dec ?a ?b] |- _ ] => destruct (Nge_dec a b)
       end.
+  End ArgConv.
 
-    Lemma ZToBounded_binop_correct : forall {n tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e,
-        bcheck (n := n) (t := tz) Z ZEvaluable (LetBinop op x y e) = true
-      -> zOp op (interp_arg x) (interp_arg y) =
-          varBoundedToZ (bOp (n := n) op (varZToBounded (interp_arg x)) (varZToBounded (interp_arg y))).
-    Proof.
-    Admitted.
-
-    Lemma ZToWord_binop_correct : forall {n tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e,
-        bcheck (n := n) (t := tz) Z ZEvaluable (LetBinop op x y e) = true
-      -> zOp op (interp_arg x) (interp_arg y) =
-          varWordToZ (wOp (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))).
-    Proof.
-    Admitted.
-
-    Lemma just_zero: forall n, exists x, just (n := n) 0 = Some x.
-    Proof.
-    Admitted.
+  Section ExprConv.
+    Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}.
 
-    (* Main correctness guarantee *)
+    Fixpoint convertExpr {t V} (a: @expr A V t): @expr B V t :=
+        match a with
+        | LetBinop _ _ out op a b _ eC =>
+          LetBinop (T := B) op (convertArg _ a) (convertArg _ b) (fun x: (arg out) =>
+            convertExpr (eC (convertArg _ x)))
 
-    Lemma RangeInterp_bounded_spec: forall {n t} (E: expr t),
-        bcheck (n := n) Z ZEvaluable E = true
-      -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (convertZToWord n E).
-    Proof.
-      intros n t E S.
-      unfold convertZToBounded, zinterp, convertZToWord, wordInterp.
+        | Return _ a => Return (convertArg _ a)
+        end.
+  End ExprConv.
 
-      induction E as [tx ty tz op x y z|]; simpl; try reflexivity.
+  Section Defaults.
+    Context {t: type} {n: nat}.
 
-      - repeat rewrite convertArg_var in *.
-        repeat rewrite convertArg_interp in *.
+    Definition Word := word n.
+    Definition Bounded := option (@BoundedWord n).
+    Definition RWV := option (RangeWithValue).
 
-        rewrite H; clear H; repeat f_equal.
+    Transparent Word Bounded RWV.
 
-        + pose proof (ZToWord_binop_correct (n := n) op x y) as C;
-            unfold zOp, wOp, varWordToZ, varZToWord in C;
-            simpl in C.
+    Instance RWVEvaluable' : Evaluable RWV := @RWVEvaluable n.
+    Instance ZEvaluable' : Evaluable Z := ZEvaluable.
 
-          induction op; apply (C (fun _ => Return (Const 0%Z))); clear C;
-            unfold bcheck, getBounds; simpl;
-            destruct (@just_zero n) as [j p]; rewrite p; reflexivity.
+    Existing Instance ZEvaluable'.
+    Existing Instance WordEvaluable.
+    Existing Instance BoundedEvaluable.
+    Existing Instance RWVEvaluable'.
 
-        + unfold bcheck, getBounds in *; simpl in *.
-          replace (interp_binop op (interp_arg x) (interp_arg y))
-             with (varBoundedToZ (n := n) (bOp (n := n) op
-                    (boundedArg (@convertArg _ _ ZEvaluable (@BoundedEvaluable n) _ x))
-                    (boundedArg (@convertArg _ _ ZEvaluable (@BoundedEvaluable n) _ y))));
-            [unfold varBoundedToZ, boundedArg; rewrite <- convertArg_var; assumption |].
+    Definition ZToWord a := @convertExpr Z Word _ _ t a.
+    Definition ZToBounded a := @convertExpr Z Bounded _ _ t a.
+    Definition ZToRWV a := @convertExpr Z RWV _ _ t a.
 
-          pose proof (ZToBounded_binop_correct (n := n) op x y) as C;
-            unfold boundedArg, zOp, wOp, varZToBounded,
-                   varBoundedToZ, convertZToBounded in *;
-            simpl in C.
+    Definition varZToWord a := @convertVar Z Word _ _ t a.
+    Definition varZToBounded a := @convertVar Z Bounded _ _ t a.
+    Definition varZToRWV a := @convertVar Z RWV _ _ t a.
 
-          repeat rewrite convertArg_interp; symmetry.
+    Definition varWordToZ a := @convertVar Word Z _ _ t a.
+    Definition varBoundedToZ a := @convertVar Bounded Z _ _ t a.
+    Definition varRWVToZ a := @convertVar RWV Z _ _ t a.
 
-          induction op; apply (C (fun _ => Return (Const 0%Z))); clear C;
-            unfold bcheck, getBounds; simpl;
-            destruct (@just_zero n) as [j p]; rewrite p; reflexivity.
+    Definition zinterp E := @interp Z _ t E.
+    Definition wordInterp E := @interp' Word _ _ t (fun x => NToWord n (Z.to_N x)) E.
+    Definition boundedInterp E := @interp Bounded _ t E.
+    Definition rwvInterp E := @interp RWV _ t E.
 
-      - simpl in S.
-        induction a as [| |t0 t1 a0 IHa0 a1 IHa1]; simpl in *; try reflexivity.
-        cbv [bcheck bcheck' getBounds interp convertExpr interp_arg convertArg match_arg_Prod] in S.
-        apply andb_true_iff in S; destruct S; rewrite IHa0, IHa1; try reflexivity; assumption.
-    Qed.
-  End Correctness.
+    Section Operations.
+      Context {tx ty tz: type}.
 
-  Section FastCorrect.
-    Context {n: nat}.
+      Definition opZ (op: binop tx ty tz)
+                 (x: @interp_type Z tx) (y: @interp_type Z ty): @interp_type Z tz :=
+        @interp_binop Z _ _ _ _ op x y.
 
-    Record RangeWithValue := rwv {
-      low: N;
-      value: N;
-      high: N
-    }.
-
-    Definition rwv_app {rangeF wordF}
-      (op: @validBinaryWordOp n rangeF wordF)
-      (X Y: RangeWithValue): option (RangeWithValue) :=
-      omap (rangeF (range N (low X) (high X)) (range N (low Y) (high Y))) (fun r' =>
-        match r' with
-        | range l h => Some (
-          rwv l (wordToN (wordF (NToWord n (value X)) (NToWord n (value Y)))) h)
-        end).
-
-    Definition proj (x: RangeWithValue): Range N := range N (low x) (high x).
-
-    Definition from_range (x: Range N): RangeWithValue :=
-      match x with
-      | range l h => rwv l h h
-      end.
+      Definition opBounded (op: binop tx ty tz)
+                 (x: @interp_type Bounded tx) (y: @interp_type Bounded ty): @interp_type Bounded tz :=
+        @interp_binop Bounded _ _ _ _ op x y.
 
-    Instance RWVEval : Evaluable (option RangeWithValue) := {
-      ezero := None;
 
-      toT := fun x =>
-        if (Nge_dec (N.pred (Npow2 n)) (Z.to_N x))
-        then Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x))
-        else None;
+      Definition opWord (op: binop tx ty tz)
+                 (x: @interp_type Word tx) (y: @interp_type Word ty): @interp_type Word tz :=
+        @interp_binop Word _ _ _ _ op x y.
 
-      fromT := fun x => orElse 0%Z (option_map Z.of_N (option_map value x));
+      Definition opRWV (op: binop tx ty tz)
+                 (x: @interp_type RWV tx) (y: @interp_type RWV ty): @interp_type RWV tz :=
+        @interp_binop RWV _ _ _ _ op x y.
+    End Operations.
 
-      eadd := fun x y => omap x (fun X => omap y (fun Y =>
-        rwv_app range_add_valid X Y));
+    Definition rangeOf := fun x =>
+      Some (rwv 0%N (Z.to_N x) (Z.to_N x)).
 
-      esub := fun x y => omap x (fun X => omap y (fun Y =>
-        rwv_app range_sub_valid X Y));
+    Definition ZtoB := fun x => omap (rangeOf x) (bwFromRWV (n := n)).
+  End Defaults.
 
-      emul := fun x y => omap x (fun X => omap y (fun Y =>
-        rwv_app range_mul_valid X Y));
-
-      eshiftr := fun x y => omap x (fun X => omap y (fun Y =>
-        rwv_app range_shiftr_valid X Y));
-
-      eand := fun x y => omap x (fun X => omap y (fun Y =>
-        rwv_app range_and_valid X Y));
-
-      eltb := fun x y =>
-        match (x, y) with
-        | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) =>
-            N.ltb xv yv
-
-        | _ => false
-        end;
-
-      eeqb := fun x y =>
-        match (x, y) with
-        | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) =>
-            andb (andb (N.eqb xlow ylow) (N.eqb xhigh yhigh)) (N.eqb xv yv)
+  Section Correctness.
+    Context {n: nat}.
 
-        | _ => false
-        end
-    }.
+    Definition W := (word n).
+    Definition B := (@Bounded n).
+    Definition R := (option RangeWithValue).
 
-    Definition getRWV {t} T (E: Evaluable T) (e : @expr T T t): @interp_type (option RangeWithValue) t :=
-      interp (@convertExpr T (option RangeWithValue) E RWVEval t e).
+    Instance RE : Evaluable R := @RWVEvaluable n.
+    Instance ZE : Evaluable Z := ZEvaluable.
+    Instance WE : Evaluable W := @WordEvaluable n.
+    Instance BE : Evaluable B := @BoundedEvaluable n.
 
-    Definition getRanges {t} T (E: Evaluable T) (e : @expr T T t): @interp_type (option (Range N)) t :=
-      typeMap (option_map proj) (getRWV T E e).
+    Transparent ZE RE WE BE W B R.
 
-    Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) :=
-      match t as t' return (interp_type t') -> bool with
-      | TT => fun x' =>
-        match x' with
-        | Some _ => true
-        | None => false
-        end
-      | Prod t0 t1 => fun x' =>
-        match x' with
-        | (x0, x1) => andb (check' x0) (check' x1)
-        end
-      end x.
-
-    Definition check {t} T (E: Evaluable T) (e : @expr T T t): bool :=
-      check' (getRWV T E e).
+    Existing Instance ZE.
+    Existing Instance RE.
+    Existing Instance WE.
+    Existing Instance BE.
 
     Ltac kill_dec :=
       repeat match goal with
@@ -417,100 +178,281 @@ Module LLConversions.
       | [H : context[Nge_dec ?a ?b] |- _ ] => destruct (Nge_dec a b)
       end.
 
-    Lemma check_spec: forall {t} (E: expr t),
-         check Z ZEvaluable E = true
-      -> bcheck (n := n) Z ZEvaluable E = true.
-    Proof.
-      intros t E H.
-      induction E as [tx ty tz op x y z eC IH| t a].
-
-      - unfold bcheck, getBounds, check, getRWV in *.
-        apply IH; simpl in *; revert H; clear IH.
-        repeat rewrite convertArg_interp.
-        generalize (interp_arg x) as X; intro X; clear x.
-        generalize (interp_arg y) as Y; intro Y; clear y.
-        intro H; rewrite <- H; clear H; repeat f_equal.
-
-        induction op; unfold ZEvaluable, BoundedEvaluable, RWVEval, just in *;
-          simpl in *; kill_dec; simpl in *; try reflexivity;
-          try rewrite (bapp_value_spec _ _ _ (fun x => Z.of_N (@wordToN n x)));
-          unfold vapp, rapp, rwv_app, overflows in *; kill_dec; simpl in *;
-          try reflexivity; try nomega.
-
-      - induction a as [c|v|t0 t1 a0 IHa0 a1 IHa1];
-          unfold bcheck, getBounds, check, getRWV in *; simpl in *; unfold just.
-
-        + induction (Nge_dec (N.pred (Npow2 n)) (Z.to_N c));
-            simpl in *; [reflexivity|inversion H].
-
-        + induction (Nge_dec (N.pred (Npow2 n)) (Z.to_N v));
-            simpl in *; [reflexivity|inversion H].
-
-        + apply andb_true_iff; apply andb_true_iff in H;
-            destruct H as [H0 H1]; split;
-            [apply IHa0|apply IHa1]; assumption.
-    Qed.
-
-    Lemma RangeInterp_spec: forall {t} (E: expr t),
-        check Z ZEvaluable E = true
-      -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (convertZToWord n E).
-    Proof.
-      intros.
-      apply RangeInterp_bounded_spec.
-      apply check_spec.
-      assumption.
-    Qed.
-
-    Lemma getRanges_spec: forall {t} T E (e: @expr T T t),
-      getRanges T E e = typeMap (t := t) (option_map (toRange (n := n))) (getBounds T E e).
-    Proof.
-      intros; induction e as [tx ty tz op x y z eC IH| t a];
-        unfold getRanges, getRWV, option_map, toRange, getBounds in *;
-        simpl in *.
-
-      - rewrite <- IH; clear IH; simpl.
-        repeat f_equal.
-        repeat rewrite (convertArg_interp x); generalize (interp_arg x) as X; intro; clear x.
-        repeat rewrite (convertArg_interp y); generalize (interp_arg y) as Y; intro; clear y.
-
-        (* induction op;
-          unfold RWVEval, BoundedEvaluable, bapp, rwv_app,
-                 overflows, omap, option_map, just; simpl;
-          kill_dec; simpl in *. *)
-    Admitted.
-  End FastCorrect.
+    Section BoundsChecking.
+      Context {T: Type} {E: Evaluable T} {f : T -> B}.
+
+      Definition getBounds {t} (e : @expr T T t): @interp_type B t :=
+        interp' f (@convertExpr T B _ _ t _ e).
+
+      Fixpoint bcheck' {t} (x: @interp_type B t) :=
+        match t as t' return (interp_type t') -> bool with
+        | TT => fun x' =>
+          match x' with
+          | Some _ => true
+          | None => false
+          end
+        | Prod t0 t1 => fun x' =>
+          match x' with
+          | (x0, x1) => andb (bcheck' x0) (bcheck' x1)
+          end
+        end x.
+
+      Definition bcheck {t} (e : expr t): bool := bcheck' (getBounds e).
+    End BoundsChecking.
+
+    Section UtilityLemmas.
+      Context {A B} {EA: Evaluable A} {EB: Evaluable B}.
+
+      Lemma convertArg_interp' : forall {t V} f (x: @arg A V t),
+          (interp_arg' (fun z => toT (fromT (f z))) (@convertArg A B EA EB _ t x))
+            = @convertVar A B EA EB t (interp_arg' f x).
+      Proof.
+        intros.
+        induction x as [| |t0 t1 i0 i1]; simpl; [reflexivity|reflexivity|].
+        induction EA, EB; simpl; f_equal; assumption.
+      Qed.
+
+      Lemma convertArg_var: forall {A B EA EB t} V (x: @interp_type A t),
+          @convertArg A B EA EB V t (uninterp_arg x) = uninterp_arg (var := V) (@convertVar A B EA EB t x).
+      Proof.
+        induction t as [|t0 IHt_0 t1 IHt_1]; simpl; intros; [reflexivity|].
+        induction x as [a b]; simpl; f_equal;
+            induction t0 as [|t0a IHt0_0 t0b IHt0_1],
+                    t1 as [|t1a IHt1_0]; simpl in *;
+            try rewrite IHt_0;
+            try rewrite IHt_1;
+            reflexivity.
+      Qed.
+
+      Lemma ZToBounded_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: @arg Z Z tx) (y: @arg Z Z ty) e f,
+          bcheck (t := tz) (f := f) (LetBinop op x y e) = true
+        -> opZ op (interp_arg x) (interp_arg y) =
+          varBoundedToZ (n := n) (opBounded op
+             (interp_arg' f (convertArg _ x))
+             (interp_arg' f (convertArg _ y))).
+      Proof.
+      Admitted.
+
+      Lemma ZToWord_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e f,
+          bcheck (t := tz) (f := f) (LetBinop op x y e) = true
+        -> opZ op (interp_arg x) (interp_arg y) =
+            varWordToZ (opWord (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))).
+      Proof.
+      Admitted.
+
+      Lemma roundTrip_0 : @toT Correctness.B BE (@fromT Z ZE 0%Z) <> None.
+      Proof.
+        intros; unfold toT, fromT, BE, ZE, BoundedEvaluable, ZEvaluable, bwFromRWV;
+          simpl; try break_match; simpl; try abstract (intro Z; inversion Z);
+          pose proof (Npow2_gt0 n); simpl in *; nomega.
+      Qed.
+
+      Lemma double_conv_var: forall t x,
+        @convertVar R Z _ _ t (@convertVar B R _ _ t x) =
+          @convertVar B Z _ _ t x.
+      Proof.
+        intros.
+      Admitted.
+
+      Lemma double_conv_arg: forall V t a,
+        @convertArg R B _ _ V t (@convertArg Z R _ _ V t a) =
+          @convertArg Z B _ _ V t a.
+      Proof.
+        intros.
+      Admitted.
+    End UtilityLemmas.
+
+
+    Section Spec.
+      Ltac kill_just n :=
+        match goal with
+        | [|- context[just ?x] ] =>
+            let Hvalue := fresh in let Hvalue' := fresh in
+            let Hlow := fresh in let Hlow' := fresh in
+            let Hhigh := fresh in let Hhigh' := fresh in
+            let Hnone := fresh in let Hnone' := fresh in
+
+            let B := fresh in
+
+            pose proof (just_value_spec (n := n) x) as Hvalue;
+            pose proof (just_low_spec (n := n) x) as Hlow;
+            pose proof (just_high_spec (n := n) x) as Hhigh;
+            pose proof (just_None_spec (n := n) x) as Hnone;
+
+            destruct (just x);
+
+            try pose proof (Hlow _ eq_refl) as Hlow';
+            try pose proof (Hvalue _ eq_refl) as Hvalue';
+            try pose proof (Hhigh _ eq_refl) as Hhigh';
+            try pose proof (Hnone eq_refl) as Hnone';
+
+            clear Hlow Hhigh Hvalue Hnone
+        end.
+
+      Lemma RangeInterp_bounded_spec: forall {t} (E: @expr Z Z t),
+          bcheck (f := ZtoB) E = true
+        -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (ZToWord _ E).
+      Proof.
+        intros t E S.
+        unfold zinterp, ZToWord, wordInterp.
+
+        induction E as [tx ty tz op x y z|]; simpl; try reflexivity.
+
+        - repeat rewrite convertArg_var in *.
+          repeat rewrite convertArg_interp in *.
+
+          rewrite H; clear H; repeat f_equal.
+
+          + pose proof (ZToWord_binop_correct op x y) as C;
+              unfold opZ, opWord, varWordToZ, varZToWord in C;
+              simpl in C.
+
+            assert (N.pred (Npow2 n) >= 0)%N. {
+              apply N.le_ge.
+              rewrite <- (N.pred_succ 0).
+              apply N.le_pred_le_succ.
+              rewrite N.succ_pred; [| apply N.neq_0_lt_0; apply Npow2_gt0].
+              apply N.le_succ_l.
+              apply Npow2_gt0.
+            }
+
+            admit. (*
+            induction op; rewrite (C (fun _ => Return (Const 0%Z))); clear C;
+              unfold bcheck, getBounds, boundedInterp, bwFromRWV in *; simpl in *;
+              kill_dec; simpl in *; kill_dec; first [reflexivity|nomega]. *)
+
+          + unfold bcheck, getBounds in *.
+            replace (interp_binop op (interp_arg x) (interp_arg y))
+                with (varBoundedToZ (n := n) (opBounded op
+                        (interp_arg' ZtoB (convertArg _ x))
+                        (interp_arg' ZtoB (convertArg _ y)))).
+
+            * rewrite <- S; f_equal; clear S.
+              simpl; repeat f_equal.
+              unfold varBoundedToZ, opBounded.
+              repeat rewrite convertArg_var.
+              Arguments convertArg _ _ _ _ _ _ _ : clear implicits.
+              admit.
+
+            * pose proof (ZToBounded_binop_correct op x y) as C;
+                unfold opZ, opWord, varZToBounded,
+                    varBoundedToZ in *;
+                simpl in C.
+
+              Local Opaque toT fromT.
+
+              induction op; erewrite (C (fun _ => Return (Const 0%Z))); clear C; try reflexivity;
+                unfold bcheck, getBounds; simpl;
+                pose proof roundTrip_0 as H;
+                induction (toT (fromT _)); first [reflexivity|contradict H; reflexivity].
+
+              Local Transparent toT fromT.
+
+        - simpl in S.
+          induction a as [| |t0 t1 a0 IHa0 a1 IHa1]; simpl in *; try reflexivity.
+          admit.
+
+          (*
+          + f_equal.
+            unfold bcheck, getBounds, boundedInterp in S; simpl in S.
+            kill_dec; simpl; [reflexivity|simpl in S; inversion S].
+
+          + f_equal.
+            unfold bcheck, getBounds, boundedInterp, boundVarInterp in S; simpl in S;
+              kill_dec; simpl; try reflexivity; try nomega.
+            inversion S.
+            admit.
+            admit.
+
+          + unfold bcheck in S; simpl in S;
+              apply andb_true_iff in S; destruct S as [S0 S1];
+              rewrite IHa0, IHa1; [reflexivity| |];
+              unfold bcheck, getBounds; simpl; assumption. *)
+      Admitted.
+    End Spec.
+
+    Section RWVSpec.
+      Section Defs.
+        Context {V} {f : V -> R}.
+
+        Definition getRanges {t} (e : @expr R V t): @interp_type (option (Range N)) t :=
+            typeMap (option_map rwvToRange) (interp' f e).
+
+        Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) :=
+            match t as t' return (interp_type t') -> bool with
+            | TT => fun x' => orElse false (option_map (checkRWV (n := n)) x')
+            | Prod t0 t1 => fun x' =>
+                match x' with
+                | (x0, x1) => andb (check' x0) (check' x1)
+                end
+            end x.
+
+        Definition check {t} (e : @expr R V t): bool := check' (interp' f e).
+      End Defs.
+
+      Ltac kill_dec :=
+        repeat match goal with
+        | [|- context[Nge_dec ?a ?b] ] => destruct (Nge_dec a b)
+        | [H : context[Nge_dec ?a ?b] |- _ ] => destruct (Nge_dec a b)
+        end.
+
+      Lemma check_spec' : forall {rangeF wordF} (op: @validBinaryWordOp n rangeF wordF) x y,
+        @convertVar B R _ _ TT (
+          omap (interp_arg' ZtoB (convertArg TT x)) (fun X =>
+            omap (interp_arg' ZtoB (convertArg TT y)) (fun Y =>
+              bapp op X Y))) =
+          omap (interp_arg' rangeOf x) (fun X =>
+            omap (interp_arg' rangeOf y) (fun Y =>
+              rwv_app (n := n) op X Y)).
+      Proof.
+      Admitted.
+
+      Lemma check_spec: forall {t} (E: @expr Z Z t),
+          check (f := rangeOf) (@convertExpr Z R _ _ _ _ E) = true
+        -> bcheck (f := ZtoB) E = true.
+      Proof.
+        intros t E H.
+        induction E as [tx ty tz op x y z eC IH| t a].
+
+        - unfold bcheck, getBounds, check in *.
+
+          simpl; apply IH; clear IH; rewrite <- H; clear H.
+          simpl; rewrite convertArg_var; repeat f_equal.
+
+          unfold interp_binop, RE, WE, BE, ZE,
+              BoundedEvaluable, RWVEvaluable, ZEvaluable,
+              eadd, emul, esub, eshiftr, eand.
+
+          admit.
+
+          (*induction op; rewrite check_spec'; reflexivity. *)
+
+        - unfold bcheck, getBounds, check in *.
+
+          induction a as [a|a|t0 t1 a0 IHa0 a1 IHa1].
+
+          + admit.
+
+
+          + unfold rangeOf in *.
+            simpl in *; kill_dec; try reflexivity; try inversion H.
+            admit.
+
+          + simpl in *; rewrite IHa0, IHa1; simpl; [reflexivity | | ];
+              apply andb_true_iff in H; destruct H as [H1 H2];
+              assumption.
+      Admitted.
+
+      Lemma RangeInterp_spec: forall {t} (E: @expr Z Z t),
+          check (f := rangeOf) (@convertExpr Z R _ _ _ _ E) = true
+        -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E)
+            = wordInterp (ZToWord _ E).
+      Proof.
+        intros.
+        apply RangeInterp_bounded_spec.
+        apply check_spec.
+        assumption.
+      Qed.
+    End RWVSpec.
+  End Correctness.
 End LLConversions.
-
-Section ConversionTest.
-  Import HL HLConversions.
-
-  Fixpoint keepAddingOne {var} (x : @expr Z var TT) (n : nat) : @expr Z var TT :=
-    match n with
-    | O => x
-    | S n' => Let (Binop OPadd x (Const 1%Z)) (fun y => keepAddingOne (Var y) n')
-    end.
-
-  Definition KeepAddingOne (n : nat) : Expr (T := Z) TT :=
-    fun var => keepAddingOne (Const 1%Z) n.
-
-  Definition testCase := Eval vm_compute in KeepAddingOne 4000.
-
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 0 testCase))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 1 testCase))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 10 testCase))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 32 testCase))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 64 testCase))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 128 testCase))).
-
-  Definition nefarious : Expr (T := Z) TT :=
-    fun var => Let (Binop OPadd (Const 10%Z) (Const 20%Z))
-                   (fun y => Binop OPmul (Var y) (Const 0%Z)).
-
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 0 nefarious))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 1 nefarious))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 4 nefarious))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 5 nefarious))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 32 nefarious))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 64 nefarious))).
-  Eval vm_compute in (typeMap (option_map toRange) (BInterp (ZToRange 128 nefarious))).
-End ConversionTest.
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v
index 2cfdaa139..0678c80bb 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -7,13 +7,33 @@ Require Import ProofIrrelevance.
 
 Import ListNotations.
 
+Section BaseTypes.
+  Inductive Range T := | range: forall (low high: T), Range T.
+
+  Record RangeWithValue := rwv {
+    rwv_low: N;
+    rwv_value: N;
+    rwv_high: N
+  }.
+
+  Record BoundedWord {n} := bounded {
+    bw_low: N;
+    bw_value: word n;
+    bw_high: N;
+
+    ge_low: (bw_low <= wordToN bw_value)%N;
+    le_high: (wordToN bw_value <= bw_high)%N;
+    high_bound: (bw_high < Npow2 n)%N
+  }.
+End BaseTypes.
+
 Section Evaluability.
   Class Evaluable T := evaluator {
     ezero: T;
 
     (* Conversions *)
-    toT: Z -> T;
-    fromT: T -> Z;
+    toT: option RangeWithValue -> T;
+    fromT: T -> option RangeWithValue;
 
     (* Operations *)
     eadd: T -> T -> T;
@@ -29,12 +49,14 @@ Section Evaluability.
 End Evaluability.
 
 Section Z.
+  Context {n: nat}.
+
   Instance ZEvaluable : Evaluable Z := {
     ezero := 0%Z;
 
     (* Conversions *)
-    toT     := fun x => x;
-    fromT   := fun x => x;
+    toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
+    fromT   := fun x => Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x));
 
     (* Operations *)
     eadd    := Z.add;
@@ -48,6 +70,46 @@ Section Z.
     eeqb    := Z.eqb
   }.
 
+  Instance ConstEvaluable : Evaluable Z := {
+    ezero := 0%Z;
+
+    (* Conversions *)
+    toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
+    fromT   := fun x =>
+      if (Nge_dec (N.pred (Npow2 n)) (Z.to_N x))
+      then Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x))
+      else None;
+
+    (* Operations *)
+    eadd    := Z.add;
+    esub    := Z.sub;
+    emul    := Z.mul;
+    eshiftr := Z.shiftr;
+    eand    := Z.land;
+
+    (* Comparisons *)
+    eltb    := Z.ltb;
+    eeqb    := Z.eqb
+  }.
+
+  Instance InputEvaluable : Evaluable Z := {
+    ezero := 0%Z;
+
+    (* Conversions *)
+    toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
+    fromT   := fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x));
+
+    (* Operations *)
+    eadd    := Z.add;
+    esub    := Z.sub;
+    emul    := Z.mul;
+    eshiftr := Z.shiftr;
+    eand    := Z.land;
+
+    (* Comparisons *)
+    eltb    := Z.ltb;
+    eeqb    := Z.eqb
+  }.
 End Z.
 
 Section Word.
@@ -57,8 +119,8 @@ Section Word.
     ezero := wzero n;
 
     (* Conversions *)
-    toT := fun x => @NToWord n (Z.to_N x);
-    fromT := fun x => Z.of_N (@wordToN n x);
+    toT := fun x => @NToWord n (orElse 0%N (option_map rwv_value x));
+    fromT := fun x => let v := @wordToN n x in (Some (rwv v v v));
 
     (* Operations *)
     eadd := @wplus n;
@@ -76,8 +138,6 @@ End Word.
 Section RangeUpdate.
   Context {n: nat}.
 
-  Inductive Range T := | range: forall (low high: T), Range T.
-
   Definition validBinaryWordOp
         (rangeF: Range N -> Range N -> option (Range N))
         (wordF: word n -> word n -> word n): Prop :=
@@ -464,19 +524,12 @@ End RangeUpdate.
 Section BoundedWord.
   Context {n: nat}.
 
-  Record BoundedWord := bounded {
-    low: N;
-    value: word n;
-    high: N;
-
-    ge_low: (low <= wordToN value)%N;
-    le_high: (wordToN value <= high)%N;
-    high_bound: (high < Npow2 n)%N
-  }.
+  Definition BW := @BoundedWord n.
+  Transparent BW.
 
   Definition bapp {rangeF wordF}
       (op: @validBinaryWordOp n rangeF wordF)
-      (X Y: BoundedWord): option BoundedWord.
+      (X Y: BW): option BW.
 
     refine (
       let op' := op _ _ _ _ _ _
@@ -484,12 +537,12 @@ Section BoundedWord.
         (ge_low Y) (le_high Y) (high_bound Y) in
 
       let result := rangeF
-        (range N (low X) (high X))
-        (range N (low Y) (high Y)) in
+        (range N (bw_low X) (bw_high X))
+        (range N (bw_low Y) (bw_high Y)) in
 
       match result as r' return result = r' -> _ with
       | Some (range low high) => fun e =>
-        Some (bounded low (wordF (value X) (value Y)) high _ _ _)
+        Some (@bounded n low (wordF (bw_value X) (bw_value Y)) high _ _ _)
       | None => fun _ => None
       end eq_refl); abstract (
 
@@ -510,26 +563,42 @@ Section BoundedWord.
       (X Y: word n): option (word n) :=
     Some (wordF X Y).
 
-  Lemma bapp_value_spec: forall {T rangeF wordF}
-      (op: @validBinaryWordOp n rangeF wordF)
-      (b0 b1: BoundedWord) (f: word n -> T),
-    option_map (fun x => f (value x)) (bapp op b0 b1)
-  = option_map (fun x => f x) (
-      omap (rapp op (range N (low b0) (high b0))
-                    (range N (low b1) (high b1))) (fun _ =>
-        vapp op (value b0) (value b1))).
-  Proof.
-  Admitted.
+  Definition bwToRWV (w: BW): RangeWithValue :=
+    rwv (bw_low w) (wordToN (bw_value w)) (bw_high w).
 
-  Definition toRange (w: BoundedWord): Range N :=
-    range N (low w) (high w).
+  Definition bwFromRWV (r: RangeWithValue): option BW.
+    refine
+      match r with
+      | rwv l v h =>
+        match (Nge_dec h v, Nge_dec v l, Nge_dec (N.pred (Npow2 n)) h) with
+        | (left p0, left p1, left p2) => Some (@bounded n l (NToWord n l) h _ _ _)
+        | _ => None
+        end
+      end; try rewrite wordToN_NToWord;
+
+      assert (N.succ h <= Npow2 n)%N by abstract (
+        apply N.ge_le in p2;
+        rewrite <- (N.pred_succ h) in p2;
+        apply -> N.le_pred_le_succ in p2;
+        rewrite N.succ_pred in p2; [assumption |];
+        apply N.neq_0_lt_0;
+        apply Npow2_gt0);
+
+      try abstract (apply (N.lt_le_trans _ (N.succ h) _);
+        [nomega|assumption]);
 
-  Definition fromRange (r: Range N): option (BoundedWord).
+      [reflexivity| etransitivity; apply N.ge_le; eassumption].
+  Defined.
+
+  Definition bwToRange (w: BW): Range N :=
+    range N (bw_low w) (bw_high w).
+
+  Definition bwFromRange (r: Range N): option BW.
     refine
       match r with
       | range l h =>
         match (Nge_dec h l, Nge_dec (N.pred (Npow2 n)) h) with
-        | (left p0, left p1) => Some (bounded l (NToWord n l) h _ _ _)
+        | (left p0, left p1) => Some (@bounded n l (NToWord n l) h _ _ _)
         | _ => None
         end
       end; try rewrite wordToN_NToWord;
@@ -546,13 +615,12 @@ Section BoundedWord.
         [nomega|assumption]);
 
       [reflexivity|apply N.ge_le; assumption].
-
   Defined.
 
-  Definition just (x: N): option (BoundedWord).
+  Definition just (x: N): option BW.
     refine
       match Nge_dec (N.pred (Npow2 n)) x with
-      | left p => Some (bounded x (NToWord n x) x _ _ _)
+      | left p => Some (@bounded n x (NToWord n x) x _ _ _)
       | right _ => None
       end; try rewrite wordToN_NToWord; try reflexivity;
 
@@ -580,29 +648,29 @@ Section BoundedWord.
     apply N.le_ge; apply N.succ_le_mono; assumption.
   Qed.
 
-  Lemma just_value_spec: forall x b, just x = Some b -> value b = NToWord n x.
+  Lemma just_value_spec: forall x b, just x = Some b -> bw_value b = NToWord n x.
   Proof.
     intros x b H; destruct b; unfold just in *;
     destruct (Nge_dec (N.pred (Npow2 n)) x);
     simpl in *; inversion H; subst; reflexivity.
   Qed.
 
-  Lemma just_low_spec: forall x b, just x = Some b -> low b = x.
+  Lemma just_low_spec: forall x b, just x = Some b -> bw_low b = x.
   Proof.
     intros x b H; destruct b; unfold just in *;
     destruct (Nge_dec (N.pred (Npow2 n)) x);
     simpl in *; inversion H; subst; reflexivity.
   Qed.
 
-  Lemma just_high_spec: forall x b, just x = Some b -> high b = x.
+  Lemma just_high_spec: forall x b, just x = Some b -> bw_high b = x.
   Proof.
     intros x b H; destruct b; unfold just in *;
     destruct (Nge_dec (N.pred (Npow2 n)) x);
     simpl in *; inversion H; subst; reflexivity.
   Qed.
 
-  Definition any: BoundedWord.
-    refine (bounded 0%N (wzero n) (N.pred (Npow2 n)) _ _ _);
+  Definition any: BW.
+    refine (@bounded n 0%N (wzero n) (N.pred (Npow2 n)) _ _ _);
       try rewrite wordToN_zero;
       try reflexivity;
       try abstract (apply N.lt_le_pred; apply Npow2_gt0).
@@ -610,17 +678,11 @@ Section BoundedWord.
     apply N.lt_pred_l; apply N.neq_0_lt_0; apply Npow2_gt0.
   Defined.
 
-  Definition orElse {T} (d: T) (o: option T): T :=
-    match o with
-    | Some v => v
-    | None => d
-    end.
-
-  Instance BoundedEvaluable : Evaluable (option BoundedWord) := {
+  Instance BoundedEvaluable : Evaluable (option BW) := {
     ezero := Some any;
 
-    toT := fun x => just (Z.to_N x);
-    fromT := fun x => orElse 0%Z (option_map (fun x' => Z.of_N (wordToN (value x'))) x);
+    toT := fun x => omap x bwFromRWV;
+    fromT := option_map bwToRWV;
 
     eadd := fun x y => omap x (fun X => omap y (fun Y => bapp range_add_valid X Y));
     esub := fun x y => omap x (fun X => omap y (fun Y => bapp range_sub_valid X Y));
@@ -630,11 +692,91 @@ Section BoundedWord.
 
     eltb := fun x y =>
       orElse false (omap x (fun X => omap y (fun Y =>
-        Some (N.ltb (high X) (high Y)))));
+        Some (N.ltb (wordToN (bw_value X)) (wordToN (bw_value Y))))));
 
     eeqb := fun x y =>
       orElse false (omap x (fun X => omap y (fun Y =>
-        Some (andb (N.eqb (low X) (low Y)) (N.eqb (high X) (high Y))))))
+        Some (N.eqb (wordToN (bw_value X)) (wordToN (bw_value Y))))))
   }.
-
 End BoundedWord.
+
+Section RangeWithValue.
+  Context {n: nat}.
+
+  Definition rwv_app {rangeF wordF}
+    (op: @validBinaryWordOp n rangeF wordF)
+    (X Y: RangeWithValue): option (RangeWithValue) :=
+    omap (rangeF (range N (rwv_low X) (rwv_high X))
+                 (range N (rwv_low Y) (rwv_high Y))) (fun r' =>
+      match r' with
+      | range l h => Some (
+          rwv l (wordToN (wordF (NToWord n (rwv_value X))
+                                (NToWord n (rwv_value Y)))) h)
+      end).
+
+  Definition checkRWV (x: RangeWithValue): bool :=
+    match x with
+    | rwv l v h =>
+      match (Nge_dec h v, Nge_dec v l, Nge_dec (N.pred (Npow2 n)) h) with
+      | (left _, left _, left _) => true
+      | _ => false
+      end
+    end.
+
+  Lemma rwv_None_spec : forall {rangeF wordF}
+      (op: @validBinaryWordOp n rangeF wordF)
+      (X Y: RangeWithValue),
+    omap (rwv_app op X Y) (bwFromRWV (n := n)) <> None.
+  Proof.
+  Admitted.
+
+  Definition rwvToRange (x: RangeWithValue): Range N :=
+    range N (rwv_low x) (rwv_high x).
+
+  Definition rwvFromRange (x: Range N): RangeWithValue :=
+    match x with
+    | range l h => rwv l h h
+    end.
+
+  Lemma bwToFromRWV: forall x, option_map (@bwToRWV n) (omap x bwFromRWV) = x.
+  Proof.
+  Admitted.
+
+  Instance RWVEvaluable : Evaluable (option RangeWithValue) := {
+    ezero := None;
+
+    toT := fun x => x;
+    fromT := fun x => omap x (fun x' => if (checkRWV x') then x else None);
+
+    eadd := fun x y => omap x (fun X => omap y (fun Y =>
+      rwv_app range_add_valid X Y));
+
+    esub := fun x y => omap x (fun X => omap y (fun Y =>
+      rwv_app range_sub_valid X Y));
+
+    emul := fun x y => omap x (fun X => omap y (fun Y =>
+      rwv_app range_mul_valid X Y));
+
+    eshiftr := fun x y => omap x (fun X => omap y (fun Y =>
+      rwv_app range_shiftr_valid X Y));
+
+    eand := fun x y => omap x (fun X => omap y (fun Y =>
+      rwv_app range_and_valid X Y));
+
+    eltb := fun x y =>
+      match (x, y) with
+      | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) =>
+          N.ltb xv yv
+
+      | _ => false
+      end;
+
+    eeqb := fun x y =>
+      match (x, y) with
+      | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) =>
+          andb (andb (N.eqb xlow ylow) (N.eqb xhigh yhigh)) (N.eqb xv yv)
+
+      | _ => false
+      end
+  }.
+End RangeWithValue.
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 7bb367a9f..3f3c34b71 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -1,5 +1,7 @@
-Require Import Crypto.Assembly.Pipeline.
+Require Import Coq.ZArith.Znat.
+Require Import Coq.ZArith.ZArith.
 
+Require Import Crypto.Assembly.Pipeline.
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.Specific.GF25519.
@@ -9,6 +11,8 @@ Module GF25519.
   Definition bits: nat := 64.
   Definition width: Width bits := W64.
 
+  Existing Instance ZEvaluable.
+
   Fixpoint makeBoundList {n} k (b: @BoundedWord n) :=
     match k with
     | O => nil
@@ -17,11 +21,12 @@ Module GF25519.
 
   Section DefaultBounds.
     Import ListNotations.
-    Local Notation rr exp := (range N 0%N (2^exp + 2^(exp-3))%N).
 
-    Definition feBound: list (Range N) :=
-      [rr 25; rr 26; rr 25; rr 26; rr 25;
-       rr 26; rr 25; rr 26; rr 25; rr 26].
+    Local Notation rr exp := (2^exp + 2^(exp-3))%Z.
+
+    Definition feBound: list Z :=
+      [rr 26; rr 27; rr 26; rr 27; rr 26;
+       rr 27; rr 26; rr 27; rr 26; rr 27].
   End DefaultBounds.
 
   Definition FE: type.
@@ -31,225 +36,272 @@ Module GF25519.
     exact t.
   Defined.
 
-  Definition liftFE {T} (F: @interp_type Z FE -> T) :=
-    fun (a b c d e f g h i j: Z) => F (a, b, c, d, e, f, g, h, i, j).
+  Section Expressions.
+    Definition flatten {T}: (@interp_type Z FE -> T) -> NAry 10 Z T.
+      intro F; refine (fun (a b c d e f g h i j: Z) =>
+        F (a, b, c, d, e, f, g, h, i, j)).
+    Defined.
 
-  Module AddExpr <: Expression.
-    Definition bits: nat := bits.
-    Definition inputs: nat := 20.
-    Definition width: Width bits := width.
-    Definition ResultType := FE.
-    Definition inputBounds := feBound ++ feBound.
+    Definition unflatten {T}:
+      (forall a b c d e f g h i j : Z, T (a, b, c, d, e, f, g, h, i, j))
+    -> (forall x: @interp_type Z FE, T x).
+    Proof.
+      intro F; refine (fun (x: @interp_type Z FE) =>
+        let '(a, b, c, d, e, f, g, h, i, j) := x in
+        F a b c d e f g h i j).
+    Defined.
+
+    Ltac intro_vars_for R := revert R;
+      match goal with
+      | [ |- forall x, @?T x ] => apply (@unflatten T); intros
+      end.
 
     Definition ge25519_add_expr :=
-        Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_add.
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in carry_add.
 
-    Definition ge25519_add' (P Q: @interp_type Z FE) :
-        { r: @HL.expr Z (@interp_type Z) FE
-        | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_add_expr P Q }.
-    Proof.
-      vm_compute in P, Q; repeat
-        match goal with
-        | [x:?T |- _] =>
-          lazymatch T with
-          | Z => fail
-          | prod _ _ => destruct x
-          | _ => clear x
-          end
-        end.
+    Definition ge25519_sub_expr :=
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in carry_sub.
 
-      eexists.
-      cbv beta delta [ge25519_add_expr].
+    Definition ge25519_mul_expr :=
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in mul.
 
-      let R := HL.rhs_of_goal in
-      let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X);
-        [reflexivity|].
+    Definition ge25519_opp_expr :=
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in opp.
 
-      cbv iota beta delta [
-            interp_type interp_binop HL.interp
-            Z.land ZEvaluable eadd esub emul eshiftr eand].
-      reflexivity.
-    Defined.
+    Definition ge25519_add' (P Q: @interp_type Z FE):
+      { r: @HL.Expr Z FE | HL.Interp r = ge25519_add_expr P Q }.
+    Proof.
+      intro_vars_for P.
+      intro_vars_for Q.
 
-    Definition ge25519_add (P Q: @interp_type Z ResultType) :=
-        proj1_sig (ge25519_add' P Q).
+      eexists.
 
-    Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        liftFE (fun p => (liftFE (fun q => ge25519_add p q))).
+      cbv beta delta [ge25519_add_expr].
 
-    Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-        refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t;
-        [ refine LL.uninterp_arg | refine LL.interp_arg ].
-    Defined.
+      etransitivity; [reflexivity|].
 
-    Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
-      Eval vm_compute in hlProg'.
-  End AddExpr.
+      let R := HL.rhs_of_goal in
+      let X := HL.Reify R in
+      transitivity (HL.Interp (X bits)); [reflexivity|].
 
-  Module SubExpr <: Expression.
-    Definition bits: nat := bits.
-    Definition inputs: nat := 20.
-    Definition width: Width bits := width.
-    Definition ResultType := FE.
-    Definition inputBounds := feBound ++ feBound.
+      cbv iota beta delta [ HL.Interp
+          interp_type interp_binop HL.interp
+          Z.land ZEvaluable eadd esub emul eshiftr eand].
 
-    Definition ge25519_sub_expr :=
-        Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_sub.
+      reflexivity.
+    Defined.
 
-    Definition ge25519_sub' (P Q: @interp_type Z FE) :
-        { r: @HL.expr Z (@interp_type Z) FE
-        | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_sub_expr P Q }.
+    Definition ge25519_sub' (P Q: @interp_type Z FE):
+      { r: @HL.Expr Z FE | HL.Interp r = ge25519_sub_expr P Q }.
     Proof.
-      vm_compute in P, Q; repeat
-        match goal with
-        | [x:?T |- _] =>
-          lazymatch T with
-          | Z => fail
-          | prod _ _ => destruct x
-          | _ => clear x
-          end
-        end.
+      intro_vars_for P.
+      intro_vars_for Q.
 
       eexists.
+
       cbv beta delta [ge25519_sub_expr].
 
+      etransitivity; [reflexivity|].
+
       let R := HL.rhs_of_goal in
-      let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X);
-        [reflexivity|].
+      let X := HL.Reify R in
+      transitivity (HL.Interp (X bits)); [reflexivity|].
+
+      cbv iota beta delta [ HL.Interp
+          interp_type interp_binop HL.interp
+          Z.land ZEvaluable eadd esub emul eshiftr eand].
 
-      cbv iota beta delta [
-        interp_type interp_binop HL.interp
-        Z.land ZEvaluable eadd esub emul eshiftr eand].
       reflexivity.
     Defined.
 
-    Definition ge25519_sub (P Q: @interp_type Z ResultType) :=
-        proj1_sig (ge25519_sub' P Q).
+    Definition ge25519_mul' (P Q: @interp_type Z FE):
+      { r: @HL.Expr Z FE | HL.Interp r = ge25519_mul_expr P Q }.
+    Proof.
+      intro_vars_for P.
+      intro_vars_for Q.
 
-    Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        liftFE (fun p => (liftFE (fun q => ge25519_sub p q))).
+      eexists.
 
-    Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-        refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t;
-        [ refine LL.uninterp_arg | refine LL.interp_arg ].
-    Defined.
+      cbv beta delta [ge25519_mul_expr].
 
-    Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
-      Eval vm_compute in hlProg'.
-  End SubExpr.
+      etransitivity; [reflexivity|].
 
-  Module MulExpr <: Expression.
-    Definition bits: nat := bits.
-    Definition inputs: nat := 20.
-    Definition width: Width bits := width.
-    Definition ResultType := FE.
-    Definition inputBounds := feBound ++ feBound.
+      let R := HL.rhs_of_goal in
+      let X := HL.Reify R in
+      transitivity (HL.Interp (X bits)); [reflexivity|].
 
-    Definition ge25519_mul_expr :=
-        Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in mul.
+      cbv iota beta delta [ HL.Interp
+          interp_type interp_binop HL.interp
+          Z.land ZEvaluable eadd esub emul eshiftr eand].
+
+      reflexivity.
+    Defined.
 
-    Definition ge25519_mul' (P Q: @interp_type Z FE) :
-        { r: @HL.expr Z (@interp_type Z) FE
-        | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_mul_expr P Q }.
+    Definition ge25519_opp' (P: @interp_type Z FE):
+      { r: @HL.Expr Z FE | HL.Interp r = ge25519_opp_expr P }.
     Proof.
-      vm_compute in P, Q; repeat
-        match goal with
-        | [x:?T |- _] =>
-          lazymatch T with
-          | Z => fail
-          | prod _ _ => destruct x
-          | _ => clear x
-          end
-      end.
+      intro_vars_for P.
 
       eexists.
-      cbv beta delta [ge25519_mul_expr].
+
+      cbv beta delta [ge25519_opp_expr zero_].
+
+      etransitivity; [reflexivity|].
 
       let R := HL.rhs_of_goal in
-      let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X);
-        [reflexivity|].
+      let X := HL.Reify R in
+      transitivity (HL.Interp (X bits)); [reflexivity|].
+
+      cbv iota beta delta [ HL.Interp
+          interp_type interp_binop HL.interp
+          Z.land ZEvaluable eadd esub emul eshiftr eand].
 
-      cbv iota beta delta [
-        interp_type interp_binop HL.interp
-        Z.land ZEvaluable eadd esub emul eshiftr eand].
       reflexivity.
     Defined.
 
-    Definition ge25519_mul (P Q: @interp_type Z ResultType) :=
-        proj1_sig (ge25519_mul' P Q).
+    Definition ge25519_add (P Q: @interp_type Z FE) :=
+        proj1_sig (ge25519_add' P Q).
 
-    Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        liftFE (fun p => (liftFE (fun q => ge25519_mul p q))).
+    Definition ge25519_sub (P Q: @interp_type Z FE) :=
+        proj1_sig (ge25519_sub' P Q).
 
-    Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-        refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t;
-        [ refine LL.uninterp_arg | refine LL.interp_arg ].
-    Defined.
+    Definition ge25519_mul (P Q: @interp_type Z FE) :=
+        proj1_sig (ge25519_mul' P Q).
 
-    Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
-      Eval vm_compute in hlProg'.
-  End MulExpr.
+    Definition ge25519_opp (P: @interp_type Z FE) :=
+        proj1_sig (ge25519_opp' P).
+  End Expressions.
 
-  Module OppExpr <: Expression.
+  Module AddExpr <: Expression.
     Definition bits: nat := bits.
-    Definition inputs: nat := 10.
+    Definition inputs: nat := 20.
     Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputBounds := feBound.
-
-    Definition ge25519_opp_expr :=
-        Eval cbv beta delta [fe25519 carry_add mul carry_sub carry_opp Let_In] in carry_opp.
+    Definition inputBounds := feBound ++ feBound.
 
-    Definition ge25519_opp' (P: @interp_type Z FE) :
-        { r: @HL.expr Z (@interp_type Z) FE
-        | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_opp_expr P }.
-    Proof.
-      vm_compute in P; repeat
-        match goal with
-        | [x:?T |- _] =>
-          lazymatch T with
-          | Z => fail
-          | prod _ _ => destruct x
-          | _ => clear x
-          end
-        end.
+    Definition prog: NAry 20 Z (@HL.Expr Z ResultType) :=
+        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_add p q)))).
+  End AddExpr.
 
-      eexists.
-      cbv beta delta [ge25519_opp_expr zero_].
+  Module SubExpr <: Expression.
+    Definition bits: nat := bits.
+    Definition inputs: nat := 20.
+    Definition width: Width bits := width.
+    Definition ResultType := FE.
+    Definition inputBounds := feBound ++ feBound.
 
-      let R := HL.rhs_of_goal in
-      let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X);
-        [reflexivity|].
+    Definition ge25519_sub_expr :=
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in
+        carry_sub.
 
-      cbv iota beta delta [
-        interp_type interp_binop HL.interp
-        Z.land ZEvaluable eadd esub emul eshiftr eand].
-      reflexivity.
-    Defined.
+    Definition prog: NAry 20 Z (@HL.Expr Z ResultType) :=
+        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_sub p q)))).
+  End SubExpr.
 
-    Definition ge25519_opp (P: @interp_type Z ResultType) :=
-        proj1_sig (ge25519_opp' P).
+  Module MulExpr <: Expression.
+    Definition bits: nat := bits.
+    Definition inputs: nat := 20.
+    Definition width: Width bits := width.
+    Definition ResultType := FE.
+    Definition inputBounds := feBound ++ feBound.
 
-    Definition hlProg'': NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        liftFE (fun p => ge25519_opp p).
+    Definition prog: NAry 20 Z (@HL.Expr Z ResultType) :=
+        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_mul p q)))).
+  End MulExpr.
 
-    Definition hlProg': NAry 10 Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-        refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t;
-        [ refine LL.uninterp_arg | refine LL.interp_arg ].
-    Defined.
+  Module OppExpr <: Expression.
+    Definition bits: nat := bits.
+    Definition inputs: nat := 10.
+    Definition width: Width bits := width.
+    Definition ResultType := FE.
+    Definition inputBounds := feBound.
 
-    Definition hlProg: NAry 10 Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
-      Eval vm_compute in hlProg'.
+    Definition prog: NAry 10 Z (@HL.Expr Z ResultType) :=
+        Eval cbv in (flatten ge25519_opp).
   End OppExpr.
 
   Module Add := Pipeline AddExpr.
   Module Sub := Pipeline SubExpr.
   Module Mul := Pipeline MulExpr.
   Module Opp := Pipeline OppExpr.
+
+  Section Instantiation.
+    Require Import InitialRing.
+
+    Definition Binary : Type := NAry 20 (word bits) (@interp_type (word bits) FE).
+    Definition Unary : Type := NAry 10 (word bits) (@interp_type (word bits) FE).
+
+    Ltac ast_simpl := cbv [
+      Add.bits Add.inputs AddExpr.inputs Add.ResultType AddExpr.ResultType
+      Add.W Add.R Add.ZEvaluable Add.WEvaluable Add.REvaluable
+      Add.AST.progW Add.LL.progW Add.HL.progW AddExpr.prog
+
+      Sub.bits Sub.inputs SubExpr.inputs Sub.ResultType SubExpr.ResultType
+      Sub.W Sub.R Sub.ZEvaluable Sub.WEvaluable Sub.REvaluable
+      Sub.AST.progW Sub.LL.progW Sub.HL.progW SubExpr.prog
+
+      Mul.bits Mul.inputs MulExpr.inputs Mul.ResultType MulExpr.ResultType
+      Mul.W Mul.R Mul.ZEvaluable Mul.WEvaluable Mul.REvaluable
+      Mul.AST.progW Mul.LL.progW Mul.HL.progW MulExpr.prog
+
+      Opp.bits Opp.inputs OppExpr.inputs Opp.ResultType OppExpr.ResultType
+      Opp.W Opp.R Opp.ZEvaluable Opp.WEvaluable Opp.REvaluable
+      Opp.AST.progW Opp.LL.progW Opp.HL.progW OppExpr.prog
+
+      HLConversions.convertExpr CompileHL.Compile CompileHL.compile
+
+      LL.interp LL.uninterp_arg LL.under_lets LL.interp_arg
+
+      ZEvaluable WordEvaluable RWVEvaluable rwv_value
+      eadd esub emul eand eshiftr toT fromT
+
+      interp_binop interp_type FE liftN NArgMap id
+      omap option_map orElse].
+
+    (* Tack this on to make a simpler AST, but it really slows us down *)
+    Ltac word_simpl := cbv [
+      AddExpr.bits SubExpr.bits MulExpr.bits OppExpr.bits bits
+      NToWord posToWord natToWord wordToNat wordToN wzero'
+      Nat.mul Nat.add].
+
+    Ltac kill_conv := let p := fresh in
+      pose proof N2Z.id as p; unfold Z.to_N in p;
+      repeat rewrite p; clear p;
+      repeat rewrite NToWord_wordToN.
+
+    Local Notation unary_eq f g
+      := (forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+             f x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+             = g x0 x1 x2 x3 x4 x5 x6 x7 x8 x9).
+    Local Notation binary_eq f g
+      := (forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9,
+             f x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9
+             = g x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9).
+
+    Definition add'
+      : {f: Binary |
+         binary_eq f (NArgMap (fun x => Z.of_N (wordToN x)) Add.AST.progW) }.
+    Proof. eexists; intros; ast_simpl; kill_conv; reflexivity. Defined.
+
+    Definition sub'
+      : {f: Binary |
+         binary_eq f (NArgMap (fun x => Z.of_N (wordToN x)) Sub.AST.progW) }.
+    Proof. eexists; ast_simpl; kill_conv; reflexivity. Defined.
+
+    Definition mul'
+      : {f: Binary |
+         binary_eq f (NArgMap (fun x => Z.of_N (wordToN x)) Mul.AST.progW) }.
+    Proof. eexists; ast_simpl; kill_conv; reflexivity. Defined.
+
+    Definition opp' : {f: Unary |
+      unary_eq f (NArgMap (fun x => Z.of_N (wordToN x)) Opp.AST.progW) }.
+    Proof. eexists; ast_simpl; kill_conv; reflexivity. Defined.
+
+    Definition add := Eval simpl in proj1_sig add'.
+    Definition sub := Eval simpl in proj1_sig sub'.
+    Definition mul := Eval simpl in proj1_sig mul'.
+    Definition opp := Eval simpl in proj1_sig opp'.
+  End Instantiation.
 End GF25519.
 
 Extraction "GF25519Add" GF25519.Add.
diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v
index 3866b3b22..1562a3e48 100644
--- a/src/Assembly/GF25519BoundedInstantiation.v
+++ b/src/Assembly/GF25519BoundedInstantiation.v
@@ -15,8 +15,8 @@ Section Operations.
   Import Assembly.GF25519.GF25519.
   Definition wfe: Type := @interp_type (word bits) FE.
 
-  Definition ExprBinOp : Type := NAry 20 (@CompileLL.WArg bits TT) (@CompileLL.WExpr bits FE).
-  Definition ExprUnOp : Type := NAry 10 (@CompileLL.WArg bits TT) (@CompileLL.WExpr bits FE).
+  Definition ExprBinOp : Type := GF25519.Binary.
+  Definition ExprUnOp : Type := GF25519.Unary.
   Axiom ExprUnOpFEToZ : Type.
   Axiom ExprUnOpWireToFE : Type.
   Axiom ExprUnOpFEToWire : Type.
@@ -26,19 +26,16 @@ Section Operations.
   Definition interp_bexpr' (op: ExprBinOp) (x y: tuple (word bits) 10): tuple (word bits) 10 :=
     let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
     let '(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9) := y in
-    let op' := NArgMap LL.Const op in
-    let z := LL.interp (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
-    z.
+    op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9.
 
   Definition interp_uexpr' (op: ExprUnOp) (x: tuple (word bits) 10): tuple (word bits) 10 :=
     let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
-    let op' := NArgMap LL.Const op in
-    let z := LL.interp (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) in
-    z.
-  Definition radd : ExprBinOp := Add.wordProg.
-  Definition rsub : ExprBinOp := Sub.wordProg.
-  Definition rmul : ExprBinOp := Mul.wordProg.
-  Definition ropp : ExprUnOp := Opp.wordProg.
+    op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+
+  Definition radd : ExprBinOp := GF25519.add.
+  Definition rsub : ExprBinOp := GF25519.sub.
+  Definition rmul : ExprBinOp := GF25519.mul.
+  Definition ropp : ExprUnOp := GF25519.opp.
 End Operations.
 
 Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
@@ -57,13 +54,9 @@ Declare Reduction asm_interp
   := cbv [id
             interp_bexpr interp_uexpr interp_bexpr' interp_uexpr'
             radd rsub rmul ropp (*rfreeze rge_modulus rpack runpack*)
-            GF25519.GF25519.Add.wordProg GF25519.GF25519.AddExpr.bits GF25519.GF25519.Add.llProg GF25519.GF25519.AddExpr.hlProg GF25519.GF25519.AddExpr.inputs
-            GF25519.GF25519.Sub.wordProg GF25519.GF25519.SubExpr.bits GF25519.GF25519.Sub.llProg GF25519.GF25519.SubExpr.hlProg GF25519.GF25519.SubExpr.inputs
-            GF25519.GF25519.Mul.wordProg GF25519.GF25519.MulExpr.bits GF25519.GF25519.Mul.llProg GF25519.GF25519.MulExpr.hlProg GF25519.GF25519.MulExpr.inputs
-            GF25519.GF25519.Opp.wordProg GF25519.GF25519.OppExpr.bits GF25519.GF25519.Opp.llProg GF25519.GF25519.OppExpr.hlProg GF25519.GF25519.OppExpr.inputs
-            (*GF25519.GF25519.Freeze.wordProg GF25519.GF25519.FreezeExpr.bits GF25519.GF25519.Freeze.llProg GF25519.GF25519.FreezeExpr.hlProg GF25519.GF25519.FreezeExpr.inputs *)
+            GF25519.GF25519.add GF25519.GF25519.sub GF25519.GF25519.mul GF25519.GF25519.opp (* GF25519.GF25519.freeze *)
             GF25519.GF25519.bits GF25519.GF25519.FE
-            QhasmCommon.liftN QhasmCommon.NArgMap Compile.CompileHL.compile LL.LL.under_lets LL.LL.interp LL.LL.interp_arg LL.LL.match_arg_Prod Conversions.LLConversions.convertZToWord Conversions.LLConversions.convertExpr Conversions.LLConversions.convertArg Conversions.LLConversions.convertVar PhoasCommon.type_rect PhoasCommon.type_rec PhoasCommon.type_ind PhoasCommon.interp_binop LL.LL.uninterp_arg
+            QhasmCommon.liftN QhasmCommon.NArgMap Compile.CompileHL.compile LL.LL.under_lets LL.LL.interp LL.LL.interp_arg LL.LL.match_arg_Prod Conversions.LLConversions.convertExpr Conversions.LLConversions.convertArg Conversions.LLConversions.convertVar PhoasCommon.type_rect PhoasCommon.type_rec PhoasCommon.type_ind PhoasCommon.interp_binop LL.LL.uninterp_arg
             Evaluables.ezero Evaluables.toT Evaluables.fromT Evaluables.eadd Evaluables.esub Evaluables.emul Evaluables.eshiftr Evaluables.eand Evaluables.eltb Evaluables.eeqb
             Evaluables.WordEvaluable Evaluables.ZEvaluable].
 
@@ -73,17 +66,19 @@ Print interp_radd.
 Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
 Definition interp_rsub : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_bexpr rsub.
-(*Print interp_rsub.*)
+Print interp_rsub.
 Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
 Definition interp_rmul : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_bexpr rmul.
-(*Print interp_rmul.*)
+Print interp_rmul.
 Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
 Definition interp_ropp : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_uexpr ropp.
+Print interp_ropp.
 Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
 Definition interp_rfreeze : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.fe25519W
   := Eval asm_interp in interp_uexpr rfreeze.
+Print interp_rfreeze.
 Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl.
 
 Definition interp_rge_modulus : Specific.GF25519BoundedCommonWord.fe25519W -> Specific.GF25519BoundedCommonWord.word64
diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v
index 0a67f1592..e9eecd4c8 100644
--- a/src/Assembly/HL.v
+++ b/src/Assembly/HL.v
@@ -1,7 +1,15 @@
 Require Import Crypto.Assembly.PhoasCommon.
+Require Import Coq.setoid_ring.InitialRing.
 Require Import Crypto.Util.LetIn.
 
 Module HL.
+  Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t.
+  Proof.
+    induction t; [refine (f x)|].
+    destruct x as [x1 x2].
+    refine (IHt1 x1, IHt2 x2).
+  Defined.
+
   Section Language.
     Context {T: Type}.
     Context {E: Evaluable T}.
@@ -10,7 +18,7 @@ Module HL.
         Context {var : type -> Type}.
 
         Inductive expr : type -> Type :=
-          | Const : @interp_type T TT -> expr TT
+          | Const : forall {_ : Evaluable T}, @interp_type T TT -> expr TT
           | Var : forall {t}, var t -> expr t
           | Binop : forall {t1 t2 t3}, binop t1 t2 t3 -> expr t1 -> expr t2 -> expr t3
           | Let : forall {tx}, expr tx -> forall {tC}, (var tx -> expr tC) -> expr tC
@@ -18,13 +26,11 @@ Module HL.
           | MatchPair : forall {t1 t2}, expr (Prod t1 t2) -> forall {tC}, (var t1 -> var t2 -> expr tC) -> expr tC.
     End expr.
 
-    Local Notation ZConst z := (@Const Z ZEvaluable _ z%Z).
+    Local Notation ZConst z := (@Const Z ConstEvaluable _ z%Z).
 
-    Definition Expr t : Type := forall var, @expr var t.
-
-    Fixpoint interp {t} (e: @expr interp_type t) : interp_type t :=
+    Fixpoint interp {t} (e: @expr interp_type t) : @interp_type T t :=
         match e in @expr _ t return interp_type t with
-        | Const n => n
+        | Const _ x => x
         | Var _ n => n
         | Binop _ _ _ op e1 e2 => interp_binop op (interp e1) (interp e2)
         | Let _ ex _ eC => dlet x := interp ex in interp (eC x)
@@ -32,15 +38,10 @@ Module HL.
         | MatchPair _ _ ep _ eC => let (v1, v2) := interp ep in interp (eC v1 v2)
         end.
 
-    Definition Interp {t} (E:Expr t) : interp_type t := interp (E interp_type).
-  End Language.
+    Definition Expr t : Type := forall var, @expr var t.
 
-  Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t.
-  Proof.
-    induction t; [refine (f x)|].
-    destruct x as [x1 x2].
-    refine (IHt1 x1, IHt2 x2).
-  Defined.
+    Definition Interp {t} (e: Expr t) : interp_type t := interp (e interp_type).
+  End Language.
 
   Definition zinterp {t} E := @interp Z ZEvaluable t E.
 
@@ -50,6 +51,8 @@ Module HL.
 
   Definition WordInterp {n t} E := @Interp (word n) (@WordEvaluable n) t E.
 
+  Existing Instance ZEvaluable.
+
   Example example_Expr : Expr TT := fun var => (
     Let (Const 7) (fun a =>
       Let (Let (Binop OPadd (Var a) (Var a)) (fun b => Pair (Var b) (Var b))) (fun p =>
@@ -79,80 +82,85 @@ Module HL.
     | Z.shiftr => constr:(OPshiftr)
     end.
 
-  Class reify {varT} (var:varT) {eT} (e:eT) {T:Type} := Build_reify : T.
+  Class reify (n: nat) {varT} (var:varT) {eT} (e:eT) {T:Type} := Build_reify : T.
   Definition reify_var_for_in_is {T} (x:T) (t:type) {eT} (e:eT) := False.
 
-  Ltac reify var e :=
+  Ltac reify n var e :=
     lazymatch e with
     | let x := ?ex in @?eC x =>
-      let ex := reify var ex in
-      let eC := reify var eC in
-      constr:(Let (T := Z) (var:=var) ex eC)
+      let ex := reify n var ex in
+      let eC := reify n var eC in
+      constr:(Let (T:=Z) (var:=var) ex eC)
     | match ?ep with (v1, v2) => @?eC v1 v2 end =>
-      let ep := reify var ep in
-      let eC := reify var eC in
-      constr:(MatchPair (T := Z) (var:=var) ep eC)
+      let ep := reify n var ep in
+      let eC := reify n var eC in
+      constr:(MatchPair (T:=Z) (var:=var) ep eC)
     | pair ?a ?b =>
-      let a := reify var a in
-      let b := reify var b in
-      constr:(Pair (T := Z) (var:=var) a b)
+      let a := reify n var a in
+      let b := reify n var b in
+      constr:(Pair (T:=Z) (var:=var) a b)
     | ?op ?a ?b =>
       let op := reify_binop op in
-      let b := reify var b in
-      let a := reify var a in
-      constr:(Binop (T := Z) (var:=var) op a b)
+      let b := reify n var b in
+      let a := reify n var a in
+      constr:(Binop (T:=Z) (var:=var) op a b)
     | (fun x : ?T => ?C) =>
       let t := reify_type T in
       (* Work around Coq 8.5 and 8.6 bug *)
       (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *)
       (* Avoid re-binding the Gallina variable referenced by Ltac [x] *)
       (* even if its Gallina name matches a Ltac in this tactic. *)
+      (* [C] here is an open term that references "x" by name *)
       let maybe_x := fresh x in
       let not_x := fresh x in
       lazymatch constr:(fun (x : T) (not_x : var t) (_:reify_var_for_in_is x t not_x) =>
-                          (_ : reify var C)) (* [C] here is an open term that references "x" by name *)
+                          (_ : reify n var C))
       with fun _ v _ => @?C v => C end
     | ?x =>
       lazymatch goal with
       | _:reify_var_for_in_is x ?t ?v |- _ => constr:(@Var Z var t v)
-      | _ => (* let t := match type of x with ?t => reify_type t end in *)
-        constr:(@Const Z var x)
+      | _ => let x' := eval cbv in x in
+        match isZcst x with
+        | true => constr:(@Const Z var (@ConstEvaluable n) x)
+        | false => constr:(@Const Z var InputEvaluable x)
+        end
       end
     end.
-  Hint Extern 0 (reify ?var ?e) => (let e := reify var e in eexact e) : typeclass_instances.
+
+  Hint Extern 0 (reify ?n ?var ?e) => (let e := reify n var e in eexact e) : typeclass_instances.
 
   Ltac Reify e :=
-    lazymatch constr:(fun (var:type->Type) => (_:reify var e)) with
-      (fun var => ?C) => constr:(fun (var:type->Type) => C) (* copy the term but not the type cast *)
+    lazymatch constr:(fun (n: nat) (var:type->Type) => (_:reify n var e)) with
+      (fun n var => ?C) => constr:(fun (n: nat) (var:type->Type) => C) (* copy the term but not the type cast *)
     end.
 
   Definition zinterp_type := @interp_type Z.
   Transparent zinterp_type.
 
-  Goal forall (x : Z) (v : zinterp_type TT) (_:reify_var_for_in_is x TT v), reify(T:=Z) zinterp_type ((fun x => x+x) x)%Z.
+  Goal forall (x : Z) (v : zinterp_type TT) (_:reify_var_for_in_is x TT v), reify (T:=Z) 16 zinterp_type ((fun x => x+x) x)%Z.
     intros.
-    let A := (reify zinterp_type (x + x)%Z) in pose A.
+    let A := (reify 16 zinterp_type (x + x + 1)%Z) in idtac A.
   Abort.
 
   Goal False.
-    let z := reify zinterp_type (let x := 0 in x)%Z in pose z.
+    let z := (reify 16 zinterp_type (let x := 0 in x)%Z) in pose z.
   Abort.
 
   Ltac lhs_of_goal := match goal with |- ?R ?LHS ?RHS => constr:(LHS) end.
   Ltac rhs_of_goal := match goal with |- ?R ?LHS ?RHS => constr:(RHS) end.
 
-  Ltac Reify_rhs :=
+  Ltac Reify_rhs n :=
     let rhs := rhs_of_goal in
     let RHS := Reify rhs in
-    transitivity (ZInterp RHS);
+    transitivity (ZInterp (RHS n));
     [|cbv iota beta delta [ZInterp Interp interp_type interp_binop interp]; reflexivity].
 
   Goal (0 = let x := 1+2 in x*3)%Z.
-    Reify_rhs.
+    Reify_rhs 32.
   Abort.
 
   Goal (0 = let x := 1 in let y := 2 in x * y)%Z.
-    Reify_rhs.
+    Reify_rhs 32.
   Abort.
 
   Section wf.
@@ -160,7 +168,7 @@ Module HL.
 
     Local Notation "x ≡ y" := (existT _ _ (x, y)).
 
-    Definition Texpr var t := @expr T var t.
+    Definition Texpr var t := @expr Z var t.
 
     Inductive wf : list (sigT (fun t => var1 t * var2 t))%type -> forall {t}, Texpr var1 t -> Texpr var2 t -> Prop :=
     | WfConst : forall G n, wf G (Const n) (Const n)
@@ -170,25 +178,25 @@ Module HL.
                   (op: binop t1 t2 t3),
         wf G e1 e1'
         -> wf G e2 e2'
-        -> wf G (Binop (T := T) op e1 e2) (Binop (T := T) op e1' e2')
+        -> wf G (Binop op e1 e2) (Binop op e1' e2')
     | WfLet : forall G t1 t2 e1 e1' (e2 : _ t1 -> Texpr _ t2) e2',
         wf G e1 e1'
         -> (forall x1 x2, wf ((x1 ≡ x2) :: G) (e2 x1) (e2' x2))
-        -> wf G (Let (T := T) e1 e2) (Let (T := T) e1' e2')
+        -> wf G (Let e1 e2) (Let e1' e2')
     | WfPair : forall G {t1} {t2} (e1: Texpr var1 t1) (e2: Texpr var1 t2)
                       (e1': Texpr var2 t1) (e2': Texpr var2 t2),
         wf G e1 e1'
         -> wf G e2 e2'
-        -> wf G (Pair (T := T) e1 e2) (Pair (T := T) e1' e2')
+        -> wf G (Pair e1 e2) (Pair e1' e2')
     | WfMatchPair : forall G t1 t2 tC ep ep' (eC : _ t1 -> _ t2 -> Texpr _ tC) eC',
         wf G ep ep'
         -> (forall x1 x2 y1 y2, wf ((x1 ≡ x2) :: (y1 ≡ y2) :: G) (eC x1 y1) (eC' x2 y2))
-        -> wf G (MatchPair (T := T) ep eC) (MatchPair (T := T) ep' eC').
+        -> wf G (MatchPair ep eC) (MatchPair ep' eC').
   End wf.
 
-  Definition Wf {T: Type} {t} (E : @Expr T t) := forall var1 var2, wf nil (E var1) (E var2).
+  Definition Wf {T: Type} {t} (E : Expr t) := forall var1 var2, wf nil (E var1) (E var2).
 
-  Example example_Expr_Wf : Wf example_Expr.
+  Example example_Expr_Wf : Wf (T := Z) example_Expr.
   Proof.
     unfold Wf; repeat match goal with
     | [ |- wf _ _ _ ] => constructor
diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v
index 9662fcd31..e94933e2c 100644
--- a/src/Assembly/LL.v
+++ b/src/Assembly/LL.v
@@ -1,6 +1,8 @@
 Require Import Crypto.Assembly.PhoasCommon.
 Require Import Crypto.Util.LetIn.
 
+Local Arguments Let_In / _ _ _ _.
+
 Module LL.
   Section Language.
     Context {T: Type}.
@@ -25,6 +27,15 @@ Module LL.
         | Return : forall {t}, arg t -> expr t.
     End expr.
 
+    Definition Expr t := forall var, @expr var t.
+
+    Fixpoint interp_arg' {V t} (f: V -> T) (e: arg t) : interp_type t :=
+      match e with
+      | Pair _ _ x y => (interp_arg' f x, interp_arg' f y)
+      | Const x => x
+      | Var x => f x
+      end.
+
     Fixpoint interp_arg {t} (e: arg t) : interp_type t :=
       match e with
       | Pair _ _ x y => (interp_arg x, interp_arg y)
@@ -32,6 +43,12 @@ Module LL.
       | Var x => x
       end.
 
+    Lemma interp_arg_spec: forall {t} (x: arg t), interp_arg x = interp_arg' id x.
+    Proof.
+      intros; induction x; unfold id in *; simpl; repeat f_equal;
+        first [reflexivity| assumption].
+    Qed.
+
     Fixpoint uninterp_arg {var t} (x: interp_type t) : @arg var t :=
       match t as t' return interp_type t' -> arg t' with
       | Prod t0 t1 => fun x' =>
@@ -41,16 +58,41 @@ Module LL.
       | TT => Const
       end x.
 
+    Fixpoint uninterp_arg_as_var {var t} (x: @interp_type var t) : @arg var t :=
+      match t as t' return @interp_type var t' -> @arg var t' with
+      | Prod t0 t1 => fun x' =>
+        match x' with
+        | (x0, x1) => Pair (uninterp_arg_as_var x0) (uninterp_arg_as_var x1)
+        end
+      | TT => Var
+      end x.
+
+    Fixpoint interp' {V t} (f: V -> T) (e:expr t) : interp_type t :=
+      match e with
+      | LetBinop _ _ _ op a b _ eC =>
+        let x := interp_binop op (interp_arg' f a) (interp_arg' f b) in interp' f (eC (uninterp_arg x))
+      | Return _ a => interp_arg' f a
+      end.
+
     Fixpoint interp {t} (e:expr t) : interp_type t :=
       match e with
       | LetBinop _ _ _ op a b _ eC =>
         dlet x := interp_binop op (interp_arg a) (interp_arg b) in interp (eC (uninterp_arg x))
       | Return _ a => interp_arg a
       end.
+
+    Lemma interp_spec: forall {t} (e: expr t), interp e = interp' id e.
+    Proof.
+      intros; induction e; unfold id in *; simpl; repeat f_equal;
+        try rewrite H; simpl; repeat f_equal;
+        rewrite interp_arg_spec; repeat f_equal.
+    Qed.
   End Language.
 
+  Transparent interp interp_arg.
+
   Example example_expr :
-    (@interp Z ZEvaluable _
+    (@interp Z (ZEvaluable) _
       (LetBinop OPadd (Const 7%Z) (Const 8%Z) (fun v => Return v)) = 15)%Z.
   Proof. reflexivity. Qed.
 
@@ -80,7 +122,7 @@ Module LL.
     Definition match_arg_Prod {var t1 t2} (a:arg T var (Prod t1 t2)) : (arg T var t1 * arg T var t2) :=
       match a with
       | Pair _ _ a1 a2 => (a1, a2)
-      | Var _ | Const _ => I (* dummy value *)
+      | _ => I (* dummy *)
       end.
 
     Global Arguments match_arg_Prod / : simpl nomatch.
@@ -114,7 +156,8 @@ Module LL.
   Proof.
     induction t as [|i0 v0 i1 v1]; simpl; intros; try reflexivity.
     break_match; subst; simpl.
-    rewrite v0, v1; reflexivity.
+    unfold interp_arg in *.
+    simpl; rewrite v0, v1; reflexivity.
   Qed.
 
   Lemma interp_under_lets {T} {_: Evaluable T} {t: type} {tC: type}
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index e7fc23e0a..40d5abca9 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -20,55 +20,101 @@ Module Type Expression.
   Parameter bits: nat.
   Parameter width: Width bits.
   Parameter inputs: nat.
+  Parameter inputBounds: list Z.
   Parameter ResultType: type.
-  Parameter hlProg: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-  Parameter inputBounds: list (Range N).
+
+  Parameter prog: NAry inputs Z (@HL.Expr Z ResultType).
 End Expression.
 
 Module Pipeline (Input: Expression).
-  Export Input.
+  Definition bits := Input.bits.
+  Definition inputs := Input.inputs.
+  Definition ResultType := Input.ResultType.
+
+  Hint Unfold bits inputs ResultType.
+  Definition width: Width bits := Input.width.
+
+  Definition W: Type := word bits.
+  Definition R: Type := option RangeWithValue.
+  Definition B: Type := option (@BoundedWord bits).
+
+  Instance ZEvaluable : Evaluable Z := ZEvaluable.
+  Instance WEvaluable : Evaluable W := @WordEvaluable bits.
+  Instance REvaluable : Evaluable R := @RWVEvaluable bits.
+  Instance BEvaluable : Evaluable B := @BoundedEvaluable bits.
+
+  Existing Instances ZEvaluable WEvaluable REvaluable BEvaluable.
+
+  Module Util.
+    Fixpoint applyProgOn {A B k} (d: A) ins (f: NAry k A B): B :=
+      match k as k' return NAry k' A B -> B with
+      | O => id
+      | S m => fun f' =>
+        match ins with
+        | cons x xs => @applyProgOn A B m d xs (f' x)
+        | nil => @applyProgOn A B m d nil (f' d)
+        end
+      end f.
+  End Util.
+
+  Module HL.
+    Definition progZ: NAry inputs Z (@HL.Expr Z ResultType) :=
+      Input.prog.
+
+    Definition progR: NAry inputs Z (@HL.Expr R ResultType) :=
+      liftN (fun x v => @HLConversions.convertExpr Z R _ _ _ (x v)) Input.prog.
 
-  Definition llProg: NAry inputs Z (@LL.expr Z Z ResultType) :=
-    liftN CompileHL.compile hlProg.
+    Definition progW: NAry inputs Z (@HL.Expr W ResultType) :=
+      liftN (fun x v => @HLConversions.convertExpr Z W _ _ _ (x v)) Input.prog.
+  End HL.
 
-  Definition wordProg: NAry inputs (@CompileLL.WArg bits TT) (@LL.expr _ _ ResultType) :=
-    NArgMap (fun x => Z.of_N (wordToN (LL.interp_arg (t := TT) x))) (
-      liftN (LLConversions.convertZToWord bits) llProg).
+  Module LL.
+    Definition progZ: NAry inputs Z (@LL.expr Z Z ResultType) :=
+      liftN CompileHL.Compile HL.progZ.
 
-  Definition qhasmProg := CompileLL.compile (w := width) wordProg.
+    Definition progR: NAry inputs Z (@LL.expr R R ResultType) :=
+      liftN CompileHL.Compile HL.progR.
 
-  Definition qhasmString : option string :=
-    match qhasmProg with
-    | Some (p, _) => StringConversion.convertProgram p
-    | None => None
-    end.
+    Definition progW: NAry inputs Z (@LL.expr W W ResultType) :=
+      liftN CompileHL.Compile HL.progW.
+  End LL.
 
-  Import LLConversions.
+  Module AST.
+    Definition progZ: NAry inputs Z (@interp_type Z ResultType) :=
+      liftN LL.interp LL.progZ.
 
-  Definition RWV: Type := option RangeWithValue.
+    Definition progR: NAry inputs Z (@interp_type R ResultType) :=
+      liftN LL.interp LL.progR.
 
-  Definition rwvProg: NAry inputs RWV (@LL.expr RWV RWV ResultType) :=
-    NArgMap (fun x => orElse 0%Z (option_map (fun v => Z.of_N (value v)) x) ) (
-      liftN (@convertExpr Z RWV ZEvaluable (RWVEval (n := bits)) _) llProg).
+    Definition progW: NAry inputs Z (@interp_type W ResultType) :=
+      liftN LL.interp LL.progW.
+  End AST.
 
-  Fixpoint applyProgOn {A B k} ins (f: NAry k (option A) B): B :=
-    match k as k' return NAry k' (option A) B -> B with
-    | O => id
-    | S m => fun f' =>
-      match ins with
-      | cons x xs => @applyProgOn A B m xs (f' x)
-      | nil => @applyProgOn A B m nil (f' None)
-      end
-    end f.
+  Module Qhasm.
+    Definition pair :=
+      @CompileLL.compile bits width ResultType _ LL.progW.
 
-  Definition outputBounds :=
-    applyProgOn (map (@Some _) (map from_range inputBounds)) (
-      liftN (fun e => typeMap (option_map proj) (@LL.interp RWV (@RWVEval bits) _ e))
-        rwvProg).
+    Definition prog := option_map (@fst _ _) pair.
 
-  Definition valid :=
-    applyProgOn (map (@Some _) (map from_range inputBounds)) (
-     liftN (@check bits _ RWV (@RWVEval bits)) rwvProg).
+    Definition outputRegisters := option_map (@snd _ _) pair.
+
+    Definition code := option_map StringConversion.convertProgram prog.
+  End Qhasm.
+
+  Module Bounds.
+    Definition input := map (fun x => range N 0%N (Z.to_N x)) Input.inputBounds.
+
+    Definition upper := Z.of_N (wordToN (wones bits)).
+
+    Definition prog :=
+      Util.applyProgOn upper Input.inputBounds LL.progR.
+
+    Definition valid := LLConversions.check (n := bits) (f := id) prog.
+
+    Definition output :=
+      typeMap (option_map (fun x => range N (rwv_low x) (rwv_high x)))
+              (LL.interp prog).
+  End Bounds.
 End Pipeline.
 
 Module SimpleExample.
@@ -80,13 +126,15 @@ Module SimpleExample.
     Definition inputs: nat := 1.
     Definition ResultType := TT.
 
-    Definition hlProg: NAry 1 Z (@HL.expr Z (@LL.arg Z Z) TT) :=
-        Eval vm_compute in (fun x => HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)).
+    Definition inputBounds: list Z := [ (2^30)%Z ].
 
-    Definition inputBounds: list (Range N) := [ range N 0%N (Npow2 31) ].
+    Existing Instance ZEvaluable.
+
+    Definition prog: NAry 1 Z (@HL.Expr Z TT).
+      intros x var.
+      refine (HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)).
+    Defined.
   End SimpleExpression.
 
   Module SimplePipeline := Pipeline SimpleExpression.
-
-  Export SimplePipeline.
 End SimpleExample.
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index 79591d40d..b7dd90da6 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -80,6 +80,12 @@ Section Util.
     end.
 
   Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
+
+  Definition orElse {T} (d: T) (o: option T): T :=
+    match o with
+    | Some v => v
+    | None => d
+    end.
 End Util.
 
 Close Scope nword_scope.
\ No newline at end of file