diff options
Diffstat (limited to 'src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v')
| -rw-r--r-- | src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v index b2d76911c..7d4c82f6b 100644 --- a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v +++ b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v @@ -3,7 +3,7 @@ Require Import Coq.Strings.String. Require Import Coq.derive.Derive. Require Import Coq.Lists.List. Require Import Crypto.Experiments.NewPipeline.Arithmetic. -Require Import Crypto.Experiments.NewPipeline.Toplevel1. +Require Import Crypto.Experiments.NewPipeline.PushButtonSynthesis. Require Import Crypto.Experiments.NewPipeline.CStringification. Require Import Crypto.Util.Notations. @@ -11,6 +11,8 @@ Import ListNotations. Local Open Scope Z_scope. Import UnsaturatedSolinas. +(* TODO: Figure out what examples should go here *) +(* Module X25519_64. Definition n := 5%nat. Definition s := 2^255. @@ -889,3 +891,4 @@ expr_let x3038 := (#(Z_cast2 (uint32, bool)%core)%expr @ (#(Z_add_with_get_carry Finished transaction in 211.393 secs (210.924u,0.028s) (successful) *) End P256_32. +*) |