Theory Statements
section ‹Statements›
theory Statements
imports Expressions StateMonad
begin
locale statement_with_gas = expressions_with_gas +
fixes costs :: "S ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Gas"
assumes while_not_zero[termination_simp]: "⋀e cd st ex s0. 0 < (costs (WHILE ex s0) e cd st) "
and invoke_not_zero[termination_simp]: "⋀e cd st i xe. 0 < (costs (INVOKE i xe) e cd st)"
and external_not_zero[termination_simp]: "⋀e cd st ad i xe val. 0 < (costs (EXTERNAL ad i xe val) e cd st)"
and transfer_not_zero[termination_simp]: "⋀e cd st ex ad. 0 < (costs (TRANSFER ad ex) e cd st)"
and new_not_zero[termination_simp]: "⋀e cd st i xe val. 0 < (costs (NEW i xe val) e cd st)"
begin
subsection ‹Semantics of left expressions›
text ‹We first introduce lexp.›
fun lexp :: "L ⇒ Environment ⇒ CalldataT ⇒ State ⇒ (LType * Type, Ex, Gas) state_monad"
where "lexp (Id i) e _ st g =
(case (denvalue e) $$ i of
Some (tp, (Stackloc l)) ⇒ return (LStackloc l, tp)
| Some (tp, (Storeloc l)) ⇒ return (LStoreloc l, tp)
| _ ⇒ throw Err) g"
| "lexp (Ref i r) e cd st g =
(case (denvalue e) $$ i of
Some (tp, Stackloc l) ⇒
(case accessStore l (stack st) of
Some (KCDptr _) ⇒ throw Err
| Some (KMemptr l') ⇒
do {
t ← (case tp of Memory t ⇒ return t | _ ⇒ throw Err);
(l'', t') ← msel True t l' r e cd st;
return (LMemloc l'', Memory t')
}
| Some (KStoptr l') ⇒
do {
t ← (case tp of Storage t ⇒ return t | _ ⇒ throw Err);
(l'', t') ← ssel t l' r e cd st;
return (LStoreloc l'', Storage t')
}
| Some (KValue _) ⇒ throw Err
| None ⇒ throw Err)
| Some (tp, Storeloc l) ⇒
do {
t ← (case tp of Storage t ⇒ return t | _ ⇒ throw Err);
(l', t') ← ssel t l r e cd st;
return (LStoreloc l', Storage t')
}
| None ⇒ throw Err) g"
lemma lexp_gas[rule_format]:
"∀l5' t5' g5'. lexp l5 ev5 cd5 st5 g5 = Normal ((l5', t5'), g5') ⟶ g5' ≤ g5"
proof (induct rule: lexp.induct[where ?P="λl5 ev5 cd5 st5 g5. (∀l5' t5' g5'. lexp l5 ev5 cd5 st5 g5 = Normal ((l5', t5'), g5') ⟶ g5' ≤ g5)"])
case (1 i e uv st g)
then show ?case using lexp.simps(1) by (simp split: option.split Denvalue.split prod.split)
next
case (2 i r e cd st g)
show ?case
proof (rule allI[THEN allI, THEN allI, OF impI])
fix st5' xa xaa
assume a1: "lexp (Ref i r) e cd st g = Normal ((st5', xa), xaa)"
then show "xaa ≤ g"
proof (cases "fmlookup (denvalue e) i")
case None
with a1 show ?thesis using lexp.simps(2) by simp
next
case (Some a)
then show ?thesis
proof (cases a)
case (Pair tp b)
then show ?thesis
proof (cases b)
case (Stackloc l)
then show ?thesis
proof (cases "accessStore l (stack st)")
case None
with a1 Some Pair Stackloc show ?thesis using lexp.psimps(2) by simp
next
case s2: (Some a)
then show ?thesis
proof (cases a)
case (KValue x1)
with a1 Some Pair Stackloc s2 show ?thesis using lexp.psimps(2) by simp
next
case (KCDptr x2)
with a1 Some Pair Stackloc s2 show ?thesis using lexp.psimps(2) by simp
next
case (KMemptr l')
then show ?thesis
proof (cases tp)
case (Value _)
with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.simps(2) by simp
next
case (Calldata _)
with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.simps(2) by simp
next
case (Memory t)
then show ?thesis
proof (cases "msel True t l' r e cd st g")
case (n _ _)
with 2 a1 Some Pair Stackloc s2 KMemptr Memory show ?thesis using msel_ssel_expr_load_rexp_gas(1) by (simp split: prod.split_asm)
next
case (e _)
with a1 Some Pair Stackloc s2 KMemptr Memory show ?thesis using lexp.psimps(2) by simp
qed
next
case (Storage _)
with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.psimps(2) by simp
qed
next
case (KStoptr l')
then show ?thesis
proof (cases tp)
case (Value _)
with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp
next
case (Calldata _)
with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp
next
case (Memory _)
with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp
next
case (Storage t)
then show ?thesis
proof (cases "ssel t l' r e cd st g")
case (n _ _)
with a1 Some Pair Stackloc s2 KStoptr Storage show ?thesis using msel_ssel_expr_load_rexp_gas(2) by (auto split: prod.split_asm)
next
case (e _)
with a1 Some Pair Stackloc s2 KStoptr Storage show ?thesis using lexp.psimps(2) by simp
qed
qed
qed
qed
next
case (Storeloc l)
then show ?thesis
proof (cases tp)
case (Value _)
with a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp
next
case (Calldata _)
with a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp
next
case (Memory _)
with a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp
next
case (Storage t)
then show ?thesis
proof (cases "ssel t l r e cd st g")
case (n _ _)
with a1 Some Pair Storeloc Storage show ?thesis using msel_ssel_expr_load_rexp_gas(2) by (auto split: prod.split_asm)
next
case (e _)
with a1 Some Pair Storeloc Storage show ?thesis using lexp.psimps(2) by simp
qed
qed
qed
qed
qed
qed
qed
subsection ‹Semantics of statements›
text ‹The following is a helper function to connect the gas monad with the state monad.›
fun
toState :: "(State ⇒ ('a, 'e, Gas) state_monad) ⇒ ('a, 'e, State) state_monad" where
"toState gm = (λs. case gm s (gas s) of
Normal (a,g) ⇒ Normal(a,s⦇gas:=g⦈)
| Exception e ⇒ Exception e)"
lemma wptoState[wprule]:
assumes "⋀a g. gm s (gas s) = Normal (a, g) ⟹ P a (s⦇gas:=g⦈)"
and "⋀e. gm s (gas s) = Exception e ⟹ E e"
shows "wp (toState gm) P E s"
using assms unfolding wp_def by (simp split:result.split result.split_asm)
text ‹Now we define the semantics of statements.›
function (domintros) stmt :: "S ⇒ Environment ⇒ CalldataT ⇒ (unit, Ex, State) state_monad"
where "stmt SKIP e cd st =
(do {
assert Gas (λst. gas st > costs SKIP e cd st);
modify (λst. st⦇gas := gas st - costs SKIP e cd st⦈)
}) st"
| "stmt (ASSIGN lv ex) env cd st =
(do {
assert Gas (λst. gas st > costs (ASSIGN lv ex) env cd st);
modify (λst. st⦇gas := gas st - costs (ASSIGN lv ex) env cd st⦈);
re ← toState (expr ex env cd);
case re of
(KValue v, Value t) ⇒
do {
rl ← toState (lexp lv env cd);
case rl of
(LStackloc l, Value t') ⇒
do {
v' ← option Err (λ_. convert t t' v);
modify (λst. st ⦇stack := updateStore l (KValue v') (stack st)⦈)
}
| (LStoreloc l, Storage (STValue t')) ⇒
do {
v' ← option Err (λ_. convert t t' v);
modify (λst. st⦇storage := (storage st) (address env := fmupd l v' (storage st (address env)))⦈)
}
| (LMemloc l, Memory (MTValue t')) ⇒
do {
v' ← option Err (λ_. convert t t' v);
modify (λst. st⦇memory := updateStore l (MValue v') (memory st)⦈)
}
| _ ⇒ throw Err
}
| (KCDptr p, Calldata (MTArray x t)) ⇒
do {
rl ← toState (lexp lv env cd);
case rl of
(LStackloc l, Memory _) ⇒
do {
sv ← applyf (λst. accessStore l (stack st));
p' ← case sv of Some (KMemptr p') ⇒ return p' | _ ⇒ throw Err;
m ← option Err (λst. cpm2m p p' x t cd (memory st));
modify (λst. st⦇memory := m⦈)
}
| (LStackloc l, Storage _) ⇒
do {
sv ← applyf (λst. accessStore l (stack st));
p' ← case sv of Some (KStoptr p') ⇒ return p' | _ ⇒ throw Err;
s ← option Err (λst. cpm2s p p' x t cd (storage st (address env)));
modify (λst. st ⦇storage := (storage st) (address env := s)⦈)
}
| (LStoreloc l, _) ⇒
do {
s ← option Err (λst. cpm2s p l x t cd (storage st (address env)));
modify (λst. st ⦇storage := (storage st) (address env := s)⦈)
}
| (LMemloc l, _) ⇒
do {
m ← option Err (λst. cpm2m p l x t cd (memory st));
modify (λst. st ⦇memory := m⦈)
}
| _ ⇒ throw Err
}
| (KMemptr p, Memory (MTArray x t)) ⇒
do {
rl ← toState (lexp lv 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));
p' ← case sv of Some (KStoptr p') ⇒ return p' | _ ⇒ throw Err;
s ← option Err (λst. cpm2s p p' x t (memory st) (storage st (address env)));
modify (λst. st ⦇storage := (storage st) (address env := s)⦈)
}
| (LStoreloc l, _) ⇒
do {
s ← option Err (λst. cpm2s p l x t (memory st) (storage st (address env)));
modify (λst. st ⦇storage := (storage st) (address env := s)⦈)
}
| (LMemloc l, _) ⇒ modify (λst. st ⦇memory := updateStore l (MPointer p) (memory st)⦈)
| _ ⇒ throw Err
}
| (KStoptr p, Storage (STArray x t)) ⇒
do {
rl ← toState (lexp lv env cd);
case rl of
(LStackloc l, Memory _) ⇒
do {
sv ← applyf (λst. accessStore l (stack st));
p' ← case sv of Some (KMemptr p') ⇒ return p' | _ ⇒ throw Err;
m ← option Err (λst. cps2m p p' x t (storage st (address env)) (memory st));
modify (λst. st⦇memory := m⦈)
}
| (LStackloc l, Storage _) ⇒ modify (λst. st⦇stack := updateStore l (KStoptr p) (stack st)⦈)
| (LStoreloc l, _) ⇒
do {
s ← option Err (λst. copy p l x t (storage st (address env)));
modify (λst. st ⦇storage := (storage st) (address env := s)⦈)
}
| (LMemloc l, _) ⇒
do {
m ← option Err (λst. cps2m p l x t (storage st (address env)) (memory st));
modify (λst. st⦇memory := m⦈)
}
| _ ⇒ throw Err
}
| (KStoptr p, Storage (STMap t t')) ⇒
do {
rl ← toState (lexp lv env cd);
l ← case rl of (LStackloc l, _) ⇒ return l | _ ⇒ throw Err;
modify (λst. st⦇stack := updateStore l (KStoptr p) (stack st)⦈)
}
| _ ⇒ throw Err
}) st"
| "stmt (COMP s1 s2) e cd st =
(do {
assert Gas (λst. gas st > costs (COMP s1 s2) e cd st);
modify (λst. st⦇gas := gas st - costs (COMP s1 s2) e cd st⦈);
stmt s1 e cd;
stmt s2 e cd
}) st"
| "stmt (ITE ex s1 s2) e cd st =
(do {
assert Gas (λst. gas st > costs (ITE ex s1 s2) e cd st);
modify (λst. st⦇gas := gas st - costs (ITE ex s1 s2) e cd st⦈);
v ← toState (expr ex e cd);
b ← (case v of (KValue b, Value TBool) ⇒ return b | _ ⇒ throw Err);
if b = ShowL⇩b⇩o⇩o⇩l True then stmt s1 e cd
else if b = ShowL⇩b⇩o⇩o⇩l False then stmt s2 e cd
else throw Err
}) st"
| "stmt (WHILE ex s0) e cd st =
(do {
assert Gas (λst. gas st > costs (WHILE ex s0) e cd st);
modify (λst. st⦇gas := gas st - costs (WHILE ex s0) e cd st⦈);
v ← toState (expr ex e cd);
b ← (case v of (KValue b, Value TBool) ⇒ return b | _ ⇒ throw Err);
if b = ShowL⇩b⇩o⇩o⇩l True then
do {
stmt s0 e cd;
stmt (WHILE ex s0) e cd
}
else if b = ShowL⇩b⇩o⇩o⇩l False then return ()
else throw Err
}) st"
| "stmt (INVOKE i xe) e cd st =
(do {
assert Gas (λst. gas st > costs (INVOKE i xe) e cd st);
modify (λst. st⦇gas := gas st - costs (INVOKE i xe) e cd st⦈);
(ct, _) ← option Err (λ_. ep $$ contract e);
(fp, f) ← case ct $$ i of Some (Method (fp, False, f)) ⇒ return (fp, f) | _ ⇒ throw Err;
let e' = ffold_init ct (emptyEnv (address e) (contract e) (sender e) (svalue e)) (fmdom ct);
m⇩o ← applyf memory;
(e⇩l, cd⇩l, k⇩l, m⇩l) ← toState (load False fp xe e' emptyStore emptyStore m⇩o e cd);
k⇩o ← applyf stack;
modify (λst. st⦇stack:=k⇩l, memory:=m⇩l⦈);
stmt f e⇩l cd⇩l;
modify (λst. st⦇stack:=k⇩o⦈)
}) st"
| "stmt (EXTERNAL ad i xe val) e cd st =
(do {
assert Gas (λst. gas st > costs (EXTERNAL ad i xe val) e cd st);
modify (λst. st⦇gas := gas st - costs (EXTERNAL ad i xe val) e cd st⦈);
kad ← toState (expr ad e cd);
adv ← case kad of (KValue adv, Value TAddr) ⇒ return adv | _ ⇒ throw Err;
assert Err (λ_. adv ≠ address e);
c ← (λst. case type (accounts st adv) of Some (Contract c) ⇒ return c st | _ ⇒ throw Err st);
(ct, _, fb) ← option Err (λ_. ep $$ c);
kv ← toState (expr val e cd);
(v, t) ← case kv of (KValue v, Value t) ⇒ return (v, t) | _ ⇒ throw Err;
v' ← option Err (λ_. convert t (TUInt 256) v);
let e' = ffold_init ct (emptyEnv adv c (address e) v') (fmdom ct);
case ct $$ i of
Some (Method (fp, True, f)) ⇒
do {
(e⇩l, cd⇩l, k⇩l, m⇩l) ← toState (load True fp xe e' emptyStore emptyStore emptyStore e cd);
acc ← option Err (λst. transfer (address e) adv v' (accounts st));
(k⇩o, m⇩o) ← applyf (λst. (stack st, memory st));
modify (λst. st⦇accounts := acc, stack:=k⇩l,memory:=m⇩l⦈);
stmt f e⇩l cd⇩l;
modify (λst. st⦇stack:=k⇩o, memory := m⇩o⦈)
}
| None ⇒
do {
acc ← option Err (λst. transfer (address e) adv v' (accounts st));
(k⇩o, m⇩o) ← applyf (λst. (stack st, memory st));
modify (λst. st⦇accounts := acc,stack:=emptyStore, memory:=emptyStore⦈);
stmt fb e' emptyStore;
modify (λst. st⦇stack:=k⇩o, memory := m⇩o⦈)
}
| _ ⇒ throw Err
}) st"
| "stmt (TRANSFER ad ex) e cd st =
(do {
assert Gas (λst. gas st > costs (TRANSFER ad ex) e cd st);
modify (λst. st⦇gas := gas st - costs (TRANSFER ad ex) e cd st⦈);
kv ← toState (expr ad e cd);
adv ← case kv of (KValue adv, Value TAddr) ⇒ return adv | _ ⇒ throw Err;
kv' ← toState (expr ex e cd);
(v, t) ← case kv' of (KValue v, Value t) ⇒ return (v, t) | _ ⇒ throw Err;
v' ← option Err (λ_. convert t (TUInt 256) v);
acc ← applyf accounts;
case type (acc adv) of
Some (Contract c) ⇒
do {
(ct, _, f) ← option Err (λ_. ep $$ c);
let e' = ffold_init ct (emptyEnv adv c (address e) v') (fmdom ct);
(k⇩o, m⇩o) ← applyf (λst. (stack st, memory st));
acc' ← option Err (λst. transfer (address e) adv v' (accounts st));
modify (λst. st⦇accounts := acc', stack:=emptyStore, memory:=emptyStore⦈);
stmt f e' emptyStore;
modify (λst. st⦇stack:=k⇩o, memory := m⇩o⦈)
}
| Some EOA ⇒
do {
acc' ← option Err (λst. transfer (address e) adv v' (accounts st));
modify (λst. (st⦇accounts := acc'⦈))
}
| None ⇒ throw Err
}) st"
| "stmt (BLOCK ((id0, tp), None) s) e⇩v cd st =
(do {
assert Gas (λst. gas st > costs (BLOCK ((id0, tp), None) s) e⇩v cd st);
modify (λst. st⦇gas := gas st - costs (BLOCK ((id0, tp), None) s) e⇩v cd st⦈);
(cd', mem', sck', e') ← option Err (λst. decl id0 tp None False cd (memory st) (storage st) (cd, memory st, stack st, e⇩v));
modify (λst. st⦇stack := sck', memory := mem'⦈);
stmt s e' cd'
}) st"
| "stmt (BLOCK ((id0, tp), Some ex') s) e⇩v cd st =
(do {
assert Gas (λst. gas st > costs(BLOCK ((id0, tp), Some ex') s) e⇩v cd st);
modify (λst. st⦇gas := gas st - costs (BLOCK ((id0, tp), Some ex') s) e⇩v cd st⦈);
(v, t) ← toState (expr ex' e⇩v cd);
(cd', mem', sck', e') ← option Err (λst. decl id0 tp (Some (v, t)) False cd (memory st) (storage st) (cd, memory st, stack st, e⇩v));
modify (λst. st⦇stack := sck', memory := mem'⦈);
stmt s e' cd'
}) st"
| "stmt (NEW i xe val) e cd st =
(do {
assert Gas (λst. gas st > costs (NEW i xe val) e cd st);
modify (λst. st⦇gas := gas st - costs (NEW i xe val) e cd st⦈);
adv ← applyf (λst. hash (address e) (ShowL⇩n⇩a⇩t (contracts (accounts st (address e)))));
assert Err (λst. type (accounts st adv) = None);
kv ← toState (expr val e cd);
(v, t) ← case kv of (KValue v, Value t) ⇒ return (v, t) | _ ⇒ throw Err;
(ct, cn, _) ← option Err (λ_. ep $$ i);
let e' = ffold_init ct (emptyEnv adv i (address e) v) (fmdom ct);
(e⇩l, cd⇩l, k⇩l, m⇩l) ← toState (load True (fst cn) xe e' emptyStore emptyStore emptyStore e cd);
modify (λst. st⦇accounts := (accounts st)(adv := ⦇bal = ShowL⇩i⇩n⇩t 0, type = Some (Contract i), contracts = 0⦈), storage:=(storage st)(adv := {$$})⦈);
acc ← option Err (λst. transfer (address e) adv v (accounts st));
(k⇩o, m⇩o) ← applyf (λst. (stack st, memory st));
modify (λst. st⦇accounts := acc, stack:=k⇩l, memory:=m⇩l⦈);
stmt (snd cn) e⇩l cd⇩l;
modify (λst. st⦇stack:=k⇩o, memory := m⇩o⦈);
modify (incrementAccountContracts (address e))
}) st"
by pat_completeness auto
subsection ‹Termination›
text ‹Again, to prove termination we need a lemma regarding gas consumption.›
lemma stmt_dom_gas[rule_format]:
"stmt_dom (s6, ev6, cd6, st6) ⟹ (∀st6'. stmt s6 ev6 cd6 st6 = Normal((), st6') ⟶ gas st6' ≤ gas st6)"
proof (induct rule: stmt.pinduct[where ?P="λs6 ev6 cd6 st6. (∀st6'. stmt s6 ev6 cd6 st6 = Normal ((), st6') ⟶ gas st6' ≤ gas st6)"])
case (1 e cd st)
then show ?case using stmt.psimps(1) by simp
next
case (2 lv ex env cd st)
define g where "g = costs (ASSIGN lv ex) env cd st"
show ?case
proof (rule allI[OF impI])
fix st6'
assume stmt_def: "stmt (ASSIGN lv ex) env cd st = Normal ((), st6')"
then show "gas st6' ≤ gas st"
proof cases
assume "gas st ≤ g"
with 2(1) stmt_def show ?thesis using stmt.psimps(2) g_def by simp
next
assume "¬ gas st ≤ g"
define st' where "st' = st⦇gas := gas st - g⦈"
show ?thesis
proof (cases "expr ex env cd st' (gas st - g)")
case (n a g')
define st'' where "st'' = st'⦇gas := g'⦈"
then show ?thesis
proof (cases a)
case (Pair b c)
then show ?thesis
proof (cases b)
case (KValue v)
then show ?thesis
proof (cases c)
case (Value t)
then show ?thesis
proof (cases "lexp lv env cd st'' g'")
case n2: (n a g'')
then show ?thesis
proof (cases a)
case p1: (Pair a b)
then show ?thesis
proof (cases a)
case (LStackloc l)
then show ?thesis
proof (cases b)
case v2: (Value t')
then show ?thesis
proof (cases "convert t t' v ")
case None
with stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStackloc v2 show ?thesis using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def by simp
next
case s3: (Some v')
with 2(1) `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStackloc v2 s3
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''⦇gas := g'', stack := updateStore l (KValue v') (stack st)⦈)"
using stmt.psimps(2) g_def st'_def st''_def by simp
with stmt_def have "st6'= st''⦇gas := g'', stack := updateStore l (KValue v') (stack st)⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n2 p1 have "gas (st''⦇gas := g'', stack := updateStore l (KValue v') (stack st)⦈) ≤ gas (st'⦇gas := g'⦈)" using g_def st'_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair KValue Value have "gas (st'⦇gas := g'⦈) ≤ gas (st⦇gas := gas st - g⦈)" using g_def by simp
ultimately show ?thesis by simp
qed
next
case (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Memory x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Storage x4)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (LMemloc l)
then show ?thesis
proof (cases b)
case v2: (Value t')
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Memory x3)
then show ?thesis
proof (cases x3)
case (MTArray x11 x12)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LMemloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (MTValue t')
then show ?thesis
proof (cases "convert t t' v ")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LMemloc Memory MTValue show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case s3: (Some v')
with 2(1) `¬ gas st ≤ g` n Pair KValue Value n2 p1 LMemloc Memory MTValue s3
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''⦇gas := g'', memory := updateStore l (MValue v') (memory st'')⦈)"
using stmt.psimps(2) g_def st'_def st''_def by simp
with stmt_def have "st6'= (st''⦇gas := g'', memory := updateStore l (MValue v') (memory st'')⦈)" by simp
moreover from lexp_gas `¬ gas st ≤ g` n2 p1 have "gas (st''⦇gas := g'', stack := updateStore l (KValue v') (stack st)⦈) ≤ gas (st'⦇gas := g'⦈)" using g_def st'_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair KValue Value n2 p1 have "gas (st'⦇gas := g'⦈) ≤ gas (st⦇gas := gas st - g⦈)" using g_def by simp
ultimately show ?thesis by simp
qed
qed
next
case (Storage x4)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (LStoreloc l)
then show ?thesis
proof (cases b)
case v2: (Value t')
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Memory x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Storage x4)
then show ?thesis
proof (cases x4)
case (STArray x11 x12)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStoreloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (STMap x21 x22)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStoreloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (STValue t')
then show ?thesis
proof (cases "convert t t' v ")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStoreloc Storage STValue show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case s3: (Some v')
with 2(1) `¬ gas st ≤ g` n Pair KValue Value n2 p1 LStoreloc Storage STValue s3
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'' ⦇gas := g'', storage := (storage st'') (address env := fmupd l v' (storage st'' (address env)))⦈)"
using stmt.psimps(2) g_def st'_def st''_def by simp
with stmt_def have "st6'= st'' ⦇gas := g'', storage := (storage st'') (address env := fmupd l v' (storage st'' (address env)))⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KValue Value n2 p1 have "gas (st''⦇gas := g'', stack := updateStore l (KValue v') (stack st)⦈) ≤ gas (st'⦇gas := g'⦈)" using g_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair KValue Value n2 p1 have "gas (st'⦇gas := g'⦈) ≤ gas (st⦇gas := gas st - g⦈)" using g_def by simp
ultimately show ?thesis by simp
qed
qed
qed
qed
qed
next
case (e x)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp
next
case (Memory x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp
next
case (Storage x4)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp
qed
next
case (KCDptr p)
then show ?thesis
proof (cases c)
case (Value x1)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def by simp
next
case (Calldata x2)
then show ?thesis
proof (cases x2)
case (MTArray x t)
then show ?thesis
proof (cases "lexp lv env cd st'' g'")
case n2: (n a g'')
define st''' where "st''' = st''⦇gas := g''⦈"
then show ?thesis
proof (cases a)
case p2: (Pair a b)
then show ?thesis
proof (cases a)
case (LStackloc l)
then show ?thesis
proof (cases b)
case v2: (Value t')
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case c2: (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Memory x3)
then show ?thesis
proof (cases "accessStore l (stack st''')")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case s3: (Some a)
then show ?thesis
proof (cases a)
case (KValue x1)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case c3: (KCDptr x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (KMemptr p')
then show ?thesis
proof (cases "cpm2m p p' x t cd (memory st''')")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by (simp split:if_split_asm)
next
case (Some m')
with `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 KMemptr
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇memory := m'⦈)"
using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st''' ⦇memory := m'⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 have "gas (st'''⦇memory := m'⦈) ≤ gas st''" using st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
next
case (KStoptr p')
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
qed
qed
next
case (Storage x4)
then show ?thesis
proof (cases "accessStore l (stack st'')")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case s3: (Some a)
then show ?thesis
proof (cases a)
case (KValue x1)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case c3: (KCDptr x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (KMemptr x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (KStoptr p')
then show ?thesis
proof (cases "cpm2s p p' x t cd (storage st'' (address env))")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (Some s')
with 2(1) `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 KStoptr
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇storage := (storage st'') (address env := s')⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st''' ⦇storage := (storage st'') (address env := s')⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st''' ≤ gas st''" using g_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using g_def st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
qed
qed
qed
next
case (LMemloc l)
then show ?thesis
proof (cases "cpm2m p l x t cd (memory st''')")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by (simp split:if_split_asm)
next
case (Some m)
with `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LMemloc
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇memory := m⦈)"
using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= (st'''⦇memory := m⦈)" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st''' ≤ gas st''" using st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
next
case (LStoreloc l)
then show ?thesis
proof (cases "cpm2s p l x t cd (storage st'' (address env))")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (Some s)
with `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 LStoreloc
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇storage := (storage st'') (address env := s)⦈)"
using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= (st'''⦇storage := (storage st'') (address env := s)⦈)" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st''' ≤ gas st''" using st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
qed
qed
next
case (e x)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata MTArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (MTValue x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr Calldata show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (Memory x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Storage x4)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (KMemptr p)
then show ?thesis
proof (cases c)
case (Value x1)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Memory x3)
then show ?thesis
proof (cases x3)
case (MTArray x t)
then show ?thesis
proof (cases "lexp lv env cd st'' g'")
case n2: (n a g'')
define st''' where "st''' = st''⦇gas := g''⦈"
then show ?thesis
proof (cases a)
case p2: (Pair a b)
then show ?thesis
proof (cases a)
case (LStackloc l)
then show ?thesis
proof (cases b)
case v2: (Value t')
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case c2: (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case m2: (Memory x3)
with 2(1) `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇stack := updateStore l (KMemptr p) (stack st'')⦈)"
using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st'''⦇stack := updateStore l (KMemptr p) (stack st'')⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 have "gas st''' ≤ gas st''" using st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
next
case (Storage x4)
then show ?thesis
proof (cases "accessStore l (stack st''')")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case s3: (Some a)
then show ?thesis
proof (cases a)
case (KValue x1)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case c3: (KCDptr x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case m3: (KMemptr x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (KStoptr p')
then show ?thesis
proof (cases "cpm2s p p' x t (memory st''') (storage st''' (address env))")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (Some s)
with 2(1) `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 KStoptr
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇storage := (storage st''') (address env := s)⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st'''⦇storage := (storage st''') (address env := s)⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 have "gas st''' ≤ gas st''" using g_def st'_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
qed
qed
qed
next
case (LMemloc l)
with 2(1) `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LMemloc
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇memory := updateStore l (MPointer p) (memory st''')⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st'''⦇memory := updateStore l (MPointer p) (memory st''')⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 have "gas st''' ≤ gas st''" using g_def st'_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
next
case (LStoreloc l)
then show ?thesis
proof (cases "cpm2s p l x t (memory st''') (storage st'' (address env))")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def using st'_def st''_def st'''_def by simp
next
case (Some s)
with 2(1) `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 LStoreloc
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇storage := (storage st''') (address env := s)⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st'''⦇storage := (storage st''') (address env := s)⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KMemptr Memory MTArray n2 p2 have "gas st''' ≤ gas st''" using g_def st'_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
qed
qed
next
case (e _)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory MTArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (MTValue _)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (Storage x4)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (KStoptr p)
then show ?thesis
proof (cases c)
case (Value x1)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Memory x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Storage x4)
then show ?thesis
proof (cases x4)
case (STArray x t)
then show ?thesis
proof (cases "lexp lv env cd st'' g'")
case n2: (n a g'')
define st''' where "st''' = st''⦇gas := g''⦈"
then show ?thesis
proof (cases a)
case p2: (Pair a b)
then show ?thesis
proof (cases a)
case (LStackloc l)
then show ?thesis
proof (cases b)
case v2: (Value t')
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case c2: (Calldata x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (Memory x3)
then show ?thesis
proof (cases "accessStore l (stack st''')")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case s3: (Some a)
then show ?thesis
proof (cases a)
case (KValue x1)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case c3: (KCDptr x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (KMemptr p')
then show ?thesis
proof (cases "cps2m p p' x t (storage st''' (address env)) (memory st''')")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (Some m)
with 2(1) `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 KMemptr
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇memory := m⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st'''⦇memory := m⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KMemptr Storage STArray n2 p2 have "gas (st'''⦇memory := m⦈) ≤ gas st''" using g_def st'_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
next
case sp2: (KStoptr p')
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
qed
qed
next
case st2: (Storage x4)
with 2(1) `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStackloc
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇stack := updateStore l (KStoptr p) (stack st''')⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st'''⦇stack := updateStore l (KStoptr p) (stack st''')⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''⦇stack := updateStore l (KStoptr p) (stack st''')⦈) ≤ gas st''" using g_def st'_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
next
case (LMemloc l)
then show ?thesis
proof (cases "cps2m p l x t (storage st'' (address env)) (memory st'')")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (Some m)
with 2(1) `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LMemloc
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇memory := m⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= (st'''⦇memory := m⦈)" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''⦇memory := m⦈) ≤ gas st''" using g_def st'_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
next
case (LStoreloc l)
then show ?thesis
proof (cases "copy p l x t (storage st'' (address env))")
case None
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
next
case (Some s)
with 2(1) `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 LStoreloc
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''⦇storage := (storage st''') (address env := s)⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st'''⦇storage := (storage st''') (address env := s)⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''⦇storage := (storage st''') (address env := s')⦈) ≤ gas st''" using g_def st'_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
qed
qed
qed
next
case (e x)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (STMap t t')
then show ?thesis
proof (cases "lexp lv env cd st'' g'")
case n2: (n a g'')
define st''' where "st''' = st''⦇gas := g''⦈"
then show ?thesis
proof (cases a)
case p2: (Pair a b)
then show ?thesis
proof (cases a)
case (LStackloc l)
with 2(1) `¬ gas st ≤ g` n Pair KStoptr Storage STMap n2 p2
have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇stack := updateStore l (KStoptr p) (stack st''')⦈)"
using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
with stmt_def have "st6'= st'''⦇stack := updateStore l (KStoptr p) (stack st''')⦈" by simp
moreover from lexp_gas `¬ gas st ≤ g` n Pair KStoptr Storage STMap n2 p2 have "gas (st'''⦇stack := updateStore l (KStoptr p) (stack st''')⦈) ≤ gas st''" using g_def st'_def st''_def st'''_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st ≤ g` n Pair have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
next
case (LMemloc x2)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STMap n2 p2 show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
next
case (LStoreloc x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STMap n2 p2 show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
qed
next
case (e x)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage STMap show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
next
case (STValue x3)
with 2(1) stmt_def `¬ gas st ≤ g` n Pair KStoptr Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
qed
qed
qed
qed
next
case (e x)
with 2(1) stmt_def `¬ gas st ≤ g` show ?thesis using stmt.psimps(2) g_def st'_def by simp
qed
qed
qed
next
case (3 s1 s2 e cd st)
define g where "g = costs (COMP s1 s2) e cd st"
show ?case
proof (rule allI[OF impI])
fix st6'
assume stmt_def: "stmt (COMP s1 s2) e cd st = Normal ((), st6')"
then show "gas st6' ≤ gas st"
proof cases
assume "gas st ≤ g"
with 3(1) stmt_def g_def show ?thesis using stmt.psimps(3) by simp
next
assume "¬ gas st ≤ g"
show ?thesis
proof (cases "stmt s1 e cd (st⦇gas := gas st - g⦈)")
case (n a st')
with 3(1) stmt_def `¬ gas st ≤ g` have "stmt (COMP s1 s2) e cd st = stmt s2 e cd st'" using stmt.psimps(3)[of s1 s2 e cd st] g_def by (simp add:Let_def split:unit.split_asm)
with 3(3) stmt_def ‹¬ gas st ≤ g› n have "gas st6' ≤ gas st'" using g_def by simp
moreover from 3(2)[where ?s'a="st⦇gas := gas st - g⦈"] ‹¬ gas st ≤ g› n have "gas st' ≤ gas st" using g_def by simp
ultimately show ?thesis by simp
next
case (e x)
with 3 stmt_def `¬ gas st ≤ g` show ?thesis using stmt.psimps(3)[of s1 s2 e cd st] g_def by (simp split: Ex.split_asm)
qed
qed
qed
next
case (4 ex s1 s2 e cd st)
define g where "g = costs (ITE ex s1 s2) e cd st"
show ?case
proof (rule allI[OF impI])
fix st6'
assume stmt_def: "stmt (ITE ex s1 s2) e cd st = Normal ((), st6')"
then show "gas st6' ≤ gas st"
proof cases
assume "gas st ≤ g"
with 4(1) stmt_def show ?thesis using stmt.psimps(4) g_def by simp
next
assume "¬ gas st ≤ g"
then have l1: "assert Gas (λst. costs (ITE ex s1 s2) e cd st < gas st) st = Normal ((), st) " using g_def by simp
define st' where "st' = st⦇gas := gas st - g⦈"
then have l2: " modify (λst. st⦇gas := gas st - costs (ITE ex s1 s2) e cd st⦈) st = Normal ((), st')" using g_def by simp
show ?thesis
proof (cases "expr ex e cd st' (gas st - g)")
case (n a g')
define st'' where "st'' = st'⦇gas := g'⦈"
with n have l3: "toState (expr ex e cd) st' = Normal (a, st'')" using st'_def by simp
then show ?thesis
proof (cases a)
case (Pair b c)
then show ?thesis
proof (cases b)
case (KValue b)
then show ?thesis
proof (cases c)
case (Value x1)
then show ?thesis
proof (cases x1)
case (TSInt x1)
with 4(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def by simp
next
case (TUInt x2)
with 4(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def by simp
next
case TBool
then show ?thesis
proof cases
assume "b = ShowL⇩b⇩o⇩o⇩l True"
with 4(1) `¬ gas st ≤ g` n Pair KValue Value TBool have "stmt (ITE ex s1 s2) e cd st = stmt s1 e cd st''" using stmt.psimps(4) g_def st'_def st''_def by simp
with 4(2)[OF l1 l2 l3] stmt_def `¬ gas st ≤ g` n Pair KValue Value TBool `b = ShowL⇩b⇩o⇩o⇩l True` have "gas st6' ≤ gas st''" using g_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `¬ gas st ≤ g` n Pair KValue Value TBool have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
next
assume nt: "¬ b = ShowL⇩b⇩o⇩o⇩l True"
show ?thesis
proof cases
assume "b = ShowL⇩b⇩o⇩o⇩l False"
with 4(1) `¬ gas st ≤ g` n Pair KValue Value TBool nt have "stmt (ITE ex s1 s2) e cd st = stmt s2 e cd st''" using stmt.psimps(4) g_def st'_def st''_def by simp
with 4(3)[OF l1 l2 l3] stmt_def `¬ gas st ≤ g` n Pair KValue Value TBool nt `b = ShowL⇩b⇩o⇩o⇩l False` have "gas st6' ≤ gas st''" using g_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `¬ gas st ≤ g` n Pair KValue Value TBool have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
next
assume "¬ b = ShowL⇩b⇩o⇩o⇩l False"
with 4(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value TBool nt show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
qed
qed
next
case TAddr
with 4(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
qed
next
case (Calldata x2)
with 4(1) stmt_def `¬ gas st ≤ g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
next
case (Memory x3)
with 4(1) stmt_def `¬ gas st ≤ g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
next
case (Storage x4)
with 4(1) stmt_def `¬ gas st ≤ g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
qed
next
case (KCDptr x2)
with 4(1) stmt_def `¬ gas st ≤ g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
next
case (KMemptr x3)
with 4(1) stmt_def `¬ gas st ≤ g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
next
case (KStoptr x4)
with 4(1) stmt_def `¬ gas st ≤ g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
qed
qed
next
case (e e)
with 4(1) stmt_def `¬ gas st ≤ g` show ?thesis using stmt.psimps(4) g_def st'_def by simp
qed
qed
qed
next
case (5 ex s0 e cd st)
define g where "g = costs (WHILE ex s0) e cd st"
show ?case
proof (rule allI[OF impI])
fix st6'
assume stmt_def: "stmt (WHILE ex s0) e cd st = Normal ((), st6')"
then show "gas st6' ≤ gas st"
proof cases
assume "gas st ≤ g"
with 5(1) stmt_def show ?thesis using stmt.psimps(5) g_def by simp
next
assume gcost: "¬ gas st ≤ g"
then have l1: "assert Gas (λst. costs (WHILE ex s0) e cd st < gas st) st = Normal ((), st) " using g_def by simp
define st' where "st' = st⦇gas := gas st - g⦈"
then have l2: " modify (λst. st⦇gas := gas st - costs (WHILE ex s0) e cd st⦈) st = Normal ((), st')" using g_def by simp
show ?thesis
proof (cases "expr ex e cd st' (gas st - g)")
case (n a g')
define st'' where "st'' = st'⦇gas := g'⦈"
with n have l3: "toState (expr ex e cd) st' = Normal (a, st'')" using st'_def by simp
then show ?thesis
proof (cases a)
case (Pair b c)
then show ?thesis
proof (cases b)
case (KValue b)
then show ?thesis
proof (cases c)
case (Value x1)
then show ?thesis
proof (cases x1)
case (TSInt x1)
with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def by simp
next
case (TUInt x2)
with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def by simp
next
case TBool
then show ?thesis
proof cases
assume "b = ShowL⇩b⇩o⇩o⇩l True"
then show ?thesis
proof (cases "stmt s0 e cd st''")
case n2: (n a st''')
with 5(1) gcost n Pair KValue Value TBool `b = ShowL⇩b⇩o⇩o⇩l True` have "stmt (WHILE ex s0) e cd st = stmt (WHILE ex s0) e cd st'''" using stmt.psimps(5)[of ex s0 e cd st] g_def st'_def st''_def by (simp add: Let_def split:unit.split_asm)
with 5(3) stmt_def gcost n2 Pair KValue Value TBool `b = ShowL⇩b⇩o⇩o⇩l True` n have "gas st6' ≤ gas st'''" using g_def st'_def st''_def by simp
moreover from 5(2)[OF l1 l2 l3] gcost n2 Pair KValue Value TBool `b = ShowL⇩b⇩o⇩o⇩l True` n have "gas st''' ≤ gas st''" using g_def by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `¬ gas st ≤ g` n Pair KValue Value TBool have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using st'_def by simp
next
case (e x)
with 5(1) stmt_def gcost n Pair KValue Value TBool `b = ShowL⇩b⇩o⇩o⇩l True` show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
qed
next
assume nt: "¬ b = ShowL⇩b⇩o⇩o⇩l True"
show ?thesis
proof cases
assume "b = ShowL⇩b⇩o⇩o⇩l False"
with 5(1) gcost n Pair KValue Value TBool nt have "stmt (WHILE ex s0) e cd st = return () st''" using stmt.psimps(5) g_def st'_def st''_def by simp
with stmt_def have "gas st6' ≤ gas st''" by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `¬ gas st ≤ g` n Pair KValue Value TBool have "gas st'' ≤ gas st'" using st'_def st''_def by simp
ultimately show ?thesis using g_def st'_def st''_def by simp
next
assume "¬ b = ShowL⇩b⇩o⇩o⇩l False"
with 5(1) stmt_def gcost n Pair KValue Value TBool nt show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
qed
qed
next
case TAddr
with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
qed
next
case (Calldata x2)
with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
next
case (Memory x3)
with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
next
case (Storage x4)
with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
qed
next
case (KCDptr x2)
with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
next
case (KMemptr x3)
with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
next
case (KStoptr x4)
with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
qed
qed
next
case (e e)
with 5(1) stmt_def gcost show ?thesis using stmt.psimps(5) g_def st'_def by simp
qed
qed
qed
next
case (6 i xe e cd st)
define g where "g = costs (INVOKE i xe) e cd st"
show ?case
proof (rule allI[OF impI])
fix st6' assume a1: "stmt (INVOKE i xe) e cd st = Normal ((), st6')"
show "gas st6' ≤ gas st"
proof (cases)
assume "gas st ≤ g"
with 6(1) a1 show ?thesis using stmt.psimps(6) g_def by simp
next
assume gcost: "¬ gas st ≤ g"
then have l1: "assert Gas (λst. costs (INVOKE i xe) e cd st < gas st) st = Normal ((), st) " using g_def by simp
define st' where "st' = st⦇gas := gas st - g⦈"
then have l2: "modify (λst. st⦇gas := gas st - costs (INVOKE i xe) e cd st⦈) st = Normal ((), st')" using g_def by simp
then show ?thesis
proof (cases "ep $$ contract e")
case None
with 6(1) a1 gcost show ?thesis using stmt.psimps(6) g_def by simp
next
case (Some x)
then have l3: "option Err (λ_. ep $$ contract e) st' = Normal (x, st')" by simp
then show ?thesis
proof (cases x)
case (fields ct _ _)
then show ?thesis
proof (cases "fmlookup ct i")
case None
with 6(1) g_def a1 gcost Some fields show ?thesis using stmt.psimps(6) by simp
next
case s1: (Some a)
then show ?thesis
proof (cases a)
case (Method x1)
then show ?thesis
proof (cases x1)
case p1: (fields fp ext f)
then show ?thesis
proof (cases ext)
case True
with 6(1) a1 g_def gcost Some fields s1 Method p1 show ?thesis using stmt.psimps(6) st'_def by auto
next
case False
then have l4: "(case ct $$ i of None ⇒ throw Err | Some (Method (fp, True, f)) ⇒ throw Err
| Some (Method (fp, False, f)) ⇒ return (fp, f) | Some _ ⇒ throw Err) st' = Normal ((fp,f),st')" using s1 Method p1 by simp
define m⇩o e'
where "m⇩o = memory st'"
and "e' = ffold (init ct) (emptyEnv (address e) (contract e) (sender e) (svalue e)) (fmdom ct)"
then show ?thesis
proof (cases "load False fp xe e' emptyStore emptyStore m⇩o e cd st' (gas st - g)")
case s4: (n a g')
define st'' where "st'' = st'⦇gas := g'⦈"
then show ?thesis
proof (cases a)
case f2: (fields e⇩l cd⇩l k⇩l m⇩l)
then have l5: "toState (load False fp xe e' emptyStore emptyStore m⇩o e cd) st' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), st'')" using st'_def st''_def s4 by simp
define k⇩o where "k⇩o = stack st'"
then show ?thesis
proof (cases "stmt f e⇩l cd⇩l (st''⦇stack:=k⇩l, memory:=m⇩l⦈)")
case n2: (n a st''')
with a1 g_def gcost Some fields s1 Method p1 m⇩o_def e'_def s4 f2 k⇩o_def False
have "stmt (INVOKE i xe) e cd st = Normal ((), st'''⦇stack:=k⇩o⦈)"
using stmt.psimps(6)[OF 6(1)] st'_def st''_def by auto
with a1 have "gas st6' ≤ gas st'''" by auto
also from 6(2)[OF l1 l2 l3 fields l4 _ _ _ l5, where ?s'g="st''⦇stack := k⇩l, memory := m⇩l⦈"] n2 m⇩o_def e'_def
have "… ≤ gas st''" by auto
also from msel_ssel_expr_load_rexp_gas(4)[of False fp xe e' emptyStore emptyStore m⇩o e cd st' "(gas st - g)"] have "… ≤ gas st'" using s4 st'_def st''_def f2 by auto
finally show ?thesis using st'_def by simp
next
case (e x)
with 6(1) a1 g_def gcost Some fields s1 Method p1 m⇩o_def e'_def s4 f2 show ?thesis using stmt.psimps(6) st'_def st''_def False by auto
qed
qed
next
case (e x)
with 6(1) a1 g_def gcost Some fields s1 Method p1 m⇩o_def e'_def show ?thesis using stmt.psimps(6) st'_def False by auto
qed
qed
qed
next
case (Function _)
with 6(1) g_def a1 gcost Some fields s1 show ?thesis using stmt.psimps(6) by simp
next
case (Var _)
with 6(1) g_def a1 gcost Some fields s1 show ?thesis using stmt.psimps(6) by simp
qed
qed
qed
qed
qed
qed
next
case (7 ad i xe val e cd st)
define g where "g = costs (EXTERNAL ad i xe val) e cd st"
show ?case
proof (rule allI[OF impI])
fix st6' assume a1: "stmt (EXTERNAL ad i xe val) e cd st = Normal ((), st6')"
show "gas st6' ≤ gas st"
proof (cases)
assume "gas st ≤ g"
with 7(1) a1 show ?thesis using stmt.psimps(7) g_def by simp
next
assume gcost: "¬ gas st ≤ g"
then have l1: "assert Gas (λst. costs (EXTERNAL ad i xe val) e cd st < gas st) st = Normal ((), st) " using g_def by simp
define st' where "st' = st⦇gas := gas st - g⦈"
then have l2: " modify (λst. st⦇gas := gas st - costs (EXTERNAL ad i xe val) e cd st⦈) st = Normal ((), st')" using g_def by simp
then show ?thesis
proof (cases "expr ad e cd st' (gas st - g)")
case (n a0 g')
define st'' where "st'' = st'⦇gas := g'⦈"
with n have l3: "toState (expr ad e cd) st' = Normal (a0, st'')" using st'_def by simp
then show ?thesis
proof (cases a0)
case (Pair b c)
then show ?thesis
proof (cases b)
case (KValue adv)
then show ?thesis
proof (cases c)
case (Value x1)
then show ?thesis
proof (cases x1)
case (TSInt x1)
with 7(1) g_def a1 gcost n Pair KValue Value show ?thesis using stmt.psimps(7) st'_def by auto
next
case (TUInt x2)
with 7(1) g_def a1 gcost n Pair KValue Value show ?thesis using stmt.psimps(7) st'_def by auto
next
case TBool
with 7(1) g_def a1 gcost n Pair KValue Value show ?thesis using stmt.psimps(7) st'_def by auto
next
case TAddr
then have l4: "(case a0 of (KValue adv, Value TAddr) ⇒ return adv | (KValue adv, Value _) ⇒ throw Err | (KValue adv, _) ⇒ throw Err
| (_, b) ⇒ throw Err) st'' = Normal (adv, st'')" using Pair KValue Value by simp
then show ?thesis
proof (cases "adv = address e")
case True
with 7(1) g_def a1 gcost n Pair KValue Value TAddr show ?thesis using stmt.psimps(7) st'_def by auto
next
case False
then have l5: "assert Err (λ_. adv ≠ address e) st'' = Normal ((), st'')" by simp
then show ?thesis
proof (cases "type (accounts st'' adv)")
case None
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False show ?thesis using stmt.psimps(7) st'_def st''_def by auto
next
case (Some x2)
then show ?thesis
proof (cases x2)
case EOA
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some show ?thesis using stmt.psimps(7) st'_def st''_def by auto
next
case (Contract c)
then have l6: "(λst. case type (accounts st adv) of Some (Contract c) ⇒ return c st | _ ⇒ throw Err st) st'' = Normal (c, st'')" using Some by (simp split:atype.split option.split)
then show ?thesis
proof (cases "ep $$ c")
case None
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Contract Some show ?thesis using stmt.psimps(7) st'_def st''_def by auto
next
case s2: (Some x)
then show ?thesis
proof (cases x)
case p2: (fields ct x0 fb)
then have l7: "option Err (λ_. ep $$ c) st'' = Normal ((ct, x0, fb), st'')" using s2 by simp
then show ?thesis
proof (cases "expr val e cd st'' (gas st'')")
case n1: (n kv g'')
define st''' where "st''' = st''⦇gas := g''⦈"
with n1 have l8: "toState (expr val e cd) st'' = Normal (kv, st''')" by simp
then show ?thesis
proof (cases kv)
case p3: (Pair a b)
then show ?thesis
proof (cases a)
case k2: (KValue v)
then show ?thesis
proof (cases b)
case v: (Value t)
then have l9: "(case kv of (KValue v, Value t) ⇒ return (v, t) | (KValue v, _) ⇒ throw Err | (_, b) ⇒ throw Err) st''' = Normal ((v,t), st''')" using n1 p3 k2 by simp
show ?thesis
proof (cases "convert t (TUInt 256) v")
case None
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Contract Some s2 p2 None n1 p3 k2 v False show ?thesis using stmt.psimps(7)[OF 7(1)] st'_def st''_def st'''_def by simp
next
case s3: (Some v')
define e' where "e' = ffold (init ct) (emptyEnv adv c (address e) v') (fmdom ct)"
show ?thesis
proof (cases "fmlookup ct i")
case None
show ?thesis
proof (cases "transfer (address e) adv v' (accounts st''')")
case n2: None
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Contract Some s2 p2 None n1 p3 k2 v False s3 show ?thesis using stmt.psimps(7)[OF 7(1)] st'_def st''_def st'''_def by simp
next
case s4: (Some acc)
then have l10: "option Err (λst. transfer (address e) adv v' (accounts st)) st''' = Normal (acc, st''')" by simp
define k⇩o m⇩o
where "k⇩o = stack st'''"
and "m⇩o = memory st'''"
show ?thesis
proof (cases "stmt fb e' emptyStore (st'''⦇accounts := acc, stack:=emptyStore, memory:=emptyStore⦈)")
case n2: (n a st'''')
with g_def a1 gcost n Pair KValue Value TAddr False Contract Some s2 p2 None n1 p3 k2 v s4
have "stmt (EXTERNAL ad i xe val) e cd st = Normal ((), st''''⦇stack:=stack st''', memory := memory st'''⦈)"
using stmt.psimps(7)[OF 7(1)] st'_def st''_def st'''_def e'_def False s3 by simp
with a1 have "gas st6' ≤ gas st''''" by auto
also from 7(3)[OF l1 l2 l3 l4 l5 l6 l7 _ _ l8 l9 _ _ _ None l10, where ?s'k="st'''" and ?s'l="st'''⦇accounts := acc,stack:=emptyStore, memory:=emptyStore⦈" and ?x=e', of "(x0,fb)" x0 fb] n2
have "… ≤ gas (st'''⦇accounts := acc,stack:=emptyStore, memory:=emptyStore⦈)" using e'_def s3 by simp
also from msel_ssel_expr_load_rexp_gas(3)[of val e cd st'' "gas st''"]
have "… ≤ gas st''" using n1 st'_def st''_def st'''_def p3 by simp
also from msel_ssel_expr_load_rexp_gas(3)[of ad e cd st' "gas st - g"]
have "… ≤ gas st'" using n st'_def st''_def st'''_def p3 by fastforce
finally show ?thesis using st'_def by simp
next
case (e x)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 None n1 p3 k2 v s4 s3 show ?thesis using stmt.psimps(7)[of ad i xe val e cd st] st'_def st''_def st'''_def e'_def by simp
qed
qed
next
case s1: (Some a)
then show ?thesis
proof (cases a)
case (Method x1)
then show ?thesis
proof (cases x1)
case p4: (fields fp ext f)
then show ?thesis
proof (cases ext)
case True
then show ?thesis
proof (cases "load True fp xe e' emptyStore emptyStore emptyStore e cd st''' (gas st''')")
case s4: (n a g''')
define st'''' where "st'''' = st'''⦇gas := g'''⦈"
then show ?thesis
proof (cases a)
case f1: (fields e⇩l cd⇩l k⇩l m⇩l)
then have l10: "toState (load True fp xe e' emptyStore emptyStore emptyStore e cd) st''' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), st'''')" using s4 st''''_def by simp
show ?thesis
proof (cases "transfer (address e) adv v' (accounts st'''')")
case n2: None
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 Method p4 n1 p3 k2 v s3 f1 e'_def True s4 show ?thesis using stmt.psimps(7)[of ad i xe val e cd st] st'_def st''_def st'''_def st''''_def by simp
next
case s5: (Some acc)
then have l11: "option Err (λst. transfer (address e) adv v' (accounts st)) st'''' = Normal (acc, st'''')" by simp
define k⇩o where "k⇩o = accounts st''''"
define m⇩o where "m⇩o = accounts st''''"
show ?thesis
proof (cases "stmt f e⇩l cd⇩l (st''''⦇accounts := acc, stack:=k⇩l,memory:=m⇩l⦈)")
case n2: (n a st''''')
with 7(1) g_def a1 gcost n Pair KValue Value TAddr Some s2 Contract p2 s1 Method p4 n1 p3 k2 v k⇩o_def m⇩o_def e'_def s3 f1 s4 s5
have "stmt (EXTERNAL ad i xe val) e cd st = Normal ((), st'''''⦇stack:=stack st'''', memory := memory st''''⦈)"
using stmt.psimps(7)[of ad i xe val e cd st] st'_def st''_def st'''_def st''''_def True False by simp
with a1 have "gas st6' ≤ gas st'''''" by auto
also from 7(2)[OF l1 l2 l3 l4 l5 l6 l7 _ _ l8 l9 _ _ _ s1 Method _ _ _ l10 _ _ _ l11, where ?s'm="st''''⦇accounts := acc, stack := k⇩l, memory := m⇩l⦈" and ?s'l=st''''] p4 n2 e'_def True s3
have "… ≤ gas (st''''⦇accounts := acc, stack := k⇩l, memory := m⇩l⦈)" by simp
also from msel_ssel_expr_load_rexp_gas(4)[of True fp xe e' emptyStore emptyStore emptyStore e cd st''' "gas st'''"]
have "… ≤ gas st'''" using s3 st'_def st''_def st'''_def st''''_def f1 s4 by simp
also from msel_ssel_expr_load_rexp_gas(3)[of val e cd st'' "gas st''"]
have "… ≤ gas st''" using n1 st'_def st''_def st'''_def by fastforce
also from msel_ssel_expr_load_rexp_gas(3)[of ad e cd st' "gas st - g"]
have "… ≤ gas st'" using n st'_def st''_def st'''_def by fastforce
finally show ?thesis using st'_def by simp
next
case (e x)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 Method p4 n1 p3 k2 v k⇩o_def m⇩o_def e'_def s3 f1 s4 s5 True show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def st''''_def by simp
qed
qed
qed
next
case (e x)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 Method p4 n1 p3 k2 v e'_def True s3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
qed
next
case f: False
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 Method p4 n1 p3 k2 v s3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
qed
qed
next
case (Function _)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 n1 p3 k2 v s3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
next
case (Var _)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 s1 n1 p3 k2 v s3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
qed
qed
qed
next
case (Calldata x2)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 k2 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
next
case (Memory x3)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 k2 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
next
case (Storage x4)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 k2 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
qed
next
case (KCDptr x2)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
next
case (KMemptr x3)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
next
case (KStoptr x4)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 n1 p3 show ?thesis using stmt.psimps(7) st'_def st''_def st'''_def by simp
qed
qed
next
case n2: (e x)
with 7(1) g_def a1 gcost n Pair KValue Value TAddr False Some s2 Contract p2 show ?thesis using stmt.psimps(7) st'_def st''_def by simp
qed
qed
qed
qed
qed
qed
qed
next
case (Calldata x2)
with 7(1) g_def a1 gcost n Pair KValue show ?thesis using stmt.psimps(7) st'_def st''_def by simp
next
case (Memory x3)
with 7(1) g_def a1 gcost n Pair KValue show ?thesis using stmt.psimps(7) st'_def st''_def by simp
next
case (Storage x4)
with 7(1) g_def a1 gcost n Pair KValue show ?thesis using stmt.psimps(7) st'_def st''_def by simp
qed
next
case (KCDptr x2)
with 7(1) g_def a1 gcost n Pair show ?thesis using stmt.psimps(7) st'_def st''_def by simp
next
case (KMemptr x3)
with 7(1) g_def a1 gcost n Pair show ?thesis using stmt.psimps(7) st'_def st''_def by simp
next
case (KStoptr x4)
with 7(1) g_def a1 gcost n Pair show ?thesis using stmt.psimps(7) st'_def st''_def by simp
qed
qed
next
case (e _)
with 7(1) g_def a1 gcost show ?thesis using stmt.psimps(7) st'_def by simp
qed
qed
qed
next
case (8 ad ex e cd st)
define g where "g = costs (TRANSFER ad ex) e cd st"
show ?case
proof (rule allI[OF impI])
fix st6' assume stmt_def: "stmt (TRANSFER ad ex) e cd st = Normal ((), st6')"
show "gas st6' ≤ gas st"
proof cases
assume "gas st ≤ g"
with 8 stmt_def g_def show ?thesis using stmt.psimps(8)[of ad ex e cd st] by simp
next
assume "¬ gas st ≤ g"
then have l1: "assert Gas (λst. costs (TRANSFER ad ex) e cd st < gas st) st = Normal ((), st) " using g_def by simp
define st' where "st' = st⦇gas := gas st - g⦈"
then have l2: " modify (λst. st⦇gas := gas st - costs (TRANSFER ad ex) e cd st⦈) st = Normal ((), st')" using g_def by simp
show ?thesis
proof (cases "expr ad e cd st' (gas st - g)")
case (n a0 g')
define st'' where "st'' = st'⦇gas := g'⦈"
with n have l3: "toState (expr ad e cd) st' = Normal (a0, st'')" using st'_def by simp
then show ?thesis
proof (cases a0)
case (Pair b c)
then show ?thesis
proof (cases b)
case (KValue adv)
then show ?thesis
proof (cases c)
case (Value x1)
then show ?thesis
proof (cases x1)
case (TSInt x1)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
next
case (TUInt x2)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
next
case TBool
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
next
case TAddr
then have l4: "(case a0 of (KValue adv, Value TAddr) ⇒ return adv | (KValue adv, Value _) ⇒ throw Err | (KValue adv, _) ⇒ throw Err
| (_, b) ⇒ throw Err) st'' = Normal (adv, st'')" using Pair KValue Value by simp
then show ?thesis
proof (cases "expr ex e cd st'' (gas st'')")
case n2: (n a1 g'')
define st''' where "st''' = st''⦇gas := g''⦈"
with n2 have l5: "toState (expr ex e cd) st'' = Normal (a1, st''')" by simp
then show ?thesis
proof (cases a1)
case p2: (Pair b c)
then show ?thesis
proof (cases b)
case k2: (KValue v)
then show ?thesis
proof (cases c)
case v2: (Value t)
then have l6: "(case a1 of (KValue v, Value t) ⇒ return (v, t) | (KValue v, _) ⇒ throw Err | (_, b) ⇒ throw Err) st''' = Normal ((v,t), st''')" using p2 k2 by simp
then show ?thesis
proof (cases "convert t (TUInt 256) v")
case None
with 8(1) stmt_def g_def `¬ gas st ≤ g` n Pair KValue Value n2 p2 k2 v2 TAddr show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case (Some v')
then show ?thesis
proof (cases "type (accounts st''' adv)")
case None
with 8(1) stmt_def g_def `¬ gas st ≤ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case s0: (Some a)
then show ?thesis
proof (cases a)
case EOA
then show ?thesis
proof (cases "transfer (address e) adv v' (accounts st''')")
case None
with 8(1) stmt_def g_def `¬ gas st ≤ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some EOA s0 show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case s1: (Some acc)
then have l7: "option Err (λst. transfer (address e) adv v' (accounts st)) st''' = Normal (acc, st''')" using st'''_def by simp
with 8(1) `¬ gas st ≤ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some EOA g_def s0
have "stmt (TRANSFER ad ex) e cd st = Normal ((),st'''⦇accounts:=acc⦈)" using stmt.psimps(8)[of ad ex e cd st] st'_def st''_def st'''_def by simp
with stmt_def have "gas st6' = gas (st'''⦇accounts:=acc⦈)" by auto
also from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st'' "gas st''"]
have "… ≤ gas st''" using st'_def st''_def st'''_def n2 by fastforce
also from msel_ssel_expr_load_rexp_gas(3)[of ad e cd st' "gas st - g"]
have "… ≤ gas st'" using st'_def st''_def n by fastforce
finally show ?thesis using st'_def by simp
qed
next
case (Contract c)
then show ?thesis
proof (cases "ep $$ c")
case None
with 8(1) stmt_def g_def `¬ gas st ≤ g` n Pair KValue Value n2 p2 k2 v2 TAddr Contract Some s0 show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case s2: (Some a)
then show ?thesis
proof (cases a)
case p3: (fields ct cn f)
with s2 have l7: "option Err (λ_. ep $$ c) st''' = Normal ((ct, cn, f), st''')" by simp
define e' where "e' = ffold_init ct (emptyEnv adv c (address e) v') (fmdom ct)"
show ?thesis
proof (cases "transfer (address e) adv v' (accounts st''')")
case None
with 8(1) stmt_def g_def `¬ gas st ≤ g` n Pair KValue Value n2 p2 k2 v2 TAddr Contract Some s2 p3 s0 show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case s3: (Some acc)
then have l8: "option Err (λst. transfer (address e) adv v' (accounts st)) st''' = Normal (acc, st''')" by simp
then show ?thesis
proof (cases "stmt f e' emptyStore (st'''⦇accounts := acc, stack:=emptyStore, memory:=emptyStore⦈)")
case n3: (n a st'''')
with 8(1) `¬ gas st ≤ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some s2 p3 g_def Contract s3 s0
have "stmt (TRANSFER ad ex) e cd st = Normal ((),st''''⦇stack:=stack st''', memory := memory st'''⦈)" using e'_def stmt.psimps(8)[of ad ex e cd st] st'_def st''_def st'''_def by simp
with stmt_def have "gas st6' ≤ gas st''''" by auto
also from 8(2)[OF l1 l2 l3 l4 l5 l6, of v t _ _ "accounts st'''" "st'''", OF _ _ _ s0 Contract l7 _ _ _ _ _ l8, where ?s'k="st'''⦇accounts := acc, stack := emptyStore, memory := emptyStore⦈"] `¬ gas st ≤ g` e'_def n3 Some
have "… ≤ gas (st'''⦇accounts := acc, stack := emptyStore, memory := emptyStore⦈)" by simp
also from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st'' "gas st''"]
have "… ≤ gas st''" using st'_def st''_def st'''_def n2 by fastforce
also from msel_ssel_expr_load_rexp_gas(3)[of ad e cd st' "gas st - g"]
have "… ≤ gas st'" using st'_def st''_def n by fastforce
finally show ?thesis using st'_def by simp
next
case (e x)
with 8(1) `¬ gas st ≤ g` n Pair KValue Value n2 p2 k2 v2 TAddr Some s2 p3 g_def e'_def stmt_def Contract s3 s0 show ?thesis using stmt.psimps(8)[of ad ex e cd st] st'_def st''_def st'''_def by simp
qed
qed
qed
qed
qed
qed
qed
next
case (Calldata x2)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value TAddr n2 p2 k2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case (Memory x3)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value TAddr n2 p2 k2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case (Storage x4)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value TAddr n2 p2 k2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
qed
next
case (KCDptr x2)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value TAddr n2 p2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case (KMemptr x3)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value TAddr n2 p2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
next
case (KStoptr x4)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value TAddr n2 p2 g_def show ?thesis using stmt.psimps(8) st'_def st''_def st'''_def by simp
qed
qed
next
case (e e)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue Value TAddr g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
qed
qed
next
case (Calldata x2)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
next
case (Memory x3)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
next
case (Storage x4)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair KValue g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
qed
next
case (KCDptr x2)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
next
case (KMemptr x3)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
next
case (KStoptr x4)
with 8(1) stmt_def `¬ gas st ≤ g` n Pair g_def show ?thesis using stmt.psimps(8) st'_def st''_def by simp
qed
qed
next
case (e e)
with 8(1) stmt_def `¬ gas st ≤ g` g_def show ?thesis using stmt.psimps(8) st'_def by simp
qed
qed
qed
next
case (9 id0 tp s e⇩v cd st)
define g where "g = costs (BLOCK ((id0, tp), None) s) e⇩v cd st"
show ?case
proof (rule allI[OF impI])
fix st6' assume stmt_def: "stmt (BLOCK ((id0, tp), None) s) e⇩v cd st = Normal ((), st6')"
show "gas st6' ≤ gas st"
proof cases
assume "gas st ≤ g"
with 9 stmt_def g_def show ?thesis using stmt.psimps(9) by simp
next
assume "¬ gas st ≤ g"
then have l1: "assert Gas (λst. costs (BLOCK ((id0, tp), None) s) e⇩v cd st < gas st) st = Normal ((), st) " using g_def by simp
define st' where "st' = st⦇gas := gas st - g⦈"
then have l2: "modify (λst. st⦇gas := gas st - costs (BLOCK ((id0, tp), None) s) e⇩v cd st⦈) st = Normal ((), st')" using g_def by simp
show ?thesis
proof (cases "decl id0 tp None False cd (memory st') (storage st') (cd, (memory st'), (stack st'), e⇩v)")
case n2: None
with 9 stmt_def `¬ gas st ≤ g` g_def show ?thesis using stmt.psimps(9) st'_def by simp
next
case (Some a)
then have l3: "option Err (λst. decl id0 tp None False cd (memory st) (storage st) (cd, memory st, stack st, e⇩v)) st' = Normal (a, st')" by simp
then show ?thesis
proof (cases a)
case (fields cd' mem' sck' e')
with 9(1) stmt_def `¬ gas st ≤ g` g_def have "stmt (BLOCK ((id0, tp), None) s) e⇩v cd st = stmt s e' cd' (st⦇gas := gas st - g, stack := sck', memory := mem'⦈)" using stmt.psimps(9)[OF 9(1)] Some st'_def by simp
with 9(2)[OF l1 l2 l3] stmt_def `¬ gas st ≤ g` fields g_def have "gas st6' ≤ gas (st⦇gas := gas st - g, stack := sck', memory := mem'⦈)" using st'_def by fastforce
then show ?thesis by simp
qed
qed
qed
qed
next
case (10 id0 tp ex' s e⇩v cd st)
define g where "g = costs (BLOCK ((id0, tp), Some ex') s) e⇩v cd st"
show ?case
proof (rule allI[OF impI])
fix st6' assume stmt_def: "stmt (BLOCK ((id0, tp), Some ex') s) e⇩v cd st = Normal ((), st6')"
show "gas st6' ≤ gas st"
proof cases
assume "gas st ≤ g"
with 10 stmt_def g_def show ?thesis using stmt.psimps(10) by simp
next
assume "¬ gas st ≤ g"
then have l1: "assert Gas (λst. costs (BLOCK ((id0, tp), Some ex') s) e⇩v cd st < gas st) st = Normal ((), st) " using g_def by simp
define st' where "st' = st⦇gas := gas st - g⦈"
then have l2: "modify (λst. st⦇gas := gas st - costs (BLOCK ((id0, tp), Some ex') s) e⇩v cd st⦈) st = Normal ((), st')" using g_def by simp
show ?thesis
proof (cases "expr ex' e⇩v cd st' (gas st - g)")
case (n a g')
define st'' where "st'' = st'⦇gas := g'⦈"
with n have l3: "toState (expr ex' e⇩v cd) st' = Normal (a, st'')" using st''_def st'_def by simp
then show ?thesis
proof (cases a)
case (Pair v t)
then show ?thesis
proof (cases "decl id0 tp (Some (v, t)) False cd (memory st'') (storage st'') (cd, memory st'', stack st'', e⇩v)")
case None
with 10(1) stmt_def `¬ gas st ≤ g` n Pair g_def show ?thesis using stmt.psimps(10) st'_def st''_def by simp
next
case s2: (Some a)
then have l4: "option Err (λst. decl id0 tp (Some (v, t)) False cd (memory st) (storage st) (cd, memory st, stack st, e⇩v)) st'' = Normal (a, st'')" by simp
then show ?thesis
proof (cases a)
case (fields cd' mem' sck' e')
with 10(1) stmt_def `¬ gas st ≤ g` n Pair s2 g_def have "stmt (BLOCK ((id0, tp), Some ex') s) e⇩v cd st = stmt s e' cd' (st''⦇stack := sck', memory := mem'⦈)" using stmt.psimps(10)[of id0 tp ex' s e⇩v cd st] st'_def st''_def by simp
with 10(2)[OF l1 l2 l3 Pair l4 fields, where s'd="st''⦇stack := sck', memory := mem'⦈"] n stmt_def `¬ gas st ≤ g` s2 fields g_def have "gas st6' ≤ gas st''" by simp
moreover from msel_ssel_expr_load_rexp_gas(3)[of ex' e⇩v cd st' "gas st - g"] n have "gas st'' ≤ gas st'" using st'_def st''_def by fastforce
ultimately show ?thesis using st'_def by simp
qed
qed
qed
next
case (e e)
with 10 stmt_def `¬ gas st ≤ g` g_def show ?thesis using stmt.psimps(10) st'_def by simp
qed
qed
qed
next
case (11 i xe val e cd st)
define g where "g = costs (NEW i xe val) e cd st"
show ?case
proof (rule allI[OF impI])
fix st6' assume a1: "stmt (NEW i xe val) e cd st = Normal ((), st6')"
show "gas st6' ≤ gas st"
proof (cases)
assume "gas st ≤ g"
with 11(1) a1 show ?thesis using stmt.psimps(11) g_def by simp
next
assume gcost: "¬ gas st ≤ g"
then have l1: "assert Gas (λst. costs (NEW i xe val) e cd st < gas st) st = Normal ((), st) " using g_def by simp
define st' where "st' = st⦇gas := gas st - g⦈"
then have l2: "modify (λst. st⦇gas := gas st - costs (NEW i xe val) e cd st⦈) st = Normal ((), st')" using g_def by simp
define adv where "adv = hash (address e) (ShowL⇩n⇩a⇩t (contracts (accounts st' (address e))))"
then show ?thesis
proof (cases "type (accounts st' adv) = None")
case True
then show ?thesis
proof (cases "expr val e cd st' (gas st')")
case n0: (n kv g')
define st'' where "st'' = st'⦇gas := g'⦈"
then have l4: "toState (expr val e cd) st' = Normal (kv, st'')" using n0 by simp
then show ?thesis
proof (cases kv)
case p0: (Pair a b)
then show ?thesis
proof (cases a)
case k0: (KValue v)
then show ?thesis
proof (cases b)
case v0: (Value t)
then show ?thesis
proof (cases "ep $$ i")
case None
with a1 gcost g_def True n0 p0 k0 v0
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def st''_def by simp
next
case s0: (Some a)
then have l5: "option Err (λ_. ep $$ i) st'' = Normal (a, st'')" by simp
then show ?thesis
proof (cases a)
case f0: (fields ct cn _)
define e' where "e' = ffold_init ct (emptyEnv adv i (address e) v) (fmdom ct)"
then show ?thesis
proof (cases "load True (fst cn) xe e' emptyStore emptyStore emptyStore e cd st'' (gas st'')")
case n1: (n a g'')
define st''' where "st''' = st''⦇gas := g''⦈"
then have l6: "toState (load True (fst cn) xe e' emptyStore emptyStore emptyStore e cd) st'' = Normal (a, st''')" using n1 by simp
then show ?thesis
proof (cases a)
case f1: (fields e⇩l cd⇩l k⇩l m⇩l)
define st'''' where "st'''' = st'''⦇accounts:=(accounts st''')(adv := ⦇bal = ShowL⇩i⇩n⇩t 0, type = Some (Contract i), contracts = 0⦈), storage:=(storage st''')(adv := {$$})⦈"
then show ?thesis
proof (cases "transfer (address e) adv v (accounts st'''')")
case None
with a1 gcost g_def True n0 p0 k0 v0 s0 f0 n1 f1
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def e'_def st'_def st''_def st'''_def st''''_def by (simp add:Let_def)
next
case s1: (Some acc)
define st''''' where "st''''' = st''''⦇accounts := acc, stack:=k⇩l, memory:=m⇩l⦈"
then show ?thesis
proof (cases "stmt (snd cn) e⇩l cd⇩l st'''''")
case (n a st'''''')
define st''''''' where "st''''''' = st''''''⦇stack:=stack st'''', memory := memory st''''⦈"
define st'''''''' where "st'''''''' = incrementAccountContracts (address e) st'''''''"
from a1 gcost g_def True n0 p0 k0 v0 s0 f0 n1 f1 s1 n have "st6' = st''''''''"
using st'_def st''_def st'''_def st''''_def st'''''_def st'''''''_def st''''''''_def
stmt.psimps(11)[OF 11(1)] adv_def e'_def by (simp add:Let_def)
then have "gas st6' = gas st''''''''" by simp
also have "… ≤ gas st'''''''" using st''''''''_def incrementAccountContracts_def by simp
also have "… ≤ gas st''''''" using st'''''''_def by simp
also have "… ≤ gas st'''''" using 11(2)[OF l1 l2 _ _ l4 _ _ l5 _ _ e'_def l6, where ?s'h="st''''" and ?s'i="st''''" and ?s'j="st''''" and ?s'k="st''''⦇accounts := acc, stack := k⇩l, memory := m⇩l⦈", of st' "()"] p0 k0 v0 f0 f1 s1 n True st''''_def st'''''_def adv_def by simp
also have "… ≤ gas st''''" using st'''''_def by simp
also have "… ≤ gas st'''" using st''''_def by simp
also have "… ≤ gas st''" using st'''_def msel_ssel_expr_load_rexp_gas(4) n1 f1 by simp
also have "… ≤ gas st'" using st''_def msel_ssel_expr_load_rexp_gas(3) n0 p0 by simp
also have "… ≤ gas st" using st'_def by simp
finally show ?thesis .
next
case (e e)
with a1 gcost g_def n0 True p0 k0 v0 s0 f0 n1 f1 s1
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def e'_def st'_def st''_def st'''_def st''''_def st'''''_def by (simp add:Let_def)
qed
qed
qed
next
case (e e)
with a1 gcost g_def n0 True p0 k0 v0 s0 f0
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def e'_def st'_def st''_def by (simp add:Let_def)
qed
qed
qed
next
case (Calldata x2)
with a1 gcost g_def n0 True p0 k0
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp
next
case (Memory x3)
with a1 gcost g_def n0 True p0 k0
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp
next
case (Storage x4)
with a1 gcost g_def n0 True p0 k0
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp
qed
next
case (KCDptr x2)
with a1 gcost g_def n0 True p0
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp
next
case (KMemptr x3)
with a1 gcost g_def n0 True p0
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp
next
case (KStoptr x4)
with a1 gcost g_def n0 True p0
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp
qed
qed
next
case (e e)
with a1 gcost g_def True
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by simp
qed
next
case False
with a1 gcost g_def
show ?thesis using stmt.psimps(11)[OF 11(1)] adv_def st'_def by (simp split:if_split_asm)
qed
qed
qed
qed
subsection ‹Termination function›
text ‹Now we can prove termination using the lemma above.›
fun sgas
where "sgas l = gas (snd (snd (snd l)))"
fun ssize
where "ssize l = size (fst l)"
method stmt_dom_gas =
match premises in s: "stmt _ _ _ _ = Normal (_,_)" and d[thin]: "stmt_dom _" ⇒ ‹insert stmt_dom_gas[OF d s]›
method msel_ssel_expr_load_rexp =
match premises in e[thin]: "expr _ _ _ _ _ = Normal (_,_)" ⇒ ‹insert msel_ssel_expr_load_rexp_gas(3)[OF e]› |
match premises in l[thin]: "load _ _ _ _ _ _ _ _ _ _ _ = Normal (_,_)" ⇒ ‹insert msel_ssel_expr_load_rexp_gas(4)[OF l, THEN conjunct1]›
method costs =
match premises in "costs (WHILE ex s0) e cd st < _" for ex s0 and e::Environment and cd::CalldataT and st::State ⇒ ‹insert while_not_zero[of (unchecked) ex s0 e cd st]› |
match premises in "costs (INVOKE i xe) e cd st < _" for i xe and e::Environment and cd::CalldataT and st::State ⇒ ‹insert invoke_not_zero[of (unchecked) i xe e cd st]› |
match premises in "costs (EXTERNAL ad i xe val) e cd st < _" for ad i xe val and e::Environment and cd::CalldataT and st::State ⇒ ‹insert external_not_zero[of (unchecked) ad i xe val e cd st]› |
match premises in "costs (TRANSFER ad ex) e cd st < _" for ad ex and e::Environment and cd::CalldataT and st::State ⇒ ‹insert transfer_not_zero[of (unchecked) ad ex e cd st]› |
match premises in "costs (NEW i xe val) e cd st < _" for i xe val and e::Environment and cd::CalldataT and st::State ⇒ ‹insert new_not_zero[of (unchecked) i xe val e cd st]›
termination stmt
apply (relation "measures [sgas, ssize]")
apply (auto split: if_split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm bool.split_asm atype.split_asm)
apply ((stmt_dom_gas | msel_ssel_expr_load_rexp)+, costs?, simp)+
done
subsection ‹Gas Reduction›
text ‹
The following corollary is a generalization of @{thm [source] msel_ssel_expr_load_rexp_dom_gas}.
We first prove that the function is defined for all input values and then obtain the final result as a corollary.
›
lemma stmt_dom: "stmt_dom (s6, ev6, cd6, st6)"
apply (induct rule: stmt.induct[where ?P="λs6 ev6 cd6 st6. stmt_dom (s6, ev6, cd6, st6)"])
apply (simp_all add: stmt.domintros(1-10))
apply (rule stmt.domintros(11), force)
done
lemmas stmt_gas = stmt_dom_gas[OF stmt_dom]
lemma skip:
assumes "stmt SKIP ev cd st = Normal (x, st')"
shows "gas st > costs SKIP ev cd st"
and "st' = st⦇gas := gas st - costs SKIP ev cd st⦈"
using assms by (auto split:if_split_asm)
lemma assign:
assumes "stmt (ASSIGN lv ex) ev cd st = Normal (xx, st')"
obtains (1) v t g l t' g' v'
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Value t'),g')"
and "convert t t' v = Some v'"
and "st' = st⦇gas := g', stack := updateStore l (KValue v') (stack st)⦈"
| (2) v t g l t' g' v'
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStoreloc l, Storage (STValue t')),g')"
and "convert t t' v = Some v'"
and "st' = st⦇gas := g', storage := (storage st) (address ev := (fmupd l v' (storage st (address ev))))⦈"
| (3) v t g l t' g' v'
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LMemloc l, Memory (MTValue t')),g')"
and "convert t t' v = Some v'"
and "st' = st⦇gas := g', memory := updateStore l (MValue v') (memory st)⦈"
| (4) p x t g l t' g' p' m
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Memory t'),g')"
and "accessStore l (stack st) = Some (KMemptr p')"
and "cpm2m p p' x t cd (memory st) = Some m"
and "st' = st⦇gas := g', memory := m⦈"
| (5) p x t g l t' g' p' s
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Storage t'),g')"
and "accessStore l (stack st) = Some (KStoptr p')"
and "cpm2s p p' x t cd (storage st (address ev)) = Some s"
and "st' = st⦇gas := g', storage := (storage st) (address ev := s)⦈"
| (6) p x t g l t' g' s
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStoreloc l, t'),g')"
and "cpm2s p l x t cd (storage st (address ev)) = Some s"
and "st' = st⦇gas := g', storage := (storage st) (address ev := s)⦈"
| (7) p x t g l t' g' m
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LMemloc l, t'),g')"
and "cpm2m p l x t cd (memory st) = Some m"
and "st' = st⦇gas := g', memory := m⦈"
| (8) p x t g l t' g'
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Memory t'),g')"
and "st' = st⦇gas := g', stack := updateStore l (KMemptr p) (stack st)⦈"
| (9) p x t g l t' g' p' s
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Storage t'),g')"
and "accessStore l (stack st) = Some (KStoptr p')"
and "cpm2s p p' x t (memory st) (storage st (address ev)) = Some s"
and "st' = st⦇gas := g', storage := (storage st) (address ev := s)⦈"
| (10) p x t g l t' g' s
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStoreloc l, t'),g')"
and "cpm2s p l x t (memory st) (storage st (address ev)) = Some s"
and "st' = st⦇gas := g', storage := (storage st) (address ev := s)⦈"
| (11) p x t g l t' g'
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LMemloc l, t'),g')"
and "st' = st⦇gas := g', memory := updateStore l (MPointer p) (memory st)⦈"
| (12) p x t g l t' g' p' m
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Memory t'),g')"
and "accessStore l (stack st) = Some (KMemptr p')"
and "cps2m p p' x t (storage st (address ev)) (memory st) = Some m"
and "st' = st⦇gas := g', memory := m⦈"
| (13) p x t g l t' g'
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Storage t'),g')"
and "st' = st⦇gas := g', stack := updateStore l (KStoptr p) (stack st)⦈"
| (14) p x t g l t' g' s
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStoreloc l, t'),g')"
and "copy p l x t (storage st (address ev)) = Some s"
and "st' = st⦇gas := g', storage := (storage st) (address ev := s)⦈"
| (15) p x t g l t' g' m
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LMemloc l, t'),g')"
and "cps2m p l x t (storage st (address ev)) (memory st) = Some m"
and "st' = st⦇gas := g', memory := m⦈"
| (16) p t t' g l t'' g'
where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STMap t t')), g)"
and "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, t''),g')"
and "st' = st⦇gas := g', stack := updateStore l (KStoptr p) (stack st)⦈"
proof -
from assms consider
(1) v t g where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
| (2) p x t g where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
| (3) p x t g where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
| (4) p x t g where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x t)), g)"
| (5) p t t' g where "expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STMap t t')), g)"
by (auto split:if_split_asm result.split_asm Stackvalue.split_asm Type.split_asm MTypes.split_asm STypes.split_asm)
then show ?thesis
proof cases
case 1
with assms consider
(11) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Value t'),g')"
| (12) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStoreloc l, Storage (STValue t')),g')"
| (13) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LMemloc l, Memory (MTValue t')),g')"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm)
then show ?thesis
proof cases
case 11
with 1 assms show ?thesis using that(1) by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm)
next
case 12
with 1 assms show ?thesis using that(2) by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm)
next
case 13
with 1 assms show ?thesis using that(3) by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm)
qed
next
case 2
with assms consider
(21) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Memory t'),g')"
| (22) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Storage t'),g')"
| (23) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStoreloc l, t'),g')"
| (24) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LMemloc l, t'),g')"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm)
then show ?thesis
proof cases
case 21
moreover from assms 2 21 obtain p' where 3: "accessStore l (stack st) = Some (KMemptr p')"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
moreover from assms 2 21 3 obtain m where "cpm2m p p' x t cd (memory st) = Some m"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(4) assms 2 21
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
next
case 22
moreover from assms 2 22 obtain p' where 3: "accessStore l (stack st) = Some (KStoptr p')"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
moreover from assms 2 22 3 4 obtain s where "cpm2s p p' x t cd (storage st (address ev)) = Some s"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(5) assms 2 22
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
next
case 23
moreover from assms 2 23 3 4 obtain s where "cpm2s p l x t cd (storage st (address ev)) = Some s"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(6) assms 2
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
next
case 24
moreover from assms 2 24 obtain m where "cpm2m p l x t cd (memory st) = Some m"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(7) assms 2
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
qed
next
case 3
with assms consider
(31) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Memory t'),g')"
| (32) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Storage t'),g')"
| (33) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStoreloc l, t'),g')"
| (34) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LMemloc l, t'),g')"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm)
then show ?thesis
proof cases
case 31
then show ?thesis using that(8) assms 3 by (auto split:if_split_asm)
next
case 32
moreover from assms 3 32 obtain p' where 4: "accessStore l (stack st) = Some (KStoptr p')"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
moreover from assms 3 32 4 5 obtain s where "cpm2s p p' x t (memory st) (storage st (address ev)) = Some s"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(9) assms 3
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
next
case 33
moreover from assms 3 33 3 4 obtain s where "cpm2s p l x t (memory st) (storage st (address ev)) = Some s"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(10) assms 3
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
next
case 34
then show ?thesis using that(11) assms 3
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
qed
next
case 4
with assms consider
(41) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Memory t'),g')"
| (42) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStackloc l, Storage t'),g')"
| (43) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LStoreloc l, t'),g')"
| (44) l t' g' where "lexp lv ev cd (st⦇gas := g⦈) g = Normal((LMemloc l, t'),g')"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm)
then show ?thesis
proof cases
case 41
moreover from assms 4 41 obtain p' where 5: "accessStore l (stack st) = Some (KMemptr p')"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
moreover from assms 4 41 5 6 obtain m where "cps2m p p' x t (storage st (address ev)) (memory st) = Some m"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(12) assms 4
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
next
case 42
then show ?thesis using that(13) assms 4
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
next
case 43
moreover from assms 4 43 5 obtain s where "copy p l x t (storage st (address ev)) = Some s"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(14) assms 4
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
next
case 44
moreover from assms 4 44 5 obtain m where "cps2m p l x t (storage st (address ev)) (memory st) = Some m"
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
ultimately show ?thesis using that(15) assms 4
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
qed
next
case 5
then show ?thesis using that(16) assms
by (auto split:if_split_asm result.split_asm Type.split_asm LType.split_asm MTypes.split_asm STypes.split_asm option.split_asm Stackvalue.split_asm)
qed
qed
lemma comp:
assumes "stmt (COMP s1 s2) ev cd st = Normal (x, st')"
obtains (1) st''
where "gas st > costs (COMP s1 s2) ev cd st"
and "stmt s1 ev cd (st⦇gas := gas st - costs (COMP s1 s2) ev cd st⦈) = Normal((), st'')"
and "stmt s2 ev cd st'' = Normal((), st')"
using assms by (simp split:if_split_asm result.split_asm prod.split_asm)
lemma ite:
assumes "stmt (ITE ex s1 s2) ev cd st = Normal (x, st')"
obtains (True) g
where "gas st > costs (ITE ex s1 s2) ev cd st"
and "expr ex ev cd (st⦇gas := gas st - costs (ITE ex s1 s2) ev cd st⦈) (gas st - costs (ITE ex s1 s2) ev cd st) = Normal((KValue (ShowL⇩b⇩o⇩o⇩l True), Value TBool), g)"
and "stmt s1 ev cd (st⦇gas := g⦈) = Normal((), st')"
| (False) g
where "gas st > costs (ITE ex s1 s2) ev cd st"
and "expr ex ev cd (st⦇gas := gas st - costs (ITE ex s1 s2) ev cd st⦈) (gas st - costs (ITE ex s1 s2) ev cd st) = Normal((KValue (ShowL⇩b⇩o⇩o⇩l False), Value TBool), g)"
and "stmt s2 ev cd (st⦇gas := g⦈) = Normal((), st')"
using assms by (simp split:if_split_asm result.split_asm prod.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm)
lemma while:
assumes "stmt (WHILE ex s0) ev cd st = Normal (x, st')"
obtains (True) g st''
where "gas st > costs (WHILE ex s0) ev cd st"
and "expr ex ev cd (st⦇gas := gas st - costs (WHILE ex s0) ev cd st⦈) (gas st - costs (WHILE ex s0) ev cd st) = Normal((KValue (ShowL⇩b⇩o⇩o⇩l True), Value TBool), g)"
and "stmt s0 ev cd (st⦇gas := g⦈) = Normal((), st'')"
and "stmt (WHILE ex s0) ev cd st'' = Normal ((), st')"
| (False) g
where "gas st > costs (WHILE ex s0) ev cd st"
and "expr ex ev cd (st⦇gas := gas st - costs (WHILE ex s0) ev cd st⦈) (gas st - costs (WHILE ex s0) ev cd st) = Normal((KValue (ShowL⇩b⇩o⇩o⇩l False), Value TBool), g)"
and "st' = st⦇gas := g⦈"
using assms
proof -
from assms have 1: "gas st > costs (WHILE ex s0) ev cd st" by (simp split:if_split_asm)
moreover from assms 1 have 2: "modify (λst. st⦇gas := gas st - costs (WHILE ex s0) ev cd st⦈) st = Normal ((), st⦇gas := gas st - costs (WHILE ex s0) ev cd st⦈)" by simp
moreover from assms 1 2 obtain b g where 3: "expr ex ev cd (st⦇gas := gas st - costs (WHILE ex s0) ev cd st⦈) (gas st - costs (WHILE ex s0) ev cd st) = Normal ((KValue b, Value TBool), g)" by (simp split:result.split_asm prod.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm)
ultimately consider (True) "b = ShowL⇩b⇩o⇩o⇩l True" | (False) "b = ShowL⇩b⇩o⇩o⇩l False" | (None) "b ≠ ShowL⇩b⇩o⇩o⇩l True ∧ b ≠ ShowL⇩b⇩o⇩o⇩l False" by auto
then show ?thesis
proof cases
case True
moreover from assms 1 2 3 True obtain st' where 4: "stmt s0 ev cd (st⦇gas := g⦈) = Normal ((), st')" by (simp split:result.split_asm prod.split_asm)
moreover from assms 1 2 3 4 True obtain st'' where 5: "stmt (WHILE ex s0) ev cd st' = Normal ((), st'')" by (simp split:result.split_asm prod.split_asm)
ultimately show ?thesis using 1 2 3 that(1) assms by simp
next
case False
then show ?thesis using 1 2 3 that(2) assms true_neq_false by simp
next
case None
then show ?thesis using 1 2 3 assms by simp
qed
qed
lemma invoke:
fixes ev
defines "e' members ≡ ffold (init members) (emptyEnv (address ev) (contract ev) (sender ev) (svalue ev)) (fmdom members)"
assumes "stmt (INVOKE i xe) ev cd st = Normal (x, st')"
obtains ct fb fp f e⇩l cd⇩l k⇩l m⇩l g st''
where "gas st > costs (INVOKE i xe) ev cd st"
and "ep $$ contract ev = Some (ct, fb)"
and "ct $$ i = Some (Method (fp, False, f))"
and "load False fp xe (e' ct) emptyStore emptyStore (memory (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈)) ev cd (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) (gas st - costs (INVOKE i xe) ev cd st) = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g)"
and "stmt f e⇩l cd⇩l (st⦇gas:= g, stack:=k⇩l, memory:=m⇩l⦈) = Normal ((), st'')"
and "st' = st''⦇stack:=stack st⦈"
proof -
from assms have 1: "gas st > costs (INVOKE i xe) ev cd st" by (simp split:if_split_asm)
moreover from assms 1 obtain ct fb where 2: "ep $$ (contract ev) = Some (ct, fb)" by (simp split: prod.split_asm result.split_asm option.split_asm)
moreover from assms 1 2 obtain fp f where 3: "ct $$ i = Some (Method (fp, False, f))" by (simp split: prod.split_asm result.split_asm option.split_asm Member.split_asm bool.split_asm)
moreover from assms 1 2 3 obtain e⇩l cd⇩l k⇩l m⇩l g where 4: "load False fp xe (e' ct) emptyStore emptyStore (memory (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈)) ev cd (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) (gas st - costs (INVOKE i xe) ev cd st) = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g)" by (simp split: prod.split_asm result.split_asm)
moreover from assms 1 2 3 4 obtain st'' where 5: "stmt f e⇩l cd⇩l (st⦇gas:= g, stack:=k⇩l, memory:=m⇩l⦈) = Normal ((), st'')" by (simp split: prod.split_asm result.split_asm)
moreover from assms 1 2 3 4 5 have "st' = st''⦇stack:=stack st⦈" by (simp split: prod.split_asm result.split_asm)
ultimately show ?thesis using that by simp
qed
lemma external:
fixes ev
defines "e' members adv c v ≡ ffold (init members) (emptyEnv adv c (address ev) v) (fmdom members)"
assumes "stmt (EXTERNAL ad' i xe val) ev cd st = Normal (x, st')"
obtains (Some) adv c g ct cn fb' v t g' v' fp f e⇩l cd⇩l k⇩l m⇩l g'' acc st''
where "gas st > costs (EXTERNAL ad' i xe val) ev cd st"
and "expr ad' ev cd (st⦇gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) (gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g)"
and "adv ≠ address ev"
and "type (accounts (st⦇gas := g⦈) adv) = Some (Contract c)"
and "ep $$ c = Some (ct, cn, fb')"
and "expr val ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g')"
and "convert t (TUInt 256) v = Some v'"
and "fmlookup ct i = Some (Method (fp, True, f))"
and "load True fp xe (e' ct adv c v') emptyStore emptyStore emptyStore ev cd (st⦇gas := g'⦈) g' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g'')"
and "transfer (address ev) adv v' (accounts (st⦇gas := g''⦈)) = Some acc"
and "stmt f e⇩l cd⇩l (st⦇gas := g'', accounts := acc, stack:=k⇩l, memory:=m⇩l⦈) = Normal ((), st'')"
and "st' = st''⦇stack:=stack st, memory := memory st⦈"
| (None) adv c g ct cn fb' v t g' v' acc st''
where "gas st > costs (EXTERNAL ad' i xe val) ev cd st"
and "expr ad' ev cd (st⦇gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) (gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g)"
and "adv ≠ address ev"
and "type (accounts (st⦇gas := g⦈) adv) = Some (Contract c)"
and "ep $$ c = Some (ct, cn, fb')"
and "expr val ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g')"
and "convert t (TUInt 256) v = Some v'"
and "ct $$ i = None"
and "transfer (address ev) adv v' (accounts st) = Some acc"
and "stmt fb' (e' ct adv c v') emptyStore (st⦇gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore⦈) = Normal ((), st'')"
and "st' = st''⦇stack:=stack st, memory := memory st⦈"
proof -
from assms have 1: "gas st > costs (EXTERNAL ad' i xe val) ev cd st" by (simp split:if_split_asm)
moreover from assms 1 obtain adv g where 2: "expr ad' ev cd (st⦇gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) (gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g)" by (simp split: prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm)
moreover from assms 1 2 obtain c where 3: "type (accounts (st⦇gas := g⦈) adv) = Some (Contract c)" by (simp split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm atype.split_asm)
moreover from assms 1 2 3 obtain ct cn fb' where 4: "ep $$ c = Some (ct, cn, fb')" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm)
moreover from assms 1 2 3 4 obtain v t g' where 5: "expr val ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g')" using 1 2 by (simp split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm)
moreover from assms 1 2 3 4 5 have 6: "adv ≠ address ev" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm)
moreover from assms 1 2 3 4 5 6 obtain v' where 7: "convert t (TUInt 256) v = Some v'" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm)
ultimately consider (Some) fp f where "ct $$ i = Some (Method (fp, True, f))" | (None) "fmlookup ct i = None" using assms by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm bool.split_asm)
then show ?thesis
proof cases
case (Some fp f)
moreover from assms 1 2 3 4 5 6 7 Some obtain e⇩l cd⇩l k⇩l m⇩l g'' where 8: "load True fp xe (e' ct adv c v') emptyStore emptyStore emptyStore ev cd (st⦇gas := g'⦈) g' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g'')" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
moreover from assms 1 2 3 4 5 6 7 Some 8 obtain acc where 9: "transfer (address ev) adv v' (accounts st) = Some acc" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
moreover from assms 1 2 3 4 5 6 7 Some 8 9 obtain st'' where 10: "stmt f e⇩l cd⇩l (st⦇gas := g'', accounts := acc, stack:=k⇩l, memory:=m⇩l⦈) = Normal ((), st'')" by (simp add: Let_def transfer_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
moreover from assms 1 2 3 4 5 6 7 Some 8 9 10 have "st' = st''⦇stack:=stack st, memory := memory st⦈" by (simp add: Let_def transfer_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
ultimately show ?thesis using 1 2 3 4 5 6 7 that(1) by simp
next
case None
moreover from assms 1 2 3 4 5 6 7 None obtain acc where 8: "transfer (address ev) adv v' (accounts st) = Some acc" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
moreover from assms 1 2 3 4 5 6 7 None 8 obtain st'' where 9: "stmt fb' (e' ct adv c v') emptyStore (st⦇gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore⦈) = Normal ((), st'')" by (simp add: Let_def transfer_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
moreover from assms 1 2 3 4 5 6 7 None 8 9 have "st' = st''⦇stack:=stack st, memory := memory st⦈" by (simp add: Let_def transfer_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
ultimately show ?thesis using 1 2 3 4 5 6 7 that(2) by simp
qed
qed
lemma transfer:
fixes ev
defines "e' members adv c st v ≡ ffold (init members) (emptyEnv adv c (address ev) v) (fmdom members)"
assumes "stmt (TRANSFER ad ex) ev cd st = Normal (x, st')"
obtains (Contract) v t g adv c g' v' acc ct cn f st''
where "gas st > costs (TRANSFER ad ex) ev cd st"
and "expr ad ev cd (st⦇gas := gas st - costs (TRANSFER ad ex) ev cd st⦈) (gas st - costs (TRANSFER ad ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)"
and "expr ex ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g')"
and "convert t (TUInt 256) v = Some v'"
and "type (accounts (st⦇gas := g⦈) adv) = Some (Contract c)"
and "ep $$ c = Some (ct, cn, f)"
and "transfer (address ev) adv v' (accounts st) = Some acc"
and "stmt f (e' ct adv c (st⦇gas := g'⦈) v') emptyStore (st⦇gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore⦈) = Normal ((), st'')"
and "st' = st''⦇stack:=stack st, memory := memory st⦈"
| (EOA) v t g adv g' v' acc
where "gas st > costs (TRANSFER ad ex) ev cd st"
and "expr ad ev cd (st⦇gas := gas st - costs (TRANSFER ad ex) ev cd st⦈) (gas st - costs (TRANSFER ad ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)"
and "expr ex ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g')"
and "convert t (TUInt 256) v = Some v'"
and "type (accounts (st⦇gas := g⦈) adv) = Some EOA"
and "transfer (address ev) adv v' (accounts st) = Some acc"
and "st' = st⦇gas:=g', accounts:=acc⦈"
proof -
from assms have 1: "gas st > costs (TRANSFER ad ex) ev cd st" by (simp split:if_split_asm)
moreover from assms 1 obtain adv g where 2: "expr ad ev cd (st⦇gas := gas st - costs (TRANSFER ad ex) ev cd st⦈) (gas st - costs (TRANSFER ad ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm)
moreover from assms 1 2 obtain v t g' where 3: "expr ex ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g')" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm)
moreover from assms 1 2 3 obtain v' where 4: "convert t (TUInt 256) v = Some v'" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm)
ultimately consider (Contract) c where "type (accounts (st⦇gas := g'⦈) adv) = Some (Contract c)" | (EOA) "type (accounts (st⦇gas := g'⦈) adv) = Some EOA" using assms by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm atype.split_asm)
then show ?thesis
proof cases
case (Contract c)
moreover from assms 1 2 3 4 Contract obtain ct cn f where 5: "ep $$ c = Some (ct, cn, f)" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm atype.split_asm atype.split_asm)
moreover from assms 1 2 3 4 Contract 5 obtain acc where 6: "transfer (address ev) adv v' (accounts st) = Some acc" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
moreover from assms 1 2 3 4 Contract 5 6 obtain st'' where 7: "stmt f (e' ct adv c (st⦇gas := g'⦈) v') emptyStore (st⦇gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore⦈) = Normal ((), st'')" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
moreover from assms 1 2 3 4 Contract 5 6 7 have "st' = st''⦇stack:=stack st, memory := memory st⦈" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
ultimately show ?thesis using 1 2 3 4 that(1) by simp
next
case EOA
moreover from assms 1 2 3 4 EOA obtain acc where 5: "transfer (address ev) adv v' (accounts st) = Some acc" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
moreover from assms 1 2 3 4 EOA 5 have "st' = st⦇gas:=g', accounts:=acc⦈" by (simp add: Let_def split: if_split_asm prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm Types.split_asm option.split_asm Member.split_asm)
ultimately show ?thesis using 1 2 3 4 that(2) by simp
qed
qed
lemma blockNone:
fixes ev
assumes "stmt (BLOCK ((id0, tp), None) s) ev cd st = Normal (x, st')"
obtains cd' mem' sck' e'
where "gas st > costs (BLOCK ((id0, tp), None) s) ev cd st"
and "decl id0 tp None False cd (memory (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st⦈)) (storage (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st⦈)) (cd, memory (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st⦈), stack (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st⦈), ev) = Some (cd', mem', sck', e')"
and "stmt s e' cd' (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st, stack := sck', memory := mem'⦈) = Normal ((), st')"
using assms by (simp split:if_split_asm prod.split_asm option.split_asm)
lemma blockSome:
fixes ev
assumes "stmt (BLOCK ((id0, tp), Some ex') s) ev cd st = Normal (x, st')"
obtains v t g cd' mem' sck' e'
where "gas st > costs (BLOCK ((id0, tp), Some ex') s) ev cd st"
and "expr ex' ev cd (st⦇gas := gas st - costs (BLOCK ((id0, tp), Some ex') s) ev cd st⦈) (gas st - costs (BLOCK ((id0, tp), Some ex') s) ev cd st) = Normal((v,t),g)"
and "decl id0 tp (Some (v, t)) False cd (memory (st⦇gas := g⦈)) (storage (st⦇gas := g⦈)) (cd, memory (st⦇gas := g⦈), stack (st⦇gas := g⦈), ev) = Some (cd', mem', sck', e')"
and "stmt s e' cd' (st⦇gas := g, stack := sck', memory := mem'⦈) = Normal ((), st')"
using assms by (auto split:if_split_asm result.split_asm prod.split_asm option.split_asm)
lemma new:
fixes i xe val ev cd st
defines "st0 ≡ st⦇gas := gas st - costs (NEW i xe val) ev cd st⦈"
defines "adv0 ≡ hash (address ev) (ShowL⇩n⇩a⇩t (contracts (accounts st0 (address ev))))"
defines "st1 g ≡ st⦇gas := g, accounts := (accounts st)(adv0 := ⦇bal = ShowL⇩i⇩n⇩t 0, type = Some (Contract i), contracts = 0⦈), storage:=(storage st)(adv0 := {$$})⦈"
defines "e' members c v ≡ ffold (init members) (emptyEnv adv0 c (address ev) v) (fmdom members)"
assumes "stmt (NEW i xe val) ev cd st = Normal (x, st')"
obtains v t g ct cn fb e⇩l cd⇩l k⇩l m⇩l g' acc st''
where "gas st > costs (NEW i xe val) ev cd st"
and "type (accounts st adv0) = None"
and "expr val ev cd st0 (gas st0) = Normal((KValue v, Value t),g)"
and "ep $$ i = Some (ct, cn, fb)"
and "load True (fst cn) xe (e' ct i v) emptyStore emptyStore emptyStore ev cd (st0⦇gas := g⦈) g = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g')"
and "transfer (address ev) adv0 v (accounts (st1 g')) = Some acc"
and "stmt (snd cn) e⇩l cd⇩l (st1 g'⦇accounts := acc, stack:=k⇩l, memory:=m⇩l⦈) = Normal ((), st'')"
and "st' = incrementAccountContracts (address ev) (st''⦇stack:=stack st, memory := memory st⦈)"
proof -
from assms have 1: "gas st > costs (NEW i xe val) ev cd st" by (simp split:if_split_asm)
moreover from st0_def assms 1 have 2: "type (accounts st adv0) = None" by (simp split: if_split_asm)
moreover from st0_def assms 1 2 obtain v t g where 3: "expr val ev cd st0 (gas st0) = Normal((KValue v, Value t),g)" by (simp split: prod.split_asm result.split_asm Stackvalue.split_asm Type.split_asm)
moreover from assms 1 st0_def 2 3 obtain ct cn fb where 4: "ep $$ i = Some(ct, cn, fb)" by (simp split: prod.split_asm result.split_asm option.split_asm)
moreover from st0_def adv0_def e'_def assms 1 2 3 4 obtain e⇩l cd⇩l k⇩l m⇩l g' where 5: "load True (fst cn) xe (e' ct i v) emptyStore emptyStore emptyStore ev cd (st0⦇gas := g⦈) g = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g')" by (simp add:Let_def split: prod.split_asm result.split_asm option.split_asm)
moreover from st0_def adv0_def e'_def assms 1 2 3 4 5 obtain acc where 6: "transfer (address ev) adv0 v (accounts (st1 g')) = Some acc" by (simp add:Let_def split: prod.split_asm result.split_asm option.split_asm)
moreover from st0_def st1_def adv0_def e'_def assms 1 2 3 4 5 6 obtain st'' where "stmt (snd cn) e⇩l cd⇩l (st1 g'⦇accounts := acc, stack:=k⇩l, memory:=m⇩l⦈) = Normal ((), st'')" by (simp add:Let_def split: prod.split_asm result.split_asm option.split_asm)
ultimately show ?thesis using that assms by simp
qed
lemma atype_same:
assumes "stmt stm ev cd st = Normal (x, st')"
and "type (accounts st ad) = Some ctype"
shows "type (accounts st' ad) = Some ctype"
using assms
proof (induction arbitrary: st' rule: stmt.induct)
case (1 e cd st)
then show ?case using skip[OF 1(1)] by auto
next
case (2 lv ex env cd st)
show ?case by (cases rule: assign[OF 2(1)]; simp add: 2(2))
next
case (3 s1 s2 e cd st)
show ?case
proof (cases rule: comp[OF 3(3)])
case (1 st'')
then show ?thesis using 3 by simp
qed
next
case (4 ex s1 s2 e cd st)
show ?case
proof (cases rule: ite[OF 4(3)])
case (1 g)
then show ?thesis using 4 by simp
next
case (2 g)
then show ?thesis using 4 by (simp split: if_split_asm)
qed
next
case (5 ex s0 e cd st)
show ?case
proof (cases rule: while[OF 5(3)])
case (1 g st'')
then show ?thesis using 5 by simp
next
case (2 g)
then show ?thesis using 5 by simp
qed
next
case (6 i xe e cd st)
show ?case
proof (cases rule: invoke[OF 6(2)])
case (1 ct fb fp f e⇩l cd⇩l k⇩l m⇩l g st'')
then show ?thesis using 6 by simp
qed
next
case (7 ad' i xe val e cd st)
show ?case
proof (cases rule: external[OF 7(3)])
case (1 adv c g ct cn fb' v t g' v' fp f e⇩l cd⇩l k⇩l m⇩l g'' acc st'')
moreover from 7(4) have "type (acc ad) = Some ctype" using transfer_type_same[OF 1(10)] by simp
ultimately show ?thesis using 7(1) by simp
next
case (2 adv c g ct cn fb' v t g' v' acc st'')
moreover from 7(4) have "type (acc ad) = Some ctype" using transfer_type_same[OF 2(9)] by simp
ultimately show ?thesis using 7(2) by simp
qed
next
case (8 ad' ex e cd st)
show ?case
proof (cases rule: transfer[OF 8(2)])
case (1 v t g adv c g' v' acc ct cn f st'')
moreover from 8(3) have "type (acc ad) = Some ctype" using transfer_type_same[OF 1(7)] by simp
ultimately show ?thesis using 8(1) by simp
next
case (2 v t g adv g' v' acc)
moreover from 8(3) have "type (acc ad) = Some ctype" using transfer_type_same[OF 2(6)] by simp
ultimately show ?thesis by simp
qed
next
case (9 id0 tp s e⇩v cd st)
show ?case
proof (cases rule: blockNone[OF 9(2)])
case (1 cd' mem' sck' e')
then show ?thesis using 9 by simp
qed
next
case (10 id0 tp ex' s e⇩v cd st)
show ?case
proof (cases rule: blockSome[OF 10(2)])
case (1 v t g cd' mem' sck' e')
then show ?thesis using 10 by simp
qed
next
case (11 i xe val e cd st)
show ?case
proof (cases rule: new[OF 11(2)])
case (1 v t g ct cn fb e⇩l cd⇩l k⇩l m⇩l g' acc st'')
moreover have "hash (address e) ⌊contracts (accounts st (address e))⌋ ≠ ad" using 11(3) 1(2) by auto
ultimately show ?thesis
using 11 transfer_type_same[OF 1(6)] incrementAccountContracts_type by simp
qed
qed
declare lexp.simps[simp del, solidity_symbex add]
declare stmt.simps[simp del, solidity_symbex add]
end
subsection ‹A minimal cost model›
fun costs_min :: "S ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Gas"
where
"costs_min SKIP e cd st = 0"
| "costs_min (ASSIGN lv ex) e cd st = 0"
| "costs_min (COMP s1 s2) e cd st = 0"
| "costs_min (ITE ex s1 s2) e cd st = 0"
| "costs_min (WHILE ex s0) e cd st = 1"
| "costs_min (TRANSFER ad ex) e cd st = 1"
| "costs_min (BLOCK ((id0, tp), ex) s) e cd st =0"
| "costs_min (INVOKE _ _) e cd st = 1"
| "costs_min (EXTERNAL _ _ _ _) e cd st = 1"
| "costs_min (NEW _ _ _) e cd st = 1"
fun costs_ex :: "E ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Gas"
where
"costs_ex (E.INT _ _) e cd st = 0"
| "costs_ex (UINT _ _) e cd st = 0"
| "costs_ex (ADDRESS _) e cd st = 0"
| "costs_ex (BALANCE _) e cd st = 0"
| "costs_ex THIS e cd st = 0"
| "costs_ex SENDER e cd st = 0"
| "costs_ex VALUE e cd st = 0"
| "costs_ex (TRUE) e cd st = 0"
| "costs_ex (FALSE) e cd st = 0"
| "costs_ex (LVAL _) e cd st = 0"
| "costs_ex (PLUS _ _) e cd st = 0"
| "costs_ex (MINUS _ _) e cd st = 0"
| "costs_ex (EQUAL _ _) e cd st = 0"
| "costs_ex (LESS _ _) e cd st = 0"
| "costs_ex (AND _ _) e cd st = 0"
| "costs_ex (OR _ _) e cd st = 0"
| "costs_ex (NOT _) e cd st = 0"
| "costs_ex (CALL _ _) e cd st = 1"
| "costs_ex (ECALL _ _ _) e cd st = 1"
| "costs_ex CONTRACTS e cd st = 0"