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

Pancake to target correctness proof (resource aware version) #958

Merged
merged 12 commits into from Jul 5, 2023
Merged

Pancake to target correctness proof (resource aware version) #958

merged 12 commits into from Jul 5, 2023

Commits on Jun 28, 2023

  1. pancake: Pancake code never returns NotEnoughSpace for wordSem

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    e8464b2 View commit details
    Browse the repository at this point in the history

  2. pancake: add stack_size & stack_limit const lemmas

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    17e982c View commit details
    Browse the repository at this point in the history

  3. pancake: add compile_prog_max 

    this returns the value computed with max_depth along with
the original compile_prog return value

for Pancake to target
    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    fde8d1b View commit details
    Browse the repository at this point in the history

  4. pancake: add option_lt

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    fb58aa1 View commit details
    Browse the repository at this point in the history

  5. pancake: pan_to_target compiler proof (resource aware) 

    pancake to target compiler correctness proof with
precise resource limit condition
    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    0162036 View commit details
    Browse the repository at this point in the history

  6. export LENGTH_read_mem

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    650c2dd View commit details
    Browse the repository at this point in the history

  7. pancake: use LENGTH_read_mem (remove duplicate)

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    f8831c4 View commit details
    Browse the repository at this point in the history

  8. pancake: improve word assumptions for heap

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    236c797 View commit details
    Browse the repository at this point in the history

  9. pancake: remove the old correctness proof

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    59d6dec View commit details
    Browse the repository at this point in the history

  10. pancake: cleanup

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    068d314 View commit details
    Browse the repository at this point in the history

  11. pancake: rename

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    9a80d5b View commit details
    Browse the repository at this point in the history

  12. pancake: fix rebase fallouts

    @mktnk3
    mktnk3 committed Jun 28, 2023
    Copy the full SHA
    29c1b18 View commit details
    Browse the repository at this point in the history