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

Mr Solver support for monadic Cryptol specs #1609

Merged
merged 16 commits into from
Mar 11, 2022
Merged

Mr Solver support for monadic Cryptol specs #1609

merged 16 commits into from
Mar 11, 2022

Commits on Mar 9, 2022

  1. added the cryptol_add_prim_type SAW command to set the translation of… 

    … Cryptol abstract types
    Eddy Westbrook committed Mar 9, 2022
    Configuration menu
    Copy the full SHA
    63bc072 View commit details
    Browse the repository at this point in the history

  2. whoops, marked cryptol_add_prim_type as experimental

    Eddy Westbrook committed Mar 9, 2022
    Configuration menu
    Copy the full SHA
    c0b9ed3 View commit details
    Browse the repository at this point in the history

Commits on Mar 10, 2022

  1. added cryptol_add_prim; also fixed a bug in translating abstract type… 

    …s, where the translation of the types were not getting applied
    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    7952a1d View commit details
    Browse the repository at this point in the history

  2. added a macro for monadifying the either eliminator

    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    eb4ed6a View commit details
    Browse the repository at this point in the history

  3. changed cryptol monadification to translate any global of semi-pure t… 

    …ype to itself
    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    747d31f View commit details
    Browse the repository at this point in the history

  4. added a case to computation normalization in Mr Solver to handle beta… 

    … redexes
    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    fa1110a View commit details
    Browse the repository at this point in the history

  5. changed mrApplyAll to use the new scApplyAllBeta combinator rather th… 

    …an beta normalizing the entire output term
    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    a25cefc View commit details
    Browse the repository at this point in the history

  6. trying to prove is_elem refines a cryptol spec for its behavior

    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    235dcf4 View commit details
    Browse the repository at this point in the history

  7. reimplemented assertFiniteM to use the maybe eliminator

    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    8ec0be1 View commit details
    Browse the repository at this point in the history

  8. added support to Mr Solver for maybe eliminators over isFinite proofs

    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    09681ad View commit details
    Browse the repository at this point in the history

  9. added support for CompM types during normalization with normSMTProp

    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    6cacfc5 View commit details
    Browse the repository at this point in the history

  10. changed the handling for normalizing multiFixM so that the function b… 

    …eing called is not unfolded during normalization; also added a special case for normalizing multiArgFixM
    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    5daa95a View commit details
    Browse the repository at this point in the history

  11. renamed normSMTProp to mrNormTerm, and added a mrNormOpenTerm functio… 

    …n that can normalize open terms
    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    54be292 View commit details
    Browse the repository at this point in the history

  12. updated the linked_list_mr_solver.saw test case to prove that is_elem… 

    … refines a cryptol version of its specification
    Eddy Westbrook committed Mar 10, 2022
    Configuration menu
    Copy the full SHA
    648c5ba View commit details
    Browse the repository at this point in the history

Commits on Mar 11, 2022

  1. whoops, fixed some typos

    Eddy Westbrook committed Mar 11, 2022
    Configuration menu
    Copy the full SHA
    3007ec9 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into cryptol-abstract-types

    Eddy Westbrook committed Mar 11, 2022
    Configuration menu
    Copy the full SHA
    e1c225a View commit details
    Browse the repository at this point in the history