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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Address ram in renaming pass	Michalis Pardalos	2021-09-02	1	-7/+5
\|
*	Get Memorygen to compile again	Michalis Pardalos	2021-08-31	1	-475/+484
\|
*	Clean up Memorygen file	Yann Herklotz	2021-04-07	1	-219/+1
\|
*	No admitted theorems in Memorygen proof (~‾▿‾)~	Yann Herklotz	2021-04-07	1	-76/+99
\|
*	Basically done with proof	Yann Herklotz	2021-04-07	1	-6/+32
\|
*	Let everything compile again	Yann Herklotz	2021-04-06	1	-7/+18
\|
*	Finish load and store proof, but broke top-level	Yann Herklotz	2021-04-06	1	-250/+118
\|
*	Finish Veriloggenproof completely	Yann Herklotz	2021-04-04	1	-18/+60
\|
*	Prove all admit in load but one	Yann Herklotz	2021-04-04	1	-162/+183
\|
*	Finish most of load proof	Yann Herklotz	2021-04-04	1	-21/+167
\|
*	Finish store proof without admit	Yann Herklotz	2021-04-04	1	-187/+526
\|
*	Add declarations	Yann Herklotz	2021-04-01	1	-6/+7
\|
*	Add new enable interface	Yann Herklotz	2021-04-01	1	-35/+46
\|
*	Add memory disable	Yann Herklotz	2021-03-31	1	-156/+293
\|
*	Temporary done	Yann Herklotz	2021-03-30	1	-48/+247
\|
*	Add more checks to the implementation	Yann Herklotz	2021-03-29	1	-27/+82
\|
*	Update declared size	Yann Herklotz	2021-03-28	1	-1/+1
\|
*	Finish main match proof in store	Yann Herklotz	2021-03-28	1	-50/+555
\|
*	Add proofs of size preservation of statements and ram	Yann Herklotz	2021-03-25	1	-47/+92
\|
*	Work more on size-preserving lemmas	Yann Herklotz	2021-03-25	1	-104/+129
\|
*	Add forall_ram proof	Yann Herklotz	2021-03-25	1	-6/+40
\|
*	Prove lt property for statements	Yann Herklotz	2021-03-25	1	-4/+67
\|
*	Add many more array theorems	Yann Herklotz	2021-03-24	1	-4/+100
\|
*	Completed match_arrs_gss proof	Yann Herklotz	2021-03-23	1	-21/+100
\|
*	Complete top-level again with smaller admitted	Yann Herklotz	2021-03-22	1	-24/+48
\|
*	Fix second part of proof again	Yann Herklotz	2021-03-22	1	-18/+43
\|
*	Finish unchanged proof without admits	Yann Herklotz	2021-03-22	1	-21/+175
\|
*	Finish a merging proof	Yann Herklotz	2021-03-21	1	-12/+30
\|
*	Add many lemmas about arrays	Yann Herklotz	2021-03-21	1	-12/+233
\|
*	Add check for ram in module	Yann Herklotz	2021-03-20	1	-16/+161
\|
*	Prove very top-level theorem	Yann Herklotz	2021-03-19	1	-80/+173
\|
*	Fix proof with new array matching	Yann Herklotz	2021-03-17	1	-20/+47
\|
*	Fix main proofs with smaller admits	Yann Herklotz	2021-03-17	1	-25/+50
\|
*	Proof of equivalent stmnt runs with matching start	Yann Herklotz	2021-03-17	1	-155/+263
\|
*	Prove one case of transf_code correct	Yann Herklotz	2021-03-16	1	-1/+54
\|
*	Greatly simplify proof	Yann Herklotz	2021-03-16	1	-44/+23
\|
*	Finish proof of simple transformation	Yann Herklotz	2021-03-16	1	-0/+90
\|
*	Fix memory inferrence generation	Yann Herklotz	2021-03-15	1	-28/+32
\|
*	Prove top-level theorem with admitted theorems	Yann Herklotz	2021-03-12	1	-159/+182
\|
*	Try and fix identity proof in Memorygen	Yann Herklotz	2021-03-12	1	-1/+12
\|
*	Prove idempotency of array merge	Yann Herklotz	2021-03-11	1	-16/+78
\|
*	Update RAM generation proofs	Yann Herklotz	2021-03-09	1	-60/+450
\|
*	Add RAM semantics to HTL and fix proof	Yann Herklotz	2021-03-03	1	-8/+83
\|
*	Add implementation	Yann Herklotz	2021-03-02	1	-28/+79
\|
*	Fix memory generation by generating a power of 2	Yann Herklotz	2021-03-02	1	-34/+50
\|
*	Finish initial implementation of memory gen	Yann Herklotz	2021-03-01	1	-0/+84
\|
*	Add initial memory generation	Yann Herklotz	2021-03-01	1	-0/+17