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

[Heapster] Don't use Coq let-bindings in Heapster specs #1545

Merged
merged 10 commits into from
Dec 23, 2021
Merged

[Heapster] Don't use Coq let-bindings in Heapster specs #1545

merged 10 commits into from
Dec 23, 2021

Commits on Dec 15, 2021

  1. use sawLet for translating TypedSetReg

    @m-yac
    m-yac committed Dec 15, 2021
    Configuration menu
    Copy the full SHA
    38a7d32 View commit details
    Browse the repository at this point in the history

  2. get sawLet working, add exp_explosion example

    @m-yac
    m-yac committed Dec 15, 2021
    Configuration menu
    Copy the full SHA
    977521b View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2021

  1. added a sawLet-minimization pass to completeNormOpenTerm

    Eddy Westbrook committed Dec 17, 2021
    Configuration menu
    Copy the full SHA
    3f52794 View commit details
    Browse the repository at this point in the history

Commits on Dec 20, 2021

  1. Merge branch 'master' into heapster/sawLet

    @m-yac
    m-yac committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    62e6dd7 View commit details
    Browse the repository at this point in the history

  2. clean up sha512 example, regenerate Coq files

    @m-yac
    m-yac committed Dec 20, 2021
    Configuration menu
    Copy the full SHA
    e791355 View commit details
    Browse the repository at this point in the history

Commits on Dec 21, 2021

  1. commit sha512.bc

    @m-yac
    m-yac committed Dec 21, 2021
    Configuration menu
    Copy the full SHA
    40519f8 View commit details
    Browse the repository at this point in the history

  2. fix Coq proofs to account for sawLets

    @m-yac
    m-yac committed Dec 21, 2021
    Configuration menu
    Copy the full SHA
    6641ebe View commit details
    Browse the repository at this point in the history

Commits on Dec 22, 2021

  1. Merge branch 'master' into heapster/sawLet

    Eddy Westbrook authored Dec 22, 2021
    Configuration menu
    Copy the full SHA
    11f8adf View commit details
    Browse the repository at this point in the history

  2. improve exp_explosion example

    @m-yac
    m-yac committed Dec 22, 2021
    Configuration menu
    Copy the full SHA
    359f0d6 View commit details
    Browse the repository at this point in the history

  3. remove exp_explosion timeout for CI

    @m-yac
    m-yac committed Dec 22, 2021
    Configuration menu
    Copy the full SHA
    02ecc7c View commit details
    Browse the repository at this point in the history