Merge branch 'rsloan-phoas' of github.com:mit-plv/fiat-crypto into rsloan-phoas

6 files changed, 57 insertions, 14 deletions

diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v
index 91eb37a16..e072342a5 100644
--- a/src/Assembly/Compile.v
+++ b/src/Assembly/Compile.v
@@ -9,6 +9,8 @@ Require Import Crypto.Assembly.QhasmEvalCommon.
 Require Import Crypto.Assembly.QhasmCommon.
 Require Import Crypto.Assembly.Qhasm.
 
+Local Arguments LetIn.Let_In _ _ _ _ / .
+
 Module CompileHL.
   Section Compilation.
     Context {T: Type}.
@@ -281,11 +283,12 @@ Module CompileLL.
         (fun rt var op x y out => Some out)
         (fun t' a => Some (vars a)).
 
-    Fixpoint fillInputs {t inputs} (prog: NAry inputs Z (WExpr t)) {struct inputs}: WExpr t :=
+    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 (Z.of_nat inputs))
+      | S inputs'' => fun p => @fillInputs _ _ (p (Z.of_nat inputs))
       end prog.
+    Global Arguments fillInputs {t inputs} _.
 
     Definition compile {t inputs} (p: NAry inputs Z (WExpr t)): option (Program * list nat) :=
       let p' := fillInputs p in
diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v
index e4ea4b5d1..c24cf618f 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -18,6 +18,8 @@ Require Import Coq.NArith.Nnat Coq.NArith.Ndigits.
 
 Require Import Coq.Bool.Sumbool.
 
+Local Arguments LetIn.Let_In _ _ _ _ / .
+
 Definition typeMap {A B t} (f: A -> B) (x: @interp_type A t): @interp_type B t.
 Proof.
   induction t; [refine (f x)|].
@@ -282,7 +284,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;
-          kill_dec; simpl; kill_dec; simpl; try abstract (intro Z; inversion Z);
+          break_match; simpl; try break_match; simpl; try abstract (intro Z; inversion Z);
           pose proof (Npow2_gt0 n); simpl in *; nomega.
       Qed.
 
@@ -361,7 +363,7 @@ Module LLConversions.
               kill_dec; simpl in *; kill_dec; first [reflexivity|nomega]. *)
 
           + unfold bcheck, getBounds in *.
-            replace (interp_binop op _ _)
+            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)))).
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v
index 8d68ac696..c4aa56175 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -13,7 +13,7 @@ Section BaseTypes.
   Record RangeWithValue := rwv {
     rwv_low: N;
     rwv_value: N;
-    rwv_high: N;
+    rwv_high: N
   }.
 
   Record BoundedWord {n} := bounded {
@@ -23,7 +23,7 @@ Section BaseTypes.
 
     ge_low: (bw_low <= wordToN bw_value)%N;
     le_high: (wordToN bw_value <= bw_high)%N;
-    high_bound: (bw_high < Npow2 n)%N;
+    high_bound: (bw_high < Npow2 n)%N
   }.
 End BaseTypes.
 
@@ -652,11 +652,11 @@ Section BoundedWord.
     eand := fun x y => omap x (fun X => omap y (fun Y => bapp range_and_valid X Y));
 
     eltb := fun x y =>
-      orElse false (omap x (fun X => omap y (fun Y => 
+      orElse false (omap x (fun X => omap y (fun 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 => 
+      orElse false (omap x (fun X => omap y (fun Y =>
         Some (N.eqb (wordToN (bw_value X)) (wordToN (bw_value Y))))))
   }.
 End BoundedWord.
@@ -729,7 +729,7 @@ Section RangeWithValue.
       | (Some (rwv xlow xv xhigh), Some (rwv ylow yv yhigh)) =>
           N.ltb xv yv
 
-      | _ => false 
+      | _ => false
       end;
 
     eeqb := fun x y =>
@@ -738,6 +738,6 @@ Section RangeWithValue.
           andb (andb (N.eqb xlow ylow) (N.eqb xhigh yhigh)) (N.eqb xv yv)
 
       | _ => false
-      end;
+      end
   }.
 End RangeWithValue.
diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v
index 83b0dd4bf..07c074f5e 100644
--- a/src/Assembly/GF25519BoundedInstantiation.v
+++ b/src/Assembly/GF25519BoundedInstantiation.v
@@ -7,6 +7,7 @@ Require Import Crypto.Assembly.GF25519.
 Require Import Crypto.Specific.GF25519.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tuple.
 
 (* Totally fine to edit these definitions; DO NOT change the type signatures at all *)
@@ -43,6 +44,39 @@ Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W ->
   := interp_uexpr'.
 Axiom rfreeze : ExprUnOp.
 
+Declare Reduction asm_interp
+  := cbv [id
+            interp_bexpr interp_uexpr interp_bexpr' interp_uexpr'
+            radd rsub rmul ropp (*rfreeze*)
+            GF25519.GF25519.Add.wordProg GF25519.GF25519.AddExpr.bits GF25519.GF25519.Add.llProg GF25519.GF25519.AddExpr.hlProg GF25519.GF25519.AddExpr.inputs
+            GF25519.GF25519.Sub.wordProg GF25519.GF25519.SubExpr.bits GF25519.GF25519.Sub.llProg GF25519.GF25519.SubExpr.hlProg GF25519.GF25519.SubExpr.inputs
+            GF25519.GF25519.Mul.wordProg GF25519.GF25519.MulExpr.bits GF25519.GF25519.Mul.llProg GF25519.GF25519.MulExpr.hlProg GF25519.GF25519.MulExpr.inputs
+            GF25519.GF25519.Opp.wordProg GF25519.GF25519.OppExpr.bits GF25519.GF25519.Opp.llProg GF25519.GF25519.OppExpr.hlProg GF25519.GF25519.OppExpr.inputs
+            (*GF25519.GF25519.Freeze.wordProg GF25519.GF25519.FreezeExpr.bits GF25519.GF25519.Freeze.llProg GF25519.GF25519.FreezeExpr.hlProg GF25519.GF25519.FreezeExpr.inputs *)
+            GF25519.GF25519.bits GF25519.GF25519.FE
+            QhasmCommon.liftN QhasmCommon.NArgMap Compile.CompileHL.compile LL.LL.under_lets LL.LL.interp LL.LL.interp_arg LL.LL.match_arg_Prod Conversions.LLConversions.convertZToWord Conversions.LLConversions.convertExpr Conversions.LLConversions.convertArg Conversions.LLConversions.convertVar PhoasCommon.type_rect PhoasCommon.type_rec PhoasCommon.type_ind PhoasCommon.interp_binop LL.LL.uninterp_arg
+            Evaluables.ezero Evaluables.toT Evaluables.fromT Evaluables.eadd Evaluables.esub Evaluables.emul Evaluables.eshiftr Evaluables.eand Evaluables.eltb Evaluables.eeqb
+            Evaluables.WordEvaluable Evaluables.ZEvaluable].
+
+Definition interp_radd : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+  := Eval asm_interp in interp_bexpr radd.
+Print interp_radd.
+Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
+Definition interp_rsub : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+  := Eval asm_interp in interp_bexpr rsub.
+(*Print interp_rsub.*)
+Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
+Definition interp_rmul : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+  := Eval asm_interp in interp_bexpr rmul.
+(*Print interp_rmul.*)
+Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
+Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+  := Eval asm_interp in interp_uexpr ropp.
+Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
+Definition interp_rfreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+  := Eval asm_interp in interp_uexpr rfreeze.
+Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl.
+
 Local Notation binop_correct_and_bounded rop op
   := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing).
 Local Notation unop_correct_and_bounded rop op
diff --git a/src/Assembly/HL.v b/src/Assembly/HL.v
index 14ca2edca..2107b7f0a 100644
--- a/src/Assembly/HL.v
+++ b/src/Assembly/HL.v
@@ -1,5 +1,6 @@
 Require Import Crypto.Assembly.PhoasCommon.
 Require Import Coq.setoid_ring.InitialRing.
+Require Import Crypto.Util.LetIn.
 
 Module HL.
   Section Language.
@@ -27,7 +28,7 @@ Module HL.
         | Const n => n
         | Var _ n => n
         | Binop _ _ _ op e1 e2 => interp_binop op (interp e1) (interp e2)
-        | Let _ ex _ eC => let x := interp ex in interp (eC x)
+        | Let _ ex _ eC => dlet x := interp ex in interp (eC x)
         | Pair _ e1 _ e2 => (interp e1, interp e2)
         | MatchPair _ _ ep _ eC => let (v1, v2) := interp ep in interp (eC v1 v2)
         end.
diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v
index fd0a92f96..e0588214c 100644
--- a/src/Assembly/LL.v
+++ b/src/Assembly/LL.v
@@ -1,4 +1,7 @@
 Require Import Crypto.Assembly.PhoasCommon.
+Require Import Crypto.Util.LetIn.
+
+Local Arguments Let_In / _ _ _ _.
 
 Module LL.
   Section Language.
@@ -61,7 +64,7 @@ Module LL.
         match x' with
         | (x0, x1) => Pair (uninterp_arg_as_var x0) (uninterp_arg_as_var x1)
         end
-      | TT => Var 
+      | TT => Var
       end x.
 
     Fixpoint interp' {V t} (f: V -> T) (e:expr t) : interp_type t :=
@@ -74,7 +77,7 @@ Module LL.
     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))
+        dlet x := interp_binop op (interp_arg a) (interp_arg b) in interp (eC (uninterp_arg x))
       | Return _ a => interp_arg a
       end.
 
@@ -153,7 +156,7 @@ Module LL.
     induction t as [|i0 v0 i1 v1]; simpl; intros; try reflexivity.
     break_match; subst; simpl.
     unfold interp_arg in *.
-    cbn; rewrite v0, v1; reflexivity.
+    simpl; rewrite v0, v1; reflexivity.
   Qed.
 
   Lemma interp_under_lets {T} {_: Evaluable T} {t: type} {tC: type}