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

Mode	Name	Size
-rw-r--r--	AbstractInterpretation.v	52064	log plain
-rw-r--r--	AbstractInterpretationProofs.v	82135	log plain
-rw-r--r--	AbstractInterpretationWf.v	54220	log plain
-rw-r--r--	AbstractInterpretationZRangeProofs.v	35828	log plain
-rw-r--r--	Arithmetic.v	193759	log plain
-rw-r--r--	CLI.v	18754	log plain
-rw-r--r--	CStringification.v	125991	log plain
-rw-r--r--	CompilersTestCases.v	14051	log plain
d---------	ExtractionHaskell	149	log plain
d---------	ExtractionOCaml	149	log plain
-rw-r--r--	GENERATEDIdentifiersWithoutTypes.v	152475	log plain
-rw-r--r--	GENERATEDIdentifiersWithoutTypesProofs.v	10359	log plain
-rw-r--r--	Language.v	82127	log plain
-rw-r--r--	LanguageInversion.v	37042	log plain
-rw-r--r--	LanguageWf.v	86469	log plain
-rw-r--r--	MiscCompilerPasses.v	5142	log plain
-rw-r--r--	MiscCompilerPassesProofs.v	8817	log plain
-rw-r--r--	README.md	4451	log plain
-rw-r--r--	Rewriter.v	161651	log plain
-rw-r--r--	RewriterInterpProofs1.v	83903	log plain
-rw-r--r--	RewriterProofs.v	10878	log plain
-rw-r--r--	RewriterRulesGood.v	23505	log plain
-rw-r--r--	RewriterRulesInterpGood.v	46925	log plain
-rw-r--r--	RewriterWf1.v	142077	log plain
-rw-r--r--	RewriterWf2.v	59927	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	192052	log plain
-rw-r--r--	Toplevel2.v	158738	log plain
-rw-r--r--	UnderLets.v	8489	log plain
-rw-r--r--	UnderLetsProofs.v	55837	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	517194	log plain
-rw-r--r--	haskell.sed	179	log plain
-rw-r--r--	nbe_rewrite_head.out	118667	log plain