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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Continue proofs about Abstr.v	Yann Herklotz	2023-05-04	4	-279/+331
\|
*	Add IfConversionOracle.ml	Yann Herklotz	2023-05-04	1	-0/+43
\|
*	Add structural equality for predicates	Yann Herklotz	2023-05-02	1	-0/+29
\|
*	Fix warnings introduced by Coq 8.17	Yann Herklotz	2023-05-02	1	-8/+14
\|
*	Fix definitions of structural equality	Yann Herklotz	2023-05-02	1	-18/+125
\|
*	Add relations to the NonEmpty module	Yann Herklotz	2023-05-02	1	-0/+77
\|
*	Update Sat.v names	Yann Herklotz	2023-04-28	2	-300/+280
\|
*	Finish decidability proof of SAT	Yann Herklotz	2023-04-28	1	-39/+219
\|
*	Update to Coq 8.17 and CompCert 3.12	Yann Herklotz	2023-04-27	6	-112/+9
\|
*	Change nat to positive in Sat proof	Yann Herklotz	2023-04-27	8	-68/+202
\|
*	Work on finishing the SAT decidability proofs	Yann Herklotz	2023-04-24	1	-26/+44
\|
*	Added lemmas about decidability of Sat	Yann Herklotz	2023-04-24	3	-117/+293
\|
*	Add temp files	Yann Herklotz	2023-03-12	2	-10/+24
\|
*	Work on proof of norm_expression	Yann Herklotz	2023-02-22	3	-57/+261
\|
*	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	4	-3/+352
\|
*	Change evaluation of predicates and remove forest_evaluable	Yann Herklotz	2023-02-11	4	-100/+125
\|
*	Switch to half lazy evaluation	Yann Herklotz	2023-02-05	3	-52/+113
\|
*	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	2	-41/+99
\|
*	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	2	-6/+13
\|
*	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	2	-43/+344
\|
*	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	2	-37/+312
\|
*	Add proofs for sem_pexpr and app_predicated	Yann Herklotz	2022-10-25	2	-43/+270
\|
*	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	9	-149/+170
\|
*	Add helper functions to NonEmpty.v	Yann Herklotz	2022-10-10	1	-0/+18
\|
*	[sched] Remove some unprovable lemmas	Yann Herklotz	2022-10-06	5	-901/+179
\|
*	Add new if-conversion pass with top-level fold	Yann Herklotz	2022-09-29	3	-65/+83
\|
*	Add proof using to ifconversionproof	Yann Herklotz	2022-09-29	2	-24/+30
\|
*	Add global monad notation using Instances	Yann Herklotz	2022-09-26	10	-104/+169
\| \| \| \|	This was mostly inspired by the std++ library.
*	Add more monads	Yann Herklotz	2022-09-24	3	-1/+63
\|
*	Update and fix the transformation	Yann Herklotz	2022-08-05	4	-272/+313
\|
*	Add back changes to Abstr	Yann Herklotz	2022-08-04	2	-246/+362
\|
*	Add forest type	Yann Herklotz	2022-08-01	1	-3/+8
\|
*	Merge remote-tracking branch 'origin/dev/scheduling' into dev/scheduling	Yann Herklotz	2022-07-31	3	-112/+115
\|\
\| *	Add current changes	Yann Herklotz	2022-07-31	2	-112/+5
\| \|
\| *	Add NonEmpty.v	Yann Herklotz	2022-07-31	1	-0/+110
\| \|
* \|	Start refactor in Abstr	Yann Herklotz	2022-07-31	1	-14/+29
\|/