chriseth

pragma solidity ^0.4.0;

library Pairing {
    struct G1Point {
        uint X;
        uint Y;
        uint Z;
    }
    struct G2Point {
        uint[2] X;

chriseth

Solidity Assembly

This assembly language tries to achieve several goals:

1. Programs written in it should be readable, even if the code is generated by a compiler from Solidity.
2. The translation from assembly to bytecode should contain as few “surprises” as possible.
3. Control flow should be easy to detect to help in formal verification and optimization.

In order to achieve the first and last goal, assembly provides high-level constructs like for loops, switch statements and function calls. It should be possible to write assembly programs that do not make use of explicit SWAP, DUP, JUMP and JUMPI statements, because the first two obfuscate the data flow and the last two obfuscate control flow. Furthermore, functional statements of the form ‘mul(add(x, y), 7)’ are preferred over pure opcode statements like ‘7 x y add mul’ because in the first form, it is much easier to see which operand is used for which opcode.

chriseth

Having seen @pirapira's sketch of Bamboo ( https://github.com/pirapira/bamboo/ ), which proposed to add better control about the "smart contract program flow", even across calls, I thought that this should certainly be added to Solidity, and actually, it might even be possible now to a certain degree using inline assembly.

The problem is that with many functions in a contract, it is not always clear which can be called at which stage in the contract's lifetime. Certain smart contracts would be easier to understand if written as follows:

chriseth

This gist shows how formal conditions of Solidity smart contracts can be automatically verified even in the presence of potential re-entrant calls from other contracts.

Solidity already supports formal verification of some contracts that do not make calls to other contracts. This of course excludes any contract that transfers Ether or tokens.

The Solidity contract below models a crude crowdfunding contract that can hold Ether and some person can withdraw Ether according to their shares. It is missing the actual access control, but the point that wants to be made

chriseth

Test interface

If testing is enabled the following features are disabled:

 - proof of work verification
 - future timestamp checks
 
It is important to ignore future timestamps so that the time can be set to e.g. 1 year in the future and
also because the timestamp has to increase by one each block, which means that if a lot of blocks are mined
in one run, they will be in the future.

chriseth

In order to easy source code verification of complex contracts that are spread across several files, we need a standardized interface how to describe the relations between those files. In order to achieve that, the remapping feature was recently integrated into the compiler itself.

The next step is to define how the names of source files and the addresses of libraries are handed over to the compiler. The following json description format will serve both as input to the compiler and as output from it. It is used to uniquely determine the input that results in a certain bytecode for a single contract. If the compiler is invoked in a different way, not using this input (for example by using a file content retrieval callback), the compiler can still generate it alongside the bytecode of each contract.

chriseth

contract EVM {
    struct VMState {
        uint[1024] stack;
        uint stackHeight;
        bytes bytecode;
        uint pc;
        uint[] mem;
    }
    function step(VMState _state) internal returns (bool)
    {

chriseth

; ModuleID = 'ff3464194a50cf29cad4ee2fe53e021f8310b662d72bdd581f1d734fa3faaa41-ff4707a95aa344ac'

%Runtime = type { %RuntimeData*, %Env*, %Array }
%RuntimeData = type { i64, i64, i8*, i64, i256, i256, i256, i256, i256, i256, i256, i256, i64, i64, i8*, i64 }
%Env = type opaque
%Array = type { i256*, i64, i64 }

@code = private unnamed_addr constant [301 x i8] c"`\00``\81\81R`\80\82\81R`\C0`@\81\90R`\A0\84\81Ra\03\E8\94\90\91\81\90\81\90\81\90b\0FB@\90\80Y\10a\002WPY[\81\81Rc\01\E8H \81\01`@\81\90R\90\98P\80Y\10a\00NWPY[\81\81Rc\01\E8H \81\01`@\81\90R\90\97P\80Y\10a\00jWPY[\90\81Rc\01\E8H \81\01`@R\94P[\87\84\10\15a\00\B8W`\00\92P\82P[\87\83\10\15a\00\F9W\82\88\85\02`\01\01\01` \02\90P\82\84\02\81\88\01R\82\84\02\81\87\01R`\01\92\90\92\01\91a\00\89V[`\00\93P\83P[\87\84\10\15a\01\05W`\00\92P\82P[\87\83\10\15a\01\1AWP\82\87\02\82\01`\01\90\81\01` \02\86\81\01Q\88\82\01Q\01\86\82\01R\92\01\91a\00\CEV[`\01\93\90\93\01\92a\00zV[PPPPPPPP`\06\80a\01&`\009`\00\F3[`\01\93\90\93\01\92a\00\BFV```@R\00\00"

define i32 @ff3

chriseth

> 2016/02/03 23:18:56.520211  length=32 from=0 to=31
 7b 22 69 64 22 3a 31 2c 22 6d 65 74 68 6f 64 22  {"id":1,"method"
 3a 22 72 70 63 5f 6d 6f 64 75 6c 65 73 22 7d 0a  :"rpc_modules"}.
--
< 2016/02/03 23:18:56.520604  length=134 from=0 to=133
 7b 22 65 72 72 6f 72 22 3a 7b 22 63 6f 64 65 22  {"error":{"code"
 3a 2d 33 32 36 30 30 2c 22 6d 65 73 73 61 67 65  :-32600,"message
 22 3a 22 49 4e 56 41 4c 49 44 5f 4a 53 4f 4e 5f  ":"INVALID_JSON_
 52 45 51 55 45 53 54 3a 20 54 68 65 20 4a 53 4f  REQUEST: The JSO
 4e 20 73 65 6e 74 20 69 73 20 6e 6f 74 20 61 20  N sent is not a 

chriseth

I0122 16:04:34.770502   29461 blockchain.go:1048] imported 191 receipt(s) (0 ignored) in 176.38277ms. #196800 [bd41370d… / 2383dfe8…]
I0122 16:04:34.891049   29461 blockchain.go:881] imported 192 header(s) (0 ignored) in 299.480358ms. #196992 [1f79eaec… / d4e5bddf…]
I0122 16:04:34.894795   29461 downloader.go:1118] Peer 8d8da6a5d75369fa [blocks 1253.54/s, receipts 932.03/s, states 0.00/s, lacking    0]: fetching 192 headers from #196993
I0122 16:04:34.900714   29461 downloader.go:1478] Peer 8d8da6a5d75369fa [blocks 1253.54/s, receipts 932.03/s, states 0.00/s, lacking    0]: requesting 45 receipt(s), first at #196805
I0122 16:04:34.906579   29461 downloader.go:1478] Peer 8d8da6a5d75369fa [blocks 1253.54/s, receipts 932.03/s, states 0.00/s, lacking    0]: requesting 55 body(s), first at #196805
I0122 16:04:34.907889   29461 downloader.go:1527] Inserting chain with 4 items (#196801 [1f79eaec…] - #196804 [80b2abc8…])
I0122 16:04:34.909395   29461 blockchain.go:1048] imported 4 receipt(s) (0 ignored) in 1.423602ms