Skip to content

Instantly share code, notes, and snippets.

@sarthakbagaria
Created July 28, 2018 18:27
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save sarthakbagaria/cbcaadd57e7c9a04e7452651b386715c to your computer and use it in GitHub Desktop.
Save sarthakbagaria/cbcaadd57e7c9a04e7452651b386715c to your computer and use it in GitHub Desktop.
A simple UTxO based blockchain ledger implementation with formally verified invariants.
#!/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) ]
@sarthakbagaria
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment