diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-20 03:13:59 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 03:13:59 -0400 |
| commit | aafcec91728330c79d74f4c984729cf3aadc3605 (patch) | |
| tree | 8699975633a47b5d1929014af1e14eb19ecd1993 /src/Specific/GF25519.v | |
| parent | a7c3e57cb7c3280dfec3a95b18dec83ee6e6d4f4 (diff) | |
| parent | b41ac7998a11354618b122874c03bc68c2833a94 (diff) | |
Merge branch 'field-experiment'
includes broken files to be removed in next commit
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 8ee9b25d8..7e0e815e5 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -59,6 +59,17 @@ Proof. exact Hfg. 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. |