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

[MRSolver] Changes to Mr. Solver to get zero_array working #1624

Merged
merged 20 commits into from
Mar 28, 2022
Merged

[MRSolver] Changes to Mr. Solver to get zero_array working #1624

merged 20 commits into from
Mar 28, 2022

Commits on Mar 11, 2022

  1. add exp_explosion_mr_solver.saw, add is_elem_noErrorsSpec

    @m-yac
    m-yac committed Mar 11, 2022
    Configuration menu
    Copy the full SHA
    747aa97 View commit details
    Browse the repository at this point in the history

Commits on Mar 12, 2022

  1. progress on mr_solver zero_array |= zero_array_spec

    @m-yac
    m-yac committed Mar 12, 2022
    Configuration menu
    Copy the full SHA
    1f50d52 View commit details
    Browse the repository at this point in the history

Commits on Mar 14, 2022

  1. fix mrFunOutType, fix lifting and use asApplyAll in askMRSolverH

    @m-yac
    m-yac committed Mar 14, 2022
    Configuration menu
    Copy the full SHA
    e06f2dc View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2022

  1. implement vecMapM, (ec)atM, (ec)updateM without Nat__rec

    @m-yac
    m-yac committed Mar 15, 2022
    Configuration menu
    Copy the full SHA
    5478892 View commit details
    Browse the repository at this point in the history

  2. add maybe elim for IsLe(/Lt)Nat

    @m-yac
    m-yac committed Mar 15, 2022
    Configuration menu
    Copy the full SHA
    dcbe342 View commit details
    Browse the repository at this point in the history

  3. make bvNat w (bvToNat w' n) reduce to n in the simulator

    @m-yac
    m-yac committed Mar 15, 2022
    Configuration menu
    Copy the full SHA
    2156e70 View commit details
    Browse the repository at this point in the history

Commits on Mar 19, 2022

  1. add cases for vecMapM, atM, updateM to normComp/normBind

    @m-yac
    m-yac committed Mar 19, 2022
    Configuration menu
    Copy the full SHA
    17e0926 View commit details
    Browse the repository at this point in the history

  2. remove maybe elim for IsLe(/Lt)Nat, always unfold is_bvule(t) in maybe

    @m-yac
    m-yac committed Mar 19, 2022
    Configuration menu
    Copy the full SHA
    9462c5c View commit details
    Browse the repository at this point in the history

Commits on Mar 21, 2022

  1. add macro for precondHint in Monadify.hs

    @m-yac
    m-yac committed Mar 21, 2022
    Configuration menu
    Copy the full SHA
    0b93a5e View commit details
    Browse the repository at this point in the history

Commits on Mar 23, 2022

  1. do beta reds + look past asserts in mrGetPrecond, get loop spec working

    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    b7fd7f5 View commit details
    Browse the repository at this point in the history

  2. added specification primitives for cryptol

    @m-yac
    Eddy Westbrook authored and m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    936cebf View commit details
    Browse the repository at this point in the history

  3. add precondHint to specPrims.saw, lookup macros in set_monadification

    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    fdb4974 View commit details
    Browse the repository at this point in the history

  4. rename precondHint to invariantHint

    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    bce1ea6 View commit details
    Browse the repository at this point in the history

  5. add assertingM, assumingM, and their monadification macros

    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    82fed00 View commit details
    Browse the repository at this point in the history

  6. add assertingM, assumingM to Mr. Solver

    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    4d08030 View commit details
    Browse the repository at this point in the history

  7. add bvVecMapInvarM, get zero_array_spec refinement working

    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    5212c58 View commit details
    Browse the repository at this point in the history

  8. update Prelude.v, clean up comments

    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    45d91a8 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' of https://github.com/GaloisInc/saw-script into… 

    … mr-solver/heterogeneous
    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    75b97ab View commit details
    Browse the repository at this point in the history

  10. whoops remove SAWCorePrelude.v

    @m-yac
    m-yac committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    e2f41cb View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2022

  1. attempt to fix CI build failure on GHC 8.8.4

    @m-yac
    m-yac committed Mar 24, 2022
    Configuration menu
    Copy the full SHA
    7a0b46c View commit details
    Browse the repository at this point in the history