diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-03 20:25:30 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-03 20:30:04 -0400 |
| commit | bc0239c0f6f5bafcf264cbabf3d783ca1146360d (patch) | |
| tree | c0737b1b8f9b86e0e9b43d84f8e66ab926ca54de /src/Specific/GF25519Bounded.v | |
| parent | e776995e4eb910e778a608cd0d5e3e52e1c36392 (diff) | |
separate Ed25519Extraction.v, add extraction to Makefile
@JasonGross: src/Specific/GF25519Bounded.v has another constant that I
think needs a extraction-friendly version, I added a comment
Diffstat (limited to 'src/Specific/GF25519Bounded.v')
| -rw-r--r-- | src/Specific/GF25519Bounded.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v index 0ce49f1c0..2d83b8dbd 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -172,6 +172,7 @@ Proof. exact (proj2_sig (eqbW_sig f' g')). Qed. +(* TODO(jgross): use NToWord or such for this constant too *) Definition sqrt_m1W : fe25519W := Eval vm_compute in fe25519ZToW sqrt_m1. |