Add reification of various operations

We split the reification up into separate files, one operation per file,
so that we can run all the reification in parallel when building.

13 files changed, 58 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 763f205e8..5803b3735 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -143,6 +143,18 @@ src/Specific/FancyMachine256/Barrett.v
 src/Specific/FancyMachine256/Core.v
 src/Specific/FancyMachine256/Montgomery.v
 src/Specific/GF25519Reflective/Common.v
+src/Specific/GF25519Reflective/Reified.v
+src/Specific/GF25519Reflective/Reified/Add.v
+src/Specific/GF25519Reflective/Reified/CarryAdd.v
+src/Specific/GF25519Reflective/Reified/CarryOpp.v
+src/Specific/GF25519Reflective/Reified/CarrySub.v
+src/Specific/GF25519Reflective/Reified/Freeze.v
+src/Specific/GF25519Reflective/Reified/GeModulus.v
+src/Specific/GF25519Reflective/Reified/Mul.v
+src/Specific/GF25519Reflective/Reified/Opp.v
+src/Specific/GF25519Reflective/Reified/Pack.v
+src/Specific/GF25519Reflective/Reified/Sub.v
+src/Specific/GF25519Reflective/Reified/Unpack.v
 src/Tactics/VerdiTactics.v
 src/Tactics/Algebra_syntax/Nsatz.v
 src/Test/Curve25519SpecTestVectors.v
diff --git a/src/Specific/GF25519Reflective/Reified.v b/src/Specific/GF25519Reflective/Reified.v
new file mode 100644
index 000000000..98edc1282
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified.v
@@ -0,0 +1,13 @@
+(** We split the reification up into separate files, one operation per
+    file, so that it can run in parallel. *)
+Require Export Crypto.Specific.GF25519Reflective.Reified.Add.
+Require Export Crypto.Specific.GF25519Reflective.Reified.CarryAdd.
+Require Export Crypto.Specific.GF25519Reflective.Reified.Sub.
+Require Export Crypto.Specific.GF25519Reflective.Reified.CarrySub.
+Require Export Crypto.Specific.GF25519Reflective.Reified.Mul.
+Require Export Crypto.Specific.GF25519Reflective.Reified.Opp.
+Require Export Crypto.Specific.GF25519Reflective.Reified.CarryOpp.
+Require Export Crypto.Specific.GF25519Reflective.Reified.Freeze.
+Require Export Crypto.Specific.GF25519Reflective.Reified.GeModulus.
+Require Export Crypto.Specific.GF25519Reflective.Reified.Pack.
+Require Export Crypto.Specific.GF25519Reflective.Reified.Unpack.
diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v
new file mode 100644
index 000000000..0babb591f
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Add.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition raddZ_sig : rexpr_binop_sig add. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
new file mode 100644
index 000000000..f3c65a02b
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rcarry_addZ_sig : rexpr_binop_sig carry_add. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
new file mode 100644
index 000000000..11356deeb
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rcarry_oppZ_sig : rexpr_unop_sig carry_opp. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v
new file mode 100644
index 000000000..a77a67909
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rcarry_subZ_sig : rexpr_binop_sig carry_sub. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v
new file mode 100644
index 000000000..9ea71132b
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Freeze.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rfreezeZ_sig : rexpr_unop_sig freeze. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/GeModulus.v b/src/Specific/GF25519Reflective/Reified/GeModulus.v
new file mode 100644
index 000000000..225faacce
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rge_modulusZ_sig : rexpr_unop_FEToZ_sig ge_modulus. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v
new file mode 100644
index 000000000..c298b3563
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Mul.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rmulZ_sig : rexpr_binop_sig mul. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v
new file mode 100644
index 000000000..7a625b4e1
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Opp.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition roppZ_sig : rexpr_unop_sig opp. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v
new file mode 100644
index 000000000..a645ee6e4
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Pack.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rpackZ_sig : rexpr_unop_FEToWire_sig pack. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v
new file mode 100644
index 000000000..2695da171
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Sub.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition rsubZ_sig : rexpr_binop_sig sub. Proof. reify_sig. Defined.
diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v
new file mode 100644
index 000000000..4e7cba388
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/Unpack.v
@@ -0,0 +1,3 @@
+Require Import Crypto.Specific.GF25519Reflective.Common.
+
+Definition runpackZ_sig : rexpr_unop_WireToFE_sig unpack. Proof. reify_sig. Defined.