diff options
| author |  Robert Sloan <varomodt@google.com> | 2016-10-18 22:07:24 -0700 |
|---|---|---|
| committer | Robert Sloan <varomodt@google.com> | 2016-10-18 22:07:24 -0700 |
| commit | ff878dbde61374e42235b10d85c5fec2ab22e7d1 (patch) | |
| tree | 4151a06594a82b21300c6dbcb6485497ca2c9d1d /src/Assembly/GF25519.v | |
| parent | f8680ec8e73f8acb39cb55f6e616a0e5d10347f8 (diff) | |
Fast bounds-checking machinery but lower-bounds are broken
Diffstat (limited to 'src/Assembly/GF25519.v')
| -rw-r--r-- | src/Assembly/GF25519.v | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index 9723c75a0..80d9044c4 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -17,10 +17,9 @@ Module GF25519. Section DefaultBounds. Import ListNotations. - Local Notation rr exp := - (orElse any (make (n := bits) 0 (wzero _) (2^exp + 2^exp/10)%N)). + Local Notation rr exp := (range N 0%N (2^exp + 2^exp/10)%N). - Definition feBound: list (@BoundedWord bits) := + Definition feBound: list (Range N) := [rr 26; rr 27; rr 26; rr 27; rr 26; rr 27; rr 26; rr 27; rr 26; rr 27]. End DefaultBounds. @@ -40,7 +39,7 @@ Module GF25519. Definition inputs: nat := 20. Definition width: Width bits := width. Definition ResultType := FE. - Definition inputBounds: list (@BoundedWord bits) := feBound ++ feBound. + Definition inputBounds := feBound ++ feBound. Definition ge25519_add_expr := Eval cbv beta delta [fe25519 add mul sub Let_In] in add. @@ -93,7 +92,7 @@ Module GF25519. Definition inputs: nat := 20. Definition width: Width bits := width. Definition ResultType := FE. - Definition inputBounds: list (@BoundedWord bits) := feBound ++ feBound. + Definition inputBounds := feBound ++ feBound. Definition ge25519_sub_expr := Eval cbv beta delta [fe25519 add mul sub Let_In] in sub. @@ -146,7 +145,7 @@ Module GF25519. Definition inputs: nat := 20. Definition width: Width bits := width. Definition ResultType := FE. - Definition inputBounds: list (@BoundedWord bits) := feBound ++ feBound. + Definition inputBounds := feBound ++ feBound. Definition ge25519_mul_expr := Eval cbv beta delta [fe25519 add mul sub Let_In] in mul. @@ -199,7 +198,7 @@ Module GF25519. Definition inputs: nat := 10. Definition width: Width bits := width. Definition ResultType := FE. - Definition inputBounds: list (@BoundedWord bits) := feBound. + Definition inputBounds := feBound. Definition ge25519_opp_expr := Eval cbv beta delta [fe25519 add mul sub opp Let_In] in opp. @@ -256,4 +255,4 @@ End GF25519. Extraction "GF25519Add" GF25519.Add. Extraction "GF25519Sub" GF25519.Sub. Extraction "GF25519Mul" GF25519.Mul. -Extraction "GF25519Opp" GF25519.Opp. +Extraction "GF25519Opp" GF25519.Opp.
\ No newline at end of file |