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

	Commit message (Expand)	Author	Age	Files	Lines
...
\| * \| \| \| \| \| \| \| \|	Fix stack frame issue.	James Pollard	2020-06-30	1	-46/+25
* \| \| \| \| \| \| \| \| \|	Add HTL pretty printer	Yann Herklotz	2020-06-30	1	-0/+81
* \| \| \| \| \| \| \| \| \|	Add htl pretty printing	Yann Herklotz	2020-06-30	8	-12/+23
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Add command line flags for initial block	Yann Herklotz	2020-06-30	4	-7/+22
* \| \| \| \| \| \| \| \|	Merge branch 'develop' of github.com:ymherklotz/CoqUp into develop	Yann Herklotz	2020-06-30	2	-36/+210
\|\ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \|	Merge pull request #8 from p0llard/develop	Yann Herklotz	2020-06-30	2	-36/+210
\| \|\\| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-29	4	-8/+31
\| \| \|\ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \|	Eliminate memory bounds assumption!	James Pollard	2020-06-29	2	-37/+211
* \| \| \| \| \| \| \| \| \| \|	Make the proofs more concise	Yann Herklotz	2020-06-30	1	-17/+21
\|/ / / / / / / / / /
* \| / / / / / / / /	Add equivalence between int add value add	Yann Herklotz	2020-06-30	1	-10/+54
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Develop compiles again	Yann Herklotz	2020-06-29	4	-8/+11
* \| \| \| \| \| \| \| \|	Merge remote-tracking branch 'james/arrays-proof' into develop	Yann Herklotz	2020-06-29	1	-0/+34
\|\\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Add missing file.	James Pollard	2020-06-29	1	-0/+34
\| \| \|_\|_\|_\|_\|_\|/ \| \|/\| \| \| \| \| \|
* / \| \| \| \| \| \|	Work on addition proof	Yann Herklotz	2020-06-29	1	-1/+21
\|/ / / / / / /
* \| \| \| \| \| \|	Fix proof again with Verilog semantics changes	Yann Herklotz	2020-06-28	2	-1/+23
* \| \| \| \| \| \|	Merge remote-tracking branch 'james/arrays-proof' into develop	Yann Herklotz	2020-06-28	5	-101/+961
\|\ \ \ \ \ \ \
\| * \| \| \| \| \| \|	Finish store proof modulo:	James Pollard	2020-06-28	1	-1/+206
\| * \| \| \| \| \| \|	Fix second IStore proof.	James Pollard	2020-06-28	1	-29/+50
\| * \| \| \| \| \| \|	Finish first IStore proof (modulo some admissions).	James Pollard	2020-06-28	2	-69/+305
\| * \| \| \| \| \| \|	Fix unsigned/signed issues.	James Pollard	2020-06-28	4	-97/+92
\| * \| \| \| \| \| \|	Work on proof.	James Pollard	2020-06-28	4	-2/+405
* \| \| \| \| \| \| \|	Add yosys to dependencies	Yann Herklotz	2020-06-28	2	-2/+2
* \| \| \| \| \| \| \|	Fix Verilog semantics and fix order of always blocks	Yann Herklotz	2020-06-26	3	-8/+5
* \| \| \| \| \| \| \|	Progress on proof of Veriloggen	Yann Herklotz	2020-06-25	3	-15/+24
* \| \| \| \| \| \| \|	Work on Veriloggen proof	Yann Herklotz	2020-06-25	3	-6/+55
* \| \| \| \| \| \| \|	Finish Internal main proof	Yann Herklotz	2020-06-24	1	-14/+29
\|/ / / / / / /
* \| \| \| \| \| \|	HTLgenproof passing.arrays-proof	James Pollard	2020-06-24	2	-50/+127
* \| \| \| \| \| \|	Merge branch 'develop' into arrays-proof	James Pollard	2020-06-24	2	-9/+5
\|\ \ \ \ \ \ \
\| * \| \| \| \| \| \|	Fixes to make develop compile	Yann Herklotz	2020-06-24	4	-8/+6
* \| \| \| \| \| \| \|	Merge branch 'develop' of github.com:ymherklotz/coqup into arrays-proof	James Pollard	2020-06-24	80	-115/+15708
\|\\| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	Merge branch 'master' into develop	Yann Herklotz	2020-06-24	3	-81/+96
\| \|\ \ \ \ \ \ \
\| \| * \| \| \| \| \| \|	Fix assumption of main	Yann Herklotz	2020-06-24	3	-83/+97
\| \| \| \|_\|_\|_\|_\|/ \| \| \|/\| \| \| \| \|
\| * \| \| \| \| \| \|	More to proof	Yann Herklotz	2020-06-23	1	-7/+9
\| * \| \| \| \| \| \|	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
\| \|\ \ \ \ \ \
\| * \ \ \ \ \ \	Merge branch 'master' into develop	Yann Herklotz	2020-06-22	76	-20/+15522
\| \|\ \ \ \ \ \ \ \| \| \| \|/ / / / / \| \| \|/\| \| \| \| \|
\| \| * \| \| \| \| \|	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	3	-7/+23
\| \| * \| \| \| \| \|	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 CHstone	Yann Herklotz	2020-06-19	72	-1/+15485
\| \| * \| \| \|	Merge branch 'develop'	Yann Herklotz	2020-06-14	5	-24/+32
\| \| \|\ \ \ \ \| \| \| \|_\|_\|/ \| \| \|/\| \| \|
\| * \| \| \| \|	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
\| \|\ \ \ \ \ \| \| \|_\|/ / / \| \|/\| \| \| \|
\| * \| \| \| \|	Fix coqproject	Yann Herklotz	2020-06-14	1	-1/+1
\| * \| \| \| \|	Add more unproven instructions, Admitted equiv to spec	Yann Herklotz	2020-06-14	4	-23/+31
\| \| \|/ / / \| \|/\| \| \|
* \| \| \| \|	Finish ILoad proof with some assumptions:	James Pollard	2020-06-24	3	-192/+197
* \| \| \| \|	Normalise entire expression to avoid overflow issues.	James Pollard	2020-06-23	5	-272/+523