diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-09 14:44:43 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-09 14:44:43 -0400 |
| commit | dea31a7824f569fe1c4b36186b8854709b19a042 (patch) | |
| tree | a9798698749d35f170aad307a6a319b16be3792d /src/Specific/GF25519.v | |
| parent | f133536977a4ef623d9144766a605f6ba7f65c62 (diff) | |
Tweaked structure of GF [carry_mul] so that carry chain is specified in Specific.
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index b0323c4a0..14935a184 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -37,6 +37,13 @@ Instance subCoeff : SubtractionCoefficient modulus params25519. vm_decide. Defined. +Instance carryChain : CarryChain limb_widths. + apply Build_CarryChain with (carry_chain := ([0;1;2;3;4;5;6;7;8;9;0;1])%nat). + intros. + repeat (destruct H as [|H]; [subst; vm_compute; repeat constructor | ]). + contradiction H. +Defined. + Definition freezePreconditions25519 : freezePreconditions params25519 int_width. Proof. constructor; compute_preconditions. |