Erc20 elliot#24

Open

EllbellCode wants to merge 110 commits intoNethermindEth:mainfrom

EllbellCode:erc20_Elliot

Commits on Aug 7, 2024

Commits on Aug 22, 2024

Explicitly match none case
jkopanski
committed

Commits on Aug 26, 2024

Commits on Aug 28, 2024

Verify helper for accessing dynamic arrays
jkopanski
committed

Commits on Sep 26, 2024

Commits on Sep 27, 2024

Remove unneeded `aesop` Fixes build of `State.lean`

Coda-Coda
authored and
jkopanski
committed
Add `mstore_preserves_keccak_map` lemma and use it to progress the proof

Coda-Coda
authored and
jkopanski
committed
Spec and proof for the address keccak helper
jkopanski
committed

Commits on Oct 1, 2024

Commits on Oct 2, 2024

Add more preserved lemmas, finish balanceOf with it
jkopanski
committed

Commits on Oct 3, 2024

Remove unused preds from proofs
jkopanski
committed

Commits on Oct 4, 2024

Commits on Oct 7, 2024

[wip] rewark balance_of using ERC20 predicate
jkopanski
committed
Progess `balanceOf` proof

Coda-Coda
authored and
jkopanski
committed
Updated predicate, some lemmas
jkopanski
committed

Commits on Oct 8, 2024

[wip]
jkopanski
committed

Commits on Oct 9, 2024

more [wip]
jkopanski
committed

Commits on Oct 14, 2024

Commits on Oct 16, 2024

Extending keccak used range
jkopanski
committed

Commits on Oct 17, 2024

Commits on Oct 18, 2024

[wip] Fill sorry for `s["var_spender"]!! = var_spender`
Coda-Coda
committed

Commits on Oct 21, 2024

Commits on Oct 22, 2024

Commits on Oct 24, 2024

Commits on Oct 25, 2024

Commits on Oct 29, 2024

Commits on Nov 8, 2024

Commits on Nov 10, 2024

Fixed some simple remaining sorrys
Julek
committed

Commits on Nov 18, 2024

fix generation of double { {, credit to Daniel

Ferinko
authored and
Coda-Coda
committed

Commits on Nov 20, 2024

Commits on Nov 28, 2024

Commits on Nov 29, 2024

Commits on Dec 3, 2024

Commits on Feb 6, 2025

Defining transfer function
EllbellCode
committed

Commits on Feb 20, 2025

Progress
EllbellCode
committed
prove IsERC20 erc_20_ s
Ferinko
committed

Commits on Feb 24, 2025

progress
EllbellCode
committed
prove not out of fuel
Ferinko
committed

Commits on Feb 25, 2025

Commits on Feb 26, 2025

Completed fun_transfer lemma
EllbellCode
committed

Commits on Mar 3, 2025

tidying up transfer proof
EllbellCode
committed
tidying up transfer lemma
EllbellCode
committed

Commits on Mar 4, 2025

Edited msgSender, _transfer
EllbellCode
committed
progress
EllbellCode
committed

Commits on Mar 6, 2025

completion of transferfrom
EllbellCode
committed

Commits on Mar 12, 2025

updated reversion
EllbellCode
committed
reversion update
EllbellCode
committed

Commits on Mar 18, 2025

abi_encode
EllbellCode
committed

Commits on Mar 19, 2025

encode function verifications
EllbellCode
committed
encode functions
EllbellCode
committed
encode polish
EllbellCode
committed

Commits on Mar 26, 2025

progress and modification of revert
EllbellCode
committed

Commits on Mar 31, 2025

nested encodings
EllbellCode
committed

Commits on Apr 1, 2025

storage logic
EllbellCode
committed

Commits on Apr 2, 2025

checked_add proof
EllbellCode
committed

Commits on Apr 4, 2025

sorted mapping issue that broke clr_spec
EllbellCode
committed

Commits on Apr 7, 2025

switch proof
EllbellCode
committed
switch 2
EllbellCode
committed

Commits on Apr 8, 2025

update spec
EllbellCode
committed