Daejun Park

Inconsistency with the standard for `burn` and `operatorBurn`

1

There is a discrepancy between the standard and the reference implementation regarding the `burn` and `operatorBurn` functions: The current standard (https://github.com/ethereum/EIPs/blob/b41669ede219b9599a6a1c637e578b8a444ad6b1/EIPS/eip-777.md) says: > The data field of the tokensToSend hook...

out of memory error in parsing

8

Parsing doesn't scale well for Bag, Set, and Map. For example, a bag with _only_ **16** elements requires ~**6GB** memory to be parsed! To reproduce: run the following command: ```...

Preventing vault price reset in ERC4626

4

**🧐 Motivation** New security feature recommendation preventing the ERC4626 vault price reset. **📝 Details** I'm concerned with the _possibility_ of ERC4626 vaults being emptied during their lifecycle. This is because,...

Failed to conform to ES5.1, Section 8.7.2 PutValue (V, W), [[Put]], Step 7.a

2

It seems to me that S5 does not conform to ES5.1, Section 8.7.2 PutValue (V, W), [[Put]], Step 7.a. For the following test program: ``` // 8.7.2 PutValue (V, W),...

Failed to conform to ES5.1, Section 10.2.1.1.3 SetMutableBinding (N,V,S), Step 4

2

It seems to me that S5 does not conform to ES5.1, Section 10.2.1.1.3 SetMutableBinding (N,V,S), Step 4, if-condition is true. For the following test program: ``` // 10.2.1.1.3 SetMutableBinding (N,V,S),...

Proposal for additional verification specs

1

In addition to the [existing specs](https://github.com/morpho-org/metamorpho/tree/398c553b06769fc3a84d044c4d1f097de77a8548/certora), the following specs could also be considered. If the prover is incapable of verifying them, fuzzing could be considered as an alternative. 1. **[Share...

wip

support multiple array lengths at once, e.g., (syntax to be decided), `halmos --array-lengths x={1,2,3}` this should be equivalent to running halmos multiple times for each length value: ``` halmos --array-lengths...

(do not merge)

currently erc4626 tests fail due to timeout