chriseth

Solidity Assembly

This assembly language tries to achieve several goals:

Programs written in it should be readable, even if the code is generated by a compiler from Solidity.
The translation from assembly to bytecode should contain as few “surprises” as possible.
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.

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:

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

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.



	bool ExpresionCompiler::visit(BinaryExpression const& _expr)
	{
	// noteResult returns the julia-equivalent of the expression.
	// it also inserts a comment containing the source location of _expr
	// Anything inside angle brackets is looked up in the table passed
	// as third argument and a plain string replacement is performed.
	// The convert function calls visit recursively (or instanciates a
	// new AST walker) and returns what was supplied to "noteResult".

	{
	// Some elementary helpers ---------------------------------------

	function memptr() -> addr
	{
	addr := 0x40
	}
	function allocate(size) -> addr
	{
	addr := mload(memptr())

	pragma solidity ^0.4.0;

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

	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.

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

	; 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