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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add beginning to memory generation proof	Yann Herklotz	2023-07-29	1	-7/+8
\|
*	Finish mutual exclusivity check	Yann Herklotz	2023-06-25	1	-1/+29
\|
*	Finished the propert version of from_predicated_sem_pred_expr2	Yann Herklotz	2023-06-02	1	-0/+12
\|
*	Finished painful product proof	Yann Herklotz	2023-05-30	1	-2/+2
\|
*	Prove more admitted theorems	Yann Herklotz	2023-05-29	1	-0/+21
\|
*	Prove evaluable_pred_expr_exists_RBsetpred	Yann Herklotz	2023-05-21	1	-0/+13
\|
*	Add new proofs about semantic identity	Yann Herklotz	2023-05-18	1	-1/+69
\|
*	Split proof up into more files	Yann Herklotz	2023-05-09	1	-0/+11
\|
*	Add check for mutexcl and fix top-level proof	Yann Herklotz	2023-05-06	1	-3/+7
\|
*	Finish forward and backward proofs for predicated proof	Yann Herklotz	2023-05-05	1	-0/+5
\|
*	Add relations to the NonEmpty module	Yann Herklotz	2023-05-02	1	-0/+77
\|
*	Add many more proofs about sem_pred_expr	Yann Herklotz	2022-10-26	1	-1/+1
\|
*	Add proofs for sem_pexpr and app_predicated	Yann Herklotz	2022-10-25	1	-0/+1
\|
*	Clean up proofs	Yann Herklotz	2022-10-11	1	-6/+25
\|
*	Add helper functions to NonEmpty.v	Yann Herklotz	2022-10-10	1	-0/+18
\|
*	[sched] Remove some unprovable lemmas	Yann Herklotz	2022-10-06	1	-2/+1
\|
*	Add global monad notation using Instances	Yann Herklotz	2022-09-26	5	-11/+81
\| \| \| \|	This was mostly inspired by the std++ library.
*	Add more monads	Yann Herklotz	2022-09-24	3	-1/+63
\|
*	Add NonEmpty.v	Yann Herklotz	2022-07-31	1	-0/+110
\|
*	Add the opion monad file	Yann Herklotz	2022-07-20	1	-0/+66
\|
*	Work on implementing abstract predicates	Yann Herklotz	2022-07-19	2	-43/+8
\|
*	Add new block generation for Gible	Yann Herklotz	2022-05-26	1	-2/+5
\|
*	Work on specification of RTLBlock generation	Yann Herklotz	2022-03-28	1	-0/+150
\|
*	Remove literal files again	Yann Herklotz	2022-03-26	1	-2/+3
\|
*	Move forall_ptree into common	Yann Herklotz	2022-03-22	1	-0/+43
\|
*	Update Coq version to 8.14.1	Yann Herklotz	2022-03-02	3	-39/+12
\|
*	Fix warnings for Coq 8.13.2	Yann Herklotz	2021-10-09	2	-6/+6
\|
*	Remove dependency on Tactics	Yann Herklotz	2021-02-16	1	-1/+0
\|
*	Add destruction to context match expressions	Yann Herklotz	2021-01-26	1	-2/+5
\|
*	Fix imports in Coq modules	Yann Herklotz	2021-01-21	3	-26/+35
\|
*	Add correct copyright notices in files	Yann Herklotz	2021-01-10	5	-0/+93
\|
*	Fix build for Coq 8.12.1	Yann Herklotz	2020-11-26	2	-7/+249
\|
*	Update definition of Vneg	Yann Herklotz	2020-11-07	1	-1/+1
\|
*	Finish implementation of shrx_shrx_alt_equiv	Yann Herklotz	2020-11-05	1	-74/+133
\|
*	Proven with some assumptions	Yann Herklotz	2020-11-04	1	-4/+20
\|
*	Continue to prove signed_neg	Yann Herklotz	2020-11-04	1	-1/+44
\|
*	Add to Oshrximm proof	Yann Herklotz	2020-11-03	1	-55/+109
\|
*	Add intextra	Yann Herklotz	2020-11-03	1	-0/+115
\|
*	Rename to Vericertlib	Yann Herklotz	2020-07-17	1	-0/+0
\|
*	Change name to Vericert	Yann Herklotz	2020-07-14	5	-6/+6
\|
*	Merge remote-tracking branch 'james/develop' into develop	Yann Herklotz	2020-07-04	1	-10/+42
\|\
\| *	Working on determinacy proof.	James Pollard	2020-07-04	1	-10/+42
\| \|
* \|	Define ofbytes	Yann Herklotz	2020-07-04	1	-1/+72
\|/
*	Switch to uvalueToZ in lessdef.	James Pollard	2020-07-02	2	-29/+54
\|
*	Remove all <> Admitted	Yann Herklotz	2020-07-02	1	-0/+15
\|
*	Improve (?) automation.	James Pollard	2020-07-01	2	-15/+37
\|
*	Heavy automation of proofs.	James Pollard	2020-06-30	1	-1/+8
\|
*	Eliminate memory bounds assumption!	James Pollard	2020-06-29	1	-2/+2
\|
*	Add missing file.	James Pollard	2020-06-29	1	-0/+34
\|
*	Finish first IStore proof (modulo some admissions).	James Pollard	2020-06-28	1	-12/+12
\|