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 (x (Address ad))))"

context Solidity
begin

lemma 1:
    fixes bal
  assumes "SUMM bal ≤ Balances s this"
      and "bal (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 bal (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 (bal (Address ad))))) +
    unat (valtype.uint (storage_data.vt (bal (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 (bal (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 21:
    fixes bal bal'
  assumes "SUMM bal ≤ Balances s this"
      and "bal (Address msg_sender) = storage_data.Value (Uint y)"
      and "bal' (Address msg_sender) = storage_data.Value (Uint 0)"
      and "Balances s' this = Balances s this"
      and "∧x. x ≠ msg_sender ==> bal' (Address x) = bal (Address x)"
    shows "SUMM bal' ≤ Balances s' this - unat y"
proof -
  from sum_addr[of _ msg_sender] have
    "(∑ad|ad ∈ UNIV ∧ ad ≠ msg_sender. unat (valtype.uint (storage_data.vt (bal (Address ad))))) +
      (unat (valtype.uint (storage_data.vt (bal (Address msg_sender)))) - unat y)
    ≤ Balances s 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 (bal (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 22:
    fixes bal bal'
  assumes "SUMM bal ≤ Balances s this"
      and "bal (Address msg_sender) = storage_data.Value (Uint y)"
      and "bal' (Address msg_sender) = storage_data.Value (Uint 0)"
      and "Balances s' this = Balances s this"
      and "∧x. x ≠ msg_sender ==> bal' (Address x) = bal (Address x)"
    shows "SUMM bal' ≤ Balances s' this"
  using 21[OF assms] by simp

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
    "∀x. (fst sb) balances = storage_data.Map x ⟶ (snd sb) ≥ SUMM x"
  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))))"

declare(in bank) sum_balI[wprules del]

verification sum_bal:
  sum_bal
  "K True" "K (K (K True))"
  deposit "K True" "K (K (K True))" and
  withdraw "K True" "K (K (K True))" and
  reset "K True" 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 sum_bal (K True) (K (K (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 "∧call. effect (reset call) s r ==>
       (∧x h r. effect (call x) h r ==> vcond x h r) ==> post s r (K True) (K True) reset_post"
    unfolding reset_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding inv_state_def
    apply vcg
    by auto

  show "∧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 sum_bal (K True) (K (K (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
    apply (auto simp add: wpsimps intro!: sum_balI 1)
    apply vcg
    apply (auto simp add: wpsimps)
    apply (rule bal_msg_sender, assumption)
    by vcg

  show "∧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 sum_bal (K True) (K (K (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: 22)
    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: 21)
    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