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

	Commit message (Expand)	Author	Age	Files	Lines
*	Merge branch 'master' into develop	Yann Herklotz	2020-06-22	3	-9/+58
\|\
\| *	Admit everything temporarily	Yann Herklotz	2020-06-22	3	-9/+58
* \|	Admit the value proof	Yann Herklotz	2020-06-22	1	-3/+5
* \|	Merge branch 'arrays-proof' into develop	Yann Herklotz	2020-06-22	3	-31/+204
\|\ \
\| * \|	Factor out addressing checks, check signed range.	James Pollard	2020-06-21	1	-10/+17
\| * \|	Lea op now checks alignment.	James Pollard	2020-06-21	1	-12/+15
\| * \|	Finish structure of Aindexed2scaled ILoad proof.	James Pollard	2020-06-20	2	-14/+177
* \| \|	Merge branch 'master' into develop	Yann Herklotz	2020-06-22	3	-18/+33
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Only print out main as everything is inlined	Yann Herklotz	2020-06-22	1	-8/+10
\| * \|	Add print for debug always block in module	Yann Herklotz	2020-06-22	2	-6/+19
\| * \|	Some fixes, but still buggy probably	Yann Herklotz	2020-06-20	1	-2/+2
\| * \|	Add bugs to support more operations	Yann Herklotz	2020-06-20	1	-4/+4
* \| \|	Add proof of nat equiv	Yann Herklotz	2020-06-20	1	-2/+15
* \| \|	Merge remote-tracking branch 'james/arrays-proof' into develop	Yann Herklotz	2020-06-20	9	-111/+725
\|\ \ \ \| \|/ / \|/\| / \| \|/
\| *	Working on proof.	James Pollard	2020-06-19	1	-10/+86
\| *	Enforce stack size alignment to fix proof.	James Pollard	2020-06-18	3	-10/+22
\| *	Tidy up proof.	James Pollard	2020-06-18	2	-13/+16
\| *	Finish AInStack proof with minor assertions.	James Pollard	2020-06-18	1	-32/+21
\| *	Fix up ILoad proof.	James Pollard	2020-06-18	1	-95/+58
\| *	Fix array semantics behaviour for undefined values.	James Pollard	2020-06-18	1	-1/+1
\| *	Fix Inop proof to work with new array semantics.	James Pollard	2020-06-17	2	-7/+44
\| *	Some (very) useful lemmas about arrays.	James Pollard	2020-06-17	3	-7/+139
\| *	Use NBAs for loads and stores.	James Pollard	2020-06-17	2	-4/+4
\| *	Fix array semantics merge granularity.	James Pollard	2020-06-17	4	-30/+87
\| *	Array semantics now uses dependent Array type.	James Pollard	2020-06-14	4	-48/+49
\| *	Move some standard tactics to Coquplib.	James Pollard	2020-06-14	1	-0/+10
\| *	Add a basic length-indexed list type.	James Pollard	2020-06-13	1	-0/+123
\| *	Fix broken proof.	James Pollard	2020-06-12	1	-4/+4
\| *	Merge branch 'master' into arrays-proof	James Pollard	2020-06-12	1	-4/+6
\| \|\
\| * \	Merge branch 'master' into arrays-proof	James Pollard	2020-06-12	14	-1028/+364
\| \|\ \
\| * \| \|	Some work on store proof.	James Pollard	2020-06-12	1	-11/+38
\| * \| \|	Rough outline of stack address proof	James Pollard	2020-06-11	3	-34/+109
\| * \| \|	Working on proof.	James Pollard	2020-06-11	5	-47/+156
* \| \| \|	Add more unproven instructions, Admitted equiv to spec	Yann Herklotz	2020-06-14	4	-23/+31
\| \|_\|/ \|/\| \|
* \| \|	Fix addressing bug.	James Pollard	2020-06-12	1	-4/+6
\| \|/ \|/\|
* \|	Add declaration of loads	Yann Herklotz	2020-06-12	2	-4/+6
* \|	Fix declaring function arguments correctly	Yann Herklotz	2020-06-12	3	-12/+69
* \|	Fix printing of Verilog with new datatypes	Yann Herklotz	2020-06-12	2	-17/+27
* \|	Remove Verilog proofs	Yann Herklotz	2020-06-12	3	-133/+10
* \|	Declare all registers properly in HTL	Yann Herklotz	2020-06-12	3	-51/+95
* \|	Remove extraction of simulator	Yann Herklotz	2020-06-12	1	-2/+2
* \|	Fix top level invocation to translate through HTL	Yann Herklotz	2020-06-12	2	-4/+8
* \|	Remove Test.v	Yann Herklotz	2020-06-12	1	-99/+0
* \|	Generate Verilog from HTL	Yann Herklotz	2020-06-12	2	-713/+154
\|/
*	Start fixing proof	James Pollard	2020-06-09	1	-94/+116
*	Fix automation tactic for modified constructor	James Pollard	2020-06-09	1	-2/+4
*	Start extending HTL proof to cover arrays.	James Pollard	2020-06-09	1	-18/+31
*	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-09	4	-56/+156
\|\
\| *	Finished main proof with small assumptions	Yann Herklotz	2020-06-04	5	-59/+157
* \|	Fix HTLgenspec proof for arrays.	James Pollard	2020-06-03	1	-31/+43