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.

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

Conversation

Coda-Coda
Copy link
Collaborator

@Coda-Coda Coda-Coda commented Nov 20, 2024

Replaced by #22 due to #20 (comment).
This pull request, currently a DRAFT, is to prepare for merging the ERC-20 example into main.
This is a work in progress.

jkopanski and others added 25 commits October 25, 2024 09:22
`allowance` and `balanceOf` build with hash collision handling
Make use of the keccak helper proof for the other keccak helper
As required, add `s₀.evm.isEVMState` as a precondition for `allowance` and `balanceOf`.
…oofs"

Restore existing proofs overwritten by the generator.
Copied in from `Ferinko/balanceOf` branch, currently 673b85.

Co-authored-by: Frantisek Silvasi <[email protected]>
Copied across `Wheels.lean` and `ProofGenerator.hs` from `Ferinko/Workshop` branch, currently 7631d8.

Co-authored-by: Frantisek Silvasi <[email protected]>
Restore existing proofs overwritten by the generator.
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.
@Coda-Coda Coda-Coda changed the base branch from main to keccak-helper November 21, 2024 23:46
@Coda-Coda Coda-Coda changed the base branch from keccak-helper to main November 21, 2024 23:46
@Coda-Coda
Copy link
Collaborator Author

main updated, see #21. It seems necessary to create a new PR to get GitHub Actions to build using the new main.

@Coda-Coda Coda-Coda closed this Nov 21, 2024
@Coda-Coda Coda-Coda changed the title [Draft] Add ERC-20 Example (Replaced by #22) [Draft] Add ERC-20 Example Nov 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants