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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Finish some proofs and remove unnecessary Admitted	Yann Herklotz	2023-06-26	7	-33/+76
\|
*	Finish mutual exclusivity check	Yann Herklotz	2023-06-25	5	-31/+150
\|
*	Finish SMT proof	Yann Herklotz	2023-06-23	1	-3/+100
\|
*	Add SMTCoq solver as dependency	Yann Herklotz	2023-06-21	14	-71/+233
\|
*	Update makefile to build cohpred	Yann Herklotz	2023-06-19	1	-2/+6
\|
*	Update cohpred library	Yann Herklotz	2023-06-18	1	-0/+0
\|
*	Update cohpred git submodule	Yann Herklotz	2023-06-14	2	-1/+1
\|
*	Add CohPred and SMTCoq dependency	Yann Herklotz	2023-06-12	4	-2/+29
\|
*	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
\|
*	Add lp_solve dependency to nix	Yann Herklotz	2023-06-02	1	-1/+1
\|
*	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	7	-44/+316
\|
*	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	5	-13/+127
\|
*	Prove more admitted theorems	Yann Herklotz	2023-05-29	6	-47/+190
\|
*	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	5	-100/+506
\|
*	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	6	-211/+348
\|
*	Add new proofs about semantic identity	Yann Herklotz	2023-05-18	6	-600/+978
\|
*	Work on scheduling proof	Yann Herklotz	2023-05-16	4	-25/+154
\|