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

Mode	Name	Size
-rw-r--r--	AbstractInterpretation.v	52862	log plain
-rw-r--r--	AbstractInterpretationProofs.v	83456	log plain
-rw-r--r--	AbstractInterpretationWf.v	55036	log plain
-rw-r--r--	AbstractInterpretationZRangeProofs.v	35666	log plain
-rw-r--r--	Arithmetic.v	184963	log plain
-rw-r--r--	CLI.v	18313	log plain
-rw-r--r--	CStringification.v	125991	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	154210	log plain
-rw-r--r--	GENERATEDIdentifiersWithoutTypesProofs.v	8653	log plain
-rw-r--r--	Language.v	79752	log plain
-rw-r--r--	LanguageInversion.v	33875	log plain
-rw-r--r--	LanguageWf.v	69285	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	133987	log plain
-rw-r--r--	RewriterProofs.v	5427	log plain
-rw-r--r--	RewriterRulesGood.v	21851	log plain
-rw-r--r--	RewriterWf1.v	54963	log plain
-rw-r--r--	RewriterWf2.v	72858	log plain
-rw-r--r--	SlowPrimeSynthesisExamples.v	61029	log plain
-rw-r--r--	StandaloneHaskellMain.v	2799	log plain
-rw-r--r--	StandaloneOCamlMain.v	4129	log plain
-rw-r--r--	Toplevel1.v	184377	log plain
-rw-r--r--	Toplevel2.v	157664	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	97116	log plain
-rw-r--r--	fancy_rewrite_head.out	92473	log plain
-rw-r--r--	haskell.sed	179	log plain
-rw-r--r--	nbe_rewrite_head.out	171650	log plain