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

	Commit message (Expand)	Author	Age	Files	Lines
*	defines fsem (aka functional semantics) of BTL	Sylvain Boulmé	2021-05-20	1	-3/+3
*	finishing RTLtoBTL	Léo Gourdin	2021-05-17	1	-23/+34
*	mib lemma	Léo Gourdin	2021-05-17	1	-26/+29
*	Lemmas on ISTEP	Léo Gourdin	2021-05-17	1	-194/+126
*	some advance	Léo Gourdin	2021-05-16	1	-24/+191
*	iblock_istep rec and correct lemmas	Léo Gourdin	2021-05-13	1	-0/+83
*	ascii simu	Léo Gourdin	2021-05-12	1	-17/+48
*	finish proof	Léo Gourdin	2021-05-11	1	-39/+45
*	new lemma definition, some preparations in existing proofs	Léo Gourdin	2021-05-11	1	-52/+65
*	new strong_state predicate and lemma	Léo Gourdin	2021-05-10	1	-38/+72
*	Some more proof cases, comments and cleanup	Léo Gourdin	2021-05-10	1	-29/+96
*	is_exp and bcond proof	Léo Gourdin	2021-05-10	1	-18/+35
*	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Léo Gourdin	2021-05-09	1	-0/+2
\|\
\| *	idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" !	Sylvain Boulmé	2021-05-08	1	-0/+2
* \|	mib_exit draft	Léo Gourdin	2021-05-09	1	-3/+4
* \|	Some advance in proof and NOTRAP loads fix	Léo Gourdin	2021-05-07	1	-4/+53
* \|	intermediate lemma for opt_simu intro case	Léo Gourdin	2021-05-07	1	-10/+21
\|/
*	a draft for the Bnop case	Léo Gourdin	2021-05-07	1	-11/+25
*	proof OK for Call and Return states	Léo Gourdin	2021-05-07	1	-6/+21
*	starting RTL->BTL proof	Léo Gourdin	2021-05-06	1	-4/+46
*	fix match_states	Sylvain Boulmé	2021-05-06	1	-6/+8
*	cleaner match_states	Sylvain Boulmé	2021-05-06	1	-16/+21
*	start RTL -> BTL	Sylvain Boulmé	2021-05-06	1	-0/+239