# Theory Accounts

```section‹Accounts›
theory Accounts
imports Valuetypes
begin

type_synonym Balance = Valuetype
type_synonym Identifier = String.literal

(*
Contract None means not initialized yet
*)
datatype atype =
EOA
| Contract Identifier

record account =
bal :: Balance
type :: "atype option"
contracts :: nat

lemma bind_case_atype_cong [fundef_cong]:
assumes "x = x'"
and "x = EOA ⟹ f s = f' s"
and "⋀a. x = Contract a ⟹ g a s = g' a s"
shows "(case x of EOA ⇒ f | Contract a ⇒ g a) s
= (case x' of EOA ⇒ f' | Contract a ⇒ g' a) s"
using assms by (cases x, auto)

definition emptyAcc :: account
where "emptyAcc = ⦇bal = ShowL⇩i⇩n⇩t 0, type = None, contracts = 0⦈"

declare emptyAcc_def [solidity_symbex]

type_synonym Accounts = "Address ⇒ account"

definition emptyAccount :: "Accounts"
where
"emptyAccount _ = emptyAcc"

declare emptyAccount_def [solidity_symbex]

where
in if (v < 2^256)
else None)
else None)"

proof
proof (cases "ReadL⇩i⇩n⇩t val ≥ 0")
case t1: True
with assms(2) have "v ≥0" by (simp add: t1)
then show ?thesis
proof (cases "v < 2^256")
case t2: True
with t2 `v ≥0` show ?thesis using assms Read_ShowL_id by auto
next
case False
with t1 v_def show ?thesis using assms(1) unfolding addBalance_def by simp
qed
next
case False
then show ?thesis using assms(1) unfolding addBalance_def by simp
qed
qed

proof -
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed

proof -
qed

proof -
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed

definition subBalance :: "Address ⇒ Valuetype ⇒ Accounts ⇒ Accounts option"
where
in if (v ≥ 0)
else None)
else None)"

declare subBalance_def [solidity_symbex]

lemma subBalance_val1:
assumes "subBalance ad val acc = Some acc'"
using assms unfolding subBalance_def by (simp split:if_split_asm)

lemma subBalance_val2:
assumes "subBalance ad val acc = Some acc'"
using assms unfolding subBalance_def by (simp split:if_split_asm)

lemma subBalance_sub:
assumes "subBalance ad val acc = Some acc'"
proof -
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed

lemma subBalance_limit:
assumes "subBalance ad val acc = Some acc'"
proof
proof (cases "ReadL⇩i⇩n⇩t val ≥ 0")
case t1: True
with assms(2) t1 have "v < 2 ^ 256" by (smt (verit))
then show ?thesis
proof (cases "v ≥ 0")
case t2: True
with t1 v_def have "subBalance ad val acc = Some (acc(ad := acc ad⦇bal:=ShowL⇩i⇩n⇩t v⦈))" unfolding subBalance_def by simp
with t2 `v < 2 ^ 256` show ?thesis using assms Read_ShowL_id by auto
next
case False
with t1 v_def show ?thesis using assms(1) unfolding subBalance_def by simp
qed
next
case False
then show ?thesis using assms(1) unfolding subBalance_def by simp
qed
qed

lemma subBalance_mono:
assumes "subBalance ad val acc = Some acc'"
proof -
thus ?thesis using v_def Read_ShowL_id assms unfolding subBalance_def by (simp split:if_split_asm)
qed

lemma subBalance_eq:
assumes "subBalance ad val acc = Some acc'"
proof -
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed

definition transfer :: "Address ⇒ Address ⇒ Valuetype ⇒ Accounts ⇒ Accounts option"
where
(case subBalance ads val acc of
| None ⇒ None)"

declare transfer_def [solidity_symbex]

lemma transfer_val1:
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"
then show "ReadL⇩i⇩n⇩t val ≥ 0" using subBalance_val1[OF *] by simp
qed

lemma transfer_val2:
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"

with * show ?thesis using assms(2) subBalance_eq[OF *] by simp
qed

lemma transfer_val3:
using assms by (auto simp add: Let_def subBalance_def transfer_def split:if_split_asm)

proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"

ultimately show ?thesis using Read_ShowL_id by simp
qed

lemma transfer_sub:
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"

ultimately show ?thesis using Read_ShowL_id by simp
qed

lemma transfer_same:
proof -
from assms obtain acc'' where *: "subBalance ad val acc = Some acc''" by (simp add: subBalance_def transfer_def split:if_split_asm)
ultimately show ?thesis by simp
qed

lemma transfer_mono:
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"

show ?thesis
case True
ultimately show ?thesis using Read_ShowL_id by auto
next
case False
finally show ?thesis .
qed
qed

lemma transfer_eq:

lemma transfer_limit:
proof
from assms(1) obtain acc'' where "subBalance ads val acc = Some acc''" and "addBalance addr val acc'' = Some acc'" by (simp add: subBalance_def transfer_def split: if_split_asm)
with subBalance_limit[OF _ assms(2)]
qed

lemma transfer_type_same: