vericert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Use main instead of top for synthesising Vericert designsoopsla21	Yann Herklotz	2021-07-24	1	-1/+1
\|
*	Update instructions and fix testv1.2.1	Yann Herklotz	2021-07-12	4	-6/+5
\|
*	Remove comments in docker file	Yann Herklotz	2021-07-12	1	-3/+3
\|
*	Update the artifact description	Yann Herklotz	2021-07-12	7	-4/+204
\|
*	Remove more OCaml files to compile successfully without admits.	Yann Herklotz	2021-07-11	5	-1085/+0
\|
*	Remove unnecessary files and proofs	Yann Herklotz	2021-07-11	7	-16/+19
\|
*	Update the run-legup.sh file	Yann Herklotz	2021-07-11	1	-0/+4
\|
*	Add legup script	Yann Herklotz	2021-07-11	4	-4/+74
\|
*	Fix the small test bench for Vericert	Yann Herklotz	2021-07-11	7	-137/+67
\|
*	Fix some more of the benchmarks	Yann Herklotz	2021-07-11	8	-49/+35
\|
*	Add divider benchmarks	Yann Herklotz	2021-07-11	44	-0/+3581
\|
*	Fix makefiles and add a parent makefile	Yann Herklotz	2021-07-10	4	-3/+18
\|
*	Fix Makefiles slightly	Yann Herklotz	2021-07-10	8	-7/+12
\|
*	Add more documentation and clean up benchmarks	Yann Herklotz	2021-07-10	12	-158/+139
\|
*	Add docker file and some comments	Yann Herklotz	2021-07-09	2	-0/+6
\|
*	Clean up Memorygen file	Yann Herklotz	2021-04-07	1	-219/+1
\|
*	Remove Admitted in the highest of top-levelsv1.2.0	Yann Herklotz	2021-04-07	1	-5/+10
\|
*	No admitted theorems in Memorygen proof (~‾▿‾)~	Yann Herklotz	2021-04-07	1	-76/+99
\|
*	Basically done with proof	Yann Herklotz	2021-04-07	6	-18/+62
\|
*	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	7	-289/+317
\|
*	Finish Veriloggenproof completely	Yann Herklotz	2021-04-04	4	-57/+339
\|
*	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	2	-189/+533
\|
*	Add logo to readme	Yann Herklotz	2021-04-02	1	-6/+3
\|
*	Fix initialisation more	Yann Herklotz	2021-04-01	1	-7/+7
\|
*	Add 0 initialisation	Yann Herklotz	2021-04-01	1	-1/+1
\|
*	Add declarations	Yann Herklotz	2021-04-01	1	-6/+7
\|
*	Add new enable interface	Yann Herklotz	2021-04-01	4	-53/+66
\|
*	Add memory disable	Yann Herklotz	2021-03-31	4	-163/+306
\|
*	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	2	-29/+250
\|
*	Add check for ram in module	Yann Herklotz	2021-03-20	1	-16/+161
\|
*	Prove very top-level theorem	Yann Herklotz	2021-03-19	2	-83/+176
\|
*	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
\|