src - fiat-crypto - fast, formally verified cryptography

Mode	Name	Size
-rw-r--r--	AbstractInterpretation.v	52016	log plain
-rw-r--r--	AbstractInterpretationProofs.v	81955	log plain
-rw-r--r--	AbstractInterpretationWf.v	54088	log plain
-rw-r--r--	AbstractInterpretationZRangeProofs.v	35636	log plain
d---------	Algebra	381	log plain
-rw-r--r--	Arithmetic.v	228472	log plain
d---------	Arithmetic	242	log plain
-rw-r--r--	BoundsPipeline.v	29947	log plain
-rw-r--r--	CLI.v	18542	log plain
-rw-r--r--	COperationSpecifications.v	23722	log plain
-rw-r--r--	CStringification.v	126491	log plain
-rw-r--r--	CompilersTestCases.v	13907	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
-rw-r--r--	GENERATEDIdentifiersWithoutTypes.v	152427	log plain
-rw-r--r--	GENERATEDIdentifiersWithoutTypesProofs.v	10287	log plain
-rw-r--r--	Language.v	82127	log plain
-rw-r--r--	LanguageInversion.v	37018	log plain
-rw-r--r--	LanguageWf.v	86421	log plain
-rw-r--r--	MiscCompilerPasses.v	5118	log plain
-rw-r--r--	MiscCompilerPassesProofs.v	8721	log plain
d---------	Primitives	87	log plain
-rw-r--r--	PushButtonSynthesis.v	141995	log plain
d---------	PushButtonSynthesis	46	log plain
-rw-r--r--	Rewriter.v	164549	log plain
-rw-r--r--	RewriterInterpProofs1.v	83735	log plain
-rw-r--r--	RewriterProofs.v	10614	log plain
-rw-r--r--	RewriterRulesGood.v	23337	log plain
-rw-r--r--	RewriterRulesInterpGood.v	47607	log plain
-rw-r--r--	RewriterWf1.v	141933	log plain
-rw-r--r--	RewriterWf2.v	59759	log plain
-rw-r--r--	SlowPrimeSynthesisExamples.v	61025	log plain
d---------	Spec	325	log plain
-rw-r--r--	StandaloneHaskellMain.v	2761	log plain
-rw-r--r--	StandaloneOCamlMain.v	4091	log plain
-rw-r--r--	Toplevel2.v	160866	log plain
-rw-r--r--	UnderLets.v	8465	log plain
-rw-r--r--	UnderLetsProofs.v	55741	log plain
d---------	Util	2783	log plain
-rw-r--r--	arith_rewrite_head.out	75233	log plain
-rw-r--r--	arith_with_casts_rewrite_head.out	125981	log plain
-rw-r--r--	fancy_rewrite_head.out	9200	log plain
-rw-r--r--	fancy_with_casts_rewrite_head.out	635522	log plain
-rw-r--r--	haskell.sed	179	log plain
-rw-r--r--	nbe_rewrite_head.out	118667	log plain