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

Updating prover #260

Merged
merged 15 commits into from
Nov 21, 2023
Merged

Updating prover #260

merged 15 commits into from
Nov 21, 2023

Commits on Nov 19, 2023

  1. Added #halt rule to signify end of execution.

    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    d0d90aa View commit details
    Browse the repository at this point in the history

  2. [BROKEN] Added KMIRSemantics with explicit terminal rules. 

    Error occurs from `pyk` internal call to `is_terminal`
    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    07d64c2 View commit details
    Browse the repository at this point in the history

  3. Added booster as backend target

    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    8ec8d4c View commit details
    Browse the repository at this point in the history

  4. Added runLemma doneLemma paradigm

    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    e61684c View commit details
    Browse the repository at this point in the history

  5. added simplify init

    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    39bcbbe View commit details
    Browse the repository at this point in the history

  6. failing proof working again

    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    edaa357 View commit details
    Browse the repository at this point in the history

  7. Fixed proof failure information

    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    24755af View commit details
    Browse the repository at this point in the history

  8. Moved halt rules so that SYMBOLIC module could see them

    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    2d4f13d View commit details
    Browse the repository at this point in the history

  9. Added empty start-finish MIR program for verification

    @dkcumming
    dkcumming committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    cd948ee View commit details
    Browse the repository at this point in the history

Commits on Nov 20, 2023

  1. Moved #halt back to MIR and MIR-SYMBOLIC now imports MIR

    @dkcumming
    dkcumming committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    b8977d9 View commit details
    Browse the repository at this point in the history

  2. Corrected empty-program.k and added Rust and Mir for it

    @dkcumming
    dkcumming committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    1cb379d View commit details
    Browse the repository at this point in the history

  3. Added naming to proofs in simple-spec.k

    @dkcumming
    dkcumming committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    8cd3f2e View commit details
    Browse the repository at this point in the history

  4. added empty-program.k to CI

    @dkcumming
    dkcumming committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    236a2c2 View commit details
    Browse the repository at this point in the history

  5. removed duplicate rule in MIR module

    @dkcumming
    dkcumming committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    47014fe View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2023

  1. removing commented out imports

    @dkcumming
    dkcumming committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    95562f6 View commit details
    Browse the repository at this point in the history