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

Some rules for Lib and CLib #785

Merged
merged 13 commits into from
Jul 11, 2024
Merged

Some rules for Lib and CLib #785

merged 13 commits into from
Jul 11, 2024

Commits on Jul 11, 2024

  1. clib: remove no_fail assumption from ccorres_While 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    f9ba601 View commit details
    Browse the repository at this point in the history

  2. clib: add hoarep_isNormal_exec_handlers to Corres_UL_C 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    58646c2 View commit details
    Browse the repository at this point in the history

  3. clib: add ccorres_empty_handler_stackI to Corres_UL_C 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    9241ec4 View commit details
    Browse the repository at this point in the history

  4. clib: add ccorres_to_vcg_with_prop' to Corres_UL_C 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    5d86998 View commit details
    Browse the repository at this point in the history

  5. clib: strengthen intermediate_Normal_state 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    3628a3e View commit details
    Browse the repository at this point in the history

  6. clib: add hoarep_conj_lift 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    a7f3ced View commit details
    Browse the repository at this point in the history

  7. clib: add ccorres_assert2_abs 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    81898d0 View commit details
    Browse the repository at this point in the history

  8. lib: add more schematics to corres_symb_exec_r_conj_ex_abs 

    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
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    23baa74 View commit details
    Browse the repository at this point in the history

  9. monads/nondet: add gets_the_Some_get 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    412de2b View commit details
    Browse the repository at this point in the history

  10. monads/reader_option: add ask_wp 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    194e3ec View commit details
    Browse the repository at this point in the history

  11. monads/reader_option: add no_ofail_ask 

    Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    af9c160 View commit details
    Browse the repository at this point in the history

  12. monads/reader_option: add ostate_assert 

    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
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    2c20961 View commit details
    Browse the repository at this point in the history

  13. lib+proof: move corres_add_noop_rhs and corres_add_noop_rhs2 to Lib 

    Moved from DRefine and CRefine, respectively

Signed-off-by: Michael McInerney <[email protected]>
    @michaelmcinerney
    michaelmcinerney committed Jul 11, 2024
    Configuration menu
    Copy the full SHA
    96799b8 View commit details
    Browse the repository at this point in the history