diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-15 14:36:39 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-15 14:36:39 -0500 |
| commit | 949d85496b76c22931cf3aa975b7b719beb6c200 (patch) | |
| tree | 3653a563faf910d1a710ec8744f5266d3239e56e /src/Specific | |
| parent | 5b907ea0099b312864264d181ca7b1dd71d1673b (diff) | |
ported some of EdDSA25519 to new field framework
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/EdDSA25519.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v index d037339b4..242661bc5 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -89,13 +89,15 @@ Module EdDSA25519_Params <: EdDSAParams. + auto. + pose proof q_odd; unfold q in *; omega. + apply div2_p_1mod4; auto. - + apply nonzero_range; auto. + + rewrite GF_Zmod. + apply nonzero_range; auto. + rewrite GFexp_Zpow in A by (auto || apply Z_div_pos; prime_bound). rewrite inject_mod_eq in A. apply gf_eq in A. replace (GFToZ 1) with 1%Z in A by auto. rewrite GFToZ_inject in A. rewrite Z.mod_mod in A by auto. + rewrite GF_Zmod. exact A. } { rewrite GFexp_Zpow by first [apply Z.div_pos; pose proof q_odd; omega | auto]. @@ -104,7 +106,8 @@ Module EdDSA25519_Params <: EdDSAParams. rewrite GFToZ_inject. apply euler_criterion; auto. + apply nonzero_range; auto. - + apply square_Zmod_GF; auto. + + rewrite <- GF_Zmod. + apply square_Zmod_GF; auto. } Qed. |