Compilers « src - fiat-crypto - fast, formally verified cryptography

Mode	Name	Size
-rw-r--r--	CommonSubexpressionElimination.v	11325	log plain
-rw-r--r--	CommonSubexpressionEliminationDenote.v	6291	log plain
-rw-r--r--	CommonSubexpressionEliminationInterp.v	10744	log plain
-rw-r--r--	CommonSubexpressionEliminationProperties.v	11123	log plain
-rw-r--r--	CommonSubexpressionEliminationWf.v	12792	log plain
-rw-r--r--	Conversion.v	4098	log plain
-rw-r--r--	CountLets.v	2521	log plain
-rw-r--r--	Equality.v	4236	log plain
-rw-r--r--	Eta.v	3353	log plain
-rw-r--r--	EtaInterp.v	5747	log plain
-rw-r--r--	EtaWf.v	4891	log plain
-rw-r--r--	ExprInversion.v	13749	log plain
-rw-r--r--	FilterLive.v	2861	log plain
-rw-r--r--	FoldTypes.v	1574	log plain
-rw-r--r--	GeneralizeVar.v	1850	log plain
-rw-r--r--	GeneralizeVarInterp.v	3874	log plain
-rw-r--r--	GeneralizeVarWf.v	3594	log plain
d---------	InSet	116	log plain
-rw-r--r--	Inline.v	4627	log plain
-rw-r--r--	InlineConstAndOp.v	6791	log plain
-rw-r--r--	InlineConstAndOpByRewrite.v	4113	log plain
-rw-r--r--	InlineConstAndOpByRewriteInterp.v	6050	log plain
-rw-r--r--	InlineConstAndOpByRewriteWf.v	7890	log plain
-rw-r--r--	InlineConstAndOpInterp.v	6978	log plain
-rw-r--r--	InlineConstAndOpWf.v	9753	log plain
-rw-r--r--	InlineInterp.v	5807	log plain
-rw-r--r--	InlineWf.v	9904	log plain
-rw-r--r--	InputSyntax.v	11245	log plain
-rw-r--r--	InterpByIso.v	1563	log plain
-rw-r--r--	InterpByIsoProofs.v	5436	log plain
-rw-r--r--	InterpProofs.v	2609	log plain
-rw-r--r--	InterpRewriting.v	7666	log plain
-rw-r--r--	InterpSideConditions.v	2090	log plain
-rw-r--r--	InterpWf.v	3036	log plain
-rw-r--r--	InterpWfRel.v	4255	log plain
-rw-r--r--	Intros.v	3868	log plain
-rw-r--r--	Linearize.v	4684	log plain
-rw-r--r--	LinearizeInterp.v	5834	log plain
-rw-r--r--	LinearizeWf.v	7271	log plain
-rw-r--r--	Map.v	1259	log plain
-rw-r--r--	MapBaseType.v	4847	log plain
-rw-r--r--	MapBaseTypeWf.v	4907	log plain
-rw-r--r--	MapCastByDeBruijn.v	3265	log plain
-rw-r--r--	MapCastByDeBruijnInterp.v	7431	log plain
-rw-r--r--	MapCastByDeBruijnWf.v	5944	log plain
-rw-r--r--	MultiSizeTest.v	7456	log plain
d---------	Named	1735	log plain
-rw-r--r--	Reify.v	27349	log plain
-rw-r--r--	Relations.v	18312	log plain
-rw-r--r--	RenameBinders.v	3071	log plain
-rw-r--r--	Rewriter.v	1541	log plain
-rw-r--r--	RewriterInterp.v	2162	log plain
-rw-r--r--	RewriterWf.v	2347	log plain
-rw-r--r--	SmartMap.v	23107	log plain
-rw-r--r--	StripExpr.v	1148	log plain
-rw-r--r--	Syntax.v	6171	log plain
-rw-r--r--	TestCase.v	13103	log plain
-rw-r--r--	Tuple.v	4154	log plain
-rw-r--r--	TypeInversion.v	7641	log plain
-rw-r--r--	TypeUtil.v	1426	log plain
-rw-r--r--	Wf.v	3207	log plain
-rw-r--r--	WfInversion.v	7163	log plain
-rw-r--r--	WfProofs.v	21039	log plain
-rw-r--r--	WfReflective.v	14089	log plain
-rw-r--r--	WfReflectiveGen.v	16987	log plain
d---------	Z	1792	log plain
d---------	ZExtended	429	log plain