Fast bounds-checking machinery but lower-bounds are broken

4 files changed, 373 insertions, 173 deletions

diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v
index 368cf8fd1..593aa06a4 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -16,6 +16,8 @@ Require Import Coq.ZArith.Znat.
 
 Require Import Coq.NArith.Nnat Coq.NArith.Ndigits.
 
+Require Import Coq.Bool.Sumbool.
+
 Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t.
 Proof.
   induction t; [refine (f x)|].
@@ -96,7 +98,7 @@ Module HLConversions.
 
   Example interp_example_range :
     option_map high (BInterp (ZToRange 32 example_Expr)) = Some 28%N.
-  Proof. reflexivity. Qed.
+  Proof. cbv; reflexivity. Qed.
 End HLConversions.
 
 Module LLConversions.
@@ -144,7 +146,7 @@ Module LLConversions.
 
   Definition wordInterp {n t} E := @interp (word n) (@WordEvaluable n) t E.
 
-  Definition rangeInterp {n t} E: @interp_type (option (@BoundedWord n)) t :=
+  Definition boundedInterp {n t} E: @interp_type (option (@BoundedWord n)) t :=
     @interp (option (@BoundedWord n)) (@BoundedEvaluable n) t E.
 
   Section Correctness.
@@ -179,28 +181,25 @@ Module LLConversions.
 
     Definition wordArg {n t} (x: @arg (word n) (word n) t) := @interp_arg _ _ x.
 
-    (* Bounds-checking fixpoint *)
+    (* BoundedWord-based Bounds-checking fixpoint *)
+
+    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).
 
-    Fixpoint checkVar {n t} (x: @interp_type (option (@BoundedWord n)) t) :=
+    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
+        match x' with
         | Some _ => true
         | None => false
         end
       | Prod t0 t1 => fun x' =>
         match x' with
-        | (x0, x1) => andb (checkVar (n := n) x0) (checkVar (n := n) x1)
+        | (x0, x1) => andb (bcheck' x0) (bcheck' x1)
         end
       end x.
 
-    Fixpoint check {n t} (e : @expr (option (@BoundedWord n)) (option (@BoundedWord n)) t): bool :=
-      match e with
-      | LetBinop ta tb tc op a b _ eC =>
-        andb (@checkVar n tc (bOp op (interp_arg a) (interp_arg b)))
-             (check (eC (uninterp_arg (bOp op (interp_arg a) (interp_arg b)))))
-      | Return _ a => checkVar (interp_arg a)
-      end.
+    Definition bcheck {n t} T (E: Evaluable T) (e : @expr T T t): bool := bcheck' (n := n) (getBounds T E e).
 
     (* Utility Lemmas *)
 
@@ -223,53 +222,69 @@ Module LLConversions.
         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.
+
     Lemma ZToBounded_binop_correct : forall {n tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e,
-        check (t := tz) (convertZToBounded n (LetBinop op x y e)) = true
+        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.
-      intros until e; intro S; simpl in S; apply andb_true_iff in S; destruct S as [S0 S1].
     Admitted.
 
     Lemma ZToWord_binop_correct : forall {n tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e,
-        check (t := tz) (convertZToBounded n (LetBinop op x y e)) = true
+        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.
-      intros until e; intro S; simpl in S; apply andb_true_iff in S; destruct S as [S0 S1].
     Admitted.
 
-    Lemma check_zero: forall {n}, @check n TT (@convertExpr Z _ ZEvaluable (@BoundedEvaluable n) TT (Return (Const 0%Z))) = true.
+    Lemma just_zero: forall n, exists x, just (n := n) 0 = Some x.
     Proof.
-      intros; simpl; unfold make; simpl.
-
-      repeat match goal with
-      | [|- context[Nge_dec ?A ?B] ] => destruct (Nge_dec A B)
-      end; simpl; unfold id in *; intuition; try nomega.
-
-      rewrite wzero'_def in *.
-      rewrite <- NToWord_zero in *.
-      rewrite wordToN_NToWord in *; try apply Npow2_gt0.
-      nomega.
-    Qed.
+    Admitted.
 
     (* Main correctness guarantee *)
 
-    Lemma RangeInterp_correct: forall {n t} (E: expr t),
-        check (convertZToBounded n E) = true
+    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 rangeInterp, convertZToBounded, zinterp,
-             convertZToWord, wordInterp.
+      unfold convertZToBounded, zinterp, convertZToWord, wordInterp.
 
       induction E as [tx ty tz op x y z|]; simpl; try reflexivity.
 
       - repeat rewrite convertArg_var in *.
         repeat rewrite convertArg_interp in *.
 
-        simpl in S; apply andb_true_iff in S; destruct S as [S0 S1].
-
         rewrite H; clear H; repeat f_equal.
 
         + pose proof (ZToWord_binop_correct (n := n) op x y) as C;
@@ -277,15 +292,15 @@ Module LLConversions.
             simpl in C.
 
           induction op; apply (C (fun _ => Return (Const 0%Z))); clear C;
-            try apply andb_true_iff; split;
-            try apply check_zero;
-            assumption.
+            unfold bcheck, getBounds; simpl;
+            destruct (@just_zero n) as [j p]; rewrite p; reflexivity.
 
-        + replace (interp_binop op _ _)
-             with (varBoundedToZ (bOp op
+        + 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 | clear S1].
+            [unfold varBoundedToZ, boundedArg; rewrite <- convertArg_var; assumption |].
 
           pose proof (ZToBounded_binop_correct (n := n) op x y) as C;
             unfold boundedArg, zOp, wOp, varZToBounded,
@@ -295,17 +310,172 @@ Module LLConversions.
           repeat rewrite convertArg_interp; symmetry.
 
           induction op; apply (C (fun _ => Return (Const 0%Z))); clear C;
-            try apply andb_true_iff; repeat split;
-            try apply check_zero;
-            repeat rewrite convertArg_interp in S0;
-            repeat rewrite convertArg_interp;
-            assumption.
+            unfold bcheck, getBounds; simpl;
+            destruct (@just_zero n) as [j p]; rewrite p; reflexivity.
 
       - 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.
+
+    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;
+
+      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;
+    }.
+
+    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 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).
+
+    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).
+
+    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 {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.
 End LLConversions.
 
 Section ConversionTest.
@@ -322,24 +492,22 @@ Section ConversionTest.
 
   Definition testCase := Eval vm_compute in KeepAddingOne 4000.
 
-  (* Test Cases
-  Eval vm_compute in BInterp (ZToRange 0 testCase).
-  Eval vm_compute in BInterp (ZToRange 1 testCase).
-  Eval vm_compute in BInterp (ZToRange 10 testCase).
-  Eval vm_compute in BInterp (ZToRange 32 testCase).
-  Eval vm_compute in BInterp (ZToRange 64 testCase).
-  Eval vm_compute in BInterp (ZToRange 128 testCase). *)
+  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)).
 
-  (* Test Cases
-  Eval vm_compute in BInterp (ZToRange 0 nefarious).
-  Eval vm_compute in BInterp (ZToRange 1 nefarious).
-  Eval vm_compute in BInterp (ZToRange 4 nefarious).
-  Eval vm_compute in BInterp (ZToRange 5 nefarious).
-  Eval vm_compute in BInterp (ZToRange 32 nefarious).
-  Eval vm_compute in BInterp (ZToRange 64 nefarious).
-  Eval vm_compute in BInterp (ZToRange 128 nefarious). *)
+  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 5bfc88a4d..c22709331 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -33,8 +33,8 @@ Section Z.
     ezero := 0%Z;
 
     (* Conversions *)
-    toT     := id;
-    fromT   := id;
+    toT     := fun x => x;
+    fromT   := fun x => x;
 
     (* Operations *)
     eadd    := Z.add;
@@ -474,65 +474,132 @@ Section BoundedWord.
     high_bound: (high < Npow2 n)%N;
   }.
 
-  Definition make (l: N) (v: word n) (h: N): option (BoundedWord).
+  Definition bapp {rangeF wordF}
+      (op: @validBinaryWordOp n rangeF wordF)
+      (X Y: BoundedWord): option BoundedWord.
+
+    refine (
+      let op' := op _ _ _ _ _ _
+        (ge_low X) (le_high X) (high_bound X)
+        (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
+
+      match result as r' return result = r' -> _ with
+      | Some (range low high) => fun e =>
+        Some (bounded low (wordF (value X) (value Y)) high _ _ _)
+      | None => fun _ => None
+      end eq_refl); abstract (
+
+      pose proof op' as p; clear op';
+      unfold result in *;
+      rewrite e in p;
+      destruct p as [p0 p1]; destruct p1 as [p1 p2];
+      assumption).
+  Defined.
+
+  Definition rapp {rangeF wordF}
+      (op: @validBinaryWordOp n rangeF wordF)
+      (X Y: Range N): option (Range N) :=
+    rangeF X Y.
+
+  Definition vapp {rangeF wordF}
+      (op: @validBinaryWordOp n rangeF wordF)
+      (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 toRange (w: BoundedWord): Range N :=
+    range N (low w) (high w).
+
+  Definition fromRange (r: Range N): option (BoundedWord).
     refine
-      match (Nge_dec (wordToN v) l,
-             Nge_dec h (wordToN v),
-             Nge_dec (N.pred (Npow2 n)) h) with
-      | (left p0, left p1, left p2) => Some (bounded l v h _ _ _)
-      | _ => None
-      end; try (apply N.ge_le; assumption); abstract (
-        apply N.ge_le in p2;
-        apply (N.lt_le_trans _ (N.succ h) _); [nomega|];
-        rewrite <- (N.pred_succ h) in p2;
-        apply -> N.le_pred_le_succ in p2;
-        rewrite N.succ_pred in p2; [assumption |];
+      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 _ _ _)
+        | _ => None
+        end
+      end; try rewrite wordToN_NToWord;
+
+      assert (N.succ h <= Npow2 n)%N by abstract (
+        apply N.ge_le in p1;
+        rewrite <- (N.pred_succ h) in p1;
+        apply -> N.le_pred_le_succ in p1;
+        rewrite N.succ_pred in p1; [assumption |];
         apply N.neq_0_lt_0;
-        apply Npow2_gt0).
+        apply Npow2_gt0);
+
+      try abstract (apply (N.lt_le_trans _ (N.succ h) _);
+        [nomega|assumption]);
+
+      [reflexivity|apply N.ge_le; assumption].
+
+  Defined.
+
+  Definition just (x: N): option (BoundedWord).
+    refine
+      match Nge_dec (N.pred (Npow2 n)) x with
+      | left p => Some (bounded x (NToWord n x) x _ _ _)
+      | right _ => None
+      end; try rewrite wordToN_NToWord; try reflexivity;
+
+    assert (N.succ x <= Npow2 n)%N by abstract (
+        apply N.ge_le in p;
+        rewrite <- (N.pred_succ x) in p;
+        apply -> N.le_pred_le_succ in p;
+        rewrite N.succ_pred in p; [assumption |];
+        apply N.neq_0_lt_0;
+        apply Npow2_gt0);
+
+    try abstract (
+      apply (N.lt_le_trans _ (N.succ x) _);
+        [nomega|assumption]).
   Defined.
 
-  Lemma make_low_spec: forall l v h b, make l v h = Some b -> low b = l.
+  Lemma just_None_spec: forall x, just x = None -> (x >= Npow2 n)%N.
   Proof.
-    intros l v h b H; unfold make in H; simpl;
-      repeat destruct (Nge_dec _ _); inversion_clear H;
-      simpl; reflexivity.
+    intros x H; unfold just in *.
+    destruct (Nge_dec (N.pred (Npow2 n)) x) as [p|p]; [inversion H |].
+    rewrite <- (N.pred_succ x) in p.
+    apply N.lt_pred_lt_succ in p.
+    rewrite N.succ_pred in p; [|apply N.neq_0_lt_0; nomega].
+    apply N.le_succ_l in p.
+    apply N.le_ge; apply N.succ_le_mono; assumption.
   Qed.
-  
-  Lemma make_value_spec: forall l v h b, make l v h = Some b -> value b = v.
+
+  Lemma just_value_spec: forall x b, just x = Some b -> value b = NToWord n x.
   Proof.
-    intros l v h b H; unfold make in H; simpl;
-      repeat destruct (Nge_dec _ _); inversion_clear H;
-      simpl; reflexivity.
+    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 make_high_spec: forall l v h b, make l v h = Some b -> high b = h.
+  Lemma just_low_spec: forall x b, just x = Some b -> low b = x.
   Proof.
-    intros l v h b H; unfold make in H; simpl;
-      repeat destruct (Nge_dec _ _); inversion_clear H;
-      simpl; reflexivity.
+    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 bapp {rangeF wordF}
-      (op: @validBinaryWordOp n rangeF wordF)
-      (X Y: BoundedWord): option BoundedWord.
-
-    refine (
-      match (rangeF (range N (low X) (high X))
-                    (range N (low Y) (high Y))) as r'
-          return _ = r' -> _ with
-      | Some (range low high) => fun _ =>
-        Some (bounded low (wordF (value X) (value Y)) high _ _ _)
-      | _ => fun _ => None
-      end eq_refl);
 
-      pose proof (op _ _ _ _ _ _
-            (ge_low X) (le_high X) (high_bound X)
-            (ge_low Y) (le_high Y) (high_bound Y)) as p';
-
-      rewrite e in p';
-      destruct p' as [p0 p1]; destruct p1 as [p1 p2];
-      assumption.
-  Defined.
+  Lemma just_high_spec: forall x b, just x = Some b -> 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)) _ _ _);
@@ -552,7 +619,7 @@ Section BoundedWord.
   Instance BoundedEvaluable : Evaluable (option BoundedWord) := {
     ezero := Some any;
 
-    toT := fun x => make (Z.to_N x) (NToWord _ (Z.to_N x)) (Z.to_N x);
+    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);
 
     eadd := fun x y => omap x (fun X => omap y (fun Y => bapp range_add_valid X Y));
@@ -570,43 +637,4 @@ Section BoundedWord.
         Some (andb (N.eqb (low X) (low Y)) (N.eqb (high X) (high Y))))))
   }.
 
-End BoundedWord.
-
-Section Range.
-  Context {n: nat}.
-
-  Definition rapp {f g} (op: @validBinaryWordOp n f g) (x y: Range N):
-      option (Range N) := f x y.
-
-  Instance RangeEvaluable : Evaluable (option (Range N)) := {
-    ezero := Some (range N 0%N (N.pred (Npow2 n)));
-
-    toT := fun x => Some (range N (Z.to_N x) (Z.to_N x));
-    fromT := fun x => orElse 0%Z (omap x (fun r =>
-      match r with
-      | range low high => Some (Z.of_N high)
-      end));
-
-    eadd := fun x y => omap x (fun X => omap y (fun Y => rapp range_add_valid X Y));
-    esub := fun x y => omap x (fun X => omap y (fun Y => rapp range_sub_valid X Y));
-    emul := fun x y => omap x (fun X => omap y (fun Y => rapp range_mul_valid X Y));
-    eshiftr := fun x y => omap x (fun X => omap y (fun Y => rapp range_shiftr_valid X Y));
-    eand := fun x y => omap x (fun X => omap y (fun Y => rapp range_and_valid X Y));
-
-    eltb := fun x y =>
-      match (x, y) with
-      | (Some (range xlow xhigh), Some (range ylow yhigh)) =>
-        N.ltb xhigh yhigh
-
-      | _ => false 
-      end;
-
-    eeqb := fun x y =>
-      match (x, y) with
-      | (Some (range xlow xhigh), Some (range ylow yhigh)) =>
-        andb (N.eqb xlow ylow) (N.eqb xhigh yhigh)
-
-      | _ => false
-      end;
-  }.
-End Range.
+End BoundedWord.
\ No newline at end of file
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 9723c75a0..80d9044c4 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -17,10 +17,9 @@ Module GF25519.
 
   Section DefaultBounds.
     Import ListNotations.
-    Local Notation rr exp :=
-      (orElse any (make (n := bits) 0 (wzero _) (2^exp + 2^exp/10)%N)).
+    Local Notation rr exp := (range N 0%N (2^exp + 2^exp/10)%N).
 
-    Definition feBound: list (@BoundedWord bits) :=
+    Definition feBound: list (Range N) :=
       [rr 26; rr 27; rr 26; rr 27; rr 26;
        rr 27; rr 26; rr 27; rr 26; rr 27].
   End DefaultBounds.
@@ -40,7 +39,7 @@ Module GF25519.
     Definition inputs: nat := 20.
     Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputBounds: list (@BoundedWord bits) := feBound ++ feBound.
+    Definition inputBounds := feBound ++ feBound.
 
     Definition ge25519_add_expr :=
         Eval cbv beta delta [fe25519 add mul sub Let_In] in add.
@@ -93,7 +92,7 @@ Module GF25519.
     Definition inputs: nat := 20.
     Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputBounds: list (@BoundedWord bits) := feBound ++ feBound.
+    Definition inputBounds := feBound ++ feBound.
 
     Definition ge25519_sub_expr :=
         Eval cbv beta delta [fe25519 add mul sub Let_In] in sub.
@@ -146,7 +145,7 @@ Module GF25519.
     Definition inputs: nat := 20.
     Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputBounds: list (@BoundedWord bits) := feBound ++ feBound.
+    Definition inputBounds := feBound ++ feBound.
 
     Definition ge25519_mul_expr :=
         Eval cbv beta delta [fe25519 add mul sub Let_In] in mul.
@@ -199,7 +198,7 @@ Module GF25519.
     Definition inputs: nat := 10.
     Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputBounds: list (@BoundedWord bits) := feBound.
+    Definition inputBounds := feBound.
 
     Definition ge25519_opp_expr :=
         Eval cbv beta delta [fe25519 add mul sub opp Let_In] in opp.
@@ -256,4 +255,4 @@ End GF25519.
 Extraction "GF25519Add" GF25519.Add.
 Extraction "GF25519Sub" GF25519.Sub.
 Extraction "GF25519Mul" GF25519.Mul.
-Extraction "GF25519Opp" GF25519.Opp.
+Extraction "GF25519Opp" GF25519.Opp.
\ No newline at end of file
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index 87fc8cc92..e7fc23e0a 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -1,4 +1,5 @@
 Require Export Crypto.Assembly.QhasmCommon.
+
 Require Export Crypto.Assembly.PhoasCommon.
 Require Export Crypto.Assembly.HL.
 Require Export Crypto.Assembly.LL.
@@ -21,7 +22,7 @@ Module Type Expression.
   Parameter inputs: nat.
   Parameter ResultType: type.
   Parameter hlProg: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-  Parameter inputBounds: list (@BoundedWord bits).
+  Parameter inputBounds: list (Range N).
 End Expression.
 
 Module Pipeline (Input: Expression).
@@ -42,28 +43,32 @@ Module Pipeline (Input: Expression).
     | None => None
     end.
 
-  Definition B: Type := option (@BoundedWord bits).
+  Import LLConversions.
+
+  Definition RWV: Type := option RangeWithValue.
 
-  Definition boundedProg: NAry inputs B (@LL.expr B B ResultType) :=
-    NArgMap (fun x =>
-        orElse (Z.of_N (N.pred (Npow2 bits)))
-               (option_map Z.of_N (option_map Evaluables.high x))) (
-      liftN (LLConversions.convertZToBounded bits) llProg).
+  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).
 
-  Fixpoint valid' {T k} ins (f: NAry k B T) :=
-    match k as k' return NAry k' B T -> T with
+  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 => @valid' _ m xs (f' x)
-      | nil => @valid' _ m nil (f' None)
+      | cons x xs => @applyProgOn A B m xs (f' x)
+      | nil => @applyProgOn A B m nil (f' None)
       end
     end f.
 
-  Definition outputBounds := valid' (map (@Some _) inputBounds) boundedProg.
+  Definition outputBounds :=
+    applyProgOn (map (@Some _) (map from_range inputBounds)) (
+      liftN (fun e => typeMap (option_map proj) (@LL.interp RWV (@RWVEval bits) _ e))
+        rwvProg).
 
   Definition valid :=
-    valid' (map (@Some _) inputBounds) (liftN (LLConversions.check) boundedProg).
+    applyProgOn (map (@Some _) (map from_range inputBounds)) (
+     liftN (@check bits _ RWV (@RWVEval bits)) rwvProg).
 End Pipeline.
 
 Module SimpleExample.
@@ -78,7 +83,7 @@ Module SimpleExample.
     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 (@BoundedWord bits) := [ any ].
+    Definition inputBounds: list (Range N) := [ range N 0%N (Npow2 31) ].
   End SimpleExpression.
 
   Module SimplePipeline := Pipeline SimpleExpression.