diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2015-11-10 11:31:59 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2015-11-10 11:31:59 -0500 |
| commit | 23198db0816fa4ca97dbb1d0599d2524e7531520 (patch) | |
| tree | e85917d1ad23bd4f312b00236422d57db247e008 /src/Specific/GF25519.v | |
| parent | f5b35696b789fdd427823eefecad2eb5428e70bf (diff) | |
BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs (first element of base is 1).
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 722b1bde4..a9d745501 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -12,6 +12,12 @@ Module Base25Point5_10limbs <: BaseCoefs. Proof. compute; intros; repeat break_or_hyp; intuition. Qed. + + Lemma b0_1 : forall x, nth_default x base 0 = 1. + Proof. + reflexivity. + Qed. + Lemma base_good : forall i j, (i+j < length base)%nat -> let b := nth_default 0 base in @@ -65,8 +71,7 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb repeat break_or_hyp; try omega; vm_compute; reflexivity. Qed. - - Lemma b0_1 : nth_default 0 base 0 = 1. + Lemma b0_1 : forall x, nth_default x base 0 = 1. Proof. reflexivity. Qed. |