src - fiat-crypto - fast, formally verified cryptography

Mode	Name	Size
-rw-r--r--	AbstractInterpretation.v	56732	log plain
-rw-r--r--	AbstractInterpretationProofs.v	84566	log plain
-rw-r--r--	AbstractInterpretationWf.v	57561	log plain
-rw-r--r--	AbstractInterpretationZRangeProofs.v	37317	log plain
d---------	Algebra	381	log plain
d---------	Arithmetic	703	log plain
-rw-r--r--	BoundsPipeline.v	30979	log plain
-rw-r--r--	CLI.v	21193	log plain
-rw-r--r--	COperationSpecifications.v	23116	log plain
-rw-r--r--	CStringification.v	134903	log plain
-rw-r--r--	CompilersTestCases.v	13933	log plain
d---------	Curves	109	log plain
-rw-r--r--	Demo.v	9935	log plain
d---------	ExtractionHaskell	149	log plain
d---------	ExtractionOCaml	149	log plain
d---------	Fancy	189	log plain
-rw-r--r--	GENERATEDIdentifiersWithoutTypes.v	74628	log plain
-rw-r--r--	GENERATEDIdentifiersWithoutTypesProofs.v	8000	log plain
-rw-r--r--	Language.v	92629	log plain
-rw-r--r--	LanguageInversion.v	41365	log plain
-rw-r--r--	LanguageWf.v	92278	log plain
-rw-r--r--	MiscCompilerPasses.v	5118	log plain
-rw-r--r--	MiscCompilerPassesProofs.v	8721	log plain
-rw-r--r--	PreLanguage.v	2455	log plain
d---------	Primitives	87	log plain
d---------	PushButtonSynthesis	792	log plain
-rw-r--r--	Rewriter.v	139893	log plain
d---------	Rewriter	242	log plain
-rw-r--r--	RewriterAll.v	811	log plain
-rw-r--r--	RewriterAllTactics.v	5126	log plain
-rw-r--r--	RewriterInterpProofs1.v	81473	log plain
-rw-r--r--	RewriterRules.v	49603	log plain
-rw-r--r--	RewriterRulesProofs.v	24975	log plain
-rw-r--r--	RewriterWf1.v	210236	log plain
-rw-r--r--	RewriterWf2.v	59774	log plain
-rw-r--r--	SlowPrimeSynthesisExamples.v	70637	log plain
d---------	Spec	325	log plain
-rw-r--r--	StandaloneHaskellMain.v	2718	log plain
-rw-r--r--	StandaloneOCamlMain.v	4048	log plain
-rw-r--r--	TAPSort.v	480	log plain
-rw-r--r--	UnderLets.v	10675	log plain
-rw-r--r--	UnderLetsProofs.v	78067	log plain
d---------	Util	2823	log plain
-rw-r--r--	haskell.sed	179	log plain