fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add UnderLets flat_map interp proofs,other changes	Jason Gross	2019-04-04
\| \| \| \| \| \| \| \|	Also remove a rewrite rule using cast from the non-cast arith rules, regenerate the .out files, add ident.gets_inlined for eventual use in the rewriter, and generalize the rewrite rule lemmas over cast_out_of_range so that we can actually make use of their proofs for interp.
*	Update .out files	Jason Gross	2019-03-07
\|
*	Update .out files	Jason Gross	2019-02-18
\|
*	Insert casts before literals during bounds analysis	Jason Gross	2019-02-11
	Unless we explicitly say not to. The ability to explicitly say not to is required for, e.g., eta-expansion where we want to replace variable lists of known length with with cons cells indexing into the variable list, but don't want to pollute the code with casts. Uniformity in this way allows rewrite rules to not blow up exponentially (in the number of wildcards); we previously required a separate rewrite rule for each way of choosing between wildcard and literal. To preserve output of the pipeline, we add another pass that just strips the casts off of literals at the end. After \| File Name \| Before \|\| Change \| % Change -------------------------------------------------------------------------------------------- 20m27.24s \| Total \| 22m39.70s \|\| -2m12.46s \| -9.74% -------------------------------------------------------------------------------------------- 0m44.27s \| Rewriter.vo \| 2m11.58s \|\| -1m27.31s \| -66.35% 1m15.23s \| RewriterRulesInterpGood.vo \| 1m50.28s \|\| -0m35.04s \| -31.78% 1m40.19s \| RewriterRulesGood.vo \| 1m58.05s \|\| -0m17.85s \| -15.12% 0m26.99s \| AbstractInterpretationProofs.vo \| 0m16.91s \|\| +0m10.07s \| +59.60% 3m15.98s \| p384_32.c \| 3m07.78s \|\| +0m08.19s \| +4.36% 0m42.52s \| ExtractionHaskell/word_by_word_montgomery \| 0m44.60s \|\| -0m02.07s \| -4.66% 0m28.63s \| ExtractionHaskell/unsaturated_solinas \| 0m31.38s \|\| -0m02.75s \| -8.76% 0m21.76s \| ExtractionHaskell/saturated_solinas \| 0m24.56s \|\| -0m02.79s \| -11.40% 0m09.87s \| ExtractionOCaml/unsaturated_solinas \| 0m11.28s \|\| -0m01.41s \| -12.50% 1m59.22s \| RewriterWf2.vo \| 2m00.09s \|\| -0m00.87s \| -0.72% 1m07.03s \| Fancy/Montgomery256.vo \| 1m07.31s \|\| -0m00.28s \| -0.41% 0m52.60s \| Fancy/Barrett256.vo \| 0m53.16s \|\| -0m00.55s \| -1.05% 0m48.17s \| RewriterInterpProofs1.vo \| 0m48.72s \|\| -0m00.54s \| -1.12% 0m40.16s \| AbstractInterpretationWf.vo \| 0m40.23s \|\| -0m00.07s \| -0.17% 0m38.35s \| p521_32.c \| 0m38.26s \|\| +0m00.09s \| +0.23% 0m31.56s \| p521_64.c \| 0m31.53s \|\| +0m00.02s \| +0.09% 0m24.64s \| RewriterWf1.vo \| 0m24.01s \|\| +0m00.62s \| +2.62% 0m23.54s \| AbstractInterpretationZRangeProofs.vo \| 0m23.64s \|\| -0m00.10s \| -0.42% 0m23.48s \| PushButtonSynthesis/WordByWordMontgomery.vo \| 0m23.26s \|\| +0m00.21s \| +0.94% 0m20.92s \| SlowPrimeSynthesisExamples.vo \| 0m20.62s \|\| +0m00.30s \| +1.45% 0m19.92s \| PushButtonSynthesis/UnsaturatedSolinas.vo \| 0m19.80s \|\| +0m00.12s \| +0.60% 0m16.60s \| ExtractionOCaml/word_by_word_montgomery \| 0m17.56s \|\| -0m00.95s \| -5.46% 0m14.72s \| p448_solinas_64.c \| 0m14.66s \|\| +0m00.06s \| +0.40% 0m13.70s \| secp256k1_32.c \| 0m13.45s \|\| +0m00.25s \| +1.85% 0m13.68s \| p256_32.c \| 0m13.33s \|\| +0m00.34s \| +2.62% 0m13.28s \| CStringification.vo \| 0m13.26s \|\| +0m00.01s \| +0.15% 0m11.88s \| p484_64.c \| 0m11.74s \|\| +0m00.14s \| +1.19% 0m09.96s \| ExtractionOCaml/word_by_word_montgomery.ml \| 0m10.24s \|\| -0m00.27s \| -2.73% 0m07.47s \| ExtractionOCaml/saturated_solinas \| 0m07.93s \|\| -0m00.46s \| -5.80% 0m06.78s \| BoundsPipeline.vo \| 0m05.96s \|\| +0m00.82s \| +13.75% 0m06.72s \| ExtractionOCaml/unsaturated_solinas.ml \| 0m07.03s \|\| -0m00.31s \| -4.40% 0m06.38s \| p224_32.c \| 0m06.54s \|\| -0m00.16s \| -2.44% 0m06.21s \| ExtractionHaskell/word_by_word_montgomery.hs \| 0m06.34s \|\| -0m00.12s \| -2.05% 0m05.45s \| p384_64.c \| 0m05.18s \|\| +0m00.27s \| +5.21% 0m04.82s \| ExtractionHaskell/unsaturated_solinas.hs \| 0m04.84s \|\| -0m00.01s \| -0.41% 0m04.80s \| ExtractionOCaml/saturated_solinas.ml \| 0m05.07s \|\| -0m00.27s \| -5.32% 0m03.83s \| ExtractionHaskell/saturated_solinas.hs \| 0m04.07s \|\| -0m00.24s \| -5.89% 0m03.30s \| PushButtonSynthesis/Primitives.vo \| 0m03.31s \|\| -0m00.01s \| -0.30% 0m03.26s \| PushButtonSynthesis/SmallExamples.vo \| 0m03.24s \|\| +0m00.01s \| +0.61% 0m03.08s \| PushButtonSynthesis/SaturatedSolinas.vo \| 0m02.96s \|\| +0m00.12s \| +4.05% 0m02.16s \| curve25519_32.c \| 0m02.16s \|\| +0m00.00s \| +0.00% 0m01.57s \| curve25519_64.c \| 0m01.47s \|\| +0m00.10s \| +6.80% 0m01.40s \| CLI.vo \| 0m01.32s \|\| +0m00.07s \| +6.06% 0m01.27s \| PushButtonSynthesis/MontgomeryReduction.vo \| 0m01.19s \|\| +0m00.08s \| +6.72% 0m01.26s \| StandaloneHaskellMain.vo \| 0m01.18s \|\| +0m00.08s \| +6.77% 0m01.22s \| PushButtonSynthesis/BarrettReduction.vo \| 0m01.29s \|\| -0m00.07s \| -5.42% 0m01.13s \| RewriterProofs.vo \| 0m01.10s \|\| +0m00.02s \| +2.72% 0m01.10s \| secp256k1_64.c \| 0m01.01s \|\| +0m00.09s \| +8.91% 0m01.08s \| StandaloneOCamlMain.vo \| 0m01.13s \|\| -0m00.04s \| -4.42% 0m01.06s \| p256_64.c \| 0m01.02s \|\| +0m00.04s \| +3.92% 0m01.05s \| AbstractInterpretation.vo \| 0m01.00s \|\| +0m00.05s \| +5.00% 0m01.00s \| CompilersTestCases.vo \| 0m01.08s \|\| -0m00.08s \| -7.40% 0m01.00s \| p224_64.c \| 0m01.00s \|\| +0m00.00s \| +0.00%

| | | | | | | |

Also remove a rewrite rule using cast from the non-cast arith rules, regenerate the .out files, add ident.gets_inlined for eventual use in the rewriter, and generalize the rewrite rule lemmas over cast_out_of_range so that we can actually make use of their proofs for interp.

|

Unless we explicitly say not to. The ability to explicitly say not to is required for, e.g., eta-expansion where we want to replace variable lists of known length with with cons cells indexing into the variable list, but don't want to pollute the code with casts. Uniformity in this way allows rewrite rules to not blow up exponentially (in the number of wildcards); we previously required a separate rewrite rule for each way of choosing between wildcard and literal. To preserve output of the pipeline, we add another pass that just strips the casts off of literals at the end. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 20m27.24s | Total | 22m39.70s || -2m12.46s | -9.74% -------------------------------------------------------------------------------------------- 0m44.27s | Rewriter.vo | 2m11.58s || -1m27.31s | -66.35% 1m15.23s | RewriterRulesInterpGood.vo | 1m50.28s || -0m35.04s | -31.78% 1m40.19s | RewriterRulesGood.vo | 1m58.05s || -0m17.85s | -15.12% 0m26.99s | AbstractInterpretationProofs.vo | 0m16.91s || +0m10.07s | +59.60% 3m15.98s | p384_32.c | 3m07.78s || +0m08.19s | +4.36% 0m42.52s | ExtractionHaskell/word_by_word_montgomery | 0m44.60s || -0m02.07s | -4.66% 0m28.63s | ExtractionHaskell/unsaturated_solinas | 0m31.38s || -0m02.75s | -8.76% 0m21.76s | ExtractionHaskell/saturated_solinas | 0m24.56s || -0m02.79s | -11.40% 0m09.87s | ExtractionOCaml/unsaturated_solinas | 0m11.28s || -0m01.41s | -12.50% 1m59.22s | RewriterWf2.vo | 2m00.09s || -0m00.87s | -0.72% 1m07.03s | Fancy/Montgomery256.vo | 1m07.31s || -0m00.28s | -0.41% 0m52.60s | Fancy/Barrett256.vo | 0m53.16s || -0m00.55s | -1.05% 0m48.17s | RewriterInterpProofs1.vo | 0m48.72s || -0m00.54s | -1.12% 0m40.16s | AbstractInterpretationWf.vo | 0m40.23s || -0m00.07s | -0.17% 0m38.35s | p521_32.c | 0m38.26s || +0m00.09s | +0.23% 0m31.56s | p521_64.c | 0m31.53s || +0m00.02s | +0.09% 0m24.64s | RewriterWf1.vo | 0m24.01s || +0m00.62s | +2.62% 0m23.54s | AbstractInterpretationZRangeProofs.vo | 0m23.64s || -0m00.10s | -0.42% 0m23.48s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.26s || +0m00.21s | +0.94% 0m20.92s | SlowPrimeSynthesisExamples.vo | 0m20.62s || +0m00.30s | +1.45% 0m19.92s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.80s || +0m00.12s | +0.60% 0m16.60s | ExtractionOCaml/word_by_word_montgomery | 0m17.56s || -0m00.95s | -5.46% 0m14.72s | p448_solinas_64.c | 0m14.66s || +0m00.06s | +0.40% 0m13.70s | secp256k1_32.c | 0m13.45s || +0m00.25s | +1.85% 0m13.68s | p256_32.c | 0m13.33s || +0m00.34s | +2.62% 0m13.28s | CStringification.vo | 0m13.26s || +0m00.01s | +0.15% 0m11.88s | p484_64.c | 0m11.74s || +0m00.14s | +1.19% 0m09.96s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.24s || -0m00.27s | -2.73% 0m07.47s | ExtractionOCaml/saturated_solinas | 0m07.93s || -0m00.46s | -5.80% 0m06.78s | BoundsPipeline.vo | 0m05.96s || +0m00.82s | +13.75% 0m06.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.03s || -0m00.31s | -4.40% 0m06.38s | p224_32.c | 0m06.54s || -0m00.16s | -2.44% 0m06.21s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.34s || -0m00.12s | -2.05% 0m05.45s | p384_64.c | 0m05.18s || +0m00.27s | +5.21% 0m04.82s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.84s || -0m00.01s | -0.41% 0m04.80s | ExtractionOCaml/saturated_solinas.ml | 0m05.07s || -0m00.27s | -5.32% 0m03.83s | ExtractionHaskell/saturated_solinas.hs | 0m04.07s || -0m00.24s | -5.89% 0m03.30s | PushButtonSynthesis/Primitives.vo | 0m03.31s || -0m00.01s | -0.30% 0m03.26s | PushButtonSynthesis/SmallExamples.vo | 0m03.24s || +0m00.01s | +0.61% 0m03.08s | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.96s || +0m00.12s | +4.05% 0m02.16s | curve25519_32.c | 0m02.16s || +0m00.00s | +0.00% 0m01.57s | curve25519_64.c | 0m01.47s || +0m00.10s | +6.80% 0m01.40s | CLI.vo | 0m01.32s || +0m00.07s | +6.06% 0m01.27s | PushButtonSynthesis/MontgomeryReduction.vo | 0m01.19s || +0m00.08s | +6.72% 0m01.26s | StandaloneHaskellMain.vo | 0m01.18s || +0m00.08s | +6.77% 0m01.22s | PushButtonSynthesis/BarrettReduction.vo | 0m01.29s || -0m00.07s | -5.42% 0m01.13s | RewriterProofs.vo | 0m01.10s || +0m00.02s | +2.72% 0m01.10s | secp256k1_64.c | 0m01.01s || +0m00.09s | +8.91% 0m01.08s | StandaloneOCamlMain.vo | 0m01.13s || -0m00.04s | -4.42% 0m01.06s | p256_64.c | 0m01.02s || +0m00.04s | +3.92% 0m01.05s | AbstractInterpretation.vo | 0m01.00s || +0m00.05s | +5.00% 0m01.00s | CompilersTestCases.vo | 0m01.08s || -0m00.08s | -7.40% 0m01.00s | p224_64.c | 0m01.00s || +0m00.00s | +0.00%