committing unstable refactors to patch master

9 files changed, 730 insertions, 1358 deletions

diff --git a/src/Assembly/Bounded.v b/src/Assembly/Bounded.v
deleted file mode 100644
index 964f6f810..000000000
--- a/src/Assembly/Bounded.v
+++ /dev/null
@@ -1,732 +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 _ (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.
-
-    (* TODO(rsloan): how do we fix this? *)
-    Unshelve.
-    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.
\ No newline at end of file
diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v
index 53612cfbb..2ff50e0e1 100644
--- a/src/Assembly/Compile.v
+++ b/src/Assembly/Compile.v
@@ -10,31 +10,46 @@ Require Import Crypto.Assembly.QhasmCommon.
 Require Import Crypto.Assembly.Qhasm.
 
 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 {V t} (e:@HL.expr T (@LL.arg T V) t) : @LL.expr T V 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 Expr' t : Type := forall var, @HL.expr T (@LL.arg T var) t.
+
+    Definition Compile {t} (e:@Expr' t) : @LL.Expr T t :=
+        fun var => compile (e var).
+  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.
@@ -69,8 +84,8 @@ Module CompileLL.
   Section Compile.
     Context {n: nat} {w: Width n}.
 
-    Definition WArg t': Type := @LL.arg (word n) (word n) t'.
-    Definition WExpr t': Type := @LL.expr (word n) (word n) t'.
+    Definition WArg t': Type := @LL.arg (word n) Z t'.
+    Definition WExpr t': Type := @LL.expr (word n) Z t'.
 
     Section Mappings.
       Definition indexize (x: nat) : Index n.
@@ -85,7 +100,7 @@ Module CompileLL.
       Definition getMapping (x: WArg TT) :=
         match x with
         | Const v => constM n (@constant n w v)
-        | Var v => regM n (@reg n w (wordToNat v))
+        | Var v => regM n (@reg n w (Z.to_nat v))
         end.
 
       Definition getReg (x: Mapping n): option (Reg n) :=
@@ -188,7 +203,7 @@ Module CompileLL.
       match t as t' return WArg t' -> list nat with
       | TT => fun a' =>
         match a' with
-        | Var v' => [wordToNat v']
+        | Var v' => [Z.to_nat v']
         | _ => @nil nat
         end
       | Prod t0 t1 => fun a' =>
@@ -239,7 +254,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 (Z.of_nat r)
                     | _ => zeros _
                     end in
 
@@ -266,13 +281,13 @@ 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.
 
-    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 593aa06a4..436a6639b 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -61,25 +61,12 @@ Module HLConversions.
         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.
+    @convertExpr Z (word n) (@ZEvaluable n) (@WordEvaluable n) t v a.
 
   Definition convertZToBounded {t} n v a :=
     @convertExpr Z (option (@BoundedWord n))
-                 ZEvaluable (@BoundedEvaluable n) t v a.
+                 (@ZEvaluable n) (@BoundedEvaluable n) t v a.
 
   Definition ZToWord {t} n (a: @Expr Z t): @Expr (word n) t :=
     fun v => convertZToWord n v (a v).
@@ -97,316 +84,130 @@ Module HLConversions.
           Binop OPadd (Var x) (Var y)))))%Z.
 
   Example interp_example_range :
-    option_map high (BInterp (ZToRange 32 example_Expr)) = Some 28%N.
+    option_map bw_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].
+  Section VarConv.
+    Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}.
 
-    - 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 [_ _ _ _ _ _].
-
-  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.
+  End ArgConv.
 
-    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.
+  Section ExprConv.
+    Context {A B: Type} {EA: Evaluable A} {EB: Evaluable B}.
 
-    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.
+    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 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.
+        | Return _ a => Return (convertArg _ a)
+        end.
+  End ExprConv.
 
-    Lemma just_zero: forall n, exists x, just (n := n) 0 = Some x.
-    Proof.
-    Admitted.
+  Section Defaults.
+    Context {t: type} {n: nat}.
 
-    (* Main correctness guarantee *)
+    Definition Word := word n.
+    Definition Bounded := option (@BoundedWord n).
+    Definition RWV := option (RangeWithValue).
 
-    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.
+    Transparent Word Bounded RWV.
 
-      induction E as [tx ty tz op x y z|]; simpl; try reflexivity.
+    Instance RWVEvaluable' : Evaluable RWV := @RWVEvaluable n.
+    Instance ZEvaluable' : Evaluable Z := @ZEvaluable n.
 
-      - repeat rewrite convertArg_var in *.
-        repeat rewrite convertArg_interp in *.
+    Existing Instance ZEvaluable'.
+    Existing Instance WordEvaluable.
+    Existing Instance BoundedEvaluable.
+    Existing Instance RWVEvaluable'.
 
-        rewrite H; clear H; repeat f_equal.
+    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 (ZToWord_binop_correct (n := n) op x y) as C;
-            unfold zOp, wOp, varWordToZ, varZToWord in C;
-            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.
 
-          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 varWordToZ a := @convertVar Word Z _ _ t a.
+    Definition varBoundedToZ a := @convertVar Bounded Z _ _ t a.
+    Definition varRWVToZ a := @convertVar RWV Z _ _ t a.
 
-        + unfold bcheck, getBounds in *; simpl in *.
-          replace (interp_binop op _ _)
-             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 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.
 
-          pose proof (ZToBounded_binop_correct (n := n) op x y) as C;
-            unfold boundedArg, zOp, wOp, varZToBounded,
-                   varBoundedToZ, convertZToBounded in *;
-            simpl in C.
+    Section Operations.
+      Context {tx ty tz: type}.
 
-          repeat rewrite convertArg_interp; symmetry.
+      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.
 
-          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 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.
 
-      - simpl in S.
-        induction a as [| |t0 t1 a0 IHa0 a1 IHa1]; simpl in *; try reflexivity.
-        apply andb_true_iff in S; destruct S; rewrite IHa0, IHa1; try reflexivity; assumption.
-    Qed.
-  End Correctness.
-
-  Section FastCorrect.
-    Context {n: nat}.
-
-    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 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.
 
-    Instance RWVEval : Evaluable (option RangeWithValue) := {
-      ezero := None;
+      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.
+  End Defaults.
 
-      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;
-
-      fromT := fun x => orElse 0%Z (option_map Z.of_N (option_map value x));
-
-      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;
-    }.
+  Section Correctness.
+    Context {n: nat}.
 
-    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).
+    Definition W := (word n).
+    Definition B := (@Bounded n).
+    Definition R := (option RangeWithValue).
 
-    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).
+    Instance RE : Evaluable R := @RWVEvaluable n.
+    Instance ZE : Evaluable Z := @ZEvaluable n.
+    Instance WE : Evaluable W := @WordEvaluable n.
+    Instance BE : Evaluable B := @BoundedEvaluable n.
 
-    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.
+    Transparent ZE RE WE BE W B R.
 
-    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
@@ -414,68 +215,297 @@ 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}.
+
+      Definition boundVarInterp := fun x => bwFromRWV (n := n) (rwv 0%N (Z.to_N x) (Z.to_N x)).
+
+      Definition getBounds {t} (e : @expr T Z t): @interp_type B t :=
+        interp' boundVarInterp (@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,
+          bcheck (t := tz) (LetBinop op x y e) = true
+        -> opZ (n := n) op (interp_arg x) (interp_arg y) =
+          varBoundedToZ (n := n) (opBounded op
+             (interp_arg' boundVarInterp (convertArg _ x))
+             (interp_arg' boundVarInterp (convertArg _ y))).
+      Proof.
+      Admitted.
+
+      Lemma ZToWord_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e,
+          bcheck (t := tz) (LetBinop op x y e) = true
+        -> opZ (n := n) 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;
+          kill_dec; simpl; kill_dec; 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 t),
+          bcheck (@convertExpr Z R _ _ _ _ E) = true
+        -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp (n := n) 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 _ _)
+                with (varBoundedToZ (n := n) (opBounded op
+                        (interp_arg' boundVarInterp (convertArg _ x))
+                        (interp_arg' boundVarInterp (convertArg _ y)))).
+
+            * rewrite <- S; f_equal; clear S.
+              simpl; repeat f_equal.
+              unfold varBoundedToZ, opBounded.
+              repeat rewrite convertArg_var.
+              Arguments convertArg _ _ _ _ _ _ _ : clear implicits.
+              rewrite double_conv_var.
+              repeat rewrite double_conv_arg.
+              reflexivity.
+
+            * pose proof (ZToBounded_binop_correct op x y) as C;
+                unfold opZ, opWord, varZToBounded,
+                    varBoundedToZ in *;
+                simpl in C.
+
+              Local Opaque boundVarInterp toT fromT.
+
+              induction op; rewrite (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 boundVarInterp 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.
+      Definition rangeOf := fun x =>
+        Some (rwv 0%N (Z.to_N x) (Z.to_N x)).
+
+      Definition getRWV {t} (e : @expr R Z t): @interp_type R t :=
+        interp' rangeOf e.
+
+      Definition getRanges {t} (e : @expr R Z t): @interp_type (option (Range N)) t :=
+        typeMap (option_map rwvToRange) (getRWV e).
+
+      Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) :=
+        match t as t' return (interp_type t') -> bool with
+        | TT => fun x' =>
+            match omap x' (bwFromRWV (n := n)) 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} (e : @expr R Z t): bool := check' (getRWV e).
+
+      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' boundVarInterp (convertArg TT x)) (fun X =>
+            omap (interp_arg' boundVarInterp (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 R Z t), check E = true -> bcheck 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 *.
+
+          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.
+
+          induction op; rewrite check_spec'; reflexivity.
+
+        - unfold bcheck, getBounds, check, getRWV in *.
+
+          induction a as [a|a|t0 t1 a0 IHa0 a1 IHa1].
+
+          + induction a as [a|]; [| inversion H]; simpl in *.
+
+            assert (Z : (exists a', bwFromRWV (n := n) a = Some a')
+                  \/ bwFromRWV (n := n) a = None) by (
+              destruct (bwFromRWV a);
+              [left; eexists; reflexivity | right; reflexivity]).
+
+            destruct Z as [aSome|aNone]; [destruct aSome as [a' aSome] |].
+
+            * rewrite aSome; simpl; rewrite aSome; reflexivity.
+            * rewrite aNone in H; inversion H.
+
+          + unfold boundVarInterp, rangeOf in *.
+            simpl in *; kill_dec; try reflexivity; try inversion H.
+
+          + simpl in *; rewrite IHa0, IHa1; simpl; [reflexivity | | ];
+              apply andb_true_iff in H; destruct H as [H1 H2];
+              assumption.
+      Qed.
+
+      Lemma RangeInterp_spec: forall {t} (E: expr t),
+          check (convertExpr E) = true
+        -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp (n := n) E)
+            = wordInterp (ZToWord _ E).
+      Proof.
+        intros.
+        apply RangeInterp_bounded_spec.
+        apply check_spec.
+        assumption.
+      Qed.
+    End RWVSpec.
+  End Correctness.
 End LLConversions.
 
 Section ConversionTest.
@@ -492,22 +522,22 @@ Section ConversionTest.
 
   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))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 0 testCase))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 1 testCase))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 10 testCase))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 32 testCase))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 64 testCase))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (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))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 0 nefarious))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 1 nefarious))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 4 nefarious))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 5 nefarious))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 32 nefarious))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 64 nefarious))).
+  Eval vm_compute in (typeMap (option_map bwToRange) (BInterp (ZToRange 128 nefarious))).
 End ConversionTest.
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v
index c22709331..0b19b5237 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,16 @@ 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 =>
+      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;
@@ -47,7 +71,6 @@ Section Z.
     eltb    := Z.ltb;
     eeqb    := Z.eqb;
   }.
-
 End Z.
 
 Section Word.
@@ -57,8 +80,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 +99,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 +485,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 +498,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 +524,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 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;
 
-  Definition toRange (w: BoundedWord): Range N :=
-    range N (low w) (high w).
+      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]);
+
+      [reflexivity| etransitivity; apply N.ge_le; eassumption].
+  Defined.
 
-  Definition fromRange (r: Range N): option (BoundedWord).
+  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 +576,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 +609,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 +639,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 +653,82 @@ 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.
 
-End BoundedWord.
\ No newline at end of file
+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).
+
+  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 (omap x (bwFromRWV (n := n))) (fun _ => x);
+
+    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.
\ No newline at end of file
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 80d9044c4..a21b54cf0 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -9,6 +9,9 @@ Module GF25519.
   Definition bits: nat := 64.
   Definition width: Width bits := W64.
 
+  Instance ZE : Evaluable Z := @ZEvaluable bits.
+  Existing Instance ZE.
+
   Fixpoint makeBoundList {n} k (b: @BoundedWord n) :=
     match k with
     | O => nil
@@ -17,9 +20,9 @@ Module GF25519.
 
   Section DefaultBounds.
     Import ListNotations.
-    Local Notation rr exp := (range N 0%N (2^exp + 2^exp/10)%N).
+    Local Notation rr exp := (2^exp + 2^exp/10)%Z.
 
-    Definition feBound: list (Range N) :=
+    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.
@@ -45,8 +48,7 @@ Module GF25519.
         Eval cbv beta delta [fe25519 add mul sub Let_In] in 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 }.
+        { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_add_expr P Q }.
     Proof.
       vm_compute in P, Q; repeat
         match goal with
@@ -63,8 +65,7 @@ Module GF25519.
 
       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|].
+      transitivity (HL.interp (t := ResultType) X); [reflexivity|].
 
       cbv iota beta delta [
             interp_type interp_binop HL.interp
@@ -75,124 +76,10 @@ Module GF25519.
     Definition ge25519_add (P Q: @interp_type Z ResultType) :=
         proj1_sig (ge25519_add' P Q).
 
-    Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
+    Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
         liftFE (fun p => (liftFE (fun q => ge25519_add 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 hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
-      Eval vm_compute in hlProg'.
   End AddExpr.
 
-  Module SubExpr <: Expression.
-    Definition bits: nat := bits.
-    Definition inputs: nat := 20.
-    Definition width: Width bits := width.
-    Definition ResultType := FE.
-    Definition inputBounds := feBound ++ feBound.
-
-    Definition ge25519_sub_expr :=
-        Eval cbv beta delta [fe25519 add mul sub Let_In] in sub.
-
-    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 }.
-    Proof.
-      vm_compute in P, Q; repeat
-        match goal with
-        | [x:?T |- _] =>
-          lazymatch T with
-          | Z => fail
-          | prod _ _ => destruct x
-          | _ => clear x
-          end
-        end.
-
-      eexists.
-      cbv beta delta [ge25519_sub_expr].
-
-      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|].
-
-      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 hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        liftFE (fun p => (liftFE (fun q => 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 hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
-      Eval vm_compute in hlProg'.
-  End SubExpr.
-
-  Module MulExpr <: Expression.
-    Definition bits: nat := bits.
-    Definition inputs: nat := 20.
-    Definition width: Width bits := width.
-    Definition ResultType := FE.
-    Definition inputBounds := feBound ++ feBound.
-
-    Definition ge25519_mul_expr :=
-        Eval cbv beta delta [fe25519 add mul sub Let_In] in mul.
-
-    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 }.
-    Proof.
-      vm_compute in P, Q; repeat
-        match goal with
-        | [x:?T |- _] =>
-          lazymatch T with
-          | Z => fail
-          | prod _ _ => destruct x
-          | _ => clear x
-          end
-      end.
-
-      eexists.
-      cbv beta delta [ge25519_mul_expr].
-
-      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|].
-
-      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 hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        liftFE (fun p => (liftFE (fun q => ge25519_mul 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 hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
-      Eval vm_compute in hlProg'.
-  End MulExpr.
-
   Module OppExpr <: Expression.
     Definition bits: nat := bits.
     Definition inputs: nat := 10.
@@ -205,7 +92,7 @@ Module GF25519.
 
     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 }.
+        | HL.interp (E := @ZEvaluable bits) (t := FE) r = ge25519_opp_expr P }.
     Proof.
       vm_compute in P; repeat
         match goal with
@@ -222,7 +109,7 @@ Module GF25519.
 
       let R := HL.rhs_of_goal in
       let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X);
+      transitivity (HL.interp (E := @ZEvaluable bits) (t := ResultType) X);
         [reflexivity|].
 
       cbv iota beta delta [
@@ -234,25 +121,41 @@ Module GF25519.
     Definition ge25519_opp (P: @interp_type Z ResultType) :=
         proj1_sig (ge25519_opp' P).
 
-    Definition hlProg'': NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) :=
+    Definition hlProg: NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) :=
         liftFE (fun p => ge25519_opp p).
-
-    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.
-
-    Definition hlProg: NAry 10 Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
-      Eval vm_compute in hlProg'.
   End OppExpr.
 
   Module Add := Pipeline AddExpr.
-  Module Sub := Pipeline SubExpr.
-  Module Mul := Pipeline MulExpr.
   Module Opp := Pipeline OppExpr.
+
+  Section Operations.
+    Definition wfe: Type := @interp_type (word bits) FE.
+
+    Definition ExprBinOp : Type := NAry 20 Z (@CompileLL.WExpr bits FE).
+    Definition ExprUnOp : Type := NAry 10 Z (@CompileLL.WExpr bits FE).
+
+    Existing Instance WordEvaluable.
+
+    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 (fun v => Z.of_N (@wordToN bits v)) 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.
+
+    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 (fun v => Z.of_N (@wordToN bits v)) 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 ropp : ExprUnOp := Opp.wordProg.
+  End Operations.
 End GF25519.
 
 Extraction "GF25519Add" GF25519.Add.
 Extraction "GF25519Sub" GF25519.Sub.
 Extraction "GF25519Mul" GF25519.Mul.
-Extraction "GF25519Opp" GF25519.Opp.
\ No newline at end of file
+Extraction "GF25519Opp" GF25519.Opp.
+
diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v
index 264cd0351..14ca2edca 100644
--- a/src/Assembly/HL.v
+++ b/src/Assembly/HL.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Assembly.PhoasCommon.
+Require Import Coq.setoid_ring.InitialRing.
 
 Module HL.
   Section Language.
@@ -41,9 +42,9 @@ Module HL.
     refine (IHt1 x1, IHt2 x2).
   Defined.
 
-  Definition zinterp {t} E := @interp Z ZEvaluable t E.
+  Definition zinterp {n t} E := @interp Z (@ZEvaluable n) t E.
 
-  Definition ZInterp {t} E := @Interp Z ZEvaluable t E.
+  Definition ZInterp {n t} E := @Interp Z (@ZEvaluable n) t E.
 
   Definition wordInterp {n t} E := @interp (word n) (@WordEvaluable n) t E.
 
@@ -55,7 +56,7 @@ Module HL.
         MatchPair (Var p) (fun x y =>
           Binop OPadd (Var x) (Var y)))))%Z.
 
-  Example interp_example_Expr : ZInterp example_Expr = 28%Z.
+  Example interp_example_Expr : ZInterp (n := 16) example_Expr = 28%Z.
   Proof. reflexivity. Qed.
 
   (* Reification assumes the argument type is Z *)
@@ -114,10 +115,15 @@ Module HL.
     | ?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 x)
+        | false => constr:(@Var Z var TT x)
+        end
       end
     end.
+
   Hint Extern 0 (reify ?var ?e) => (let e := reify var e in eexact e) : typeclass_instances.
 
   Ltac Reify e :=
@@ -130,7 +136,7 @@ Module HL.
 
   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.
     intros.
-    let A := (reify zinterp_type (x + x)%Z) in pose A.
+    let A := (reify zinterp_type (x + x + 1)%Z) in pose A.
   Abort.
 
   Goal False.
@@ -140,18 +146,18 @@ Module HL.
   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 (n := n) RHS);
     [|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.
diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v
index 92f07832f..e08b752fe 100644
--- a/src/Assembly/LL.v
+++ b/src/Assembly/LL.v
@@ -24,6 +24,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)
@@ -31,6 +40,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' =>
@@ -40,16 +55,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 =>
         let 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 (n := 32)) _
       (LetBinop OPadd (Const 7%Z) (Const 8%Z) (fun v => Return v)) = 15)%Z.
   Proof. reflexivity. Qed.
 
@@ -112,7 +152,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 *.
+    cbn; 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..31988ab10 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -21,19 +21,34 @@ Module Type Expression.
   Parameter width: Width bits.
   Parameter inputs: nat.
   Parameter ResultType: type.
-  Parameter hlProg: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-  Parameter inputBounds: list (Range N).
+  Parameter hlProg: NAry inputs Z (@HL.expr Z (@interp_type Z) ResultType).
+  Parameter inputBounds: list Z.
 End Expression.
 
 Module Pipeline (Input: Expression).
   Export Input.
 
+  Module Util.
+    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.
+  End Util.
+
+  Definition hlProg': NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType) :=
+    liftN (HLConversions.mapVar (fun t => @LL.uninterp_arg_as_var _ _ t)
+                                (fun t => @LL.interp_arg _ t)) hlProg.
+
   Definition llProg: NAry inputs Z (@LL.expr Z Z ResultType) :=
-    liftN CompileHL.compile hlProg.
+    liftN CompileHL.compile hlProg'.
 
-  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).
+  Definition wordProg: NAry inputs Z (@CompileLL.WExpr bits ResultType) :=
+    liftN (LLConversions.ZToWord (n := bits) Z) llProg.
 
   Definition qhasmProg := CompileLL.compile (w := width) wordProg.
 
@@ -47,28 +62,22 @@ Module Pipeline (Input: Expression).
 
   Definition RWV: Type := option RangeWithValue.
 
-  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).
+  Instance RWVEvaluable : Evaluable RWV := @RWVEvaluable bits.
+
+  Existing Instance RWVEvaluable.
 
-  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.
+  Definition rwvProg: @LL.expr RWV Z ResultType :=
+    Util.applyProgOn (map (@Some _) inputBounds) (
+      NArgMap (orElse 0%Z) (
+        liftN (@convertExpr Z RWV (@ZEvaluable bits) _ _ _)
+          llProg)).
 
   Definition outputBounds :=
-    applyProgOn (map (@Some _) (map from_range inputBounds)) (
-      liftN (fun e => typeMap (option_map proj) (@LL.interp RWV (@RWVEval bits) _ e))
-        rwvProg).
+    typeMap (option_map rwvToRange) (
+      LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) (
+        rwvProg)).
 
-  Definition valid :=
-    applyProgOn (map (@Some _) (map from_range inputBounds)) (
-     liftN (@check bits _ RWV (@RWVEval bits)) rwvProg).
+  Definition valid := check (n := bits) rwvProg.
 End Pipeline.
 
 Module SimpleExample.
@@ -80,10 +89,10 @@ 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 hlProg: NAry 1 Z (@HL.expr Z (@interp_type Z) TT) :=
+      Eval vm_compute in (fun x => HL.Binop OPadd (HL.Var x) (HL.Const 5%Z)).
 
-    Definition inputBounds: list (Range N) := [ range N 0%N (Npow2 31) ].
+    Definition inputBounds: list Z := [ (2^30)%Z ].
   End SimpleExpression.
 
   Module SimplePipeline := Pipeline SimpleExpression.
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