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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add fixes to main memory generation proof	Yann Herklotz	2023-07-31	2	-799/+808
\|
*	Remove RTLParFu and fix DMemorygen.v	Yann Herklotz	2023-07-31	5	-1974/+1949
\|
*	Add beginning to memory generation proof	Yann Herklotz	2023-07-29	17	-2662/+6789
\|
*	Add equivalence classes	Yann Herklotz	2023-07-11	6	-191/+334
\|
*	Add if-conversion decision procedure	Yann Herklotz	2023-07-06	5	-27/+53
\|
*	Finish some proofs and remove unnecessary Admitted	Yann Herklotz	2023-06-26	5	-32/+74
\|
*	Finish mutual exclusivity check	Yann Herklotz	2023-06-25	4	-30/+121
\|
*	Finish SMT proof	Yann Herklotz	2023-06-23	1	-3/+100
\|
*	Add SMTCoq solver as dependency	Yann Herklotz	2023-06-21	6	-47/+216
\|
*	Finish complete evaluability proof	Yann Herklotz	2023-06-10	1	-19/+88
\|
*	Try to prove main theorem	Yann Herklotz	2023-06-10	1	-0/+5
\| \| \| \|	Missing some link between forests
*	Add more to proof of evaluability	Yann Herklotz	2023-06-10	2	-1/+57
\|
*	Finish abstract_sequence_evaluable_m	Yann Herklotz	2023-06-09	1	-1/+104
\|
*	Prove abstract_sequence_evaluable	Yann Herklotz	2023-06-09	1	-0/+2
\|
*	Finish abstract_sequence_evaluable_fold2	Yann Herklotz	2023-06-09	1	-5/+42
\|
*	Finish abstract_sequence_evaluable_fold	Yann Herklotz	2023-06-09	1	-12/+68
\|
*	Add outline of proof of evaluable when predicate is false	Yann Herklotz	2023-06-09	1	-19/+54
\|
*	Add proof outline for evaluability	Yann Herklotz	2023-06-08	2	-20/+44
\|
*	Work towards proving evaluability	Yann Herklotz	2023-06-05	3	-38/+169
\|
*	Move around generating functions	Yann Herklotz	2023-06-03	2	-68/+68
\|
*	Fix proof of predicates completely	Yann Herklotz	2023-06-02	2	-7/+24
\|
*	Fix top-level proof with Isetpred missing	Yann Herklotz	2023-06-02	1	-12/+55
\|
*	Finished the propert version of from_predicated_sem_pred_expr2	Yann Herklotz	2023-06-02	6	-44/+304
\|
*	Finish from_predicated_sem_pred_expr	Yann Herklotz	2023-05-31	1	-8/+97
\|
*	Remove unnecessary assumption from sem_merge_list	Yann Herklotz	2023-05-30	1	-4/+3
\|
*	Fix other proofs and attempt from_predicated proof	Yann Herklotz	2023-05-30	1	-7/+26
\|
*	Prove merge list_translation	Yann Herklotz	2023-05-30	1	-2/+16
\|
*	Prove fold_right over Elist	Yann Herklotz	2023-05-30	1	-4/+74
\|
*	Finish second flap2 proof	Yann Herklotz	2023-05-30	1	-1/+9
\|
*	Finished painful product proof	Yann Herklotz	2023-05-30	4	-11/+125
\|
*	Prove more admitted theorems	Yann Herklotz	2023-05-29	5	-47/+169
\|
*	Finish two AbstrSemIdent false proofs	Yann Herklotz	2023-05-28	1	-11/+50
\|
*	Finish max predicate proof	Yann Herklotz	2023-05-28	1	-1/+78
\|
*	Finish proofs in GiblePargenproofForward.v	Yann Herklotz	2023-05-28	2	-5/+49
\|
*	Work on forward proofs	Yann Herklotz	2023-05-28	2	-1/+18
\|
*	Finish proofs in GiblePargenproofBackward.v	Yann Herklotz	2023-05-27	1	-26/+101
\|
*	Add proofs of gather_predicates	Yann Herklotz	2023-05-26	1	-25/+196
\|
*	Finish predicate inclusion proofs	Yann Herklotz	2023-05-25	1	-48/+99
\|
*	Finish gather_predicate proofs	Yann Herklotz	2023-05-24	1	-17/+502
\|
*	Prove evaluability of predicates throughout	Yann Herklotz	2023-05-22	1	-61/+126
\|
*	Work on smaller evaluability proof	Yann Herklotz	2023-05-22	1	-49/+88
\|
*	Finish abstr_seq_reverse_correct_fold	Yann Herklotz	2023-05-21	3	-35/+116
\|
*	Add proof about preds_empty	Yann Herklotz	2023-05-21	1	-3/+12
\|
*	Add proofs about RBexit	Yann Herklotz	2023-05-21	1	-2/+63
\|
*	Prove evaluable_pred_expr_exists_RBsetpred	Yann Herklotz	2023-05-21	4	-100/+493
\|
*	Work on evaluability proof	Yann Herklotz	2023-05-19	1	-0/+37
\|
*	Prepare work on evaluability of instructions	Yann Herklotz	2023-05-19	3	-71/+133
\|
*	Finish evaluability proof of RBop	Yann Herklotz	2023-05-19	5	-210/+338
\|
*	Add new proofs about semantic identity	Yann Herklotz	2023-05-18	4	-599/+868
\|
*	Work on scheduling proof	Yann Herklotz	2023-05-16	4	-25/+154
\|