fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Uncurry rewriter rules	Jason Gross	2018-11-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This will hopefully make various proofs easier. We have to keep the rewrite-rule-specific proofs curried, however, because otherwise lookup in evar maps blocks reduction, and is both a pain and slow to deal with. After \| File Name \| Before \|\| Change \| % Change -------------------------------------------------------------------------------------------------------------------- 31m39.26s \| Total \| 33m01.82s \|\| -1m22.55s \| -4.16% -------------------------------------------------------------------------------------------------------------------- 0m36.85s \| Experiments/NewPipeline/Rewriter.vo \| 1m26.67s \|\| -0m49.82s \| -57.48% 1m10.16s \| Experiments/NewPipeline/RewriterRulesGood.vo \| 1m42.34s \|\| -0m32.18s \| -31.44% 1m46.01s \| Experiments/NewPipeline/RewriterRulesInterpGood.vo \| 2m12.58s \|\| -0m26.57s \| -20.04% 5m10.66s \| Experiments/NewPipeline/Toplevel1.vo \| 5m03.90s \|\| +0m06.76s \| +2.22% 2m09.11s \| Experiments/NewPipeline/RewriterWf2.vo \| 2m02.40s \|\| +0m06.71s \| +5.48% 7m01.32s \| p384_32.c \| 6m56.98s \|\| +0m04.33s \| +1.04% 1m44.69s \| Experiments/NewPipeline/Toplevel2.vo \| 1m42.84s \|\| +0m01.84s \| +1.79% 0m21.28s \| p256_32.c \| 0m19.93s \|\| +0m01.35s \| +6.77% 0m19.06s \| Experiments/NewPipeline/RewriterWf1.vo \| 0m17.64s \|\| +0m01.41s \| +8.04% 6m28.29s \| Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \| 6m28.50s \|\| -0m00.20s \| -0.05% 0m41.80s \| Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery \| 0m42.08s \|\| -0m00.28s \| -0.66% 0m41.72s \| p521_32.c \| 0m41.20s \|\| +0m00.51s \| +1.26% 0m34.42s \| p521_64.c \| 0m34.30s \|\| +0m00.12s \| +0.34% 0m27.32s \| Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas \| 0m27.49s \|\| -0m00.16s \| -0.61% 0m20.66s \| secp256k1_32.c \| 0m20.20s \|\| +0m00.46s \| +2.27% 0m19.90s \| Experiments/NewPipeline/ExtractionHaskell/saturated_solinas \| 0m19.95s \|\| -0m00.05s \| -0.25% 0m16.11s \| Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery \| 0m15.54s \|\| +0m00.57s \| +3.66% 0m12.50s \| p384_64.c \| 0m12.59s \|\| -0m00.08s \| -0.71% 0m09.90s \| Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml \| 0m09.42s \|\| +0m00.48s \| +5.09% 0m09.34s \| Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas \| 0m08.87s \|\| +0m00.47s \| +5.29% 0m08.47s \| p224_32.c \| 0m08.52s \|\| -0m00.04s \| -0.58% 0m06.94s \| Experiments/NewPipeline/ExtractionOCaml/saturated_solinas \| 0m05.96s \|\| +0m00.98s \| +16.44% 0m06.38s \| Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml \| 0m06.19s \|\| +0m00.18s \| +3.06% 0m06.20s \| Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs \| 0m06.18s \|\| +0m00.02s \| +0.32% 0m05.02s \| Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs \| 0m04.51s \|\| +0m00.50s \| +11.30% 0m04.88s \| Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml \| 0m04.71s \|\| +0m00.16s \| +3.60% 0m03.82s \| Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs \| 0m03.82s \|\| +0m00.00s \| +0.00% 0m02.32s \| curve25519_32.c \| 0m02.37s \|\| -0m00.05s \| -2.10% 0m02.12s \| p224_64.c \| 0m02.08s \|\| +0m00.04s \| +1.92% 0m02.02s \| p256_64.c \| 0m01.97s \|\| +0m00.05s \| +2.53% 0m02.02s \| secp256k1_64.c \| 0m02.16s \|\| -0m00.14s \| -6.48% 0m01.62s \| curve25519_64.c \| 0m01.57s \|\| +0m00.05s \| +3.18% 0m01.50s \| Experiments/NewPipeline/CLI.vo \| 0m01.53s \|\| -0m00.03s \| -1.96% 0m01.36s \| Experiments/NewPipeline/StandaloneOCamlMain.vo \| 0m01.29s \|\| +0m00.07s \| +5.42% 0m01.34s \| Experiments/NewPipeline/StandaloneHaskellMain.vo \| 0m01.42s \|\| -0m00.07s \| -5.63% 0m01.19s \| Experiments/NewPipeline/CompilersTestCases.vo \| 0m01.11s \|\| +0m00.07s \| +7.20% 0m00.97s \| Experiments/NewPipeline/RewriterProofs.vo \| 0m01.01s \|\| -0m00.04s \| -3.96%
*	Update the post-bounds rewrite rules	Jason Gross	2018-11-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	They are all proven, and they work! To make this possible, we had to make casting commute with negation. After \| File Name \| Before \|\| Change \| % Change -------------------------------------------------------------------------------------------------------------------- 32m30.13s \| Total \| 32m17.70s \|\| +0m12.42s \| +0.64% -------------------------------------------------------------------------------------------------------------------- 1m38.96s \| Experiments/NewPipeline/RewriterRulesGood.vo \| 1m23.70s \|\| +0m15.26s \| +18.23% 4m44.45s \| Experiments/NewPipeline/Toplevel1.vo \| 4m58.41s \|\| -0m13.95s \| -4.67% 2m08.47s \| Experiments/NewPipeline/RewriterRulesInterpGood.vo \| 1m56.27s \|\| +0m12.19s \| +10.49% 6m36.50s \| p384_32.c \| 6m42.34s \|\| -0m05.84s \| -1.45% 6m19.09s \| Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \| 6m15.11s \|\| +0m03.97s \| +1.06% 1m24.28s \| Experiments/NewPipeline/Rewriter.vo \| 1m20.87s \|\| +0m03.40s \| +4.21% 0m40.26s \| Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery \| 0m43.07s \|\| -0m02.81s \| -6.52% 1m57.38s \| Experiments/NewPipeline/RewriterWf2.vo \| 1m59.36s \|\| -0m01.98s \| -1.65% 1m40.57s \| Experiments/NewPipeline/Toplevel2.vo \| 1m41.68s \|\| -0m01.11s \| -1.09% 0m42.80s \| Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery \| 0m41.59s \|\| +0m01.20s \| +2.90% 0m25.06s \| Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas \| 0m26.26s \|\| -0m01.20s \| -4.56% 0m18.78s \| p256_32.c \| 0m17.12s \|\| +0m01.66s \| +9.69% 0m18.49s \| secp256k1_32.c \| 0m17.05s \|\| +0m01.43s \| +8.44% 0m15.98s \| Experiments/NewPipeline/RewriterWf1.vo \| 0m17.00s \|\| -0m01.01s \| -5.99% 0m08.04s \| p224_32.c \| 0m07.03s \|\| +0m01.00s \| +14.36% 0m39.70s \| p521_32.c \| 0m40.46s \|\| -0m00.75s \| -1.87% 0m33.03s \| p521_64.c \| 0m33.98s \|\| -0m00.94s \| -2.79% 0m23.34s \| Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas \| 0m22.79s \|\| +0m00.55s \| +2.41% 0m18.64s \| Experiments/NewPipeline/ExtractionHaskell/saturated_solinas \| 0m17.70s \|\| +0m00.94s \| +5.31% 0m14.98s \| Experiments/NewPipeline/ExtractionOCaml/saturated_solinas \| 0m14.20s \|\| +0m00.78s \| +5.49% 0m11.58s \| p384_64.c \| 0m11.49s \|\| +0m00.08s \| +0.78% 0m09.16s \| Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml \| 0m09.29s \|\| -0m00.12s \| -1.39% 0m06.04s \| Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml \| 0m06.01s \|\| +0m00.03s \| +0.49% 0m05.80s \| Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs \| 0m05.85s \|\| -0m00.04s \| -0.85% 0m04.74s \| Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs \| 0m04.36s \|\| +0m00.37s \| +8.71% 0m04.57s \| Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml \| 0m04.91s \|\| -0m00.33s \| -6.92% 0m03.66s \| Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs \| 0m03.55s \|\| +0m00.11s \| +3.09% 0m02.24s \| curve25519_32.c \| 0m02.29s \|\| -0m00.04s \| -2.18% 0m02.04s \| p224_64.c \| 0m01.86s \|\| +0m00.17s \| +9.67% 0m01.98s \| secp256k1_64.c \| 0m02.45s \|\| -0m00.47s \| -19.18% 0m01.97s \| p256_64.c \| 0m01.88s \|\| +0m00.09s \| +4.78% 0m01.49s \| curve25519_64.c \| 0m01.55s \|\| -0m00.06s \| -3.87% 0m01.40s \| Experiments/NewPipeline/CLI.vo \| 0m01.49s \|\| -0m00.09s \| -6.04% 0m01.30s \| Experiments/NewPipeline/StandaloneHaskellMain.vo \| 0m01.34s \|\| -0m00.04s \| -2.98% 0m01.26s \| Experiments/NewPipeline/StandaloneOCamlMain.vo \| 0m01.31s \|\| -0m00.05s \| -3.81% 0m01.10s \| Experiments/NewPipeline/CompilersTestCases.vo \| 0m01.12s \|\| -0m00.02s \| -1.78% 0m01.00s \| Experiments/NewPipeline/RewriterProofs.vo \| 0m00.97s \|\| +0m00.03s \| +3.09%
*	Split off all of the arithmetic rules that need bounds info	Jason Gross	2018-11-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Because we need to do extra passes of DCE and subst01 to fully reduce things, we generalize some of the interp proofs over cast behavior. For ease of rewriting, we make [ident.interp] an alias (notation) for [ident.gen_interp], rather than a [Definition]. We also factor out the rewriting wrapper inside the pipeline module into its own definition. After \| File Name \| Before \|\| Change \| % Change --------------------------------------------------------------------------------------------------------------------- 32m09.80s \| Total \| 26m07.22s \|\| +6m02.58s \| +23.13% --------------------------------------------------------------------------------------------------------------------- 6m41.53s \| p384_32.c \| 0m28.22s \|\| +6m13.30s \| +1322.85% 1m19.67s \| Experiments/NewPipeline/Rewriter.vo \| 2m22.97s \|\| -1m03.29s \| -44.27% 0m21.90s \| secp256k1_32.c \| 0m06.46s \|\| +0m15.43s \| +239.00% 0m21.24s \| p256_32.c \| 0m06.32s \|\| +0m14.91s \| +236.07% 6m18.26s \| Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \| 6m13.65s \|\| +0m04.61s \| +1.23% 0m14.12s \| p384_64.c \| 0m10.22s \|\| +0m03.89s \| +38.16% 0m07.86s \| p224_32.c \| 0m03.92s \|\| +0m03.94s \| +100.51% 4m34.19s \| Experiments/NewPipeline/Toplevel1.vo \| 4m37.15s \|\| -0m02.95s \| -1.06% 1m41.50s \| Experiments/NewPipeline/Toplevel2.vo \| 1m38.62s \|\| +0m02.87s \| +2.92% 0m37.69s \| p521_64.c \| 0m35.62s \|\| +0m02.07s \| +5.81% 0m29.75s \| Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas \| 0m27.09s \|\| +0m02.66s \| +9.81% 0m17.88s \| Experiments/NewPipeline/ExtractionOCaml/saturated_solinas \| 0m15.52s \|\| +0m02.35s \| +15.20% 1m47.75s \| Experiments/NewPipeline/RewriterRulesInterpGood.vo \| 1m46.74s \|\| +0m01.00s \| +0.94% 0m44.38s \| p521_32.c \| 0m42.47s \|\| +0m01.91s \| +4.49% 0m43.92s \| Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery \| 0m41.97s \|\| +0m01.95s \| +4.64% 0m24.99s \| Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas \| 0m26.52s \|\| -0m01.53s \| -5.76% 0m20.62s \| Experiments/NewPipeline/ExtractionHaskell/saturated_solinas \| 0m22.26s \|\| -0m01.64s \| -7.36% 0m11.42s \| Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml \| 0m12.88s \|\| -0m01.46s \| -11.33% 0m08.44s \| Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs \| 0m07.12s \|\| +0m01.31s \| +18.53% 1m50.48s \| Experiments/NewPipeline/RewriterWf2.vo \| 1m50.18s \|\| +0m00.29s \| +0.27% 1m15.53s \| Experiments/NewPipeline/RewriterRulesGood.vo \| 1m15.26s \|\| +0m00.26s \| +0.35% 0m43.94s \| Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery \| 0m43.00s \|\| +0m00.93s \| +2.18% 0m10.25s \| Experiments/NewPipeline/RewriterWf1.vo \| 0m10.46s \|\| -0m00.21s \| -2.00% 0m07.27s \| Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml \| 0m07.41s \|\| -0m00.14s \| -1.88% 0m06.29s \| Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs \| 0m05.75s \|\| +0m00.54s \| +9.39% 0m05.54s \| Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml \| 0m06.24s \|\| -0m00.70s \| -11.21% 0m04.86s \| Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs \| 0m05.62s \|\| -0m00.75s \| -13.52% 0m02.86s \| curve25519_32.c \| 0m02.43s \|\| +0m00.42s \| +17.69% 0m02.80s \| secp256k1_64.c \| 0m02.29s \|\| +0m00.50s \| +22.27% 0m02.74s \| p256_64.c \| 0m02.67s \|\| +0m00.07s \| +2.62% 0m02.13s \| curve25519_64.c \| 0m02.38s \|\| -0m00.25s \| -10.50% 0m01.97s \| p224_64.c \| 0m01.86s \|\| +0m00.10s \| +5.91% 0m01.46s \| Experiments/NewPipeline/CLI.vo \| 0m01.52s \|\| -0m00.06s \| -3.94% 0m01.36s \| Experiments/NewPipeline/StandaloneHaskellMain.vo \| 0m01.25s \|\| +0m00.11s \| +8.80% 0m01.22s \| Experiments/NewPipeline/StandaloneOCamlMain.vo \| 0m01.19s \|\| +0m00.03s \| +2.52% 0m01.02s \| Experiments/NewPipeline/CompilersTestCases.vo \| 0m01.05s \|\| -0m00.03s \| -2.85% 0m00.97s \| Experiments/NewPipeline/RewriterProofs.vo \| 0m00.94s \|\| +0m00.03s \| +3.19%
*	Add under_forall_vars_relation1_lam_forall_vars, remove ↵	Jason Gross	2018-10-25
\| \| \| \|	forall2_type_of_list_cps alias of under_type_of_list_relation_cps
*	Update rewriter correctness condition	Jason Gross	2018-10-23
\| \| \| \| \| \|	Now we don't need any relation on values when going under binders to get the cps-id condition. This seems essential to getting the rewriter interp correctness proofs to work.
*	Add placeholder rewrite rules for rewriting after bounds	Jason Gross	2018-10-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Currently, there aren't any interesting rewrite rules in the lists, but this allows us to move rewrite rules that depend on cast behavior to after bounds analysis. Unfortunately, it takes a lot of time to build from Rewriter.v to the standalone binaries, so it'll probably make sense to inline some stuff for more rapid development. Note that we also now have a tactic that does all of the evaluation for rewrite rules (assuming the right [Arguments] commands have been issued).
*	Parameterize rewriter proofs over cast-outside-of-range behavior	Jason Gross	2018-10-11
\|
*	Add interp-correctness condition for rewriter	Jason Gross	2018-10-11
	The NBE-rewrite rules are proven correct. The arith and fancy rewrite rules are reduced to lemmas about Z, most of which are inconsistent (and therefore indicate rewrite rules which are missing side-conditions). One bad rewrite rule was found in this process, and corrected in 0842563b23f8d780f4ff1080d7620fc3f368191f The next step after this will be using the rewrite rule correctness to prove the rewriter correct.

| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |

This will hopefully make various proofs easier. We have to keep the rewrite-rule-specific proofs curried, however, because otherwise lookup in evar maps blocks reduction, and is both a pain and slow to deal with. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 31m39.26s | Total | 33m01.82s || -1m22.55s | -4.16% -------------------------------------------------------------------------------------------------------------------- 0m36.85s | Experiments/NewPipeline/Rewriter.vo | 1m26.67s || -0m49.82s | -57.48% 1m10.16s | Experiments/NewPipeline/RewriterRulesGood.vo | 1m42.34s || -0m32.18s | -31.44% 1m46.01s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 2m12.58s || -0m26.57s | -20.04% 5m10.66s | Experiments/NewPipeline/Toplevel1.vo | 5m03.90s || +0m06.76s | +2.22% 2m09.11s | Experiments/NewPipeline/RewriterWf2.vo | 2m02.40s || +0m06.71s | +5.48% 7m01.32s | p384_32.c | 6m56.98s || +0m04.33s | +1.04% 1m44.69s | Experiments/NewPipeline/Toplevel2.vo | 1m42.84s || +0m01.84s | +1.79% 0m21.28s | p256_32.c | 0m19.93s || +0m01.35s | +6.77% 0m19.06s | Experiments/NewPipeline/RewriterWf1.vo | 0m17.64s || +0m01.41s | +8.04% 6m28.29s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m28.50s || -0m00.20s | -0.05% 0m41.80s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m42.08s || -0m00.28s | -0.66% 0m41.72s | p521_32.c | 0m41.20s || +0m00.51s | +1.26% 0m34.42s | p521_64.c | 0m34.30s || +0m00.12s | +0.34% 0m27.32s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m27.49s || -0m00.16s | -0.61% 0m20.66s | secp256k1_32.c | 0m20.20s || +0m00.46s | +2.27% 0m19.90s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m19.95s || -0m00.05s | -0.25% 0m16.11s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m15.54s || +0m00.57s | +3.66% 0m12.50s | p384_64.c | 0m12.59s || -0m00.08s | -0.71% 0m09.90s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.42s || +0m00.48s | +5.09% 0m09.34s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m08.87s || +0m00.47s | +5.29% 0m08.47s | p224_32.c | 0m08.52s || -0m00.04s | -0.58% 0m06.94s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m05.96s || +0m00.98s | +16.44% 0m06.38s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.19s || +0m00.18s | +3.06% 0m06.20s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.18s || +0m00.02s | +0.32% 0m05.02s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.51s || +0m00.50s | +11.30% 0m04.88s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.71s || +0m00.16s | +3.60% 0m03.82s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.82s || +0m00.00s | +0.00% 0m02.32s | curve25519_32.c | 0m02.37s || -0m00.05s | -2.10% 0m02.12s | p224_64.c | 0m02.08s || +0m00.04s | +1.92% 0m02.02s | p256_64.c | 0m01.97s || +0m00.05s | +2.53% 0m02.02s | secp256k1_64.c | 0m02.16s || -0m00.14s | -6.48% 0m01.62s | curve25519_64.c | 0m01.57s || +0m00.05s | +3.18% 0m01.50s | Experiments/NewPipeline/CLI.vo | 0m01.53s || -0m00.03s | -1.96% 0m01.36s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.29s || +0m00.07s | +5.42% 0m01.34s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.42s || -0m00.07s | -5.63% 0m01.19s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.11s || +0m00.07s | +7.20% 0m00.97s | Experiments/NewPipeline/RewriterProofs.vo | 0m01.01s || -0m00.04s | -3.96%

| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |

They are all proven, and they work! To make this possible, we had to make casting commute with negation. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 32m30.13s | Total | 32m17.70s || +0m12.42s | +0.64% -------------------------------------------------------------------------------------------------------------------- 1m38.96s | Experiments/NewPipeline/RewriterRulesGood.vo | 1m23.70s || +0m15.26s | +18.23% 4m44.45s | Experiments/NewPipeline/Toplevel1.vo | 4m58.41s || -0m13.95s | -4.67% 2m08.47s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 1m56.27s || +0m12.19s | +10.49% 6m36.50s | p384_32.c | 6m42.34s || -0m05.84s | -1.45% 6m19.09s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m15.11s || +0m03.97s | +1.06% 1m24.28s | Experiments/NewPipeline/Rewriter.vo | 1m20.87s || +0m03.40s | +4.21% 0m40.26s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m43.07s || -0m02.81s | -6.52% 1m57.38s | Experiments/NewPipeline/RewriterWf2.vo | 1m59.36s || -0m01.98s | -1.65% 1m40.57s | Experiments/NewPipeline/Toplevel2.vo | 1m41.68s || -0m01.11s | -1.09% 0m42.80s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m41.59s || +0m01.20s | +2.90% 0m25.06s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m26.26s || -0m01.20s | -4.56% 0m18.78s | p256_32.c | 0m17.12s || +0m01.66s | +9.69% 0m18.49s | secp256k1_32.c | 0m17.05s || +0m01.43s | +8.44% 0m15.98s | Experiments/NewPipeline/RewriterWf1.vo | 0m17.00s || -0m01.01s | -5.99% 0m08.04s | p224_32.c | 0m07.03s || +0m01.00s | +14.36% 0m39.70s | p521_32.c | 0m40.46s || -0m00.75s | -1.87% 0m33.03s | p521_64.c | 0m33.98s || -0m00.94s | -2.79% 0m23.34s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m22.79s || +0m00.55s | +2.41% 0m18.64s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m17.70s || +0m00.94s | +5.31% 0m14.98s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m14.20s || +0m00.78s | +5.49% 0m11.58s | p384_64.c | 0m11.49s || +0m00.08s | +0.78% 0m09.16s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.29s || -0m00.12s | -1.39% 0m06.04s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.01s || +0m00.03s | +0.49% 0m05.80s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.85s || -0m00.04s | -0.85% 0m04.74s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.36s || +0m00.37s | +8.71% 0m04.57s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.91s || -0m00.33s | -6.92% 0m03.66s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.55s || +0m00.11s | +3.09% 0m02.24s | curve25519_32.c | 0m02.29s || -0m00.04s | -2.18% 0m02.04s | p224_64.c | 0m01.86s || +0m00.17s | +9.67% 0m01.98s | secp256k1_64.c | 0m02.45s || -0m00.47s | -19.18% 0m01.97s | p256_64.c | 0m01.88s || +0m00.09s | +4.78% 0m01.49s | curve25519_64.c | 0m01.55s || -0m00.06s | -3.87% 0m01.40s | Experiments/NewPipeline/CLI.vo | 0m01.49s || -0m00.09s | -6.04% 0m01.30s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.34s || -0m00.04s | -2.98% 0m01.26s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.31s || -0m00.05s | -3.81% 0m01.10s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.12s || -0m00.02s | -1.78% 0m01.00s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.97s || +0m00.03s | +3.09%

| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |

Because we need to do extra passes of DCE and subst01 to fully reduce things, we generalize some of the interp proofs over cast behavior. For ease of rewriting, we make [ident.interp] an alias (notation) for [ident.gen_interp], rather than a [Definition]. We also factor out the rewriting wrapper inside the pipeline module into its own definition. After | File Name | Before || Change | % Change --------------------------------------------------------------------------------------------------------------------- 32m09.80s | Total | 26m07.22s || +6m02.58s | +23.13% --------------------------------------------------------------------------------------------------------------------- 6m41.53s | p384_32.c | 0m28.22s || +6m13.30s | +1322.85% 1m19.67s | Experiments/NewPipeline/Rewriter.vo | 2m22.97s || -1m03.29s | -44.27% 0m21.90s | secp256k1_32.c | 0m06.46s || +0m15.43s | +239.00% 0m21.24s | p256_32.c | 0m06.32s || +0m14.91s | +236.07% 6m18.26s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m13.65s || +0m04.61s | +1.23% 0m14.12s | p384_64.c | 0m10.22s || +0m03.89s | +38.16% 0m07.86s | p224_32.c | 0m03.92s || +0m03.94s | +100.51% 4m34.19s | Experiments/NewPipeline/Toplevel1.vo | 4m37.15s || -0m02.95s | -1.06% 1m41.50s | Experiments/NewPipeline/Toplevel2.vo | 1m38.62s || +0m02.87s | +2.92% 0m37.69s | p521_64.c | 0m35.62s || +0m02.07s | +5.81% 0m29.75s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m27.09s || +0m02.66s | +9.81% 0m17.88s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m15.52s || +0m02.35s | +15.20% 1m47.75s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 1m46.74s || +0m01.00s | +0.94% 0m44.38s | p521_32.c | 0m42.47s || +0m01.91s | +4.49% 0m43.92s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m41.97s || +0m01.95s | +4.64% 0m24.99s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m26.52s || -0m01.53s | -5.76% 0m20.62s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m22.26s || -0m01.64s | -7.36% 0m11.42s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m12.88s || -0m01.46s | -11.33% 0m08.44s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m07.12s || +0m01.31s | +18.53% 1m50.48s | Experiments/NewPipeline/RewriterWf2.vo | 1m50.18s || +0m00.29s | +0.27% 1m15.53s | Experiments/NewPipeline/RewriterRulesGood.vo | 1m15.26s || +0m00.26s | +0.35% 0m43.94s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m43.00s || +0m00.93s | +2.18% 0m10.25s | Experiments/NewPipeline/RewriterWf1.vo | 0m10.46s || -0m00.21s | -2.00% 0m07.27s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m07.41s || -0m00.14s | -1.88% 0m06.29s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m05.75s || +0m00.54s | +9.39% 0m05.54s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m06.24s || -0m00.70s | -11.21% 0m04.86s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m05.62s || -0m00.75s | -13.52% 0m02.86s | curve25519_32.c | 0m02.43s || +0m00.42s | +17.69% 0m02.80s | secp256k1_64.c | 0m02.29s || +0m00.50s | +22.27% 0m02.74s | p256_64.c | 0m02.67s || +0m00.07s | +2.62% 0m02.13s | curve25519_64.c | 0m02.38s || -0m00.25s | -10.50% 0m01.97s | p224_64.c | 0m01.86s || +0m00.10s | +5.91% 0m01.46s | Experiments/NewPipeline/CLI.vo | 0m01.52s || -0m00.06s | -3.94% 0m01.36s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.25s || +0m00.11s | +8.80% 0m01.22s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.19s || +0m00.03s | +2.52% 0m01.02s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.05s || -0m00.03s | -2.85% 0m00.97s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.94s || +0m00.03s | +3.19%

| | | |

forall2_type_of_list_cps alias of under_type_of_list_relation_cps

| | | | | |

Now we don't need any relation on values when going under binders to get the cps-id condition. This seems essential to getting the rewriter interp correctness proofs to work.

| | | | | | | | | | | | | |

Currently, there aren't any interesting rewrite rules in the lists, but this allows us to move rewrite rules that depend on cast behavior to after bounds analysis. Unfortunately, it takes a lot of time to build from Rewriter.v to the standalone binaries, so it'll probably make sense to inline some stuff for more rapid development. Note that we also now have a tactic that does all of the evaluation for rewrite rules (assuming the right [Arguments] commands have been issued).

|

The NBE-rewrite rules are proven correct. The arith and fancy rewrite rules are reduced to lemmas about Z, most of which are inconsistent (and therefore indicate rewrite rules which are missing side-conditions). One bad rewrite rule was found in this process, and corrected in 0842563b23f8d780f4ff1080d7620fc3f368191f The next step after this will be using the rewrite rule correctness to prove the rewriter correct.