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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Add predicate semantics to abstractdev/io	Yann Herklotz	2021-05-26	1	-69/+296
\|
*	Finish top-level of proof	Yann Herklotz	2021-05-21	1	-9/+1
\|
*	Finish up step_cf_instr_correct again	Yann Herklotz	2021-05-16	1	-0/+18
\|
*	Fix the top-level proofs with new state_match	Yann Herklotz	2021-05-15	1	-8/+101
\|
*	Finish abstract interpretation	Yann Herklotz	2021-05-12	1	-75/+199
\|
*	Fix admitted in first proof of sem. preservation	Yann Herklotz	2021-05-10	1	-19/+68
\|
*	Finish correctness of semantics wrt. RTBlock	Yann Herklotz	2021-05-06	1	-84/+327
\|
*	Add admitted proof of translations in RTLPargen	Yann Herklotz	2021-05-03	1	-27/+177
\|
*	Fix RTLPar to use instr list list list	Yann Herklotz	2021-02-16	1	-7/+1
\|
*	Add temporary fixes to get everything to compiledev/predicated-execution	Yann Herklotz	2021-02-12	1	-1/+9
\|
*	Add Vrange and predicates	Yann Herklotz	2021-02-02	1	-4/+5
\|
*	Fix proofs with better defined equality	Yann Herklotz	2021-01-30	1	-11/+6
\|
*	Fix definitions of proofs some more	Yann Herklotz	2021-01-29	1	-47/+51
\|
*	Fix HTLPargen and RTLPargen	Yann Herklotz	2021-01-29	1	-51/+173
\|
*	Add more proofs for RTLPargen correctness	Yann Herklotz	2021-01-27	1	-6/+22
\|
*	Remove the schedule oracle	Yann Herklotz	2021-01-26	1	-3/+515
\|
*	Share code between RTLBlock and Par	Yann Herklotz	2021-01-21	1	-44/+7
\|
*	Correct translation of scheduling with oracle check	Yann Herklotz	2021-01-13	1	-4/+53
\|
*	Add RTLPargen.v	Yann Herklotz	2021-01-13	1	-0/+27