Theory Statements

section ‹Statements›
theory Statements
  imports Expressions StateMonad
begin

locale statement_with_gas = expressions_with_gas +
  fixes costs :: "S  Environment  CalldataT  State  Gas"
  assumes while_not_zero[termination_simp]: "e cd st ex s0. 0 < (costs (WHILE ex s0) e cd st) "
      and invoke_not_zero[termination_simp]: "e cd st i xe. 0 < (costs (INVOKE i xe) e cd st)"
      and external_not_zero[termination_simp]: "e cd st ad i xe val. 0 < (costs (EXTERNAL ad i xe val) e cd st)"
      and transfer_not_zero[termination_simp]: "e cd st ex ad. 0 < (costs (TRANSFER ad ex) e cd st)"
      and new_not_zero[termination_simp]: "e cd st i xe val. 0 < (costs (NEW i xe val) e cd st)"
begin

subsection ‹Semantics of left expressions›

text ‹We first introduce lexp.›

fun lexp :: "L  Environment  CalldataT  State  (LType * Type, Ex, Gas) state_monad"
  where "lexp (Id i) e _ st g =
    (case (denvalue e) $$ i of
      Some (tp, (Stackloc l))  return (LStackloc l, tp)
    | Some (tp, (Storeloc l))  return (LStoreloc l, tp)
    | _  throw Err) g"
| "lexp (Ref i r) e cd st g =
    (case (denvalue e) $$ i of
      Some (tp, Stackloc l) 
        (case accessStore l (stack st) of
          Some (KCDptr _)  throw Err
        | Some (KMemptr l') 
          do {
            t  (case tp of Memory t  return t | _  throw Err);
            (l'', t')  msel True t l' r e cd st;
            return (LMemloc l'', Memory t')
          }
        | Some (KStoptr l') 
          do {
            t  (case tp of Storage t  return t | _  throw Err);
            (l'', t')  ssel t l' r e cd st;
            return (LStoreloc l'', Storage t')
          }
        | Some (KValue _)  throw Err
        | None  throw Err)
    | Some (tp, Storeloc l) 
        do {
          t  (case tp of Storage t  return t | _  throw Err);
          (l', t')  ssel t l r e cd st;
          return (LStoreloc l', Storage t')
        }
    | None  throw Err) g"

lemma lexp_gas[rule_format]:
    "l5' t5' g5'. lexp l5 ev5 cd5 st5 g5 = Normal ((l5', t5'), g5')  g5'  g5"
proof (induct rule: lexp.induct[where ?P="λl5 ev5 cd5 st5 g5. (l5' t5' g5'. lexp l5 ev5 cd5 st5 g5 = Normal ((l5', t5'), g5')  g5'  g5)"])
  case (1 i e uv st g)
  then show ?case using lexp.simps(1) by (simp split: option.split Denvalue.split prod.split)
next
  case (2 i r e cd st g)
  show ?case
  proof (rule allI[THEN allI, THEN allI, OF impI])
    fix st5' xa xaa
    assume a1: "lexp (Ref i r) e cd st g = Normal ((st5', xa), xaa)"
    then show "xaa  g"
    proof (cases "fmlookup (denvalue e) i")
      case None
      with a1 show ?thesis using lexp.simps(2) by simp
    next
      case (Some a)
      then show ?thesis
      proof (cases a)
        case (Pair tp b)
        then show ?thesis
        proof (cases b)
          case (Stackloc l)
          then show ?thesis
          proof (cases "accessStore l (stack st)")
            case None
            with a1 Some Pair Stackloc show ?thesis using lexp.psimps(2) by simp
          next
            case s2: (Some a)
            then show ?thesis
            proof (cases a)
              case (KValue x1)
              with a1 Some Pair Stackloc s2 show ?thesis using lexp.psimps(2) by simp
            next
              case (KCDptr x2)
              with a1 Some Pair Stackloc s2 show ?thesis using lexp.psimps(2) by simp
            next
              case (KMemptr l')
              then show ?thesis
              proof (cases tp)
                case (Value _)
                with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.simps(2) by simp
              next
                case (Calldata _)
                with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.simps(2) by simp
              next
                case (Memory t)
                then show ?thesis
                proof (cases "msel True t l' r e cd st g")
                  case (n _ _)
                  with 2 a1 Some Pair Stackloc s2 KMemptr Memory show ?thesis using msel_ssel_expr_load_rexp_gas(1) by (simp split: prod.split_asm)
                next
                  case (e _)
                  with a1 Some Pair Stackloc s2 KMemptr Memory show ?thesis using lexp.psimps(2) by simp
                qed
              next
                case (Storage _)
                with a1 Some Pair Stackloc s2 KMemptr show ?thesis using lexp.psimps(2) by simp
              qed
            next
              case (KStoptr l')
              then show ?thesis
              proof (cases tp)
                case (Value _)
                with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp
              next
                case (Calldata _)
                with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp
              next
                case (Memory _)
                with a1 Some Pair Stackloc s2 KStoptr show ?thesis using lexp.psimps(2) by simp
              next
                case (Storage t)
                then show ?thesis
                proof (cases "ssel t l' r e cd st g")
                  case (n _ _)
                  with a1 Some Pair Stackloc s2 KStoptr Storage show ?thesis using msel_ssel_expr_load_rexp_gas(2) by (auto split: prod.split_asm)
                next
                  case (e _)
                  with a1 Some Pair Stackloc s2 KStoptr Storage show ?thesis using lexp.psimps(2) by simp
                qed
              qed
            qed
          qed
        next
          case (Storeloc l)
          then show ?thesis
          proof (cases tp)
            case (Value _)
            with a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp
          next
            case (Calldata _)
            with  a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp
          next
            case (Memory _)
            with a1 Some Pair Storeloc show ?thesis using lexp.psimps(2) by simp
          next
            case (Storage t)
            then show ?thesis
            proof (cases "ssel t l r e cd st g")
              case (n _ _)
              with a1 Some Pair Storeloc Storage show ?thesis using msel_ssel_expr_load_rexp_gas(2) by (auto split: prod.split_asm)
            next
              case (e _)
              with a1 Some Pair Storeloc Storage show ?thesis using lexp.psimps(2) by simp
            qed
          qed
        qed
      qed
    qed
  qed
qed

subsection ‹Semantics of statements›

text ‹The following is a helper function to connect the gas monad with the state monad.›

fun
  toState :: "(State  ('a, 'e, Gas) state_monad)  ('a, 'e, State) state_monad" where
 "toState gm = (λs. case gm s (gas s) of
                     Normal (a,g)  Normal(a,sgas:=g)
                    | Exception e  Exception e)"

lemma wptoState[wprule]:
  assumes "a g. gm s (gas s) = Normal (a, g)  P a (sgas:=g)"
      and "e. gm s (gas s) = Exception e  E e"
    shows "wp (toState gm) P E s"
  using assms unfolding wp_def by (simp split:result.split result.split_asm)

text ‹Now we define the semantics of statements.›
function (domintros) stmt :: "S  Environment  CalldataT  (unit, Ex, State) state_monad"
  where "stmt SKIP e cd st =
    (do {
      assert Gas (λst. gas st > costs SKIP e cd st);
      modify (λst. stgas := gas st - costs SKIP e cd st)
    }) st"
| "stmt (ASSIGN lv ex) env cd st =
    (do {
      assert Gas (λst. gas st > costs (ASSIGN lv ex) env cd st);
      modify (λst. stgas := gas st - costs (ASSIGN lv ex) env cd st);
      re  toState (expr ex env cd);
      case re of
        (KValue v, Value t) 
          do {
            rl  toState (lexp lv env cd);
            case rl of
              (LStackloc l, Value t') 
                do {
                  v'  option Err (λ_. convert t t' v);
                  modify (λst. st stack := updateStore l (KValue v') (stack st))
                }
            | (LStoreloc l, Storage (STValue t')) 
                do {
                  v'  option Err (λ_. convert t t' v);
                  modify (λst. ststorage := (storage st) (address env := fmupd l v' (storage st (address env))))
                }
            | (LMemloc l, Memory (MTValue t')) 
                do {
                  v'  option Err (λ_. convert t t' v);
                  modify (λst. stmemory := updateStore l (MValue v') (memory st))
                }
            | _  throw Err
          }
      | (KCDptr p, Calldata (MTArray x t)) 
          do {
            rl  toState (lexp lv env cd);
            case rl of
              (LStackloc l, Memory _) 
                do {
                  sv  applyf (λst. accessStore l (stack st));
                  p'  case sv of Some (KMemptr p')  return p' | _  throw Err;
                  m  option Err (λst. cpm2m p p' x t cd (memory st));
                  modify (λst. stmemory := m)
                }
            | (LStackloc l, Storage _) 
                do {
                  sv  applyf (λst. accessStore l (stack st));
                  p'  case sv of Some (KStoptr p')  return p' | _  throw Err;
                  s  option Err (λst. cpm2s p p' x t cd (storage st (address env)));
                  modify (λst. st storage := (storage st) (address env := s))
                }
            | (LStoreloc l, _) 
                do {
                  s  option Err (λst. cpm2s p l x t cd (storage st (address env)));
                  modify (λst. st storage := (storage st) (address env := s))
                }
            | (LMemloc l, _) 
                do {
                  m  option Err (λst. cpm2m p l x t cd (memory st));
                  modify (λst. st memory := m)
                }
            | _  throw Err
          }
      | (KMemptr p, Memory (MTArray x t)) 
          do {
            rl  toState (lexp lv env cd);
            case rl of
              (LStackloc l, Memory _)  modify (λst. ststack := updateStore l (KMemptr p) (stack st))
            | (LStackloc l, Storage _) 
                do {
                  sv  applyf (λst. accessStore l (stack st));
                  p'  case sv of Some (KStoptr p')  return p' | _  throw Err;
                  s  option Err (λst. cpm2s p p' x t (memory st) (storage st (address env)));
                  modify (λst. st storage := (storage st) (address env := s))
                }
            | (LStoreloc l, _) 
                do {
                  s  option Err (λst. cpm2s p l x t (memory st) (storage st (address env)));
                  modify (λst. st storage := (storage st) (address env := s))
                }
            | (LMemloc l, _)  modify (λst. st memory := updateStore l (MPointer p) (memory st))
            | _  throw Err
          }
      | (KStoptr p, Storage (STArray x t)) 
          do {
            rl  toState (lexp lv env cd);
            case rl of
              (LStackloc l, Memory _) 
                do {
                  sv  applyf (λst. accessStore l (stack st));
                  p'  case sv of Some (KMemptr p')  return p' | _  throw Err;
                  m  option Err (λst. cps2m p p' x t (storage st (address env)) (memory st));
                  modify (λst. stmemory := m)
                }
            | (LStackloc l, Storage _)  modify (λst. ststack := updateStore l (KStoptr p) (stack st))
            | (LStoreloc l, _) 
                do {
                  s  option Err (λst. copy p l x t (storage st (address env)));
                  modify (λst. st storage := (storage st) (address env := s))
                }
            | (LMemloc l, _) 
                do {
                  m  option Err (λst. cps2m p l x t (storage st (address env)) (memory st));
                  modify (λst. stmemory := m)
                }
            | _  throw Err
          }
      | (KStoptr p, Storage (STMap t t')) 
          do {
            rl  toState (lexp lv env cd);
            l  case rl of (LStackloc l, _)  return l | _  throw Err;
            modify (λst. ststack := updateStore l (KStoptr p) (stack st))
          }
      | _  throw Err
    }) st"
| "stmt (COMP s1 s2) e cd st =
    (do {
      assert Gas (λst. gas st > costs (COMP s1 s2) e cd st);
      modify (λst. stgas := gas st - costs (COMP s1 s2) e cd st);
      stmt s1 e cd;
      stmt s2 e cd
    }) st"
| "stmt (ITE ex s1 s2) e cd st =
    (do {
      assert Gas (λst. gas st > costs (ITE ex s1 s2) e cd st);
      modify (λst. stgas := 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 = ShowLbool True then stmt s1 e cd
      else if b = ShowLbool False then stmt s2 e cd
      else throw Err
    }) st"
| "stmt (WHILE ex s0) e cd st =
    (do {
      assert Gas (λst. gas st > costs (WHILE ex s0) e cd st);
      modify (λst. stgas := 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 = ShowLbool True then
        do {
          stmt s0 e cd;
          stmt (WHILE ex s0) e cd
        }
      else if b = ShowLbool False then return ()
      else throw Err
    }) st"
| "stmt (INVOKE i xe) e cd st =
    (do {
      assert Gas (λst. gas st > costs (INVOKE i xe) e cd st);
      modify (λst. stgas := 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);
      mo  applyf memory;
      (el, cdl, kl, ml)  toState (load False fp xe e' emptyStore emptyStore mo e cd);
      ko  applyf stack;
      modify (λst. ststack:=kl, memory:=ml);
      stmt f el cdl;
      modify (λst. ststack:=ko)
    }) 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. gas st > costs (EXTERNAL ad i xe val) e cd st);
      modify (λst. stgas := gas st - costs (EXTERNAL ad i xe val) e cd st);
      kad  toState (expr ad e cd);
      adv  case kad of (KValue adv, Value TAddr)  return adv | _  throw Err;
      assert Err (λ_. adv  address e);
      c  (λst. case type (accounts st adv) of Some (Contract c)  return c st | _  throw Err st);
      (ct, _, fb)  option Err (λ_. ep $$ c);
      kv  toState (expr val e cd);
      (v, t)  case kv of (KValue v, Value t)  return (v, t) | _  throw Err;
      v'  option Err (λ_. convert t (TUInt 256) v);
      let e' = ffold_init ct (emptyEnv adv c (address e) v') (fmdom ct);
      case ct $$ i of
        Some (Method (fp, True, f)) 
          do {
            (el, cdl, kl, ml)  toState (load True fp xe e' emptyStore emptyStore emptyStore e cd);
            acc  option Err (λst. transfer (address e) adv v' (accounts st));
            (ko, mo)  applyf (λst. (stack st, memory st));
            modify (λst. staccounts := acc, stack:=kl,memory:=ml);
            stmt f el cdl;
            modify (λst. ststack:=ko, memory := mo)
          }
      | None 
          do {
            acc  option Err (λst. transfer (address e) adv v' (accounts st));
            (ko, mo)  applyf (λst. (stack st, memory st));
            modify (λst. staccounts := acc,stack:=emptyStore, memory:=emptyStore);
            stmt fb e' emptyStore;
            modify (λst. ststack:=ko, memory := mo)
          }
      | _  throw Err
    }) st"
| "stmt (TRANSFER ad ex) e cd st =
    (do {
      assert Gas (λst. gas st > costs (TRANSFER ad ex) e cd st);
      modify (λst. stgas := gas st - costs (TRANSFER ad ex) e cd st);
      kv  toState (expr ad e cd);
      adv  case kv of (KValue adv, Value TAddr)  return adv | _  throw Err;
      kv'  toState (expr ex e cd);
      (v, t)  case kv' of (KValue v, Value t)  return (v, t) | _  throw Err;
      v'  option Err (λ_. convert t (TUInt 256) v);
      acc  applyf accounts;
      case type (acc adv) of
        Some (Contract c) 
          do {
            (ct, _, f)  option Err (λ_. ep $$ c);
            let e' = ffold_init ct (emptyEnv adv c (address e) v') (fmdom ct);
            (ko, mo)  applyf (λst. (stack st, memory st));
            acc'  option Err (λst. transfer (address e) adv v' (accounts st));
            modify (λst. staccounts := acc', stack:=emptyStore, memory:=emptyStore);
            stmt f e' emptyStore;
            modify (λst. ststack:=ko, memory := mo)
          }
      | Some EOA 
          do {
            acc'  option Err (λst. transfer (address e) adv v' (accounts st));
            modify (λst. (staccounts := acc'))
          }
      | None  throw Err
    }) st"
| "stmt (BLOCK ((id0, tp), None) s) ev cd st =
    (do {
      assert Gas (λst. gas st > costs (BLOCK ((id0, tp), None) s) ev cd st);
      modify (λst. stgas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st);
      (cd', mem', sck', e')  option Err (λst. decl id0 tp None False cd (memory st) (storage st) (cd, memory st, stack st, ev));
      modify (λst. ststack := sck', memory := mem');
      stmt s e' cd'
    }) st"
| "stmt (BLOCK ((id0, tp), Some ex') s) ev cd st =
    (do {
      assert Gas (λst. gas st > costs(BLOCK ((id0, tp), Some ex') s) ev cd st);
      modify (λst. stgas := gas st - costs (BLOCK ((id0, tp), Some ex') s) ev cd st);
      (v, t)  toState (expr ex' ev cd);
      (cd', mem', sck', e')  option Err (λst. decl id0 tp (Some (v, t)) False cd (memory st) (storage st) (cd, memory st, stack st, ev));
      modify (λst. ststack := sck', memory := mem');
      stmt s e' cd'
    }) st"
(*
  Note: We cannot use (ct, (fp, cn), fb) <- option Err (λ_. ep $$ i)
*)
| "stmt (NEW i xe val) e cd st =
    (do {
      assert Gas (λst. gas st > costs (NEW i xe val) e cd st);
      modify (λst. stgas := gas st - costs (NEW i xe val) e cd st);
      adv  applyf (λst. hash (address e) (ShowLnat (contracts (accounts st (address e)))));
      assert Err (λst. type (accounts st adv) = None);
      kv  toState (expr val e cd);
      (v, t)  case kv of (KValue v, Value t)  return (v, t) | _  throw Err;
      (ct, cn, _)  option Err (λ_. ep $$ i);
      let e' = ffold_init ct (emptyEnv adv i (address e) v) (fmdom ct);
      (el, cdl, kl, ml)  toState (load True (fst cn) xe e' emptyStore emptyStore emptyStore e cd);
      modify (λst. staccounts := (accounts st)(adv := bal = ShowLint 0, type = Some (Contract i), contracts = 0), storage:=(storage st)(adv := {$$}));
      acc  option Err (λst. transfer (address e) adv v (accounts st));
      (ko, mo)  applyf (λst. (stack st, memory st));
      modify (λst. staccounts := acc, stack:=kl, memory:=ml);
      stmt (snd cn) el cdl;
      modify (λst. ststack:=ko, memory := mo);
      modify (incrementAccountContracts (address e))
    }) st"
by pat_completeness auto

subsection ‹Termination›

text ‹Again, to prove termination we need a lemma regarding gas consumption.›

lemma stmt_dom_gas[rule_format]:
    "stmt_dom (s6, ev6, cd6, st6)  (st6'. stmt s6 ev6 cd6 st6 = Normal((), st6')  gas st6'  gas st6)"
proof (induct rule: stmt.pinduct[where ?P="λs6 ev6 cd6 st6. (st6'. stmt s6 ev6 cd6 st6 = Normal ((), st6')  gas st6'  gas st6)"])
  case (1 e cd st)
  then show ?case using stmt.psimps(1) by simp
next
  case (2 lv ex env cd st)
  define g where "g = costs (ASSIGN lv ex) env cd st"
  show ?case
  proof (rule allI[OF impI])
    fix st6'
    assume stmt_def: "stmt (ASSIGN lv ex) env cd st = Normal ((), st6')"
    then show "gas st6'  gas st"
    proof cases
      assume "gas st  g"
      with 2(1) stmt_def show ?thesis using stmt.psimps(2) g_def by simp
    next
      assume "¬ gas st  g"
      define st' where "st' = stgas := gas st - g"
      show ?thesis
      proof (cases "expr ex env cd st' (gas st - g)")
        case (n a g')
        define st'' where "st'' = st'gas := g'"
        then show ?thesis
        proof (cases a)
          case (Pair b c)
          then show ?thesis
          proof (cases b)
            case (KValue v)
            then show ?thesis
            proof (cases c)
              case (Value t)
              then show ?thesis
              proof (cases "lexp lv env cd st'' g'")
                case n2: (n a g'')
                then show ?thesis
                proof (cases a)
                  case p1: (Pair a b)
                  then show ?thesis
                  proof (cases a)
                    case (LStackloc l)
                    then show ?thesis
                    proof (cases b)
                      case v2: (Value t')
                      then show ?thesis
                      proof (cases "convert t t' v ")
                        case None
                        with stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStackloc v2 show ?thesis using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def by simp
                      next
                        case s3: (Some v')
                        with 2(1) `¬ gas st  g` n Pair KValue Value n2 p1 LStackloc v2 s3
                        have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''gas := g'', stack := updateStore l (KValue v') (stack st))"
                          using stmt.psimps(2) g_def st'_def st''_def by simp
                        with stmt_def have "st6'= st''gas := g'', stack := updateStore l (KValue v') (stack st)" by simp
                        moreover from lexp_gas `¬ gas st  g` n2 p1 have "gas (st''gas := g'', stack := updateStore l (KValue v') (stack st))  gas (st'gas := g')" using g_def st'_def by simp
                        moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair KValue Value have "gas (st'gas := g')  gas (stgas := gas st - g)" using g_def by simp
                        ultimately show ?thesis by simp
                      qed
                    next
                      case (Calldata x2)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    next
                      case (Memory x3)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    next
                      case (Storage x4)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    qed
                  next
                    case (LMemloc l)
                    then show ?thesis
                    proof (cases b)
                      case v2: (Value t')
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    next
                      case (Calldata x2)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    next
                      case (Memory x3)
                      then show ?thesis
                      proof (cases x3)
                        case (MTArray x11 x12)
                        with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LMemloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case (MTValue t')
                        then show ?thesis
                        proof (cases "convert t t' v ")
                          case None
                          with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LMemloc Memory MTValue show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                        next
                          case s3: (Some v')
                          with 2(1) `¬ gas st  g` n Pair KValue Value n2 p1 LMemloc Memory MTValue s3
                          have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''gas := g'', memory := updateStore l (MValue v') (memory st''))"
                            using stmt.psimps(2) g_def st'_def st''_def by simp
                          with stmt_def have "st6'= (st''gas := g'', memory := updateStore l (MValue v') (memory st''))" by simp
                          moreover from lexp_gas `¬ gas st  g` n2 p1 have "gas (st''gas := g'', stack := updateStore l (KValue v') (stack st))  gas (st'gas := g')" using g_def st'_def by simp
                          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair KValue Value n2 p1 have "gas (st'gas := g')  gas (stgas := gas st - g)" using g_def by simp
                          ultimately show ?thesis by simp
                        qed
                      qed
                    next
                      case (Storage x4)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    qed
                  next
                    case (LStoreloc l)
                    then show ?thesis
                    proof (cases b)
                      case v2: (Value t')
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    next
                      case (Calldata x2)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    next
                      case (Memory x3)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    next
                      case (Storage x4)
                      then show ?thesis
                      proof (cases x4)
                        case (STArray x11 x12)
                        with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStoreloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case (STMap x21 x22)
                        with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStoreloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case (STValue t')
                        then show ?thesis
                        proof (cases "convert t t' v ")
                          case None
                          with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value n2 p1 LStoreloc Storage STValue show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                        next
                          case s3: (Some v')
                          with 2(1) `¬ gas st  g` n Pair KValue Value n2 p1 LStoreloc Storage STValue s3
                          have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'' gas := g'', storage := (storage st'') (address env := fmupd l v' (storage st'' (address env))))"
                            using stmt.psimps(2) g_def st'_def st''_def by simp
                          with stmt_def have "st6'= st'' gas := g'', storage := (storage st'') (address env := fmupd l v' (storage st'' (address env)))" by simp
                          moreover from lexp_gas `¬ gas st  g` n Pair KValue Value n2 p1 have "gas (st''gas := g'', stack := updateStore l (KValue v') (stack st))  gas (st'gas := g')" using g_def by simp
                          moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair KValue Value n2 p1 have "gas (st'gas := g')  gas (stgas := gas st - g)" using g_def by simp
                          ultimately show ?thesis by simp
                        qed
                      qed
                    qed
                  qed
                qed
              next
                case (e x)
                with 2(1) stmt_def `¬ gas st  g` n Pair KValue Value show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
              qed
            next
              case (Calldata x2)
              with 2(1) stmt_def `¬ gas st  g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp
            next
              case (Memory x3)
              with 2(1) stmt_def `¬ gas st  g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp
            next
              case (Storage x4)
              with 2(1) stmt_def `¬ gas st  g` n Pair KValue show ?thesis using stmt.psimps(2) g_def st'_def by simp
            qed
          next
            case (KCDptr p)
            then show ?thesis
            proof (cases c)
              case (Value x1)
              with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def by simp
            next
              case (Calldata x2)
              then show ?thesis
              proof (cases x2)
                case (MTArray x t)
                then show ?thesis
                proof (cases "lexp lv env cd st'' g'")
                  case n2: (n a g'')
                  define st''' where "st''' = st''gas := g''"
                  then show ?thesis
                  proof (cases a)
                    case p2: (Pair a b)
                    then show ?thesis
                    proof (cases a)
                      case (LStackloc l)
                      then show ?thesis
                      proof (cases b)
                        case v2: (Value t')
                        with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case c2: (Calldata x2)
                        with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case (Memory x3)
                        then show ?thesis
                        proof (cases "accessStore l (stack st''')")
                          case None
                          with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                        next
                          case s3: (Some a)
                          then show ?thesis
                          proof (cases a)
                            case (KValue x1)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case c3: (KCDptr x2)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case (KMemptr p')
                            then show ?thesis
                            proof (cases "cpm2m p p' x t cd (memory st''')")
                              case None
                              with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by (simp split:if_split_asm)
                            next
                              case (Some m')
                              with `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 KMemptr
                              have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' memory := m')"
                                using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp
                              with stmt_def have "st6'= st''' memory := m'" by simp
                              moreover from lexp_gas `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 have "gas (st'''memory := m')  gas st''" using st''_def st'''_def by simp
                              moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                              ultimately show ?thesis using st'_def by simp
                            qed
                          next
                            case (KStoptr p')
                            with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          qed
                        qed
                      next
                        case (Storage x4)
                        then show ?thesis
                        proof (cases "accessStore l (stack st'')")
                          case None
                          with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                        next
                          case s3: (Some a)
                          then show ?thesis
                          proof (cases a)
                            case (KValue x1)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case c3: (KCDptr x2)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case (KMemptr x3)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case (KStoptr p')
                            then show ?thesis
                            proof (cases "cpm2s p p' x t cd (storage st'' (address env))")
                              case None
                              with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                            next
                              case (Some s')
                              with 2(1) `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStackloc Storage s3 KStoptr
                              have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' storage := (storage st'') (address env := s'))"
                                using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                              with stmt_def have "st6'= st''' storage := (storage st'') (address env := s')" by simp
                              moreover from lexp_gas `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st'''  gas st''" using g_def st''_def st'''_def by simp
                              moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using g_def st'_def st''_def by simp
                              ultimately show ?thesis using st'_def by simp
                            qed
                          qed
                        qed
                      qed
                    next
                      case (LMemloc l)
                      then show ?thesis
                      proof (cases "cpm2m p l x t cd (memory st''')")
                        case None
                        with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by (simp split:if_split_asm)
                      next
                        case (Some m)
                        with `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LMemloc
                        have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''memory := m)"
                          using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp
                        with stmt_def have "st6'= (st'''memory := m)" by simp
                        moreover from lexp_gas `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st'''  gas st''" using st''_def st'''_def by simp
                        moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                        ultimately show ?thesis using st'_def by simp
                      qed
                    next
                      case (LStoreloc l)
                      then show ?thesis
                      proof (cases "cpm2s p l x t cd (storage st'' (address env))")
                        case None
                        with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                      next
                        case (Some s)
                        with `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 LStoreloc
                        have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' storage := (storage st'') (address env := s))"
                          using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp
                        with stmt_def have "st6'= (st'''storage := (storage st'') (address env := s))" by simp
                        moreover from lexp_gas `¬ gas st  g` n Pair KCDptr Calldata MTArray n2 p2 have "gas st'''  gas st''" using st''_def st'''_def by simp
                        moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                        ultimately show ?thesis using st'_def by simp
                      qed
                    qed
                  qed
                next
                  case (e x)
                  with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata MTArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                qed
              next
                case (MTValue x2)
                with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr Calldata show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
              qed
            next
              case (Memory x3)
              with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
            next
              case (Storage x4)
              with 2(1) stmt_def `¬ gas st  g` n Pair KCDptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
            qed
          next
            case (KMemptr p)
            then show ?thesis
            proof (cases c)
              case (Value x1)
              with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
            next
              case (Calldata x2)
              with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
            next
              case (Memory x3)
              then show ?thesis
              proof (cases x3)
                case (MTArray x t)
                then show ?thesis
                proof (cases "lexp lv env cd st'' g'")
                  case n2: (n a g'')
                  define st''' where "st''' = st''gas := g''"
                  then show ?thesis
                  proof (cases a)
                    case p2: (Pair a b)
                    then show ?thesis
                    proof (cases a)
                      case (LStackloc l)
                      then show ?thesis
                      proof (cases b)
                        case v2: (Value t')
                        with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case c2: (Calldata x2)
                        with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case m2: (Memory x3)
                        with 2(1) `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc
                        have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''stack := updateStore l (KMemptr p) (stack st''))"
                          using stmt.psimps(2)[OF 2(1)] g_def st'_def st''_def st'''_def by simp
                        with stmt_def have "st6'= st'''stack := updateStore l (KMemptr p) (stack st'')" by simp
                        moreover from lexp_gas `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 have "gas st'''  gas st''" using st''_def st'''_def by simp
                        moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                        ultimately show ?thesis using st'_def by simp
                      next
                        case (Storage x4)
                        then show ?thesis
                        proof (cases "accessStore l (stack st''')")
                          case None
                          with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                        next
                          case s3: (Some a)
                          then show ?thesis
                          proof (cases a)
                            case (KValue x1)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case c3: (KCDptr x2)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case m3: (KMemptr x3)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case (KStoptr p')
                            then show ?thesis
                            proof (cases "cpm2s p p' x t (memory st''') (storage st''' (address env))")
                              case None
                              with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                            next
                              case (Some s)
                              with 2(1) `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStackloc Storage s3 KStoptr
                              have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''storage := (storage st''') (address env := s))"
                                using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                              with stmt_def have "st6'= st'''storage := (storage st''') (address env := s)" by simp
                              moreover from lexp_gas `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 have "gas st'''  gas st''" using g_def st'_def st''_def st'''_def by simp
                              moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                              ultimately show ?thesis using st'_def by simp
                            qed
                          qed
                        qed
                      qed
                    next
                      case (LMemloc l)
                      with 2(1) `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LMemloc
                      have "stmt (ASSIGN lv ex) env cd st =  Normal ((), st'''memory := updateStore l (MPointer p) (memory st'''))"
                        using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                      with stmt_def have "st6'= st'''memory := updateStore l (MPointer p) (memory st''')" by simp
                      moreover from lexp_gas `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 have "gas st'''  gas st''" using g_def st'_def st''_def st'''_def by simp
                      moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                      ultimately show ?thesis using st'_def by simp
                    next
                      case (LStoreloc l)
                      then show ?thesis
                      proof (cases "cpm2s p l x t (memory st''') (storage st'' (address env))")
                        case None
                        with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def using st'_def st''_def st'''_def by simp
                      next
                        case (Some s)
                        with 2(1) `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 LStoreloc
                        have "stmt (ASSIGN lv ex) env cd st =  Normal ((), st'''storage := (storage st''') (address env := s))"
                          using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                        with stmt_def have "st6'= st'''storage := (storage st''') (address env := s)" by simp
                        moreover from lexp_gas `¬ gas st  g` n Pair KMemptr Memory MTArray n2 p2 have "gas st'''  gas st''" using g_def st'_def st''_def st'''_def by simp
                        moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                        ultimately show ?thesis using st'_def by simp
                      qed
                    qed
                  qed
                next
                  case (e _)
                  with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory MTArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                qed
              next
                case (MTValue _)
                with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
              qed
            next
              case (Storage x4)
              with 2(1) stmt_def `¬ gas st  g` n Pair KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
            qed
          next
            case (KStoptr p)
            then show ?thesis
            proof (cases c)
              case (Value x1)
              with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
            next
              case (Calldata x2)
              with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
            next
              case (Memory x3)
              with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
            next
              case (Storage x4)
              then show ?thesis
              proof (cases x4)
                case (STArray x t)
                then show ?thesis
                proof (cases "lexp lv env cd st'' g'")
                  case n2: (n a g'')
                  define st''' where "st''' = st''gas := g''"
                  then show ?thesis
                  proof (cases a)
                    case p2: (Pair a b)
                    then show ?thesis
                    proof (cases a)
                      case (LStackloc l)
                      then show ?thesis
                      proof (cases b)
                        case v2: (Value t')
                        with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case c2: (Calldata x2)
                        with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                      next
                        case (Memory x3)
                        then show ?thesis
                        proof (cases "accessStore l (stack st''')")
                          case None
                          with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                        next
                          case s3: (Some a)
                          then show ?thesis
                          proof (cases a)
                            case (KValue x1)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case c3: (KCDptr x2)
                            with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          next
                            case (KMemptr p')
                            then show ?thesis
                            proof (cases "cps2m p p' x t (storage st''' (address env)) (memory st''')")
                              case None
                              with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 KMemptr show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                            next
                              case (Some m)
                              with 2(1) `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 KMemptr
                              have "stmt (ASSIGN lv ex) env cd st =  Normal ((), st'''memory := m)"
                                using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                              with stmt_def have "st6'= st'''memory := m" by simp
                              moreover from lexp_gas `¬ gas st  g` n Pair KMemptr Storage STArray n2 p2 have "gas (st'''memory := m)  gas st''" using g_def st'_def st''_def st'''_def by simp
                              moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                              ultimately show ?thesis using st'_def by simp
                            qed
                          next
                            case sp2: (KStoptr p')
                            with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc Memory s3 show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                          qed
                        qed
                      next
                        case st2: (Storage x4)
                        with 2(1) `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStackloc
                        have "stmt (ASSIGN lv ex) env cd st =  Normal ((), st'''stack := updateStore l (KStoptr p) (stack st'''))"
                          using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                        with stmt_def have "st6'= st'''stack := updateStore l (KStoptr p) (stack st''')" by simp
                        moreover from lexp_gas `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''stack := updateStore l (KStoptr p) (stack st'''))  gas st''" using g_def st'_def st''_def st'''_def by simp
                        moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                        ultimately show ?thesis using st'_def by simp
                      qed
                    next
                      case (LMemloc l)
                      then show ?thesis
                      proof (cases "cps2m p l x t (storage st'' (address env)) (memory st'')")
                        case None
                        with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LMemloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                      next
                        case (Some m)
                        with 2(1) `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LMemloc
                        have "stmt (ASSIGN lv ex) env cd st =  Normal ((), st'''memory := m)"
                          using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                        with stmt_def have "st6'= (st'''memory := m)" by simp
                        moreover from lexp_gas `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''memory := m)  gas st''" using g_def st'_def st''_def st'''_def by simp
                        moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                        ultimately show ?thesis using st'_def by simp
                      qed
                    next
                      case (LStoreloc l)
                      then show ?thesis
                      proof (cases "copy p l x t (storage st'' (address env))")
                        case None
                        with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStoreloc show ?thesis using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                      next
                        case (Some s)
                        with 2(1) `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 LStoreloc
                        have "stmt (ASSIGN lv ex) env cd st = Normal ((), st'''storage := (storage st''') (address env := s))"
                          using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                        with stmt_def have "st6'= st'''storage := (storage st''') (address env := s)" by simp
                        moreover from lexp_gas `¬ gas st  g` n Pair KStoptr Storage STArray n2 p2 have "gas (st'''storage := (storage st''') (address env := s'))  gas st''" using g_def st'_def st''_def st'''_def by simp
                        moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                        ultimately show ?thesis using st'_def by simp
                      qed
                    qed
                  qed
                next
                  case (e x)
                  with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STArray show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                qed
              next
                case (STMap t t')
                then show ?thesis
                proof (cases "lexp lv env cd st'' g'")
                  case n2: (n a g'')
                  define st''' where "st''' = st''gas := g''"
                  then show ?thesis
                  proof (cases a)
                    case p2: (Pair a b)
                    then show ?thesis
                    proof (cases a)
                      case (LStackloc l)
                      with 2(1) `¬ gas st  g` n Pair KStoptr Storage STMap n2 p2
                      have "stmt (ASSIGN lv ex) env cd st = Normal ((), st''' stack := updateStore l (KStoptr p) (stack st'''))"
                        using stmt.psimps(2) g_def st'_def st''_def st'''_def by simp
                      with stmt_def have "st6'= st'''stack := updateStore l (KStoptr p) (stack st''')" by simp
                      moreover from lexp_gas `¬ gas st  g` n Pair KStoptr Storage STMap n2 p2 have "gas (st'''stack := updateStore l (KStoptr p) (stack st'''))  gas st''" using g_def st'_def st''_def st'''_def by simp
                      moreover from msel_ssel_expr_load_rexp_gas(3)[of ex env cd st' "gas st - g"] `¬ gas st  g` n Pair have "gas st''  gas st'" using st'_def st''_def by simp
                      ultimately show ?thesis using st'_def by simp
                    next
                      case (LMemloc x2)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STMap n2 p2 show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    next
                      case (LStoreloc x3)
                      with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STMap n2 p2 show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                    qed
                  qed
                next
                  case (e x)
                  with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage STMap show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
                qed
              next
                case (STValue x3)
                with 2(1) stmt_def `¬ gas st  g` n Pair KStoptr Storage show ?thesis using stmt.psimps(2) g_def st'_def st''_def by simp
              qed
            qed
          qed
        qed
      next
        case (e x)
        with 2(1) stmt_def `¬ gas st  g` show ?thesis using stmt.psimps(2) g_def st'_def by simp
      qed
    qed
  qed
next
  case (3 s1 s2 e cd st)
  define g where "g = costs (COMP s1 s2) e cd st"
  show ?case
  proof (rule allI[OF impI])
    fix st6'
    assume stmt_def: "stmt (COMP s1 s2) e cd st = Normal ((), st6')"
    then show "gas st6'  gas st"
    proof cases
      assume "gas st  g"
      with 3(1) stmt_def g_def show ?thesis using stmt.psimps(3) by simp
    next
      assume "¬ gas st  g"
      show ?thesis
      proof (cases "stmt s1 e cd (stgas := gas st - g)")
        case (n a st')
        with 3(1) stmt_def `¬ gas st  g` have "stmt (COMP s1 s2) e cd st = stmt s2 e cd st'" using stmt.psimps(3)[of s1 s2 e cd st] g_def by (simp add:Let_def split:unit.split_asm)
        with 3(3) stmt_def ¬ gas st  g n have "gas st6'  gas st'" using g_def by simp
        moreover from 3(2)[where ?s'a="stgas := gas st - g"] ¬ gas st  g n have "gas st'  gas st" using g_def by simp
        ultimately show ?thesis by simp
      next
        case (e x)
        with 3 stmt_def `¬ gas st  g` show ?thesis using stmt.psimps(3)[of s1 s2 e cd st] g_def by (simp split: Ex.split_asm)
      qed
    qed
  qed
next
  case (4 ex s1 s2 e cd st)
  define g where "g = costs (ITE ex s1 s2) e cd st"
  show ?case
  proof (rule allI[OF impI])
    fix st6'
    assume stmt_def: "stmt (ITE ex s1 s2) e cd st = Normal ((), st6')"
    then show "gas st6'  gas st"
    proof cases
      assume "gas st  g"
      with 4(1) stmt_def show ?thesis using stmt.psimps(4) g_def by simp
    next
      assume "¬ gas st  g"
      then have l1: "assert Gas (λst. costs (ITE ex s1 s2) e cd st < gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = stgas := gas st - g"
      then have l2: " modify (λst. stgas := gas st - costs (ITE ex s1 s2) e cd st) st = Normal ((), st')" using g_def by simp
      show ?thesis
      proof (cases "expr ex e cd st' (gas st - g)")
        case (n a g')
        define st'' where "st'' = st'gas := g'"
        with n have l3: "toState (expr ex e cd) st' = Normal (a, st'')" using st'_def by simp
        then show ?thesis
        proof (cases a)
          case (Pair b c)
          then show ?thesis
          proof (cases b)
            case (KValue b)
            then show ?thesis
            proof (cases c)
              case (Value x1)
              then show ?thesis
              proof (cases x1)
                case (TSInt x1)
                with 4(1) stmt_def `¬ gas st  g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def by simp
              next
                case (TUInt x2)
                with 4(1) stmt_def `¬ gas st  g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def by simp
              next
                case TBool
                then show ?thesis
                proof cases
                  assume "b = ShowLbool True"
                  with 4(1) `¬ gas st  g` n Pair KValue Value TBool have "stmt (ITE ex s1 s2) e cd st = stmt s1 e cd st''" using stmt.psimps(4) g_def st'_def st''_def by simp
                  with 4(2)[OF l1 l2 l3] stmt_def `¬ gas st  g` n Pair KValue Value TBool `b = ShowLbool True` have "gas st6'  gas st''" using g_def by simp
                  moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `¬ gas st  g` n Pair KValue Value TBool have "gas st''  gas st'" using st'_def st''_def by simp
                  ultimately show ?thesis using st'_def by simp
                next
                  assume nt: "¬ b = ShowLbool True"
                  show ?thesis
                  proof cases
                    assume "b = ShowLbool False"
                    with 4(1) `¬ gas st  g` n Pair KValue Value TBool nt have "stmt (ITE ex s1 s2) e cd st = stmt s2 e cd st''" using stmt.psimps(4) g_def st'_def st''_def by simp
                    with 4(3)[OF l1 l2 l3] stmt_def `¬ gas st  g` n Pair KValue Value TBool nt `b = ShowLbool False` have "gas st6'  gas st''" using g_def by simp
                    moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `¬ gas st  g` n Pair KValue Value TBool have "gas st''  gas st'" using st'_def st''_def by simp
                    ultimately show ?thesis using st'_def by simp
                  next
                    assume "¬ b = ShowLbool False"
                    with 4(1) stmt_def `¬ gas st  g` n Pair KValue Value TBool nt show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
                  qed
                qed
              next
                case TAddr
                with 4(1) stmt_def `¬ gas st  g` n Pair KValue Value show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
              qed
            next
              case (Calldata x2)
              with 4(1) stmt_def `¬ gas st  g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
            next
              case (Memory x3)
              with 4(1) stmt_def `¬ gas st  g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
            next
              case (Storage x4)
              with 4(1) stmt_def `¬ gas st  g` n Pair KValue show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
            qed
          next
            case (KCDptr x2)
            with 4(1) stmt_def `¬ gas st  g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
          next
            case (KMemptr x3)
            with 4(1) stmt_def `¬ gas st  g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
          next
            case (KStoptr x4)
            with 4(1) stmt_def `¬ gas st  g` n Pair show ?thesis using stmt.psimps(4) g_def st'_def st''_def by simp
          qed
        qed
      next
        case (e e)
        with 4(1) stmt_def `¬ gas st  g` show ?thesis using stmt.psimps(4) g_def st'_def by simp
      qed
    qed
  qed
next
  case (5 ex s0 e cd st)
  define g where "g = costs (WHILE ex s0) e cd st"
  show ?case
  proof (rule allI[OF impI])
    fix st6'
    assume stmt_def: "stmt (WHILE ex s0) e cd st = Normal ((), st6')"
    then show "gas st6'  gas st"
    proof cases
      assume "gas st  g"
      with 5(1) stmt_def show ?thesis using stmt.psimps(5) g_def by simp
    next
      assume gcost: "¬ gas st  g"
      then have l1: "assert Gas (λst. costs (WHILE ex s0) e cd st < gas st) st = Normal ((), st) " using g_def by simp
      define st' where "st' = stgas := gas st - g"
      then have l2: " modify (λst. stgas := gas st - costs (WHILE ex s0) e cd st) st = Normal ((), st')" using g_def by simp
      show ?thesis
      proof (cases "expr ex e cd st' (gas st - g)")
        case (n a g')
        define st'' where "st'' = st'gas := g'"
        with n have l3: "toState (expr ex e cd) st' = Normal (a, st'')" using st'_def by simp
        then show ?thesis
        proof (cases a)
          case (Pair b c)
          then show ?thesis
          proof (cases b)
            case (KValue b)
            then show ?thesis
            proof (cases c)
              case (Value x1)
              then show ?thesis
              proof (cases x1)
                case (TSInt x1)
                with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def by simp
              next
                case (TUInt x2)
                with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def by simp
              next
                case TBool
                then show ?thesis
                proof cases
                  assume "b = ShowLbool 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 = ShowLbool 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 = ShowLbool True` n have "gas st6'  gas st'''" using g_def st'_def st''_def by simp
                    moreover from 5(2)[OF l1 l2 l3] gcost n2 Pair KValue Value TBool `b = ShowLbool True` n have "gas st'''  gas st''" using g_def by simp
                    moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `¬ gas st  g` n Pair KValue Value TBool have "gas st''  gas st'" using st'_def st''_def by simp
                    ultimately show ?thesis using st'_def by simp
                  next
                    case (e x)
                    with 5(1) stmt_def gcost n Pair KValue Value TBool `b = ShowLbool True` show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
                  qed
                next
                  assume nt: "¬ b = ShowLbool True"
                  show ?thesis
                  proof cases
                    assume "b = ShowLbool False"
                    with 5(1) gcost n Pair KValue Value TBool nt have "stmt (WHILE ex s0) e cd st = return () st''" using stmt.psimps(5) g_def st'_def st''_def by simp
                    with stmt_def have "gas st6'  gas st''" by simp
                    moreover from msel_ssel_expr_load_rexp_gas(3)[of ex e cd st' "gas st - g"] `¬ gas st  g` n Pair KValue Value TBool have "gas st''  gas st'" using st'_def st''_def by simp
                    ultimately show ?thesis using g_def st'_def st''_def by simp
                  next
                    assume "¬ b = ShowLbool False"
                    with 5(1) stmt_def gcost n Pair KValue Value TBool nt show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
                  qed
                qed
              next
                case TAddr
                with 5(1) stmt_def gcost n Pair KValue Value show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
              qed
            next
              case (Calldata x2)
              with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
            next
              case (Memory x3)
              with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
            next
              case (Storage x4)
              with 5(1) stmt_def gcost n Pair KValue show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
            qed
          next
            case (KCDptr x2)
            with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
          next
            case (KMemptr x3)
            with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
          next
            case (KStoptr x4)
            with 5(1) stmt_def gcost n Pair show ?thesis using stmt.psimps(5) g_def st'_def st''_def by simp
          qed
        qed
      next
        case (e e)
        with 5(1) stmt_def gcost show ?thesis using stmt.psimps(5) g_def st'_def by simp
      qed
    qed
  qed
next
  case (6 i xe e cd st)
  define g where "g = costs (INVOKE i xe) e cd st"
  show ?case
  proof (rule allI[OF impI])
    fix st6' assume a1: "stmt (INVOKE i xe) e cd st = Normal ((), st6')"
    show "gas st6'  gas st"
    proof (cases)
      assume "gas st  g"
      with 6(1) a1 show