Tactics to manually remove Z.to/of_N and such

3 files changed, 86 insertions, 20 deletions

diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 5011237ee..00a76c391 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -1,3 +1,6 @@
+Require Import Coq.ZArith.Znat.
+Require Import Coq.ZArith.ZArith.
+
 Require Import Crypto.Assembly.Pipeline.
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.ModularBaseSystem.
@@ -19,7 +22,7 @@ Module GF25519.
   Section DefaultBounds.
     Import ListNotations.
 
-    Local Notation rr exp := (2^exp + 2^exp/10)%Z.
+    Local Notation rr exp := (2^exp + 2^(exp-3))%Z.
 
     Definition feBound: list Z :=
       [rr 26; rr 27; rr 26; rr 27; rr 26;
@@ -221,9 +224,79 @@ Module GF25519.
   Module Sub := Pipeline SubExpr.
   Module Mul := Pipeline MulExpr.
   Module Opp := Pipeline OppExpr.
+
+  Section Instantiation.
+    Require Import InitialRing.
+
+    Definition Binary : Type := NAry 20 (word bits) (@interp_type (word bits) FE).
+    Definition Unary : Type := NAry 10 (word bits) (@interp_type (word bits) FE).
+
+    Ltac ast_simpl := cbv [
+      Add.bits Add.inputs AddExpr.inputs Add.ResultType AddExpr.ResultType
+      Add.W Add.R Add.ZEvaluable Add.WEvaluable Add.REvaluable
+      Add.AST.progW Add.LL.progW Add.HL.progW AddExpr.prog
+
+      Sub.bits Sub.inputs SubExpr.inputs Sub.ResultType SubExpr.ResultType
+      Sub.W Sub.R Sub.ZEvaluable Sub.WEvaluable Sub.REvaluable
+      Sub.AST.progW Sub.LL.progW Sub.HL.progW SubExpr.prog
+
+      Mul.bits Mul.inputs MulExpr.inputs Mul.ResultType MulExpr.ResultType
+      Mul.W Mul.R Mul.ZEvaluable Mul.WEvaluable Mul.REvaluable
+      Mul.AST.progW Mul.LL.progW Mul.HL.progW MulExpr.prog
+
+      Opp.bits Opp.inputs OppExpr.inputs Opp.ResultType OppExpr.ResultType
+      Opp.W Opp.R Opp.ZEvaluable Opp.WEvaluable Opp.REvaluable
+      Opp.AST.progW Opp.LL.progW Opp.HL.progW OppExpr.prog
+
+      HLConversions.convertExpr CompileHL.Compile CompileHL.compile
+
+      LL.interp LL.uninterp_arg LL.under_lets LL.interp_arg
+
+      ZEvaluable WordEvaluable RWVEvaluable rwv_value
+      eadd esub emul eand eshiftr toT fromT
+
+      interp_binop interp_type FE liftN NArgMap id
+      omap option_map orElse].
+
+    (* Tack this on to make a simpler AST, but it really slows us down *)
+    Ltac word_simpl := cbv [
+      AddExpr.bits SubExpr.bits MulExpr.bits OppExpr.bits bits
+      NToWord posToWord natToWord wordToNat wordToN wzero'
+      Nat.mul Nat.add].
+
+    Ltac lift :=
+      repeat (apply functional_extensionality; intro).
+
+    Ltac kill_conv := let p := fresh in
+      pose proof N2Z.id as p; unfold Z.to_N in p;
+      repeat rewrite p; clear p;
+      repeat rewrite NToWord_wordToN.
+
+    Definition add' : {f: Binary |
+      f = NArgMap (fun x => Z.of_N (wordToN x)) Add.AST.progW }.
+    Proof. eexists; ast_simpl; lift; kill_conv; reflexivity. Defined.
+
+    Definition sub' : {f: Binary |
+      f = NArgMap (fun x => Z.of_N (wordToN x)) Sub.AST.progW }.
+    Proof. eexists; ast_simpl; lift; kill_conv; reflexivity. Defined.
+
+    Definition mul' : {f: Binary |
+      f = NArgMap (fun x => Z.of_N (wordToN x)) Mul.AST.progW }.
+    Proof. eexists; ast_simpl; lift; kill_conv; reflexivity. Defined.
+
+    Definition opp' : {f: Unary |
+      f = NArgMap (fun x => Z.of_N (wordToN x)) Opp.AST.progW }.
+    Proof. eexists; ast_simpl; lift; kill_conv; reflexivity. Defined.
+
+    Definition add := Eval simpl in proj1_sig add'.
+    Definition sub := Eval simpl in proj1_sig sub'.
+    Definition mul := Eval simpl in proj1_sig mul'.
+    Definition opp := Eval simpl in proj1_sig opp'.
+  End Instantiation.
 End GF25519.
 
 Extraction "GF25519Add" GF25519.Add.
 Extraction "GF25519Sub" GF25519.Sub.
 Extraction "GF25519Mul" GF25519.Mul.
-Extraction "GF25519Opp" GF25519.Opp.
\ No newline at end of file
+Extraction "GF25519Opp" GF25519.Opp.
+
diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v
index 07c074f5e..b12694067 100644
--- a/src/Assembly/GF25519BoundedInstantiation.v
+++ b/src/Assembly/GF25519BoundedInstantiation.v
@@ -15,26 +15,24 @@ Section Operations.
   Import Assembly.GF25519.GF25519.
   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).
+  Definition ExprBinOp : Type := GF25519.Binary.
+  Definition ExprUnOp : Type := GF25519.Unary.
 
   Local 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.
+    op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9.
 
   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.
+    op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
 
-  Definition radd : ExprBinOp := GF25519.Add.wordProg.
-  Definition ropp : ExprUnOp := GF25519.Opp.wordProg.
+  Definition radd : ExprBinOp := GF25519.add.
+  Definition rsub : ExprBinOp := GF25519.sub.
+  Definition rmul : ExprBinOp := GF25519.mul.
+  Definition ropp : ExprUnOp := GF25519.opp.
 End Operations.
 
 
@@ -47,14 +45,10 @@ 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 *)
+            radd rsub rmul ropp
+            GF25519.GF25519.add GF25519.GF25519.sub GF25519.GF25519.mul GF25519.GF25519.opp
             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
+            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.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].
 
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index 8eaa07161..5dc3b28bf 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -138,4 +138,3 @@ Module SimpleExample.
 
   Module SimplePipeline := Pipeline SimpleExpression.
 End SimpleExample.
-