KProve Web applied to the Vat proofs in the KEVM regression test suite

[0xverif]

Goal is to go from vat.sol to running the regression test suite with the fewest human interaction and nice UI.

• [x] Single proofs working on summarizer ( + demo )
• [ ] Get KProve Web upstreamed and merged on K frontend repo (working on some simple regression tests there) https://github.com/runtimeverification/erc20-verification/issues/304
• [ ] Video demo of kprove-web on ERC20 contract in KEVM repo (tests/specs/examples/erc20-spec.md)
• [ ] Multi-contract support needed in solc-to-k to hack together MCD example (hardcoding addresses or supplying in separate config file is fine): https://github.com/runtimeverification/ksummarize/issues/38
• [ ] Migrate KEVM MCD regression test-suite to start from Solidity files and go to proofs.
• [ ] Get all Vat proofs running on the summarizer (requires finding missing lemmas and adding them into the semantics)
• [ ] Video demo of kprove-web being used to port a Vat proof to haskell backend (from viewers perspective, we're just verifying a contract)