diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-06 18:35:31 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-06 18:35:31 -0400 |
| commit | 3c8a22e82b2162bff4d6d7b8ce813430bc859c77 (patch) | |
| tree | 1843ac9830c50ef4073dd6e04d1ec04df53e8dae /src/Specific/GF25519.v | |
| parent | c255dd3d45d9ab3e487ae5db58c14bac3a51c90c (diff) | |
ed25519: refactor some Proper
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 8aaf8caf6..044bf074b 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -51,6 +51,17 @@ Proof. compute_formula. Time Defined. +Local Transparent Let_In. +Infix "<<" := Z.shiftr (at level 50). +Infix "&" := Z.land (at level 50). +Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_mul_reduce_formula Let_In] in + fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 => proj1_sig ( + GF25519Base25Point5_mul_reduce_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9). +Local Opaque Let_In. + + Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula. (* It's easy enough to use extraction to get the proper nice-looking formula. * More Ltac acrobatics will be needed to get out that formula for further use in Coq. |