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

	Commit message (Expand)	Author	Age	Files	Lines
...
* \| \| \|	Merge branch 'mppa-RTLpathSE-verif' into mppa-RTLpathSE-verif-hash-junk	Sylvain Boulmé	2020-07-22	2	-224/+528
\|\\| \| \|
\| * \| \|	Progress	Cyril SIX	2020-07-21	2	-72/+109
\| * \| \|	hsistate_simu_core_correct	Cyril SIX	2020-07-21	2	-170/+183
\| * \| \|	Progress	Cyril SIX	2020-07-16	2	-55/+207
\| * \| \|	fix hsilocal_simu_core_correct	Sylvain Boulmé	2020-07-11	1	-0/+38
\| * \| \|	Lemmas on hsilocal_simu ---> relies on reflexivity of istate_simu (which isn'...	Cyril SIX	2020-07-10	1	-7/+64
\| * \| \|	fix comment	Sylvain Boulmé	2020-07-10	1	-1/+1
\| * \| \|	remove junk comment	Sylvain Boulmé	2020-07-10	1	-10/+0
\| * \| \|	try to fix refinement definition on exits	Sylvain Boulmé	2020-07-10	2	-33/+78
* \| \| \|	start a junk implementation of the pre-pass verifier	Sylvain Boulmé	2020-07-22	2	-1/+590
* \| \| \|	seval_condition_refines ---> refinement correct only for successful executions ?	Cyril SIX	2020-07-09	1	-19/+47
\|/ / /
* \| \|	Merge branch 'mppa-RTLpathSE-verif-test-sfval_simu' into mppa-RTLpathSE-verif	Sylvain Boulmé	2020-07-09	4	-796/+1058
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	adapting Cyril's proofs in RTLpathSE_impl for the new definitions of simu.	Sylvain Boulmé	2020-07-08	3	-657/+525
\| * \|	weaker sfval_simu	Sylvain Boulmé	2020-07-08	3	-134/+183
\| * \|	Characterizing Op dependency on memory	Sylvain Boulmé	2020-07-08	1	-0/+39
\| * \|	Avancement	Cyril SIX	2020-07-07	2	-88/+290
\| * \|	ssem_final with less dependencies	Cyril SIX	2020-07-06	1	-11/+14
\| * \|	init_hsistate_correct	Cyril SIX	2020-07-06	1	-5/+29
\| * \|	Version without dependency on rs0, m0, ge and sp ?	Cyril SIX	2020-07-03	1	-44/+60
* \| \|	hsexec_correct proved (under admitted lemmas).	Sylvain Boulmé	2020-07-03	1	-68/+48
\|/ /
* \|	Scope issue..	Cyril SIX	2020-07-03	1	-11/+12
* \|	Fixing ge, sp, rs, m issue	Cyril SIX	2020-07-03	1	-8/+9
* \|	fix the proof sketch	Sylvain Boulmé	2020-07-03	1	-30/+22
* \|	sketch the proof of symbolic execution of one instruction	Sylvain Boulmé	2020-07-03	2	-35/+68
* \|	slightly simpler code	Sylvain Boulmé	2020-07-02	1	-64/+88
* \|	Optimization of Iop symbolic execution	Sylvain Boulmé	2020-07-02	2	-35/+107
* \|	Fix hypothesis on environment in hsstate_simu	Sylvain Boulmé	2020-07-02	1	-3/+4
* \|	remove useless (and unprovable) lemmas on completeness of the refinement	Sylvain Boulmé	2020-07-02	1	-47/+66
* \|	Avancement, mais est-ce prouvable ?	Cyril SIX	2020-07-01	1	-0/+37
* \|	hsexec_complete	Cyril SIX	2020-07-01	1	-37/+36
* \|	Avancement	Cyril SIX	2020-07-01	2	-74/+120
* \|	hsexec_correct	Cyril SIX	2020-07-01	2	-27/+138
* \|	Some renaming	Cyril SIX	2020-07-01	1	-38/+49
* \|	a minor comment	Sylvain Boulmé	2020-06-30	1	-2/+2
* \|	starting refinement of (abstract) symbolic executions	Sylvain Boulmé	2020-06-30	1	-0/+160
* \|	Must generalize silocal_simub with a list of regs	Cyril SIX	2020-06-29	1	-3/+5
* \|	Only silocal_simub left	Cyril SIX	2020-06-29	1	-132/+171
* \|	sfval_simub_correct	Cyril SIX	2020-06-29	1	-6/+175
* \|	Going further in sfval_simub	Cyril SIX	2020-06-29	1	-6/+60
* \|	sval_simub + sval_simub_correct	Cyril SIX	2020-06-29	1	-9/+51
* \|	Start of sval_simub	Cyril SIX	2020-06-25	1	-3/+93
* \|	Proving small lemmas	Cyril SIX	2020-06-25	1	-6/+33
* \|	Proof of sistate_simub_correct with smaller admitted lemmas	Cyril SIX	2020-06-24	1	-55/+45
* \|	Some progress	Cyril SIX	2020-06-24	1	-2/+52
* \|	Fixing sistate_simub_correct ; no need for injection	Cyril SIX	2020-06-23	3	-29/+20
* \|	Reverting injectivity ?	Cyril SIX	2020-06-23	1	-8/+9
* \|	Modification on istate_simu to go further in the proof of sistate_simub_correct	Cyril SIX	2020-06-22	3	-10/+46
* \|	Start of sistate_simub_correct	Cyril SIX	2020-06-22	1	-5/+54
* \|	Splitting sistate_simub	Cyril SIX	2020-06-22	1	-2/+72
* \|	Proof of sexec_exact	Cyril SIX	2020-06-19	1	-3/+3