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

(Replaced by #22) [Draft] Add ERC-20 Example #20

Closed
wants to merge 71 commits into from
Closed

(Replaced by #22) [Draft] Add ERC-20 Example #20

wants to merge 71 commits into from

Commits on Aug 7, 2024

  1. ERC20 code generated by VC

    @jkopanski
    jkopanski committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    289fbdd View commit details
    Browse the repository at this point in the history

  2. totalSupply verification

    @jkopanski
    jkopanski committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    8966ea2 View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2024

  1. Explicitly match none case

    @jkopanski
    jkopanski committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    bb2c323 View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2024

  1. Additional Address lemmas

    @jkopanski
    jkopanski committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    bef6cf9 View commit details
    Browse the repository at this point in the history

  2. EVM state reasoning lemmas

    @jkopanski
    jkopanski committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    a154fbd View commit details
    Browse the repository at this point in the history

Commits on Aug 28, 2024

  1. Verify helper for accessing dynamic arrays

    @jkopanski
    jkopanski committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    e9f9951 View commit details
    Browse the repository at this point in the history

Commits on Sep 26, 2024

  1. [wip] Useful lemmas, mostly regarding memory

    @jkopanski
    jkopanski committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    561e7f8 View commit details
    Browse the repository at this point in the history

  2. keccak based proof

    @jkopanski
    jkopanski committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    e748061 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2024

  1. Remove unneeded aesop Fixes build of State.lean

    @jkopanski
    Daniel Britten authored and jkopanski committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    1b79eb4 View commit details
    Browse the repository at this point in the history

  2. Add mstore_preserves_keccak_map lemma and use it to progress the proof 

    Note: this commit was made making some use of `claude-3.5-sonnet` using Cursor (https://www.cursor.com/).
    @jkopanski
    Daniel Britten authored and jkopanski committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    ee2c85c View commit details
    Browse the repository at this point in the history

  3. Spec and proof for the address keccak helper

    @jkopanski
    jkopanski committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    805f3cd View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2024

  1. [wip] balance of

    @jkopanski
    jkopanski committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    6697b11 View commit details
    Browse the repository at this point in the history

  2. Other kind of isPure

    @jkopanski
    jkopanski committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    666be98 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2024

  1. Add more preserved lemmas, finish balanceOf with it

    @jkopanski
    jkopanski committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    7df27ae View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2024

  1. Remove unused preds from proofs

    @jkopanski
    jkopanski committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    ddde452 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. ERC20 predicate

    @jkopanski
    jkopanski committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    313e842 View commit details
    Browse the repository at this point in the history

  2. Total supply that works with ERC20 predicate

    @jkopanski
    jkopanski committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    25dc2aa View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2024

  1. [wip] rewark balance_of using ERC20 predicate

    @jkopanski
    jkopanski committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    032ec1c View commit details
    Browse the repository at this point in the history

  2. Progess balanceOf proof

    @jkopanski
    Daniel Britten authored and jkopanski committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    5853aeb View commit details
    Browse the repository at this point in the history

  3. Updated predicate, some lemmas

    @jkopanski
    jkopanski committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    c08c17c View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2024

  1. [wip]

    @jkopanski
    jkopanski committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    4ec6099 View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2024

  1. more [wip]

    @jkopanski
    jkopanski committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    92219ee View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2024

  1. almost there

    @jkopanski
    jkopanski committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    2ebf7f8 View commit details
    Browse the repository at this point in the history

  2. Use proper items from predicate

    @jkopanski
    jkopanski committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    ff583de View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2024

  1. Extending keccak used range

    @jkopanski
    jkopanski committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    2db665f View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2024

  1. Ensure type of owner and spender is Address not UInt256 

    Adjust the `fun_balanceOf_abs_of_concrete` lemma so that `fun_balanceOf_user.lean` still builds successfully.
    Daniel Britten committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    0da520c View commit details
    Browse the repository at this point in the history

  2. [wip] 

    Based on `fun_balanceOf_abs_of_concrete`
    @Coda-Coda
    Coda-Coda authored and Daniel Britten committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    7d30c37 View commit details
    Browse the repository at this point in the history

  3. [wip]

    Daniel Britten committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    c262ae1 View commit details
    Browse the repository at this point in the history

  4. [wip]

    Daniel Britten committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    d267d41 View commit details
    Browse the repository at this point in the history

  5. keccak injectivity preservation

    @jkopanski
    jkopanski committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    ab6bec4 View commit details
    Browse the repository at this point in the history

  6. possible new spec

    @jkopanski
    jkopanski authored and Daniel Britten committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    5a68d47 View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

  1. [wip] Fill sorry for s["var_spender"]!! = var_spender

    Daniel Britten committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    d962a22 View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2024

  1. [wip] Main aspects of allowance proof finished

    Daniel Britten committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    a5956ef View commit details
    Browse the repository at this point in the history

  2. [wip] Fill final two sorries in fun_allowance_abs_of_concrete

    Daniel Britten committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    fb2e9c9 View commit details
    Browse the repository at this point in the history

Commits on Oct 22, 2024

  1. [wip] Update balanceOf proof so that it still builds 

    Needed due to changes in:
`Predicate.lean`
and
`mapping_index_access_mapping_address_uint256_of_address_user.lean`
which were made for the `allowance` proof.
    Daniel Britten committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    ab1c421 View commit details
    Browse the repository at this point in the history

  2. [wip] Begin making proof style improvements

    Daniel Britten committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    4d1dfd9 View commit details
    Browse the repository at this point in the history

  3. Merge pull request #15 from NethermindEth/allowance 

    Add `allowance` proof and tweak `balanceOf` proof, with updates to `Predicate.lean` and the helper functions
    @jkopanski
    jkopanski authored Oct 22, 2024
    Configuration menu
    Copy the full SHA
    0b333cf View commit details
    Browse the repository at this point in the history

Commits on Oct 24, 2024

  1. [wip] Handle hash collisions properly in specifications for `allowanc… 

    …e`, `balanceOf` and the helper
    Daniel Britten committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    e33c914 View commit details
    Browse the repository at this point in the history

  2. updated_keccak_map

    @jkopanski
    jkopanski committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    cdcdb54 View commit details
    Browse the repository at this point in the history

  3. [wip] a bit of adjustment for new spec

    @jkopanski
    jkopanski committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    74d7435 View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2024

  1. [wip] Correction to helper spec

    Daniel Britten committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    2dfc22a View commit details
    Browse the repository at this point in the history

  2. [wip] QED on allowance, except sorries

    Daniel Britten committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    c185534 View commit details
    Browse the repository at this point in the history

  3. [wip]

    Daniel Britten committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    c836928 View commit details
    Browse the repository at this point in the history

  4. [wip] QED on allowance

    Daniel Britten committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    6840248 View commit details
    Browse the repository at this point in the history

  5. [wip] QED on balanceOf

    Daniel Britten committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    2d37414 View commit details
    Browse the repository at this point in the history

  6. [wip] Remove some leftover commented out code

    Daniel Britten committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    4bd6a34 View commit details
    Browse the repository at this point in the history

  7. Merge pull request #16 from NethermindEth/WIP-erc20-daniel-3 

    `allowance` and `balanceOf` build with hash collision handling
    @jkopanski
    jkopanski authored Oct 25, 2024
    Configuration menu
    Copy the full SHA
    fa05917 View commit details
    Browse the repository at this point in the history

  8. Fixed deep recursion in the panic_error_0x11

    @jkopanski
    jkopanski committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    6ee04d8 View commit details
    Browse the repository at this point in the history

  9. keccak helper

    @jkopanski
    jkopanski committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    f20cdff View commit details
    Browse the repository at this point in the history

  10. [wip] adjust for EVM structure split

    @jkopanski
    jkopanski committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    5dd0ad9 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2024

  1. Make use of the keccak helper proof for the other keccak helper

    Daniel Britten committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    9c5e923 View commit details
    Browse the repository at this point in the history

  2. Merge pull request #18 from NethermindEth/keccak-helper-for-allowance 

    Make use of the keccak helper proof for the other keccak helper
    @jkopanski
    jkopanski authored Oct 29, 2024
    Configuration menu
    Copy the full SHA
    6586986 View commit details
    Browse the repository at this point in the history

  3. Use new tactic

    @jkopanski
    jkopanski committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    9df1fda View commit details
    Browse the repository at this point in the history

Commits on Nov 8, 2024

  1. Add mstore_preserves_used_range lemma

    @Coda-Coda
    Coda-Coda committed Nov 8, 2024
    Configuration menu
    Copy the full SHA
    f223382 View commit details
    Browse the repository at this point in the history

  2. Add preservation of isEVMState to helper spec and prove it

    @Coda-Coda
    Coda-Coda committed Nov 8, 2024
    Configuration menu
    Copy the full SHA
    c243670 View commit details
    Browse the repository at this point in the history

  3. Fill sorries related to preservation of isEVMState 

    As required, add `s₀.evm.isEVMState` as a precondition for `allowance` and `balanceOf`.
    @Coda-Coda
    Coda-Coda committed Nov 8, 2024
    Configuration menu
    Copy the full SHA
    26439d7 View commit details
    Browse the repository at this point in the history

Commits on Nov 10, 2024

  1. Fixed some simple remaining sorrys

    @Julek
    Julek committed Nov 10, 2024
    Configuration menu
    Copy the full SHA
    74ef5ef View commit details
    Browse the repository at this point in the history

Commits on Nov 18, 2024

  1. fix generation of double { {, credit to Daniel

    @Ferinko
    Ferinko authored and Daniel Britten committed Nov 18, 2024
    Configuration menu
    Copy the full SHA
    1a96b5e View commit details
    Browse the repository at this point in the history

Commits on Nov 20, 2024

  1. Improvements to generator: switch cases. By František 

    Co-authored-by: Frantisek Silvasi <[email protected]>
    @Ferinko
    Daniel Britten and Ferinko committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    004ecae View commit details
    Browse the repository at this point in the history

  2. Improvements to generator. By František 

    Co-authored-by: Frantisek Silvasi <[email protected]>
    @Ferinko
    Daniel Britten and Ferinko committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    583fd60 View commit details
    Browse the repository at this point in the history

  3. Generate erc20shim.yul as described in erc20shim-generation.md

    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    4befbe0 View commit details
    Browse the repository at this point in the history

  4. Regenerate ERC20, excluding files with existing proofs

    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    9974e69 View commit details
    Browse the repository at this point in the history

  5. [To revert] Regenerate rest of ERC20, overwriting existing proofs

    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    715d172 View commit details
    Browse the repository at this point in the history

  6. Revert "[To revert] Regenerate rest of ERC20, overwriting existing pr… 

    …oofs"

Restore existing proofs overwritten by the generator.
    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    d9d3122 View commit details
    Browse the repository at this point in the history

  7. Improve balanceOf proof. By František. 

    Copied in from `Ferinko/balanceOf` branch, currently 673b85.

Co-authored-by: Frantisek Silvasi <[email protected]>
    @Ferinko
    Daniel Britten and Ferinko committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    892c143 View commit details
    Browse the repository at this point in the history

  8. Change clr_varstore tactic and include it in generator. By František. 

    Copied across `Wheels.lean` and `ProofGenerator.hs` from `Ferinko/Workshop` branch, currently 7631d8.

Co-authored-by: Frantisek Silvasi <[email protected]>
    @Ferinko
    Daniel Britten and Ferinko committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    c1b6bdc View commit details
    Browse the repository at this point in the history

  9. Update stack.yaml.lock (automatic change from stack build)

    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    ca1f0a0 View commit details
    Browse the repository at this point in the history

  10. Regenerate ERC20, excluding files with existing proofs

    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    0c9754a View commit details
    Browse the repository at this point in the history

  11. [To revert] Regenerate ERC20, overwriting existing proofs

    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    cf4e755 View commit details
    Browse the repository at this point in the history

  12. Revert "[To revert] Regenerate ERC20, overwriting existing proofs" 

    Restore existing proofs overwritten by the generator.
    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    57c033d View commit details
    Browse the repository at this point in the history

  13. Add commas to reflect new clr_varstore syntax 

    This makes the invocations of `clr_varstore,` behave the same as `clr_varstore` without the comma did prior to the changes to `Wheels.lean` in 61166b.
    Daniel Britten committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    087fa5c View commit details
    Browse the repository at this point in the history