Add vyper support

[karmacoma-eth]

Halmos is an EVM-level tool, which means that in principle we can target any bytecode, regardless of the source language used (Solidity, Vyper, Huff, ...)

However at the moment at the moment we only provide a Foundry frontend, which means that halmos tests need to be expressed in foundry-style Solidity contracts.

This task is about adding a vyper frontend -- here is a rough sketch of what will be needed:

• detecting the project framework
• invoking the right tool to build the project
• parse the build output (we need the contract names and their bytecode, as well as function names and custom annotations if these are supported)
• specify the search target -- halmos currently looks for assertion failures, i.e. executions that finish with Panic(1). Does this work the same in vyper or does it need to be changed?
• halmos-cheatcodes are available as a solidity library, do we need an equivalent in vyper to write tests comfortably?

So mostly this is about wiring the inputs and outputs correctly, I don't expect changes in the core sevm execution engine.

Any help from devs proficient in vyper would be appreciated! 🙏

[ControlCplusControlV]

Right now Vyper projects are split between 2 main frameworks,

1. Titanoboa, a Vyper interpreter

2. Apeworx, a more universal and standard testing framework

Titanoboa translates Vyper code into Python AST and runs it natively, so supporting that may be difficult, while apeworx takes a standard tx-based approach and runs code in py-evm. I prefer Titanoboa myself but supporting both would be good. I know though that @fubuloubu has done a lot of work to ensure that Apeworx complies with an ERC standard artifact though, so it's best to start there imo (and more builtin compiler options, as Titanoboa isn't really a stand-alone thing and most vyper projects can easily support Ape)

AFAIK assertion failures are Panic(1)

Apeworx supports chain-level cheatcodes like time advancing, and we could even use ape-foundry if it makes it easier on the backend to support (I think that is how this works?)

[fubuloubu]

The vyper interpreter in titanoboa executes code via py-evm, it actually functions very similarly to foundry in that all code is executed natively without transaction semantics automatically applied (unlike ape or Hardhat).

What makes titanoboa a little different is that you would still use python to work with the interpreter and create tests for vyper code. Injecting the Panic opcode is possible since we supportUNREACHABLE as a semantic switch inside vyper to generate the designated Invalid opcode, which can be used by the engine

[charles-cooper]

0xFE is generated by the assert ..., UNREACHABLE statement.

re. titanoboa - it was originally designed to execute code via py-evm, but it actually has multiple backends now, including network mode which executes via RPC. 3rd party integrations could work presumably the same way, by overriding execute_code and deploy_code as here: https://github.com/vyperlang/titanoboa/blob/429fcd9fb6a1da2215dd8cf709965cce13ea93be/boa/network.py

[karmacoma-eth]

Right now Vyper projects are split between 2 main frameworks,

what about brownie? Curve uses it, right?

[fubuloubu]

Right now Vyper projects are split between 2 main frameworks,

what about brownie? Curve uses it, right?

We are in the process of converting them from brownie to ape, with Titanoboa being used fairly heavily as well

[charles-cooper]

new curve projects are pretty much off brownie btw - see for instance curve-stablecoin and tricrypto-ng. they are pretty much using titanoboa for unit/fuzzing and ape for integration.

[karmacoma-eth]

Update: analyzing vyper bytecode fails on storage access for mappings

vyper: keccak256(uint256(slot) . uint256(key))
solidity: keccak256(uint256(key) . uint256(slot))

this is a blocker, we need to fix this first in halmos

[daejunpark]

Update: analyzing vyper bytecode fails on storage access for mappings

vyper: keccak256(uint256(slot) . uint256(key)) solidity: keccak256(uint256(key) . uint256(slot))

this is a blocker, we need to fix this first in halmos

this will be fixed by #192
e.g., vyper erc20 test: f692863