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 type.Memory t ⇒ return t | _ ⇒ throw Err);
            (l'', t') ← msel True t l' r e cd st;
            return (LMemloc l'', type.Memory t')
          }
        | Some (KStoptr l') ⇒
          do {
            t ← (case tp of type.Storage t ⇒ return t | _ ⇒ throw Err);
            (l'', t') ← ssel t l' r e cd st;
            return (LStoreloc l'', type.Storage t')
          }
        | Some (KValue _) ⇒ throw Err
        | None ⇒ throw Err)
    | Some (tp, Storeloc l) ⇒
        do {
          t ← (case tp of type.Storage t ⇒ return t | _ ⇒ throw Err);
          (l', t') ← ssel t l r e cd st;
          return (LStoreloc l', type.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 (state.Gas s) of
                     Normal (a,g) ⇒ Normal(a,s⦇Gas:=g⦈)
                    | Exception e ⇒ Exception e)"

lemma wptoState[wprule]:
  assumes "⋀a g. gm s (state.Gas s) = Normal (a, g) ⟹ P a (s⦇Gas:=g⦈)"
      and "⋀e. gm s (state.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. state.Gas st > costs SKIP e cd st);
      modify (λst. st⦇Gas := state.Gas st - costs SKIP e cd st⦈)
    }) st"
| "stmt (ASSIGN lv ex) env cd st =
    (do {
      assert Gas (λst. state.Gas st > costs (ASSIGN lv ex) env cd st);
      modify (λst. st⦇Gas := state.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, type.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, type.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, type.Memory t') ⇒
              (if t' = (MTArray x t) then
                do {
                  sv ← applyf (λst. accessStore l (Stack st));
                  p' ← case sv of Some (KMemptr p') ⇒ return p' | _ ⇒ throw Err;
                  sv' ← applyf (λst. updateStore l (KMemptr (ShowL⇩n⇩a⇩t (Toploc (Memory st)))) (Stack st));
                  m ← option Err (λst. cpm2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t cd (snd (allocate(Memory st))));
                  modify (λst. st⦇Memory := m, Stack := sv'⦈)
                }
                else throw Err)
            | (LStackloc l, type.Storage t') ⇒
                (if cps2mTypeCompatible t' (MTArray x t) then
                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)⦈)
                } else throw Err)
            | (LStoreloc l, type.Storage t') ⇒
                (if cps2mTypeCompatible t' (MTArray x t) then
                do {
                  s ← option Err (λst. cpm2s p l x t cd (Storage st (Address env)));
                  modify (λst. st ⦇Storage := (Storage st) (Address env := s)⦈)
                } else throw Err)
            | (LMemloc l, type.Memory t') ⇒
              (if t' = (MTArray x t) then
                do {
                  
                  m ← option Err (λst. cpm2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t cd (snd (allocate(Memory st))));
                  m' ← applyf (λst. updateStore l (MPointer ((ShowL⇩n⇩a⇩t (Toploc (Memory st))))) m); 
                  modify (λst. st ⦇Memory := m'⦈)
                }
                else throw Err)
            | _ ⇒ throw Err
          }
      | (KMemptr p, type.Memory (MTArray x t)) ⇒
          do {
            rl ← toState (lexp lv env cd);
            case rl of
              (LStackloc l, type.Memory t') ⇒ 
              (if t' = (MTArray x t) then 
                modify (λst. st⦇Stack := updateStore l (KMemptr p) (Stack st)⦈)
               else throw Err)
            | (LStackloc l, type.Storage t') ⇒
                (if cps2mTypeCompatible t' (MTArray x t) then
                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)⦈)
                } else throw Err)
            | (LStoreloc l, type.Storage t') ⇒
                (if cps2mTypeCompatible t' (MTArray x t) then
                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)⦈)
                } else throw Err)
            | (LMemloc l, type.Memory t') ⇒ 
              (if t' = (MTArray x t) then
                modify (λst. st ⦇Memory := updateStore l (MPointer p) (Memory st)⦈)
               else throw Err)
            | _ ⇒ throw Err
          }
      | (KStoptr p, type.Storage (STArray x t)) ⇒
          do {
            rl ← toState (lexp lv env cd);
            case rl of
              (LStackloc l, type.Memory t') ⇒
                (if cps2mTypeCompatible (STArray x t) t' then
                do {
                  sv ← applyf (λst. accessStore l (Stack st));
                  p' ← case sv of Some (KMemptr p') ⇒ return p' | _ ⇒ throw Err;
                  sv' ← applyf (λst. updateStore l (KMemptr (ShowL⇩n⇩a⇩t (Toploc (Memory st)))) (Stack st));
                  m ← option Err (λst. cps2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t (Storage st (Address env)) (snd (allocate(Memory st))));
                  modify (λst. st⦇Memory := m, Stack := sv'⦈)
                } else throw Err)
            | (LStackloc l, type.Storage t') ⇒ 
              (if t' = (STArray x t) then
                modify (λst. st⦇Stack := updateStore l (KStoptr p) (Stack st)⦈)
               else throw Err)
            | (LStoreloc l, type.Storage t') ⇒
                (if t' = STArray x t then
                do {
                  s ← option Err (λst. copy p l x t (Storage st (Address env)));
                  modify (λst. st ⦇Storage := (Storage st) (Address env := s)⦈)
                }else throw Err)
            | (LMemloc l, type.Memory t') ⇒
              (if cps2mTypeCompatible (STArray x t) t' then
                do {
                  m ← option Err (λst. cps2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t (Storage st (Address env)) (snd (allocate(Memory st))));
                  m' ← applyf (λst. updateStore l (MPointer ((ShowL⇩n⇩a⇩t (Toploc (Memory st))))) m); 
                  modify (λst. st⦇Memory := m'⦈)
                } else throw Err)
            | _ ⇒ throw Err
          }
      | (KStoptr p, type.Storage (STMap t t')) ⇒
          do {
            rl ← toState (lexp lv env cd);
            (l, t'') ← case rl of (LStackloc l, type.Storage t'') ⇒ return (l,t'') | _ ⇒ throw Err;
            (if t'' = STMap t t' then            
              modify (λst. st⦇Stack := updateStore l (KStoptr p) (Stack st)⦈)
             else throw Err)
          }
      | _ ⇒ throw Err
    }) st"
| "stmt (COMP s1 s2) e cd st =
    (do {
      assert Gas (λst. state.Gas st > costs (COMP s1 s2) e cd st);
      modify (λst. st⦇state.Gas := state.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. state.Gas st > costs (ITE ex s1 s2) e cd st);
      modify (λst. st⦇state.Gas := state.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. state.Gas st > costs (WHILE ex s0) e cd st);
      modify (λst. st⦇state.Gas := state.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. state.Gas st > costs (INVOKE i xe) e cd st);
      modify (λst. st⦇state.Gas := state.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'  emptyTypedStore 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"
(*External Method calls allow to send some money val with it*)
(*However this transfer does NOT trigger a fallback*)
(*External methods can only be called from externally*)
| "stmt (EXTERNAL ad i xe val) e cd st =
    (do {
      assert Gas (λst. state.Gas st > costs (EXTERNAL ad i xe val) e cd st);
      modify (λst. st⦇state.Gas := state.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 (atype.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 b256) 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' emptyTypedStore emptyStore emptyTypedStore 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:=emptyTypedStore⦈);
            stmt fb e' emptyTypedStore;
            modify (λst. st⦇Stack:=k⇩o, Memory := m⇩o⦈)
          }
      | _ ⇒ throw Err
    }) st"
| "stmt (TRANSFER ad ex) e cd st =
    (do {
      assert Gas (λst. state.Gas st > costs (TRANSFER ad ex) e cd st);
      modify (λst. st⦇state.Gas := state.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 b256) v);
      acc ← applyf Accounts;
      case Type (acc adv) of
        Some (atype.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:=emptyTypedStore⦈);
            stmt f e' emptyTypedStore;
            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. state.Gas st > costs (BLOCK (id0, tp, None) s) e⇩v cd st);
      modify (λst. st⦇state.Gas := state.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 (Address e⇩v)) (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. state.Gas st > costs(BLOCK (id0, tp, Some ex') s) e⇩v cd st);
      modify (λst. st⦇state.Gas := state.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 (Address e⇩v)) (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. state.Gas st > costs (NEW i xe val) e cd st);
      modify (λst. st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈);
      adv ← applyf (λst. hash_version (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;
      v' ← option Err (λ_. convert t (TUInt b256) v);
      (ct, cn, _) ← option Err (λ_. ep $$ i);
      modify (λst. st⦇Accounts := (Accounts st)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage:=(Storage st)(adv := {$$})⦈);
      
      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' emptyTypedStore emptyStore emptyTypedStore 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 (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') ⟶ state.Gas st6' ≤ state.Gas st6)"
proof (induct rule: stmt.pinduct[where ?P="λs6 ev6 cd6 st6. (∀st6'. stmt s6 ev6 cd6 st6 = Normal ((), st6') ⟶ state.Gas st6' ≤ state.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 "state.Gas st6' ≤ state.Gas st"
    proof cases
      assume "state.Gas st ≤ g"
      with 2(1) stmt_def show ?thesis using stmt.psimps(2) g_def by simp
    next
      assume "¬ state.Gas st ≤ g"
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then consider (KVal) v t g' where "expr ex env cd st' (state.Gas st - g) = Normal ((KValue v, Value t), g')"
        | (CD) p x t g' where "expr ex env cd st' (state.Gas st - g) = Normal ((KCDptr p, type.Calldata (MTArray x t)), g')"
        | (Mem) p x t g' where "expr ex env cd st' (state.Gas st - g) = Normal ((KMemptr p, type.Memory (MTArray x t)), g')"
        | (Sto) p x t g' where "expr ex env cd st' (state.Gas st - g) = Normal ((KStoptr p, type.Storage (STArray x t)), g')"
        | (StoMap) p t t' g' where "expr ex env cd st' (state.Gas st - g) = Normal ((KStoptr p, type.Storage (STMap t t')), g')"
        using 2(1) stmt_def `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def 
        by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits)
      then show ?thesis
      proof(cases)
        case KVal
        define st'' where "st'' = st'⦇state.Gas := g'⦈"
        then consider (Stack) l t' g'' where "lexp lv env cd st'' g' = Normal ((LStackloc l, Value t'), g'')"
          | (Store) l t' g'' where "lexp lv env cd st'' g' = Normal ((LStoreloc l, type.Storage (STValue t')), g'')"
          | (Mem) l t' g'' where "lexp lv env cd st'' g' = Normal ((LMemloc l, type.Memory (MTValue t')), g'')"
          using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def KVal 
          by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits)
        then show ?thesis 
        proof(cases)
          case Stack
          then obtain v' where v'Def:"convert t t' v = Some v'" 
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def KVal 
            by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits option.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''⦇state.Gas := g'', Stack := updateStore l (KValue v') (Stack st)⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def KVal Stack by simp
          with stmt_def have "st6'= st''⦇state.Gas := g'', Stack := updateStore l (KValue v') (Stack st)⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g` have "state.Gas (st''⦇state.Gas := g'', Stack := updateStore l (KValue v') (Stack st)⦈) ≤ state.Gas (st'⦇state.Gas := g'⦈)" 
            using g_def st'_def v'Def Stack by simp
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` Stack KVal 
          have "state.Gas (st'⦇state.Gas := g'⦈) ≤ state.Gas (st⦇state.Gas := state.Gas st - g⦈)" using g_def by simp
          ultimately show ?thesis by simp
        next
          case Store
          then obtain v' where v'Def:"convert t t' v = Some v'" 
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def KVal 
            by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits option.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''⦇state.Gas := g'', Storage := (Storage st) (Address env := fmupd l v' (Storage st (Address env)))⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def KVal Store by simp
          with stmt_def have "st6'= st''⦇state.Gas := g'', Storage := (Storage st) (Address env := fmupd l v' (Storage st (Address env)))⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g` have "state.Gas (st''⦇state.Gas := g'', Stack := updateStore l (KValue v') (Stack st)⦈) ≤ state.Gas (st'⦇state.Gas := g'⦈)" 
            using g_def st'_def v'Def Store by simp
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` Store KVal 
          have "state.Gas (st'⦇state.Gas := g'⦈) ≤ state.Gas (st⦇state.Gas := state.Gas st - g⦈)" using g_def by simp
          ultimately show ?thesis by simp
        next
          case Mem
          then obtain v' where v'Def:"convert t t' v = Some v'" 
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def KVal 
            by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits option.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''⦇state.Gas := g'', Memory := updateStore l (MValue v') (Memory st)⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def KVal Mem by simp
          with stmt_def have "st6'= st''⦇state.Gas := g'', Memory := updateStore l (MValue v') (Memory st)⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g` have "state.Gas (st''⦇state.Gas := g'', Stack := updateStore l (KValue v') (Stack st)⦈) ≤ state.Gas (st'⦇state.Gas := g'⦈)" 
            using g_def st'_def v'Def Mem by simp
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` Mem KVal 
          have "state.Gas (st'⦇state.Gas := g'⦈) ≤ state.Gas (st⦇state.Gas := state.Gas st - g⦈)" using g_def by simp
          ultimately show ?thesis by simp
        qed
      next
        case CD
        define st'' where "st'' = st'⦇state.Gas := g'⦈"
        then consider (StackM) l  g'' where "lexp lv env cd st'' g' = Normal ((LStackloc l, type.Memory (MTArray x t)), g'')"
          | (StackS) l  t' g'' where "lexp lv env cd st'' g' = Normal ((LStackloc l, type.Storage t'), g'') ∧ cps2mTypeCompatible t' (MTArray x t)"
          | (Store) l t' g''  where "lexp lv env cd st'' g' = Normal ((LStoreloc l,  type.Storage t'), g'') ∧ cps2mTypeCompatible t' (MTArray x t)"
          | (Mem) l g'' where "lexp lv env cd st'' g' = Normal ((LMemloc l, type.Memory (MTArray x t)), g'')"
          using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def CD 
          by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits)
        then show ?thesis 
        proof(cases)
          case StackM
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain p' where acc:"accessStore l (Stack (st'⦇state.Gas := g'⦈)) = Some (KMemptr p')"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def CD StackM
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          then obtain stc st'''' where st4Def:"updateStore l (KMemptr (ShowL⇩n⇩a⇩t (Toploc (Memory st''')))) (Stack st''') = stc ∧ st'''' = st'''⦇Stack := stc⦈"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def CD StackM
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          then obtain m' where m'Def:"Some m' = cpm2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st''''))) x t cd (snd (allocate(Memory st'''')))"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD StackM acc
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''' ⦇Memory := m'⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD StackM acc st4Def
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st'''' ⦇Memory := m'⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''''⦇Memory := m'⦈) ≤ state.Gas st''" using st''_def st'''_def CD StackM acc st4Def by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def CD StackM acc st4Def by simp
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def CD StackM acc st4Def by simp
          ultimately show ?thesis using st'_def by simp
        next
          case StackS
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain p' where acc:"accessStore l (Stack (st'''⦇state.Gas := g'⦈)) = Some (KStoptr p')"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def CD StackS
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          
          then obtain s where sDef:"cpm2s p p' x t cd (Storage st''' (Address env)) = Some s"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD StackS acc
            by(auto split:if_splits option.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Storage := (Storage st) (Address env := s)⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD StackS acc 
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Storage := (Storage st) (Address env := s)⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''' ⦇Storage := (Storage st) (Address env := s)⦈) ≤ state.Gas st''" using st''_def st'''_def CD StackS acc sDef by auto
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def CD StackS acc  by auto
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def CD StackS acc  by simp
          ultimately show ?thesis using st'_def by simp
        next
          case Store
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain s where sDef:"cpm2s p l x t cd (Storage st (Address env)) = Some s"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD Store 
            by(auto split:if_splits option.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Storage := (Storage st) (Address env := s)⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD Store  
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Storage := (Storage st) (Address env := s)⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''' ⦇Storage := (Storage st) (Address env := s)⦈) ≤ state.Gas st''" using st''_def st'''_def CD Store  sDef by auto
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def CD Store   by auto
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def CD Store   by simp
          ultimately show ?thesis using st'_def by simp
        next
          case Mem
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain m where mDef:"Some m = cpm2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st'''))) x t cd (snd (allocate(Memory st''')))"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD Mem 
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          then obtain m' where m'Def:"m' = updateStore l (MPointer ((ShowL⇩n⇩a⇩t (Toploc (Memory st'''))))) m"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD Mem 
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Memory := m'⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def CD mDef Mem
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Memory := m'⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st'''⦇Memory := m'⦈) ≤ state.Gas st''" using st''_def st'''_def CD mDef Mem by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def CD mDef Mem by simp
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def CD mDef Mem by simp
          ultimately show ?thesis using st'_def by simp
        qed
      next
        case Mem
        define st'' where "st'' = st'⦇state.Gas := g'⦈"
        then consider (StackM) l  g'' where "lexp lv env cd st'' g' = Normal ((LStackloc l, type.Memory (MTArray x t)), g'')"
          | (StackS) l  t' g'' where "lexp lv env cd st'' g' = Normal ((LStackloc l, type.Storage t'), g'') ∧ cps2mTypeCompatible t' (MTArray x t)"
          | (Store) l t' g''  where "lexp lv env cd st'' g' = Normal ((LStoreloc l,  type.Storage t'), g'') ∧ cps2mTypeCompatible t' (MTArray x t)"
          | (Mem2) l g'' where "lexp lv env cd st'' g' = Normal ((LMemloc l, type.Memory (MTArray x t)), g'')"
          using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def Mem
          by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits)
        then show ?thesis 
        proof(cases)
          case StackM
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Stack := updateStore l (KMemptr p) (Stack st''')⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def StackM Mem
            by (auto split:if_splits prod.splits option.splits result.splits stackvalue.splits type.splits ltype.splits stypes.splits mtypes.splits)
          with stmt_def have "st6'= st''' ⦇Stack := updateStore l (KMemptr p) (Stack st''')⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''' ⦇Stack := updateStore l (KMemptr p) (Stack st''')⦈) ≤ state.Gas st''" using st''_def st'''_def Mem StackM by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def Mem StackM by simp
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def Mem StackM by simp
          ultimately show ?thesis using st'_def by simp
        next
          case StackS
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain p' where acc:"accessStore l (Stack (st'''⦇state.Gas := g'⦈)) = Some (KStoptr p')"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def Mem StackS
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          
          then obtain s where sDef:"cpm2s p p' x t (Memory st''') (Storage st''' (Address env)) = Some s"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Mem StackS acc
            by(auto split:if_splits option.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Storage := (Storage st) (Address env := s)⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Mem StackS acc 
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Storage := (Storage st) (Address env := s)⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''' ⦇Storage := (Storage st) (Address env := s)⦈) ≤ state.Gas st''" using st''_def st'''_def Mem StackS acc sDef by auto
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def Mem StackS acc  by auto
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def Mem StackS acc  by simp
          ultimately show ?thesis using st'_def by simp
        next
          case Store
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain s where sDef:"cpm2s p l x t (Memory st''') (Storage st (Address env)) = Some s"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Mem Store 
            by(auto split:if_splits option.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Storage := (Storage st) (Address env := s)⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Mem Store  
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Storage := (Storage st) (Address env := s)⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''' ⦇Storage := (Storage st) (Address env := s)⦈) ≤ state.Gas st''" using st''_def st'''_def Mem Store  sDef by auto
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def Mem Store   by auto
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def Mem Store   by simp
          ultimately show ?thesis using st'_def by simp
        next
          case Mem2
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Memory := updateStore l (MPointer p) (Memory st)⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Mem2  Mem
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Memory := updateStore l (MPointer p) (Memory st)⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st'''⦇Memory := updateStore l (MPointer p) (Memory st)⦈) ≤ state.Gas st''" using st''_def st'''_def Mem2  Mem by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def Mem2  Mem by simp
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def Mem2  Mem by simp
          ultimately show ?thesis using st'_def by simp
        qed
      next
        case Sto
        define st'' where "st'' = st'⦇state.Gas := g'⦈"
        then consider (StackM) l t' g'' where "lexp lv env cd st'' g' = Normal ((LStackloc l, type.Memory t'), g'') ∧ cps2mTypeCompatible (STArray x t) t'"
          | (StackS) l   g'' where "lexp lv env cd st'' g' = Normal ((LStackloc l, type.Storage (STArray x t)), g'')"
          | (Store) l  g''  where "lexp lv env cd st'' g' = Normal ((LStoreloc l,  type.Storage (STArray x t)), g'')"
          | (Mem) l g'' t' where "lexp lv env cd st'' g' = Normal ((LMemloc l, type.Memory t'), g'') ∧ cps2mTypeCompatible (STArray x t) t'"
          using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def Sto
          by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits)
        then show ?thesis 
        proof(cases)
          case StackM
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain st'''' stk where st4Def:"updateStore l (KMemptr (ShowL⇩n⇩a⇩t (Toploc (Memory st''')))) (Stack st''') = stk 
                                              ∧ st'''' = st'''⦇Stack:= stk⦈"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def Sto StackM
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          
          then obtain m where mDef:"cps2m  p (ShowL⇩n⇩a⇩t (Toploc (Memory st''''))) x t (Storage st (Address env)) (snd (allocate(Memory st''''))) = Some m"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Sto StackM st4Def
            by(auto split:if_splits option.splits stackvalue.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''' ⦇Memory := m⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Sto StackM st4Def 
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st'''' ⦇Memory := m⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st'''' ⦇Memory := m⦈) ≤ state.Gas st''" using st''_def st'''_def Sto StackM st4Def by auto
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def  Sto StackM st4Def   by auto
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def Sto StackM st4Def  by simp
          ultimately show ?thesis using st'_def by simp
        next
          case StackS
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Stack := updateStore l (KStoptr p) (Stack st''')⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Sto StackS
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Stack := updateStore l (KStoptr p) (Stack st''')⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''' ⦇Stack := updateStore l (KStoptr p) (Stack st''')⦈) ≤ state.Gas st''" using st''_def st'''_def Sto StackS by auto
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def Sto StackS by auto
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def Sto StackS by simp
          ultimately show ?thesis using st'_def by simp
        next
          case Store
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain s where sDef:"copy p l x t (Storage st'' (Address env)) = Some s"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Store Sto 
            by(auto split:if_splits option.splits)
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Storage := (Storage st) (Address env := s)⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Store Sto 
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Storage := (Storage st) (Address env := s)⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''' ⦇Storage := (Storage st) (Address env := s)⦈) ≤ state.Gas st''" using st''_def st'''_def Store Sto  by auto
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''') ≤ state.Gas st''" using st''_def st'''_def Store Sto    by auto
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def Store Sto   by simp
          ultimately show ?thesis using st'_def by simp
        next
          case Mem
          define st''' where "st''' = st''⦇state.Gas := g''⦈"
          then obtain m where mDef:"cps2m  p (ShowL⇩n⇩a⇩t (Toploc (Memory st'''))) x t (Storage st (Address env)) (snd (allocate(Memory st'''))) = Some m"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Sto Mem
            by(auto split:if_splits option.splits)
          then obtain m' where m'Def:"updateStore l (MPointer ((ShowL⇩n⇩a⇩t (Toploc (Memory st'''))))) m = m'"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def Sto Mem
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          
          
          then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' ⦇Memory := m'⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def Sto Mem mDef m'Def 
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st''' ⦇Memory := m'⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st''' ⦇Memory := m'⦈) ≤ state.Gas st''" using st''_def st'''_def Sto Sto Mem mDef m'Def  by auto
          
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def Sto Sto Mem mDef m'Def  by simp
          ultimately show ?thesis using st'_def by simp
        qed
      next
        case StoMap
        define st'' where "st'' = st'⦇state.Gas := g'⦈"

        then obtain l t'' g'' where lexpD:"lexp lv env cd st'' g' = Normal((LStackloc l, type.Storage t''), g'')" 
          using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def StoMap
          by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits)
        then have tSame:"t'' = STMap t t'"
          using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def StoMap
          by (auto split:result.splits mtypes.splits if_splits prod.splits stackvalue.splits type.splits ltype.splits stypes.splits)
        then have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'' ⦇state.Gas:=g'',Stack := updateStore l (KStoptr p) (Stack st'')⦈)"
            using 2(1) stmt_def  `¬ state.Gas st ≤ g` stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def StoMap lexpD tSame 
            by (auto split:if_splits option.splits result.splits stackvalue.splits)
          with stmt_def have "st6'= st'' ⦇state.Gas:=g'',Stack := updateStore l (KStoptr p) (Stack st'')⦈" by simp
          moreover from lexp_gas `¬ state.Gas st ≤ g`
          have "state.Gas (st'' ⦇state.Gas:=g'',Stack := updateStore l (KStoptr p) (Stack st'')⦈) ≤ state.Gas st''" using st''_def StoMap lexpD  by auto
          
          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` 
          have "state.Gas st'' ≤ state.Gas st'" using st'_def st''_def StoMap lexpD by simp
          ultimately show ?thesis using 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 "state.Gas st6' ≤ state.Gas st"
    proof cases
      assume "state.Gas st ≤ g"
      with 3(1) stmt_def g_def show ?thesis using stmt.psimps(3) by simp
    next
      assume "¬ state.Gas st ≤ g"
      show ?thesis
      proof (cases "stmt s1 e cd (st⦇state.Gas := state.Gas st - g⦈)")
        case (n a st')
        with 3(1) stmt_def `¬ state.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 ‹¬ state.Gas st ≤ g› n have "state.Gas st6' ≤ state.Gas st'" using g_def by simp
        moreover from 3(2)[where ?s'a="st⦇state.Gas := state.Gas st - g⦈"] ‹¬ state.Gas st ≤ g› n have "state.Gas st' ≤ state.Gas st" using g_def by simp
        ultimately show ?thesis by simp
      next
        case (e x)
        with 3 stmt_def `¬ state.Gas st ≤ g` show ?thesis using stmt.psimps(3)[of s1 s2 e cd st] g_def by (simp)
      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 "state.Gas st6' ≤ state.Gas st"
    proof cases
      assume "state.Gas st ≤ g"
      with 4(1) stmt_def show ?thesis using stmt.psimps(4) g_def by simp
    next
      assume "¬ state.Gas st ≤ g"
      then have l1: "assert ex.Gas (λst. costs (ITE ex s1 s2) e cd st < state.Gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then have l2: " modify (λst. st⦇state.Gas := state.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' (state.Gas st - g)")
        case (n a g')
        define st'' where "st'' = st'⦇state.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 `¬ state.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 `¬ state.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) `¬ state.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 `¬ state.Gas st ≤ g` n Pair KValue Value TBool `b = ShowL⇩b⇩o⇩o⇩l True` have "state.Gas st6' ≤ state.Gas st''" using g_def by simp
                  moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` n Pair KValue Value TBool have "state.Gas st'' ≤ state.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) `¬ state.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 `¬ state.Gas st ≤ g` n Pair KValue Value TBool nt `b = ShowL⇩b⇩o⇩o⇩l False` have "state.Gas st6' ≤ state.Gas st''" using g_def by simp
                    moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` n Pair KValue Value TBool have "state.Gas st'' ≤ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 "state.Gas st6' ≤ state.Gas st"
    proof cases
      assume "state.Gas st ≤ g"
      with 5(1) stmt_def show ?thesis using stmt.psimps(5) g_def by simp
    next
      assume gcost: "¬ state.Gas st ≤ g"
      then have l1: "assert Gas (λst. costs (WHILE ex s0) e cd st < state.Gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then have l2: " modify (λst. st⦇state.Gas := state.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' (state.Gas st - g)")
        case (n a g')
        define st'' where "st'' = st'⦇state.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 "state.Gas st6' ≤ state.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 "state.Gas st''' ≤ state.Gas st''" using g_def by simp
                    moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` n Pair KValue Value TBool have "state.Gas st'' ≤ state.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 "state.Gas st6' ≤ state.Gas st''" by simp
                    moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "state.Gas st - g"] `¬ state.Gas st ≤ g` n Pair KValue Value TBool have "state.Gas st'' ≤ state.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 "state.Gas st6' ≤ state.Gas st"
    proof (cases)
      assume "state.Gas st ≤ g"
      with 6(1) a1 show ?thesis using stmt.psimps(6) g_def by simp
    next
      assume gcost: "¬ state.Gas st ≤ g"
      then have l1: "assert Gas (λst. costs (INVOKE i xe) e cd st < state.Gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then have l2: "modify (λst. st⦇state.Gas := state.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' emptyTypedStore emptyStore m⇩o e cd st' (state.Gas st - g)")
                    case s4: (n a g')
                    define st'' where "st'' = st'⦇state.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' emptyTypedStore 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 "state.Gas st6' ≤ state.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 "… ≤ state.Gas st''" by auto
                        also from msel_ssel_expr_load_rexp_gas(4)[of False fp xe e' emptyTypedStore emptyStore m⇩o e cd st' "(state.Gas st - g)"] have "… ≤ state.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 "state.Gas st6' ≤ state.Gas st"
    proof (cases)
      assume "state.Gas st ≤ g"
      with 7(1) a1 show ?thesis using stmt.psimps(7) g_def by simp
    next
      assume gcost: "¬ state.Gas st ≤ g"
      then have l1: "assert Gas (λst. costs (EXTERNAL ad i xe val) e cd st < state.Gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then have l2: " modify (λst. st⦇state.Gas := state.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' (state.Gas st - g)")
        case (n a0 g')
        define st'' where "st'' = st'⦇state.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 (atype.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'' (state.Gas st'')")
                            case n1: (n kv g'')
                            define st''' where "st''' = st''⦇state.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 b256) 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' emptyTypedStore (st'''⦇Accounts := acc, Stack:=emptyStore, Memory:=emptyTypedStore⦈)")
                                          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 "state.Gas st6' ≤ state.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:=emptyTypedStore⦈" and ?x=e', of "(x0,fb)" x0 fb] n2 
                                            have "… ≤ state.Gas (st'''⦇Accounts := acc,Stack:=emptyStore, Memory:=emptyTypedStore⦈)" using e'_def s3 by simp
                                          also from msel_ssel_expr_load_rexp_gas(3)[of val e cd st'' "state.Gas st''"]
                                            have "… ≤ state.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' "state.Gas st - g"]
                                            have "… ≤ state.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' emptyTypedStore emptyStore emptyTypedStore e cd st''' (state.Gas st''')")
                                              case s4: (n a g''')
                                              define st'''' where "st'''' = st'''⦇state.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' emptyTypedStore emptyStore emptyTypedStore 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 "state.Gas st6' ≤ state.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 "… ≤ state.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' emptyTypedStore emptyStore emptyTypedStore e cd st''' "state.Gas st'''"]
                                                      have "… ≤ state.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'' "state.Gas st''"]
                                                      have "… ≤ state.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' "state.Gas st - g"]
                                                      have "… ≤ state.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 "state.Gas st6' ≤ state.Gas st"
    proof cases
      assume "state.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 "¬ state.Gas st ≤ g"
      then have l1: "assert Gas (λst. costs (TRANSFER ad ex) e cd st < state.Gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then have l2: " modify (λst. st⦇state.Gas := state.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' (state.Gas st - g)")
        case (n a0 g')
        define st'' where "st'' = st'⦇state.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 `¬ state.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 `¬ state.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 `¬ state.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'' (state.Gas st'')")
                  case n2: (n a1 g'')
                  define st''' where "st''' = st''⦇state.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 b256) v")
                          case None
                          with 8(1) stmt_def g_def `¬ state.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 `¬ state.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 `¬ state.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) `¬ state.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 "state.Gas st6' = state.Gas (st'''⦇Accounts:=acc⦈)" by auto
                                also from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st'' "state.Gas st''"]
                                  have "… ≤ state.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' "state.Gas st - g"]
                                  have "… ≤ state.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 `¬ state.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 `¬ state.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' emptyTypedStore (st'''⦇Accounts := acc, Stack:=emptyStore, Memory:=emptyTypedStore⦈)")
                                      case n3: (n a st'''')
                                      with 8(1) `¬ state.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 "state.Gas st6' ≤ state.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 := emptyTypedStore⦈"] `¬ state.Gas st ≤ g` e'_def n3 Some
                                        have "… ≤ state.Gas (st'''⦇Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" by simp
                                      also from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st'' "state.Gas st''"]
                                        have "… ≤ state.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' "state.Gas st - g"]
                                        have "… ≤ state.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) `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 `¬ state.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 "state.Gas st6' ≤ state.Gas st"
    proof cases
      assume "state.Gas st ≤ g"
      with 9 stmt_def g_def show ?thesis using stmt.psimps(9) by simp
    next
      assume "¬ state.Gas st ≤ g"
      then have l1: "assert Gas (λst. costs (BLOCK (id0, tp, None) s) e⇩v cd st < state.Gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then have l2: "modify (λst. st⦇state.Gas := state.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' (Address e⇩v)) (cd, (Memory st'), (Stack st'), e⇩v)")
        case n2: None
        with 9 stmt_def `¬ state.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 (Address e⇩v)) (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 `¬ state.Gas st ≤ g` g_def have "stmt (BLOCK (id0, tp, None) s) e⇩v cd st = stmt s e' cd' (st⦇state.Gas := state.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 `¬ state.Gas st ≤ g` fields g_def have "state.Gas st6' ≤ state.Gas (st⦇state.Gas := state.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 "state.Gas st6' ≤ state.Gas st"
    proof cases
      assume "state.Gas st ≤ g"
      with 10 stmt_def g_def show ?thesis using stmt.psimps(10) by simp
    next
      assume "¬ state.Gas st ≤ g"
      then have l1: "assert Gas (λst. costs (BLOCK (id0, tp, Some ex') s) e⇩v cd st < state.Gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then have l2: "modify (λst. st⦇state.Gas := state.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' (state.Gas st - g)")
        case (n a g')
        define st'' where "st'' = st'⦇state.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'' (Address e⇩v)) (cd, Memory st'', Stack st'', e⇩v)")
            case None
            with 10(1) stmt_def `¬ state.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 (Address e⇩v)) (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 `¬ state.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 `¬ state.Gas st ≤ g` s2 fields g_def have "state.Gas st6' ≤ state.Gas st''" by simp
              moreover from msel_ssel_expr_load_rexp_gas(3)[of ex' e⇩v cd st' "state.Gas st - g"] n have "state.Gas st'' ≤ state.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 `¬ state.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 "state.Gas st6' ≤ state.Gas st"
    proof (cases)
      assume "state.Gas st ≤ g"
      with 11(1) a1 show ?thesis using stmt.psimps(11) g_def by simp
    next
      assume gcost: "¬ state.Gas st ≤ g"
      then have l1: "assert Gas (λst. costs (NEW i xe val) e cd st < state.Gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = st⦇state.Gas := state.Gas st - g⦈"
      then have l2: "modify (λst. st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) st = Normal ((), st')" using g_def by simp
      define adv where "adv = hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts st' (Address e))))"
      then have l25:"applyf (λst. hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address e))))) st' =
    Normal (adv, st')" by simp
      then show ?thesis
      proof (cases "Type (Accounts st' adv) = None")
        case True
        then have l28:"assert Err (λst. Type (Accounts st adv) = None) st' = Normal ((), st')" by simp
        then obtain v t g' where n0:"expr val e cd st' (state.Gas st') = Normal ((KValue v, Value t), g')"
          using a1 stmt.psimps(11)[OF 11(1)] g_def 11(1) gcost l1 l2 by (auto split:if_splits result.splits stackvalue.splits type.splits option.splits)
        define st'' where "st'' = st'⦇state.Gas := g'⦈"
        then have l4: "toState (expr val e cd) st' = Normal ((KValue v, Value t), st'')" using n0 by simp
        then have l43:"(case (KValue v, Value t) of (KValue v, Value t) ⇒ return (v, t)
     | (KValue v, _) ⇒ throw Err | (_, b) ⇒ throw Err) st'' = Normal ((v,t), st'')" by simp
        then obtain v' where l45:"convert t (TUInt b256) v = Some v'" 
          using a1 stmt.psimps(11)[OF 11(1)] g_def 11(1) gcost l1 l2 l4
          by (auto split:if_splits result.splits stackvalue.splits type.splits option.splits)
        then have l46:"option Err (λ_. convert t (TUInt b256) v) st'' = Normal(v', st'')" by simp
        then obtain ct cn dud where n1:"ep $$ i = Some (ct, cn, dud)"
          using a1 stmt.psimps(11)[OF 11(1)] g_def 11(1) gcost l1 l2 
          by (auto split:if_splits result.splits stackvalue.splits type.splits option.splits)
        then have l5: "option Err (λ_. ep $$ i) st'' = Normal ((ct,cn,dud), st'')" by simp
        define e' where "e' = ffold_init ct (emptyEnv adv i (Address e) v') (fmdom ct)"
        define st''' where "st''' = st''⦇Accounts:=(Accounts st'')(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage:=(Storage st'')(adv := {$$})⦈"
        then have l6:" modify (λst. st⦇Accounts := (Accounts st)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage:=(Storage st)(adv := {$$})⦈) st'' =  Normal ((), st''')"
          by simp
        
        then obtain e⇩l cd⇩l k⇩l m⇩l g'' where
          n2:"load True (fst cn) xe e' emptyTypedStore emptyStore emptyTypedStore e cd st''' (state.Gas st''') = Normal((e⇩l, cd⇩l, k⇩l, m⇩l),g'')"
          using a1 stmt.psimps(11)[OF 11(1)] g_def 11(1) gcost l1 l2 l4 l46 l5 l6 st''_def e'_def st'''_def adv_def
          by (auto split:if_splits result.splits stackvalue.splits type.splits option.splits)
        define st'''' where "st'''' = st'''⦇state.Gas:=g''⦈"
        then have l65: "toState (load True (fst cn) xe e' emptyTypedStore emptyStore emptyTypedStore e cd) st''' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), st'''')"
          using n1 n2 st'''_def by (simp split:result.splits)
        then obtain acc where n3:"transfer (Address e) adv v' (Accounts st'''') = Some acc"
          using a1 stmt.psimps(11)[OF 11(1)] g_def 11(1) gcost l1 l2 l4 l46 l5 l65 st''_def e'_def st'''_def adv_def
          by (auto split:if_splits result.splits stackvalue.splits type.splits option.splits) 
        then have l68:"option Err (λst. transfer (Address e) adv v' (Accounts st)) st'''' = Normal (acc, st'''')" by auto
        define st''''' where "st''''' = st''''⦇Accounts := acc, Stack:=k⇩l, Memory:=m⇩l⦈"
        then have l69:"modify (λst. st⦇Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) st'''' =
                            Normal ((), st''''')" by simp
        then obtain st'''''' where l7:"stmt (snd cn) e⇩l cd⇩l st''''' = Normal ((),st'''''')" 
          using a1 stmt.psimps(11)[OF 11(1)] g_def 11(1) gcost l1 l2 l4 l46 l5 l65  n3 st''_def e'_def st'''_def adv_def
          by (auto split:if_splits result.splits stackvalue.splits type.splits option.splits) 
        define st''''''' where "st''''''' = st''''''⦇Stack:=Stack st'''', Memory := Memory st''''⦈"
        define st'''''''' where "st'''''''' = incrementAccountContracts (Address e) st'''''''"
         have "st6' = st''''''''"
          using st'_def st''_def st'''_def st''''_def st'''''_def st'''''''_def st''''''''_def
          using a1 stmt.psimps(11)[OF 11(1)] g_def 11(1) gcost l1 l2 l4 l46 l5 l65 l7 n3 st''_def e'_def st'''_def adv_def
          by (auto split:if_splits result.splits stackvalue.splits type.splits option.splits) 
        then have "state.Gas st6' = state.Gas st''''''''" by simp
        also have "… ≤ state.Gas st'''''''" using st''''''''_def incrementAccountContracts_def by simp
        also have "… ≤ state.Gas st''''''" using st'''''''_def by simp
        also have "...≤ state.Gas st'''''" 
          using 11(2)[OF l1 l2 l25 l28 l4 l43 _ l46 l5 _ _ l6 e'_def l65 _ _ _ l68 _ _ l69 ,
              where ?ac="e⇩l" and ?ad="cd⇩l" ] l7 adv_def st'''''_def  
          by (auto)
        also have "… ≤ state.Gas st''''" using st'''''_def by simp
        also have "… ≤ state.Gas st'''" using st''''_def msel_ssel_expr_load_rexp_gas(4) n2 by simp
        also have "… ≤ state.Gas st''" using st'''_def  by simp
        also have "… ≤ state.Gas st'" using st''_def msel_ssel_expr_load_rexp_gas(3) n0 by simp
        also have "… ≤ state.Gas st" using st'_def by simp
        finally show ?thesis .

      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 = state.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 "state.Gas st > costs SKIP ev cd st"
      and "st' = st⦇state.Gas := state.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⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, Value t'),g')"
      and "convert t t' v = Some v'"
      and "st' = st⦇state.Gas := g', Stack := updateStore l (KValue v') (Stack st)⦈"
  | (2) v t g l t' g' v'
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStoreloc l, type.Storage (STValue t')),g')"
      and "convert t t' v = Some v'"
      and "st' = st⦇state.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⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LMemloc l, type.Memory (MTValue t')),g')"
      and "convert t t' v = Some v'"
      and "st' = st⦇state.Gas := g', Memory := updateStore l (MValue v') (Memory st)⦈"
  | (4) p x t g l g' p' m t' st''
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Memory t'),g')"
      and "(MTArray x t) =t'"
      and "accessStore l (Stack st) = Some (KMemptr p')"
      and "(updateStore l (KMemptr (ShowL⇩n⇩a⇩t (Toploc (Memory st)))) (Stack st)) = st''"
      and "cpm2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t cd (snd (allocate (Memory st))) = Some m"
      and "st' = st⦇state.Gas := g', Memory := m, Stack := st''⦈"
  | (5) p x t g l t' g' p' s
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Storage t'),g')"
      and "accessStore l (Stack st) = Some (KStoptr p')"
      and "cps2mTypeCompatible t' (MTArray x t) "
      and "cpm2s p p' x t cd (Storage st (Address ev)) = Some s"
      and "st' = st⦇state.Gas := g', Storage := (Storage st) (Address ev := s)⦈"
  | (6) p x t g l t' g' s
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStoreloc l, type.Storage t'),g')"
      and "cps2mTypeCompatible t' (MTArray x t)"
      and "cpm2s p l x t cd (Storage st (Address ev)) = Some s"
      and "st' = st⦇state.Gas := g', Storage := (Storage st) (Address ev := s)⦈"
  | (7) p x t g l t' g' m m'
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LMemloc l, type.Memory t'),g')"
      and "(MTArray x t) = t'"
      and "cpm2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t cd (snd (allocate (Memory st))) = Some m"
      and "(updateStore l (MPointer (ShowL⇩n⇩a⇩t (Toploc (Memory st)))) m) = m'"
      and "st' = st⦇state.Gas := g', Memory := m'⦈"
  | (8) p x t g l t' g'
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, type.Memory (MTArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Memory t'),g')"
      and "t' = MTArray x t"
      and "st' = st⦇state.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⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, type.Memory (MTArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Storage t'),g')"
      and "cps2mTypeCompatible t' (MTArray x t)"
      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⦇state.Gas := g', Storage := (Storage st) (Address ev := s)⦈"
  | (10) p x t g l t' g' s
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, type.Memory (MTArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStoreloc l, type.Storage t'),g')"
      and "cps2mTypeCompatible t' (MTArray x t)"
      and "cpm2s p l x t (Memory st) (Storage st (Address ev)) = Some s"
      and "st' = st⦇state.Gas := g', Storage := (Storage st) (Address ev := s)⦈"
  | (11) p x t g l t' g'
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, type.Memory (MTArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LMemloc l, type.Memory t'),g')"
      and "t' = MTArray x t"
      and "st' = st⦇state.Gas := g', Memory := updateStore l (MPointer p) (Memory st)⦈"
  | (12) p x t g l t' g' p' m st''
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, type.Storage (STArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Memory t'),g')"
      and "cps2mTypeCompatible (STArray x t) t'"
      and "accessStore l (Stack st) = Some (KMemptr p')"
      and "st'' = updateStore l (KMemptr (ShowL⇩n⇩a⇩t (Toploc (Memory st)))) (Stack st)"
      and "cps2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t (Storage st (Address ev)) (snd (allocate(Memory st))) = Some m"
      and "st' = st⦇state.Gas := g', Memory := m, Stack := st''⦈"
  | (13) p x t g l t' g'
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, type.Storage (STArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Storage t'),g')"
      and "t' = STArray x t"
      and "st' = st⦇state.Gas := g', Stack := updateStore l (KStoptr p) (Stack st)⦈"
  | (14) p x t g l t' g' s
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, type.Storage (STArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStoreloc l, type.Storage t'),g')"
      and "t' = (STArray x t)"
      and "copy p l x t (Storage st (Address ev)) = Some s"
      and "st' = st⦇state.Gas := g', Storage := (Storage st) (Address ev := s)⦈"
  | (15) p x t g l t' g' m m'
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, type.Storage (STArray x t)), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LMemloc l, type.Memory t'),g')"
      and "cps2mTypeCompatible (STArray x t) t'"
      and "cps2m p (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t (Storage st (Address ev)) (snd (allocate(Memory st))) = Some m"
      and "updateStore l (MPointer ((ShowL⇩n⇩a⇩t (Toploc (Memory st))))) m = m'"
      and "st' = st⦇state.Gas := g', Memory := m'⦈"
  | (16) p t t' g l g' t''
    where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, type.Storage (STMap t t')), g)"
      and "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Storage t''),g')"
      and "t'' = (STMap t t')"
      and "st' = st⦇state.Gas := g', Stack := updateStore l (KStoptr p) (Stack st)⦈"
proof -
  from assms consider
    (1) v t g where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.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⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, type.Calldata (MTArray x t)), g)"
  | (3) p x t g where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, type.Memory (MTArray x t)), g)"
  | (4) p x t g where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, type.Storage (STArray x t)), g)"
  | (5) p t t' g where "expr ex ev cd (st⦇state.Gas := state.Gas st - costs  (ASSIGN lv ex) ev cd st⦈) (state.Gas st - costs  (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, type.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⦇state.Gas := g⦈) g = Normal((LStackloc l, Value t'),g')"
    | (12) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStoreloc l, type.Storage (STValue t')),g')"
    | (13) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LMemloc l, type.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 stmt.simps(2) consider
      (21) l g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Memory (MTArray x t)),g')"
    | (22) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Storage t'),g')"
    | (23) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStoreloc l, t'),g')"
    | (24) l g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LMemloc l, type.Memory (MTArray x t)),g')"
      by (auto split:if_split_asm result.split_asm type.split_asm ltype.split_asm mtypes.split_asm stypes.split_asm option.splits stackvalue.splits)
    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 (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t cd (snd (allocate (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 (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t cd (snd (allocate (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)
      moreover obtain m' where  "(updateStore l (MPointer (ShowL⇩n⇩a⇩t (Toploc (Memory st)))) m) = m'" by blast
      ultimately show ?thesis using that(7) assms 2 24
        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⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Memory t'),g')"
    | (32) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Storage t'),g')"
    | (33) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStoreloc l, t'),g')"
    | (34) l t' g' where "lexp lv ev cd (st⦇state.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⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Memory t'),g')"
    | (42) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStackloc l, type.Storage t'),g')"
    | (43) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LStoreloc l, t'),g')"
    | (44) l t' g' where "lexp lv ev cd (st⦇state.Gas := g⦈) g = Normal((LMemloc l, type.Memory 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)
      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 (ShowL⇩n⇩a⇩t (Toploc (Memory st))) x t (Storage st (Address ev)) (snd (allocate(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 "state.Gas st > costs (COMP s1 s2) ev cd st"
    and "stmt s1 ev cd (st⦇state.Gas := state.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 "state.Gas st > costs (ITE ex s1 s2) ev cd st"
    and "expr ex ev cd (st⦇state.Gas := state.Gas st - costs (ITE ex s1 s2) ev cd st⦈) (state.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⦇state.Gas := g⦈) = Normal((), st')"
| (False) g
  where "state.Gas st > costs (ITE ex s1 s2) ev cd st"
    and "expr ex ev cd (st⦇state.Gas := state.Gas st - costs (ITE ex s1 s2) ev cd st⦈) (state.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⦇state.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 "state.Gas st > costs (WHILE ex s0) ev cd st"
      and "expr ex ev cd (st⦇state.Gas := state.Gas st - costs (WHILE ex s0) ev cd st⦈) (state.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⦇state.Gas := g⦈) = Normal((), st'')"
      and "stmt (WHILE ex s0) ev cd st'' = Normal ((), st')"
    | (False) g
  where "state.Gas st > costs (WHILE ex s0) ev cd st"
    and "expr ex ev cd (st⦇state.Gas := state.Gas st - costs (WHILE ex s0) ev cd st⦈) (state.Gas st - costs (WHILE ex s0) ev cd st) = Normal((KValue (ShowL⇩b⇩o⇩o⇩l False), Value TBool), g)"
    and "st' = st⦇state.Gas := g⦈"
  using assms
proof -
  from assms have 1: "state.Gas st > costs (WHILE ex s0) ev cd st" by (simp split:if_split_asm)
  moreover from assms 1 have 2: "modify (λst. st⦇state.Gas := state.Gas st - costs (WHILE ex s0) ev cd st⦈) st = Normal ((), st⦇state.Gas := state.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⦇state.Gas := state.Gas st - costs (WHILE ex s0) ev cd st⦈) (state.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⦇state.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 whileE:
  fixes st ex sm ev cd
  defines "nGas ≡ state.Gas st - costs (WHILE ex sm) ev cd st"
  assumes "stmt (WHILE ex sm) ev cd st = Exception e"
  obtains (Gas) "e = Gas"
        | (Err) "e = Err"
        | (Exp) "expr ex ev cd (st⦇Gas := nGas⦈) nGas = Exception e"
        | (Stm) g where "expr ex ev cd (st⦇Gas := nGas⦈) nGas = Normal ((KValue (ShowL⇩b⇩o⇩o⇩l True), Value TBool), g)" and "stmt sm ev cd (st⦇Gas := g⦈) = Exception e"
        | (While) g st' where "state.Gas st > costs (WHILE ex sm) ev cd st" and "expr ex ev cd (st⦇Gas := nGas⦈) nGas = Normal ((KValue (ShowL⇩b⇩o⇩o⇩l True), Value TBool), g)" and "stmt sm ev cd (st⦇Gas := g⦈) = Normal ((), st')" and "local.stmt (WHILE ex sm) ev cd st' = Exception e"
  using assms stmt.simps(5)[of ex sm ev cd st] that by (simp del:stmt.simps split: if_split_asm result.split_asm prod.split_asm stackvalue.split_asm type.split_asm types.split_asm)


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 "state.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) emptyTypedStore emptyStore (Memory (st⦇state.Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈)) ev cd (st⦇state.Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) (state.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⦇state.Gas:= g, Stack:=k⇩l, Memory:=m⇩l⦈) = Normal ((), st'')"
      and "st' = st''⦇Stack:=Stack st⦈"
proof -
  from assms have 1: "state.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) emptyTypedStore emptyStore (Memory (st⦇state.Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈)) ev cd (st⦇state.Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) (state.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⦇state.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 "state.Gas st > costs (EXTERNAL ad' i xe val) ev cd st"
      and "expr ad' ev cd (st⦇state.Gas := state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) (state.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⦇state.Gas := g⦈) adv) = Some (atype.Contract c)"
      and "ep $$ (c) = Some (ct, cn, fb')"
      and "expr val ev cd (st⦇state.Gas := g⦈) g = Normal ((KValue v, Value t), g')"
      and "convert t (TUInt b256) v = Some v'"
      and "fmlookup ct i = Some (Method (fp, True, f))"
      and "load True fp xe (e' ct adv c v') emptyTypedStore emptyStore emptyTypedStore ev cd (st⦇state.Gas := g'⦈) g' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g'')"
      and "transfer (Address ev) adv v' (Accounts (st⦇state.Gas := g''⦈)) = Some acc"
      and "stmt f e⇩l cd⇩l (st⦇state.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 "state.Gas st > costs (EXTERNAL ad' i xe val) ev cd st"
      and "expr ad' ev cd (st⦇state.Gas := state.Gas st - costs  (EXTERNAL ad' i xe val) ev cd st⦈) (state.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⦇state.Gas := g⦈) adv) = Some (atype.Contract c)"
      and "ep $$ c = Some (ct, cn, fb')"
      and "expr val ev cd (st⦇state.Gas := g⦈) g = Normal ((KValue v, Value t), g')"
      and "convert t (TUInt b256) 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') emptyTypedStore (st⦇state.Gas := g', Accounts := acc, Stack:=emptyStore, Memory:=emptyTypedStore⦈) = Normal ((), st'')"
      and "st' = st''⦇Stack:=Stack st, Memory := Memory st⦈"
proof -
  from assms have 1: "state.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⦇state.Gas := state.Gas st - costs  (EXTERNAL ad' i xe val) ev cd st⦈) (state.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⦇state.Gas := g⦈) adv) = Some (atype.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⦇state.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 b256) 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') emptyTypedStore emptyStore emptyTypedStore ev cd (st⦇state.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⦇state.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') emptyTypedStore (st⦇state.Gas := g', Accounts := acc, Stack:=emptyStore, Memory:=emptyTypedStore⦈) = 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 "state.Gas st > costs (TRANSFER ad ex) ev cd st"
      and "expr ad ev cd (st⦇state.Gas := state.Gas st - costs (TRANSFER ad ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)"
      and "expr ex ev cd (st⦇state.Gas := g⦈) g = Normal ((KValue v, Value t), g')"
      and "convert t (TUInt b256) v = Some v'"
      and "Type (Accounts (st⦇state.Gas := g⦈) adv) = Some (atype.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⦇state.Gas := g'⦈) v') emptyTypedStore (st⦇state.Gas := g', Accounts := acc, Stack:=emptyStore, Memory:=emptyTypedStore⦈) = Normal ((), st'')"
      and "st' = st''⦇Stack:=Stack st, Memory := Memory st⦈"
    | (EOA) v t g adv g' v' acc
    where "state.Gas st > costs (TRANSFER ad ex) ev cd st"
      and "expr ad ev cd (st⦇state.Gas := state.Gas st - costs  (TRANSFER ad ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)"
      and "expr ex ev cd (st⦇state.Gas := g⦈) g = Normal ((KValue v, Value t), g')"
      and "convert t (TUInt b256) v = Some v'"
      and "Type (Accounts (st⦇state.Gas := g⦈) adv) = Some EOA"
      and "transfer (Address ev) adv v' (Accounts st) = Some acc"
      and "st' = st⦇state.Gas:=g', Accounts:=acc⦈"
proof -
  from assms have 1: "state.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⦇state.Gas := state.Gas st - costs  (TRANSFER ad ex) ev cd st⦈) (state.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⦇state.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 b256) 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⦇state.Gas := g'⦈) adv) = Some (atype.Contract c)" 
    | (EOA) "Type (Accounts (st⦇state.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⦇state.Gas := g'⦈) v') emptyTypedStore (st⦇state.Gas := g', Accounts := acc, Stack:=emptyStore, Memory:=emptyTypedStore⦈) = 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⦇state.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 "state.Gas st > costs (BLOCK (id0, tp, None) s) ev cd st"
      and "decl id0 tp None False cd (Memory (st⦇state.Gas := state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st⦈)) ((Storage (st⦇state.Gas := state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st⦈)) (Address ev)) (cd, Memory (st⦇state.Gas := state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st⦈), Stack (st⦇state.Gas := state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st⦈), ev) = Some (cd', mem', sck', e')"
      and "stmt s e' cd' (st⦇state.Gas := state.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 "state.Gas st > costs (BLOCK (id0, tp, Some ex') s) ev cd st"
      and "expr ex' ev cd (st⦇state.Gas := state.Gas st - costs (BLOCK (id0, tp, Some ex') s) ev cd st⦈) 
(state.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⦇state.Gas := g⦈)) ((Storage (st⦇state.Gas := g⦈)) (Address ev))
 (cd, Memory (st⦇state.Gas := g⦈), Stack (st⦇state.Gas := g⦈), ev) = Some (cd', mem', sck', e')"
      and "stmt s e' cd' (st⦇state.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⦇state.Gas := state.Gas st - costs (NEW i xe val) ev cd st⦈"
  defines "adv0 ≡ hash_version (Address ev) (ShowL⇩n⇩a⇩t (Contracts (Accounts st0 (Address ev))))"
  defines "st1 g ≡ st⦇state.Gas := g, Accounts := (Accounts st)(adv0 := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.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'' v'
    where "state.Gas st > costs (NEW i xe val) ev cd st"
      and "Type (Accounts st0 adv0) = None"
      and "expr val ev cd st0 (state.Gas st0) = Normal((KValue v, Value t),g)"
      and "convert t (TUInt b256) v = Some v'"
      and "ep $$ i = Some (ct, cn, fb)"
      and "load True (fst cn) xe (e' ct i v') emptyTypedStore emptyStore emptyTypedStore ev cd (st1 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 -
  have a1:"assert Gas (λst. state.Gas st > costs (NEW i xe val) ev cd st) st = Normal((), st)" using assms by (simp split:if_split_asm)
   have a2:"modify (λst. st⦇state.Gas := state.Gas st - costs (NEW i xe val) ev cd st⦈) st = Normal ((), st0)" using a1 assms(1) by (simp split:if_split_asm)
   have a3:"applyf (λst. hash_version (Address ev) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address ev))))) st0 = Normal (adv0,st0) " 
    using assms by simp
   have a4:"assert Err (λst. Type (Accounts st adv0) = None) st0 = Normal((),st0)" using assms by (simp split:if_split_asm)
  from st0_def assms a1 a2 a3 a4 obtain v t g where 3: "expr val ev cd st0 (state.Gas st0) = Normal((KValue v, Value t),g)" by (simp split: prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
   have a5:"toState (expr val ev cd) st0 = Normal((KValue v, Value t),st0⦇state.Gas:=g⦈)"
    using st0_def assms a1 a2 a3 a4 3
    by (simp split: prod.split_asm result.split_asm stackvalue.split_asm type.split_asm )
   have a6:"(case (KValue v, Value t) of (KValue v, Value t) ⇒ return (v, t) | _ ⇒ throw Err) 
(st0⦇state.Gas:=g⦈) = Normal ((v,t), st0⦇state.Gas:=g⦈)" by auto

   obtain v' where a7:"option Err (λ_. convert t (TUInt b256) v) (st0⦇state.Gas:=g⦈) = Normal (v', st0⦇state.Gas:=g⦈)"
    using st0_def assms a1 a2 a3 a4 a5 a6 by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
   obtain ct cn fb where a8:" option Err (λ_. ep $$ i) (st0⦇state.Gas:=g⦈)= Normal ((ct, cn, fb), st0⦇state.Gas:=g⦈)" 
    using st0_def assms a1 a2 a3 a4 a5 a6 by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)

   have a9:"modify (λst. st⦇Accounts := (Accounts st)
                  (adv0 := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), 
                  Storage:=(Storage st)(adv0 := {$$})⦈) (st0⦇state.Gas:=g⦈) = Normal ((), (st1 g))" 
    using st0_def st1_def assms a1 a2 a3 a4 a5 a6 by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
   obtain e'' where a10:"e'' = ffold_init ct (emptyEnv adv0 i (Address ev) v') (fmdom ct)" by simp
   
   then have e''Def:"(e' ct i v') = e''" using st0_def adv0_def  assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 by simp
   from st0_def adv0_def  assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
   
  obtain e⇩l cd⇩l k⇩l m⇩l g' where 5: "load True (fst cn) xe (e' ct i v') emptyTypedStore emptyStore emptyTypedStore ev cd (st1 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)

   have  a11:"toState (load True (fst cn) xe e'' emptyTypedStore emptyStore emptyTypedStore ev cd)(st1 g)
= Normal((e⇩l, cd⇩l, k⇩l, m⇩l), ((st1 g')))"
    using st0_def st1_def assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 Let_def 5 unfolding toState.simps
    by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)

   obtain acc where 
a12:"option Err (λst. transfer (Address ev) adv0 v' (Accounts st)) (st1 g') = Normal(acc, (st1 g'))" 
using st0_def st1_def assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 Let_def  unfolding toState.simps
    by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
   obtain k⇩o m⇩o where a13:"applyf (λst. (Stack st, Memory st)) (st1 g') = Normal ((k⇩o, m⇩o), (st1 g'))"
    using st0_def st1_def assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 Let_def  unfolding toState.simps
    by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
   have a14:"modify (λst. st⦇Accounts := acc, Stack:=k⇩l, Memory:=m⇩l⦈) (st1 g') = Normal((),(st1 g')⦇Accounts := acc, Stack:=k⇩l, Memory:=m⇩l⦈)"
    using st0_def st1_def assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 Let_def  unfolding toState.simps
    by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
   obtain st'' where a15: "stmt (snd cn) e⇩l cd⇩l ((st1 g')⦇Accounts := acc, Stack:=k⇩l, Memory:=m⇩l⦈) = Normal((), st'')"
      using st0_def st1_def assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 Let_def  unfolding toState.simps
    by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
   have a16:" modify (λst. st⦇Stack:=k⇩o, Memory := m⇩o⦈) st'' = Normal ((), st''⦇Stack:=k⇩o, Memory := m⇩o⦈)"
    using st0_def st1_def assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 Let_def  unfolding toState.simps
    by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
  have a17:"modify (incrementAccountContracts (Address ev)) (st''⦇Stack:=k⇩o, Memory := m⇩o⦈)
                      = Normal((), st')"
    using st0_def st1_def assms a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 Let_def  unfolding toState.simps
    by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
  
  have cc1:"state.Gas st > costs (NEW i xe val) ev cd st" using a1 by (simp split:if_split_asm)
   have cc2:"Type (Accounts st0 adv0) = None" using a3 a4 by (simp split:if_split_asm)
   have cc3:"expr val ev cd st0 (state.Gas st0) = Normal((KValue v, Value t),g)" using a5 3 by simp
   have cc4:"convert t (TUInt b256) v = Some v'" using a7 a6 a5 3  by (simp split:if_split_asm option.splits)
   have cc5:"ep $$ i = Some (ct, cn, fb)" using a8 by (simp split:if_split_asm option.splits)
   have cc6:"load True (fst cn) xe (e' ct i v') emptyTypedStore emptyStore emptyTypedStore ev cd (st1 g) g = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g')"
    using a10 a11 5 e''Def by simp
   have cc7:"transfer (Address ev) adv0 v' (Accounts (st1 g')) = Some acc" using a12 by (simp split:if_split_asm option.splits)
   have cc8:"stmt (snd cn) e⇩l cd⇩l (st1 g'⦇Accounts := acc, Stack:=k⇩l, Memory:=m⇩l⦈) = Normal ((), st'')"
    using a15 by blast
   have cc9:"st' = incrementAccountContracts (Address ev) (st''⦇Stack:=Stack st, Memory := Memory st⦈)"  
    using a17 a16 a15 a14 a13 a12 assms by (simp split:if_split_asm option.splits)
   show ?thesis using that[OF cc1 cc2 cc3 cc4 cc5 cc6 cc7 cc8 cc9] by blast 
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'' v')
      let ?st1 = "(st⦇state.Gas := g',
           Accounts :=
             (Accounts st)
             (hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts (st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) (Address e)))) :=
                ⦇Bal = (ShowL⇩n⇩a⇩t 0), Type = Some (atype.Contract i), Contracts = 0⦈),
           Storage := (Storage st)(hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts (st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) (Address e)))) := {$$})⦈)"
      let ?st2="(st⦇state.Gas := g',
           Accounts :=
             (Accounts st)
             (hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts (st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) (Address e)))) :=
                ⦇Bal = (ShowL⇩n⇩a⇩t 0), Type = Some (atype.Contract i), Contracts = 0⦈),
           Storage := (Storage st)(hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts (st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) (Address e)))) := {$$}),
           Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈)"
      have a1:"Accounts (st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) = Accounts st" by simp
    moreover have "hash_version (Address e) (ShowL⇩n⇩a⇩t  (Contracts (Accounts st (Address e)))) ≠ ad" using 11(3) 1(2) by auto
    moreover have "Type (acc ad) =  Type (Accounts ?st1 ad)" using transfer_type_same[OF 1(7), of ad] by simp
    moreover have "(Accounts st ad) = (Accounts ?st1) ad" using calculation by auto
    have "Type (Accounts st ad) = Some ctype" using 11(3) by simp
    moreover have "Type (Accounts (st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) ad) = Type (Accounts st ad)"
      using a1 by auto
    have "Type (Accounts st'' ad) = Some ctype" 
    proof -
      have a1:"assert Gas (λst. state.Gas st > costs (NEW i xe val) e cd st) st = Normal((), st)" using 11 by (simp split:if_split_asm)
      let ?st0="st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈"
      let ?adv0="hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address e))))"

   have a2:"modify (λst. st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) st = Normal ((), ?st0)" using a1 assms(1) by (simp split:if_split_asm)
   have a3:"applyf (λst. hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address e))))) ?st0 = Normal (?adv0,?st0) " 
    using 11 by simp
   have a4:"assert Err (λst. Type (Accounts st ?adv0) = None) ?st0 = Normal((),?st0)" using 11 by (simp split:if_split_asm)
   
  
   have a5:"toState (expr val e cd) ?st0 = Normal((KValue v, Value t),?st0⦇state.Gas:=g⦈)"
    using 1 a1 a2 a3 a4 by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
   have a6:"(case (KValue v, Value t) of (KValue v, Value t) ⇒ return (v, t) | _ ⇒ throw Err) 
            (?st0⦇state.Gas:=g⦈) = Normal ((v,t), ?st0⦇state.Gas:=g⦈)" by auto

   have a7:"option Err (λ_. convert t (TUInt b256) v) (?st0⦇state.Gas:=g⦈) = Normal (v', ?st0⦇state.Gas:=g⦈)"
    using 1 a1 a2 a3 a4 a5 a6 by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
    have a8:" option Err (λ_. ep $$ i) (?st0⦇state.Gas:=g⦈)= Normal ((ct, cn, fb), ?st0⦇state.Gas:=g⦈)" 
      using 1 a1 a2 a3 a4 a5 a6 by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
  
    let ?st1 ="st⦇state.Gas := g, Accounts := (Accounts st)(?adv0 := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage:=(Storage st)(?adv0 := {$$})⦈"
     have a9:"modify (λst. st⦇Accounts := (Accounts st)
                    (?adv0 := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), 
                    Storage:=(Storage st)(?adv0 := {$$})⦈) (?st0⦇state.Gas:=g⦈) = Normal ((), (?st1))" 
      using  1 a1 a2 a3 a4 a5 a6 by (simp split: option.split_asm prod.split_asm result.split_asm stackvalue.split_asm type.split_asm)
     
    obtain e'' where a10:"e'' = ffold_init ct (emptyEnv ?adv0 i (Address e) v') (fmdom ct)" by simp
    then have a15:"toState (load True (fst cn) xe e'' emptyTypedStore emptyStore emptyTypedStore e cd) ?st1 =
      Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), (?st1⦇state.Gas:=g'⦈))"
      using 1 by simp
    have a20:"transfer (Address e) (hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts (st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) (Address e))))) v'
     (Accounts (?st1⦇state.Gas:=g'⦈)) = Some acc" using 1 a10 a15 by simp
    have a30:" modify
     (λst. st
         ⦇Accounts := (Accounts st)(hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address e)))) 
            := ⦇Bal = (ShowL⇩n⇩a⇩t 0), Type = Some (atype.Contract i), Contracts = 0⦈),
            Storage := (Storage st)(hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address e)))) := {$$})⦈)
     (st⦇state.Gas := state.Gas st - costs (NEW i xe val) e cd st, state.Gas := g⦈) =
    Normal
     ((),
      st⦇state.Gas := g, Accounts := (Accounts st)(hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address e)))) := ⦇Bal = (ShowL⇩n⇩a⇩t 0), Type = Some (atype.Contract i), Contracts = 0⦈),
           Storage := (Storage st)(hash_version (Address e) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address e)))) := {$$})⦈)" by auto
    have a90:"Type (acc ad) = Some ctype" using transfer_type_same[OF 1(7), of ad] 1 assms 11 by fastforce
    show ?thesis 
      using 11(1)[OF a1 a2 a3 a4 a5 a6 _ a7 a8 _ _ _ a10 a15, of "(cn,fb)" fb _ e⇩l "(cd⇩l, k⇩l, m⇩l)" cd⇩l "( k⇩l, m⇩l)" k⇩l m⇩l  _ _ _ _ _ _ _ ?st2 st'' ]  
      using 1 a90 by simp
    qed
    moreover have "Type (Accounts st' ad) = Type (Accounts st'' ad)" using 1(9) unfolding incrementAccountContracts_def by auto
     
    ultimately show ?thesis
      using 11  by argo
  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"

global_interpretation solidity: statement_with_gas costs_ex fmempty costs_min
  defines stmt = "solidity.stmt" 
      and lexp = solidity.lexp
      and expr = solidity.expr
      and ssel = solidity.ssel
      and rexp = solidity.rexp
      and msel = solidity.msel
      and load = solidity.load
  by unfold_locales auto

section ‹Examples›

subsection ‹msel›

abbreviation mymemory2::memoryT
  where "mymemory2 ≡
    ⦇Mapping = fmap_of_list
      [(STR ''3.2'', MPointer STR ''5'')],
     Toploc = 1,
     Typed_Mapping = fmap_of_list
      [(STR ''3.2'', MTArray 6 (MTValue TBool))]⦈"

lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT b8 3] eempty emptyTypedStore (mystate⦇state.Gas:=1⦈) 1
= Normal ((STR ''3.2'', MTArray 6 (MTValue TBool)), 1)"
by Solidity_Symbex.solidity_symbex

lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT b8 3, UINT b8 4] eempty emptyTypedStore (mystate⦇state.Gas:=1,Memory:=mymemory2⦈) 1
= Normal ((STR ''4.5'', MTValue TBool), 1)" by Solidity_Symbex.solidity_symbex

lemma "msel True (MTArray 5 (MTArray 6 (MTValue TBool))) (STR ''2'') [UINT b8 5] eempty emptyTypedStore (mystate⦇state.Gas:=1,Memory:=mymemory2⦈) 1
= Exception (Err)" by Solidity_Symbex.solidity_symbex

end