diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-24 23:11:27 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-24 23:11:41 -0400 |
| commit | dfcae14436538ff9196b92061603ed832947f6af (patch) | |
| tree | 9e0a3236f1f0a27563551cf94d4247f25ef9b357 /src/Specific/GF25519.v | |
| parent | 3e980c7a7cd6c6084bf763bd9b748c20fc37f649 (diff) | |
Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implementation, and pushed that up through Specific.
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index c8ea2e571..3a96b2669 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -260,6 +260,24 @@ Proof. reflexivity. Defined. +Definition opp_sig (f : fe25519) : + { g : fe25519 | g = opp_opt f }. +Proof. + eexists. + cbv [opp_opt]. + rewrite <-sub_correct. + rewrite zero_subst. + cbv [sub]. + reflexivity. +Defined. + +Definition opp (f : fe25519) : fe25519 + := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f). + +Definition opp_correct (f : fe25519) + : opp f = opp_opt f + := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f). + Definition inv (f : fe25519) : fe25519 := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f). @@ -287,7 +305,7 @@ Proof. + intros; rewrite sub_correct, sub_opt_correct; reflexivity. + intros; rewrite add_correct, add_opt_correct; reflexivity. + intros; rewrite inv_correct, inv_opt_correct; reflexivity. - + reflexivity. + + intros; rewrite opp_correct, opp_opt_correct; reflexivity. Qed. Lemma homomorphism_F25519 : |