Skip to content

Commit

Permalink
Add UnsaturatedSolinasHeuristics/Tests.v
Browse files Browse the repository at this point in the history 
<details><summary>Timing Diff</summary>
<p>

```
   After |  Peak Mem | File Name                             |   Before | Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
-------------------------------------------------------------------------------------------------------------------------------------------
0m25.96s | 566428 ko | Total Time / Peak Mem                 | 0m00.00s |     0 ko || +0m25.96s ||    566428 ko |   N/A    |              ∞
-------------------------------------------------------------------------------------------------------------------------------------------
0m25.97s | 566428 ko | UnsaturatedSolinasHeuristics/Tests.vo |   N/A    |   N/A    || +0m25.96s ||    566428 ko |        ∞ |              ∞

```
</p>
  • Loading branch information
@JasonGross
JasonGross committed May 23, 2020
1 parent 493b5fd commit b5d9ba0
Show file tree
Hide file tree
Showing 4 changed files with 224 additions and 2 deletions.
6 changes: 4 additions & 2 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,8 @@ JAVA_EXTRA_ARGS_32 := $(JAVA_EXTRA_ARGS_ALL)

OUTPUT_VOS := \
src/Fancy/Montgomery256.vo \
src/Fancy/Barrett256.vo
src/Fancy/Barrett256.vo \
src/UnsaturatedSolinasHeuristics/Tests.vo

OUTPUT_PREOUTS := \
Crypto.Fancy.Montgomery256.Prod.MontRed256 \
Expand All @@ -189,7 +190,8 @@ OUTPUT_PREOUTS := \
Crypto.Fancy.Barrett256.Prod.MulMod \
Crypto.Fancy.Barrett256.prod_barrett_red256_correct \
Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions \
Crypto.Fancy.Barrett256.barrett_red256
Crypto.Fancy.Barrett256.barrett_red256 \
Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs

CHECK_OUTPUTS := $(addprefix check-,$(OUTPUT_PREOUTS))
ACCEPT_OUTPUTS := $(addprefix accept-,$(OUTPUT_PREOUTS))
Expand Down
1 change: 1 addition & 0 deletions _CoqProject
View file
Original file line number Diff line number Diff line change
Expand Up @@ -159,6 +159,7 @@ src/Stringification/IR.v
src/Stringification/Java.v
src/Stringification/Language.v
src/Stringification/Rust.v
src/UnsaturatedSolinasHeuristics/Tests.v
src/Util/AdditionChainExponentiation.v
src/Util/Arg.v
src/Util/AutoRewrite.v
Expand Down
62 changes: 62 additions & 0 deletions output-tests/Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs.expected
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
possible_limbs =
Some
[("2^127 - 1", [(64, [3]); (32, [5; 6; 7])]);
("2^129 - 25", [(64, [3; 4; 5]); (32, [5; 6; 7; 8; 9])]);
("2^130 - 5", [(64, [3; 4; 5]); (32, [5; 6; 7; 8; 9])]);
("2^137 - 13", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
("2^140 - 27", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
("2^141 - 9", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
("2^150 - 5", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
("2^150 - 3", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
("2^152 - 17", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
("2^158 - 15", [(64, [3; 4; 5]); (32, [6; 7; 8; 9])]);
("2^165 - 25", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
("2^166 - 5", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
("2^171 - 19", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
("2^174 - 17", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
("2^174 - 3", [(64, [3; 4; 5]); (32, [7; 8; 9; 10; 11])]);
("2^189 - 25", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
("2^190 - 11", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
("2^191 - 19", [(64, [4; 5]); (32, [8; 9; 10; 11])]);
("2^194 - 33", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
("2^196 - 15", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
("2^198 - 17", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
("2^206 - 5", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
("2^212 - 29", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13])]);
("2^213 - 3", [(64, [4; 5; 6; 7]); (32, [8; 9; 10; 11; 12; 13])]);
("2^221 - 3", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13])]);
("2^222 - 117", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13])]);
("2^226 - 5", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
("2^230 - 27", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
("2^235 - 15", [(64, [4; 5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
("2^243 - 9", [(64, [5; 6; 7]); (32, [9; 10; 11; 12; 13; 14; 15])]);
("2^251 - 9", [(64, [5; 6; 7]); (32, [10; 11; 12; 13; 14; 15])]);
("2^255 - 765", [(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
("2^255 - 19", [(64, [5; 6; 7]); (32, [10; 11; 12; 13; 14; 15])]);
("2^256 - 189", [(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
("2^266 - 3",
[(64, [5; 6; 7; 8; 9]); (32, [10; 11; 12; 13; 14; 15; 16; 17])]);
("2^285 - 9", [(64, [5; 6; 7; 8; 9]); (32, [11; 12; 13; 14; 15; 16; 17])]);
("2^291 - 19",
[(64, [5; 6; 7; 8; 9]); (32, [12; 13; 14; 15; 16; 17; 18; 19])]);
("2^321 - 9",
[(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
("2^336 - 17",
[(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
("2^336 - 3",
[(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
("2^338 - 15",
[(64, [6; 7; 8; 9; 10; 11]); (32, [13; 14; 15; 16; 17; 18; 19; 20; 21])]);
("2^192 - 2^64 - 1", [(64, [4; 5]); (32, [9; 10; 11])]);
("2^216 - 2^108 - 1", [(64, [4; 5; 6; 7]); (32, [8; 10; 11; 12; 13])]);
("2^322 - 2^161 - 1",
[(64, [6; 7; 8; 9; 10; 11]); (32, [12; 14; 15; 16; 17; 18; 19; 20; 21])]);
("2^205 - 45*2^198 - 1", [(64, []); (32, [])]);
("2^224 - 2^96 + 1", [(64, [5; 6; 7]); (32, [10; 11; 12; 13])]);
("2^256 - 2^224 + 2^192 + 2^96 - 1",
[(64, [5; 6; 7]); (32, [11; 12; 13; 14; 15])]);
("2^256 - 2^32 - 977", [(64, [6; 7]); (32, [12; 13; 14; 15])]);
("2^256 - 4294968273", [(64, [6; 7]); (32, [])]);
("2^256 - 88*2^240 - 1", [(64, []); (32, [])]);
("2^254 - 127*2^240 - 1", [(64, []); (32, [])])]
: option (list (string * list (nat * list nat)))
157 changes: 157 additions & 0 deletions src/UnsaturatedSolinasHeuristics/Tests.v
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,157 @@
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.Option.
Require Import Crypto.UnsaturatedSolinasHeuristics.
Require Import Crypto.Util.Strings.ParseArithmeticToTaps.
Require Import Crypto.Util.OptionList.
Import ListNotations.
Import Coq.Lists.List.
Local Open Scope option_scope.
Local Open Scope string_scope.
Local Open Scope list_scope.
Local Open Scope nat_scope.
Local Open Scope Z_scope.
Local Open Scope core_scope.

Definition single_tap_primes : list string :=
[
(* single-tap: *)

"2^127 - 1"; (* "kummer strikes back" *)
"2^129 - 25";
"2^130 - 5"; (* poly1305 *)
"2^137 - 13";
"2^140 - 27";
"2^141 - 9";
"2^150 - 5";
"2^150 - 3";
"2^152 - 17";
"2^158 - 15";
"2^165 - 25";
"2^166 - 5";
"2^171 - 19";
"2^174 - 17";
"2^174 - 3";
"2^189 - 25";
"2^190 - 11";
"2^191 - 19";
"2^194 - 33";
"2^196 - 15";
"2^198 - 17";
"2^206 - 5";
"2^212 - 29";
"2^213 - 3";
"2^221 - 3";
"2^222 - 117";
"2^226 - 5";
"2^230 - 27";
"2^235 - 15";
"2^243 - 9";
"2^251 - 9";
"2^255 - 765";
"2^255 - 19"; (* curve25519 *)
"2^256 - 189";
"2^266 - 3";
"2^285 - 9";
"2^291 - 19";
"2^321 - 9";
"2^336 - 17";
"2^336 - 3";
"2^338 - 15";
"2^369 - 25";
"2^379 - 19";
"2^382 - 105";
"2^383 - 421";
"2^383 - 187";
"2^383 - 31";
"2^384 - 317";
"2^389 - 21";
"2^401 - 31";
"2^413 - 21";
"2^414 - 17";
"2^444 - 17";
"2^452 - 3";
"2^468 - 17";
"2^488 - 17";
"2^489 - 21";
"2^495 - 31";
"2^511 - 481";
"2^511 - 187";
"2^512 - 569";
"2^521 - 1" (* p512 *)
].

Definition two_tap_golden_ratio_primes : list string :=
[

(* two taps, golden ratio: *)

"2^192 - 2^64 - 1";
"2^216 - 2^108 - 1";
"2^322 - 2^161 - 1";
"2^416 - 2^208 - 1";
"2^448 - 2^224 - 1"; (* goldilocks *)
"2^450 - 2^225 - 1";
"2^480 - 2^240 - 1" (* ridinghood *)
].

Definition two_or_more_tap_primes : list string :=
[
(* two or more taps *)

"2^205 - 45*2^198 - 1";
"2^224 - 2^96 + 1"; (* p224 *)
"2^256 - 2^224 + 2^192 + 2^96 - 1"; (* p256 *)
"2^256 - 2^32 - 977"; (* bitcoin *)
"2^256 - 4294968273"; (* bitcoin, for 64-bit impl *)
"2^384 - 2^128 - 2^96 + 2^32 - 1" (* p384 *)
].

Definition montgomery_friendly_primes : list string :=
[
(* Montgomery-Friendly *)

"2^256 - 88*2^240 - 1";
"2^254 - 127*2^240 - 1";
"2^384 - 79*2^376 - 1";
"2^384 - 5*2^368 - 1";
"2^512 - 491*2^496 - 1";
"2^510 - 290*2^496 - 1"
].

Definition multitap_primes : list string :=
two_tap_golden_ratio_primes
++ two_or_more_tap_primes
++ montgomery_friendly_primes.

Definition primes : list string :=
single_tap_primes ++ multitap_primes.

Local Instance : tight_upperbound_fraction_opt := default_tight_upperbound_fraction.

(* 15.5 s for primes up to 2^301 *)
(* 25.674 s for primes up to 2^351 *)
(* 76.298 s for primes 2^300 up to 2^401 *)
Local Open Scope nat_scope.
Local Open Scope core_scope.
Time Definition possible_limbs :=
Eval native_compute in
Option.List.lift
(Option.List.map
(fun p => match parseZ_arith_to_taps p with
| Some (s, c)
=> if (s <=? 2^350)%Z
then Some (Some (p, [(64, get_possible_limbs s c 64); (32, get_possible_limbs s c 32)]))
else None
| None => Some None
end)
primes).
Local Notation "[ ]" := nil (format "[ ]") : core_scope.
Local Notation "[ x ]" := (cons x nil) : core_scope.
Local Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) (format "'[hv ' [ x ; '/' y ; '/' .. ; '/' z ] ']'") : core_scope.
Local Close Scope list_scope.
Local Open Scope core_scope.
Set Printing Width 250.
Redirect "Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs"
Print possible_limbs.

0 comments on commit b5d9ba0

Please sign in to comment.