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