fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add more interp lemmas	Jason Gross	2018-08-09
\|
*	Add wf_splice_list, wf_splice_list_no_order	Jason Gross	2018-08-03
\|
*	More precise wf_Proper_list_impl	Jason Gross	2018-07-31
\|
*	Comment out wf_splice_list	Jason Gross	2018-07-31
\| \| \| \|	It wasn't actually ready yet
*	Add wf_Proper_list, wf_splice_list	Jason Gross	2018-07-31
\|
*	Add UnderLets.wf_Proper_list	Jason Gross	2018-07-30
\|
*	Add wf_splice	Jason Gross	2018-07-30
\|
*	Integrate Wf and Interp proofs	Jason Gross	2018-07-30
	Now the only admits remaining in Toplevel1 are glue ones about freeze/to_bytes/from_bytes/fe_nonzero. What remains (beyond those admits, and the ones about word-by-word montgomery building blocks in Arithmetic), are the proofs about abstract interpretation and the rewriter. After \| File Name \| Before \|\| Change \| % Change -------------------------------------------------------------------------------------------------------- 12m13.17s \| Total \| 11m45.42s \|\| +0m27.75s \| +3.93% -------------------------------------------------------------------------------------------------------- 3m47.20s \| Experiments/NewPipeline/Toplevel1 \| 3m27.51s \|\| +0m19.68s \| +9.48% 0m17.98s \| Experiments/NewPipeline/UnderLetsProofs \| N/A \|\| +0m17.98s \| ∞ N/A \| Experiments/NewPipeline/UnderLetsWf \| 0m17.94s \|\| -0m17.94s \| -100.00% 4m49.57s \| Experiments/NewPipeline/SlowPrimeSynthesisExamples \| 4m45.22s \|\| +0m04.34s \| +1.52% 1m16.28s \| Experiments/NewPipeline/Toplevel2 \| 1m13.33s \|\| +0m02.95s \| +4.02% 0m02.96s \| Experiments/NewPipeline/MiscCompilerPassesProofs \| N/A \|\| +0m02.96s \| ∞ N/A \| Experiments/NewPipeline/MiscCompilerPassesWf \| 0m02.91s \|\| -0m02.91s \| -100.00% 0m58.32s \| Experiments/NewPipeline/Rewriter \| 0m58.58s \|\| -0m00.25s \| -0.44% 0m28.19s \| Experiments/NewPipeline/LanguageInversion \| 0m28.02s \|\| +0m00.17s \| +0.60% 0m13.14s \| Experiments/NewPipeline/LanguageWf \| 0m13.09s \|\| +0m00.05s \| +0.38% 0m10.11s \| Experiments/NewPipeline/CStringification \| 0m10.12s \|\| -0m00.00s \| -0.09% 0m01.21s \| Experiments/NewPipeline/CLI \| 0m01.19s \|\| +0m00.02s \| +1.68% 0m01.11s \| Experiments/NewPipeline/StandaloneOCamlMain \| 0m01.13s \|\| -0m00.01s \| -1.76% 0m01.09s \| Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes \| 0m01.08s \|\| +0m00.01s \| +0.92% 0m01.05s \| Experiments/NewPipeline/StandaloneHaskellMain \| 0m01.07s \|\| -0m00.02s \| -1.86% 0m00.98s \| Experiments/NewPipeline/Language \| 0m00.96s \|\| +0m00.02s \| +2.08% 0m00.96s \| Experiments/NewPipeline/AbstractInterpretation \| 0m00.90s \|\| +0m00.05s \| +6.66% 0m00.90s \| Experiments/NewPipeline/CompilersTestCases \| 0m00.92s \|\| -0m00.02s \| -2.17% 0m00.66s \| Experiments/NewPipeline/RewriterProofs \| N/A \|\| +0m00.66s \| ∞ 0m00.64s \| Experiments/NewPipeline/MiscCompilerPasses \| 0m00.65s \|\| -0m00.01s \| -1.53% 0m00.42s \| Experiments/NewPipeline/UnderLets \| 0m00.38s \|\| +0m00.03s \| +10.52% 0m00.40s \| Experiments/NewPipeline/AbstractInterpretationProofs \| 0m00.42s \|\| -0m00.01s \| -4.76%