Skip to content

Instantly share code, notes, and snippets.

@chriseth
chriseth / BinarySearch.sol
Last active August 3, 2022 19:22
Verified binary search in sorted array
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 {
@patcon
patcon / INSTALL.md
Last active July 28, 2017 10:34
Installing why3 IDE for verifying sample Ethereum contract (Ubuntu 14.04)
# install ocaml and deps
apt-get install ocaml ocaml-native-compilers
apt-get install liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev libocamlgraph-ocaml-dev

# install opam from binaries (ocaml package manager)
# See https://opam.ocaml.org/doc/Install.html#Binarydistribution
wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin/

#### OR
@aaronjensen
aaronjensen / drain_stop.ex
Last active November 28, 2022 06:59
Phoenix Drain Stop
# ATTENTION: This is now supported in plug_cowboy as of 2.1.0:
# https://hexdocs.pm/plug_cowboy/Plug.Cowboy.Drainer.html
defmodule DrainStop do
@moduledoc """
DrainStop Attempts to gracefully shutdown an endpoint when a normal shutdown
occurs. It first shuts down the acceptor, ensuring that no new requests can be
made. It then waits for all pending requests to complete. If the timeout
expires before this happens, it stops waiting, allowing the supervision tree
to continue its shutdown order.
@chriseth
chriseth / 0 README.md
Last active November 6, 2022 19:55
Formal verification for re-entrant Solidity contracts

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

@bitwalker
bitwalker / config.ex
Created July 19, 2016 23:00
Useful config wrapper for Elixir
defmodule Config do
@moduledoc """
This module handles fetching values from the config with some additional niceties
"""
@doc """
Fetches a value from the config, or from the environment if {:system, "VAR"}
is provided.
An optional default value can be provided if desired.