NewPipeline « Experiments « src - fiat-crypto - fast, formally verified cryptography

Mode	Name	Size
-rw-r--r--	AbstractInterpretation.v	50620	log plain
-rw-r--r--	AbstractInterpretationProofs.v	50401	log plain
-rw-r--r--	AbstractInterpretationWf.v	52769	log plain
-rw-r--r--	Arithmetic.v	189131	log plain
-rw-r--r--	CLI.v	16419	log plain
-rw-r--r--	CStringification.v	125982	log plain
-rw-r--r--	CompilersTestCases.v	13823	log plain
d---------	ExtractionHaskell	149	log plain
d---------	ExtractionOCaml	149	log plain
-rw-r--r--	GENERATEDIdentifiersWithoutTypes.v	107858	log plain
-rw-r--r--	GENERATEDIdentifiersWithoutTypesProofs.v	3266	log plain
-rw-r--r--	Language.v	78814	log plain
-rw-r--r--	LanguageInversion.v	35292	log plain
-rw-r--r--	LanguageWf.v	64236	log plain
-rw-r--r--	MiscCompilerPasses.v	6585	log plain
-rw-r--r--	MiscCompilerPassesProofs.v	9251	log plain
-rw-r--r--	README.md	4447	log plain
-rw-r--r--	Rewriter.v	115113	log plain
-rw-r--r--	RewriterProofs.v	94810	log plain
-rw-r--r--	SlowPrimeSynthesisExamples.v	60994	log plain
-rw-r--r--	StandaloneHaskellMain.v	2984	log plain
-rw-r--r--	StandaloneOCamlMain.v	4312	log plain
-rw-r--r--	Toplevel1.v	183894	log plain
-rw-r--r--	Toplevel2.v	158868	log plain
-rw-r--r--	UnderLets.v	8413	log plain
-rw-r--r--	UnderLetsProofs.v	35967	log plain
-rw-r--r--	arith_rewrite_head.out	112246	log plain
-rw-r--r--	fancy_rewrite_head.out	114520	log plain
-rw-r--r--	haskell.sed	179	log plain
-rw-r--r--	nbe_rewrite_head.out	122204	log plain