amiller

pragma solidity ^0.5.0;

contract MyContract {
    // 0x83CC162a944afA8537DAaDec8f39C88E4B6c4E31   mainnet registry
    // mainnet resolver
    
    // 0x12a0083531C904fe4ac490DF231c2e4e4403dB60 ropsten registry
    // 0x12299799a50340FB860D276805E78550cBaD3De3 ropsten resolver
    ETHRegistrarController registrar = ETHRegistrarController(0x12a0083531C904fe4ac490DF231c2e4e4403dB60);
    BaseRegistrar base = BaseRegistrar(0x227Fcb6Ddf14880413EF4f1A3dF2Bbb32bcb29d7);

amiller

import json, sys
import subprocess
import requests
import time
import csv
import re

balances = {} # map addr => balance

# Parse the vote string

amiller

open import Data.Bool
open import Data.Empty
open import Data.Maybe
open import Data.Nat
open import Relation.Nullary 
open import Relation.Binary.PropositionalEquality
open import Data.Fin
open import Data.List
open import Data.Unit
open import Data.Sum hiding (map)

amiller

pragma solidity ^0.4.22;   
// ECE 398 SC - Smart Contracts and Blockchain Security 
// http://soc1024.ece.illinois.edu/teaching/ece398sc/spring2018/

// Simpest possible duplex-micropayment channel
// - Funded with an up front amount at initialization
// - The contract creator is called "alice". The other party, "bob", is passed
// as an argument to the Constructor
// - There is no fixed deadline, but instead any party can initiate a dispute,
// which lasts for a fixed time

amiller

pragma solidity ^0.4.22;

contract ECVerify {
    function ecrecovery(bytes32 hash, bytes sig) public pure returns (address) {
        bytes32 r;
        bytes32 s;
        uint8 v;

        if (sig.length != 65) {
            return 0;

amiller

(* Andrew Miller March 2014 
   Hash-value Highway - See also: https://bitcointalk.org/index.php?topic=98986 *)

open Merkle (* provides authtype *)

type tx = string
type block = Genesis | Blk of block authtype * block authtype * tx * int * int

(* Boiler plate for authenticated data structure parser 
   Indicates data structure definitions end here *)

amiller

import asyncio
import concurrent.futures
import logging
import time
import random

# Examples of running in executor
# https://docs.python.org/3/library/concurrent.futures.html#concurrent.futures.ThreadPoolExecutor
# https://pymotw.com/3/asyncio/executors.html

amiller

import asyncio
import concurrent.futures
import logging
import time
import cffi
import random

# Examples of running in executor
# https://docs.python.org/3/library/concurrent.futures.html#concurrent.futures.ThreadPoolExecutor
# https://pymotw.com/3/asyncio/executors.html

amiller

pragma solidity ^0.4.21;
// ECE 398 SC - Smart Contracts and Blockchain Security
// http://soc1024.ece.illinois.edu/teaching/ece398sc/spring2018/

contract SolidityChallenges {

    // 1. Simple syntax

    function arithmeticA(uint x) public pure returns(uint) {
        // The following fragment of code is a for-loop that assigns a value

amiller

Bitcoin provides Broadcast in a model where it's not clear otherwise how to get it.

Most distributed systems network models assume there is some kind of pre-established authenticated communication channel among a fixed set of participants, for example a PKI. Bitcoin is meant to work in a weaker model where there is no such assumption. Instead Bitcoin relies on a non-standard assumption about the allocation of computational resources - ignoring incentives for now, the assumption is that honest parties contribute more power in total than the adversary.

Some pre-established communication channel must still be assumed, just not an authenticated one. When formalizing Bitcoin things, I usually call it a "synchronous message diffusion" channel. Any honest party can publish a message, and that message is delivered to every other honest party within some time bound. A party that receives a message does not learn the identity of the sender (this essentially makes Sybil attacks possible). Additionally, the advers