diff options
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index fdef4898b..b69d4224e 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -743,3 +743,31 @@ Definition unpack (f : wire_digits) : fe25519 := Definition unpack_correct (f : wire_digits) : unpack f = unpack_opt params25519 wire_widths_nonneg bits_eq f := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f). + +Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. +Definition edwards_extended_add_coordinates td P Q := +Eval cbv iota beta delta [ + Extended.add_coordinates + add sub mul + ] in + (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). +Print edwards_extended_add_coordinates. + +Local Existing Instance field25519. +Create HintDb edwards_extended_add_coordinates_correct discriminated. +Hint Rewrite + (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_decode)) + (Ring.homomorphism_add(H1 :=homomorphism_F25519_decode)) + (Ring.homomorphism_sub(H1 :=homomorphism_F25519_decode)) + : edwards_extended_add_coordinates_correct . +Lemma edwards_extended_add_coordinates_correct td P Q : + Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q) + = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)). +Proof. + change (edwards_extended_add_coordinates td P Q) + with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q). + destruct_head' prod. + simpl. + rewrite_strat topdown hints edwards_extended_add_coordinates_correct. + reflexivity. +Qed.
\ No newline at end of file |