From f75ee6473af2c170cb8b27b97e70797dabcc358a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 5 Sep 2024 14:46:40 +0000 Subject: [PATCH] Move secp256k1 out of End2End, remove compiler dep src/Bedrock/Secp256k1/JoyeLadder.vo (real: 574.02, user: 573.33, sys: 0.61, mem: 2376404 ko) src/Bedrock/Secp256k1/JacobianCoZ.vo (real: 407.23, user: 406.46, sys: 0.73, mem: 2358200 ko) src/Bedrock/Secp256k1/Addchain.vo (real: 158.30, user: 157.63, sys: 0.65, mem: 2284480 ko) src/Bedrock/Secp256k1/Field256k1.vo (real: 64.89, user: 64.51, sys: 0.37, mem: 1485752 ko) src/Bedrock/Everything.vo (real: 3.81, user: 3.13, sys: 0.67, mem: 1408968 ko) 1210.95user 7.12system 17:36.03elapsed 115%CPU (0avgtext+0avgdata 2376404maxresident)k --- src/Bedrock/{End2End => }/Secp256k1/Addchain.v | 7 +++---- .../{End2End => }/Secp256k1/Field256k1.v | 0 .../{End2End => }/Secp256k1/JacobianCoZ.v | 7 +++---- .../{End2End => }/Secp256k1/JoyeLadder.v | 17 ++++++++--------- 4 files changed, 14 insertions(+), 17 deletions(-) rename src/Bedrock/{End2End => }/Secp256k1/Addchain.v (98%) rename src/Bedrock/{End2End => }/Secp256k1/Field256k1.v (100%) rename src/Bedrock/{End2End => }/Secp256k1/JacobianCoZ.v (99%) rename src/Bedrock/{End2End => }/Secp256k1/JoyeLadder.v (99%) diff --git a/src/Bedrock/End2End/Secp256k1/Addchain.v b/src/Bedrock/Secp256k1/Addchain.v similarity index 98% rename from src/Bedrock/End2End/Secp256k1/Addchain.v rename to src/Bedrock/Secp256k1/Addchain.v index 67729db445a..32c7d92f8b6 100644 --- a/src/Bedrock/End2End/Secp256k1/Addchain.v +++ b/src/Bedrock/Secp256k1/Addchain.v @@ -11,16 +11,15 @@ Require Import bedrock2.Syntax. Require Import bedrock2.WeakestPrecondition. Require Import bedrock2.WeakestPreconditionProperties. Require Import bedrock2.ZnWords. -Require Import compiler.MMIO. -Require Import compiler.Pipeline. -Require Import compiler.Symbols. Require Import coqutil.Byte. Require Import coqutil.Map.Interface. +Require Import coqutil.Map.Properties. Require Import coqutil.Map.OfListWord. From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string. Require Import coqutil.Word.Bitwidth64. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Word.Interface. +Require Import coqutil.Word.Properties. Require Import Coq.Init.Byte. Require Import Coq.Lists.List. Require Import Coq.Strings.String. @@ -30,7 +29,7 @@ Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Bedrock.Field.Interface.Compilation2. Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery. Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. -Require Import Crypto.Bedrock.End2End.Secp256k1.Field256k1. +Require Import Crypto.Bedrock.Secp256k1.Field256k1. Require Import Crypto.Bedrock.Specs.Field. Require Import Crypto.Arithmetic.FLia. Require Import Crypto.Algebra.Hierarchy. diff --git a/src/Bedrock/End2End/Secp256k1/Field256k1.v b/src/Bedrock/Secp256k1/Field256k1.v similarity index 100% rename from src/Bedrock/End2End/Secp256k1/Field256k1.v rename to src/Bedrock/Secp256k1/Field256k1.v diff --git a/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v b/src/Bedrock/Secp256k1/JacobianCoZ.v similarity index 99% rename from src/Bedrock/End2End/Secp256k1/JacobianCoZ.v rename to src/Bedrock/Secp256k1/JacobianCoZ.v index f02a138dc3b..d73cea4d411 100644 --- a/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v +++ b/src/Bedrock/Secp256k1/JacobianCoZ.v @@ -11,16 +11,15 @@ Require Import bedrock2.Syntax. Require Import bedrock2.WeakestPrecondition. Require Import bedrock2.WeakestPreconditionProperties. Require Import bedrock2.ZnWords. -Require Import compiler.MMIO. -Require Import compiler.Pipeline. -Require Import compiler.Symbols. Require Import coqutil.Byte. Require Import coqutil.Map.Interface. +Require Import coqutil.Map.Properties. Require Import coqutil.Map.OfListWord. From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string. Require Import coqutil.Word.Bitwidth64. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Word.Interface. +Require Import coqutil.Word.Properties. Require Import Coq.Init.Byte. Require Import Coq.Lists.List. Require Import Coq.Strings.String. @@ -29,7 +28,7 @@ Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Bedrock.Field.Interface.Compilation2. Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery. Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. -Require Import Crypto.Bedrock.End2End.Secp256k1.Field256k1. +Require Import Crypto.Bedrock.Secp256k1.Field256k1. Require Import Crypto.Bedrock.Specs.Field. Require Import Crypto.Util.Decidable. Require Import Curves.Weierstrass.Jacobian.Jacobian. diff --git a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v b/src/Bedrock/Secp256k1/JoyeLadder.v similarity index 99% rename from src/Bedrock/End2End/Secp256k1/JoyeLadder.v rename to src/Bedrock/Secp256k1/JoyeLadder.v index cc15f56be69..09c66210009 100644 --- a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v +++ b/src/Bedrock/Secp256k1/JoyeLadder.v @@ -11,16 +11,15 @@ Require Import bedrock2.Syntax. Require Import bedrock2.WeakestPrecondition. Require Import bedrock2.WeakestPreconditionProperties. Require Import bedrock2.ZnWords. -Require Import compiler.MMIO. -Require Import compiler.Pipeline. -Require Import compiler.Symbols. Require Import coqutil.Byte. Require Import coqutil.Map.Interface. +Require Import coqutil.Map.Properties. Require Import coqutil.Map.OfListWord. From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string. Require Import coqutil.Word.Bitwidth64. Require Import coqutil.Word.Bitwidth. Require Import coqutil.Word.Interface. +Require Import coqutil.Word.Properties. Require Import Coq.Init.Byte. Require Import Coq.Lists.List. Require Import Coq.Strings.String. @@ -29,9 +28,9 @@ Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Bedrock.Field.Interface.Compilation2. Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery. Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. -Require Import Crypto.Bedrock.End2End.Secp256k1.Field256k1. -Require Import Crypto.Bedrock.End2End.Secp256k1.JacobianCoZ. -Require Import Crypto.Bedrock.End2End.Secp256k1.Addchain. +Require Import Crypto.Bedrock.Secp256k1.Field256k1. +Require Import Crypto.Bedrock.Secp256k1.JacobianCoZ. +Require Import Crypto.Bedrock.Secp256k1.Addchain. Require Import Crypto.Bedrock.Specs.Field. Require Import Crypto.Util.Decidable. Require Import Curves.Weierstrass.Jacobian.Jacobian. @@ -571,8 +570,8 @@ Section WithParameters. repeat straightline. single_step. instantiate (3 := Jacobian.of_affine P). - unfold Jacobian.of_affine, WeierstrassCurve.W.coordinates. - cbn [proj1_sig]. rewrite (sig_eta P). rewrite H15. eexists. reflexivity. + unfold Jacobian.of_affine, Jacobian.of_affine_impl, WeierstrassCurve.W.coordinates. + cbn [proj1_sig]. rewrite H15. eexists. reflexivity. 1-2: solve_bounds. repeat match goal with | H: context [Array.array ptsto _ ?a _] |- context [Field.FElem ?a _] => @@ -928,7 +927,7 @@ Section WithParameters. destruct R1' as (((?X & ?Y) & ?Z) & ?H). destruct R0' as (((?X & ?Y) & ?Z) & ?H). destruct vswap; repeat rewrite red_proj1_sig; f_equal; f_equal; ring. } - unfold Jacobian.to_affine. rewrite red_proj1_sig. + unfold Jacobian.to_affine, Jacobian.to_affine_impl. rewrite red_proj1_sig. destruct (Z.testbit k 0); [rewrite H83|rewrite H82]; match goal with | |- context [if ?test then _ else _] => destruct test