matheusaaguiar
matheusaaguiar
If anyone is interested in taking over the PR, the changes are available at branch [fixInheritedReturnsPrivateFunction](https://github.com/ethereum/solidity/tree/fixInheritedReturnsPrivateFunction)
**Gas benchmarks for external tests** ** OUTDATED ** IR-NO-OPTIMIZE |------------------|---------------|----------------|------------| | project | bytecode_size | deployment_gas | method_gas | |------------------|---------------|----------------|------------| | bleeps | | | | | brink | |...
Benchmarks for [commit f71e542 ](https://github.com/ethereum/solidity/pull/13177/commits/f71e542f9a1e0c57be4c1bad82ccf05df6143b62) (different checks for less than or equal int128) IR-NO-OPTIMIZE |------------------|---------------|----------------|------------| | project | bytecode_size | deployment_gas | method_gas | |------------------|---------------|----------------|------------| | bleeps | | |...
@wechman I tried that, but it only works for uint256bit. I was testing this approach yesterday to get benchmarks, but the proof is not passing and I am not sure...
**Benchmarks for [commit](https://github.com/ethereum/solidity/pull/13177/commits/003f02b023ad53e337f84216905a097d2b1ece29) (Added special case for uint256)** IR-NO-OPTIMIZE |------------------|---------------|----------------|------------| | project | bytecode_size | deployment_gas | method_gas | |------------------|---------------|----------------|------------| | bleeps | | | | | brink | |...
Looking at the failed [test](https://app.circleci.com/pipelines/github/ethereum/solidity/25171/workflows/3f7f702b-9124-4b30-b873-ce0a28444259/jobs/1108929) I guess that z3 solver is having trouble proving the rules for 16 bit.
**Updated Benchmarks** IR-NO-OPTIMIZE |------------------|---------------|----------------|------------| | project | bytecode_size | deployment_gas | method_gas | |------------------|---------------|----------------|------------| | bleeps | | | | | brink | | | | | chainlink | |...
> > @wechman I tried that, but it only works for uint256bit. I was testing this approach yesterday to get benchmarks, but the proof is not passing and I am...
Yes. I am testing this approach with signed int too. I am checking if numbers between 128bit and 256bit are going to be properly covered, but I think it should...
I think the problem is that, for signed int, when we do `product = (x*y) & bitmask`, the MSB (sign bit) gets turned off. This is a problem for negative...