diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-17 18:00:35 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-17 22:21:34 -0500 |
| commit | 92f64f828136f04ca88670303cd028f6f6cc7553 (patch) | |
| tree | 29092ccfe92b718c0b6950cb50a06f9a31179752 /src/Specific/GF25519BoundedAddCoordinates.v | |
| parent | c34f4e69a33dd5c22c27942a7810a0e0a9e428e2 (diff) | |
Finish proofs about eliminating useless carries
Diffstat (limited to 'src/Specific/GF25519BoundedAddCoordinates.v')
| -rw-r--r-- | src/Specific/GF25519BoundedAddCoordinates.v | 23 |
1 files changed, 1 insertions, 22 deletions
diff --git a/src/Specific/GF25519BoundedAddCoordinates.v b/src/Specific/GF25519BoundedAddCoordinates.v index ad7f44558..141c950bb 100644 --- a/src/Specific/GF25519BoundedAddCoordinates.v +++ b/src/Specific/GF25519BoundedAddCoordinates.v @@ -1,31 +1,10 @@ -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 Coq.ZArith.ZArith. Require Import Crypto.Specific.GF25519. Require Import Crypto.Specific.GF25519BoundedCommon. Require Import Crypto.Specific.GF25519ReflectiveAddCoordinates. -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. - Local Ltac bounded_t opW blem := apply blem; apply is_bounded_proj1_fe25519. |