# Theory Statements

section ‹Statements›
theory Statements
begin

subsection ‹Syntax›

subsubsection ‹Expressions›
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" E

subsubsection ‹Statements›
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

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 ‹Contracts›

text ‹
A contract consists of methods or storage variables.
A method is a triple consisting of
\begin{itemize}
\item A list of formal parameters
\item A statement
\item An optional return value
\end{itemize}
›

datatype Member = Method "(Identifier × Type) list × S × E option"
| Var STypes

text ‹
A procedure environment assigns a contract to an address.
A contract consists of
\begin{itemize}
\item An assignment of members to identifiers
\item An optional fallback statement which is executed after money is beeing transferred to the contract.
\end{itemize}
\url{https://docs.soliditylang.org/en/v0.8.6/contracts.html#fallback-function}
›

type_synonym Environment⇩P = "(Address, (Identifier, Member) fmap × S) 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)"

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 x1)
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_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 x1)
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 x1)
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 x1)
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

"address (init ct i e) = address e ∧ 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 x1)
with Some show ?thesis by simp
next
case (Var tp)
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 x1)
with Some show ?thesis by simp
next
case (Var tp)
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 x1)
with Some show ?thesis by simp
next
case (Var tp)
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_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 x1)
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 x1)
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

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]

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 = Var a ⟹ g a s = g' a s"
shows "(case x of (Method a) ⇒ f a | (Var a) ⇒ g a) s
= (case x' of (Method a) ⇒ f' a | (Var a) ⇒ g' 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)

abbreviation lift ::
"(E ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ (Stackvalue * Type, Ex, State) state_monad)
⇒ (Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option)
⇒ E ⇒ E ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ (Stackvalue * Type, Ex, State) state_monad"
where
"lift expr f e1 e2 e⇩p e cd ≡
(do {
kv1 ← expr e1 e⇩p e cd;
(case kv1 of
(KValue v1, Value t1) ⇒ (do
{
kv2 ← expr e2 e⇩p e cd;
(case kv2 of
(KValue v2, Value t2) ⇒
(case f t1 t2 v1 v2 of
Some (v, t) ⇒ return (KValue v, Value t)
| None ⇒ throw Err)
| _ ⇒ (throw Err::(Stackvalue * Type, Ex, State) state_monad))
})
| _ ⇒ (throw Err::(Stackvalue * Type, Ex, State) state_monad))
})"

abbreviation gascheck ::
"(State ⇒ Gas) ⇒ (unit, Ex, State) state_monad"
where
"gascheck check ≡
do {
g ← (applyf check::(Gas, Ex, State) state_monad);
(assert Gas (λst. gas st ≤ g) (modify (λst. st ⦇gas:=gas st - g⦈)::(unit, Ex, State) state_monad))
}"

subsection ‹Semantics›

datatype LType = LStackloc Location
| LMemloc Location
| LStoreloc Location

locale statement_with_gas =
fixes costs :: "S⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Gas"
and costs⇩e :: "E⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Gas"
assumes while_not_zero[termination_simp]: "⋀e e⇩p cd st ex s0. 0 < (costs (WHILE ex s0) e⇩p e cd st) "
and call_not_zero[termination_simp]: "⋀e e⇩p cd st i ix. 0 < (costs⇩e (CALL i ix) e⇩p e cd st)"
and ecall_not_zero[termination_simp]: "⋀e e⇩p cd st a i ix val. 0 < (costs⇩e (ECALL a i ix val) e⇩p e cd st)"
and invoke_not_zero[termination_simp]: "⋀e e⇩p cd st i xe. 0 < (costs (INVOKE i xe) e⇩p e cd st)"
and external_not_zero[termination_simp]: "⋀e e⇩p cd st ad i xe val. 0 < (costs (EXTERNAL ad i xe val) e⇩p e cd st)"
and transfer_not_zero[termination_simp]: "⋀e e⇩p cd st ex ad. 0 < (costs (TRANSFER ad ex) e⇩p e cd st)"
begin

function msel::"bool ⇒ MTypes ⇒ Location ⇒ E list ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ (Location * MTypes, Ex, State) state_monad"
and ssel::"STypes ⇒ Location ⇒ E list ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ (Location * STypes, Ex, State) state_monad"
and lexp :: "L ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ (LType * Type, Ex, State) state_monad"
and expr::"E ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ (Stackvalue * Type, Ex, State) state_monad"
and load :: "bool ⇒ (Identifier × Type) list ⇒ E list ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Environment ⇒ CalldataT ⇒ (Environment × CalldataT × State, Ex, State) state_monad"
and rexp::"L ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ (Stackvalue * Type, Ex, State) state_monad"
and stmt :: "S ⇒ Environment⇩P ⇒ Environment ⇒ CalldataT ⇒ (unit, Ex, State) state_monad"
where
"msel _ _ _ [] _ _ _ st = throw Err st"
| "msel _ (MTValue _) _ _ _ _ _ st = throw Err st"
| "msel _ (MTArray al t) loc [x] e⇩p env cd st =
(do {
kv ← expr x e⇩p env cd;
(case kv of
(KValue v, Value t') ⇒
(if less t' (TUInt 256) v (ShowL⇩i⇩n⇩t al) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool)
then return (hash loc v, t)
else throw Err)
| _ ⇒ throw Err)
}) st"
(*
Note that it is indeed possible to modify the state while evaluating the expression
to determine the index of the array to look up.
*)
| "msel mm (MTArray al t) loc (x # y # ys) e⇩p env cd st =
(do {
kv ← expr x e⇩p env cd;
(case kv of
(KValue v, Value t') ⇒
(if less t' (TUInt 256) v (ShowL⇩i⇩n⇩t al) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool)
then do {
s ← applyf (λst. if mm then memory st else cd);
(case accessStore (hash loc v) s of
Some (MPointer l) ⇒ msel mm t l (y#ys) e⇩p env cd
| _ ⇒ throw Err)
} else throw Err)
| _ ⇒ throw Err)
}) st"
| "ssel tp loc Nil _ _ _ st = return (loc, tp) st"
| "ssel (STValue _) _ (_ # _) _ _ _ st = throw Err st"
| "ssel (STArray al t) loc (x # xs) e⇩p env cd st =
(do {
kv ← expr x e⇩p env cd;
(case kv of
(KValue v, Value t') ⇒
(if less t' (TUInt 256) v (ShowL⇩i⇩n⇩t al) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool)
then ssel t (hash loc v) xs e⇩p env cd
else throw Err)
| _ ⇒ throw Err)
}) st"
| "ssel (STMap _ t) loc (x # xs) e⇩p env cd st =
(do {
kv ← expr x e⇩p env cd;
(case kv of
(KValue v, _) ⇒ ssel t (hash loc v) xs e⇩p env cd
| _ ⇒ throw Err)
}) st"
| "lexp (Id i) _ e _ st =
(case fmlookup (denvalue e) i of
Some (tp, (Stackloc l)) ⇒ return (LStackloc l, tp)
| Some (tp, (Storeloc l)) ⇒ return (LStoreloc l, tp)
| _ ⇒ throw Err) st"
| "lexp (Ref i r) e⇩p e cd st =
(case fmlookup (denvalue e) i of
Some (tp, Stackloc l) ⇒
do {
k ← applyf (λst. accessStore l (stack st));
(case k of
Some (KCDptr _) ⇒ throw Err
| Some (KMemptr l') ⇒
(case tp of
Memory t ⇒
do {
(l'', t') ← msel True t l' r e⇩p e cd;
return (LMemloc l'', Memory t')
}
| _ ⇒ throw Err)
| Some (KStoptr l') ⇒
(case tp of
Storage t ⇒
do {
(l'', t') ← ssel t l' r e⇩p e cd;
return (LStoreloc l'', Storage t')
}
| _ ⇒ throw Err)
| Some (KValue _) ⇒ throw Err
| None ⇒ throw Err)
}
| Some (tp, Storeloc l) ⇒
(case tp of
Storage t ⇒
do {
(l', t') ← ssel t l r e⇩p e cd;
return (LStoreloc l', Storage t')
}
| _ ⇒ throw Err)
| None ⇒ throw Err) st"
| "expr (E.INT b x) e⇩p e cd st =
(do {
gascheck (costs⇩e (E.INT b x) e⇩p e cd);
(if (b ∈ vbits)
then (return (KValue (createSInt b x), Value (TSInt b)))
else (throw Err))
}) st"
| "expr (UINT b x) e⇩p e cd st =
(do {
gascheck (costs⇩e (UINT b x) e⇩p e cd);
(if (b ∈ vbits)
then (return (KValue (createUInt b x), Value (TUInt b)))
else (throw Err))
}) st"
(do {
}) st"
| "expr (BALANCE ad) e⇩p e cd st =
(do {
gascheck (costs⇩e (BALANCE ad) e⇩p e cd);
kv ← expr ad e⇩p e cd;
(case kv of
return (KValue (accessBalance (accounts st) adv), Value (TUInt 256))
| _ ⇒ throw Err)
}) st"
| "expr THIS e⇩p e cd st =
(do {
gascheck (costs⇩e THIS e⇩p e cd);
}) st"
| "expr SENDER e⇩p e cd st =
(do {
gascheck (costs⇩e SENDER e⇩p e cd);
return (KValue (sender e), Value TAddr)
}) st"
| "expr VALUE e⇩p e cd st =
(do {
gascheck (costs⇩e VALUE e⇩p e cd);
return (KValue (svalue e), Value (TUInt 256))
}) st"
| "expr TRUE e⇩p e cd st =
(do {
gascheck (costs⇩e TRUE e⇩p e cd);
return (KValue (ShowL⇩b⇩o⇩o⇩l True), Value TBool)
}) st"
| "expr FALSE e⇩p e cd st =
(do {
gascheck (costs⇩e FALSE e⇩p e cd);
return (KValue (ShowL⇩b⇩o⇩o⇩l False), Value TBool)
}) st"
| "expr (NOT x) e⇩p e cd st =
(do {
gascheck (costs⇩e (NOT x) e⇩p e cd);
kv ← expr x e⇩p e cd;
(case kv of
(KValue v, Value t) ⇒
(if v = ShowL⇩b⇩o⇩o⇩l True
then expr FALSE e⇩p e cd
else (if v = ShowL⇩b⇩o⇩o⇩l False
then expr TRUE e⇩p e cd
else throw Err))
| _ ⇒ throw Err)
}) st"
| "expr (PLUS e1 e2) e⇩p e cd st = (gascheck (costs⇩e (PLUS e1 e2) e⇩p e cd) ⤜ (λ_. lift expr add e1 e2 e⇩p e cd)) st"
| "expr (MINUS e1 e2) e⇩p e cd st = (gascheck (costs⇩e (MINUS e1 e2) e⇩p e cd) ⤜ (λ_. lift expr sub e1 e2 e⇩p e cd)) st"
| "expr (LESS e1 e2) e⇩p e cd st = (gascheck (costs⇩e (LESS e1 e2) e⇩p e cd) ⤜ (λ_. lift expr less e1 e2 e⇩p e cd)) st"
| "expr (EQUAL e1 e2) e⇩p e cd st = (gascheck (costs⇩e (EQUAL e1 e2) e⇩p e cd) ⤜ (λ_. lift expr equal e1 e2 e⇩p e cd)) st"
| "expr (AND e1 e2) e⇩p e cd st = (gascheck (costs⇩e (AND e1 e2) e⇩p e cd) ⤜ (λ_. lift expr vtand e1 e2 e⇩p e cd)) st"
| "expr (OR e1 e2) e⇩p e cd st = (gascheck (costs⇩e (OR e1 e2) e⇩p e cd) ⤜ (λ_. lift expr vtor e1 e2 e⇩p e cd)) st"
| "expr (LVAL i) e⇩p e cd st =
(do {
gascheck (costs⇩e (LVAL i) e⇩p e cd);
rexp i e⇩p e cd
}) st"
- Internal method calls use a fresh environment and stack but keep the memory [1]
- External method calls use a fresh environment and stack and memory [2]
[1]: https://docs.soliditylang.org/en/v0.8.5/control-structures.html#internal-function-calls
[2]: https://docs.soliditylang.org/en/v0.8.5/control-structures.html#external-function-calls

TODO: Functions with no return value should be able to execute
*)
| "expr (CALL i xe) e⇩p e cd st =
(do {
gascheck (costs⇩e (CALL i xe) e⇩p e cd);
(case fmlookup e⇩p (address e) of
Some (ct, _) ⇒
(case fmlookup ct i of
Some (Method (fp, f, Some x)) ⇒
let e' = ffold_init ct (emptyEnv (address e) (sender e) (svalue e)) (fmdom ct)
in (do {
st' ← applyf (λst. st⦇stack:=emptyStore⦈);
(e'', cd', st'') ← load False fp xe e⇩p e' emptyStore st' e cd;
st''' ← get;
put st'';
stmt f e⇩p e'' cd';
rv ← expr x e⇩p e'' cd';
modify (λst. st⦇stack:=stack st''', memory := memory st'''⦈);
return rv
})
| _ ⇒ throw Err)
| None ⇒ throw Err)
}) st"
| "expr (ECALL ad i xe val) e⇩p e cd st =
(do {
gascheck (costs⇩e (ECALL ad i xe val) e⇩p e cd);
Some (ct, _) ⇒
(case fmlookup ct i of
Some (Method (fp, f, Some x)) ⇒
(do {
kv ← expr val e⇩p e cd;
(case kv of
(KValue v, Value t) ⇒
let e' = ffold_init ct (emptyEnv adv (address e) v) (fmdom ct)
in (do {
st' ← applyf (λst. st⦇stack:=emptyStore, memory:=emptyStore⦈);
(e'', cd', st'') ← load True fp xe e⇩p e' emptyStore st' e cd;
st''' ← get;
Some acc ⇒
do {
put (st''⦇accounts := acc⦈);
stmt f e⇩p e'' cd';
rv ← expr x e⇩p e'' cd';
modify (λst. st⦇stack:=stack st''', memory := memory st'''⦈);
return rv
}
| None ⇒ throw Err)
})
| _ ⇒ throw Err)
})
| _ ⇒ throw Err)
| None ⇒ throw Err)
| _ ⇒ throw Err)
}) st"
| "load cp ((i⇩p, t⇩p)#pl) (e#el) e⇩p e⇩v' cd' st' e⇩v cd st =
(do {
(v, t) ← expr e e⇩p e⇩v cd;
st'' ← get;
put st';
(cd'', e⇩v'') ← decl i⇩p t⇩p (Some (v,t)) cp cd (memory st'') cd' e⇩v';
st''' ← get;
put st'';
load cp pl el e⇩p e⇩v'' cd'' st''' e⇩v cd
}) st"
| "load _ [] (_#_) _ _ _ _ _ _ st = throw Err st"
| "load _ (_#_) [] _ _ _ _ _ _ st = throw Err st"
| "load _ [] [] _ e⇩v' cd' st' e⇩v cd st = return (e⇩v', cd', st') st"
(*TODO: Should be possible to simplify*)
| "rexp (Id i) e⇩p e cd st =
(case fmlookup (denvalue e) i of
Some (tp, Stackloc l) ⇒
do {
s ← applyf (λst. accessStore l (stack st));
(case s of
Some (KValue v) ⇒ return (KValue v, tp)
| Some (KCDptr p) ⇒ return (KCDptr p, tp)
| Some (KMemptr p) ⇒ return (KMemptr p, tp)
| Some (KStoptr p) ⇒ return (KStoptr p, tp)
| _ ⇒ throw Err)
}
| Some (Storage (STValue t), Storeloc l) ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address e));
(case so of
Some s ⇒ return (KValue (accessStorage t l s), Value t)
| None ⇒ throw Err)
}
| Some (Storage (STArray x t), Storeloc l) ⇒ return (KStoptr l, Storage (STArray x t))
| _ ⇒ throw Err) st"
| "rexp (Ref i r) e⇩p e cd st =
(case fmlookup (denvalue e) i of
Some (tp, (Stackloc l)) ⇒
do {
kv ← applyf (λst. accessStore l (stack st));
(case kv of
Some (KCDptr l') ⇒
(case tp of
Calldata t ⇒
do {
(l'', t') ← msel False t l' r e⇩p e cd;
(case t' of
MTValue t'' ⇒
(case accessStore l'' cd of
Some (MValue v) ⇒ return (KValue v, Value t'')
| _ ⇒ throw Err)
| MTArray x t'' ⇒
(case accessStore l'' cd of
Some (MPointer p) ⇒ return (KCDptr p, Calldata (MTArray x t''))
| _ ⇒ throw Err))
}
| _ ⇒ throw Err)
| Some (KMemptr l') ⇒
(case tp of
Memory t ⇒
do {
(l'', t') ← msel True t l' r e⇩p e cd;
(case t' of
MTValue t'' ⇒
do {
mv ← applyf (λst. accessStore l'' (memory st));
(case mv of
Some (MValue v) ⇒ return (KValue v, Value t'')
| _ ⇒ throw Err)
}
| MTArray x t'' ⇒
do {
mv ← applyf (λst. accessStore l'' (memory st));
(case mv of
Some (MPointer p) ⇒ return (KMemptr p, Memory (MTArray x t''))
| _ ⇒ throw Err)
}
)
}
| _ ⇒ throw Err)
| Some (KStoptr l') ⇒
(case tp of
Storage t ⇒
do {
(l'', t') ← ssel t l' r e⇩p e cd;
(case t' of
STValue t'' ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address e));
(case so of
Some s ⇒ return (KValue (accessStorage t'' l'' s), Value t'')
| None ⇒ throw Err)
}
| STArray _ _ ⇒ return (KStoptr l'', Storage t')
| STMap _ _ ⇒ return (KStoptr l'', Storage t'))
}
| _ ⇒ throw Err)
| _ ⇒ throw Err)
}
| Some (tp, (Storeloc l)) ⇒
(case tp of
Storage t ⇒
do {
(l', t') ← ssel t l r e⇩p e cd;
(case t' of
STValue t'' ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address e));
(case so of
Some s ⇒ return (KValue (accessStorage t'' l' s), Value t'')
| None ⇒ throw Err)
}
| STArray _ _ ⇒ return (KStoptr l', Storage t')
| STMap _ _ ⇒ return (KStoptr l', Storage t'))
}
| _ ⇒ throw Err)
| None ⇒ throw Err) st"
| "stmt SKIP e⇩p e cd st = gascheck (costs SKIP e⇩p e cd) st"
| "stmt (ASSIGN lv ex) e⇩p env cd st =
(do {
gascheck (costs (ASSIGN lv ex) e⇩p env cd);
re ← expr ex e⇩p env cd;
(case re of
(KValue v, Value t) ⇒
do {
rl ← lexp lv e⇩p env cd;
(case rl of
(LStackloc l, Value t') ⇒
(case convert t t' v of
Some (v', _) ⇒ modify (λst. st ⦇stack := updateStore l (KValue v') (stack st)⦈)
| None ⇒ throw Err)
| (LStoreloc l, Storage (STValue t')) ⇒
(case convert t t' v of
Some (v', _) ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address env));
(case so of
Some s ⇒ modify (λst. st⦇storage := fmupd (address env) (fmupd l v' s) (storage st)⦈)
| None ⇒ throw Err)
}
| None ⇒ throw Err)
| (LMemloc l, Memory (MTValue t')) ⇒
(case convert t t' v of
Some (v', _) ⇒ modify (λst. st⦇memory := updateStore l (MValue v') (memory st)⦈)
| None ⇒ throw Err)
| _ ⇒ throw Err)
}
| (KCDptr p, Calldata (MTArray x t)) ⇒
do {
rl ← lexp lv e⇩p env cd;
(case rl of
(LStackloc l, Memory _) ⇒ modify (λst. st ⦇stack := updateStore l (KCDptr p) (stack st)⦈)
| (LStackloc l, Storage _) ⇒
do {
sv ← applyf (λst. accessStore l (stack st));
(case sv of
Some (KStoptr p') ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address env));
(case so of
Some s ⇒
(case cpm2s p p' x t cd s of
Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
| None ⇒ throw Err)
| None ⇒ throw Err)
}
| _ ⇒ throw Err)
}
| (LStoreloc l, _) ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address env));
(case so of
Some s ⇒
(case cpm2s p l x t cd s of
Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
| None ⇒ throw Err)
| None ⇒ throw Err)
}
| (LMemloc l, _) ⇒
do {
cs ← applyf (λst. cpm2m p l x t cd (memory st));
(case cs of
Some m ⇒ modify (λst. st ⦇memory := m⦈)
| None ⇒ throw Err)
}
| _ ⇒ throw Err)
}
| (KMemptr p, Memory (MTArray x t)) ⇒
do {
rl ← lexp lv e⇩p env cd;
(case rl of
(LStackloc l, Memory _) ⇒ modify (λst. st⦇stack := updateStore l (KMemptr p) (stack st)⦈)
| (LStackloc l, Storage _) ⇒
do {
sv ← applyf (λst. accessStore l (stack st));
(case sv of
Some (KStoptr p') ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address env));
(case so of
Some s ⇒
do {
cs ← applyf (λst. cpm2s p p' x t (memory st) s);
(case cs of
Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
| None ⇒ throw Err)
}
| None ⇒ throw Err)
}
| _ ⇒ throw Err)
}
| (LStoreloc l, _) ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address env));
(case so of
Some s ⇒
do {
cs ← applyf (λst. cpm2s p l x t (memory st) s);
(case cs of
Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
| None ⇒ throw Err)
}
| None ⇒ throw Err)
}
| (LMemloc l, _) ⇒ modify (λst. st ⦇memory := updateStore l (MPointer p) (memory st)⦈)
| _ ⇒ throw Err)
}
| (KStoptr p, Storage (STArray x t)) ⇒
do {
rl ← lexp lv e⇩p env cd;
(case rl of
(LStackloc l, Memory _) ⇒
do {
sv ← applyf (λst. accessStore l (stack st));
(case sv of
Some (KMemptr p') ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address env));
(case so of
Some s ⇒
do {
cs ← applyf (λst. cps2m p p' x t s (memory st));
(case cs of
Some m ⇒ modify (λst. st⦇memory := m⦈)
| None ⇒ throw Err)
}
| None ⇒ throw Err)
}
| _ ⇒ throw Err)
}
| (LStackloc l, Storage _) ⇒ modify (λst. st⦇stack := updateStore l (KStoptr p) (stack st)⦈)
| (LStoreloc l, _) ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address env));
(case so of
Some s ⇒
(case copy p l x t s of
Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
| None ⇒ throw Err)
| None ⇒ throw Err)
}
| (LMemloc l, _) ⇒
do {
so ← applyf (λst. fmlookup (storage st) (address env));
(case so of
Some s ⇒
do {
cs ← applyf (λst. cps2m p l x t s (memory st));
(case cs of
Some m ⇒ modify (λst. st⦇memory := m⦈)
| None ⇒ throw Err)
}
| None ⇒ throw Err)
}
| _ ⇒ throw Err)
}
| (KStoptr p, Storage (STMap t t')) ⇒
do {
rl ← lexp lv e⇩p env cd;
(case rl of
(LStackloc l, _) ⇒ modify (λst. st⦇stack := updateStore l (KStoptr p) (stack st)⦈)
| _ ⇒ throw Err)
}
| _ ⇒ throw Err)
}) st"
| "stmt (COMP s1 s2) e⇩p e cd st =
(do {
gascheck (costs (COMP s1 s2) e⇩p e cd);
stmt s1 e⇩p e cd;
stmt s2 e⇩p e cd
}) st"
| "stmt (ITE ex s1 s2) e⇩p e cd st =
(do {
gascheck (costs (ITE ex s1 s2)  e⇩p e cd);
v ← expr ex e⇩p e cd;
(case v of
(KValue b, Value TBool) ⇒
(if b = ShowL⇩b⇩o⇩o⇩l True
then stmt s1 e⇩p e cd
else stmt s2 e⇩p e cd)
| _ ⇒ throw Err)
}) st"
| "stmt (WHILE ex s0) e⇩p e cd st =
(do {
gascheck (costs (WHILE ex s0) e⇩p e cd);
v ← expr ex e⇩p e cd;
(case v of
(KValue b, Value TBool) ⇒
(if b = ShowL⇩b⇩o⇩o⇩l True
then do {
stmt s0 e⇩p e cd;
stmt (WHILE ex s0) e⇩p e cd
}
else return ())
| _ ⇒ throw Err)
}) st"
| "stmt (INVOKE i xe) e⇩p e cd st =
(do {
gascheck (costs (INVOKE i xe) e⇩p e cd);
(case fmlookup e⇩p (address e) of
Some (ct, _) ⇒
(case fmlookup ct i of
Some (Method (fp, f, None)) ⇒
(let e' = ffold_init ct (emptyEnv (address e) (sender e) (svalue e)) (fmdom ct)
in (do {
st' ← applyf (λst. (st⦇stack:=emptyStore⦈));
(e'', cd', st'') ← load False fp xe e⇩p e' emptyStore st' e cd;
st''' ← get;
put st'';
stmt f e⇩p e'' cd';
modify (λst. st⦇stack:=stack st''', memory := memory st'''⦈)
}))
| _ ⇒ throw Err)
| None  ⇒ throw Err)
}) st"
(*External Method calls allow to send some money val with it*)
(*However this transfer does NOT trigger a fallback*)
| "stmt (EXTERNAL ad i xe val) e⇩p e cd st =
(do {
gascheck (costs (EXTERNAL ad i xe val) e⇩p e cd);
Some (ct, fb) ⇒
(do {
kv ← expr val e⇩p e cd;
(case kv of
(KValue v, Value t) ⇒
(case fmlookup ct i of
Some (Method (fp, f, None)) ⇒
let e' = ffold_init ct (emptyEnv adv (address e) v) (fmdom ct)
in (do {
st' ← applyf (λst. st⦇stack:=emptyStore, memory:=emptyStore⦈);
(e'', cd', st'') ← load True fp xe e⇩p e' emptyStore st' e cd;
st''' ← get;
Some acc ⇒
do {
put (st''⦇accounts := acc⦈);
stmt f e⇩p e'' cd';
modify (λst. st⦇stack:=stack st''', memory := memory st'''⦈)
}
| None ⇒ throw Err)
})
| None ⇒
do {
st' ← get;
Some acc ⇒
do {
st'' ← get;
modify (λst. st⦇accounts := acc,stack:=emptyStore, memory:=emptyStore⦈);
modify (λst. st⦇stack:=stack st'', memory := memory st''⦈)
}
| None ⇒ throw Err)
}
| _ ⇒ throw Err)
| _ ⇒ throw Err)
})
| None ⇒ throw Err)
| _ ⇒ throw Err)
}) st"
| "stmt (TRANSFER ad ex) e⇩p e cd st =
(do {
gascheck (costs (TRANSFER ad ex) e⇩p e cd);
kv ← expr ex e⇩p e cd;
(case kv of
(KValue v, Value t) ⇒
(do {
kv' ← expr ad e⇩p e cd;
(case kv' of
(do {
acs ← applyf accounts;
Some acc ⇒ (case fmlookup e⇩p adv of
Some (ct, f) ⇒
let e' = ffold_init ct (emptyEnv adv (address e) v) (fmdom ct)
in (do {
st' ← get;
modify (λst. (st⦇accounts := acc, stack:=emptyStore, memory:=emptyStore⦈));
stmt f e⇩p e' emptyStore;
modify (λst. st⦇stack:=stack st', memory := memory st'⦈)
})
| None ⇒ modify (λst. (st⦇accounts := acc⦈)))
| None ⇒ throw Err)
})
| _ ⇒ throw Err)
})
| _ ⇒ throw Err)
}) st"
| "stmt (BLOCK ((id0, tp), ex) s) e⇩p e⇩v cd st =
(do {
gascheck (costs (BLOCK ((id0, tp), ex) s) e⇩p e⇩v cd);
(case ex of
None ⇒ (do {
mem ← applyf memory;
(cd', e') ← decl id0 tp None False cd mem cd e⇩v;
stmt s e⇩p e' cd'
})
| Some ex' ⇒ (do {
(v, t) ← expr ex' e⇩p e⇩v cd;
mem ← applyf memory;
(cd', e') ← decl id0 tp (Some (v, t)) False cd mem cd e⇩v;
stmt s e⇩p e' cd'
}))
}) st"
by pat_completeness auto

subsection ‹Gas Consumption›

lemma lift_gas:
assumes "lift expr f e1 e2 e⇩p e cd st = Normal ((v, t), st4')"
and "⋀st4' v4 t4. expr e1 e⇩p e cd st = Normal ((v4, t4), st4') ⟹ gas st4' ≤ gas st"
and "⋀x1 x y xa ya x1a x1b st4' v4 t4. expr e1 e⇩p e cd st = Normal (x, y)
⟹ (xa, ya) = x
⟹ xa = KValue x1a
⟹ ya = Value x1b
⟹ expr e2 e⇩p e cd y = Normal ((v4, t4), st4')
⟹ gas st4' ≤ gas y"
shows "gas st4' ≤ gas st"
proof (cases "expr e1 e⇩p e cd st")
case (n a st')
then show ?thesis
proof (cases a)
case (Pair b c)
then show ?thesis
proof (cases b)
case (KValue v1)
then show ?thesis
proof (cases c)
case (Value t1)
then show ?thesis
proof (cases "expr e2 e⇩p e cd st'")
case r2: (n a' st'')
then show ?thesis
proof (cases a')
case p2: (Pair b c)
then show ?thesis
proof (cases b)
case v2: (KValue v2)
then show ?thesis
proof (cases c)
case t2: (Value t2)
then show ?thesis
proof (cases "f t1 t2 v1 v2")
case None
with assms n Pair KValue Value r2 p2 v2 t2 show ?thesis by simp
next
case (Some a'')
then show ?thesis
proof (cases a'')
case p3: (Pair v t)
with assms n Pair KValue Value r2 p2 v2 t2 Some have "gas st4'≤gas st''" by simp
moreover from assms n Pair KValue Value r2 p2 v2 t2 Some have "gas st''≤gas st'" by simp
moreover from assms n Pair KValue Value r2 p2 v2 t2 Some have "gas st'≤gas st" by simp
ultimately show ?thesis by arith
qed
qed
next
case (Calldata x2)
with assms n Pair KValue Value r2 p2 v2 show ?thesis by simp
next
case (Memory x3)
with assms n Pair KValue Value r2 p2 v2 show ?thesis by simp
next
case (Storage x4)
with assms n Pair KValue Value r2 p2 v2 show ?thesis by simp
qed
next
case (KCDptr x2)
with assms n Pair KValue Value r2 p2 show ?thesis by simp
next
case (KMemptr x3)
with assms n Pair KValue Value r2 p2 show ?thesis by simp
next
case (KStoptr x4)
with assms n Pair KValue Value r2 p2 show ?thesis by simp
qed
qed
next
case (e x)
with assms n Pair KValue Value show ?thesis by simp
qed
next
case (Calldata x2)
with assms n Pair KValue show ?thesis by simp
next
case (Memory x3)
with assms n Pair KValue show ?thesis by simp
next
case (Storage x4)
with assms n Pair KValue show ?thesis by simp
qed
next
case (KCDptr x2)
with assms n Pair show ?thesis by simp
next
case (KMemptr x3)
with assms n Pair show ?thesis by simp
next
case (KStoptr x4)
with assms n Pair show ?thesis by simp
qed
qed
next
case (e x)
with assms show ?thesis by simp
qed

⟹ (∀ev cd st st'. load lcp lis lxs lep lev0 lcd0 lst0 lev lcd lst = Normal ((ev, cd, st), st') ⟶ gas st ≤ gas