aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-07 02:41:33 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-10-18 23:01:29 -0400
commitd576e6d6553a074c160afa41dda1f1174dcdd2cf (patch)
tree5211818c3169f25f8f9616527f8b410fb2b78544 /src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
parent795c30b733163e1a1f05a0c5f5a8c36cc69a0a1d (diff)
Support p256 / montgomery in json format
Extra time comes from adding AMD128 to NISTP256, mostly. After | File Name | Before || Change --------------------------------------------------------------------------------------------- 13m25.13s | Total | 13m30.82s || -0m05.69s --------------------------------------------------------------------------------------------- N/A | Specific/IntegrationTestMontgomeryP256_128 | 0m25.42s || -0m25.42s 0m22.75s | Specific/NISTP256/AMD128/femul | N/A || +0m22.75s 1m31.64s | Specific/NISTP256/AMD64/femul | 1m52.42s || -0m20.78s 0m14.46s | Specific/NISTP256/AMD128/fesub | N/A || +0m14.46s 0m14.25s | Specific/NISTP256/AMD128/feadd | N/A || +0m14.25s 0m14.12s | Specific/NISTP256/AMD128/fenz | N/A || +0m14.11s N/A | Specific/NISTP256/AMD64/MontgomeryP256 | 0m13.00s || -0m13.00s N/A | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.40s || -0m12.40s N/A | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.99s || -0m11.99s 0m11.74s | Specific/NISTP256/AMD128/feopp | N/A || +0m11.74s N/A | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.22s || -0m11.22s N/A | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.27s || -0m09.26s N/A | Specific/MontgomeryP256_128 | 0m09.26s || -0m09.25s 0m08.42s | Specific/NISTP256/AMD64/Synthesis | N/A || +0m08.41s 0m14.67s | Specific/NISTP256/AMD64/fenz | 0m09.98s || +0m04.68s 0m04.12s | Specific/Framework/ArithmeticSynthesis/Montgomery | N/A || +0m04.12s 0m03.58s | Specific/NISTP256/AMD128/Synthesis | N/A || +0m03.58s 1m10.78s | Specific/X2555/C128/ladderstep | 1m08.36s || +0m02.42s 1m02.10s | Specific/X25519/C32/femul | 1m00.59s || +0m01.50s 0m43.59s | Specific/X2448/Karatsuba/C64/Synthesis | 0m44.86s || -0m01.26s 0m34.97s | Specific/X25519/C32/fesquare | 0m35.98s || -0m01.00s 0m20.10s | Specific/NISTP256/AMD64/fesub | 0m18.37s || +0m01.73s 0m17.61s | Specific/NISTP256/AMD64/feadd | 0m15.94s || +0m01.67s 2m09.77s | Specific/X25519/C64/ladderstep | 2m09.79s || -0m00.01s 1m11.70s | Specific/X2448/Karatsuba/C64/femul | 1m11.60s || +0m00.10s 0m32.14s | Specific/X25519/C32/Synthesis | 0m31.70s || +0m00.44s 0m27.94s | Specific/X25519/C32/freeze | 0m28.06s || -0m00.11s 0m17.62s | Specific/X25519/C64/femul | 0m17.41s || +0m00.21s 0m15.21s | Specific/X25519/C64/freeze | 0m14.74s || +0m00.47s 0m14.86s | Specific/NISTP256/AMD64/feopp | 0m14.96s || -0m00.10s 0m14.58s | Specific/X25519/C64/fesquare | 0m14.06s || +0m00.51s 0m10.10s | Specific/X25519/C64/Synthesis | 0m09.78s || +0m00.32s 0m06.22s | Specific/X2555/C128/Synthesis | 0m06.17s || +0m00.04s 0m01.01s | Specific/X25519/C32/CurveParameters | 0m01.05s || -0m00.04s 0m00.99s | Specific/Framework/SynthesisFramework | 0m01.08s || -0m00.09s 0m00.79s | Specific/Framework/MontgomeryReificationTypes | N/A || +0m00.79s 0m00.78s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.70s || +0m00.08s 0m00.78s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.75s || +0m00.03s 0m00.76s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | N/A || +0m00.76s 0m00.75s | Specific/Framework/IntegrationTestTemporaryMiscCommon | 0m00.80s || -0m00.05s 0m00.75s | Specific/Framework/MontgomeryReificationTypesPackage | N/A || +0m00.75s 0m00.73s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m00.75s || -0m00.02s 0m00.72s | Specific/Framework/ReificationTypesPackage | 0m00.70s || +0m00.02s 0m00.72s | Specific/Framework/ArithmeticSynthesis/Base | 0m00.73s || -0m00.01s 0m00.72s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.69s || +0m00.03s 0m00.72s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.76s || -0m00.04s 0m00.70s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.75s || -0m00.05s 0m00.70s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.77s || -0m00.07s 0m00.69s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.71s || -0m00.02s 0m00.67s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.74s || -0m00.06s 0m00.43s | Specific/X25519/C64/CurveParameters | 0m00.43s || +0m00.00s 0m00.38s | Specific/Framework/IntegrationTestDisplayCommon | 0m00.40s || -0m00.02s 0m00.38s | Specific/Framework/IntegrationTestDisplayCommonTactics | 0m00.37s || +0m00.01s 0m00.34s | Specific/Framework/CurveParameters | 0m00.32s || +0m00.02s 0m00.33s | Specific/X2555/C128/CurveParameters | 0m00.33s || +0m00.00s 0m00.32s | Specific/NISTP256/AMD128/CurveParameters | N/A || +0m00.32s 0m00.32s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.33s || -0m00.01s 0m00.31s | Specific/Framework/CurveParametersPackage | 0m00.33s || -0m00.02s 0m00.30s | Specific/NISTP256/AMD64/CurveParameters | N/A || +0m00.30s
Diffstat (limited to 'src/Specific/IntegrationTestMontgomeryP256_128_Sub.v')
-rw-r--r--src/Specific/IntegrationTestMontgomeryP256_128_Sub.v126
1 files changed, 0 insertions, 126 deletions
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
deleted file mode 100644
index 8f3df4cdf..000000000
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
+++ /dev/null
@@ -1,126 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Local Open Scope Z_scope.
-
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
-Require Import Crypto.Arithmetic.Core. Import B.
-Require Crypto.Arithmetic.Saturated.MontgomeryAPI.
-Require Import Crypto.Arithmetic.Saturated.UniformWeight.
-Require Import Crypto.Specific.MontgomeryP256_128.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
-Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.MoveLetIn.
-Require Import Crypto.Util.Tactics.DestructHead.
-Import ListNotations.
-
-Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
-
-Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-
-Section BoundedField25p5.
- Local Coercion Z.of_nat : nat >-> Z.
-
- Let bounds : Tuple.tuple zrange sz
- := Eval compute in
- Tuple.repeat {| lower := 0 ; upper := r-1 |} sz.
-
- Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))).
- Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
- Let feZ : Type := tuple Z sz.
- Let feW : Type := tuple (wordT lgbitwidth) sz.
- Let feBW : Type := BoundedWord sz bitwidth bounds.
- Let eval : feBW -> Z :=
- fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
- Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }.
- Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
- Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
- Let phi : feBW -> F m :=
- fun x => montgomery_to_F (eval x).
-
- Local Ltac op_sig_side_conditions_t _ :=
- try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption.
-
- (* TODO : change this to field once field isomorphism happens *)
- Definition sub
- : { sub : feBW_small -> feBW_small -> feBW_small
- | forall A B, phi (sub A B) = F.sub (phi A) (phi B) }.
- Proof.
- start_preglue.
- all:cbv [feBW_of_feBW_small eval].
- do_rewrite_with_sig_by sub op_sig_side_conditions_t.
- cbv_runtime.
- all:fin_preglue.
- factor_out_bounds_and_strip_eval sub_bounded op_sig_side_conditions_t.
- (* jgross start here! *)
- Set Ltac Profiling.
- (* Set Ltac Profiling.
- Print Ltac ReflectiveTactics.solve_side_conditions.
- Ltac ReflectiveTactics.solve_side_conditions ::= idtac.
- Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
- { Time ReflectiveTactics.do_reify. }
- { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
- { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
- { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
- { Require Import CNotations.
- Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
- { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
- { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
- { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
- { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. }
- { Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
- { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
- { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
- { Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
- { Time ReflectiveTactics.handle_boundedness_side_condition. } *)
- Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
- Show Ltac Profile.
- (* total time: 19.632s
-
- tactic local total calls max
-────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s
-─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s
-─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s
-─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s
-─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s
-─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s
-─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s
-─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s
-─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s
-─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s
-─eexact -------------------------------- 4.1% 4.1% 68 0.028s
-─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s
-─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s
-─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s
-─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s
-─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s
-─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s
-─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s
-
- tactic local total calls max
-────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s
- ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s
- │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s
- │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s
- │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s
- │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s
- │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s
- │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s
- │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s
- │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s
- │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s
- │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s
- │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s
- │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s
- │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s
- └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s
-*)
- Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *)
-
-Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *)
-
-Print Assumptions sub.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 07:14:47 +0000