Prove decodeSchedControl_configureFlags_ccorres and decodeInvocation_ccorres#902
Prove decodeSchedControl_configureFlags_ccorres and decodeInvocation_ccorres#902
decodeSchedControl_configureFlags_ccorres and decodeInvocation_ccorres#902Conversation
michaelmcinerney
added
the
MCS
Xaphiosis
left a comment
Xaphiosis
left a comment
There was a problem hiding this comment.
Good progress. Minor comments on content.
Have an issue with the commit "rt spec+crefine: prove decodeSchedControl_ConfigureFlags_ccorres": it's doing too much. Doing a multi-arch restructure like that and making something arch-specific should be in its own commit. This will be particularly important when dealing with arch-split in future.
The decode_sched_control_configure_flags update can indeed go in with the proof commit.
lsf37
left a comment
lsf37
left a comment
There was a problem hiding this comment.
Nice. Only some arch split and lemma moving comments, content is good.
michaelmcinerney
force-pushed
the
michaelm-decodeSchedControl
branch
from
6493044 to
1eec353
Compare
|
I've updated the PR, hopefully addressing all the comments. There's a new commit for |
lsf37
left a comment
lsf37
left a comment
There was a problem hiding this comment.
Good from my side, only request is to put the word_bits lemma higher up in the theory tree.
michaelmcinerney
force-pushed
the
michaelm-decodeSchedControl
branch
from
eb9d9ee to
85bc1fd
Compare
This corrects the value of TIME_ARG_SIZE/timeArgSize for RISCV, and furthermore gives an architecture independent definition of this constant. Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
force-pushed
the
michaelm-decodeSchedControl
branch
from
85bc1fd to
cbf743c
Compare
|
Force pushed after rebasing over |
Signed-off-by: Michael McInerney <[email protected]>
The definition of decode_sched_control_configure_flags is updated to align with the C. Signed-off-by: Michael McInerney <[email protected]>
Signed-off-by: Michael McInerney <[email protected]>
michaelmcinerney
force-pushed
the
michaelm-decodeSchedControl
branch
from
cbf743c to
5be5ba3
Compare
3 participants
Test with seL4/seL4#1472