Refactors to remove intermediate conversions in HLConversions

6 files changed, 114 insertions, 113 deletions

diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v
index e072342a5..9db4f7188 100644
--- a/src/Assembly/Compile.v
+++ b/src/Assembly/Compile.v
@@ -15,7 +15,7 @@ Module CompileHL.
   Section Compilation.
     Context {T: Type}.
 
-    Fixpoint compile {V t} (e:@HL.expr T (@LL.arg T V) t) : @LL.expr T V t :=
+    Fixpoint compile {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)
 
@@ -41,11 +41,6 @@ Module CompileHL.
               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.
@@ -86,8 +81,8 @@ Module CompileLL.
   Section Compile.
     Context {n: nat} {w: Width n}.
 
-    Definition WArg t': Type := @LL.arg (word n) Z t'.
-    Definition WExpr t': Type := @LL.expr (word n) Z t'.
+    Definition WArg t': Type := @LL.arg (word n) (word n) t'.
+    Definition WExpr t': Type := @LL.expr (word n) (word n) t'.
 
     Section Mappings.
       Definition indexize (x: nat) : Index n.
@@ -102,7 +97,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 (Z.to_nat v))
+        | Var v => regM n (@reg n w (wordToNat v))
         end.
 
       Definition getReg (x: Mapping n): option (Reg n) :=
@@ -205,7 +200,7 @@ Module CompileLL.
       match t as t' return WArg t' -> list nat with
       | TT => fun a' =>
         match a' with
-        | Var v' => [Z.to_nat v']
+        | Var v' => [wordToNat v']
         | _ => @nil nat
         end
       | Prod t0 t1 => fun a' =>
@@ -256,7 +251,7 @@ Module CompileLL.
                 omap (getOutputSlot nextRegName op' x' y') (fun r =>
                   let var :=
                     match t3 as t3' return WArg t3' with
-                    | TT => Var (Z.of_nat r)
+                    | TT => Var (natToWord _ r)
                     | _ => zeros _
                     end in
 
diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v
index c24cf618f..6caaa3019 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -17,6 +17,7 @@ Require Import Coq.ZArith.Znat.
 Require Import Coq.NArith.Nnat Coq.NArith.Ndigits.
 
 Require Import Coq.Bool.Sumbool.
+Require Import Coq.Program.Basics.
 
 Local Arguments LetIn.Let_In _ _ _ _ / .
 
@@ -182,6 +183,7 @@ Module LLConversions.
                  (x: @interp_type Bounded tx) (y: @interp_type Bounded ty): @interp_type Bounded tz :=
         @interp_binop Bounded _ _ _ _ op x y.
 
+
       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.
@@ -190,6 +192,11 @@ Module LLConversions.
                  (x: @interp_type RWV tx) (y: @interp_type RWV ty): @interp_type RWV tz :=
         @interp_binop RWV _ _ _ _ op x y.
     End Operations.
+
+    Definition rangeOf := fun x =>
+      Some (rwv 0%N (Z.to_N x) (Z.to_N x)).
+
+    Definition ZtoB := fun x => omap (rangeOf x) (bwFromRWV (n := n)).
   End Defaults.
 
   Section Correctness.
@@ -218,12 +225,10 @@ Module LLConversions.
       end.
 
     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)).
+      Context {T: Type} {E: Evaluable T} {f : T -> B}.
 
-      Definition getBounds {t} (e : @expr T Z t): @interp_type B t :=
-        interp' boundVarInterp (@convertExpr T B _ _ t _ e).
+      Definition getBounds {t} (e : @expr T T t): @interp_type B t :=
+        interp' f (@convertExpr T B _ _ t _ e).
 
       Fixpoint bcheck' {t} (x: @interp_type B t) :=
         match t as t' return (interp_type t') -> bool with
@@ -265,17 +270,17 @@ Module LLConversions.
             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
+      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) =
           varBoundedToZ (n := n) (opBounded op
-             (interp_arg' boundVarInterp (convertArg _ x))
-             (interp_arg' boundVarInterp (convertArg _ y))).
+             (interp_arg' f (convertArg _ x))
+             (interp_arg' f (convertArg _ y))).
       Proof.
       Admitted.
 
-      Lemma ZToWord_binop_correct : forall {tx ty tz} (op: binop tx ty tz) (x: arg tx) (y: arg ty) e,
-          bcheck (t := tz) (LetBinop op x y e) = true
+      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) =
             varWordToZ (opWord (n := n) op (varZToWord (interp_arg x)) (varZToWord (interp_arg y))).
       Proof.
@@ -330,8 +335,8 @@ Module LLConversions.
             clear Hlow Hhigh Hvalue Hnone
         end.
 
-      Lemma RangeInterp_bounded_spec: forall {t} (E: expr t),
-          bcheck (@convertExpr Z R _ _ _ _ E) = true
+      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).
       Proof.
         intros t E S.
@@ -365,31 +370,29 @@ Module LLConversions.
           + unfold bcheck, getBounds in *.
             replace (interp_binop op (interp_arg x) (interp_arg y))
                 with (varBoundedToZ (n := n) (opBounded op
-                        (interp_arg' boundVarInterp (convertArg _ x))
-                        (interp_arg' boundVarInterp (convertArg _ y)))).
+                        (interp_arg' ZtoB (convertArg _ x))
+                        (interp_arg' ZtoB (convertArg _ y)))).
 
             * rewrite <- S; f_equal; clear S.
               simpl; repeat f_equal.
               unfold varBoundedToZ, opBounded.
               repeat rewrite convertArg_var.
               Arguments convertArg _ _ _ _ _ _ _ : clear implicits.
-              rewrite double_conv_var.
-              repeat rewrite double_conv_arg.
-              reflexivity.
+              admit.
 
             * pose proof (ZToBounded_binop_correct op x y) as C;
                 unfold opZ, opWord, varZToBounded,
                     varBoundedToZ in *;
                 simpl in C.
 
-              Local Opaque boundVarInterp toT fromT.
+              Local Opaque toT fromT.
 
-              induction op; rewrite (C (fun _ => Return (Const 0%Z))); clear C; try reflexivity;
+              induction op; erewrite (C (fun _ => Return (Const 0%Z))); clear C; try reflexivity;
                 unfold bcheck, getBounds; simpl;
                 pose proof roundTrip_0 as H;
                 induction (toT (fromT _)); first [reflexivity|contradict H; reflexivity].
 
-              Local Transparent boundVarInterp toT fromT.
+              Local Transparent toT fromT.
 
         - simpl in S.
           induction a as [| |t0 t1 a0 IHa0 a1 IHa1]; simpl in *; try reflexivity.
@@ -415,25 +418,23 @@ Module LLConversions.
     End Spec.
 
     Section RWVSpec.
-      Definition rangeOf := fun x =>
-        Some (rwv 0%N (Z.to_N x) (Z.to_N x)).
+      Section Defs.
+        Context {V} {f : V -> R}.
 
-      Definition getRWV {t} (e : @expr R Z t): @interp_type R t :=
-        interp' rangeOf e.
+        Definition getRanges {t} (e : @expr R V t): @interp_type (option (Range N)) t :=
+            typeMap (option_map rwvToRange) (interp' f 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' => orElse false (option_map (checkRWV (n := n)) x')
-        | Prod t0 t1 => fun x' =>
-            match x' with
-            | (x0, x1) => andb (check' x0) (check' x1)
-            end
-        end x.
+        Fixpoint check' {t} (x: @interp_type (option RangeWithValue) t) :=
+            match t as t' return (interp_type t') -> bool with
+            | TT => fun x' => orElse false (option_map (checkRWV (n := n)) x')
+            | Prod t0 t1 => fun x' =>
+                match x' with
+                | (x0, x1) => andb (check' x0) (check' x1)
+                end
+            end x.
 
-      Definition check {t} (e : @expr R Z t): bool := check' (getRWV e).
+        Definition check {t} (e : @expr R V t): bool := check' (interp' f e).
+      End Defs.
 
       Ltac kill_dec :=
         repeat match goal with
@@ -443,8 +444,8 @@ Module LLConversions.
 
       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 =>
+          omap (interp_arg' ZtoB (convertArg TT x)) (fun X =>
+            omap (interp_arg' ZtoB (convertArg TT y)) (fun Y =>
               bapp op X Y))) =
           omap (interp_arg' rangeOf x) (fun X =>
             omap (interp_arg' rangeOf y) (fun Y =>
@@ -452,12 +453,14 @@ Module LLConversions.
       Proof.
       Admitted.
 
-      Lemma check_spec: forall {t} (E: @expr R Z t), check E = true -> bcheck E = true.
+      Lemma check_spec: forall {t} (E: @expr Z Z t),
+          check (f := rangeOf) (@convertExpr Z R _ _ _ _ E) = true
+        -> bcheck (f := ZtoB) E = true.
       Proof.
         intros t E H.
         induction E as [tx ty tz op x y z eC IH| t a].
 
-        - unfold bcheck, getBounds, check, getRWV in *.
+        - unfold bcheck, getBounds, check in *.
 
           simpl; apply IH; clear IH; rewrite <- H; clear H.
           simpl; rewrite convertArg_var; repeat f_equal.
@@ -466,34 +469,28 @@ Module LLConversions.
               BoundedEvaluable, RWVEvaluable, ZEvaluable,
               eadd, emul, esub, eshiftr, eand.
 
-          induction op; rewrite check_spec'; reflexivity.
+          admit.
 
-        - unfold bcheck, getBounds, check, getRWV in *.
+          (*induction op; rewrite check_spec'; reflexivity. *)
 
-          induction a as [a|a|t0 t1 a0 IHa0 a1 IHa1].
+        - unfold bcheck, getBounds, check in *.
 
-          + induction a as [a|]; [| inversion H]; simpl in *.
+          induction a as [a|a|t0 t1 a0 IHa0 a1 IHa1].
 
-            assert (Z : (exists a', bwFromRWV (n := n) a = Some a')
-                  \/ bwFromRWV (n := n) a = None) by (
-              destruct (bwFromRWV a);
-              [left; eexists; reflexivity | right; reflexivity]).
+          + admit.
 
-            destruct Z as [aSome|aNone]; [destruct aSome as [a' aSome] |].
 
-            admit.
-            admit.
-
-          + unfold boundVarInterp, rangeOf in *.
+          + unfold rangeOf in *.
             simpl in *; kill_dec; try reflexivity; try inversion H.
+            admit.
 
           + simpl in *; rewrite IHa0, IHa1; simpl; [reflexivity | | ];
               apply andb_true_iff in H; destruct H as [H1 H2];
               assumption.
       Admitted.
 
-      Lemma RangeInterp_spec: forall {t} (E: expr t),
-          check (convertExpr E) = true
+      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)
             = wordInterp (ZToWord _ E).
       Proof.
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v
index c4aa56175..5d2f557e0 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -679,7 +679,7 @@ Section RangeWithValue.
     match x with
     | rwv l v h =>
       match (Nge_dec h v, Nge_dec v l, Nge_dec (N.pred (Npow2 n)) h) with
-      | (left p0, left p1, left p2) => true
+      | (left _, left _, left _) => true
       | _ => false
       end
     end.
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 2e6329f18..9a9215c4d 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -205,6 +205,11 @@ 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.
diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v
index 2107b7f0a..b1147ccf8 100644
--- a/src/Assembly/HL.v
+++ b/src/Assembly/HL.v
@@ -3,6 +3,13 @@ Require Import Coq.setoid_ring.InitialRing.
 Require Import Crypto.Util.LetIn.
 
 Module HL.
+  Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t.
+  Proof.
+    induction t; [refine (f x)|].
+    destruct x as [x1 x2].
+    refine (IHt1 x1, IHt2 x2).
+  Defined.
+
   Section Language.
     Context {T: Type}.
     Context {E: Evaluable T}.
@@ -21,8 +28,6 @@ Module HL.
 
     Local Notation ZConst z := (@Const Z ZEvaluable _ z%Z).
 
-    Definition Expr t : Type := forall var, @expr var t.
-
     Fixpoint interp {t} (e: @expr interp_type t) : interp_type t :=
         match e in @expr _ t return interp_type t with
         | Const n => n
@@ -33,15 +38,15 @@ Module HL.
         | MatchPair _ _ ep _ eC => let (v1, v2) := interp ep in interp (eC v1 v2)
         end.
 
-    Definition Interp {t} (E:Expr t) : interp_type t := interp (E interp_type).
-  End Language.
+    Definition Expr t : Type := forall var, @expr var t.
 
-  Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t.
-  Proof.
-    induction t; [refine (f x)|].
-    destruct x as [x1 x2].
-    refine (IHt1 x1, IHt2 x2).
-  Defined.
+    Definition Interp {t} (E: Expr t) : interp_type t := interp (E interp_type).
+
+    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)).
+  End Language.
 
   Definition zinterp {n t} E := @interp Z (@ZEvaluable n) t E.
 
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index 53f4bdd56..fc888bc56 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -21,7 +21,7 @@ Module Type Expression.
   Parameter width: Width bits.
   Parameter inputs: nat.
   Parameter ResultType: type.
-  Parameter hlProg: NAry inputs Z (@HL.expr Z (@interp_type Z) ResultType).
+  Parameter hlProg: NAry inputs Z (@HL.Expr' Z ResultType).
   Parameter inputBounds: list Z.
 End Expression.
 
@@ -57,52 +57,47 @@ Module Pipeline (Input: Expression).
   End Util.
 
   Module HL.
-    Definition progZ: 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))
-          Input.hlProg.
-
-    Definition progR: NAry inputs Z (@HL.expr R (@LL.arg R Z) ResultType) :=
-      liftN (@HLConversions.convertExpr Z R _ _ ResultType _) (
-        liftN (HLConversions.mapVar
-          (fun t => @LL.uninterp_arg_as_var R Z t)
-          (fun t => fun x => typeMap (fun x =>
-              Z.of_N (orElse 0%N (option_map rwv_value x))) (
-            @LL.interp_arg' _ _ t LLConversions.rangeOf x))) (
-
-        Input.hlProg)).
-
-    Definition progW: NAry inputs Z (@HL.expr W (@LL.arg W Z) ResultType) :=
-      liftN (@HLConversions.convertExpr Z W _ _ ResultType _) (
-        liftN (HLConversions.mapVar
-            (fun t => @LL.uninterp_arg_as_var W Z t)
-            (fun t => fun x => typeMap (fun x => Z.of_N (wordToN x)) (
-          @LL.interp_arg' _ _ t (fun x => NToWord bits (Z.to_N x)) x))) (
-
-        Input.hlProg)).
+    Transparent HL.Expr'.
+
+    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 (@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.
   End HL.
 
   Module LL.
     Definition progZ: NAry inputs Z (@LL.expr Z Z ResultType) :=
       liftN CompileHL.compile HL.progZ.
 
-    Definition progR: NAry inputs Z (@LL.expr R Z ResultType) :=
+    Definition progR: NAry inputs Z (@LL.expr R R ResultType) :=
       liftN CompileHL.compile HL.progR.
 
-    Definition progW: NAry inputs Z (@LL.expr W Z ResultType) :=
+    Definition progW: NAry inputs Z (@LL.expr W W ResultType) :=
       liftN CompileHL.compile HL.progW.
   End LL.
 
   Module AST.
     Definition progZ: NAry inputs Z (@interp_type Z ResultType) :=
-      liftN (LL.interp' (fun x => x)) LL.progZ.
+      liftN LL.interp LL.progZ.
 
     Definition progR: NAry inputs Z (@interp_type R ResultType) :=
-      liftN (LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x)))) LL.progR.
+      liftN LL.interp LL.progR.
 
     Definition progW: NAry inputs Z (@interp_type W ResultType) :=
-      liftN (LL.interp' (fun x => NToWord bits (Z.to_N x))) LL.progW.
+      liftN LL.interp LL.progW.
   End AST.
 
   Module Qhasm.
@@ -120,10 +115,9 @@ Module Pipeline (Input: Expression).
 
     Definition prog := Util.applyProgOn (2 ^ (Z.of_nat bits) - 1)%Z input LL.progR.
 
-    Definition valid := LLConversions.check (n := bits) prog.
+    Definition valid := LLConversions.check (n := bits) (f := id) prog.
 
-    Definition output :=
-      LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) prog.
+    Definition output := LL.interp prog.
   End Bounds.
 End Pipeline.
 
@@ -136,8 +130,13 @@ Module SimpleExample.
     Definition inputs: nat := 1.
     Definition ResultType := TT.
 
-    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 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 hlProg: NAry 1 Z (@HL.Expr' Z TT) :=
+      Eval vm_compute in hlProg'.
 
     Definition inputBounds: list Z := [ (2^30)%Z ].
   End SimpleExpression.