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

	Commit message (Collapse)	Author	Age	Files	Lines
*	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
\|
*	Fix unsigned/signed issues.	James Pollard	2020-06-28	2	-21/+30
\|
*	Work on proof.	James Pollard	2020-06-28	2	-0/+53
\|
*	Finish ILoad proof with some assumptions:	James Pollard	2020-06-24	1	-184/+163
\| \| \| \| \| \|	* EXPR_OK: Yann to work on this. * READ_BOUNDS: To axiomise (or find a better solution). * 32-bit range of register values.
*	Normalise entire expression to avoid overflow issues.	James Pollard	2020-06-23	2	-0/+245
\|
*	Tidy up proof for Aindexed2scaled.	James Pollard	2020-06-22	1	-1/+54
\|
*	Some (very) useful lemmas about arrays.	James Pollard	2020-06-17	1	-0/+2
\|
*	Fix array semantics merge granularity.	James Pollard	2020-06-17	1	-0/+7
\|
*	Move some standard tactics to Coquplib.	James Pollard	2020-06-14	1	-0/+10
\|
*	Continuing work on proving specification	Yann Herklotz	2020-05-25	1	-0/+6
\|
*	Add statemonad declaration	Yann Herklotz	2020-05-24	2	-0/+103
\|
*	Remove Admitted Maps Lemma	Yann Herklotz	2020-05-07	1	-6/+0
\|
*	Add do notation for option	Yann Herklotz	2020-04-15	1	-0/+11
\|
*	Add documentation and fix makefile for Compcert	Yann Herklotz	2020-03-31	3	-75/+75
\|
*	Update printing	Yann Herklotz	2020-03-25	1	-0/+4
\|
*	Remove dunes and make the build recursive	Yann Herklotz	2020-03-25	1	-3/+0
\|
*	Add Maps and HTL.v	Yann Herklotz	2020-03-25	1	-0/+49
\|
*	Add compcert library to coquplib	Yann Herklotz	2020-03-22	1	-0/+4
\|
*	Convert Tactics to Coquplib: export common modules	Yann Herklotz	2020-03-20	1	-1/+8
\|
*	Lower case folders	Yann Herklotz	2020-03-19	4	-0/+132