Currently, when when an annotation appears before JUMPDEST, this breaks JUMPs to that destination. This issue keeps track of fixing this.

Currently an account's program is represented as a single list of instructions. With this representation I face a performance problem in Isabelle/HOL when the program has more than 100 instructions. Isabelle/HOL cannot display the intermediate goals within 10 minutes. This issue keeps track of implementing the program as a function from the program counter to an instruction. The hope is that the program is not going to be copied around and the intermediate goals stay small enough to display.

Try the simplification debugger in https://arxiv.org/abs/1406.0292, to see if it is useful against the current performance problem around simplification in Deed.thy.

We can reason about what happens during a CALL, using the invariant we establish. For DELEGATECALL, we need to import the invariant from somewhere else. This issue keeps track of designing and implementing an interface for that.

In https://github.com/ethereum/solidity/blob/develop/libevmasm/ExpressionClasses.cpp, there is a list of optimization rules called Rules::Rules(), which look like a good target for Isabelle/HOL.

A while ago I attended a talk about implementing some complicated procedure in Isabelle/HOL the only thing I remember was "decompose records and pass the individual members in a long list of arguments". The speaker didn't want to do that but that was necessary for performance improvements. Apply this technique in ContractSem.thy.

This issue keeps track of formal verification of Deed contract that can be found here: https://github.com/Arachnid/ens/blob/master/HashRegistrarSimplified.sol

• add some annotations
• define an invariant
• prove that the invariant is kept and the annotations are followed
• prove that only the registrar can decrease the balance
• make one mistake and catch it.
• use the Isabelle/HOL feature to create a PDF about the above development

For #5, it is necessary to call the extracted EVM (prepared in #30) on the test data parsed in #31.

This issue keeps track of annotating ContractEnv.thy so that it produces a nice PDF.

This issue keeps track of testing the EVM implementation in this directory against https://github.com/ethereum/tests/tree/develop/VMTests

This task keeps track of trying a relational version of program_sem and see if that makes the proof one line or not.

Currently the sizes of the proof goals seem to grow rapidly when the program under verification is bigger. This issue keeps track of making the goals smaller.

This issue keeps track of annotating ContractSem.thy so that the Isabelle system can produce a readable PDF.

Currently RelationalSem.thy defines a predicate no_assertion_failure that uses an invariant. This issue keeps track of generalizing this predicate so that the precondition and the postcondition can be different. This would allow, for example, to prove that a contract does not change its status unless it is called by a particular address.

Currently Deed.thy tries to verify that the code of the account never changes but sometimes it becomes empty. This issue keeps track of fixing this problem by changing the statement.

In the definition of jump in ContractSem.thy, a variable_env is copied into two subterms. This issue keeps track of streamlining the occurrences so that the variable_env does not need to be copied.

The current approaches do not work for programs that contain loops. For verifying programs with loops we need

1. a framework that composes Hoare triples
2. the rule for loops in that Hoare logic
3. proof of soundness of the Hoare logic with respect to the operational semantics
4. an example verification of a program with loops

• import the Lem definitions from https://github.com/mrsmkl/ethereum-lem
• create a script that translates Lem definitions into Isabelle/HOL files
• change the readme about insalling Lem
• Fix AlwaysFail and FailOnReentrance.

When I try to write a proof about a ~500 byte proof, the simp tactic does not finish.

Things I can try:

• write a more efficient parser in Isabelle/HOL (spent a few hours on it)
• write an external parser in another language (try this next)
• find an Isabelle/HOL command that forces some normalization

In AlwaysFails.thy it takes less than a second to execute one instruction symbolically, while in Deed.thy it takes a few minutes (#11). This issue keeps track of solving this performance problem.

• compare the simplification trace in AlwaysFails.thy and in Deed.thy and identify if any superfluous rewriting is happening.
• make sure the program is not parsed every time an instruction is executed

Currently the predicate account_state_responds_to_world requires an abstract specification. This predicate is for functional correctness.

We need another predicate that states that all assertions hold after any history of invocations, returns and failures.

Currently venv_advance_pc looks up the program to figure out the size of the current instruction. However, at the time venv_advance_pc is used, the instruction is already known. There would be performance improvements if we replaced the whole program with a number.

This issue keeps track of the tests in JSON formats (https://github.com/ethereum/tests/tree/develop/VMTests) in OCaml.

The let expression is not expanded by default, and it is dangerous to tell Isabelle/HOL to do so. This issue keeps track of cleaning ContractSem.thy file so that it does not contain let expressions.

Currently, the simplifier expands any term of the form

program_content program n

using the definition of program. This grows the size of the term unnecessarily when n is not a concrete value. This issue keeps track of restricting this rewriting to the cases when n is a concrete value.

Currently the compilation has to be checked in the Isabelle/HOL IDE. This issue keeps track of adding a Makefile that compiles all files.

When suicide happens during reentrance, the effect of the suicide should not be visible to the caller. In order to fix this problem, a "suicide list" is necessary.

This issue keeps track of annotating RelationalSem.thy so that it produces a readable PDF under the Isabelle system.

The binary tree format used in #26 makes the verification much (at least 50 times) faster than the list format which is currently used.

This issue keeps track of porting https://github.com/mrsmkl/evmverif/blob/master/coq/Fragment.v#L148 into this repository.

This issue keeps track of annotating Deed.thy so that it produces a readable PDF.

The Word library of Isabelle/HOL already defines a function called uint. So the datatype uint should be called with another name.

Implement the gas mechanism so that out-of-gas happens. Also make GAS return the correct value.

Currently return_result record contains the balance of all accounts, then, conceptually speaking, the record should also contain the storage of the account under verification. This issue keeps track of answering this suggestion.

The memory usage should keep track of the memory usage and this can be stated and proved. If this fails, that might indicate an error in the formalization or in the original specification.

This issue keeps track of annotating Instructions.thy so that it produces a nice PDF.

This issue keeps track of extracting the program_sem function and update_account_state functions so that these codes run in OCaml.

Currently the relational semantics considers the possibility of returning to a program counter not after CALL, DELEGATECALL, CALLCODE or CREATE. This creates many superfluous possibilities. This issue keeps track of removing these cases.

After a contract destroys itself, currently, its account state does not change. The code should become empty and the balance should become zero.

Without this property, the regsitrar authentication is not very useful.