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] Improved heterogenous interface, bug fixes for SHA512 example #1743

Merged
merged 13 commits into from
Sep 29, 2022
Merged

[MRSolver] Improved heterogenous interface, bug fixes for SHA512 example #1743

merged 13 commits into from
Sep 29, 2022

Commits on Aug 15, 2022

  1. fail more gracefully when natSize is undefined, improve panic traces

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

  2. add implementation of scSplitM, ecJoinM

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

  3. refactor mrRefinesFunH to use types directly, use mrProveEq in BVVec het

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

  4. introduce equality arguments as assumptions

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

  5. WIP on processBlocks

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

Commits on Aug 16, 2022

  1. revert lifting of uvar ctx in withUVars

    @m-yac
    m-yac committed Aug 16, 2022
    Configuration menu
    Copy the full SHA
    59dfb09 View commit details
    Browse the repository at this point in the history

  2. add MRVarCtx to avoid ambiguity about var ctx orderings

    @m-yac
    m-yac committed Aug 16, 2022
    6 Configuration menu
    Copy the full SHA
    7de0965 View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2022

  1. address comments about MRVarCtx

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

Commits on Aug 26, 2022

  1. add genCryM/atCryM and tweak Prims to get split normalizing

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

  2. fix bug in genBVVecFromVec prim

    @m-yac
    m-yac committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    1522ed5 View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2022

  1. replace matchHet with findInjConvs

    @m-yac
    m-yac committed Sep 9, 2022
    Configuration menu
    Copy the full SHA
    f496f69 View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2022

  1. fix bugs in new InjConversion interface

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

Commits on Sep 29, 2022

  1. Merge branch 'master' into mr-solver-split

    Eddy Westbrook committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    46280b1 View commit details
    Browse the repository at this point in the history