diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-03 15:01:22 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-07 00:05:30 -0400 |
| commit | 8f574164df9968eab1ccc0b7d97bbfe84eb135c3 (patch) | |
| tree | e0f4daf66fb8ba07c304b280ded08eb93dffbcfc /src/Specific/IntegrationTestFreeze.v | |
| parent | 3d77eaabd3aac64f1ab8b01a06b964b065889432 (diff) | |
Generalize phis
After | File Name | Before || Change
-----------------------------------------------------------------------
3m56.20s | Total | 4m14.86s || -0m18.66s
-----------------------------------------------------------------------
0m02.44s | Specific/X25519/C32/ReificationTypes | 0m19.48s || -0m17.03s
2m00.12s | Specific/X25519/C64/ladderstep | 1m55.72s || +0m04.40s
0m01.16s | Specific/X25519/C64/ReificationTypes | 0m05.17s || -0m04.00s
0m26.27s | Specific/X25519/C32/fesquare | 0m27.76s || -0m01.49s
0m52.60s | Specific/X25519/C32/femul | 0m52.46s || +0m00.14s
0m10.35s | Specific/X25519/C64/femul | 0m10.28s || +0m00.07s
0m08.30s | Specific/IntegrationTestSub | 0m08.69s || -0m00.38s
0m07.97s | Specific/IntegrationTestFreeze | 0m08.00s || -0m00.03s
0m06.99s | Specific/X25519/C64/fesquare | 0m07.31s || -0m00.31s
Diffstat (limited to 'src/Specific/IntegrationTestFreeze.v')
| -rw-r--r-- | src/Specific/IntegrationTestFreeze.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v index ebfab0c69..79466b8d6 100644 --- a/src/Specific/IntegrationTestFreeze.v +++ b/src/Specific/IntegrationTestFreeze.v @@ -6,13 +6,10 @@ Require Import Crypto.Util.BoundedWord. Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. -Local Definition phi : feBW -> F m := - fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x). - (* TODO : change this to field once field isomorphism happens *) Definition freeze : { freeze : feBW -> feBW - | forall a, phi (freeze a) = phi a }. + | forall a, phiBW (freeze a) = phiBW a }. Proof. start_preglue. do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime. |