vericert - Vericert is a formally verified high-level synthesis tool.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Finished painful product proof	Yann Herklotz	2023-05-30	1	-4/+4
\|
*	Rename backwards proof	Yann Herklotz	2023-05-12	1	-30/+4
\|
*	Split proof up into more files	Yann Herklotz	2023-05-09	1	-2006/+79
\|
*	Add assumption and prove assumption that preds are evaluable	Yann Herklotz	2023-05-06	1	-0/+1
\|
*	Add check for mutexcl and fix top-level proof	Yann Herklotz	2023-05-06	1	-18/+33
\|
*	Finish forward and backward proofs for predicated proof	Yann Herklotz	2023-05-05	1	-90/+0
\|
*	Change nat to positive in Sat proof	Yann Herklotz	2023-04-27	1	-8/+4
\|
*	Added lemmas about decidability of Sat	Yann Herklotz	2023-04-24	1	-21/+0
\|
*	Work on proof of norm_expression	Yann Herklotz	2023-02-22	1	-48/+0
\|
*	Remove aborted evaluable proofs	Yann Herklotz	2023-02-18	1	-96/+4
\|
*	Prove abstr_fold_falsy correct	Yann Herklotz	2023-02-12	1	-21/+100
\|
*	Prove sem_update_instr_term correct	Yann Herklotz	2023-02-12	1	-8/+19
\|
*	Prove abstr_fold_correct inductive case fully	Yann Herklotz	2023-02-12	1	-12/+15
\|
*	Finish eval_predf_update_true	Yann Herklotz	2023-02-12	1	-3/+6
\|
*	Finish sem_update_instr finally	Yann Herklotz	2023-02-12	1	-3/+247
\|
*	Change evaluation of predicates and remove forest_evaluable	Yann Herklotz	2023-02-11	1	-84/+52
\|
*	Switch to half lazy evaluation	Yann Herklotz	2023-02-05	1	-43/+84
\|
*	Work on intermediate lemma for evaluation	Yann Herklotz	2023-01-29	1	-5/+12
\|
*	Prove abstr_fold_correct top-down	Yann Herklotz	2023-01-29	1	-41/+94
\|
*	Add documentation and continue on top-down proof	Yann Herklotz	2023-01-28	1	-6/+54
\|
*	Work on simplifying seq_app evaluation lemma	Yann Herklotz	2023-01-02	1	-6/+11
\|
*	Add all_evaluable lemma for seq_app	Yann Herklotz	2023-01-01	1	-0/+9
\|
*	Add proofs about evaluation of body of expressions	Yann Herklotz	2022-12-27	1	-7/+59
\|
*	Add proofs about evaluability of predicates in the abstract state	Yann Herklotz	2022-12-24	1	-23/+55
\|
*	Add todo	Yann Herklotz	2022-12-01	1	-76/+163
\|
*	Prove top level theorems with evaluability	Yann Herklotz	2022-11-15	1	-43/+333
\|
*	Add proofs about evaluability of predicates	Yann Herklotz	2022-11-10	1	-18/+132
\|
*	Add many more proofs about sem_pred_expr	Yann Herklotz	2022-10-26	1	-36/+311
\|
*	Add proofs for sem_pexpr and app_predicated	Yann Herklotz	2022-10-25	1	-43/+269
\|
*	Prove sem_update for load and create lemma	Yann Herklotz	2022-10-24	1	-3/+51
\|
*	Work on abstract lemmas for update function	Yann Herklotz	2022-10-20	1	-8/+318
\|
*	Clean up proofs	Yann Herklotz	2022-10-11	1	-11/+31
\|
*	[sched] Remove some unprovable lemmas	Yann Herklotz	2022-10-06	1	-842/+113
\|
*	Add global monad notation using Instances	Yann Herklotz	2022-09-26	1	-83/+75
\| \| \| \|	This was mostly inspired by the std++ library.
*	Update and fix the transformation	Yann Herklotz	2022-08-05	1	-252/+253
\|
*	Update lemmas with new update function	Yann Herklotz	2022-07-26	1	-35/+128
\|
*	Fix main proof	Yann Herklotz	2022-07-20	1	-21/+27
\|
*	Work on implementing abstract predicates	Yann Herklotz	2022-07-19	1	-10/+10
\|
*	Add work on abstract predicates	Yann Herklotz	2022-07-14	1	-35/+223
\|
*	Working on scheduling proof	Yann Herklotz	2022-07-04	1	-53/+147
\|
*	Try and fix pargenproof	Yann Herklotz	2022-07-04	1	-8/+7
\|
*	Add work on scheduling	Yann Herklotz	2022-07-03	1	-15/+11
\|
*	Rewrite a lot fixing scheduling of Gible	Yann Herklotz	2022-05-27	1	-0/+1148