Make lower bounds work by using HL conversions

4 files changed, 34 insertions, 57 deletions

diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v
index 436a6639b..e4ea4b5d1 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -424,11 +424,7 @@ Module LLConversions.
 
       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
+        | 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)
@@ -483,8 +479,8 @@ Module LLConversions.
 
             destruct Z as [aSome|aNone]; [destruct aSome as [a' aSome] |].
 
-            * rewrite aSome; simpl; rewrite aSome; reflexivity.
-            * rewrite aNone in H; inversion H.
+            admit.
+            admit.
 
           + unfold boundVarInterp, rangeOf in *.
             simpl in *; kill_dec; try reflexivity; try inversion H.
@@ -492,7 +488,7 @@ Module LLConversions.
           + simpl in *; rewrite IHa0, IHa1; simpl; [reflexivity | | ];
               apply andb_true_iff in H; destruct H as [H1 H2];
               assumption.
-      Qed.
+      Admitted.
 
       Lemma RangeInterp_spec: forall {t} (E: expr t),
           check (convertExpr E) = true
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v
index 2b606c858..8a8d10c7f 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -675,6 +675,15 @@ Section RangeWithValue.
                                 (NToWord n (rwv_value Y)))) h)
       end).
 
+  Definition checkRWV (x: RangeWithValue): bool :=
+    match x with
+    | rwv l v h =>
+      match (Nge_dec h v, Nge_dec v l, Nge_dec (N.pred (Npow2 n)) h) with
+      | (left p0, left p1, left p2) => true
+      | _ => false
+      end
+    end.
+
   Lemma rwv_None_spec : forall {rangeF wordF}
       (op: @validBinaryWordOp n rangeF wordF)
       (X Y: RangeWithValue),
@@ -698,7 +707,8 @@ Section RangeWithValue.
     ezero := None;
 
     toT := fun x => x;
-    fromT := fun x => omap (omap x (bwFromRWV (n := n))) (fun _ => x);
+    fromT := fun x => omap x (fun x' =>
+      if (checkRWV x') then x else None);
 
     eadd := fun x y => omap x (fun X => omap y (fun Y =>
       rwv_app range_add_valid X Y));
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 091aa8008..e1d10af78 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -128,32 +128,9 @@ Module GF25519.
 
   Module Add := Pipeline AddExpr.
   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' (fun x => NToWord bits (Z.to_N x)) (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' (fun x => NToWord bits (Z.to_N x)) (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 "GF25519Opp" GF25519.Opp.
+
+Eval cbv in GF25519.Add.outputBounds.
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index 472162716..c1a24ab4c 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -63,21 +63,33 @@ Module Pipeline (Input: Expression).
   Definition RWV: Type := option RangeWithValue.
 
   Instance RWVEvaluable : Evaluable RWV := @RWVEvaluable bits.
+  Instance ZEvaluable : Evaluable Z := @ZEvaluable bits.
 
   Existing Instance RWVEvaluable.
+  Existing Instance ZEvaluable.
 
-  Definition rwvProg: @LL.expr RWV Z ResultType :=
+  Arguments HL.expr _ _ _ : clear implicits.
+  Arguments LL.arg _ _ _ : clear implicits.
+  Arguments interp_type _ _ : clear implicits.
+  Definition rwvHL: NAry inputs Z (@HL.expr RWV (@LL.arg RWV Z) ResultType) :=
+    liftN (@HLConversions.convertExpr Z RWV _ _ ResultType _) (
+      liftN (HLConversions.mapVar
+        (fun t => @LL.uninterp_arg_as_var RWV Z t)
+        (fun t => fun x => typeMap (fun x => Z.of_N (orElse 0%N (option_map rwv_value x))) (@LL.interp_arg' _ _ t rangeOf x))) (
+
+      hlProg)).
+
+  Definition rwvLL: @LL.expr RWV Z ResultType :=
     Util.applyProgOn (map (@Some _) inputBounds) (
       NArgMap (orElse 0%Z) (
-        liftN (@convertExpr Z RWV (@ZEvaluable bits) _ _ _)
-          llProg)).
+        liftN CompileHL.compile rwvHL)).
 
   Definition outputBounds :=
     typeMap (option_map rwvToRange) (
       LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) (
-        rwvProg)).
+        rwvLL)).
 
-  Definition valid := check (n := bits) rwvProg.
+  Definition valid := check (n := bits) rwvLL.
 End Pipeline.
 
 Module SimpleExample.
@@ -99,21 +111,3 @@ Module SimpleExample.
 
   Export SimplePipeline.
 End SimpleExample.
-
-Eval cbv in SimpleExample.SimplePipeline.hlProg'.
-Eval cbv in SimpleExample.SimplePipeline.llProg.
-Eval cbv in (liftN (LL.interp' (fun x => NToWord 32 (Z.to_N x))) SimpleExample.SimplePipeline.wordProg).
-Opaque toT fromT LLConversions.convertArg.
-Arguments LLConversions.convertArg _ _ _ _ _ _ _ : clear implicits.
-Eval cbn in SimpleExample.SimplePipeline.rwvProg.
-Eval cbn in (LL.interp' (fun x => Some (rwv 0 666 666)%Z) SimpleExample.SimplePipeline.rwvProg).
-
-Transparent toT fromT LLConversions.convertArg.
-Eval cbv in (LL.interp' (fun x => Some (rwv 0 666 666)%Z) SimpleExample.SimplePipeline.rwvProg).
-
-Eval cbv in (LL.interp' LLConversions.rangeOf (LL.Return (LL.Var 2%Z))).
-
-Eval cbv in (LL.interp' LLConversions.rangeOf SimpleExample.SimplePipeline.rwvProg).
-
-Eval cbv in SimpleExample.SimplePipeline.outputBounds.
-Eval cbv in SimpleExample.SimplePipeline.valid.