Tactics to manually remove Z.to/of_N and such

1 files changed, 75 insertions, 2 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.
+