diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 14:23:43 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 14:23:43 -0400 |
| commit | 1b9f8c10fef9b8cff935deda8e89b8351703b119 (patch) | |
| tree | 797cebc62ca59d259bade2306aad1aabf8cf3531 /src/Specific/GF25519Reflective/Reified | |
| parent | 94793ff420b2d0af6da59eba882e5614abe7e3e3 (diff) | |
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.
Diffstat (limited to 'src/Specific/GF25519Reflective/Reified')
| -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 |
11 files changed, 33 insertions, 0 deletions
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. |