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 file is MIT Licensed.
//
// Copyright 2017 Christian Reitwiessner
// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF O

chriseth

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

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

chriseth

Answers to Deep Questions about Solidity

The following list of questions was taken from https://www.reddit.com/r/ethereum/comments/72reba/do_you_have_deep_questions_about_solidity_or_the/

An updated summary on the different ways one could have two contracts interact (DELEGATECALL, STATICCALL, libraries, all that stuff) with clear pros/cons for each (gas cost, whether it requires EVM assembly directives, etc)

Question by /u/drcode

I won't talk about low-level opcodes here because of the brevity of the answer. In general, there are four ways functions can be called in Solidity:

chriseth

// unmodified

contract Token {

    uint8 public decimals = 18;

    string public name;
    uint256 public lastTouched;
    address public hub;
    address public owner;

chriseth

/*******************************************************
 *                       WARNING                       *
 *  Solidity to Yul compilation is still EXPERIMENTAL  *
 *       It can result in LOSS OF FUNDS or worse       *
 *                !USE AT YOUR OWN RISK!               *
 *******************************************************/

object "ERC20_396" {
    code {
        {

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

// Adapted from  https://github.com/omgnetwork/plasma-contracts
// Licensed under Apache License 2.0
// SPDX-License-Identifier: Apache-2.0

export { Queue, insert, pop, min, defaultLessThanMemory, defaultLessThanStorage }

struct Queue<T> {
    T[] heap;
    function(T memory, T storage) internal view returns (bool) lessThanMemory;
    function(T storage, T storage) internal view returns (bool) lessThanStorage;

chriseth

contract BinarySearch {
  ///@why3
  /// requires { arg_data.length < UInt256.max_uint256 }
  /// requires { 0 <= to_int arg_begin <= to_int arg_end <= arg_data.length }
  /// requires { forall i j: int. 0 <= i <= j < arg_data.length -> to_int arg_data[i] <= to_int arg_data[j] }
  /// variant { to_int arg_end - to_int arg_begin }
  /// ensures {
  ///   to_int result < UInt256.max_uint256 -> (to_int arg_begin <= to_int result < to_int arg_end && to_int arg_data[to_int result] = to_int arg_value)
  /// }
  /// ensures {

chriseth

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