Refactors to remove intermediate conversions

7 files changed, 253 insertions, 288 deletions

diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v
index 9db4f7188..f0ee42e7c 100644
--- a/src/Assembly/Compile.v
+++ b/src/Assembly/Compile.v
@@ -15,9 +15,9 @@ Module CompileHL.
   Section Compilation.
     Context {T: Type}.
 
-    Fixpoint compile {t} (e:@HL.expr T (@LL.arg T T) t) : @LL.expr T T t :=
+    Fixpoint compile {T t} (e:@HL.expr T (@LL.arg T T) t) : @LL.expr T T t :=
         match e with
-        | HL.Const n => LL.Return (LL.Const n)
+        | HL.Const _ n => LL.Return (LL.Const n)
 
         | HL.Var _ arg => LL.Return arg
 
@@ -41,6 +41,9 @@ Module CompileHL.
               let (a1, a2) := LL.match_arg_Prod arg in
               compile (eC a1 a2))
         end.
+
+    Definition Compile {T t} (e:@HL.Expr T t) : @LL.expr T T t :=
+      compile (e (@LL.arg T T)).
   End Compilation.
 
   Section Correctness.
diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v
index 6caaa3019..c7801c63a 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -31,29 +31,9 @@ Defined.
 Module HLConversions.
   Import HL.
 
-  Fixpoint mapVar {A: Type} {t V0 V1} (f: forall t, V0 t -> V1 t) (g: forall t, V1 t -> V0 t) (a: expr (T := A) (var := V0) t): expr (T := A) (var := V1) t :=
+  Fixpoint convertExpr {A B: Type} {EB: Evaluable B} {t v} (a: expr (T := A) (var := v) t): expr (T := B) (var := v) t :=
     match a with
-    | Const x => Const x
-    | Var t x => Var (f _ x)
-    | Binop t1 t2 t3 o e1 e2 => Binop o (mapVar f g e1) (mapVar f g e2)
-    | Let tx e tC h => Let (mapVar f g e) (fun x => mapVar f g (h (g _ x)))
-    | Pair t1 e1 t2 e2 => Pair (mapVar f g e1) (mapVar f g e2)
-    | MatchPair t1 t2 e tC h => MatchPair (mapVar f g e) (fun x y => mapVar f g (h (g _ x) (g _ y)))
-    end.
-
-  Definition convertVar {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t} (a: interp_type (T := A) t): interp_type (T := B) t.
-  Proof.
-    induction t as [| t3 IHt1 t4 IHt2].
-
-    - refine (@toT B EB (@fromT A EA _)); assumption.
-
-    - destruct a as [a1 a2]; constructor;
-        [exact (IHt1 a1) | exact (IHt2 a2)].
-  Defined.
-
-  Fixpoint convertExpr {A B: Type} {EA: Evaluable A} {EB: Evaluable B} {t v} (a: expr (T := A) (var := v) t): expr (T := B) (var := v) t :=
-    match a with
-    | Const x => Const (@toT B EB (@fromT A EA x))
+    | Const E x => Const (@toT B EB (@fromT A E x))
     | Var t x => @Var B _ t x
     | Binop t1 t2 t3 o e1 e2 =>
       @Binop B _ t1 t2 t3 o (convertExpr e1) (convertExpr e2)
@@ -63,32 +43,6 @@ Module HLConversions.
     | MatchPair t1 t2 e tC f => MatchPair (convertExpr e) (fun x y =>
         convertExpr (f x y))
     end.
-
-  Definition convertZToWord {t} n 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 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).
-
-  Definition ZToRange {t} n (a: @Expr Z t): @Expr (option (@BoundedWord n)) t :=
-    fun v => convertZToBounded n v (a v).
-
-  Definition BInterp {n t} E: @interp_type (option (@BoundedWord n)) t :=
-    @Interp (option (@BoundedWord n)) (@BoundedEvaluable n) t E.
-
-  Example example_Expr : Expr TT := fun var => (
-    Let (Const 7) (fun a =>
-      Let (Let (Binop OPadd (Var a) (Var a)) (fun b => Pair (Var b) (Var b))) (fun p =>
-        MatchPair (Var p) (fun x y =>
-          Binop OPadd (Var x) (Var y)))))%Z.
-
-  Example interp_example_range :
-    option_map bw_high (BInterp (ZToRange 32 example_Expr)) = Some 28%N.
-  Proof. cbv; reflexivity. Qed.
 End HLConversions.
 
 Module LLConversions.
@@ -148,7 +102,7 @@ Module LLConversions.
     Transparent Word Bounded RWV.
 
     Instance RWVEvaluable' : Evaluable RWV := @RWVEvaluable n.
-    Instance ZEvaluable' : Evaluable Z := @ZEvaluable n.
+    Instance ZEvaluable' : Evaluable Z := ZEvaluable.
 
     Existing Instance ZEvaluable'.
     Existing Instance WordEvaluable.
@@ -207,7 +161,7 @@ Module LLConversions.
     Definition R := (option RangeWithValue).
 
     Instance RE : Evaluable R := @RWVEvaluable n.
-    Instance ZE : Evaluable Z := @ZEvaluable n.
+    Instance ZE : Evaluable Z := ZEvaluable.
     Instance WE : Evaluable W := @WordEvaluable n.
     Instance BE : Evaluable B := @BoundedEvaluable n.
 
@@ -272,7 +226,7 @@ Module LLConversions.
 
       Lemma ZToBounded_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: @arg Z Z tx) (y: @arg Z Z ty) e f,
           bcheck (t := tz) (f := f) (LetBinop op x y e) = true
-        -> opZ (n := n) op (interp_arg x) (interp_arg y) =
+        -> opZ op (interp_arg x) (interp_arg y) =
           varBoundedToZ (n := n) (opBounded op
              (interp_arg' f (convertArg _ x))
              (interp_arg' f (convertArg _ y))).
@@ -281,7 +235,7 @@ Module LLConversions.
 
       Lemma ZToWord_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e f,
           bcheck (t := tz) (f := f) (LetBinop op x y e) = true
-        -> opZ (n := n) op (interp_arg x) (interp_arg y) =
+        -> opZ op (interp_arg x) (interp_arg y) =
             varWordToZ (opWord (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))).
       Proof.
       Admitted.
@@ -289,7 +243,7 @@ Module LLConversions.
       Lemma roundTrip_0 : @toT Correctness.B BE (@fromT Z ZE 0%Z) <> None.
       Proof.
         intros; unfold toT, fromT, BE, ZE, BoundedEvaluable, ZEvaluable, bwFromRWV;
-          break_match; simpl; try break_match; simpl; try abstract (intro Z; inversion Z);
+          simpl; try break_match; simpl; try abstract (intro Z; inversion Z);
           pose proof (Npow2_gt0 n); simpl in *; nomega.
       Qed.
 
@@ -337,7 +291,7 @@ Module LLConversions.
 
       Lemma RangeInterp_bounded_spec: forall {t} (E: @expr Z Z t),
           bcheck (f := ZtoB) E = true
-        -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp (n := n) E) = wordInterp (ZToWord _ E).
+        -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E) = wordInterp (ZToWord _ E).
       Proof.
         intros t E S.
         unfold zinterp, ZToWord, wordInterp.
@@ -491,7 +445,7 @@ Module LLConversions.
 
       Lemma RangeInterp_spec: forall {t} (E: @expr Z Z t),
           check (f := rangeOf) (@convertExpr Z R _ _ _ _ E) = true
-        -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp (n := n) E)
+        -> typeMap (fun x => NToWord n (Z.to_N x)) (zinterp E)
             = wordInterp (ZToWord _ E).
       Proof.
         intros.
@@ -502,37 +456,3 @@ Module LLConversions.
     End RWVSpec.
   End Correctness.
 End LLConversions.
-
-Section ConversionTest.
-  Import HL HLConversions.
-
-  Fixpoint keepAddingOne {var} (x : @expr Z var TT) (n : nat) : @expr Z var TT :=
-    match n with
-    | O => x
-    | S n' => Let (Binop OPadd x (Const 1%Z)) (fun y => keepAddingOne (Var y) n')
-    end.
-
-  Definition KeepAddingOne (n : nat) : Expr (T := Z) TT :=
-    fun var => keepAddingOne (Const 1%Z) n.
-
-  Definition testCase := Eval vm_compute in KeepAddingOne 4000.
-
-  Eval vm_compute in (typeMap (option_map 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 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 5d2f557e0..0678c80bb 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -50,11 +50,31 @@ End Evaluability.
 
 Section Z.
   Context {n: nat}.
+
   Instance ZEvaluable : Evaluable Z := {
     ezero := 0%Z;
 
     (* Conversions *)
     toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
+    fromT   := fun x => Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x));
+
+    (* Operations *)
+    eadd    := Z.add;
+    esub    := Z.sub;
+    emul    := Z.mul;
+    eshiftr := Z.shiftr;
+    eand    := Z.land;
+
+    (* Comparisons *)
+    eltb    := Z.ltb;
+    eeqb    := Z.eqb
+  }.
+
+  Instance ConstEvaluable : Evaluable Z := {
+    ezero := 0%Z;
+
+    (* Conversions *)
+    toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
     fromT   := fun x =>
       if (Nge_dec (N.pred (Npow2 n)) (Z.to_N x))
       then Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x))
@@ -71,6 +91,25 @@ Section Z.
     eltb    := Z.ltb;
     eeqb    := Z.eqb
   }.
+
+  Instance InputEvaluable : Evaluable Z := {
+    ezero := 0%Z;
+
+    (* Conversions *)
+    toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
+    fromT   := fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x));
+
+    (* Operations *)
+    eadd    := Z.add;
+    esub    := Z.sub;
+    emul    := Z.mul;
+    eshiftr := Z.shiftr;
+    eand    := Z.land;
+
+    (* Comparisons *)
+    eltb    := Z.ltb;
+    eeqb    := Z.eqb
+  }.
 End Z.
 
 Section Word.
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 9a9215c4d..5011237ee 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -1,5 +1,4 @@
 Require Import Crypto.Assembly.Pipeline.
-
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.Specific.GF25519.
@@ -9,8 +8,7 @@ Module GF25519.
   Definition bits: nat := 64.
   Definition width: Width bits := W64.
 
-  Instance ZE : Evaluable Z := @ZEvaluable bits.
-  Existing Instance ZE.
+  Existing Instance ZEvaluable.
 
   Fixpoint makeBoundList {n} k (b: @BoundedWord n) :=
     match k with
@@ -35,168 +33,188 @@ Module GF25519.
     exact t.
   Defined.
 
-  Definition flatten {T}: (@interp_type Z FE -> T) -> NAry 10 Z T.
-    intro F; refine (fun (a b c d e f g h i j: Z) =>
-      F (a, b, c, d, e, f, g, h, i, j)).
-  Defined.
+  Section Expressions.
+    Definition flatten {T}: (@interp_type Z FE -> T) -> NAry 10 Z T.
+      intro F; refine (fun (a b c d e f g h i j: Z) =>
+        F (a, b, c, d, e, f, g, h, i, j)).
+    Defined.
 
-  Definition unflatten {T}:
+    Definition unflatten {T}:
       (forall a b c d e f g h i j, T (a, b, c, d, e, f, g, h, i, j))
     -> (forall x: @interp_type Z FE, T x).
-  Proof.
-    intro F; refine (fun (x: @interp_type Z FE) =>
-      let '(a, b, c, d, e, f, g, h, i, j) := x in
-      F a b c d e f g h i j).
-  Defined.
-
-  Ltac intro_vars_for R := revert R;
-    match goal with
-    | [ |- forall x, @?T x ] => apply (@unflatten T); intros
-    end.
+    Proof.
+      intro F; refine (fun (x: @interp_type Z FE) =>
+        let '(a, b, c, d, e, f, g, h, i, j) := x in
+        F a b c d e f g h i j).
+    Defined.
 
-  Module AddExpr <: Expression.
-    Definition bits: nat := bits.
-    Definition inputs: nat := 20.
-    Definition width: Width bits := width.
-    Definition ResultType := FE.
-    Definition inputBounds := feBound ++ feBound.
+    Ltac intro_vars_for R := revert R;
+      match goal with
+      | [ |- forall x, @?T x ] => apply (@unflatten T); intros
+      end.
 
     Definition ge25519_add_expr :=
-        Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_add.
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in carry_add.
 
-    Definition ge25519_add' (P Q: @interp_type Z FE) :
-        { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_add_expr P Q }.
+    Definition ge25519_sub_expr :=
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in carry_sub.
+
+    Definition ge25519_mul_expr :=
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in mul.
+
+    Definition ge25519_opp_expr :=
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in opp.
+
+    Definition ge25519_add' (P Q: @interp_type Z FE):
+      { r: @HL.Expr Z FE | HL.Interp r = ge25519_add_expr P Q }.
     Proof.
       intro_vars_for P.
       intro_vars_for Q.
 
       eexists.
+
       cbv beta delta [ge25519_add_expr].
 
+      etransitivity; [reflexivity|].
+
       let R := HL.rhs_of_goal in
-      let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (t := ResultType) X); [reflexivity|].
+      let X := HL.Reify R in
+      transitivity (HL.Interp (X bits)); [reflexivity|].
+
+      cbv iota beta delta [ HL.Interp
+          interp_type interp_binop HL.interp
+          Z.land ZEvaluable eadd esub emul eshiftr eand].
 
-      cbv iota beta delta [
-            interp_type interp_binop HL.interp
-            Z.land ZEvaluable eadd esub emul eshiftr eand].
       reflexivity.
     Defined.
 
-    Definition ge25519_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) :=
-        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_add p q)))).
-  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 carry_add mul carry_sub Let_In] in carry_sub.
-
-    Definition ge25519_sub' (P Q: @interp_type Z FE) :
-        { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_sub_expr P Q }.
+    Definition ge25519_sub' (P Q: @interp_type Z FE):
+      { r: @HL.Expr Z FE | HL.Interp r = ge25519_sub_expr P Q }.
     Proof.
       intro_vars_for P.
       intro_vars_for Q.
 
       eexists.
+
       cbv beta delta [ge25519_sub_expr].
 
+      etransitivity; [reflexivity|].
+
       let R := HL.rhs_of_goal in
-      let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (t := ResultType) X); [reflexivity|].
+      let X := HL.Reify R in
+      transitivity (HL.Interp (X bits)); [reflexivity|].
+
+      cbv iota beta delta [ HL.Interp
+          interp_type interp_binop HL.interp
+          Z.land ZEvaluable eadd esub emul eshiftr eand].
 
-      cbv iota beta delta [
-            interp_type interp_binop HL.interp
-            Z.land ZEvaluable eadd esub emul eshiftr eand].
       reflexivity.
     Defined.
 
-    Definition ge25519_sub (P Q: @interp_type Z ResultType) :=
-        proj1_sig (ge25519_sub' P Q).
+    Definition ge25519_mul' (P Q: @interp_type Z FE):
+      { r: @HL.Expr Z FE | HL.Interp r = ge25519_mul_expr P Q }.
+    Proof.
+      intro_vars_for P.
+      intro_vars_for Q.
 
-    Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_sub p q)))).
-  End SubExpr.
+      eexists.
 
-  Module MulExpr <: Expression.
-    Definition bits: nat := bits.
-    Definition inputs: nat := 20.
-    Definition width: Width bits := width.
-    Definition ResultType := FE.
-    Definition inputBounds := feBound ++ feBound.
+      cbv beta delta [ge25519_mul_expr].
 
-    Definition ge25519_mul_expr :=
-        Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in mul.
+      etransitivity; [reflexivity|].
+
+      let R := HL.rhs_of_goal in
+      let X := HL.Reify R in
+      transitivity (HL.Interp (X bits)); [reflexivity|].
+
+      cbv iota beta delta [ HL.Interp
+          interp_type interp_binop HL.interp
+          Z.land ZEvaluable eadd esub emul eshiftr eand].
 
-    Definition ge25519_mul' (P Q: @interp_type Z FE) :
-        { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_mul_expr P Q }.
+      reflexivity.
+    Defined.
+
+    Definition ge25519_opp' (P: @interp_type Z FE):
+      { r: @HL.Expr Z FE | HL.Interp r = ge25519_opp_expr P }.
     Proof.
       intro_vars_for P.
-      intro_vars_for Q.
 
       eexists.
-      cbv beta delta [ge25519_mul_expr].
+
+      cbv beta delta [ge25519_opp_expr zero_].
+
+      etransitivity; [reflexivity|].
 
       let R := HL.rhs_of_goal in
-      let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (t := ResultType) X); [reflexivity|].
+      let X := HL.Reify R in
+      transitivity (HL.Interp (X bits)); [reflexivity|].
+
+      cbv iota beta delta [ HL.Interp
+          interp_type interp_binop HL.interp
+          Z.land ZEvaluable eadd esub emul eshiftr eand].
 
-      cbv iota beta delta [
-            interp_type interp_binop HL.interp
-            Z.land ZEvaluable eadd esub emul eshiftr eand].
       reflexivity.
     Defined.
 
-    Definition ge25519_mul (P Q: @interp_type Z ResultType) :=
+    Definition ge25519_add (P Q: @interp_type Z FE) :=
+        proj1_sig (ge25519_add' P Q).
+
+    Definition ge25519_sub (P Q: @interp_type Z FE) :=
+        proj1_sig (ge25519_sub' P Q).
+
+    Definition ge25519_mul (P Q: @interp_type Z FE) :=
         proj1_sig (ge25519_mul' P Q).
 
-    Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_mul p q)))).
-  End MulExpr.
+    Definition ge25519_opp (P: @interp_type Z FE) :=
+        proj1_sig (ge25519_opp' P).
+  End Expressions.
 
-  Module OppExpr <: Expression.
+  Module AddExpr <: Expression.
     Definition bits: nat := bits.
-    Definition inputs: nat := 10.
+    Definition inputs: nat := 20.
     Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputBounds := feBound.
+    Definition inputBounds := feBound ++ feBound.
 
-    Definition ge25519_opp_expr :=
-        Eval cbv beta delta [fe25519 carry_add mul carry_sub carry_opp Let_In] in carry_opp.
+    Definition prog: NAry 20 Z (@HL.Expr Z ResultType) :=
+        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_add p q)))).
+  End AddExpr.
 
-    Definition ge25519_opp' (P: @interp_type Z FE) :
-        { r: @HL.expr Z (@interp_type Z) FE
-        | HL.interp (E := @ZEvaluable bits) (t := FE) r = ge25519_opp_expr P }.
-    Proof.
-      intro_vars_for P.
+  Module SubExpr <: Expression.
+    Definition bits: nat := bits.
+    Definition inputs: nat := 20.
+    Definition width: Width bits := width.
+    Definition ResultType := FE.
+    Definition inputBounds := feBound ++ feBound.
 
-      eexists.
-      cbv beta delta [ge25519_opp_expr zero_].
+    Definition ge25519_sub_expr :=
+      Eval cbv beta delta [fe25519 carry_add mul carry_sub opp Let_In] in
+        carry_sub.
 
-      let R := HL.rhs_of_goal in
-      let X := HL.reify (@interp_type Z) R in
-      transitivity (HL.interp (E := @ZEvaluable bits) (t := ResultType) X);
-        [reflexivity|].
+    Definition prog: NAry 20 Z (@HL.Expr Z ResultType) :=
+        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_sub p q)))).
+  End SubExpr.
 
-      cbv iota beta delta [
-        interp_type interp_binop HL.interp
-        Z.land ZEvaluable eadd esub emul eshiftr eand].
-      reflexivity.
-    Defined.
+  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_opp (P: @interp_type Z ResultType) :=
-        proj1_sig (ge25519_opp' P).
+    Definition prog: NAry 20 Z (@HL.Expr Z ResultType) :=
+        Eval cbv in (flatten (fun p => (flatten (fun q => ge25519_mul p q)))).
+  End MulExpr.
+
+  Module OppExpr <: Expression.
+    Definition bits: nat := bits.
+    Definition inputs: nat := 10.
+    Definition width: Width bits := width.
+    Definition ResultType := FE.
+    Definition inputBounds := feBound.
 
-    Definition hlProg: NAry 10 Z (@HL.expr Z (@interp_type Z) ResultType) :=
-        Eval cbv in (flatten (fun p => ge25519_opp p)).
+    Definition prog: NAry 10 Z (@HL.Expr Z ResultType) :=
+        Eval cbv in (flatten ge25519_opp).
   End OppExpr.
 
   Module Add := Pipeline AddExpr.
@@ -205,12 +223,7 @@ Module GF25519.
   Module Opp := Pipeline OppExpr.
 End GF25519.
 
-Set Printing All.
-Opaque eadd esub emul eshiftr eand toT fromT.
-Eval cbv iota beta delta in GF25519.Add.HL.progZ.
-Eval cbv iota beta delta in GF25519.Add.AST.progZ.
-
 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/HL.v b/src/Assembly/HL.v
index b1147ccf8..e9eecd4c8 100644
--- a/src/Assembly/HL.v
+++ b/src/Assembly/HL.v
@@ -18,7 +18,7 @@ Module HL.
         Context {var : type -> Type}.
 
         Inductive expr : type -> Type :=
-          | Const : @interp_type T TT -> expr TT
+          | Const : forall {_ : Evaluable T}, @interp_type T TT -> expr TT
           | Var : forall {t}, var t -> expr t
           | Binop : forall {t1 t2 t3}, binop t1 t2 t3 -> expr t1 -> expr t2 -> expr t3
           | Let : forall {tx}, expr tx -> forall {tC}, (var tx -> expr tC) -> expr tC
@@ -26,11 +26,11 @@ Module HL.
           | MatchPair : forall {t1 t2}, expr (Prod t1 t2) -> forall {tC}, (var t1 -> var t2 -> expr tC) -> expr tC.
     End expr.
 
-    Local Notation ZConst z := (@Const Z ZEvaluable _ z%Z).
+    Local Notation ZConst z := (@Const Z ConstEvaluable _ z%Z).
 
-    Fixpoint interp {t} (e: @expr interp_type t) : interp_type t :=
+    Fixpoint interp {t} (e: @expr interp_type t) : @interp_type T t :=
         match e in @expr _ t return interp_type t with
-        | Const n => n
+        | Const _ x => x
         | Var _ n => n
         | Binop _ _ _ op e1 e2 => interp_binop op (interp e1) (interp e2)
         | Let _ ex _ eC => dlet x := interp ex in interp (eC x)
@@ -40,29 +40,26 @@ Module HL.
 
     Definition Expr t : Type := forall var, @expr var t.
 
-    Definition Interp {t} (E: Expr t) : interp_type t := interp (E interp_type).
-
-    Definition Expr' t : Type := forall var, (forall t', @interp_type Z t' -> var t') -> @expr var t.
-
-    Definition Interp' {t} (f: Z -> T) (E: Expr' t) : interp_type t :=
-      interp (E (@interp_type T) (fun t' x => typeMap (t := t') f x)).
+    Definition Interp {t} (e: Expr t) : interp_type t := interp (e interp_type).
   End Language.
 
-  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 ZInterp {t} E := @Interp Z ZEvaluable t E.
 
   Definition wordInterp {n t} E := @interp (word n) (@WordEvaluable n) t E.
 
   Definition WordInterp {n t} E := @Interp (word n) (@WordEvaluable n) t E.
 
+  Existing Instance ZEvaluable.
+
   Example example_Expr : Expr TT := fun var => (
     Let (Const 7) (fun a =>
       Let (Let (Binop OPadd (Var a) (Var a)) (fun b => Pair (Var b) (Var b))) (fun p =>
         MatchPair (Var p) (fun x y =>
           Binop OPadd (Var x) (Var y)))))%Z.
 
-  Example interp_example_Expr : ZInterp (n := 16) example_Expr = 28%Z.
+  Example interp_example_Expr : ZInterp example_Expr = 28%Z.
   Proof. reflexivity. Qed.
 
   (* Reification assumes the argument type is Z *)
@@ -85,68 +82,68 @@ Module HL.
     | Z.shiftr => constr:(OPshiftr)
     end.
 
-  Class reify {varT} (var:varT) {eT} (e:eT) {T:Type} := Build_reify : T.
+  Class reify (n: nat) {varT} (var:varT) {eT} (e:eT) {T:Type} := Build_reify : T.
   Definition reify_var_for_in_is {T} (x:T) (t:type) {eT} (e:eT) := False.
 
-  Ltac reify var e :=
+  Ltac reify n var e :=
     lazymatch e with
     | let x := ?ex in @?eC x =>
-      let ex := reify var ex in
-      let eC := reify var eC in
-      constr:(Let (T := Z) (var:=var) ex eC)
+      let ex := reify n var ex in
+      let eC := reify n var eC in
+      constr:(Let (T:=Z) (var:=var) ex eC)
     | match ?ep with (v1, v2) => @?eC v1 v2 end =>
-      let ep := reify var ep in
-      let eC := reify var eC in
-      constr:(MatchPair (T := Z) (var:=var) ep eC)
+      let ep := reify n var ep in
+      let eC := reify n var eC in
+      constr:(MatchPair (T:=Z) (var:=var) ep eC)
     | pair ?a ?b =>
-      let a := reify var a in
-      let b := reify var b in
-      constr:(Pair (T := Z) (var:=var) a b)
+      let a := reify n var a in
+      let b := reify n var b in
+      constr:(Pair (T:=Z) (var:=var) a b)
     | ?op ?a ?b =>
       let op := reify_binop op in
-      let b := reify var b in
-      let a := reify var a in
-      constr:(Binop (T := Z) (var:=var) op a b)
+      let b := reify n var b in
+      let a := reify n var a in
+      constr:(Binop (T:=Z) (var:=var) op a b)
     | (fun x : ?T => ?C) =>
       let t := reify_type T in
       (* Work around Coq 8.5 and 8.6 bug *)
       (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4998> *)
       (* Avoid re-binding the Gallina variable referenced by Ltac [x] *)
       (* even if its Gallina name matches a Ltac in this tactic. *)
+      (* [C] here is an open term that references "x" by name *)
       let maybe_x := fresh x in
       let not_x := fresh x in
       lazymatch constr:(fun (x : T) (not_x : var t) (_:reify_var_for_in_is x t not_x) =>
-                          (_ : reify var C)) (* [C] here is an open term that references "x" by name *)
+                          (_ : reify n var C))
       with fun _ v _ => @?C v => C end
     | ?x =>
       lazymatch goal with
       | _:reify_var_for_in_is x ?t ?v |- _ => constr:(@Var Z var t v)
-      | _ =>
-        let x' := eval cbv in x in
-        match isZcst x' with
-        | true => constr:(@Const Z var x)
-        | false => constr:(@Var Z var TT x)
+      | _ => let x' := eval cbv in x in
+        match isZcst x with
+        | true => constr:(@Const Z var (@ConstEvaluable n) x)
+        | false => constr:(@Const Z var InputEvaluable x)
         end
       end
     end.
 
-  Hint Extern 0 (reify ?var ?e) => (let e := reify var e in eexact e) : typeclass_instances.
+  Hint Extern 0 (reify ?n ?var ?e) => (let e := reify n var e in eexact e) : typeclass_instances.
 
   Ltac Reify e :=
-    lazymatch constr:(fun (var:type->Type) => (_:reify var e)) with
-      (fun var => ?C) => constr:(fun (var:type->Type) => C) (* copy the term but not the type cast *)
+    lazymatch constr:(fun (n: nat) (var:type->Type) => (_:reify n var e)) with
+      (fun n var => ?C) => constr:(fun (n: nat) (var:type->Type) => C) (* copy the term but not the type cast *)
     end.
 
   Definition zinterp_type := @interp_type Z.
   Transparent zinterp_type.
 
-  Goal forall (x : Z) (v : zinterp_type TT) (_:reify_var_for_in_is x TT v), reify(T:=Z) zinterp_type ((fun x => x+x) x)%Z.
+  Goal forall (x : Z) (v : zinterp_type TT) (_:reify_var_for_in_is x TT v), reify (T:=Z) 16 zinterp_type ((fun x => x+x) x)%Z.
     intros.
-    let A := (reify zinterp_type (x + x + 1)%Z) in pose A.
+    let A := (reify 16 zinterp_type (x + x + 1)%Z) in idtac A.
   Abort.
 
   Goal False.
-    let z := reify zinterp_type (let x := 0 in x)%Z in pose z.
+    let z := (reify 16 zinterp_type (let x := 0 in x)%Z) in pose z.
   Abort.
 
   Ltac lhs_of_goal := match goal with |- ?R ?LHS ?RHS => constr:(LHS) end.
@@ -155,7 +152,7 @@ Module HL.
   Ltac Reify_rhs n :=
     let rhs := rhs_of_goal in
     let RHS := Reify rhs in
-    transitivity (ZInterp (n := n) RHS);
+    transitivity (ZInterp (RHS n));
     [|cbv iota beta delta [ZInterp Interp interp_type interp_binop interp]; reflexivity].
 
   Goal (0 = let x := 1+2 in x*3)%Z.
@@ -171,7 +168,7 @@ Module HL.
 
     Local Notation "x ≡ y" := (existT _ _ (x, y)).
 
-    Definition Texpr var t := @expr T var t.
+    Definition Texpr var t := @expr Z var t.
 
     Inductive wf : list (sigT (fun t => var1 t * var2 t))%type -> forall {t}, Texpr var1 t -> Texpr var2 t -> Prop :=
     | WfConst : forall G n, wf G (Const n) (Const n)
@@ -181,25 +178,25 @@ Module HL.
                   (op: binop t1 t2 t3),
         wf G e1 e1'
         -> wf G e2 e2'
-        -> wf G (Binop (T := T) op e1 e2) (Binop (T := T) op e1' e2')
+        -> wf G (Binop op e1 e2) (Binop op e1' e2')
     | WfLet : forall G t1 t2 e1 e1' (e2 : _ t1 -> Texpr _ t2) e2',
         wf G e1 e1'
         -> (forall x1 x2, wf ((x1 ≡ x2) :: G) (e2 x1) (e2' x2))
-        -> wf G (Let (T := T) e1 e2) (Let (T := T) e1' e2')
+        -> wf G (Let e1 e2) (Let e1' e2')
     | WfPair : forall G {t1} {t2} (e1: Texpr var1 t1) (e2: Texpr var1 t2)
                       (e1': Texpr var2 t1) (e2': Texpr var2 t2),
         wf G e1 e1'
         -> wf G e2 e2'
-        -> wf G (Pair (T := T) e1 e2) (Pair (T := T) e1' e2')
+        -> wf G (Pair e1 e2) (Pair e1' e2')
     | WfMatchPair : forall G t1 t2 tC ep ep' (eC : _ t1 -> _ t2 -> Texpr _ tC) eC',
         wf G ep ep'
         -> (forall x1 x2 y1 y2, wf ((x1 ≡ x2) :: (y1 ≡ y2) :: G) (eC x1 y1) (eC' x2 y2))
-        -> wf G (MatchPair (T := T) ep eC) (MatchPair (T := T) ep' eC').
+        -> wf G (MatchPair ep eC) (MatchPair ep' eC').
   End wf.
 
-  Definition Wf {T: Type} {t} (E : @Expr T t) := forall var1 var2, wf nil (E var1) (E var2).
+  Definition Wf {T: Type} {t} (E : Expr t) := forall var1 var2, wf nil (E var1) (E var2).
 
-  Example example_Expr_Wf : Wf example_Expr.
+  Example example_Expr_Wf : Wf (T := Z) example_Expr.
   Proof.
     unfold Wf; repeat match goal with
     | [ |- wf _ _ _ ] => constructor
diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v
index e0588214c..60587eb19 100644
--- a/src/Assembly/LL.v
+++ b/src/Assembly/LL.v
@@ -92,7 +92,7 @@ Module LL.
   Transparent interp interp_arg.
 
   Example example_expr :
-    (@interp Z (ZEvaluable (n := 32)) _
+    (@interp Z (ZEvaluable) _
       (LetBinop OPadd (Const 7%Z) (Const 8%Z) (fun v => Return v)) = 15)%Z.
   Proof. reflexivity. Qed.
 
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index fc888bc56..8eaa07161 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -20,9 +20,10 @@ Module Type Expression.
   Parameter bits: nat.
   Parameter width: Width bits.
   Parameter inputs: nat.
-  Parameter ResultType: type.
-  Parameter hlProg: NAry inputs Z (@HL.Expr' Z ResultType).
   Parameter inputBounds: list Z.
+  Parameter ResultType: type.
+
+  Parameter prog: NAry inputs Z (@HL.Expr Z ResultType).
 End Expression.
 
 Module Pipeline (Input: Expression).
@@ -37,7 +38,7 @@ Module Pipeline (Input: Expression).
   Definition R: Type := option RangeWithValue.
   Definition B: Type := option (@BoundedWord bits).
 
-  Instance ZEvaluable : Evaluable Z := @ZEvaluable bits.
+  Instance ZEvaluable : Evaluable Z := ZEvaluable.
   Instance WEvaluable : Evaluable W := @WordEvaluable bits.
   Instance REvaluable : Evaluable R := @RWVEvaluable bits.
   Instance BEvaluable : Evaluable B := @BoundedEvaluable bits.
@@ -57,36 +58,25 @@ Module Pipeline (Input: Expression).
   End Util.
 
   Module HL.
-    Transparent HL.Expr'.
+    Definition progZ: NAry inputs Z (@HL.Expr Z ResultType) :=
+      Input.prog.
 
-    Definition progZ: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-      refine (liftN _ Input.hlProg); intro X; apply X.
-      refine (fun t x => @LL.uninterp_arg Z Z t x).
-    Defined.
+    Definition progR: NAry inputs Z (@HL.Expr R ResultType) :=
+      liftN (fun x v => @HLConversions.convertExpr Z R _ _ _ (x v)) Input.prog.
 
-    Definition progR: NAry inputs Z (@HL.expr R (@LL.arg R R) ResultType).
-      refine (liftN _ _); [eapply (@HLConversions.convertExpr Z R _ _)|].
-      refine (liftN _ Input.hlProg); intro X; apply X.
-      refine (fun t x => @LL.uninterp_arg R R t (typeMap LLConversions.rangeOf x)).
-    Defined.
-
-    Definition progW: NAry inputs Z (@HL.expr W (@LL.arg W W) ResultType).
-      refine (liftN _ _); [eapply (@HLConversions.convertExpr Z W _ _)|].
-      refine (liftN _ Input.hlProg); intro X; apply X.
-      refine (fun t x => @LL.uninterp_arg W W t (typeMap (fun v =>
-        NToWord bits (Z.to_N v)) x)).
-    Defined.
+    Definition progW: NAry inputs Z (@HL.Expr W ResultType) :=
+      liftN (fun x v => @HLConversions.convertExpr Z W _ _ _ (x v)) Input.prog.
   End HL.
 
   Module LL.
     Definition progZ: NAry inputs Z (@LL.expr Z Z ResultType) :=
-      liftN CompileHL.compile HL.progZ.
+      liftN CompileHL.Compile HL.progZ.
 
     Definition progR: NAry inputs Z (@LL.expr R R ResultType) :=
-      liftN CompileHL.compile HL.progR.
+      liftN CompileHL.Compile HL.progR.
 
     Definition progW: NAry inputs Z (@LL.expr W W ResultType) :=
-      liftN CompileHL.compile HL.progW.
+      liftN CompileHL.Compile HL.progW.
   End LL.
 
   Module AST.
@@ -101,7 +91,8 @@ Module Pipeline (Input: Expression).
   End AST.
 
   Module Qhasm.
-    Definition pair := @CompileLL.compile bits width ResultType _ LL.progW.
+    Definition pair :=
+      @CompileLL.compile bits width ResultType _ LL.progW.
 
     Definition prog := option_map fst pair.
 
@@ -111,13 +102,18 @@ Module Pipeline (Input: Expression).
   End Qhasm.
 
   Module Bounds.
-    Definition input := Input.inputBounds.
+    Definition input := map (fun x => range N 0%N (Z.to_N x)) Input.inputBounds.
 
-    Definition prog := Util.applyProgOn (2 ^ (Z.of_nat bits) - 1)%Z input LL.progR.
+    Definition upper := Z.of_N (wordToN (wones bits)).
+
+    Definition prog :=
+      Util.applyProgOn upper Input.inputBounds LL.progR.
 
     Definition valid := LLConversions.check (n := bits) (f := id) prog.
 
-    Definition output := LL.interp prog.
+    Definition output :=
+      typeMap (option_map (fun x => range N (rwv_low x) (rwv_high x)))
+              (LL.interp prog).
   End Bounds.
 End Pipeline.
 
@@ -130,19 +126,16 @@ Module SimpleExample.
     Definition inputs: nat := 1.
     Definition ResultType := TT.
 
-    Definition hlProg': NAry 1 Z (@HL.Expr' Z TT).
-      intros x t f.
-      refine (HL.Binop OPadd (HL.Var (f TT x)) (HL.Const 5%Z)).
-    Defined.
+    Definition inputBounds: list Z := [ (2^30)%Z ].
 
-    Definition hlProg: NAry 1 Z (@HL.Expr' Z TT) :=
-      Eval vm_compute in hlProg'.
+    Existing Instance ZEvaluable.
 
-    Definition inputBounds: list Z := [ (2^30)%Z ].
+    Definition prog: NAry 1 Z (@HL.Expr Z TT).
+      intros x var.
+      refine (HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)).
+    Defined.
   End SimpleExpression.
 
   Module SimplePipeline := Pipeline SimpleExpression.
-
-  Export SimplePipeline.
 End SimpleExample.