diff options
author | 2015-11-20 03:29:09 -0500 | |
---|---|---|
committer | 2015-11-20 03:29:09 -0500 | |
commit | dc562d8bf9596fde07e3e3242f345c93c460982a (patch) | |
tree | 61e9aa013e98a426a7f7815e05af22444bcb6d65 /src/Specific | |
parent | 545e521740d69724430909e8a1b9059b957ed13d (diff) |
ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved carry_rep.
Diffstat (limited to 'src/Specific')
-rw-r--r-- | src/Specific/GF25519.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index a9d745501..650990252 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -71,6 +71,15 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb repeat break_or_hyp; try omega; vm_compute; reflexivity. Qed. + Lemma base_succ : forall i, ((S i) < length base)%nat -> + let b := nth_default 0 base in + b (S i) mod b i = 0. + Admitted. + + Lemma base_tail_matches_modulus: + 2^k mod nth_default 0 base (pred (length base)) = 0. + Admitted. + Lemma b0_1 : forall x, nth_default x base 0 = 1. Proof. reflexivity. |