Theory Bank

theory Bank
  imports Solidity_Main
begin

section ‹Banking Contract›

subsection ‹Specification›

abbreviation "balances ≡ STR ''balances''"
abbreviation "bal ≡ STR ''bal''"

contract Bank
  for balances: "SType.TMap (SType.TValue TAddress) (SType.TValue TSint)"

constructor
where
  "⟨skip⟩"

cfunction deposit external payable
where
  "balances [⟨sender⟩] ::=⇩s balances ~⇩s [⟨sender⟩] ⟨+⟩ ⟨value⟩" ,

cfunction reset
where
  "balances [⟨sender⟩] ::=⇩s ⟨sint⟩ 0" ,

cfunction withdraw external
where
  "do {
    bal :: TSint;
    bal [] ::= balances ~⇩s [⟨sender⟩];
    icall reset;
    ⟨transfer⟩ ⟨sender⟩ (bal ~ [])
  }"

context bank
begin
  thm constructor_def
  thm deposit_def
  thm withdraw_def
end

subsection ‹Verifying an Invariant›

abbreviation
  "SUMM x ≡
    ∑ad∈UNIV. unat (valtype.uint (storage_data.vt (storage_data.mp (x balances) (Address ad))))"

context Solidity
begin

lemma sum_leq_value:
    fixes bal mp
  assumes "(∑ad∈UNIV. unat (valtype.uint (storage_data.vt (mp (Address ad))))) ≤ Balances s this"
      and "mp (Address msg_sender) = storage_data.Value (Uint y)"
      and "unat y + unat msg_value < 2^256"
    shows "(∑ad∈UNIV. unat (valtype.uint (storage_data.vt
             (if ad = msg_sender then storage_data.Value (Uint (y + msg_value))
              else mp (Address ad)))))
           ≤ Balances s this + unat msg_value"
proof -
  from sum_addr[of _ msg_sender]
  have "(∑ad|ad ∈ UNIV ∧ ad ≠ msg_sender.
    unat (valtype.uint (storage_data.vt (mp (Address ad))))) +
    unat (valtype.uint (storage_data.vt (mp (Address msg_sender)))) + unat msg_value
    ≤ Balances s this + unat msg_value"
  using assms(1) by simp
  moreover have "unat (valtype.uint (storage_data.vt (storage_data.Value (Uint (y + msg_value)))))
    ≤ unat (valtype.uint (storage_data.vt (mp (Address msg_sender)))) + unat msg_value"
    using assms(2,3) unat_add_lem[where ?'a =256] by simp
  ultimately show ?thesis using sum_addr[of _ msg_sender] by simp
qed

lemma sum_leq_this:
    fixes bal bal' mp
  assumes "(∑ad∈UNIV. unat (valtype.uint (storage_data.vt (mp (Address ad))))) ≤ Balances sa this"
      and "mp (Address this) = storage_data.Value (Uint y)"
      and "mp' (Address this) = storage_data.Value (Uint 0)"
      and "Balances s = Balances sa"
      and "⋀x. x ≠ this ⟹ mp' (Address x) = mp (Address x)"
    shows "(∑ad∈UNIV. unat (valtype.uint (storage_data.vt (mp' (Address ad))))) ≤ Balances sa this"
proof -
  from sum_addr[of _ this] have
    "(∑ad|ad ∈ UNIV ∧ ad ≠ this. unat (valtype.uint (storage_data.vt (mp (Address ad))))) +
      (unat (valtype.uint (storage_data.vt (mp (Address this)))) - unat y)
    ≤ Balances sa this - unat y"
    using assms(1,2) by simp
  moreover have "unat (valtype.uint (storage_data.vt (storage_data.Value (Uint 0))))
    ≤ unat (valtype.uint (storage_data.vt (mp (Address msg_sender)))) + unat msg_value - unat y"
    using assms(2) unat_add_lem[where ?'a =256] by simp
  ultimately show ?thesis using assms sum_addr[of _ this] by auto
qed

lemma sum_leq_sender:
    fixes bal bal' mp
  assumes "(∑ad∈UNIV. unat (valtype.uint (storage_data.vt (mp (Address ad))))) ≤ Balances sa this"
      and "mp (Address msg_sender) = storage_data.Value (Uint y)"
      and "mp' (Address msg_sender) = storage_data.Value (Uint 0)"
      and "Balances s = Balances sa"
      and "⋀x. x ≠ msg_sender ⟶ mp' (Address x) = mp (Address x)"
    shows "(∑ad∈UNIV. unat (valtype.uint (storage_data.vt (mp' (Address ad))))) ≤ Balances sa this - unat y"
proof -
  from sum_addr[of _ msg_sender] have
    "(∑ad|ad ∈ UNIV ∧ ad ≠ msg_sender. unat (valtype.uint (storage_data.vt (mp (Address ad))))) +
      (unat (valtype.uint (storage_data.vt (mp (Address msg_sender)))) - unat y)
    ≤ Balances sa this - unat y"
    using assms(1,2) by simp
  moreover have "unat (valtype.uint (storage_data.vt (storage_data.Value (Uint 0))))
    ≤ unat (valtype.uint (storage_data.vt (mp (Address msg_sender)))) + unat msg_value - unat y"
    using assms(2) unat_add_lem[where ?'a =256] by simp
  ultimately show ?thesis using assms sum_addr[of _ msg_sender] by auto
qed

lemma(in Solidity) bal_msg_sender:
  fixes bal
  assumes "∀x. ∃y. bal x = storage_data.Value (Uint y)"
  obtains y where "bal (Address msg_sender) = storage_data.Value (Uint y)"
  using assms by auto

text ‹
  Now we can start verifying the invariant.
  To this end our package provides a keyword invariant which takes a property as parameter and generates proof obligations.
›
end

invariant sum_bal sb where
    "snd sb ≥ SUMM (fst sb)"
  for "Bank"

abbreviation(in Solidity) reset_post where
"reset_post start_state return_value end_state ≡
  Balances start_state = Balances end_state ∧
  (∀mp. state.Storage start_state this balances = storage_data.Map mp ∧
  (∀y. ∃si. mp y = storage_data.Value (Uint si))
  ⟶ (∃mp'. state.Storage end_state this balances = storage_data.Map mp'
    ∧ mp' (Address msg_sender) = storage_data.Value (valtype.Uint 0)
    ∧ (∀x ≠ msg_sender. mp' (Address x) = mp (Address x))
    ∧ (∀y. ∃si. mp' y = storage_data.Value (Uint si))))"

abbreviation(in Solidity) true_pre where
"true_pre _  ≡ True"

abbreviation(in Solidity) true_post where
"true_post _ _ _  ≡ True"

declare(in bank) sum_balI[wprules del]

verification sum_bal:
  sum_bal
  deposit and
  withdraw and
  reset (true_pre, reset_post)
  for "Bank"
proof -
  show
    "⋀call.
       (⋀x h r. effect (call x) h r ⟹ vcond x h r)
        ⟹ effect (constructor call) s r
        ⟹ post s r (K (K (inv_state sum_bal))) (K True)"
    unfolding constructor_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding  inv_state_def
    by (vcg wprules: sum_balI | auto)+

  show
    b: "⋀call.
      effect (reset call) s r
        ⟹ (⋀x h r. effect (call x) h r ⟹ vcond x h r)
        ⟹ True ⟹ (post s r reset_post (K True))"
    unfolding reset_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding inv_state_def
    apply vcg
    by auto

  show
    c: "⋀call.
      (⋀x h r. effect (call x) h r ⟹ vcond x h r)
        ⟹ effect (deposit call) s r
        ⟹ inv_state sum_bal s
        ⟹ post s r (K (K (inv_state sum_bal))) (K True)"
    unfolding deposit_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding inv_state_def
    apply vcg
         apply (auto simp add: wpsimps)
     apply (rule bal_msg_sender, assumption)
     apply vcg
    by (auto simp add: wpsimps elim: allE[of _ "Address msg_sender"] intro!: sum_balI sum_leq_value)

  show
    d: "⋀call.
      (⋀x h r. effect (call x) h r ⟹ vcond x h r)
        ⟹ effect (withdraw call) s r
        ⟹ inv_state sum_bal s
        ⟹ post s r (K (K (inv_state sum_bal))) (K True)"
    unfolding withdraw_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding inv_state_def icall_def
    apply (case_tac "msg_sender = this")
     apply (vcg)
     apply (rule_tac s = msg_sender in subst,assumption)
     apply (vcg)
    (* Apply precondition for internal method call *)
           apply (subgoal_tac "(⋀x h r. effect (call x) h r ⟹ vcond x h r)")
            apply (rule_tac c=call and x=Reset_m and P'=reset_post in wp_post)
    using vcond(3) apply simp apply blast
    (* End: Apply precondition for internal method call *)
             apply (vcg)
             apply (rule_tac s=msg_sender in subst, assumption)
             apply (vcg)
             apply (auto simp add:wpsimps)
      apply (vcg)
         apply (auto simp add:wpsimps)
      apply (rule bal_msg_sender, assumption)
      apply (vcg)
         apply (rule_tac mp = mp' in sum_balI)
          apply (auto simp add:wpsimps intro: sum_leq_this)
       apply (vcg)
       apply (rule_tac mp = mpa in sum_balI)
        apply (vcg)
    (* Apply precondition for internal method call *)
        apply (subgoal_tac "(⋀x h r. effect (call x) h r ⟹ vcond x h r)")
         apply (rule_tac c=call and x=Reset_m and P'=reset_post in wp_post)
    using vcond(3) apply simp apply blast
    (* End: Apply precondition for internal method call *)
          apply vcg
          apply (auto simp add:wpsimps)
     apply vcg
        apply (auto simp add:wpsimps)
     apply (rule bal_msg_sender, assumption)
     apply vcg
        apply (rule_tac mp = mp' in sum_balI)
         apply (auto simp add:wpsimps intro: sum_leq_sender)
      defer
      apply vcg
    apply (rule_tac mp = mpa in sum_balI)
     apply vcg
    done
qed

context bank_external
begin
  thm sum_bal
  thm vcond_def
end

end