Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Cherry-pick rules for Lib, with fixups #792

Merged
merged 15 commits into from
Jul 15, 2024
Merged

Cherry-pick rules for Lib, with fixups #792

merged 15 commits into from
Jul 15, 2024

Conversation

michaelmcinerney
Copy link
Contributor

No description provided.

@michaelmcinerney
clib: remove no_fail assumption from ccorres_While
ee31cd3 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
clib: add hoarep_isNormal_exec_handlers to Corres_UL_C
3ec612d 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
clib: add ccorres_empty_handler_stackI to Corres_UL_C
a67b8c2 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
clib: add ccorres_to_vcg_with_prop' to Corres_UL_C
cd2ee53 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
clib: strengthen intermediate_Normal_state
de5c910 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
clib: add hoarep_conj_lift
06c389f 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
clib: add ccorres_assert2_abs
b7f6167 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
lib: add more schematics to corres_symb_exec_r_conj_ex_abs
da3ebe5 
This helps to reduce dependence between the schematics used in
the assumptions, and allows for easier wp reasoning.

Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
monads/nondet: add gets_the_Some_get
5c2cb63 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
monads/reader_option: add ask_wp
f727f5b 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
monads/reader_option: add no_ofail_ask
5d301b2 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
monads/reader_option: add ostate_assert
98d8daf 
This adds ostate_assert and ohaskell_state_assert, which are
versions of state_assert/stateAssert for the reader monad.
Also adds several rules for basic reasoning about these
functions.

Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
lib+proof: move corres_add_noop_rhs and corres_add_noop_rhs2 to Lib
23a30df 
Moved from DRefine and CRefine, respectively

Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
lib: adjust corres_symb_exec_r_conj_ex_abs_forwards
f3375ad 
This was required after a recent update to the schematics of
corres_symb_exec_r_conj_ex_abs

Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
rt crefine: fixup after removing assumption from ccorres_While
19cde8e 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney michaelmcinerney added the MCS related to `rt` branch and mixed-criticality systems label Jul 15, 2024
@michaelmcinerney michaelmcinerney self-assigned this Jul 15, 2024
lsf37
lsf37 approved these changes Jul 15, 2024
View reviewed changes
Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me. Cherry-picking the corres_symb_exec_r_conj_ex_abs back to master would be good, just so that things are more in sync.

@lsf37
Copy link
Member

lsf37 commented Jul 15, 2024

Am I correct in assuming that everything apart from the last two commits (currently f3375ad and 19cde8e) is cherry-picked from the master branch?

@michaelmcinerney
Copy link
Contributor Author

Am I correct in assuming that everything apart from the last two commits (currently f3375ad and 19cde8e) is cherry-picked from the master branch?

Yes, that's right

@michaelmcinerney michaelmcinerney merged commit b2733e7 into rt Jul 15, 2024
10 of 11 checks passed
@michaelmcinerney michaelmcinerney deleted the michaelm-rules_for_lib_on_rt_july_2024 branch July 15, 2024 07:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lsf37 lsf37 lsf37 approved these changes

@Xaphiosis Xaphiosis Awaiting requested review from Xaphiosis

@corlewis corlewis Awaiting requested review from corlewis

Assignees

@michaelmcinerney michaelmcinerney

Labels
MCS related to `rt` branch and mixed-criticality systems
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@michaelmcinerney @lsf37