Provably Correct Smart Contracts using DeepSEA

Daniel Britten

Ethereum Engineering Group Meetup 2023

It's great to be here...

Overall Goal: Demonstate a technique for showing the correctness of smart contracts

Overview:

Theorem-proving example in the proof assistant Coq
DeepSEA by example
Modelling a blockchain
Handling reentrancy
A correctness property of a Crowdfunding contract

Introduction to theorem-proving in Coq

Example: Even and odd numbers

Definition Even (n : nat) := exists k, n = 2 * k.
Definition Odd  (m : nat) := exists l, m = 2 * l + 1.

Lemma EvenToOdd : forall (n : nat), Even n -> Odd (n + 1).forall n : nat, Even n -> Odd (n + 1)
Proof.forall n : nat, Even n -> Odd (n + 1)
  intros.n: nat
H: Even n
Odd (n + 1)
  unfold Even in H.n: nat
H: exists k : nat, n = 2 * k
Odd (n + 1)
  destruct H as [k].n, k: nat
H: n = 2 * k
Odd (n + 1)
  unfold Odd.n, k: nat
H: n = 2 * k
exists l : nat, n + 1 = 2 * l + 1
  exists k.n, k: nat
H: n = 2 * k
n + 1 = 2 * k + 1
  rewrite <- H.n, k: nat
H: n = 2 * k
n + 1 = n + 1
  reflexivity.
Qed.

DeepSEA

Introduction to creating a DeepSEA smart contract

Example: Trivial contract converting bool to int

object signature trivial = {
    const boolToInt : bool -> int;
    boolToIntTracker : bool -> int
}

object Trivial : trivial {
    let seenTrueYet : bool := false

    let boolToInt b =
      if b then 1 else 0

    let boolToIntTracker b =
      if b then
        begin
            seenTrueYet := true;
            1
        end
      else 0
}

layer CONTRACT = { o = Trivial }

$ dsc trivial.ds bytecode
5b60005b60206109205101610920525b61022660006020610920510301525b60006020
610920510301516101005260206101002060006020610920510301525b600060006020
61092051030151555b60206109205103610920525b60005b9050386300000073600039
386000f35b60006000fd5b610940610920527c01000000000000000000000000000000
000000000000000000000000006000350480635192f3c01463000000495780631e01e7
071463000000965760006000fd5b6004355b60006109205101610920525b8063000000
67576300000085565b600190505b60006109205103610920525b805b90506000526020
6000f35b60009050630000006c565b60006000fd5b6004355b60206109205101610920
525b8063000000b4576300000111565b61022660006020610920510301525b60006020
610920510301516101005260206101002060006020610920510301525b600160006020
61092051030151555b600190505b60206109205103610920525b805b90506000526020
6000f35b6000905063000000f8565b60006000fd

$ dsc trivial.ds abi

[ {"type":"constructor",
  "name":"constructor",
  "inputs":[], "outputs":[], "payable":false,
  "constant":false, "stateMutability":"nonpayable"},
{"type":"function",
  "name":"boolToInt",
  "inputs":[{"name":"b", "type":"bool"}],
  "outputs":[{"name":"", "type":"uint256"}],
  "payable":false,
  "constant":true,
  "stateMutability":"view"},
{"type":"function",
  "name":"boolToIntTracker",
  "inputs":[{"name":"b", "type":"bool"}],
  "outputs":[{"name":"", "type":"uint256"}],
  "payable":true,
  "constant":false,
  "stateMutability":"payable"}]

Next slide is a reminder of the contract definition.

object signature trivial = {
  const boolToInt : bool -> int
}

object Trivial : trivial {
    let boolToInt b = if b then 1 else 0
}

layer CONTRACT  = {
    o = Trivial
}

Print Trivial_boolToInt_opt.Trivial_boolToInt_opt = 
fun (memModelOps : MemoryModelOps mem) (f : bool)
  (_ : machine_env GetHighData) => if f then ret 1 else ret 0
     : forall memModelOps : MemoryModelOps mem,
       bool -> machine_env GetHighData -> Syntax.DS Z32

Arguments Trivial_boolToInt_opt {memModelOps} _%bool_scope _

Print Trivial_boolToIntTracker_opt.Trivial_boolToIntTracker_opt = 
fun (memModelOps : MemoryModelOps mem) (f : bool)
  (_ : machine_env GetHighData) =>
if f
then MonadState.modify (update_Trivial_seenTrueYet true);; ret 1
else ret 0
     : forall memModelOps : MemoryModelOps mem,
       bool -> machine_env GetHighData -> Syntax.DS Z32

Arguments Trivial_boolToIntTracker_opt {memModelOps} _%bool_scope _

Refinement and the Lem EVM model

Modelling a Blockchain using Coq

Reentrancy

A Crowdfunding Correctness Property

References

Slides powered by Alectryon: github.com/cpitclaudel/alectryon
The DeepSEA compiler is partly based upon the CompCert Verified Compiler.

Additional Slides

Example: a property of a list membership function

Inductive list (A : Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.

Fixpoint contains (n:nat) (l:list nat) : bool :=
  match l with
  | [] => false
  | h :: tl => (n =? h) || contains n tl
end.

Lemma contains_property :
  forall n list1, contains n list1 = true
    -> forall list2, contains n (list1 ++ list2) = true.forall (n : nat) (list1 : list nat),
contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
Proof.forall (n : nat) (list1 : list nat),
contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
  intros n.n: nat
forall list1 : list nat,
contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
  induction list1.n: nat
contains n [] = true ->
forall list2 : list nat, contains n ([] ++ list2) = true
n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
contains n (a :: list1) = true ->
forall list2 : list nat, contains n ((a :: list1) ++ list2) = true
  -n: nat
contains n [] = true ->
forall list2 : list nat, contains n ([] ++ list2) = true simpl.n: nat
false = true -> forall list2 : list nat, contains n list2 = true intros.n: nat
H: false = true
list2: list nat
contains n list2 = true discriminate.
  -n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
contains n (a :: list1) = true ->
forall list2 : list nat, contains n ((a :: list1) ++ list2) = true intros.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: contains n (a :: list1) = true
list2: list nat
contains n ((a :: list1) ++ list2) = true simpl in *.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: (n =? a) || contains n list1 = true
list2: list nat
(n =? a) || contains n (list1 ++ list2) = true
    apply orb_prop in H.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: (n =? a) = true \/ contains n list1 = true
list2: list nat
(n =? a) || contains n (list1 ++ list2) = true
    destruct H.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: (n =? a) = true
list2: list nat
(n =? a) || contains n (list1 ++ list2) = true
n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: contains n list1 = true
list2: list nat
(n =? a) || contains n (list1 ++ list2) = true
    +n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: (n =? a) = true
list2: list nat
(n =? a) || contains n (list1 ++ list2) = true apply orb_true_intro.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: (n =? a) = true
list2: list nat
(n =? a) = true \/ contains n (list1 ++ list2) = true
      left.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: (n =? a) = true
list2: list nat
(n =? a) = true assumption.
    +n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: contains n list1 = true
list2: list nat
(n =? a) || contains n (list1 ++ list2) = true apply orb_true_intro.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: contains n list1 = true
list2: list nat
(n =? a) = true \/ contains n (list1 ++ list2) = true
      right.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
H: contains n list1 = true
list2: list nat
contains n (list1 ++ list2) = true
      eapply IHlist1 in H.n, a: nat
list1: list nat
IHlist1: contains n list1 = true ->
forall list2 : list nat, contains n (list1 ++ list2) = true
list2: list nat
H: contains n (list1 ++ ?list2) = true
contains n (list1 ++ list2) = true
      eassumption.
Qed.

Lemma contains_correctness : forall n l, contains n l = true <-> In n l.forall (n : nat) (l : list nat), contains n l = true <-> In n l
Proof.forall (n : nat) (l : list nat), contains n l = true <-> In n l
  Print In.In = 
fun A : Type =>
fix In (a : A) (l : list A) {struct l} : Prop :=
  match l with
  | [] => False
  | b :: m => b = a \/ In a m
  end
     : forall A : Type, A -> list A -> Prop

Arguments In [A]%type_scope _ _%list_scope
forall (n : nat) (l : list nat), contains n l = true <-> In n l
  split.n: nat
l: list nat
contains n l = true -> In n l
n: nat
l: list nat
In n l -> contains n l = true
  -n: nat
l: list nat
contains n l = true -> In n l induction l as [|l'].n: nat
contains n [] = true -> In n []
n, l': nat
l: list nat
IHl: contains n l = true -> In n l
contains n (l' :: l) = true -> In n (l' :: l)
    +n: nat
contains n [] = true -> In n [] simpl.n: nat
false = true -> False discriminate.
    +n, l': nat
l: list nat
IHl: contains n l = true -> In n l
contains n (l' :: l) = true -> In n (l' :: l) simpl.n, l': nat
l: list nat
IHl: contains n l = true -> In n l
(n =? l') || contains n l = true -> l' = n \/ In n l intros.n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: (n =? l') || contains n l = true
l' = n \/ In n l
      apply orb_prop in H.n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: (n =? l') = true \/ contains n l = true
l' = n \/ In n l
      destruct H.n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: (n =? l') = true
l' = n \/ In n l
n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: contains n l = true
l' = n \/ In n l
      *n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: (n =? l') = true
l' = n \/ In n l left.n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: (n =? l') = true
l' = n rewrite Nat.eqb_eq in H.n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: n = l'
l' = n auto.
      *n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: contains n l = true
l' = n \/ In n l right.n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: contains n l = true
In n l apply IHl in H.n, l': nat
l: list nat
IHl: contains n l = true -> In n l
H: In n l
In n l assumption.
  -n: nat
l: list nat
In n l -> contains n l = true induction l as [|l'].n: nat
In n [] -> contains n [] = true
n, l': nat
l: list nat
IHl: In n l -> contains n l = true
In n (l' :: l) -> contains n (l' :: l) = true
    +n: nat
In n [] -> contains n [] = true simpl.n: nat
False -> false = true contradiction.
    +n, l': nat
l: list nat
IHl: In n l -> contains n l = true
In n (l' :: l) -> contains n (l' :: l) = true simpl.n, l': nat
l: list nat
IHl: In n l -> contains n l = true
l' = n \/ In n l -> (n =? l') || contains n l = true intros.n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: l' = n \/ In n l
(n =? l') || contains n l = true
      destruct H.n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: l' = n
(n =? l') || contains n l = true
n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: In n l
(n =? l') || contains n l = true
      *n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: l' = n
(n =? l') || contains n l = true apply orb_true_intro.n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: l' = n
(n =? l') = true \/ contains n l = true
        left.n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: l' = n
(n =? l') = true
        subst.n: nat
l: list nat
IHl: In n l -> contains n l = true
(n =? n) = true
        apply Nat.eqb_refl.
      *n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: In n l
(n =? l') || contains n l = true apply orb_true_intro.n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: In n l
(n =? l') = true \/ contains n l = true
        right.n, l': nat
l: list nat
IHl: In n l -> contains n l = true
H: In n l
contains n l = true
        auto.
Qed.

Example: Simple state machine

Inductive State :=
  | initial
  | middle
  | extra
  | final
.

Inductive Transition (before : State) :=
  | advance (prf : before <> final)
  | sidetrack (prf : before = initial).

Program Definition step (s : State) (t : Transition s) :=
  match t with
  | advance _ =>
    match s with
    | initial => middle
    | middle => final
    | extra => middle
    | final => _
    end
  | sidetrack _ =>
    match s with
    | initial => extra
    | _ => _
    end
end.

Next Obligation.forall (s : State) (t : Transition s) (wildcard' : s <> final),
advance s wildcard' = t -> final = s -> State
intros.s: State
t: Transition s
wildcard': s <> final
Heq_t: advance s wildcard' = t
Heq_s: final = s
State
exfalso.s: State
t: Transition s
wildcard': s <> final
Heq_t: advance s wildcard' = t
Heq_s: final = s
False
subst.wildcard': final <> final
False
contradiction.
Defined.
Next Obligation.forall (s : State) (t : Transition s) (wildcard'0 : s = initial),
sidetrack s wildcard'0 = t ->
forall wildcard' : State,
initial <> wildcard' -> wildcard' = s -> State
intros.s: State
t: Transition s
wildcard'0: s = initial
Heq_t: sidetrack s wildcard'0 = t
wildcard': State
H: initial <> wildcard'
Heq_s: wildcard' = s
State
exfalso.s: State
t: Transition s
wildcard'0: s = initial
Heq_t: sidetrack s wildcard'0 = t
wildcard': State
H: initial <> wildcard'
Heq_s: wildcard' = s
False
subst.H: initial <> initial
False
contradiction.
Defined.

Local Obligation Tactic := try discriminate. (* Used for the above. *)

Lemma three_transitions_gives_final :
forall t1 t2 t3, let s1 := step initial t1 in let s2 := step s1 t2 in
  step s2 t3 = final.forall (t1 : Transition initial) (t2 : Transition (step initial t1))
  (t3 : Transition (step (step initial t1) t2)),
let s1 := step initial t1 in
let s2 := step s1 t2 in step s2 t3 = final
Proof.forall (t1 : Transition initial) (t2 : Transition (step initial t1))
  (t3 : Transition (step (step initial t1) t2)),
let s1 := step initial t1 in
let s2 := step s1 t2 in step s2 t3 = final
intros.t1: Transition initial
t2: Transition (step initial t1)
t3: Transition (step (step initial t1) t2)
s1:= step initial t1: State
s2:= step s1 t2: State
step s2 t3 = final
destruct t1.prf: initial <> final
t2: Transition (step initial (advance initial prf))
t3: Transition (step (step initial (advance initial prf)) t2)
s1:= step initial (advance initial prf): State
s2:= step s1 t2: State
step s2 t3 = final
prf: initial = initial
t2: Transition (step initial (sidetrack initial prf))
t3: Transition (step (step initial (sidetrack initial prf)) t2)
s1:= step initial (sidetrack initial prf): State
s2:= step s1 t2: State
step s2 t3 = final simpl in *.prf: initial <> final
t2: Transition middle
t3: Transition (step middle t2)
s1:= middle: State
s2:= step s1 t2: State
step s2 t3 = final
prf: initial = initial
t2: Transition (step initial (sidetrack initial prf))
t3: Transition (step (step initial (sidetrack initial prf)) t2)
s1:= step initial (sidetrack initial prf): State
s2:= step s1 t2: State
step s2 t3 = final
  -prf: initial <> final
t2: Transition middle
t3: Transition (step middle t2)
s1:= middle: State
s2:= step s1 t2: State
step s2 t3 = final destruct t2.prf: initial <> final
prf0: middle <> final
t3: Transition (step middle (advance middle prf0))
s1:= middle: State
s2:= step s1 (advance middle prf0): State
step s2 t3 = final
prf: initial <> final
prf0: middle = initial
t3: Transition (step middle (sidetrack middle prf0))
s1:= middle: State
s2:= step s1 (sidetrack middle prf0): State
step s2 t3 = final simpl in *.prf: initial <> final
prf0: middle <> final
t3: Transition final
s1:= middle: State
s2:= final: State
step s2 t3 = final
prf: initial <> final
prf0: middle = initial
t3: Transition (step middle (sidetrack middle prf0))
s1:= middle: State
s2:= step s1 (sidetrack middle prf0): State
step s2 t3 = final
    +prf: initial <> final
prf0: middle <> final
t3: Transition final
s1:= middle: State
s2:= final: State
step s2 t3 = final destruct t3.prf: initial <> final
prf0: middle <> final
prf1: final <> final
s1:= middle: State
s2:= final: State
step s2 (advance final prf1) = final
prf: initial <> final
prf0: middle <> final
prf1: final = initial
s1:= middle: State
s2:= final: State
step s2 (sidetrack final prf1) = final
      *prf: initial <> final
prf0: middle <> final
prf1: final <> final
s1:= middle: State
s2:= final: State
step s2 (advance final prf1) = final contradiction.
      *prf: initial <> final
prf0: middle <> final
prf1: final = initial
s1:= middle: State
s2:= final: State
step s2 (sidetrack final prf1) = final discriminate.
    +prf: initial <> final
prf0: middle = initial
t3: Transition (step middle (sidetrack middle prf0))
s1:= middle: State
s2:= step s1 (sidetrack middle prf0): State
step s2 t3 = final discriminate.
  -prf: initial = initial
t2: Transition (step initial (sidetrack initial prf))
t3: Transition (step (step initial (sidetrack initial prf)) t2)
s1:= step initial (sidetrack initial prf): State
s2:= step s1 t2: State
step s2 t3 = final destruct t2.prf: initial = initial
prf0: step initial (sidetrack initial prf) <> final
t3: Transition
  (step (step initial (sidetrack initial prf))
     (advance (step initial (sidetrack initial prf)) prf0))
s1:= step initial (sidetrack initial prf): State
s2:= step s1 (advance (step initial (sidetrack initial prf)) prf0): State
step s2 t3 = final
prf: initial = initial
prf0: step initial (sidetrack initial prf) = initial
t3: Transition
  (step (step initial (sidetrack initial prf))
     (sidetrack (step initial (sidetrack initial prf)) prf0))
s1:= step initial (sidetrack initial prf): State
s2:= step s1 (sidetrack (step initial (sidetrack initial prf)) prf0): State
step s2 t3 = final simpl in *.prf: initial = initial
prf0: extra <> final
t3: Transition middle
s1:= extra: State
s2:= middle: State
step s2 t3 = final
prf: initial = initial
prf0: step initial (sidetrack initial prf) = initial
t3: Transition
  (step (step initial (sidetrack initial prf))
     (sidetrack (step initial (sidetrack initial prf)) prf0))
s1:= step initial (sidetrack initial prf): State
s2:= step s1 (sidetrack (step initial (sidetrack initial prf)) prf0): State
step s2 t3 = final
    +prf: initial = initial
prf0: extra <> final
t3: Transition middle
s1:= extra: State
s2:= middle: State
step s2 t3 = final destruct t3.prf: initial = initial
prf0: extra <> final
prf1: middle <> final
s1:= extra: State
s2:= middle: State
step s2 (advance middle prf1) = final
prf: initial = initial
prf0: extra <> final
prf1: middle = initial
s1:= extra: State
s2:= middle: State
step s2 (sidetrack middle prf1) = final simpl in *.prf: initial = initial
prf0: extra <> final
prf1: middle <> final
s1:= extra: State
s2:= middle: State
final = final
prf: initial = initial
prf0: extra <> final
prf1: middle = initial
s1:= extra: State
s2:= middle: State
step s2 (sidetrack middle prf1) = final
      *prf: initial = initial
prf0: extra <> final
prf1: middle <> final
s1:= extra: State
s2:= middle: State
final = final reflexivity.
      *prf: initial = initial
prf0: extra <> final
prf1: middle = initial
s1:= extra: State
s2:= middle: State
step s2 (sidetrack middle prf1) = final discriminate.
    +prf: initial = initial
prf0: step initial (sidetrack initial prf) = initial
t3: Transition
  (step (step initial (sidetrack initial prf))
     (sidetrack (step initial (sidetrack initial prf)) prf0))
s1:= step initial (sidetrack initial prf): State
s2:= step s1 (sidetrack (step initial (sidetrack initial prf)) prf0): State
step s2 t3 = final discriminate.
Qed.