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

Helper changes for symbolic testing #769

Merged
merged 38 commits into from
May 12, 2020
Merged

Helper changes for symbolic testing #769

merged 38 commits into from
May 12, 2020

Commits on Apr 28, 2020

  1. symb-test: evm-types: Yi changes

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    fa6a7b9 View commit details
    Browse the repository at this point in the history

  2. edsl,evm-types,serialization: extensions for symb-test

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    48e4fde View commit details
    Browse the repository at this point in the history

  3. edsl: small refactoring for symb-test

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    4c482ba View commit details
    Browse the repository at this point in the history

  4. specs/lemmas.k: extracted some lemmas common to Java and Haskell to c… 

    …ommon module. Required for symbolic testing.
    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    1674e30 View commit details
    Browse the repository at this point in the history

  5. lemmas: extra lemma for byte array simplification (+1 squashed commits) 

    Squashed commits:

[ca5056a] lemmas.k: extra for kore and symb-testing.
    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    d88352e View commit details
    Browse the repository at this point in the history

  6. evm-types: #lookup: marking [functional]. Sound change.

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    52b430d View commit details
    Browse the repository at this point in the history

  7. formatting fixes

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    47ec63e View commit details
    Browse the repository at this point in the history

  8. Revert "symb-test: evm-types: Yi changes" 

    This reverts commit 8682019.
    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    d927c81 View commit details
    Browse the repository at this point in the history

  9. evm-types, edsl: replacing some [functional] with #Ceil rules

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    4e23fc2 View commit details
    Browse the repository at this point in the history

  10. formatting fixes

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    bdd5aa6 View commit details
    Browse the repository at this point in the history

  11. evm-types: One more #Ceil rule

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    ff2aef8 View commit details
    Browse the repository at this point in the history

  12. evm-types: #Ceil rule correction

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    ba9fa92 View commit details
    Browse the repository at this point in the history

  13. evm-types: replaced [functional] with #Ceil for #lookup

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    d0bbce2 View commit details
    Browse the repository at this point in the history

  14. lemmas: PR comments addressed

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    74c6517 View commit details
    Browse the repository at this point in the history

  15. evm-types: moved all #Ceil rules in one place, to be compatible with … 

    …all backends.
    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    2fdc586 View commit details
    Browse the repository at this point in the history

  16. PR fixes

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    00dc5d7 View commit details
    Browse the repository at this point in the history

  17. PR fix - #Ceil(#buf) rule generates condition for SIZE and DATA

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    4888f75 View commit details
    Browse the repository at this point in the history

  18. symb-test: #Ceil rules for #padToWidth, #patRightToWidth corrected.

    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    ad1ff19 View commit details
    Browse the repository at this point in the history

  19. symb-test: reverting rule #Ceil(#buf(SIZE, DATA)) to simplified form … 

    …for performance reasons.
    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    96a57c3 View commit details
    Browse the repository at this point in the history

  20. evm-types, Makefile: tangle filter for #Ceil(padToWidth) & related ru… 

    …les.
    @denis-bogdanas
    denis-bogdanas committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    aa18686 View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2020

  1. lemmas.k: [..] rule simplified

    @denis-bogdanas
    denis-bogdanas committed Apr 29, 2020
    Configuration menu
    Copy the full SHA
    ade2972 View commit details
    Browse the repository at this point in the history

  2. lemmas.k: #sizeWordStack rule side conditions

    @denis-bogdanas
    denis-bogdanas committed Apr 29, 2020
    Configuration menu
    Copy the full SHA
    d31368a View commit details
    Browse the repository at this point in the history

Commits on Apr 30, 2020

  1. erc20/abstract-semantics-segmented-gas.k: dependency removed

    @denis-bogdanas
    denis-bogdanas committed Apr 30, 2020
    Configuration menu
    Copy the full SHA
    1818dd4 View commit details
    Browse the repository at this point in the history

  2. fix for previous

    @denis-bogdanas
    denis-bogdanas committed Apr 30, 2020
    Configuration menu
    Copy the full SHA
    267b847 View commit details
    Browse the repository at this point in the history

Commits on May 5, 2020

  1. evm-types: removed #Ceil rules for padLeftBytes, padRightBytes. Moved… 

    … to k/domains.k
    @denis-bogdanas
    denis-bogdanas committed May 5, 2020
    Configuration menu
    Copy the full SHA
    5617780 View commit details
    Browse the repository at this point in the history

  2. edsl: Full #Ceil rule for #buf, but slow for erc20-verifier.

    @denis-bogdanas
    denis-bogdanas committed May 5, 2020
    Configuration menu
    Copy the full SHA
    b5f6ff4 View commit details
    Browse the repository at this point in the history

  3. evm-types: replaced 3 #Ceil rules with complete definition and [fun… 

    …ctional]
    @denis-bogdanas
    denis-bogdanas committed May 5, 2020
    Configuration menu
    Copy the full SHA
    eaad80d View commit details
    Browse the repository at this point in the history

Commits on May 6, 2020

  1. Reverse commit "evm-types, Makefile: tangle filter for #Ceil(padToWid… 

    …th) & related rules"
    @denis-bogdanas
    denis-bogdanas committed May 6, 2020
    Configuration menu
    Copy the full SHA
    0a625af View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into symb-test-prep

    @denis-bogdanas
    denis-bogdanas committed May 6, 2020
    Configuration menu
    Copy the full SHA
    04118fe View commit details
    Browse the repository at this point in the history

  3. formatting

    @denis-bogdanas
    denis-bogdanas committed May 6, 2020
    Configuration menu
    Copy the full SHA
    8beec67 View commit details
    Browse the repository at this point in the history

  4. evm: performance enhancement driven by profiling ERC20 specs.

    @denis-bogdanas
    denis-bogdanas committed May 6, 2020
    Configuration menu
    Copy the full SHA
    3b3e533 View commit details
    Browse the repository at this point in the history

  5. Makefile: added tangle mode symbolic-bytes just for Haskell backend.

    @denis-bogdanas
    denis-bogdanas committed May 6, 2020
    Configuration menu
    Copy the full SHA
    90032ce View commit details
    Browse the repository at this point in the history

  6. evm-types: fixes

    @denis-bogdanas
    denis-bogdanas committed May 6, 2020
    Configuration menu
    Copy the full SHA
    c42ce64 View commit details
    Browse the repository at this point in the history

Commits on May 8, 2020

  1. evm-types: make #padToWidth and #padRightToWidth total

    @ehildenb
    ehildenb committed May 8, 2020
    Configuration menu
    Copy the full SHA
    e570a6b View commit details
    Browse the repository at this point in the history

  2. evm-types: leave wordstack alone if negative update is provided

    @ehildenb
    ehildenb committed May 8, 2020
    Configuration menu
    Copy the full SHA
    f030a30 View commit details
    Browse the repository at this point in the history

  3. evm: formatting

    @ehildenb
    ehildenb committed May 8, 2020
    Configuration menu
    Copy the full SHA
    959450f View commit details
    Browse the repository at this point in the history

  4. Reverse commit "Makefile: added tangle mode symbolic-bytes just for… 

    … Haskell backend."
    @denis-bogdanas
    denis-bogdanas committed May 8, 2020
    Configuration menu
    Copy the full SHA
    8616b05 View commit details
    Browse the repository at this point in the history

Commits on May 11, 2020

  1. Merge branch 'master' into symb-test-prep

    @ehildenb
    ehildenb authored May 11, 2020
    Configuration menu
    Copy the full SHA
    d2a42e0 View commit details
    Browse the repository at this point in the history