Provably Correct Smart Contracts

Daniel Britten

Software Innovation New Zealand Workshop 2023

It's great to be here...

The talks are about 5 minutes long. - Contract owner example

Definition setMessage (msg : String.string)
                      (callInfo : machine_environment)
                      : DS unit :=
  owner <- gets owner;;
  if (owner =? (caller callInfo))
    then puts (update_message msg)
    else fail.

Definition getMessage (callInfo : machine_environment)
                      : DS string :=
  message <- gets message;;
  ret message.

Definition changeOwner (new_owner : nat)
                       (callInfo : machine_environment)
                       : DS unit :=
  owner <- gets owner;;
  if (owner =? (caller callInfo))
    then
      puts (update_owner new_owner)
    else fail.

Lemma differentMessageImpliesOwnerIsCaller :
  forall msg callInfo stOld result stNew,
    (setMessage msg callInfo stOld = Some (result, stNew)
      /\ message stNew <> message stOld)
    -> caller callInfo = owner stOld.forall (msg : string) (callInfo : machine_environment)
  (stOld : message_board_storage_type) (result : unit)
  (stNew : message_board_storage_type),
setMessage msg callInfo stOld = Some (result, stNew) /\
message stNew <> message stOld -> caller callInfo = owner stOld
Proof.forall (msg : string) (callInfo : machine_environment)
  (stOld : message_board_storage_type) (result : unit)
  (stNew : message_board_storage_type),
setMessage msg callInfo stOld = Some (result, stNew) /\
message stNew <> message stOld -> caller callInfo = owner stOld
intros.msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H: setMessage msg callInfo stOld = Some (result, stNew) /\
message stNew <> message stOld
caller callInfo = owner stOld
destruct (setMessage msg callInfo stOld) as [r'|stNew'] eqn:Def;
destruct H; inversion H; subst.Unused introduction pattern: r' [unused-intro-pattern,tactics]
msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H: Some (result, stNew) = Some (result, stNew)
Def: setMessage msg callInfo stOld = Some (result, stNew)
H0: message stNew <> message stOld
caller callInfo = owner stOld clear H.msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
Def: setMessage msg callInfo stOld = Some (result, stNew)
H0: message stNew <> message stOld
caller callInfo = owner stOld
unfold setMessage in Def.msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
Def: (owner <- gets owner;;
 (if owner =? caller callInfo
  then puts (update_message msg)
  else fail)) stOld = Some (result, stNew)
H0: message stNew <> message stOld
caller callInfo = owner stOld
inversion Def; clear Def.msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H0: message stNew <> message stOld
H1: (if owner stOld =? caller callInfo
 then puts (update_message msg)
 else fail) stOld = Some (result, stNew)
caller callInfo = owner stOld
destruct (owner stOld =? caller callInfo) eqn:SCase.msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H0: message stNew <> message stOld
SCase: (owner stOld =? caller callInfo) = true
H1: puts (update_message msg) stOld = Some (result, stNew)
caller callInfo = owner stOld
msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H0: message stNew <> message stOld
SCase: (owner stOld =? caller callInfo) = false
H1: fail stOld = Some (result, stNew)
caller callInfo = owner stOld
-msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H0: message stNew <> message stOld
SCase: (owner stOld =? caller callInfo) = true
H1: puts (update_message msg) stOld = Some (result, stNew)
caller callInfo = owner stOld
  Search "=?" "=" nat.Nat.eqb_refl: forall x : nat, (x =? x) = true
beq_nat_refl: forall n : nat, true = (n =? n)
Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Nat.eqb_spec: forall x y : nat, Bool.reflect (x = y) (x =? y)
beq_nat_eq: forall n m : nat, true = (n =? m) -> n = m
beq_nat_true: forall n m : nat, (n =? m) = true -> n = m
Nat.eqb_eq: forall n m : nat, (n =? m) = true <-> n = m
beq_nat_false: forall n m : nat, (n =? m) = false -> n <> m
Nat.eqb_compare:
  forall x y : nat,
  (x =? y) = match x ?= y with
             | Eq => true
             | _ => false
             end
Nat.eqb_neq: forall x y : nat, (x =? y) = false <-> x <> y
Nat.eqb_compat: Proper (eq ==> eq ==> eq) Nat.eqb
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.pow2_bits_eqb: forall n m : nat, Nat.testbit (2 ^ n) m = (n =? m)
Nat.setbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.setbit a n) m = ((n =? m) || Nat.testbit a m)%bool
Nat.clearbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.clearbit a n) m =
  (Nat.testbit a m && negb (n =? m))%bool
Nat.testbit_eqb:
  forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
(use "About" for full details on the implicit arguments of
 Nat.eqb_compat)
msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H0: message stNew <> message stOld
SCase: (owner stOld =? caller callInfo) = true
H1: puts (update_message msg) stOld = Some (result, stNew)
caller callInfo = owner stOld
  Search (forall (x y:nat), x =? y = true -> x = y).beq_nat_true: forall n m : nat, (n =? m) = true -> n = m
msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H0: message stNew <> message stOld
SCase: (owner stOld =? caller callInfo) = true
H1: puts (update_message msg) stOld = Some (result, stNew)
caller callInfo = owner stOld
  apply beq_nat_true in SCase.msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H0: message stNew <> message stOld
SCase: owner stOld = caller callInfo
H1: puts (update_message msg) stOld = Some (result, stNew)
caller callInfo = owner stOld clear -SCase.callInfo: machine_environment
stOld: message_board_storage_type
SCase: owner stOld = caller callInfo
caller callInfo = owner stOld
  auto.
-msg: string
callInfo: machine_environment
stOld: message_board_storage_type
result: unit
stNew: message_board_storage_type
H0: message stNew <> message stOld
SCase: (owner stOld =? caller callInfo) = false
H1: fail stOld = Some (result, stNew)
caller callInfo = owner stOld inversion H1.
Qed.

Definition setMessage msg callInfo : DS unit :=
owner <- gets owner;;
if (owner =? (caller callInfo))
  then puts (update_message msg)
  else fail.

Slide for space

Thank you!

I would like to thank my supervisor Professor Steve Reeves at the University of Waikato and Vilhelm Sjöberg at CertiK for their support.

I would also like to thank Associate Professor Jing Sun and the University of Auckland for kindly hosting me during this research.

Extra slides

Extra slides:

9: Extra Message definitions
10: Extra Message proofs
11: Paper overviews
17: References and link to Crowdfunding proof
18: DeepSEA example: compilation

Record message_board_storage_type := {
  owner : nat;
  message : String.string
}.

Definition update_message message r := {|
  owner := owner r;
  message := message
|}.

Definition update_owner owner r := {|
  owner := owner;
  message := message r
|}.

Record machine_environment := {
  caller : nat;
  callvalue : nat
}.

Definition init_message_board_storage
    : message_board_storage_type := {|
  owner := 4632783269828394728397482347237428347892;
  message := ""
|}.

Definition DS := StateT Maybe message_board_storage_type.

Definition gets {A : Type} f : DS A :=
  a <- get ;;
  ret (f a).

Definition puts f : DS unit :=
  a <- get ;;
  put (f a).

Definition fail {A : Type} : DS A :=
  fun (s : message_board_storage_type) => None.

Lemma changeOwner_onlyOwner :
  forall new_owner me st,
    (exists r st', changeOwner new_owner me st = Some (r, st'))
  -> (caller me) = owner st.forall (new_owner : nat) (me : machine_environment)
  (st : message_board_storage_type),
(exists (r : unit) (st' : message_board_storage_type),
   changeOwner new_owner me st = Some (r, st')) ->
caller me = owner st
Proof.forall (new_owner : nat) (me : machine_environment)
  (st : message_board_storage_type),
(exists (r : unit) (st' : message_board_storage_type),
   changeOwner new_owner me st = Some (r, st')) ->
caller me = owner st
  intros.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: exists (r : unit) (st' : message_board_storage_type),
  changeOwner new_owner me st = Some (r, st')
caller me = owner st
  destruct H as [r].new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
H: exists st' : message_board_storage_type,
  changeOwner new_owner me st = Some (r, st')
caller me = owner st destruct H as [st'].new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
H: changeOwner new_owner me st = Some (r, st')
caller me = owner st unfold changeOwner in H.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
H: (owner <- gets owner;;
 (if owner =? caller me
  then puts (update_owner new_owner)
  else fail)) st = Some (r, st')
caller me = owner st
  Check H.H
     : (owner <- gets owner;;
        (if owner =? caller me
         then puts (update_owner new_owner)
         else fail)) st = Some (r, st')
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
H: (owner <- gets owner;;
 (if owner =? caller me
  then puts (update_owner new_owner)
  else fail)) st = Some (r, st')
caller me = owner st
  idtac.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
H: (owner <- gets owner;;
 (if owner =? caller me
  then puts (update_owner new_owner)
  else fail)) st = Some (r, st')
caller me = owner st
  simpl in H.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
H: (if owner st =? caller me
 then puts (update_owner new_owner)
 else fail) st = Some (r, st')
caller me = owner st
  Check H.H
     : (if owner st =? caller me
        then puts (update_owner new_owner)
        else fail) st = Some (r, st')
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
H: (if owner st =? caller me
 then puts (update_owner new_owner)
 else fail) st = Some (r, st')
caller me = owner st
  idtac.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
H: (if owner st =? caller me
 then puts (update_owner new_owner)
 else fail) st = Some (r, st')
caller me = owner st
  destruct (owner st =? caller me) eqn:Case.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H: fail st = Some (r, st')
caller me = owner st
    +new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
    Check Case.Case
     : (owner st =? caller me) = true
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
    Check H.H
     : puts (update_owner new_owner) st = Some (r, st')
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
    idtac.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
    apply EqNat.beq_nat_true in Case.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: owner st = caller me
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
    Check Case.Case
     : owner st = caller me
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: owner st = caller me
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
    Check H.H
     : puts (update_owner new_owner) st = Some (r, st')
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: owner st = caller me
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
    idtac.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: owner st = caller me
H: puts (update_owner new_owner) st = Some (r, st')
caller me = owner st
    auto.
    +new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H: fail st = Some (r, st')
caller me = owner st
    Check Case.Case
     : (owner st =? caller me) = false
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H: fail st = Some (r, st')
caller me = owner st
    Check H.H
     : fail st = Some (r, st')
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H: fail st = Some (r, st')
caller me = owner st
    idtac.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H: fail st = Some (r, st')
caller me = owner st
    unfold fail in H.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H: None = Some (r, st')
caller me = owner st
    Check H.H
     : None = Some (r, st')
new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H: None = Some (r, st')
caller me = owner st
    idtac.new_owner: nat
me: machine_environment
st: message_board_storage_type
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H: None = Some (r, st')
caller me = owner st
    discriminate.
Qed.

Lemma changeOwner_onlyOwner_converse :
  forall new_owner me st,
  (caller me) = owner st
  -> (exists r st', changeOwner new_owner me st = Some (r, st'))
  .forall (new_owner : nat) (me : machine_environment)
  (st : message_board_storage_type),
caller me = owner st ->
exists (r : unit) (st' : message_board_storage_type),
  changeOwner new_owner me st = Some (r, st')
Proof.forall (new_owner : nat) (me : machine_environment)
  (st : message_board_storage_type),
caller me = owner st ->
exists (r : unit) (st' : message_board_storage_type),
  changeOwner new_owner me st = Some (r, st')
  intros.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  changeOwner new_owner me st = Some (r, st')
  unfold changeOwner.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  (owner <- gets owner;;
   (if owner =? caller me
    then puts (update_owner new_owner)
    else fail)) st = Some (r, st')
  simpl.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  (if owner st =? caller me
   then puts (update_owner new_owner)
   else fail) st = Some (r, st') rewrite H.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  (if owner st =? owner st
   then puts (update_owner new_owner)
   else fail) st = Some (r, st')
  rewrite PeanoNat.Nat.eqb_refl.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  puts (update_owner new_owner) st = Some (r, st')
  exists tt.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists st' : message_board_storage_type,
  puts (update_owner new_owner) st = Some (tt, st') exists (update_owner new_owner st).new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
puts (update_owner new_owner) st =
Some (tt, update_owner new_owner st)
  unfold puts.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
(a <- get;; put (update_owner new_owner a)) st =
Some (tt, update_owner new_owner st) simpl.new_owner: nat
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
Some (tt, update_owner new_owner st) =
Some (tt, update_owner new_owner st)
  reflexivity.
Qed.

Lemma setMessage_onlyOwner_converse :
  forall new_message me st,
  (caller me) = owner st
  -> (exists r st', setMessage new_message me st = Some (r, st'))
  .forall (new_message : string) (me : machine_environment)
  (st : message_board_storage_type),
caller me = owner st ->
exists (r : unit) (st' : message_board_storage_type),
  setMessage new_message me st = Some (r, st')
Proof.forall (new_message : string) (me : machine_environment)
  (st : message_board_storage_type),
caller me = owner st ->
exists (r : unit) (st' : message_board_storage_type),
  setMessage new_message me st = Some (r, st')
  intros.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  setMessage new_message me st = Some (r, st')
  unfold setMessage.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  (owner <- gets owner;;
   (if owner =? caller me
    then puts (update_message new_message)
    else fail)) st = Some (r, st')
  simpl.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  (if owner st =? caller me
   then puts (update_message new_message)
   else fail) st = Some (r, st') rewrite H.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  (if owner st =? owner st
   then puts (update_message new_message)
   else fail) st = Some (r, st')
  rewrite PeanoNat.Nat.eqb_refl.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists (r : unit) (st' : message_board_storage_type),
  puts (update_message new_message) st = Some (r, st')
  exists tt.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
exists st' : message_board_storage_type,
  puts (update_message new_message) st = Some (tt, st') exists (update_message new_message st).new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
puts (update_message new_message) st =
Some (tt, update_message new_message st)
  unfold puts.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
(a <- get;; put (update_message new_message a)) st =
Some (tt, update_message new_message st) simpl.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
Some (tt, update_message new_message st) =
Some (tt, update_message new_message st)
  reflexivity.
Qed.

Lemma changeMessage_ownerSet :
  forall new_message me st,
    (caller me) = owner st ->
    match setMessage new_message me st with
    | Some (r, st') => message st' = new_message
    | None => False
    end.forall (new_message : string) (me : machine_environment)
  (st : message_board_storage_type),
caller me = owner st ->
match setMessage new_message me st with
| None => False
| Some (_, st') => message st' = new_message
end
Proof.forall (new_message : string) (me : machine_environment)
  (st : message_board_storage_type),
caller me = owner st ->
match setMessage new_message me st with
| None => False
| Some (_, st') => message st' = new_message
end
  intros.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
match setMessage new_message me st with
| None => False
| Some (_, st') => message st' = new_message
end
  pose proof (setMessage_onlyOwner_converse new_message me st H).new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
H0: exists (r : unit) (st' : message_board_storage_type),
  setMessage new_message me st = Some (r, st')
match setMessage new_message me st with
| None => False
| Some (_, st') => message st' = new_message
end
  destruct H0 as [r].new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
H0: exists st' : message_board_storage_type,
  setMessage new_message me st = Some (r, st')
match setMessage new_message me st with
| None => False
| Some (_, st') => message st' = new_message
end destruct H0 as [st'].new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
H0: setMessage new_message me st = Some (r, st')
match setMessage new_message me st with
| None => False
| Some (_, st') => message st' = new_message
end
  rewrite H0.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
H0: setMessage new_message me st = Some (r, st')
message st' = new_message
  Check H0.H0
     : setMessage new_message me st = Some (r, st')
new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
H0: setMessage new_message me st = Some (r, st')
message st' = new_message
  idtac.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
H0: setMessage new_message me st = Some (r, st')
message st' = new_message
  unfold setMessage in H0.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
H0: (owner <- gets owner;;
 (if owner =? caller me
  then puts (update_message new_message)
  else fail)) st = Some (r, st')
message st' = new_message
  simpl in H0.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
H0: (if owner st =? caller me
 then puts (update_message new_message)
 else fail) st = Some (r, st')
message st' = new_message
  destruct (owner st =? caller me) eqn:Case.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: puts (update_message new_message) st = Some (r, st')
message st' = new_message
new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H0: fail st = Some (r, st')
message st' = new_message
    -new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: puts (update_message new_message) st = Some (r, st')
message st' = new_message unfold puts in H0.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: (a <- get;; put (update_message new_message a)) st =
Some (r, st')
message st' = new_message simpl in H0.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: Some (tt, update_message new_message st) = Some (r, st')
message st' = new_message
    inversion H0.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: Some (tt, update_message new_message st) = Some (r, st')
H2: tt = r
H3: update_message new_message st = st'
message (update_message new_message st) = new_message
    Check H2.H2
     : tt = r
new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: Some (tt, update_message new_message st) = Some (r, st')
H2: tt = r
H3: update_message new_message st = st'
message (update_message new_message st) = new_message
    Check H3.H3
     : update_message new_message st = st'
new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: Some (tt, update_message new_message st) = Some (r, st')
H2: tt = r
H3: update_message new_message st = st'
message (update_message new_message st) = new_message
    idtac.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: Some (tt, update_message new_message st) = Some (r, st')
H2: tt = r
H3: update_message new_message st = st'
message (update_message new_message st) = new_message
    simpl.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = true
H0: Some (tt, update_message new_message st) = Some (r, st')
H2: tt = r
H3: update_message new_message st = st'
new_message = new_message  reflexivity.
    -new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H0: fail st = Some (r, st')
message st' = new_message
    Check H0.H0
     : fail st = Some (r, st')
new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H0: fail st = Some (r, st')
message st' = new_message
    idtac.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H0: fail st = Some (r, st')
message st' = new_message
    unfold fail in H0.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H0: None = Some (r, st')
message st' = new_message
    Check H0.H0
     : None = Some (r, st')
new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H0: None = Some (r, st')
message st' = new_message
    idtac.new_message: string
me: machine_environment
st: message_board_storage_type
H: caller me = owner st
r: unit
st': message_board_storage_type
Case: (owner st =? caller me) = false
H0: None = Some (r, st')
message st' = new_message
discriminate.
Qed.

Paper overviews

References

Slides powered by Alectryon: https://github.com/cpitclaudel/alectryon
The DeepSEA compiler is partly based upon the CompCert Verified Compiler
My papers: https://academic.danielb.space (Get in touch here)
C DeepSEA paper: https://dl.acm.org/doi/pdf/10.1145/3360562
Verified Price Oracles paper: https://doi.org/10.4230/OASIcs.FMBC.2021.1
Crowdfunding Proof Slides
GitHub links:
- DeepSEA
- My DeepSEA fork
- The Crowdfunding contract (as for the FTSCS paper)

Introduction to creating a DeepSEA smart contract

Example: Trivial contract converting bool to int

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

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

layer CONTRACT = { o = Trivial }

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;
    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 }