diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-17 17:50:08 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-17 17:50:08 -0500 |
| commit | e26c7b5c99eb0bdba0dad274091f6121e2c388a3 (patch) | |
| tree | 313fb47132a24d192c68a7cc5d7fbfd516c6631b /src/Specific | |
| parent | c0f14ebdacb8f6543b5b136f3c6d69690c8a2225 (diff) | |
Add GF25519BoundedExtendedAddCoordinates
The lemma is currently admitted
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519BoundedAddCoordinates.v | 2 | ||||
| -rw-r--r-- | src/Specific/GF25519BoundedExtendedAddCoordinates.v | 41 |
2 files changed, 41 insertions, 2 deletions
diff --git a/src/Specific/GF25519BoundedAddCoordinates.v b/src/Specific/GF25519BoundedAddCoordinates.v index 85f90c754..ad7f44558 100644 --- a/src/Specific/GF25519BoundedAddCoordinates.v +++ b/src/Specific/GF25519BoundedAddCoordinates.v @@ -6,9 +6,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. Require Import Crypto.Specific.GF25519. -Require Import Crypto.Specific.GF25519ExtendedAddCoordinates. Require Import Crypto.Specific.GF25519BoundedCommon. -Require Import Crypto.Specific.GF25519Reflective. Require Import Crypto.Specific.GF25519ReflectiveAddCoordinates. Require Import Bedrock.Word Crypto.Util.WordUtil. Require Import Coq.Lists.List Crypto.Util.ListUtil. diff --git a/src/Specific/GF25519BoundedExtendedAddCoordinates.v b/src/Specific/GF25519BoundedExtendedAddCoordinates.v new file mode 100644 index 000000000..38449bd51 --- /dev/null +++ b/src/Specific/GF25519BoundedExtendedAddCoordinates.v @@ -0,0 +1,41 @@ +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.Specific.GF25519. +Require Import Crypto.Specific.GF25519Bounded. +Require Import Crypto.Specific.GF25519ExtendedAddCoordinates. +Require Import Crypto.Specific.GF25519BoundedAddCoordinates. +Require Import Bedrock.Word Crypto.Util.WordUtil. +Require Import Coq.Lists.List Crypto.Util.ListUtil. +Require Import Crypto.ModularArithmetic.ModularBaseSystemWord. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.HList. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Algebra. +Import ListNotations. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Local Open Scope Z. + +Lemma fieldwise_eq_extended_add_coordinates_full' twice_d P10 P11 P12 P13 P20 P21 P22 P23 + : Tuple.fieldwise + (n:=4) GF25519BoundedCommon.eq + (@GF25519BoundedAddCoordinates.add_coordinates + twice_d P10 P11 P12 P13 P20 P21 P22 P23) + (@ExtendedCoordinates.Extended.add_coordinates + GF25519BoundedCommon.fe25519 + GF25519Bounded.add GF25519Bounded.sub GF25519Bounded.mul twice_d + (P10, P11, P12, P13) (P20, P21, P22, P23)). +Proof. + unfold GF25519BoundedCommon.eq. + pose (add_coordinates_correct). +Admitted. |