diff options
| -rw-r--r-- | src/Assembly/Assembly.v | 7 | ||||
| -rw-r--r-- | src/Curves/Curve25519.v | 6 | ||||
| -rw-r--r-- | src/Galois/GaloisField.v | 2 | ||||
| -rw-r--r-- | src/Galois/GaloisFieldTheory.v | 6 |
4 files changed, 13 insertions, 8 deletions
diff --git a/src/Assembly/Assembly.v b/src/Assembly/Assembly.v new file mode 100644 index 000000000..802d832f3 --- /dev/null +++ b/src/Assembly/Assembly.v @@ -0,0 +1,7 @@ + +Require Import Fiat.Common Fiat.Computation. +Require Import Fiat.ADTNotation Fiat.ADTRefinement. + +(* TODO (rsloan) : move datatype defs here + * This is just to make sure fiat gets imported correctly ;) + *) diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index df0b2ce06..8c34ea098 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -11,12 +11,10 @@ Module Modulus25519 <: Modulus. Definition modulus := prime25519. End Modulus25519. -Declare Module GaloisField25519 : GaloisField Modulus25519. - -Declare Module GaloisTheory25519 : GaloisFieldTheory Modulus25519 GaloisField25519. +Module GaloisTheory25519 := GaloisFieldTheory Modulus25519. Module Curve25519. - Import Modulus25519 GaloisField25519 GaloisTheory25519. + Import Modulus25519 GaloisTheory25519.Field GaloisTheory25519. (* Prove some theorems! *) End Curve25519. diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v index dfae63312..85e5f3716 100644 --- a/src/Galois/GaloisField.v +++ b/src/Galois/GaloisField.v @@ -22,7 +22,7 @@ Module Type Modulus. Parameter modulus: Prime. End Modulus. -Module Type GaloisField (M: Modulus). +Module GaloisField (M: Modulus). Import M. Definition GF := {x: Z | exists y, x = y mod modulus}. diff --git a/src/Galois/GaloisFieldTheory.v b/src/Galois/GaloisFieldTheory.v index 1a478e088..aa52d2a93 100644 --- a/src/Galois/GaloisFieldTheory.v +++ b/src/Galois/GaloisFieldTheory.v @@ -7,9 +7,9 @@ Require Export Crypto.Galois.GaloisField. Set Implicit Arguments. Unset Strict Implicits. -Module Type GaloisFieldTheory (M: Modulus) (Field: GaloisField M). - Import M. - Import Field. +Module GaloisFieldTheory (M: Modulus). + Module Field := GaloisField M. + Import M Field. (* Notations *) Notation "x {+} y" := (GFplus x y) (at level 60, right associativity). |