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

	Commit message (Expand)	Author	Age	Files	Lines
*	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
\|\
\| *	Fix addressing bug.	James Pollard	2020-06-12	1	-4/+6
* \|	Merge branch 'master' into arrays-proof	James Pollard	2020-06-12	14	-1028/+364
\|\\|
\| *	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
* \|	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
\|/
*	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
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-03	3	-47/+50
\|\\|
\| *	Uncomment proof	Yann Herklotz	2020-06-03	3	-43/+46
* \|	HTLgenspec status in line with develop	James Pollard	2020-06-03	3	-26/+57
* \|	Copy over load/store from Veriloggen to HTLgen.	James Pollard	2020-06-03	1	-5/+36
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-03	3	-6/+32
\|\\|
\| *	Add proof to final_states	Yann Herklotz	2020-06-02	2	-3/+5
\| *	Add proof for initial state	Yann Herklotz	2020-06-02	2	-3/+27
* \|	Keep track of declarations in HTLgen.	James Pollard	2020-06-03	1	-23/+62
* \|	Update HTL semantics to support arrays.	James Pollard	2020-06-02	2	-19/+32
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-02	4	-84/+185
\|\\|
\| *	Get whole proof to compile	Yann Herklotz	2020-06-02	1	-14/+17
\| *	Shorten the proof a bit	Yann Herklotz	2020-06-02	1	-41/+15
\| *	Add proof for equivalence of mov	Yann Herklotz	2020-06-02	3	-40/+143
\| *	Add lemmas for preservation of globals	Yann Herklotz	2020-06-01	2	-29/+50
* \|	Paramterise associations type to avoid some duplication.	James Pollard	2020-06-02	1	-44/+40
* \|	First draft of array semantics.	James Pollard	2020-06-01	1	-112/+188
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-01	2	-13/+19
\|\\|
\| *	Copy over RTL global state	Yann Herklotz	2020-06-01	1	-8/+15
\| *	Small optimisations to proof	Yann Herklotz	2020-05-31	1	-5/+4
* \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-05-30	17	-348/+2195
\|\\|
\| *	Merge branch 'develop' of github.com:ymherklotz/CoqUp into develop	Yann Herklotz	2020-05-29	1	-6/+3
\| \|\
\| \| *	Improve automation in HTLgenspec.	James Pollard	2020-05-29	1	-6/+3
\| * \|	Fix compilation moving to PTree	Yann Herklotz	2020-05-29	6	-36/+48
\| \|/
\| *	Fix indentation	Yann Herklotz	2020-05-29	1	-6/+6
\| *	New and improved Assocmap	Yann Herklotz	2020-05-29	1	-7/+32