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

Enlarge the prefix_refinement rule set #738

Merged
merged 6 commits into from
Mar 27, 2024
Merged

Enlarge the prefix_refinement rule set #738

merged 6 commits into from
Mar 27, 2024

Commits on Mar 26, 2024

  1. lib/monads/trace: prove more rules in Trace_Monad_Equations 

    These rules are based on equivalent versions from
Nondet_Monad_Equations. They were previously left out due to their
proofs using the monad_eq tactic, which does not yet exist for the
trace monad.

Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    be4c49f View commit details
    Browse the repository at this point in the history

  2. lib/concurrency: improve style 

    Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    f3c7218 View commit details
    Browse the repository at this point in the history

  3. lib/monads/trace: add a comment for the parallel command 

    This describes an implicit condition that programs need to satisfy to be
sensibly combined by parallel.

Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    9fdbf73 View commit details
    Browse the repository at this point in the history

  4. lib/concurrency: reorder prefix_refinement arguments 

    The preconditions are generally more interesting and complicated than
the relies, so they now come afterwards.

Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    186eef5 View commit details
    Browse the repository at this point in the history

  5. lib/concurrency: enlarge prefix_refinement rule set 

    Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 26, 2024
    Configuration menu
    Copy the full SHA
    7a0377a View commit details
    Browse the repository at this point in the history

Commits on Mar 27, 2024

  1. lib/concurrency: update for changed prefix_refinement rules 

    Signed-off-by: Corey Lewis <[email protected]>
    @corlewis
    corlewis committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    dfef55f View commit details
    Browse the repository at this point in the history