Created
July 28, 2018 18:27
-
-
Save sarthakbagaria/cbcaadd57e7c9a04e7452651b386715c to your computer and use it in GitHub Desktop.
A simple UTxO based blockchain ledger implementation with formally verified invariants.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env stack | |
-- stack --resolver lts-11.6 script --package containers | |
module Blockchain where | |
import Data.Set (Set) | |
import qualified Data.Set as Set | |
-- refining just to get measures from data constructors | |
{-@ data Tx = Tx { tI :: Set Inp, tO :: [Out] } @-} | |
data Tx = Tx { tI :: Set Inp, tO :: [Out] } deriving (Eq,Ord,Show) | |
-- Input sets of two Txs should always be disjoint. | |
-- We don't verify that property here. | |
data Ledger = Ledger { ledger :: [Tx] } | |
{-@ measure llen @-} | |
llen :: [a] -> Int | |
llen [] = 0 | |
llen (x:xs) = 1 + (llen xs) | |
-- connect llen to LH's len | |
{-@ llen :: xs:[a] -> { v:Int | v == len xs } @-} | |
{- Transaction index in Inp must always be within the bounds of out list of transaction in Input -} | |
{-@ type Nat = { v:Int | v >= 0 } @-} | |
{-@ type TxOutBound Tx = { v:Nat | v < (llen (tO Tx)) } @-} | |
{-@ data Inp = Inp { iTx :: Tx, iTxInd :: TxOutBound iTx } @-} | |
data Inp = Inp { iTx :: Tx, iTxInd :: Int } deriving (Eq,Ord,Show) | |
{- refining just to get measures from data constructors -} | |
{-@ data Out = Out { oAddr :: Address, oCoin :: Coin } @-} | |
data Out = Out { oAddr :: Address, oCoin :: Coin } deriving (Eq,Ord,Show) | |
data Coin = Coin Int deriving (Eq,Ord,Show) | |
data Address = Addr String deriving (Eq,Ord,Show) | |
instance Num Coin where | |
(Coin x) + (Coin y) = Coin (x+y) | |
(Coin x) * (Coin y) = Coin (x*y) | |
abs (Coin x) = Coin (abs x) | |
signum (Coin x) = signum (Coin x) | |
fromInteger x = Coin (fromInteger x) | |
negate (Coin x) = Coin (negate x) | |
------------------------------------------------------------ | |
-- UTxO (Unspent transactions) | |
------------------------------------------------------------ | |
-- A single element map from an input to an output | |
{-@ data InpOutPair = InpOutPair { ioPairInp :: Inp, ioPairOut :: Out } @-} | |
data InpOutPair = InpOutPair { ioPairInp :: Inp, ioPairOut :: Out } deriving (Eq,Ord,Show) | |
{-@ type InpOutPairExcluding InpOutPair = { v:InpOutPair | v != InpOutPair } @-} | |
{-@ autosize UTxO @-} | |
-- A finite map from inputs to outputs | |
-- We require that the inputs in UTxO are unique for it to be | |
-- a well defined map | |
{-@ data UTxO = NoUTxO | |
| UTxO { hd :: InpOutPairExcluding utxoInps, tl :: UTxO } | |
@-} | |
data UTxO = NoUTxO | |
| UTxO { hd :: InpOutPair, tl :: UTxO } deriving Show | |
-- Set of all inputs in a given UTxO | |
{-@ measure utxoInps @-} | |
utxoInps :: UTxO -> Set Inp | |
utxoInps NoUTxO = Set.empty | |
utxoInps (UTxO io xs) = Set.singleton (ioPairInp io) `Set.union` (utxoInps xs) | |
-- Set of all transactions in inputs in a given UTxO | |
{-@ measure utxoInpTxs @-} | |
utxoInpTxs :: UTxO -> Set Tx | |
utxoInpTxs NoUTxO = Set.empty | |
utxoInpTxs (UTxO io xs) = Set.singleton (iTx (ioPairInp io)) `Set.union` (utxoInpTxs xs) | |
-- Set of all outputs in a given UTxO | |
utxoOuts :: UTxO -> Set Out | |
utxoOuts NoUTxO = Set.empty | |
utxoOuts (UTxO io xs) = Set.singleton (ioPairOut io) `Set.union` (utxoOuts xs) | |
-- TODO : teach LH utxoInp a < utxoInp b => utxoInpTxs a < utxoInpTxs b | |
-- so that we don't have to write both conditions in the operators below | |
-- UTxO restricted to a given input set | |
{-@ (⊲) :: x:Set Inp -> y:UTxO | |
-> { z:UTxO | (Set_sub (utxoAddrs z) (utxoAddrs y)) && | |
(Set_sub (utxoInps z) (utxoInps y)) && | |
(Set_sub (utxoInpTxs z) (utxoInpTxs y)) && | |
(Set_sub (utxoInps z) x) | |
} | |
@-} | |
(⊲) :: Set Inp -> UTxO -> UTxO | |
ins ⊲ NoUTxO = NoUTxO | |
ins ⊲ (UTxO x xs) | |
|(ioPairInp x) `Set.member` ins = UTxO x (ins ⊲ xs) | |
|otherwise = ins ⊲ xs | |
-- UTxO restricted to the complement of a given input set | |
{-@ (⊲/) :: x:Set Inp -> y:UTxO | |
-> { z:UTxO | (Set_sub (utxoAddrs z) (utxoAddrs y)) && | |
(Set_sub (utxoInps z) (utxoInps y)) && | |
(Set_sub (utxoInpTxs z) (utxoInpTxs y)) && | |
(Set_emp (Set_cap (utxoInps z) x)) | |
} | |
@-} | |
(⊲/) :: Set Inp -> UTxO -> UTxO | |
ins ⊲/ NoUTxO = NoUTxO | |
ins ⊲/ (UTxO x xs) | |
|(ioPairInp x) `Set.member` ins = ins ⊲/ xs | |
|otherwise = UTxO x (ins ⊲/ xs) | |
-- UTxO restricted to a given address set | |
{-@ (⊳) :: x:UTxO -> y:Set Address | |
-> { z:UTxO | (Set_sub (utxoAddrs z) (Set_cap (utxoAddrs x) y)) && | |
(Set_sub (utxoInps z) (utxoInps x)) && | |
(Set_sub (utxoInpTxs z) (utxoInpTxs x)) | |
} | |
@-} | |
(⊳) :: UTxO -> Set Address -> UTxO | |
NoUTxO ⊳ addrs = NoUTxO | |
(UTxO x xs) ⊳ addrs | |
|(oAddr (ioPairOut x)) `Set.member` addrs = UTxO x (xs ⊳ addrs) | |
|otherwise = (xs ⊳ addrs) | |
-- Combine two UTxO | |
-- This function requires the input tx sets of two UTxO to be dijoint | |
{-@ addUTxO :: x:UTxO -> { y:UTxO | Set_emp (Set_cap (utxoInpTxs x) (utxoInpTxs y)) } | |
-> { z:UTxO | (Set_sub (utxoAddrs z) (Set_cup (utxoAddrs x) (utxoAddrs y))) && | |
(Set_sub (utxoInpTxs z) (Set_cup (utxoInpTxs x) (utxoInpTxs y))) | |
} | |
@-} | |
addUTxO :: UTxO -> UTxO -> UTxO | |
addUTxO NoUTxO ys = ys | |
addUTxO (UTxO x xs) ys = UTxO x (addUTxO xs ys) | |
-- UTxO from one single transaction | |
-- Essentially a map (tx,i) -> (tO tx) !! i | |
{-@ txOuts :: x:Tx -> { y:UTxO | Set_sub (utxoInpTxs y) (Set_sng x) } @-} | |
txOuts :: Tx -> UTxO | |
txOuts tx@(Tx _ tOutputs) = go tx (tO tx) | |
where | |
-- go takes a transaction and the remaining list of outputs | |
-- from the transaction to put in the UTxO | |
{-@ go :: x:Tx -> { y:[Out] | (llen (tO x)) >= llen y } | |
-> { z:UTxO | Set_sub (utxoInpTxs z) (Set_sng x) } | |
@-} | |
go tx [] = NoUTxO | |
go tx (x:xs) = | |
UTxO | |
(InpOutPair (Inp tx n) x) | |
(go tx xs) | |
where | |
-- n is the index of the output x | |
-- in the output list of transaction tx | |
n = (llen (tO tx)) - (llen (x:xs)) | |
{-@ measure utxoAddrs @-} | |
utxoAddrs :: UTxO -> Set Address | |
utxoAddrs NoUTxO = Set.empty | |
utxoAddrs (UTxO iop xs) = Set.singleton (oAddr (ioPairOut iop)) `Set.union` (utxoAddrs xs) | |
------------------------------------------------------------ | |
-- Wallet | |
------------------------------------------------------------ | |
------------------------------------------------------------ | |
-- A wallet belongs to a set of addresses and | |
-- contains unspent trasactions ending in those addresses | |
------------------------------------------------------------ | |
{-@ type RestrictedUTxO Addrs = { v:UTxO | Set_sub (utxoAddrs v) Addrs } @-} | |
{-@ data Wallet = Wallet { walletOwners :: Set Address, walletUTxO :: RestrictedUTxO walletOwners } @-} | |
data Wallet = Wallet { walletOwners :: Set Address, walletUTxO :: UTxO } | |
-- Update wallet after a transaction | |
-- This function requires that the transaction is not already | |
-- in the input tx set of wallet UTxO | |
{-@ apply :: x:Tx -> { y:Wallet | not (Set_mem x (utxoInpTxs (walletUTxO y))) } | |
-> { z:Wallet | walletOwners z == walletOwners y } | |
@-} | |
apply :: Tx -> Wallet -> Wallet | |
apply tx (Wallet owners utxo) = Wallet owners utxoFinal | |
where | |
utxoNotUsed = tI tx ⊲/ utxo | |
utxoNew = txOuts tx ⊳ owners | |
utxoFinal = addUTxO utxoNotUsed utxoNew | |
------------------------------------------------------------ | |
-- The complexity of finding the total coins in wallet | |
-- is linear in the size of the UTXO map | |
-- i.e. number of inputs/outputs in the finite map | |
------------------------------------------------------------ | |
{-@ measure utxoCoins @-} | |
utxoCoins :: UTxO -> Coin | |
utxoCoins NoUTxO = Coin 0 | |
utxoCoins (UTxO iop xs) = (oCoin (ioPairOut iop)) + (utxoCoins xs) | |
------------------------------------------------------------ | |
-- Wallet with coin balance cache | |
-- An invariant in wallet with cached coins is the | |
-- property that sum of coins in wallet UTxO should | |
-- always be equal to the wallet coin balance cache | |
------------------------------------------------------------ | |
{-@ type UTxOCoins UTxO = { v:Coin | v == utxoCoins UTxO } @-} | |
{-@ data CWallet = CWallet { cWalletOwners :: Set Address, cWalletUTxO :: RestrictedUTxO cWalletOwners, cWalletCoins :: UTxOCoins cWalletUTxO } @-} | |
data CWallet = CWallet { cWalletOwners :: Set Address, cWalletUTxO :: UTxO, cWalletCoins :: Coin } deriving Show | |
------------------------------------------------------------ | |
-- Update CWallet after a transaction | |
-- This function requires that the transaction is not already | |
-- in the input tx set of wallet UTxO | |
------------------------------------------------------------ | |
{-@ cApply :: x:Tx -> { y:CWallet | not (Set_mem x (utxoInpTxs (cWalletUTxO y))) } | |
-> { z:CWallet | (cWalletOwners z == cWalletOwners y) && | |
(Set_sub (utxoInpTxs (cWalletUTxO z)) (Set_cup (utxoInpTxs (cWalletUTxO y)) (Set.singleton x))) | |
} | |
@-} | |
cApply :: Tx -> CWallet -> CWallet | |
cApply tx (CWallet owners utxo coins) = CWallet owners utxoFinal newCoins | |
where | |
utxoNotUsed = tI tx ⊲/ utxo | |
utxoNew = txOuts tx ⊳ owners | |
utxoFinal = addUTxO utxoNotUsed utxoNew | |
newCoins = utxoCoins utxoFinal | |
------------------------------------------------------------ | |
-- Print coin balance of address "a0" in an | |
-- example wallet | |
------------------------------------------------------------ | |
main :: IO () | |
main = print $ cWalletCoins $ | |
cApply t4 $ cApply t3 $cApply t2 $ cApply t1 $ cApply t0 $ | |
CWallet (Set.singleton $ Addr "a0") NoUTxO (Coin 0) | |
where | |
t0 = Tx Set.empty | |
[ Out (Addr "a0") (Coin 1000) ] | |
t1 = Tx (Set.singleton $ Inp t0 0) | |
[ Out (Addr "a1") (Coin 50), Out (Addr "a0") (Coin 950) ] | |
t2 = Tx (Set.singleton $ Inp t1 0 ) | |
[ Out (Addr "a2") (Coin 50) ] | |
t3 = Tx (Set.singleton $ Inp t1 1) | |
[ Out (Addr "a1") (Coin 90), Out (Addr "a2") (Coin 10), Out (Addr "a0") (Coin 850) ] | |
t4 = Tx (Set.fromList [Inp t2 0, Inp t3 1]) | |
[ Out (Addr "a0") (Coin 60) ] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
A script to demonstrate formal verification of ledger invariants using Liquid Haskell. Details of the specification can be found on this blog post and this paper.
For simply running the script to check the example wallet balance, install Haskell stack and execute the script.
For running formal verification on this module, install Liquid Haskell and pass this script to the Liquid Haskell executable. For example, if built Liquid Haskell using stack, you may run:
stack exec -- liquid utxo-blockchain.hs