Theory Contracts

```section ‹Contracts›
theory Contracts
imports Environment
begin

subsection ‹Syntax of Contracts›

datatype L = Id Identifier
| Ref Identifier "E list"
and      E = INT nat int
| UINT nat int
| BALANCE E
| THIS
| SENDER
| VALUE
| TRUE
| FALSE
| LVAL L
| PLUS E E
| MINUS E E
| EQUAL E E
| LESS E E
| AND E E
| OR E E
| NOT E
| CALL Identifier "E list"
| ECALL E Identifier "E list"
| CONTRACTS

datatype S = SKIP
| BLOCK "(Identifier × Type) × (E option)" S
| ASSIGN L E
| TRANSFER E E
| COMP S S
| ITE E S S
| WHILE E S
| INVOKE Identifier "E list"
| EXTERNAL E Identifier "E list" E
| NEW Identifier "E list" E

abbreviation
"vbits≡{8,16,24,32,40,48,56,64,72,80,88,96,104,112,120,128,
136,144,152,160,168,176,184,192,200,208,216,224,232,240,248,256}"

lemma vbits_max[simp]:
assumes "b1 ∈ vbits"
and "b2 ∈ vbits"
shows "(max b1 b2) ∈ vbits"
proof -
consider (b1) "max b1 b2 = b1" | (b2) "max b1 b2 = b2" by (metis max_def)
then show ?thesis
proof cases
case b1
then show ?thesis using assms(1) by simp
next
case b2
then show ?thesis using assms(2) by simp
qed
qed

lemma vbits_ge_0: "(x::nat)∈vbits ⟹ x>0" by auto

subsection ‹State›

type_synonym Gas = nat

record State =
accounts :: Accounts
stack :: Stack
memory :: MemoryT
gas :: Gas

lemma all_gas_le:
assumes "gas x<(gas y::nat)"
and "∀z. gas z < gas y ⟶ P z ⟶ Q z"
shows "∀z. gas z ≤ gas x ∧ P z ⟶ Q z" using assms by simp

lemma all_gas_less:
assumes "∀z. gas z < gas y ⟶ P z"
and "gas x≤(gas y::nat)"
shows "∀z. gas z < gas x ⟶ P z" using assms by simp

definition incrementAccountContracts :: "Address ⇒ State ⇒ State"

declare incrementAccountContracts_def [solidity_symbex]

lemma incrementAccountContracts_type[simp]:
using incrementAccountContracts_def by simp

lemma incrementAccountContracts_bal[simp]:
using incrementAccountContracts_def by simp

lemma incrementAccountContracts_stack[simp]:
"stack (incrementAccountContracts ad st) = stack st"
using incrementAccountContracts_def by simp

lemma incrementAccountContracts_memory[simp]:
"memory (incrementAccountContracts ad st) = memory st"
using incrementAccountContracts_def by simp

lemma incrementAccountContracts_storage[simp]:
"storage (incrementAccountContracts ad st) = storage st"
using incrementAccountContracts_def by simp

lemma incrementAccountContracts_gas[simp]:
"gas (incrementAccountContracts ad st) = gas st"
using incrementAccountContracts_def by simp

lemma gas_induct:
assumes "⋀s. ∀s'. gas s' < gas s ⟶ P s' ⟹ P s"
shows "P s" using assms by (rule Nat.measure_induct[of "λs. gas s"])

definition emptyStorage :: "Address ⇒ StorageT"
where
"emptyStorage _ = {\$\$}"

declare emptyStorage_def [solidity_symbex]

abbreviation mystate::State
where "mystate ≡ ⦇
accounts = emptyAccount,
stack = emptyStore,
memory = emptyStore,
storage = emptyStorage,
gas = 0
⦈"

datatype Ex = Gas | Err

subsection ‹Contracts›

text ‹
A contract consists of methods, functions, and storage variables.

A method is a triple consisting of
▪ A list of formal parameters
▪ A flag to signal external methods
▪ A statement

A function is a pair consisting of
▪ A list of formal parameters
▪ A flag to signal external functions
▪ An expression
›
datatype(discs_sels) Member = Method "(Identifier × Type) list × bool × S"
| Function "(Identifier × Type) list × bool × E"
| Var STypes

text ‹
A procedure environment assigns a contract to an address.
A contract consists of
▪ An assignment of contract to identifiers
▪ A constructor
▪ A fallback statement which is executed after money is beeing transferred to the contract.

\url{https://docs.soliditylang.org/en/v0.8.6/contracts.html#fallback-function}
›

type_synonym Contract = "(Identifier, Member) fmap × ((Identifier × Type) list × S) × S"

type_synonym Environment⇩P = "(Identifier, Contract) fmap"

definition init::"(Identifier, Member) fmap ⇒ Identifier ⇒ Environment ⇒ Environment"
where "init ct i e = (case fmlookup ct i of
Some (Var tp) ⇒ updateEnvDup i (Storage tp) (Storeloc i) e
| _ ⇒ e)"

declare init_def [solidity_symbex]

lemma init_s11[simp]:
assumes "fmlookup ct i = Some (Var tp)"
shows "init ct i e = updateEnvDup i (Storage tp) (Storeloc i) e"
using assms init_def by simp

lemma init_s12[simp]:
assumes "i |∈| fmdom (denvalue e)"
shows "init ct i e = e"
proof (cases "fmlookup ct i")
case None
then show ?thesis using init_def by simp
next
case (Some a)
then show ?thesis
proof (cases a)
case (Method _)
with Some show ?thesis using init_def by simp
next
case (Function _)
with Some show ?thesis using init_def by simp
next
case (Var tp)
with Some have "init ct i e = updateEnvDup i (Storage tp) (Storeloc i) e" using init_def by simp
moreover from assms have "updateEnvDup i (Storage tp) (Storeloc i) e = e" by auto
ultimately show ?thesis by simp
qed
qed

lemma init_s13[simp]:
assumes "fmlookup ct i = Some (Var tp)"
and "¬ i |∈| fmdom (denvalue e)"
shows "init ct i e = updateEnv i (Storage tp) (Storeloc i) e"
using assms init_def by auto

lemma init_s21[simp]:
assumes "fmlookup ct i = None"
shows "init ct i e = e"
using assms init_def by auto

lemma init_s22[simp]:
assumes "fmlookup ct i = Some (Method m)"
shows "init ct i e = e"
using assms init_def by auto

lemma init_s23[simp]:
assumes "fmlookup ct i = Some (Function f)"
shows "init ct i e = e"
using assms init_def by auto

lemma init_commte: "comp_fun_commute (init ct)"
proof
fix x y
show "init ct y ∘ init ct x = init ct x ∘ init ct y"
proof
fix e
show "(init ct y ∘ init ct x) e = (init ct x ∘ init ct y) e"
proof (cases "fmlookup ct x")
case None
then show ?thesis by simp
next
case s1: (Some a)
then show ?thesis
proof (cases a)
case (Method _)
with s1 show ?thesis by simp
next
case (Function _)
with s1 show ?thesis by simp
next
case v1: (Var tp)
then show ?thesis
proof (cases "x |∈| fmdom (denvalue e)")
case True
with s1 v1 have *: "init ct x e = e" by auto
then show ?thesis
proof (cases "fmlookup ct y")
case None
then show ?thesis by simp
next
case s2: (Some a)
then show ?thesis
proof (cases a)
case (Method _)
with s2 show ?thesis by simp
next
case (Function _)
with s2 show ?thesis by simp
next
case v2: (Var tp')
then show ?thesis
proof (cases "y |∈| fmdom (denvalue e)")
case t1: True
with s1 v1 True s2 v2 show ?thesis by fastforce
next
define e' where "e' = updateEnv y (Storage tp') (Storeloc y) e"
case False
with s2 v2 have "init ct y e = e'" using e'_def by auto
with s1 v1 True e'_def * show ?thesis by auto
qed
qed
qed
next
define e' where "e' = updateEnv x (Storage tp) (Storeloc x) e"
case f1: False
with s1 v1 have *: "init ct x e = e'" using e'_def by auto
then show ?thesis
proof (cases "fmlookup ct y")
case None
then show ?thesis by simp
next
case s3: (Some a)
then show ?thesis
proof (cases a)
case (Method _)
with s3 show ?thesis by simp
next
case (Function _)
with s3 show ?thesis by simp
next
case v2: (Var tp')
then show ?thesis
proof (cases "y |∈| fmdom (denvalue e)")
case t1: True
with e'_def have "y |∈| fmdom (denvalue e')" by simp
with s1 s3 v1 f1 v2 show ?thesis using e'_def by fastforce
next
define f' where "f' = updateEnv y (Storage tp') (Storeloc y) e"
define e'' where "e'' = updateEnv y (Storage tp') (Storeloc y) e'"
case f2: False
with s3 v2 have **: "init ct y e = f'" using f'_def by auto
show ?thesis
proof (cases "y = x")
case True
with s3 v2 e'_def have "init ct y e' = e'" by simp
moreover from s3 v2 True f'_def have "init ct x f' = f'" by simp
ultimately show ?thesis using True by simp
next
define f'' where "f'' = updateEnv x (Storage tp) (Storeloc x) f'"
case f3: False
with f2 have "¬ y |∈| fmdom (denvalue e')" using e'_def by simp
with s3 v2 e''_def have "init ct y e' = e''" by auto
with * have "(init ct y ∘ init ct x) e = e''" by simp
moreover have "init ct x f' = f''"
proof -
from s1 v1 have "init ct x f' = updateEnvDup x (Storage tp) (Storeloc x) f'" by simp
moreover from f1 f3 have "x |∉| fmdom (denvalue f')" using f'_def by simp
ultimately show ?thesis using f''_def by auto
qed
moreover from f''_def e''_def f'_def e'_def f3 have "Some f'' = Some e''" using env_reorder_neq by simp
ultimately show ?thesis using ** by simp
qed
qed
qed
qed
qed
qed
qed
qed
qed

proof (cases "fmlookup ct i")
case None
then show ?thesis by simp
next
case (Some a)
show ?thesis
proof (cases a)
case (Method _)
with Some show ?thesis by simp
next
case (Function _)
with Some show ?thesis by simp
next
case (Var _)
with Some show ?thesis using updateEnvDup_address updateEnvDup_sender by simp
qed
qed

lemma init_sender[simp]:
"sender (init ct i e) = sender e"
proof (cases "fmlookup ct i")
case None
then show ?thesis by simp
next
case (Some a)
show ?thesis
proof (cases a)
case (Method _)
with Some show ?thesis by simp
next
case (Function _)
with Some show ?thesis by simp
next
case (Var _)
with Some show ?thesis using updateEnvDup_sender by simp
qed
qed

lemma init_svalue[simp]:
"svalue (init ct i e) = svalue e"
proof (cases "fmlookup ct i")
case None
then show ?thesis by simp
next
case (Some a)
show ?thesis
proof (cases a)
case (Method _)
with Some show ?thesis by simp
next
case (Function _)
with Some show ?thesis by simp
next
case (Var _)
with Some show ?thesis using updateEnvDup_svalue by simp
qed
qed

lemma ffold_init_ad_same[rule_format]: "∀e'. ffold (init ct) e xs = e' ⟶ address e' = address e ∧ sender e' = sender e ∧ svalue e' = svalue e"
proof (induct xs)
case empty
then show ?case by (simp add: ffold_def)
next
case (insert x xs)
then have *: "ffold (init ct) e (finsert x xs) =
init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp
show ?case
proof (rule allI[OF impI])
fix e' assume **: "ffold (init ct) e (finsert x xs) = e'"
with * obtain e'' where ***: "ffold (init ct) e xs = e''" by simp
with insert have "address e'' = address e ∧ sender e'' = sender e ∧ svalue e'' = svalue e" by blast
with * ** *** show "address e' = address e ∧ sender e' = sender e ∧ svalue e' = svalue e" using init_address init_sender init_svalue by metis
qed
qed

lemma ffold_init_sender[simp]: "sender (ffold (init ct) e xs) = sender e"

lemma ffold_init_dom:
"fmdom (denvalue (ffold (init ct) e xs)) |⊆| fmdom (denvalue e) |∪| xs"
proof (induct "xs")
case empty
then show ?case
proof
fix x
assume "x |∈| fmdom (denvalue (ffold (init ct) e {||}))"
moreover have "ffold (init ct) e {||} = e" using FSet.comp_fun_commute.ffold_empty[OF init_commte, of ct e] by simp
ultimately show "x |∈| fmdom (denvalue e) |∪| {||}" by simp
qed
next
case (insert x xs)
then have *: "ffold (init ct) e (finsert x xs) =
init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp

show ?case
proof
fix x' assume "x' |∈| fmdom (denvalue (ffold (init ct) e (finsert x xs)))"
with * have **: "x' |∈| fmdom (denvalue (init ct x (ffold (init ct) e xs)))" by simp
then consider "x' |∈| fmdom (denvalue (ffold (init ct) e xs))" | "x'=x"
proof (cases "fmlookup ct x")
case None
then show ?thesis using that ** by simp
next
case (Some a)
then show ?thesis
proof (cases a)
case (Method _)
then show ?thesis using Some ** that by simp
next
case (Function _)
then show ?thesis using Some ** that by simp
next
case (Var x2)
show ?thesis
proof (cases "x=x'")
case True
then show ?thesis using that by simp
next
case False
then have "fmlookup (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs))) x' = fmlookup (denvalue (ffold (init ct) e xs)) x'" using updateEnvDup_dup by simp
moreover from ** Some Var have ***:"x' |∈| fmdom (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs)))" by simp
ultimately have "x' |∈| fmdom (denvalue (ffold (init ct) e xs))" by (simp add: fmlookup_dom_iff)
then show ?thesis using that by simp
qed
qed
qed
then show "x' |∈| fmdom (denvalue e) |∪| finsert x xs"
proof cases
case 1
then show ?thesis using insert.hyps by auto
next
case 2
then show ?thesis by simp
qed
qed
qed

lemma ffold_init_fmap:
assumes "fmlookup ct i = Some (Var tp)"
and "i |∉| fmdom (denvalue e)"
shows "i|∈|xs ⟹ fmlookup (denvalue (ffold (init ct) e xs)) i = Some (Storage tp, Storeloc i)"
proof (induct "xs")
case empty
then show ?case by simp
next
case (insert x xs)
then have *: "ffold (init ct) e (finsert x xs) =
init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp

from insert.prems consider (a) "i |∈| xs" | (b) "¬ i |∈| xs ∧ i = x" by auto
then show "fmlookup (denvalue (ffold (init ct) e (finsert x xs))) i = Some (Storage tp, Storeloc i)"
proof cases
case a
with insert.hyps(2) have "fmlookup (denvalue (ffold (init ct) e xs)) i = Some (Storage tp, Storeloc i)" by simp
moreover have "fmlookup (denvalue (init ct x (ffold (init ct) e xs))) i = fmlookup (denvalue (ffold (init ct) e xs)) i"
proof (cases "fmlookup ct x")
case None
then show ?thesis by simp
next
case (Some a)
then show ?thesis
proof (cases a)
case (Method _)
with Some show ?thesis by simp
next
case (Function _)
with Some show ?thesis by simp
next
case (Var x2)
with Some have "init ct x (ffold (init ct) e xs) = updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs)" using init_def[of ct x "(ffold (init ct) e xs)"] by simp
moreover from insert a have "i≠x" by auto
then have "fmlookup (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs))) i = fmlookup (denvalue (ffold (init ct) e xs)) i" using updateEnvDup_dup[of x i] by simp
ultimately show ?thesis by simp
qed
qed
ultimately show ?thesis using * by simp
next
case b
with assms(1) have "fmlookup ct x = Some (Var tp)" by simp
moreover from b assms(2) have "¬ x |∈| fmdom (denvalue (ffold (init ct) e xs))" using ffold_init_dom by auto
ultimately have "init ct x (ffold (init ct) e xs) = updateEnv x (Storage tp) (Storeloc x) (ffold (init ct) e xs)" by auto
with b * show ?thesis by simp
qed
qed

lemma ffold_init_fmdom:
assumes "fmlookup ct i = Some (Var tp)"
and "i |∉| fmdom (denvalue e)"
shows "fmlookup (denvalue (ffold (init ct) e (fmdom ct))) i = Some (Storage tp, Storeloc i)"
proof -
from assms(1) have "i |∈| fmdom ct" by (rule Finite_Map.fmdomI)
then show ?thesis using ffold_init_fmap[OF assms] by simp
qed

text‹The following definition allows for a more fine-grained configuration of the
code generator.
›
definition ffold_init::"(String.literal, Member) fmap ⇒ Environment ⇒ String.literal fset ⇒ Environment" where
‹ffold_init ct a c = ffold (init ct) a c›
declare ffold_init_def [simp,solidity_symbex]

lemma ffold_init_code [code]:
‹ffold_init ct a c = fold (init ct) (remdups (sorted_list_of_set (fset c))) a›
using  comp_fun_commute_on.fold_set_fold_remdups ffold.rep_eq
ffold_init_def init_commte sorted_list_of_fset.rep_eq
sorted_list_of_fset_simps(1)
by (metis comp_fun_commute.comp_fun_commute comp_fun_commute_on.intro order_refl)

lemma bind_case_stackvalue_cong [fundef_cong]:
assumes "x = x'"
and "⋀v. x = KValue v ⟹ f v s = f' v s"
and "⋀p. x = KCDptr p ⟹ g p s = g' p s"
and "⋀p. x = KMemptr p ⟹ h p s = h' p s"
and "⋀p. x = KStoptr p ⟹ i p s = i' p s"
shows "(case x of KValue v ⇒ f v | KCDptr p ⇒ g p | KMemptr p ⇒ h p | KStoptr p ⇒ i p) s
= (case x' of KValue v ⇒ f' v | KCDptr p ⇒ g' p | KMemptr p ⇒ h' p | KStoptr p ⇒ i' p) s"
using assms by (cases x, auto)

lemma bind_case_type_cong [fundef_cong]:
assumes "x = x'"
and "⋀t. x = Value t ⟹ f t s = f' t s"
and "⋀t. x = Calldata t ⟹ g t s = g' t s"
and "⋀t. x = Memory t ⟹ h t s = h' t s"
and "⋀t. x = Storage t ⟹ i t s = i' t s"
shows "(case x of Value t ⇒ f t | Calldata t ⇒ g t | Memory t ⇒ h t | Storage t ⇒ i t ) s
= (case x' of Value t ⇒ f' t | Calldata t ⇒ g' t | Memory t ⇒ h' t | Storage t ⇒ i' t) s"
using assms by (cases x, auto)

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

lemma bind_case_mtypes_cong [fundef_cong]:
assumes "x = x'"
and "⋀a t. x = (MTArray a t) ⟹ f a t s = f' a t s"
and "⋀p. x = (MTValue p) ⟹ g p s = g' p s"
shows "(case x of (MTArray a t) ⇒ f a t | (MTValue p) ⇒ g p) s
= (case x' of (MTArray a t) ⇒ f' a t | (MTValue p) ⇒ g' p) s"
using assms by (cases x, auto)

lemma bind_case_stypes_cong [fundef_cong]:
assumes "x = x'"
and "⋀a t. x = (STArray a t) ⟹ f a t s = f' a t s"
and "⋀a t. x = (STMap a t) ⟹ g a t s = g' a t s"
and "⋀p. x = (STValue p) ⟹ h p s = h' p s"
shows "(case x of (STArray a t) ⇒ f a t | (STMap a t) ⇒ g a t | (STValue p) ⇒ h p) s
= (case x' of (STArray a t) ⇒ f' a t | (STMap a t) ⇒ g' a t | (STValue p) ⇒ h' p) s"
using assms by (cases x, auto)

lemma bind_case_types_cong [fundef_cong]:
assumes "x = x'"
and "⋀a. x = (TSInt a) ⟹ f a s = f' a s"
and "⋀a. x = (TUInt a) ⟹ g a s = g' a s"
and "x = TBool ⟹ h s = h' s"
and "x = TAddr ⟹ i s = i' s"
shows "(case x of (TSInt a) ⇒ f a | (TUInt a) ⇒ g a | TBool ⇒ h | TAddr ⇒ i) s
= (case x' of (TSInt a) ⇒ f' a | (TUInt a) ⇒ g' a | TBool ⇒ h' | TAddr ⇒ i') s"
using assms by (cases x, auto)

lemma bind_case_contract_cong [fundef_cong]:
assumes "x = x'"
and "⋀a. x = Method a ⟹ f a s = f' a s"
and "⋀a. x = Function a ⟹ g a s = g' a s"
and "⋀a. x = Var a ⟹ h a s = h' a s"
shows "(case x of Method a ⇒ f a | Function a ⇒ g a | Var a ⇒ h a) s
= (case x' of Method a ⇒ f' a | Function a ⇒ g' a | Var a ⇒ h' a) s"
using assms by (cases x, auto)

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

end
```