Skip to content

Commit

Permalink
Move secp256k1 out of End2End, remove compiler dep
Browse files Browse the repository at this point in the history 
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
  • Loading branch information
@andres-erbsen
andres-erbsen committed Oct 29, 2024
1 parent b2d3126 commit b240a3b
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 17 deletions.
7 changes: 3 additions & 4 deletions src/Bedrock/End2End/Secp256k1/Addchain.v → src/Bedrock/Secp256k1/Addchain.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand Down
0 src/Bedrock/End2End/Secp256k1/Field256k1.v → src/Bedrock/Secp256k1/Field256k1.v
View file
File renamed without changes.
7 changes: 3 additions & 4 deletions src/Bedrock/End2End/Secp256k1/JacobianCoZ.v → src/Bedrock/Secp256k1/JacobianCoZ.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand Down
17 changes: 8 additions & 9 deletions src/Bedrock/End2End/Secp256k1/JoyeLadder.v → src/Bedrock/Secp256k1/JoyeLadder.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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 _] =>
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit b240a3b

Please sign in to comment.