diff options
| -rw-r--r-- | _CoqProject | 12 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified.v | 13 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/Add.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarryAdd.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarryOpp.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarrySub.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/Freeze.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/GeModulus.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/Mul.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/Opp.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/Pack.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/Sub.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/Unpack.v | 3 |
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. |