Theory Expressions

section ‹Expressions›
theory Expressions
  imports Contracts StateMonad
begin

subsection ‹Semantics of Expressions›

definition lift ::
  "(e ⇒ environment ⇒ calldataT ⇒ state ⇒ (stackvalue * type, ex, gas) state_monad)
  ⇒ (types ⇒ types ⇒ valuetype ⇒ valuetype ⇒ (valuetype * types) option)
  ⇒ e ⇒ e ⇒ environment ⇒ calldataT ⇒ state ⇒ (stackvalue * type, ex, gas) state_monad"
where
  "lift expr f e1 e2 e cd st ≡
    (do {
      kv1 ← expr e1 e cd st;
      (v1, t1) ← case kv1 of (KValue v1, Value t1) ⇒ return (v1, t1) | _ ⇒ (throw Err::(valuetype * types, ex, gas) state_monad);
      kv2 ← expr e2 e cd st;
      (v2, t2) ← case kv2 of (KValue v2, Value t2) ⇒ return (v2, t2) | _ ⇒ (throw Err::(valuetype * types, ex, gas) state_monad);
      (v, t) ← (option Err (λ_::gas. f t1 t2 v1 v2))::(valuetype * types, ex, gas) state_monad;
      return (KValue v, Value t)::(stackvalue * type, ex, gas) state_monad
    })"
declare lift_def[simp]

lemma lift_cong [fundef_cong]:
  assumes "expr e1 e cd st g = expr' e1 e cd st g"
      and "⋀v g'. expr' e1 e cd st g = Normal (v,g') ⟹ expr e2 e cd st g' = expr' e2 e cd st g'"
  shows "lift expr f e1 e2 e cd st g = lift expr' f e1 e2 e cd st g"
  unfolding lift_def using assms by (auto split: prod.split_asm result.split option.split_asm option.split stackvalue.split type.split)

datatype (discs_sels) ltype
  = LStackloc location
  | LMemloc location
  | LStoreloc location

locale expressions_with_gas =
  fixes costs⇩e :: "e ⇒ environment ⇒ calldataT ⇒ state ⇒ gas"
    and ep::environment⇩p
  assumes call_not_zero[termination_simp]: "⋀e cd st i ix. 0 < (costs⇩e (CALL i ix) e cd st)"
      and ecall_not_zero[termination_simp]: "⋀e cd st a i ix. 0 < (costs⇩e (ECALL a i ix) e cd st)"
begin
function (domintros) msel::"bool ⇒ mtypes ⇒ location ⇒ e list ⇒ environment ⇒ calldataT ⇒ state ⇒ (location * mtypes, ex, gas) state_monad"
     and ssel::"stypes ⇒ location ⇒ e list ⇒ environment ⇒ calldataT ⇒ state ⇒ (location * stypes, ex, gas) state_monad"
     and expr::"e ⇒ environment ⇒ calldataT ⇒ state ⇒ (stackvalue * type, ex, gas) state_monad"
     and load :: "bool ⇒ (Identifier × type) list ⇒ e list ⇒ environment ⇒ calldataT ⇒ stack ⇒ memoryT ⇒ environment ⇒ calldataT ⇒ state ⇒ (environment × calldataT × stack × memoryT, ex, gas) state_monad"
     and rexp::"l ⇒ environment ⇒ calldataT ⇒ state ⇒ (stackvalue * type, ex, gas) state_monad"
where
  "msel _ _ _ [] _ _ _ g = throw Err g"
| "msel _ (MTValue _) _ _ _ _ _ g = throw Err g"
| "msel _ (MTArray al t) loc [x] env cd st g =
    (do {
      kv ← expr x env cd st;
      (v, b) ← case kv of (KValue v, Value (TUInt b)) ⇒ return (v, b) | _ ⇒ throw Err;
      assert Err (λ_. less (TUInt b) (TUInt b256) v (ShowL⇩i⇩n⇩t (int al)) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool));
      return (hash loc v, t)
    }) g"
(*
  Note that it is indeed possible to modify the state while evaluating the expression
  to determine the index of the array to look up.
*)
| "msel mm (MTArray al t) loc (x # y # ys) env cd st g =
    (do {
      kv ← expr x env cd st;
      (v, b) ← case kv of (KValue v, Value (TUInt b)) ⇒ return (v, b) | _ ⇒ throw Err;
      assert Err (λ_. less (TUInt b) (TUInt b256) v (ShowL⇩i⇩n⇩t (int al)) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool));
      l ← case accessStore (hash loc v) (if mm then Memory st else cd) of Some (MPointer l) ⇒ return l | _ ⇒ throw Err;
      msel mm t l (y#ys) env cd st
    }) g"
| "ssel tp loc Nil _ _ _ g = return (loc, tp) g"
| "ssel (STValue _) _ (_ # _) _ _ _ g = throw Err g"
| "ssel (STArray al t) loc (x # xs) env cd st g =
    (do {
      kv ← expr x env cd st;
      (v, b) ← case kv of (KValue v, Value (TUInt b)) ⇒ return (v, b) | _ ⇒ throw Err;
      assert Err (λ_. less (TUInt b) (TUInt b256) v (ShowL⇩i⇩n⇩t (int al)) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool));
      ssel t (hash loc v) xs env cd st
    }) g"
| "ssel (STMap t t') loc (x # xs) env cd st g =
    (do {
      kv ← expr x env cd st;
      (v, t'') ← case kv of (KValue v, Value t'') ⇒ return (v, t'') | _ ⇒ throw Err;
      assert Err (λ_. comp t'' t);
      ssel t' (hash loc v) xs env cd st
    }) g"
| "expr (e.INT b x) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (e.INT b x) e cd st);
      modify (λg. g - costs⇩e (e.INT b x) e cd st);
      return (KValue (createSInt b x), Value (TSInt b))
    }) g"
| "expr (UINT b x) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (UINT b x) e cd st);
      modify (λg. g - costs⇩e (UINT b x) e cd st);
      return (KValue (createUInt b x), Value (TUInt b))
  }) g"
| "expr (ADDRESS ad) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (ADDRESS ad) e cd st);
      modify (λg. g - costs⇩e  (ADDRESS ad) e cd st);
      return (KValue (createAddress ad), Value TAddr)
    }) g"
| "expr (BALANCE ad) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (BALANCE ad) e cd st);
      modify (λg. g - costs⇩e  (BALANCE ad) e cd st);
      kv ← expr ad e cd st;
      adv ← case kv of (KValue adv, Value TAddr) ⇒ return adv | _ ⇒ throw Err; 
      return (KValue (Bal ((Accounts st) adv)), Value (TUInt b256))
    }) g"
| "expr THIS e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e THIS e cd st);
      modify (λg. g - costs⇩e THIS e cd st);
      return (KValue (Address e), Value TAddr)
    }) g"
| "expr SENDER e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e SENDER e cd st);
      modify (λg. g - costs⇩e SENDER e cd st);
      return (KValue (Sender e), Value TAddr)
    }) g"
| "expr VALUE e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e VALUE e cd st);
      modify (λg. g - costs⇩e VALUE e cd st);
      return (KValue (Svalue e), Value (TUInt b256))
    }) g"
| "expr TRUE e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e TRUE e cd st);
      modify (λg. g - costs⇩e TRUE e cd st);
      return (KValue (ShowL⇩b⇩o⇩o⇩l True), Value TBool)
    }) g"
| "expr FALSE e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e FALSE e cd st);
      modify (λg. g - costs⇩e FALSE e cd st);
      return (KValue (ShowL⇩b⇩o⇩o⇩l False), Value TBool)
    }) g"
| "expr (NOT x) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (NOT x) e cd st);
      modify (λg. g - costs⇩e (NOT x) e cd st);
      kv ← expr x e cd st;
      v ← case kv of (KValue v, Value TBool) ⇒ return v | _ ⇒ throw Err;
      (if v = ShowL⇩b⇩o⇩o⇩l True then expr FALSE e cd st
       else if v = ShowL⇩b⇩o⇩o⇩l False then expr TRUE e cd st
       else throw Err)
    }) g"
| "expr (PLUS e1 e2) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (PLUS e1 e2) e cd st);
      modify (λg. g - costs⇩e (PLUS e1 e2) e cd st);
      lift expr add e1 e2 e cd st
    }) g"
| "expr (MINUS e1 e2) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (MINUS e1 e2) e cd st);
      modify (λg. g - costs⇩e (MINUS e1 e2) e cd st);
      lift expr sub e1 e2 e cd st
    }) g"
| "expr (LESS e1 e2) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (LESS e1 e2) e cd st);
      modify (λg. g - costs⇩e (LESS e1 e2) e cd st);
      lift expr less e1 e2 e cd st
    }) g"
| "expr (EQUAL e1 e2) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (EQUAL e1 e2) e cd st);
      modify (λg. g - costs⇩e (EQUAL e1 e2) e cd st);
      lift expr equal e1 e2 e cd st
    }) g"
| "expr (AND e1 e2) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (AND e1 e2) e cd st);
      modify (λg. g - costs⇩e (AND e1 e2) e cd st);
      lift expr vtand e1 e2 e cd st
    }) g"
| "expr (OR e1 e2) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (OR e1 e2) e cd st);
      modify (λg. g - costs⇩e (OR e1 e2) e cd st);
      lift expr vtor e1 e2 e cd st
    }) g"
| "expr (LVAL i) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (LVAL i) e cd st);
      modify (λg. g - costs⇩e (LVAL i) e cd st);
      rexp i e cd st
    }) g"
(* Notes about method calls:
   - Internal method calls use a fresh environment and stack but keep the Memory [1]
   - External method calls use a fresh environment and stack and Memory [2]
   [1]: https://docs.soliditylang.org/en/v0.8.5/control-structures.html#internal-function-calls
   [2]: https://docs.soliditylang.org/en/v0.8.5/control-structures.html#external-function-calls
*)
| "expr (CALL i xe) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (CALL i xe) e cd st);
      modify (λg. g - costs⇩e (CALL i xe) e cd st);
      (ct, _) ← option Err (λ_. ep $$ (Contract e));
      (fp, x) ← case ct $$ i of Some (Function (fp, False, x)) ⇒ return (fp, x) | _ ⇒ throw Err;
      let e' = ffold_init ct (emptyEnv (Address e) (Contract e) (Sender e) (Svalue e)) (fmdom ct);
      (e⇩l, cd⇩l, k⇩l, m⇩l) ← load False fp xe e' emptyTypedStore emptyStore (Memory st) e cd st;
      (val, typ) ← expr x e⇩l cd⇩l (st⦇Stack:=k⇩l, Memory:=m⇩l⦈);
      case val of KValue x ⇒ return (val,typ)
      | KCDptr cdloc ⇒  throw Err
      | KMemptr memloc ⇒ throw Err
      | KStoptr storloc ⇒ return (val, typ)
    }) g"
(*It is not allowed to transfer money to external function calls*)
| "expr (ECALL ad i xe) e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e (ECALL ad i xe) e cd st);
      modify (λg. g - costs⇩e (ECALL ad i xe) e cd st);
      kad ← expr ad e cd st;
      adv ← case kad of (KValue adv, Value TAddr) ⇒ return adv | _ ⇒ throw Err;
      assert Err (λ_. adv ≠ Address e);
      c ← case Type (Accounts st adv) of Some (atype.Contract c) ⇒ return c | _ ⇒ throw Err;
      (ct, _) ← option Err (λ_. ep $$ c);
      (fp, x) ← case ct $$ i of Some (Function (fp, True, x)) ⇒ return (fp, x) | _ ⇒ throw Err;
      let e' = ffold_init ct (emptyEnv adv c (Address e) (ShowL⇩n⇩a⇩t 0)) (fmdom ct);
      (e⇩l, cd⇩l, k⇩l, m⇩l) ← load True fp xe e' emptyTypedStore emptyStore emptyTypedStore e cd st;
      (val, typ) ← expr x e⇩l cd⇩l (st⦇Stack:=k⇩l, Memory:=m⇩l⦈);
      case val of KValue x ⇒ return (val,typ)
      | KCDptr cdloc ⇒  throw Err
      | KMemptr memloc ⇒ throw Err
      | KStoptr storloc ⇒ throw Err
    }) g"

(* 
in practice cp True means the caller is external
 (bt) 24/04/25: Added a check which prevents function parameters from sharing variable names with values that already have been declared.
            In practice this only really impacts Contract variables by preventing function parameters from sharing the same name as "global" Contract variable names. 
            This would just require a different name to be used by the user, which would be semantically identical but much easier to prove properties over.
            In theory this will also stop two function parameters from sharing the same name (which should be true anyway)
*)
| "load cp ((i⇩p, t⇩p)#pl) (ex#el) e⇩v' cd' sck' mem' e⇩v cd st g =
    (if (case t⇩p of type.Storage x ⇒ cp | _ ⇒ False) then throw Err
     else
        (case Denvalue e⇩v' $$ i⇩p of Some x' ⇒ throw Err
        | None ⇒
        do {
        (v, t) ← expr ex e⇩v cd st;
        (c, m, k, e) ← (case decl i⇩p t⇩p (Some (v,t)) cp cd (Memory st) ((Storage st) (Address e⇩v)) (cd', mem',  sck', e⇩v')
                          of Some (c, m, k, e) ⇒ return (c, m, k, e)
                          | None ⇒ throw Err);
        load cp pl el e c k m e⇩v cd st})) g"
| "load _ [] (_#_) _ _ _ _ _ _ _ g = throw Err g"
| "load _ (_#_) [] _ _ _ _ _ _ _ g = throw Err g"
| "load _ [] [] e⇩v' cd' sck' mem' e⇩v cd st g = return (e⇩v', cd', sck', mem') g"

| "rexp (Id i) e cd st g =
    (case fmlookup (Denvalue e) i of
      Some (tp, Stackloc l) ⇒
        (case accessStore l (Stack st) of
          Some (KValue v) ⇒ return (KValue v, tp)
        | Some (KCDptr p) ⇒ return (KCDptr p, tp)
        | Some (KMemptr p) ⇒ return (KMemptr p, tp)
        | Some (KStoptr p) ⇒ return (KStoptr p, tp)
        | _ ⇒ throw Err)
    | Some (type.Storage (STValue t), Storeloc l) ⇒ return (KValue (accessStorage t l (Storage st (Address e))), Value t)
    | Some (type.Storage (STArray x t), Storeloc l) ⇒ return (KStoptr l, type.Storage (STArray x t))
    | _ ⇒ throw Err) g"
| "rexp (Ref i r) e cd st g =
    (case fmlookup (Denvalue e) i of
      Some (tp, (Stackloc l)) ⇒
        (case accessStore l (Stack st) of
          Some (KCDptr l') ⇒
            do {
              t ← case tp of Calldata t ⇒ return t | _ ⇒ throw Err;
              (l'', t') ← msel False t l' r e cd st;
              (case t' of
                MTValue t'' ⇒
                  do {
                    v ← case accessStore l'' cd of Some (MValue v) ⇒ return v | _ ⇒ throw Err;
                    return (KValue v, Value t'')
                  }
              | MTArray x t'' ⇒
                  do {
                    p ← case accessStore l'' cd of Some (MPointer p) ⇒ return p | _ ⇒ throw Err;
                    return (KCDptr p, Calldata (MTArray x t''))
                  }
              )
            }
        | 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;
              (case t' of
                MTValue t'' ⇒
                  do {
                    v ← case accessStore l'' (Memory st) of Some (MValue v) ⇒ return v | _ ⇒ throw Err;
                    return (KValue v, Value t'')
                  }
              | MTArray x t'' ⇒
                  do {
                    p ← case accessStore l'' (Memory st) of Some (MPointer p) ⇒ return p | _ ⇒ throw Err;
                    return (KMemptr p, type.Memory (MTArray x 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;
              (case t' of
                STValue t'' ⇒ return (KValue (accessStorage t'' l'' (Storage st (Address e))), Value t'')
              | STArray _ _ ⇒ return (KStoptr l'', type.Storage t')
              | STMap _ _   ⇒ return (KStoptr l'', type.Storage t'))
             }
        | _ ⇒ 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;
            (case t' of
              STValue t'' ⇒ return (KValue (accessStorage t'' l' (Storage st (Address e))), Value t'')
            | STArray _ _ ⇒ return (KStoptr l', type.Storage t')
            | STMap _ _   ⇒ return (KStoptr l', type.Storage t'))
          }
    | None ⇒ throw Err) g"
| "expr CONTRACTS e cd st g =
    (do {
      assert Gas (λg. g > costs⇩e CONTRACTS e cd st);
      modify (λg. g - costs⇩e CONTRACTS e cd st);
      prev ← case Contracts (Accounts st (Address e)) of 0 ⇒ throw Err | Suc n ⇒ return n;
      return (KValue (hash_version (Address e) (ShowL⇩n⇩a⇩t prev)), Value TAddr)
    }) g"
  by pat_completeness auto

subsection ‹Termination›

text ‹To prove termination we first need to show that expressions do not increase gas›

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

lemma msel_ssel_expr_load_rexp_dom_gas[rule_format]:
    "msel_ssel_expr_load_rexp_dom (Inl (Inl (c1, t1, l1, xe1, ev1, cd1, st1, g1)))
      ⟹ (∀v1' g1'. msel c1 t1 l1 xe1 ev1 cd1 st1 g1 = Normal (v1', g1') ⟶ g1' ≤ g1)"
    "msel_ssel_expr_load_rexp_dom (Inl (Inr (t2, l2, xe2, ev2, cd2, st2, g2)))
      ⟹ (∀v2' g2'. ssel t2 l2 xe2 ev2 cd2 st2 g2 = Normal (v2', g2') ⟶ g2' ≤ g2)"
    "msel_ssel_expr_load_rexp_dom (Inr (Inl (e4, ev4, cd4, st4, g4)))
      ⟹ (∀v4' g4'. expr e4 ev4 cd4 st4 g4 = Normal (v4', g4') ⟶ g4' ≤ g4)"
    "msel_ssel_expr_load_rexp_dom (Inr (Inr (Inl (lcp, lis, lxs, lev0, lcd0, lk, lm, lev, lcd, lst, lg))))

      ⟹ (∀ev cd k m g'. load lcp lis lxs lev0 lcd0 lk lm lev lcd lst lg = Normal ((ev, cd, k, m), g') ⟶ g' ≤ lg ∧ Address ev = Address lev0 ∧ Sender ev = Sender lev0 ∧ Svalue ev = Svalue lev0 ∧ Contract ev = Contract lev0)"
    "msel_ssel_expr_load_rexp_dom (Inr (Inr (Inr (l3, ev3, cd3, st3, g3))))
      ⟹ (∀v3' g3'. rexp l3 ev3 cd3 st3 g3 = Normal (v3', g3') ⟶ g3' ≤ g3)"
proof (induct rule: msel_ssel_expr_load_rexp.pinduct
[where ?P1.0="λc1 t1 l1 xe1 ev1 cd1 st1 g1. (∀l1' g1'. msel c1 t1 l1 xe1 ev1 cd1 st1 g1 = Normal (l1', g1') ⟶ g1' ≤ g1)"
   and ?P2.0="λt2 l2 xe2 ev2 cd2 st2 g2. (∀v2' g2'. ssel t2 l2 xe2 ev2 cd2 st2 g2 = Normal (v2', g2') ⟶ g2' ≤ g2)"
   and ?P3.0="λe4 ev4 cd4 st4 g4. (∀v4' g4'. expr e4 ev4 cd4 st4 g4 = Normal (v4', g4') ⟶ g4' ≤ g4)"
   and ?P4.0="λlcp lis lxs lev0 lcd0 lk lm lev lcd lst lg. (∀ev cd k m g'. load lcp lis lxs lev0 lcd0 lk lm lev lcd lst lg = Normal ((ev, cd, k, m), g') ⟶ g' ≤ lg ∧ Address ev = Address lev0 ∧ Sender ev = Sender lev0 ∧ Svalue ev = Svalue lev0 ∧ Contract ev = Contract lev0)"
   and ?P5.0="λl3 ev3 cd3 st3 g3. (∀v3' g3'. rexp l3 ev3 cd3 st3 g3 = Normal (v3', g3') ⟶ g3' ≤ g3)"
])
  case 1
  then show ?case using msel.psimps(1) by auto
next
  case 2
  then show ?case using msel.psimps(2) by auto
next                                                                                                                                                                         
  case 3
  then show ?case using msel.psimps(3) by (auto split: if_split_asm type.split_asm stackvalue.split_asm prod.split_asm StateMonad.result.split_asm types.split_asm)
next
  case (4 mm al t loc x y ys env cd st g)
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix v1' g1' assume a1: "msel mm (MTArray al t) loc (x # y # ys) env cd st g = Normal (v1', g1')"
    show "g1' ≤ g"
    proof (cases v1')
      case (Pair l1' t1')
      then show ?thesis
      proof (cases "expr x env cd st g")
        case (n a g')
        then show ?thesis
        proof (cases a)
          case p2: (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 t')
                case (TSInt x1)
                 with 4 a1 n p2 KValue Value show ?thesis using msel.psimps(4) by simp
              next
                case (TUInt x2)
                then show ?thesis
                proof (cases)
                  assume l: "less t' (TUInt b256) v (ShowL⇩i⇩n⇩t (int al)) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool)"
                  then show ?thesis
                  proof (cases "accessStore (hash loc v) (if mm then Memory st else cd)")
                    case None
                    with 4 a1 n p2 KValue Value l TUInt show ?thesis using msel.psimps(4) by simp
                  next
                    case (Some a)
                    then show ?thesis
                    proof (cases a)
                      case (MValue _)
                      with 4 a1 n p2 KValue Value Some l TUInt show ?thesis using msel.psimps(4) by simp
                    next
                      case (MPointer l)
                      with n p2 KValue Value l Some
                      have "msel mm (MTArray al t) loc (x # y # ys) env cd st g = msel mm t l (y # ys) env cd st g'"
                        using msel.psimps(4) 4(1) TUInt by simp
                      moreover from n have "g' ≤ g" using 4(2) by simp
                      moreover from a1 MPointer n Pair p2 KValue Value l Some
                      have "g1' ≤ g'" using msel.psimps(4) 4(3) 4(1) TUInt by simp
                      ultimately show ?thesis by simp
                    qed
                  qed
                next
                  assume "¬ less t' (TUInt b256) v (ShowL⇩i⇩n⇩t (int al)) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool)"
                  with 4 a1 n p2 KValue Value show ?thesis using msel.psimps(4) TUInt by simp
                qed
              next
                case TBool
                with 4 a1 n p2 KValue Value show ?thesis using msel.psimps(4) by simp              
              next
                case TAddr
                  with 4 a1 n p2 KValue Value show ?thesis using msel.psimps(4) by simp
              qed
            next
              case (Calldata _)
              with 4 a1 n p2 KValue show ?thesis using msel.psimps(4) by simp
            next
              case (Memory _)
              with 4 a1 n p2 KValue show ?thesis using msel.psimps(4) by simp
            next
              case (Storage _)
              with 4 a1 n p2 KValue show ?thesis using msel.psimps(4) by simp
            qed
          next
            case (KCDptr _)
            with 4 a1 n p2 show ?thesis using msel.psimps(4) by simp
          next
            case (KMemptr _)
            with 4 a1 n p2 show ?thesis using msel.psimps(4) by simp
          next
            case (KStoptr _)
            with 4 a1 n p2 show ?thesis using msel.psimps(4) by simp
          qed
        qed
      next
        case (e _)
        with 4 a1 show ?thesis using msel.psimps(4) by simp
      qed
    qed
  qed
next
  case 5
  then show ?case using ssel.psimps(1) by auto
next
  case 6
  then show ?case using ssel.psimps(2) by auto
next
  case (7 al t loc x xs env cd st g)
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix v2' g2' assume a1: "ssel (STArray al t) loc (x # xs) env cd st g = Normal (v2', g2')"
    show "g2' ≤ g"
    proof (cases v2')
      case (Pair l2' t2')
      then show ?thesis
      proof (cases "expr x env cd st g")
        case (n a g'')
        then show ?thesis
        proof (cases a)
          case p2: (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 t')
                case (TSInt x1)
                then show ?thesis using 7 a1 n p2 KValue Value ssel.psimps(3) by simp
              next
                case (TUInt x2)
                then show ?thesis
                  proof (cases)
                    assume l: "less t' (TUInt b256) v (ShowL⇩i⇩n⇩t (int al)) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool)"
                    with n p2 KValue Value l
                    have "ssel (STArray al t) loc (x # xs) env cd st g = ssel t (hash loc v) xs env cd st g''"
                    using ssel.psimps(3) 7(1) TUInt by simp
                    moreover from n have "g'' ≤ g" using 7(2) by simp
                    moreover from a1 n Pair p2 KValue Value l
                    have "g2' ≤ g''" using ssel.psimps(3) 7(3) 7(1) TUInt by simp
                    ultimately show ?thesis by simp
                  next
                    assume "¬ less t' (TUInt b256) v (ShowL⇩i⇩n⇩t (int al)) = Some (ShowL⇩b⇩o⇩o⇩l True, TBool)"
                    with 7 a1 n p2 KValue Value show ?thesis using ssel.psimps(3) TUInt by simp
                  qed
                 
              next
                case TBool
                then show ?thesis using 7 a1 n p2 KValue Value ssel.psimps(3) by simp

              next
                case TAddr
                then show ?thesis using 7 a1 n p2 KValue Value ssel.psimps(3) by simp
              qed
            next
              case (Calldata _)
              with 7 a1 n p2 KValue show ?thesis using ssel.psimps(3) by simp
            next
              case (Memory _)
              with 7 a1 n p2 KValue show ?thesis using ssel.psimps(3) by simp
            next
              case (Storage _)
              with 7 a1 n p2 KValue show ?thesis using ssel.psimps(3) by simp
            qed
          next
            case (KCDptr _)
            with 7 a1 n p2 show ?thesis using ssel.psimps(3) by simp
          next
            case (KMemptr _)
            with 7 a1 n p2 show ?thesis using ssel.psimps(3) by simp
          next
            case (KStoptr x4)
            with 7 a1 n p2 show ?thesis using ssel.psimps(3) by simp
          qed
        qed
      next
        case (e _)
        with 7 a1 show ?thesis using ssel.psimps(3) by simp
      qed
    qed
  qed
next
  case (8 vv t loc x xs env cd st g)
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix v2' g2' assume a1: "ssel (STMap vv t) loc (x # xs) env cd st g = Normal (v2', g2')"
    show "g2' ≤ g"
    proof (cases v2')
      case (Pair l2' t2')
      then show ?thesis
      proof (cases "expr x env cd st g")
        case (n a g')
        then show ?thesis
        proof (cases a)
          case p2: (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)
                assume comp: "comp t'' vv"
                with 8 n p2 KValue comp Value have "ssel (STMap vv t) loc (x # xs) env cd st g = ssel t (hash loc v) xs env cd st g'" using ssel.psimps(4) by simp
                moreover from n have "g' ≤ g" using 8(2) by simp
                moreover from a1 n Pair p2 KValue
                have "g2' ≤ g'" using ssel.psimps(4) 8(3) 8(1) comp Value by simp
                ultimately show ?thesis by simp  
                
              next
                assume comp: "¬comp t'' vv"
                with 8 a1 n p2 KValue comp Value show ?thesis using ssel.psimps(4) by simp
              qed

              next
                case (Calldata x2)
                with 8 a1 n p2 KValue show ?thesis using ssel.psimps(4) by simp
              next
                case (Memory x3)
                with 8 a1 n p2 KValue show ?thesis using ssel.psimps(4) by simp
              next
                case (Storage x4)
                with 8 a1 n p2 KValue show ?thesis using ssel.psimps(4) by simp
              qed
           
          next
            case (KCDptr _)
            with 8 a1 n p2 show ?thesis using ssel.psimps(4) by simp
          next
            case (KMemptr _)
            with 8 a1 n p2 show ?thesis using ssel.psimps(4) by simp
          next
            case (KStoptr _)
            with 8 a1 n p2 show ?thesis using ssel.psimps(4) by simp
          qed
        qed
      next
        case (e _)
        with 8 a1 show ?thesis using ssel.psimps(4) by simp
      qed
    qed
  qed
next
  case 9
  then show ?case using expr.psimps(1) by (simp split:if_split_asm)
next
  case 10
  then show ?case using expr.psimps(2) by (simp split:if_split_asm)
next
  case 11
  then show ?case using expr.psimps(3) by simp
next
  case (12 ad e cd st g)
  define gc where "gc = costs⇩e (BALANCE ad) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4 xa
    assume *: "expr (BALANCE ad) e cd st g = Normal (xa, g4)"
    show "g4 ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 12 gc_def * show ?thesis using expr.psimps(4) by simp
    next
      assume gcost: "¬ g ≤ gc"
      then show ?thesis
      proof (cases "expr ad e cd st (g - gc)")
        case (n a s)
        show ?thesis
        proof (cases a)
          case (Pair b c)
          then show ?thesis
          proof (cases b)
            case (KValue x1)
            then show ?thesis
            proof (cases c)
              case (Value x1)
              then show ?thesis
              proof (cases x1)
                case (TSInt _)
                with 12 gc_def * gcost n Pair KValue Value show ?thesis using expr.psimps(4)[of ad e cd st] by simp
              next
                case (TUInt _)
                with 12 gc_def * gcost n Pair KValue Value show ?thesis using expr.psimps(4)[of ad e cd st] by simp
              next
                case TBool
                with 12 gc_def * gcost n Pair KValue Value show ?thesis using expr.psimps(4)[of ad e cd st] by simp
              next
                case TAddr
                with 12(2)[where ?s'a="g-costs⇩e (BALANCE ad) e cd st"] gc_def * gcost n Pair KValue Value show "g4 ≤ g" using expr.psimps(4)[OF 12(1)] by simp
              qed
            next
              case (Calldata _)
              with 12 gc_def * gcost n Pair KValue show ?thesis using expr.psimps(4)[of ad e cd st] by simp
            next
              case (Memory _)
              with 12 gc_def * gcost n Pair KValue show ?thesis using expr.psimps(4)[of ad e cd st] by simp
            next
              case (Storage _)
              with 12 gc_def * gcost n Pair KValue show ?thesis using expr.psimps(4)[of ad e cd st] by simp
            qed
          next
            case (KCDptr _)
            with 12 gc_def * gcost n Pair show ?thesis using expr.psimps(4)[of ad e cd st] by simp
          next
            case (KMemptr _)
            with 12 gc_def * gcost n Pair show ?thesis using expr.psimps(4)[of ad e cd st] by simp
          next
            case (KStoptr _)
            with 12 gc_def * gcost n Pair show ?thesis using expr.psimps(4)[of ad e cd st] by simp
          qed
        qed
      next
        case (e _)
        with 12 gc_def * gcost show ?thesis using expr.psimps(4)[of ad e cd st] by simp
      qed
    qed
  qed
next
  case 13
  then show ?case using expr.psimps(5) by simp
next
  case 14
  then show ?case using expr.psimps(6) by simp
next
  case 15
  then show ?case using expr.psimps(7) by simp
next
  case 16
  then show ?case using expr.psimps(8) by simp
next
  case 17
  then show ?case using expr.psimps(9) by simp
next
  case (18 x e cd st g)
  define gc where "gc = costs⇩e (NOT x) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix v4 g4' assume a1: "expr (NOT x) e cd st g = Normal (v4, g4')"
    show "g4' ≤ g"
    proof (cases v4)
      case (Pair l4 t4)
      show ?thesis
      proof (cases)
        assume "g ≤ gc"
        with gc_def a1 show ?thesis using expr.psimps(10)[OF 18(1)] by simp
      next
        assume gcost: "¬ g ≤ gc"
        then show ?thesis
        proof (cases "expr x e cd st (g - gc)")
          case (n a g')
          then show ?thesis
          proof (cases a)
            case p2: (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 t)
                  case (TSInt x1)
                  with a1 gc_def gcost n p2 KValue Value show ?thesis using expr.psimps(10)[OF 18(1)] by simp
                next
                  case (TUInt x2)
                  with a1 gc_def gcost n p2 KValue Value show ?thesis using expr.psimps(10)[OF 18(1)] by simp
                next
                  case TBool
                  then show ?thesis
                  proof (cases)
                    assume v_def: "v = ShowL⇩b⇩o⇩o⇩l True"
                    with 18(1) gc_def gcost n p2 KValue Value TBool have "expr (NOT x) e cd st g = expr FALSE e cd st g' " using expr.psimps(10)[OF 18(1)] by simp
                    moreover from 18(2) gc_def gcost n p2 have "g' ≤ g-gc" by simp
                    moreover from 18(3)[OF _ _ n] a1 gc_def gcost have "g4' ≤ g'" using expr.psimps(10)[OF 18(1)] n Pair p2 KValue Value TBool v_def by simp
                    ultimately show ?thesis by arith
                   next
                    assume v_def: "¬ v = ShowL⇩b⇩o⇩o⇩l True"
                    then show ?thesis
                    proof (cases)
                      assume v_def2: "v = ShowL⇩b⇩o⇩o⇩l False"
                      with 18(1) gc_def gcost n p2 KValue Value v_def TBool have "expr (NOT x) e cd st g = expr TRUE e cd st g'" using expr.psimps(10) by simp
                      moreover from 18(2)[where ?s'a="g-costs⇩e (NOT x) e cd st"] gc_def gcost n p2 have "g' ≤ g" by simp
                      moreover from 18(4)[OF _ _ n] a1 gc_def gcost have "g4' ≤ g'" using expr.psimps(10)[OF 18(1)] n Pair p2 KValue Value TBool v_def v_def2 by simp
                      ultimately show ?thesis by arith
                    next
                      assume "¬ v = ShowL⇩b⇩o⇩o⇩l False"
                      with 18(1) a1 gc_def gcost n p2 KValue Value v_def TBool show ?thesis using expr.psimps(10) by simp
                    qed
                  qed
                next
                  case TAddr
                  with 18(1) a1 gc_def gcost n p2 KValue Value show ?thesis using expr.psimps(10) by simp
                qed
              next
                case (Calldata _)
                with 18(1) a1 gc_def gcost n p2 KValue show ?thesis using expr.psimps(10) by simp
              next
                case (Memory _)
                with 18(1) a1 gc_def gcost n p2 KValue show ?thesis using expr.psimps(10) by simp
              next
                case (Storage _)
                with 18(1) a1 gc_def gcost n p2 KValue show ?thesis using expr.psimps(10) by simp
              qed
            next
              case (KCDptr _)
              with 18(1) a1 gc_def gcost n p2 show ?thesis using expr.psimps(10) by simp
            next
              case (KMemptr _)
              with 18(1) a1 gc_def gcost n p2 show ?thesis using expr.psimps(10) by simp
            next
              case (KStoptr _)
              with 18(1) a1 gc_def gcost n p2 show ?thesis using expr.psimps(10) by simp
            qed
          qed
        next
          case (e _)
          with 18(1) a1 gc_def gcost show ?thesis using expr.psimps(10) by simp
        qed
      qed
    qed
  qed
next
  case (19 e1 e2 e cd st g)
  define gc where "gc = costs⇩e (PLUS e1 e2) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4 xa assume e_def: "expr (PLUS e1 e2) e cd st g = Normal (xa, g4)"
    then show "g4 ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 19(1) e_def show ?thesis using expr.psimps(11) gc_def by simp
    next
      assume "¬ g ≤ gc"
      then have *: "assert Gas ((<) (costs⇩e (PLUS e1 e2) e cd st)) g = Normal ((), g)" using gc_def by simp
      with 19(1) e_def gc_def have lift:"lift expr add e1 e2 e cd st (g - gc) = Normal (xa, g4)" using expr.psimps(11)[OF 19(1)] by simp
      moreover have **: "modify (λg. g - costs⇩e (PLUS e1 e2) e cd st) g = Normal ((), g - costs⇩e (PLUS e1 e2) e cd st)" by simp
      with 19(2)[OF * **] have "⋀g4' v4 t4. expr e1 e cd st (g-gc) = Normal ((v4, t4), g4') ⟹ g4' ≤ g - gc" unfolding gc_def by simp
      moreover obtain v g' where ***: "expr e1 e cd st (g - costs⇩e (PLUS e1 e2) e cd st) = Normal (v, g')" using expr.psimps(11)[OF 19(1)] e_def by (simp split:if_split_asm result.split_asm prod.split_asm)
      with 19(3)[OF * ** ***] have "⋀v t g' v' t' g''. expr e1 e cd st (g-gc) = Normal ((KValue v, Value t), g') ⟹ expr e2 e cd st g' = Normal ((v', t'), g'') ⟹ g'' ≤ g'" unfolding gc_def by simp
      ultimately show "g4 ≤ g" using lift_gas[OF lift] `¬ g ≤ gc` by (simp split:result.split_asm stackvalue.split_asm type.split_asm prod.split_asm)
    qed
  qed
next
  case (20 e1 e2 e cd st g)
  define gc where "gc = costs⇩e (MINUS e1 e2) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4 xa assume e_def: "expr (MINUS e1 e2) e cd st g = Normal (xa, g4)"
    then show "g4 ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 20(1) e_def show ?thesis using expr.psimps(12) gc_def by simp
    next
      assume "¬ g ≤ gc"
      then have *: "assert Gas ((<) (costs⇩e (MINUS e1 e2) e cd st)) g = Normal ((), g)" using gc_def by simp
      with 20(1) e_def gc_def have lift:"lift expr sub e1 e2 e cd st (g - gc) = Normal (xa, g4)" using expr.psimps(12)[OF 20(1)] by simp
      moreover have **: "modify (λg. g - costs⇩e (MINUS e1 e2) e cd st) g = Normal ((), g - costs⇩e (MINUS e1 e2) e cd st)" by simp
      with 20(2)[OF * **] have "⋀g4' v4 t4. expr e1 e cd st (g-gc) = Normal ((v4, t4), g4') ⟹ g4' ≤ g - gc" unfolding gc_def by simp
      moreover obtain v g' where ***: "expr e1 e cd st (g - costs⇩e (MINUS e1 e2) e cd st) = Normal (v, g')" using expr.psimps(12)[OF 20(1)] e_def by (simp split:if_split_asm result.split_asm prod.split_asm)
      with 20(3)[OF * ** ***] have "⋀v t g' v' t' g''. expr e1 e cd st (g-gc) = Normal ((KValue v, Value t), g') ⟹ expr e2 e cd st g' = Normal ((v', t'), g'') ⟹ g'' ≤ g'" unfolding gc_def by simp
      ultimately show "g4 ≤ g" using lift_gas[OF lift] `¬ g ≤ gc` by (simp split:result.split_asm stackvalue.split_asm type.split_asm prod.split_asm)
    qed
  qed
next
  case (21 e1 e2 e cd st g)
  define gc where "gc = costs⇩e (LESS e1 e2) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4 xa assume e_def: "expr (LESS e1 e2) e cd st g = Normal (xa, g4)"
    then show "g4 ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 21(1) e_def show ?thesis using expr.psimps(13) gc_def by simp
    next
      assume "¬ g ≤ gc"
      then have *: "assert Gas ((<) (costs⇩e (LESS e1 e2) e cd st)) g = Normal ((), g)" using gc_def by simp
      with 21(1) e_def gc_def have lift:"lift expr less e1 e2 e cd st (g - gc) = Normal (xa, g4)" using expr.psimps(13)[OF 21(1)] by simp
      moreover have **: "modify (λg. g - costs⇩e (LESS e1 e2) e cd st) g = Normal ((), g - costs⇩e (LESS e1 e2) e cd st)" by simp
      with 21(2)[OF * **] have "⋀g4' v4 t4. expr e1 e cd st (g-gc) = Normal ((v4, t4), g4') ⟹ g4' ≤ g - gc" unfolding gc_def by simp
      moreover obtain v g' where ***: "expr e1 e cd st (g - costs⇩e (LESS e1 e2) e cd st) = Normal (v, g')" using expr.psimps(13)[OF 21(1)] e_def by (simp split:if_split_asm result.split_asm prod.split_asm)
      with 21(3)[OF * ** ***] have "⋀v t g' v' t' g''. expr e1 e cd st (g-gc) = Normal ((KValue v, Value t), g') ⟹ expr e2 e cd st g' = Normal ((v', t'), g'') ⟹ g'' ≤ g'" unfolding gc_def by simp
      ultimately show "g4 ≤ g" using lift_gas[OF lift] `¬ g ≤ gc` by (simp split:result.split_asm stackvalue.split_asm type.split_asm prod.split_asm)
    qed
  qed
next
  case (22 e1 e2 e cd st g)
  define gc where "gc = costs⇩e (EQUAL e1 e2) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4 xa assume e_def: "expr (EQUAL e1 e2) e cd st g = Normal (xa, g4)"
    then show "g4 ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 22(1) e_def show ?thesis using expr.psimps(14) gc_def by simp
    next
      assume "¬ g ≤ gc"
      then have *: "assert Gas ((<) (costs⇩e (EQUAL e1 e2) e cd st)) g = Normal ((), g)" using gc_def by simp
      with 22(1) e_def gc_def have lift:"lift expr equal e1 e2 e cd st (g - gc) = Normal (xa, g4)" using expr.psimps(14)[OF 22(1)] by simp
      moreover have **: "modify (λg. g - costs⇩e (EQUAL e1 e2) e cd st) g = Normal ((), g - costs⇩e (EQUAL e1 e2) e cd st)" by simp
      with 22(2)[OF * **] have "⋀g4' v4 t4. expr e1 e cd st (g-gc) = Normal ((v4, t4), g4') ⟹ g4' ≤ g - gc" unfolding gc_def by simp
      moreover obtain v g' where ***: "expr e1 e cd st (g - costs⇩e (EQUAL e1 e2) e cd st) = Normal (v, g')" using expr.psimps(14)[OF 22(1)] e_def by (simp split:if_split_asm result.split_asm prod.split_asm)
      with 22(3)[OF * ** ***] have "⋀v t g' v' t' g''. expr e1 e cd st (g-gc) = Normal ((KValue v, Value t), g') ⟹ expr e2 e cd st g' = Normal ((v', t'), g'') ⟹ g'' ≤ g'" unfolding gc_def by simp
      ultimately show "g4 ≤ g" using lift_gas[OF lift] `¬ g ≤ gc` by (simp split:result.split_asm stackvalue.split_asm type.split_asm prod.split_asm)
    qed
  qed
next
  case (23 e1 e2 e cd st g)
  define gc where "gc = costs⇩e (AND e1 e2) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4 xa assume e_def: "expr (AND e1 e2) e cd st g = Normal (xa, g4)"
    then show "g4 ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 23(1) e_def show ?thesis using expr.psimps(15) gc_def by simp
    next
      assume "¬ g ≤ gc"
      then have *: "assert Gas ((<) (costs⇩e (AND e1 e2) e cd st)) g = Normal ((), g)" using gc_def by simp
      with 23(1) e_def gc_def have lift:"lift expr vtand e1 e2 e cd st (g - gc) = Normal (xa, g4)" using expr.psimps(15)[OF 23(1)] by simp
      moreover have **: "modify (λg. g - costs⇩e (AND e1 e2) e cd st) g = Normal ((), g - costs⇩e (AND e1 e2) e cd st)" by simp
      with 23(2)[OF * **] have "⋀g4' v4 t4. expr e1 e cd st (g-gc) = Normal ((v4, t4), g4') ⟹ g4' ≤ g - gc" unfolding gc_def by simp
      moreover obtain v g' where ***: "expr e1 e cd st (g - costs⇩e (AND e1 e2) e cd st) = Normal (v, g')" using expr.psimps(15)[OF 23(1)] e_def by (simp split:if_split_asm result.split_asm prod.split_asm)
      with 23(3)[OF * ** ***] have "⋀v t g' v' t' g''. expr e1 e cd st (g-gc) = Normal ((KValue v, Value t), g') ⟹ expr e2 e cd st g' = Normal ((v', t'), g'') ⟹ g'' ≤ g'" unfolding gc_def by simp
      ultimately show "g4 ≤ g" using lift_gas[OF lift] `¬ g ≤ gc` by (simp split:result.split_asm stackvalue.split_asm type.split_asm prod.split_asm)
    qed
  qed
next
  case (24 e1 e2 e cd st g)
  define gc where "gc = costs⇩e (OR e1 e2) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4 xa assume e_def: "expr (OR e1 e2) e cd st g = Normal (xa, g4)"
    then show "g4 ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 24(1) e_def show ?thesis using expr.psimps(16) gc_def by simp
    next
      assume "¬ g ≤ gc"
      then have *: "assert Gas ((<) (costs⇩e (OR e1 e2) e cd st)) g = Normal ((), g)" using gc_def by simp
      with 24(1) e_def gc_def have lift:"lift expr vtor e1 e2 e cd st (g - gc) = Normal (xa, g4)" using expr.psimps(16)[OF 24(1)] by simp
      moreover have **: "modify (λg. g - costs⇩e (OR e1 e2) e cd st) g = Normal ((), g - costs⇩e (OR e1 e2) e cd st)" by simp
      with 24(2)[OF * **] have "⋀g4' v4 t4. expr e1 e cd st (g-gc) = Normal ((v4, t4), g4') ⟹ g4' ≤ g - gc" unfolding gc_def by simp
      moreover obtain v g' where ***: "expr e1 e cd st (g - costs⇩e (OR e1 e2) e cd st) = Normal (v, g')" using expr.psimps(16)[OF 24(1)] e_def by (simp split:if_split_asm result.split_asm prod.split_asm)
      with 24(3)[OF * ** ***] have "⋀v t g' v' t' g''. expr e1 e cd st (g-gc) = Normal ((KValue v, Value t), g') ⟹ expr e2 e cd st g' = Normal ((v', t'), g'') ⟹ g'' ≤ g'" unfolding gc_def by simp
      ultimately show "g4 ≤ g" using lift_gas[OF lift] `¬ g ≤ gc` by (simp split:result.split_asm stackvalue.split_asm type.split_asm prod.split_asm)
    qed
  qed
next
  case (25 i e cd st g)
  define gc where "gc = costs⇩e (LVAL i) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4 xa xaa assume e_def: "expr (LVAL i) e cd st g = Normal (xa, g4)"
    then show "g4 ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 25(1) e_def show ?thesis using expr.psimps(17) gc_def by simp
    next
      assume "¬ g ≤ gc"
      then have *: "assert Gas ((<) (costs⇩e (LVAL i) e cd st)) g = Normal ((), g)" using gc_def by simp
      then have "expr (LVAL i) e cd st g = rexp i e cd st (g - gc)" using expr.psimps(17)[OF 25(1)] gc_def by simp
      then have "rexp i e cd st (g - gc) = Normal (xa, g4)" using e_def by simp
      moreover have **: "modify (λg. g - costs⇩e (LVAL i) e cd st) g = Normal ((), g - costs⇩e (LVAL i) e cd st)" by simp
      ultimately show ?thesis using 25(2)[OF * **] unfolding gc_def by (simp split:result.split_asm stackvalue.split_asm type.split_asm prod.split_asm)
    qed
  qed
next
  case (26 i xe e cd st g)
  define gc where "gc = costs⇩e (CALL i xe) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4' v4 assume a1: "expr (CALL i xe) e cd st g = Normal (v4, g4')"
    then have *: "assert Gas ((<) (costs⇩e (CALL i xe) e cd st)) g = Normal ((), g)" using gc_def using expr.psimps(18)[OF 26(1)] by (simp split:if_split_asm)
    have **: "modify (λg. g - costs⇩e (CALL i xe) e cd st) g = Normal ((), g - gc)" unfolding gc_def by simp
    show "g4' ≤ g"
    proof (cases)
      assume "g ≤ gc"
      with 26(1) gc_def a1 show ?thesis using expr.psimps(18) by simp
    next
      assume gcost: "¬ g ≤ gc"
      then show ?thesis
      proof (cases v4)
        case (Pair l4 t4)
        then show ?thesis
        proof (cases "ep $$ Contract e")
          case None
          with 26(1) a1 gc_def gcost show ?thesis using expr.psimps(18) by simp
        next
          case (Some a)
          then show ?thesis
          proof (cases a)
            case p2: (fields ct x0 x1)
            then have 1: "option Err (λ_. ep $$ Contract e) (g - gc) = Normal ((ct, x0, x1), (g - gc))" using Some by simp
            then show ?thesis
            proof (cases "fmlookup ct i")
              case None
              with 26(1) a1 gc_def gcost Some p2 show ?thesis using expr.psimps(18) by simp
            next
              case s1: (Some a)
              then show ?thesis
              proof (cases a)
                case (Function x1)
                then show ?thesis
                proof (cases x1)
                  case p1: (fields fp ext x)
                  then show ?thesis
                  proof (cases ext)
                    case True
                    with 26(1) a1 gc_def gcost Some p2 s1 Function p1 show ?thesis using expr.psimps(18)[of i xe e cd st] by (auto split:unit.split_asm)
                  next
                    case False
                    then have 2: "(case ct $$ i of None ⇒ throw Err | Some (Function (fp, True, xa)) ⇒ throw Err | Some (Function (fp, False, xa)) ⇒ return (fp, xa) | Some _ ⇒ throw Err) (g - gc) = Normal ((fp, x), (g - gc))" using s1 Function p1 by simp
                    define e' where "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 (Memory st) e cd st (g - gc)")
                      case s4: (n a g')
                      then show ?thesis
                      proof (cases a)
                        case f2: (fields e⇩l cd⇩l k⇩l m⇩l)
                        then show ?thesis
                        proof (cases "expr x e⇩l cd⇩l (st⦇Stack:=k⇩l, Memory:=m⇩l⦈) g'")
                          case n2: (n a g'')
                          then show ?thesis
                          proof (cases a)
                            case p3: (Pair sv tp)
                            with 26(1) a1 gc_def gcost Some p2 s1 Function p1 e'_def s4 f2 n2 False
                            have "expr (CALL i xe) e cd st g = Normal ((sv, tp), g'')"
                              using expr.psimps(18)[OF 26(1)] by (simp split:stackvalue.split_asm option.split_asm if_split_asm)
                            with a1 have "g4' ≤ g''" by simp
                            also from 26(3)[OF * ** 1 _ 2 _ _ s4] e'_def f2 n2 p3 gcost gc_def
                              have "… ≤ g'" by auto
                            also from 26(2)[OF * ** 1 _ 2 _] False e'_def f2 s4
                              have "… ≤ g - gc" unfolding ffold_init_def gc_def by blast
                            finally show ?thesis by simp
                          qed
                        next
                          case (e _)
                          with 26(1) a1 gc_def gcost Some p2 s1 Function p1 e'_def s4 f2 False show ?thesis using expr.psimps(18)[of i xe e cd st] by (auto simp add:Let_def split:unit.split_asm)
                        qed
                      qed
                    next
                      case (e _)
                      with 26(1) a1 gc_def gcost Some p2 s1 Function p1 e'_def False show ?thesis using expr.psimps(18)[of i xe e cd st] by (auto split:unit.split_asm)
                    qed
                  qed
                qed
              next
                case (Method _)
                with 26(1) a1 gc_def gcost Some p2 s1 show ?thesis using expr.psimps(18) by simp
              next
                case (Var _)
                with 26(1) a1 gc_def gcost Some p2 s1 show ?thesis using expr.psimps(18) by simp
              qed
            qed
          qed
        qed
      qed
    qed
  qed
next
  case (27 ad i xe e cd st g)
  define gc where "gc = costs⇩e (ECALL ad i xe) e cd st"
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix g4' v4 assume a1: "expr (ECALL ad i xe) e cd st g = Normal (v4, g4')"
    show "g4' ≤ g"
    proof (cases v4)
      case (Pair l4 t4)
      then show ?thesis
      proof (cases)
        assume "g ≤ gc"
        with gc_def a1 show ?thesis using expr.psimps(19)[OF 27(1)] by simp
      next
        assume gcost: "¬ g ≤ gc"
        then have *: "assert Gas ((<) (costs⇩e (ECALL ad i xe) e cd st)) g = Normal ((), g)" using gc_def using expr.psimps(19)[OF 27(1)] by (simp split:if_split_asm)
        have **: "modify (λg. g - costs⇩e (ECALL ad i xe) e cd st) g = Normal ((), g - gc)" unfolding gc_def by simp
        then show ?thesis
        proof (cases "expr ad e cd st (g-gc)")
          case (n a0 g')
          then show ?thesis
          proof (cases a0)
            case p0: (Pair a b)
            then show ?thesis
            proof (cases a)
              case (KValue adv)
              then show ?thesis
              proof (cases b)
                case (Value x1)
                then show ?thesis
                proof (cases x1)
                  case (TSInt x1)
                  with a1 gc_def gcost n p0 KValue Value show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                next
                  case (TUInt x2)
                  with a1 gc_def gcost n p0 KValue Value show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                next
                  case TBool
                  with a1 gc_def gcost n p0 KValue Value show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                next
                  case TAddr
                  then have 1: "(case a0 of (KValue adv, Value TAddr) ⇒ return adv | (KValue adv, Value _) ⇒ throw Err | (KValue adv, _) ⇒ throw Err | (_, b) ⇒ throw Err) g' = Normal (adv, g')" using p0 KValue Value by simp
                  then show ?thesis
                  proof (cases "adv = Address e")
                    case True
                    with a1 gc_def gcost n p0 KValue Value TAddr show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                  next
                    case False
                    then have 2: "assert Err (λ_. adv ≠ Address e) g' = Normal ((), g')" by simp
                    then show ?thesis
                    proof (cases "Type (Accounts st adv)")
                      case None
                      with a1 gc_def gcost n p0 KValue Value TAddr False show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                    next
                      case (Some x2)
                      then show ?thesis
                      proof (cases x2)
                        case EOA
                        with a1 gc_def gcost n p0 KValue Value TAddr False Some show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                      next
                        case c: (Contract c)
                        then have 3: "(case Type (Accounts st adv) of Some (atype.Contract c) ⇒ return c | _ ⇒ throw Err) g' = Normal (c, g')" using Some by simp
                        then show ?thesis
                        proof (cases "ep $$ c")
                          case None
                          with a1 gc_def gcost n p0 KValue Value TAddr False Some c show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                        next
                          case s0: (Some a)
                          then show ?thesis
                          proof (cases a)
                            case p1: (fields ct xa xb)
                            then have 4: "option Err (λ_. ep $$ c) g' = Normal ((ct, xa, xb), g')" using Some s0 by simp
                            then show ?thesis
                            proof (cases "ct $$ i")
                              case None
                              with a1 gc_def gcost n p0 KValue Value TAddr Some p1 False c s0 show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                            next
                              case s1: (Some a)
                              then show ?thesis
                              proof (cases a)
                                case (Function x1)
                                then show ?thesis
                                proof (cases x1)
                                  case p2: (fields fp ext x)
                                  then show ?thesis
                                  proof (cases ext)
                                    case True
                                    then have 5: "(case ct $$ i of None ⇒ throw Err | Some (Function (fp, True, xa)) ⇒ return (fp, xa) | Some (Function (fp, False, xa)) ⇒ throw Err | Some _ ⇒ throw Err) g' = Normal ((fp, x), g')" using s1 Function p2 by simp
                                    define e' where "e' = ffold (init ct) (emptyEnv adv c (Address e) (ShowL⇩n⇩a⇩t 0)) (fmdom ct)"
                                    then show ?thesis
                                    proof (cases "load True fp xe e' emptyTypedStore emptyStore emptyTypedStore e cd st g'")
                                      case n1: (n a g'')
                                      then show ?thesis
                                      proof (cases a)
                                        case f2: (fields e⇩l cd⇩l k⇩l m⇩l)
                                        show ?thesis
                                        proof (cases "expr x e⇩l cd⇩l (st⦇Stack:=k⇩l, Memory:=m⇩l⦈) g''")
                                          case n2: (n a g''')
                                          then show ?thesis
                                          proof (cases a)
                                            case p3: (Pair sv tp)
                                            with a1 gc_def gcost n p2 KValue Value TAddr Some p1 s1 Function p0 e'_def n1 f2 n2 True False s0 c
                                            have "expr (ECALL ad i xe) e cd st g = Normal ((sv, tp), g''')"
                                                using expr.psimps(19)[OF 27(1)] by (auto split: stackvalue.splits)
                                            with a1 have "g4' ≤ g'''" by auto
                                            also from 27(4)[OF * ** n 1 2 3 4 _ 5 _ _ n1] p3 f2 e'_def n2
                                              have "… ≤ g''" by simp
                                            also from 27(3)[OF * ** n 1 2 3 4 _ 5, of "(xa, xb)" fp x e'] e'_def n1 f2
                                              have "… ≤ g'" by auto
                                            also from 27(2)[OF * **] n
                                              have "… ≤ g" by simp
                                            finally show ?thesis by simp
                                          qed
                                        next
                                          case (e _)
                                          with a1 gc_def gcost n p0 KValue Value TAddr False Some p1 s1 Function p2 e'_def n1 f2 True s0 c show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                                        qed
                                      qed
                                    next
                                      case (e _)
                                      with a1 gc_def gcost n p0 KValue Value TAddr False Some p1 s1 Function p2 e'_def True s0 c show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                                    qed
                                  next
                                    case f: False
                                    with a1 gc_def gcost n p0 KValue Value TAddr Some p1 s1 Function p2 False s0 c show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                                  qed
                                qed
                              next
                                case (Method _)
                                with a1 gc_def gcost n p0 KValue Value TAddr Some p1 s1 False s0 c show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                              next
                                case (Var _)
                                with a1 gc_def gcost n p0 KValue Value TAddr Some p1 s1 False s0 c show ?thesis using expr.psimps(19)[OF 27(1)] by simp
                              qed
                            qed
                          qed
                        qed
                      qed
                    qed
                  qed
                qed
              next
                case (Calldata _)
                with a1 gc_def gcost n p0 KValue show ?thesis using expr.psimps(19)[OF 27(1)] by simp
              next
                case (Memory _)
                with a1 gc_def gcost n p0 KValue show ?thesis using expr.psimps(19)[OF 27(1)] by simp
              next
                case (Storage _)
                with a1 gc_def gcost n p0 KValue show ?thesis using expr.psimps(19)[OF 27(1)] by simp
              qed
            next
              case (KCDptr _)
              with a1 gc_def gcost n p0 show ?thesis using expr.psimps(19)[OF 27(1)] by simp
            next
              case (KMemptr _)
              with a1 gc_def gcost n p0 show ?thesis using expr.psimps(19)[OF 27(1)] by simp
            next
              case (KStoptr _)
              with a1 gc_def gcost n p0 show ?thesis using expr.psimps(19)[OF 27(1)] by simp
            qed
          qed
        next
          case (e _)
          with a1 gc_def gcost show ?thesis using expr.psimps(19)[OF 27(1)] by simp
        qed
      qed
    qed
  qed
next
  case (28 cp i⇩p t⇩p pl e el e⇩v' cd' sck' mem' e⇩v cd st g)
  then show ?case
  proof(cases "t⇩p")
    case (Value x1)
    then show ?thesis
    proof (cases "expr e e⇩v cd st g")
        case (n a g'')
        then show ?thesis
        proof (cases a)
          case (Pair v t)
          then show ?thesis
          proof (cases "decl i⇩p t⇩p (Some (v,t)) cp cd (Memory st) (Storage st (Address e⇩v)) (cd', mem',  sck', e⇩v')")
            case None
            with 28(1) n Pair Value show ?thesis using load.psimps(1) by (simp split:option.splits)
          next
            case (Some a)
            show ?thesis
            proof (cases a)
              case (fields cd'' m'' k'' e⇩v'')
              then have 1: "(case decl i⇩p t⇩p (Some (v, t)) cp cd (Memory st) (Storage st (Address e⇩v)) (cd', mem', sck', e⇩v') of None ⇒ throw Err | Some (c, m, k, e) ⇒ return (c, m, k, e)) g'' = Normal ((cd'',m'',k'',e⇩v''), g'')" using Some by simp
              show ?thesis
              proof ((rule allI)+,(rule impI))
                fix ev cda k m g' assume load_def: "load cp ((i⇩p, t⇩p) # pl) (e # el) e⇩v' cd' sck' mem' e⇩v cd st g = Normal ((ev, cda, k, m), g')"
                then have none:"Denvalue e⇩v' $$ i⇩p = None" using load.pelims[OF load_def 28(1)] Value by fastforce
                with n Pair Some fields have "load cp ((i⇩p, t⇩p) # pl) (e # el) e⇩v' cd' sck' mem' e⇩v cd st g = load cp pl el e⇩v'' cd'' k'' m'' e⇩v cd st g''" using load.psimps(1)[OF 28(1)] Value by (simp split:option.splits)
                with load_def have "load cp pl el e⇩v'' cd'' k'' m'' e⇩v cd st g'' = Normal ((ev, cda, k, m), g')" by simp
                with Pair fields have "g' ≤ g'' ∧ Address ev = Address e⇩v'' ∧ Sender ev = Sender e⇩v'' ∧ Svalue ev = Svalue e⇩v''  ∧ Contract ev = Contract e⇩v''"  using 28(3) n Pair 1 Value none 
                  by fastforce
                moreover from n have "g'' ≤ g" using 28(2) Value none by simp
                moreover from Some fields have "Address e⇩v'' =  Address e⇩v' ∧ Sender e⇩v'' = Sender e⇩v' ∧ Svalue e⇩v'' = Svalue e⇩v'  ∧ Contract e⇩v'' = Contract e⇩v'" using decl_env by auto
                ultimately show "g' ≤ g ∧ Address ev = Address e⇩v' ∧ Sender ev = Sender e⇩v' ∧ Svalue ev = Svalue e⇩v'  ∧ Contract ev = Contract e⇩v'" by auto
              qed
            qed

          qed
        qed
      next
        case (e _)
        with 28(1) show ?thesis using load.psimps(1) Value by (simp split:option.splits)
      qed
  next
    case (Calldata x2)
    then show ?thesis
    proof (cases "expr e e⇩v cd st g")
        case (n a g'')
        then show ?thesis
        proof (cases a)
          case (Pair v t)
          then show ?thesis
          proof (cases "decl i⇩p t⇩p (Some (v,t)) cp cd (Memory st) (Storage st (Address e⇩v)) (cd', mem',  sck', e⇩v')")
            case None
            with 28(1) n Pair Calldata show ?thesis using load.psimps(1)by (simp split:option.splits)
          next
            case (Some a)
            show ?thesis
            proof (cases a)
              case (fields cd'' m'' k'' e⇩v'')
              then have 1: "(case decl i⇩p t⇩p (Some (v, t)) cp cd (Memory st) (Storage st (Address e⇩v)) (cd', mem', sck', e⇩v') of None ⇒ throw Err | Some (c, m, k, e) ⇒ return (c, m, k, e)) g'' = Normal ((cd'',m'',k'',e⇩v''), g'')" using Some by simp
              show ?thesis
              proof ((rule allI)+,(rule impI))
                fix ev cda k m g' assume load_def: "load cp ((i⇩p, t⇩p) # pl) (e # el) e⇩v' cd' sck' mem' e⇩v cd st g = Normal ((ev, cda, k, m), g')"
                then have none:"Denvalue e⇩v' $$ i⇩p = None" using load.pelims[OF load_def 28(1)] Calldata by fastforce

                with n Pair Some fields have "load cp ((i⇩p, t⇩p) # pl) (e # el) e⇩v' cd' sck' mem' e⇩v cd st g = load cp pl el e⇩v'' cd'' k'' m'' e⇩v cd st g''" using load.psimps(1)[OF 28(1)] Calldata by (simp split:option.splits)
                with load_def have "load cp pl el e⇩v'' cd'' k'' m'' e⇩v cd st g'' = Normal ((ev, cda, k, m), g')" by simp
                with Pair fields have "g' ≤ g'' ∧ Address ev = Address e⇩v'' ∧ Sender ev = Sender e⇩v'' ∧ Svalue ev = Svalue e⇩v'' ∧ Contract ev = Contract e⇩v'' " using none 28(3) n Pair 1 Calldata 
                  by fastforce
                moreover from n have "g'' ≤ g" using 28(2) Calldata none by (simp add: "28.hyps"(2))
                moreover from Some fields have "Address e⇩v'' =  Address e⇩v' ∧ Sender e⇩v'' = Sender e⇩v' ∧ Svalue e⇩v'' = Svalue e⇩v' ∧ Contract e⇩v'' = Contract e⇩v'" using decl_env by auto
                ultimately show "g' ≤ g ∧ Address ev = Address e⇩v' ∧ Sender ev = Sender e⇩v' ∧ Svalue ev = Svalue e⇩v' ∧ Contract ev = Contract e⇩v' " by auto
              qed
            qed
          qed
        qed
      next
        case (e _)
        with 28(1) show ?thesis using load.psimps(1) Calldata by (simp split:option.splits)
      qed
  next
    case (Memory x3)
    then show ?thesis
    proof (cases "expr e e⇩v cd st g")
        case (n a g'')
        then show ?thesis
        proof (cases a)
          case (Pair v t)
          then show ?thesis
          proof (cases "decl i⇩p t⇩p (Some (v,t)) cp cd (Memory st) (Storage st (Address e⇩v)) (cd', mem',  sck', e⇩v')")
            case None
            with 28(1) n Pair Memory show ?thesis using load.psimps(1)by (simp split:option.splits)
          next
            case (Some a)
            show ?thesis
            proof (cases a)
              case (fields cd'' m'' k'' e⇩v'')
              then have 1: "(case decl i⇩p t⇩p (Some (v, t)) cp cd (Memory st) (Storage st (Address e⇩v)) (cd', mem', sck', e⇩v') of None ⇒ throw Err | Some (c, m, k, e) ⇒ return (c, m, k, e)) g'' = Normal ((cd'',m'',k'',e⇩v''), g'')" using Some by simp
              show ?thesis
              proof ((rule allI)+,(rule impI))
                fix ev cda k m g' assume load_def: "load cp ((i⇩p, t⇩p) # pl) (e # el) e⇩v' cd' sck' mem' e⇩v cd st g = Normal ((ev, cda, k, m), g')"
                then have none:"Denvalue e⇩v' $$ i⇩p = None" using load.pelims[OF load_def 28(1)] Memory by fastforce

                with n Pair Some fields have "load cp ((i⇩p, t⇩p) # pl) (e # el) e⇩v' cd' sck' mem' e⇩v cd st g = load cp pl el e⇩v'' cd'' k'' m'' e⇩v cd st g''" using load.psimps(1)[OF 28(1)] Memory by (simp split:option.splits)
                with load_def have "load cp pl el e⇩v'' cd'' k'' m'' e⇩v cd st g'' = Normal ((ev, cda, k, m), g')" by simp
                with Pair fields have "g' ≤ g'' ∧ Address ev = Address e⇩v'' ∧ Sender ev = Sender e⇩v'' ∧ Svalue ev = Svalue e⇩v'' ∧ Contract ev = Contract  e⇩v''" using 28(3) n Pair 1 Memory none by fastforce
                moreover from n have "g'' ≤ g" using 28(2) Memory none by (simp add: "28.hyps"(2))
                moreover from Some fields have "Address e⇩v'' =  Address e⇩v' ∧ Sender e⇩v'' = Sender e⇩v' ∧ Svalue e⇩v'' = Svalue e⇩v'∧ Contract e⇩v'' = Contract e⇩v'" using decl_env by auto
                ultimately show "g' ≤ g ∧ Address ev = Address e⇩v' ∧ Sender ev = Sender e⇩v' ∧ Svalue ev = Svalue e⇩v'∧ Contract ev = Contract e⇩v'" by auto
              qed
            qed
          qed
        qed
      next
        case (e _)
        with 28(1) show ?thesis using load.psimps(1) Memory by (simp split:option.splits)
      qed
  next
    case (Storage x4)
    then show ?thesis
    proof(cases cp)
      case True
      then show ?thesis using 28 load.psimps Storage by simp
    next
      case notCP:False
      then show ?thesis
      proof (cases "expr e e⇩v cd st g")
        case (n a g'')
        then show ?thesis
        proof (cases a)
          case (Pair v t)
          then show ?thesis
          proof (cases "decl i⇩p t⇩p (Some (v,t)) cp cd (Memory st) (Storage st (Address e⇩v)) (cd', mem',  sck', e⇩v')")
            case None
            with 28(1) n Pair Storage notCP show ?thesis using load.psimps(1) by (simp split:option.splits)
          next
            case (Some a)
            show ?thesis
            proof (cases a)
              case (fields cd'' m'' k'' e⇩v'')
              then have 1: "(case decl i⇩p t⇩p (Some (v, t)) cp cd (Memory st) (Storage st (Address e⇩v)) (cd', mem', sck', e⇩v') of None ⇒ throw Err | Some (c, m, k, e) ⇒ return (c, m, k, e)) g'' = Normal ((cd'',m'',k'',e⇩v''), g'')" using Some by simp
              show ?thesis
              proof ((rule allI)+,(rule impI))
                fix ev cda k m g' assume load_def: "load cp ((i⇩p, t⇩p) # pl) (e # el) e⇩v' cd' sck' mem' e⇩v cd st g = Normal ((ev, cda, k, m), g')"
                then have none:"Denvalue e⇩v' $$ i⇩p = None" using load.pelims[OF load_def 28(1)] Storage notCP by fastforce

                with n Pair Some fields have "load cp ((i⇩p, t⇩p) # pl) (e # el) e⇩v' cd' sck' mem' e⇩v cd st g = load cp pl el e⇩v'' cd'' k'' m'' e⇩v cd st g''" using load.psimps(1)[OF 28(1)] Storage notCP by (simp split:option.splits)
                with load_def have "load cp pl el e⇩v'' cd'' k'' m'' e⇩v cd st g'' = Normal ((ev, cda, k, m), g')" by simp
                with Pair fields have "g' ≤ g'' ∧ Address ev = Address e⇩v'' ∧ Sender ev = Sender e⇩v'' ∧ Svalue ev = Svalue e⇩v'' ∧ Contract ev = Contract  e⇩v''" using 28(3) n Pair 1 Storage notCP none by fastforce
                moreover from n have "g'' ≤ g" using 28(2) Storage notCP none by (simp add: "28.hyps"(2))
                moreover from Some fields have "Address e⇩v'' =  Address e⇩v' ∧ Sender e⇩v'' = Sender e⇩v' ∧ Svalue e⇩v'' = Svalue e⇩v'∧ Contract e⇩v'' = Contract e⇩v'" using decl_env by auto
                ultimately show "g' ≤ g ∧ Address ev = Address e⇩v' ∧ Sender ev = Sender e⇩v' ∧ Svalue ev = Svalue e⇩v'∧ Contract ev = Contract e⇩v'" by auto
              qed
            qed
          qed
        qed
      next
        case (e _)
        with 28(1) show ?thesis using load.psimps(1) Storage notCP by (simp split:option.splits)
      qed

    qed  
      
  qed
next
  case 29
  then show ?case using load.psimps(2) by auto
next
  case 30
  then show ?case using load.psimps(3) by auto
next
  case 31
  then show ?case using load.psimps(4) by auto
next
  case (32 i e cd st g)
  show ?case
  proof (rule allI[THEN allI, OF impI])
    fix xa xaa assume "rexp (l.Id i) e cd st g = Normal (xa, xaa)"
    then show "xaa ≤ g" using 32(1) rexp.psimps(1) by (simp split: option.split_asm denvalue.split_asm stackvalue.split_asm prod.split_asm type.split_asm stypes.split_asm)
  qed
next
  case (33 i r e cd st g)
  show ?case
  proof (rule allI[THEN allI,OF impI])
    fix xa xaa assume rexp_def: "rexp (Ref i r) e cd st g = Normal (xa, xaa)"
    show "xaa ≤ g"
    proof (cases "fmlookup (Denvalue e) i")
      case None
      with 33(1) show ?thesis using rexp.psimps rexp_def 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 33(1) Some Pair Stackloc show ?thesis using rexp.psimps(2) rexp_def by simp
          next
            case s1: (Some a)
            then show ?thesis
            proof (cases a)
              case (KValue x1)
              with 33(1) Some Pair Stackloc s1 show ?thesis using rexp.psimps(2) rexp_def by simp
            next
              case (KCDptr l')
              with 33 Some Pair Stackloc s1 show ?thesis using rexp.psimps(2)[of i r e cd st] rexp_def by (simp split: option.split_asm memoryvalue.split_asm mtypes.split_asm prod.split_asm type.split_asm StateMonad.result.split_asm)
            next
              case (KMemptr x3)
              with 33 Some Pair Stackloc s1 show ?thesis using rexp.psimps(2)[of i r e cd st] rexp_def by (simp split: option.split_asm memoryvalue.split_asm mtypes.split_asm prod.split_asm type.split_asm StateMonad.result.split_asm)
            next
              case (KStoptr x4)
              with 33 Some Pair Stackloc s1 show ?thesis using rexp.psimps(2)[of i r e cd st] rexp_def by (simp split: option.split_asm stypes.split_asm prod.split_asm type.split_asm StateMonad.result.split_asm)
            qed
          qed
        next
          case (Storeloc x2)
          with 33 Some Pair show ?thesis using rexp.psimps rexp_def by (simp split: option.split_asm stypes.split_asm prod.split_asm type.split_asm  StateMonad.result.split_asm)
        qed
      qed
    qed
  qed
next
  case (34 e cd st g)
  then show ?case using expr.psimps(20) by (simp split:nat.split)
qed



text ‹Now we can define the termination function›

fun mgas
  where "mgas (Inr (Inr (Inr l))) = snd (snd (snd (snd l)))" (*rexp*)
        | "mgas (Inr (Inr (Inl l))) = snd (snd (snd (snd (snd (snd (snd (snd (snd (snd l)))))))))" (*load*)
        | "mgas (Inr (Inl l)) = snd (snd (snd (snd l)))" (*expr*)
        | "mgas (Inl (Inr l)) = snd (snd (snd (snd (snd (snd l)))))"  (*ssel*)
        | "mgas (Inl (Inl l)) = snd (snd (snd (snd (snd (snd (snd l))))))" (*msel*)

fun msize
  where "msize (Inr (Inr (Inr l))) = size (fst l)"
        | "msize (Inr (Inr (Inl l))) = size_list size (fst (snd (snd l)))"
        | "msize (Inr (Inl l)) = size (fst l)"
        | "msize (Inl (Inr l)) = size_list size (fst (snd (snd l)))"
        | "msize (Inl (Inl l)) = size_list size (fst (snd (snd (snd l))))"

method msel_ssel_expr_load_rexp_dom =
  match premises in e: "expr _ _ _ _ _ = Normal (_,_)" and d[thin]: "msel_ssel_expr_load_rexp_dom (Inr (Inl _))" ⇒ ‹insert msel_ssel_expr_load_rexp_dom_gas(3)[OF d e]› |
  match premises in l: "load _ _ _ _ _ _ _ _ _ _ _ = Normal (_,_)" and d[thin]: "msel_ssel_expr_load_rexp_dom (Inr (Inr (Inl _)))" ⇒ ‹insert msel_ssel_expr_load_rexp_dom_gas(4)[OF d l, THEN conjunct1]›

method costs =
  match premises in "costs⇩e (CALL i xe) e cd st < _" for i xe and e::environment and cd::calldataT and st::state ⇒ ‹insert call_not_zero[of (unchecked) i xe e cd st]› |
  match premises in "costs⇩e (ECALL ad i xe) e cd st < _" for ad i xe and e::environment and cd::calldataT and st::state ⇒ ‹insert ecall_not_zero[of (unchecked) ad i xe e cd st]›

termination msel
  apply (relation "measures [mgas, msize]")
  apply (auto split:member.split_asm prod.split_asm bool.split_asm if_split_asm stackvalue.split_asm option.split_asm type.split_asm types.split_asm memoryvalue.split_asm atype.split_asm)
  apply (msel_ssel_expr_load_rexp_dom+, costs?, arith)+
  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 msel_ssel_expr_load_rexp_dom:
    "msel_ssel_expr_load_rexp_dom (Inl (Inl (c1, t1, l1, xe1, ev1, cd1, st1, g1)))"
    "msel_ssel_expr_load_rexp_dom (Inl (Inr (t2, l2, xe2, ev2, cd2, st2, g2)))"
    "msel_ssel_expr_load_rexp_dom (Inr (Inl (e4, ev4, cd4, st4, g4)))"
    "msel_ssel_expr_load_rexp_dom (Inr (Inr (Inl (lcp, lis, lxs, lev0, lcd0, lk, lm, lev, lcd, lst, lg))))"
    "msel_ssel_expr_load_rexp_dom (Inr (Inr (Inr (l3, ev3, cd3, st3, g3))))"
by (induct rule: msel_ssel_expr_load_rexp.induct
[where ?P1.0="λc1 t1 l1 xe1 ev1 cd1 st1 g1. msel_ssel_expr_load_rexp_dom (Inl (Inl (c1, t1, l1, xe1, ev1, cd1, st1, g1)))"
   and ?P2.0="λt2 l2 xe2 ev2 cd2 st2 g2. msel_ssel_expr_load_rexp_dom (Inl (Inr (t2, l2, xe2, ev2, cd2, st2, g2)))"
   and ?P3.0="λe4 ev4 cd4 st4 g4. msel_ssel_expr_load_rexp_dom (Inr (Inl (e4, ev4, cd4, st4, g4)))"
   and ?P4.0="λlcp lis lxs lev0 lcd0 lk lm lev lcd lst lg. msel_ssel_expr_load_rexp_dom (Inr (Inr (Inl (lcp, lis, lxs, lev0, lcd0, lk, lm, lev, lcd, lst, lg))))"
   and ?P5.0="λl3 ev3 cd3 st3 g3. msel_ssel_expr_load_rexp_dom (Inr (Inr (Inr (l3, ev3, cd3, st3, g3))))"
], simp_all add: msel_ssel_expr_load_rexp.domintros)

lemmas msel_ssel_expr_load_rexp_gas =
  msel_ssel_expr_load_rexp_dom_gas(1)[OF msel_ssel_expr_load_rexp_dom(1)]
  msel_ssel_expr_load_rexp_dom_gas(2)[OF msel_ssel_expr_load_rexp_dom(2)]
  msel_ssel_expr_load_rexp_dom_gas(3)[OF msel_ssel_expr_load_rexp_dom(3)]
  msel_ssel_expr_load_rexp_dom_gas(4)[OF msel_ssel_expr_load_rexp_dom(4)]
  msel_ssel_expr_load_rexp_dom_gas(5)[OF msel_ssel_expr_load_rexp_dom(5)]

lemma expr_sender:
  assumes "expr SENDER e cd st g = Normal ((KValue adv, Value TAddr), g')"
  shows "adv = Sender e" using assms by (simp split:if_split_asm)

declare expr.simps[simp del, solidity_symbex add]
declare load.simps[simp del, solidity_symbex add]
declare ssel.simps[simp del, solidity_symbex add]
declare msel.simps[simp del, solidity_symbex add]
declare rexp.simps[simp del, solidity_symbex add]


lemma load_denval_sub[rule_format]:
  "∀l1'  t1' g1' arr. msel c1 t1 l1 xe1 ev1 cd1 st1 g1 = Normal ((l1', t1'), g1') ⟶ True"
  "∀l2' v2' t2' g2'. ssel t2 l2 xe2 ev2 cd2 st2 g2 = Normal ((l2', t2'), g2') ⟶ True"
  "∀v t g4'. expr e4 ev4 cd4 st4 g4 = Normal ((v, t), g4') ⟶ True"        (*lev0 lcd0 lk lm*)

  "∀ev cd k m g'. load lcp lis lxs lev0 lcd0 lk lm lev lcd lst lg = Normal ((ev, cd, k, m), g') ⟶ fmdom (Denvalue lev0) |⊆| fmdom (Denvalue ev) "
  "∀v3' t3'  g3'. rexp l3 ev3 cd3 st3 g3 = Normal ((v3', t3'), g3') ⟶ True"
proof (induct rule: msel_ssel_expr_load_rexp.induct
    [where ?P1.0="λc1 t1 l1 xe1 ev1 cd1 st1 g1. (∀l1'  t1' g1' arr. msel c1 t1 l1 xe1 ev1 cd1 st1 g1 = Normal ((l1',  t1'), g1') ⟶ True)"
      and ?P2.0="λt2 l2 xe2 ev2 cd2 st2 g2. (∀l2' v2' t2' g2'. ssel t2 l2 xe2 ev2 cd2 st2 g2 = Normal ((l2',  t2'), g2')⟶ True)"
      and ?P3.0="λe4 ev4 cd4 st4 g4. (∀v t g4'. expr e4 ev4 cd4 st4 g4 = Normal ((v, t), g4')⟶ True)"
      and ?P4.0="λlcp lis lxs lev0 lcd0 lk lm lev lcd lst lg. (∀ev cd k m g'. load lcp lis lxs lev0 lcd0 lk lm lev lcd lst lg = Normal ((ev, cd, k, m), g') ⟶ fmdom (Denvalue lev0) |⊆| fmdom (Denvalue ev) )"
      and ?P5.0="λl3 ev3 cd3 st3 g3. (∀v3' t3' g3'. rexp l3 ev3 cd3 st3 g3 = Normal (( v3',  t3'), g3') ⟶ True)"
      ])
  case (1 uu uv uw ux uy uz g)
  then show ?case by simp
next
  case (2 va vb vc vd ve vf vg g)
  then show ?case by simp
next
  case (3 vh al t loc x env cd st g)
  then show ?case by simp
next
  case (4 mm al t loc x y ys env cd st g)
  then show ?case by simp
next
  case (5 tp loc vi vj vk g)
  then show ?case by simp
next
  case (6 vl vm vn vo vp vq vr g)
  then show ?case by simp
next
  case (7 al t loc x xs env cd st g)
  then show ?case by simp
next
  case (8 t t' loc x xs env cd st g)
  then show ?case by simp
next
  case (9 b x e cd st g)
  then show ?case by simp
next
  case (10 b x e cd st g)
  then show ?case by simp
next
  case (11 ad e cd st g)
  then show ?case by simp
next
  case (12 ad e cd st g)
  then show ?case by simp
next
  case (13 e cd st g)
  then show ?case by simp
next
  case (14 e cd st g)
  then show ?case by simp
next
  case (15 e cd st g)
  then show ?case by simp
next
  case (16 e cd st g)
  then show ?case by simp
next
  case (17 e cd st g)
  then show ?case by simp
next
  case (18 x e cd st g)
  then show ?case by simp
next
  case (19 e1 e2 e cd st g)
  then show ?case by simp
next
  case (20 e1 e2 e cd st g)
  then show ?case by simp
next
  case (21 e1 e2 e cd st g)
  then show ?case by simp
next
  case (22 e1 e2 e cd st g)
  then show ?case by simp
next
  case (23 e1 e2 e cd st g)
  then show ?case by simp
next
  case (24 e1 e2 e cd st g)
  then show ?case by simp
next
  case (25 i e cd st g)
  then show ?case by simp
next
  case (26 i xe e cd st g)
  then show ?case by simp
next
  case (27 ad i xe e cd st g)
  then show ?case by simp
next
 case (28 cp i⇩p t⇩p pl ex el e⇩v' cd' sck' mem' e⇩v cd st g)
  show ?case
  proof(intros)
    fix ev cda k m g' locs t l stloc
    assume as1:"local.load cp ((i⇩p, t⇩p) # pl) (ex # el) e⇩v' cd' sck' mem' e⇩v cd st g = Normal ((ev, cda, k, m), g')"
    then have none:"Denvalue e⇩v' $$ i⇩p = None" using load.simps(1)[of cp i⇩p t⇩p  pl ex  el e⇩v' cd' sck' mem' e⇩v cd st g] as1 
      by (simp split:type.splits option.splits)

    then obtain x g4' where a7:"expr ex e⇩v cd st g = Normal (x, g4')" 
      using as1 load.simps(1)[of cp i⇩p t⇩p  pl ex  el e⇩v' cd' sck' mem' e⇩v cd st g] 
      by (simp split:if_splits type.splits result.splits prod.splits option.splits)
    then have  a8:"∃v t. expr ex e⇩v cd st g = Normal ((v, t), g4')" using as1 by simp
    then obtain v t where a10:"expr ex e⇩v cd st g = Normal ((v, t), g4')"  using as1 load.simps(1)[of cp i⇩p t⇩p  pl ex  el e⇩v' cd' sck' mem' e⇩v cd st g] by (auto split: result.splits prod.splits option.splits)
    then obtain c m' k' e where a15:"decl i⇩p t⇩p (Some (v,t)) cp cd (Memory st)  (Storage st (Address e⇩v)) (cd', mem',  sck', e⇩v') = Some (c, m', k', e)" 
      using as1 load.simps(1) by (auto split:if_splits type.splits result.splits prod.splits option.splits)
    then have a20:"load cp pl el e c k' m' e⇩v cd st g4' = Normal ((ev, cda, k, m), g')"  
      using as1 load.simps(1)[of cp i⇩p t⇩p  pl ex  el e⇩v' cd' sck' mem' e⇩v cd st g] a10 a15 
      by (simp split:if_splits type.splits option.splits)
    have a30:"fmdom (Denvalue e⇩v') |⊆| fmdom (Denvalue e)"using decl_env_subset_denval a15 by simp
    have "fmdom (Denvalue e) |⊆| fmdom (Denvalue ev)" 
    proof(cases t⇩p)
      case (Value x1)
      then show ?thesis using 28 a20 a7 a8 a10 a15 none by fastforce
    next
      case (Calldata x2)
      then show ?thesis using 28 a20 a7 a8 a10 a15 none by fastforce
    next
      case (Memory x3)
      then show ?thesis using 28 a20 a7 a8 a10 a15 none by fastforce
    next
      case (Storage x4)
      then have "¬cp" using as1 load.simps by auto
      then show ?thesis using 28 a20 a7 a8 a10 a15 none Storage by fastforce
    qed
    then show "fmdom (Denvalue e⇩v') |⊆| fmdom (Denvalue ev)" using a30 by simp 
  qed
next
  case (29 vt vu vv vw vx vy vz wa wb wc g)
  show ?case
  proof(intros)
    fix ev cd k m g' locs
    assume a1: "load vt [] (vu # vv) vw vx vy vz wa wb wc g = Normal ((ev, cd, k, m), g') "
    then show "fmdom (Denvalue vw) |⊆| fmdom (Denvalue ev)" using load.simps(2) by (auto split:if_split_asm result.splits)
  qed
next
  case (30 wd we wf wg wh wi wj wk wl wm g)
  show ?case
  proof(intros)
    fix ev cd k m g' locs
    assume a1: " load wd (we # wf) [] wg wh wi wj wk wl wm g = Normal ((ev, cd, k, m), g')"
    then show " fmdom (Denvalue wg) |⊆| fmdom (Denvalue ev)" using load.simps(3) by (auto split:if_split_asm result.splits)

  qed
next
  case (31 wn e⇩v' cd' sck' mem' e⇩v cd st g)
  show ?case
  proof(intros)
    fix ev cda k m g' locs
      (* cd' = cda ⟹ sck' = k ⟹ mem' = m*)
    assume a1: " load wn [] [] e⇩v' cd' sck' mem' e⇩v cd st g = Normal ((ev, cda, k, m), g')"
    then show "fmdom (Denvalue e⇩v') |⊆| fmdom (Denvalue ev)" using load.simps(4)[of wn e⇩v' cd' sck' mem' e⇩v cd st g] by (auto split:if_split_asm result.splits)
  qed
next
  case (32 i e cd st g)
  then show ?case by simp
next
  case (33 i r e cd st g)
  then show ?case by simp
next
  case (34 e cd st g)
  then show ?case by simp
qed

lemma load_denval_existing_remain[rule_format]:
  "∀l1'  t1' g1' arr. msel c1 t1 l1 xe1 ev1 cd1 st1 g1 = Normal ((l1', t1'), g1') ⟶ True"
  "∀l2' v2' t2' g2'. ssel t2 l2 xe2 ev2 cd2 st2 g2 = Normal ((l2', t2'), g2') ⟶ True"
  "∀v t g4'. expr e4 ev4 cd4 st4 g4 = Normal ((v, t), g4') ⟶ True"        (*lev0 lcd0 lk lm*)

  "∀ev cd k m g' id x. load lcp lis lxs lev0 lcd0 lk lm lev lcd lst lg = Normal ((ev, cd, k, m), g') ∧ Denvalue lev0 $$ id = Some x ⟶ (Denvalue ev) $$ id = Some x "
  "∀v3' t3'  g3'. rexp l3 ev3 cd3 st3 g3 = Normal ((v3', t3'), g3') ⟶ True"
proof (induct rule: msel_ssel_expr_load_rexp.induct
    [where ?P1.0="λc1 t1 l1 xe1 ev1 cd1 st1 g1. (∀l1'  t1' g1' arr. msel c1 t1 l1 xe1 ev1 cd1 st1 g1 = Normal ((l1',  t1'), g1') ⟶ True)"
      and ?P2.0="λt2 l2 xe2 ev2 cd2 st2 g2. (∀l2' v2' t2' g2'. ssel t2 l2 xe2 ev2 cd2 st2 g2 = Normal ((l2',  t2'), g2')⟶ True)"
      and ?P3.0="λe4 ev4 cd4 st4 g4. (∀v t g4'. expr e4 ev4 cd4 st4 g4 = Normal ((v, t), g4')⟶ True)"
      and ?P4.0="λlcp lis lxs lev0 lcd0 lk lm lev lcd lst lg. (∀ev cd k m g' id x. load lcp lis lxs lev0 lcd0 lk lm lev lcd lst lg = Normal ((ev, cd, k, m), g') ∧ Denvalue lev0 $$ id = Some x ⟶ (Denvalue ev) $$ id = Some x)"
      and ?P5.0="λl3 ev3 cd3 st3 g3. (∀v3' t3' g3'. rexp l3 ev3 cd3 st3 g3 = Normal (( v3',  t3'), g3') ⟶ True)"
      ])
  case (1 uu uv uw ux uy uz g)
  then show ?case by simp
next
  case (2 va vb vc vd ve vf vg g)
  then show ?case by simp
next
  case (3 vh al t loc x env cd st g)
  then show ?case by simp
next
  case (4 mm al t loc x y ys env cd st g)
  then show ?case by simp
next
  case (5 tp loc vi vj vk g)
  then show ?case by simp
next
  case (6 vl vm vn vo vp vq vr g)
  then show ?case by simp
next
  case (7 al t loc x xs env cd st g)
  then show ?case by simp
next
  case (8 t t' loc x xs env cd st g)
  then show ?case by simp
next
  case (9 b x e cd st g)
  then show ?case by simp
next
  case (10 b x e cd st g)
  then show ?case by simp
next
  case (11 ad e cd st g)
  then show ?case by simp
next
  case (12 ad e cd st g)
  then show ?case by simp
next
  case (13 e cd st g)
  then show ?case by simp
next
  case (14 e cd st g)
  then show ?case by simp
next
  case (15 e cd st g)
  then show ?case by simp
next
  case (16 e cd st g)
  then show ?case by simp
next
  case (17 e cd st g)
  then show ?case by simp
next
  case (18 x e cd st g)
  then show ?case by simp
next
  case (19 e1 e2 e cd st g)
  then show ?case by simp
next
  case (20 e1 e2 e cd st g)
  then show ?case by simp
next
  case (21 e1 e2 e cd st g)
  then show ?case by simp
next
  case (22 e1 e2 e cd st g)
  then show ?case by simp
next
  case (23 e1 e2 e cd st g)
  then show ?case by simp
next
  case (24 e1 e2 e cd st g)
  then show ?case by simp
next
  case (25 i e cd st g)
  then show ?case by simp
next
  case (26 i xe e cd st g)
  then show ?case by simp
next
  case (27 ad i xe e cd st g)
  then show ?case by simp
next
 case (28 cp i⇩p t⇩p pl ex el e⇩v' cd' sck' mem' e⇩v cd st g)
  show ?case
  proof(intros)
    fix ev cda k m g' id x
    assume as1:"load cp ((i⇩p, t⇩p) # pl) (ex # el) e⇩v' cd' sck' mem' e⇩v cd st g = Normal ((ev, cda, k, m), g') ∧ Denvalue e⇩v' $$ id = Some x"
    then have none:"Denvalue e⇩v' $$ i⇩p = None" using load.simps(1)[of cp i⇩p t⇩p  pl ex  el e⇩v' cd' sck' mem' e⇩v cd st g] as1 
      by (simp split:type.splits option.splits)

    then obtain x' g4' where a7:"expr ex e⇩v cd st g = Normal (x', g4')"
      using as1 load.simps(1)[of cp i⇩p t⇩p  pl ex  el e⇩v' cd' sck' mem' e⇩v cd st g] 
      by (simp split:if_splits type.splits result.splits prod.splits option.splits)
    then have  a8:"∃v t. expr ex e⇩v cd st g = Normal ((v, t), g4')" using as1 by simp
    then obtain v t where a10:"expr ex e⇩v cd st g = Normal ((v, t), g4')"  using as1 load.simps(1)[of cp i⇩p t⇩p  pl ex  el e⇩v' cd' sck' mem' e⇩v cd st g] by (auto split: result.splits prod.splits option.splits)
    then obtain c m' k' e where a15:"decl i⇩p t⇩p (Some (v,t)) cp cd (Memory st)  (Storage st (Address e⇩v)) (cd', mem',  sck', e⇩v') = Some (c, m', k', e)"
      using as1 load.simps(1) by (auto split: if_splits type.splits result.splits prod.splits option.splits)
    then have a20:"load cp pl el e c k' m' e⇩v cd st g4' = Normal ((ev, cda, k, m), g')"  
      using as1 load.simps(1)[of cp i⇩p t⇩p  pl ex  el e⇩v' cd' sck' mem' e⇩v cd st g] a10 a15 
      by (simp split:if_splits type.splits option.splits)
    have a30:"fmdom (Denvalue e⇩v') |⊆| fmdom (Denvalue e)"using decl_env_subset_denval a15 by simp
    
    then show "Denvalue ev $$ id = Some x"
    proof(cases t⇩p)
      case (Value x1)
      then show ?thesis 
      proof(cases "id = i⇩p")
        case True
        then show ?thesis using as1 load.simps none by simp
      next
        case False
        then have a50:" Denvalue e $$ id = Some x" using a15 a20 as1 none 
          using decl_env_monotonic[OF a15, of id] 
          by simp
        have "∀ev cda k m g' id x. load cp pl el  e c k' m' e⇩v cd st g4' = Normal ((ev, cda, k, m), g') ∧ Denvalue e $$ id = Some x ⟶ Denvalue ev $$ id = Some x"
          using 28(2)[OF]  Value none a10 a20 a7 a8 a10 a15 none False by fastforce
        then have "Denvalue e $$ id = Some x ⟶ Denvalue ev $$ id = Some x" using a20 by blast
        then show ?thesis using a50 by simp
      qed
    next
      case (Calldata x2)
      then show ?thesis
      proof(cases "id = i⇩p")
        case True
        then show ?thesis using as1 load.simps none by simp
      next
        case False
        then have a50:" Denvalue e $$ id = Some x" using a15 a20 as1 none 
          using decl_env_monotonic by presburger
        have "∀ev cda k m g' id x. load cp pl el  e c k' m' e⇩v cd st g4' = Normal ((ev, cda, k, m), g') ∧ Denvalue e $$ id = Some x ⟶ Denvalue ev $$ id = Some x"
          using 28(2) Calldata none a10 a20 a7 a8 a10 a15 none False by fastforce
        then have "Denvalue e $$ id = Some x ⟶ Denvalue ev $$ id = Some x" using a20 by blast
        then show ?thesis using a50 by simp
      qed
    next
      case (Memory x3)
      then show ?thesis
      proof(cases "id = i⇩p")
        case True
        then show ?thesis using as1 load.simps none by simp
      next
        case False
        then have a50:" Denvalue e $$ id = Some x" using a15 a20 as1 none 
          using decl_env_monotonic by presburger
        have "∀ev cda k m g' id x. load cp pl el  e c k' m' e⇩v cd st g4' = Normal ((ev, cda, k, m), g') ∧ Denvalue e $$ id = Some x ⟶ Denvalue ev $$ id = Some x"
          using 28(2) Memory a20 a7 a8 a10 a15 none False by fastforce
        then have "Denvalue e $$ id = Some x ⟶ Denvalue ev $$ id = Some x" using a20 by blast
        then show ?thesis using a50 by simp
      qed
    next
      case (Storage x4)
      then show ?thesis
      proof(cases "id = i⇩p")
        case True
        then show ?thesis using as1 load.simps none by simp
      next
        case False
        then have a50:" Denvalue e $$ id = Some x" using a15 a20 as1 none 
          using decl_env_monotonic by presburger
        have "¬cp" using as1 load.simps Storage by auto
        then have "∀ev cda k m g' id x. load cp pl el  e c k' m' e⇩v cd st g4' = Normal ((ev, cda, k, m), g') ∧ Denvalue e $$ id = Some x ⟶ Denvalue ev $$ id = Some x"
          using 28(2) Storage a20 a7 a8 a10 a15 none False by fastforce
        then have "Denvalue e $$ id = Some x ⟶ Denvalue ev $$ id = Some x" using a20 by blast
        then show ?thesis using a50 by simp
      qed
    qed
  qed
next
  case (29 vt vu vv vw vx vy vz wa wb wc g)
  show ?case
  proof(intros)
    fix ev cd k m g' locs id x
    assume a1: "load vt [] (vu # vv) vw vx vy vz wa wb wc g = Normal ((ev, cd, k, m), g') ∧ Denvalue vw $$ id = Some x"
    then show "Denvalue ev $$ id = Some x " using load.simps(2) by (auto split:if_split_asm result.splits)
  qed
next
  case (30 wd we wf wg wh wi wj wk wl wm g)
  show ?case
  proof(intros)
    fix ev cd k m g' locs id x
    assume a1: " load wd (we # wf) [] wg wh wi wj wk wl wm g = Normal ((ev, cd, k, m), g')∧ Denvalue wg $$ id = Some x"
    then show "Denvalue ev $$ id = Some x" using load.simps(3) by (auto split:if_split_asm result.splits)

  qed
next
  case (31 wn e⇩v' cd' sck' mem' e⇩v cd st g)
  show ?case
  proof(intros)
    fix ev cda k m g' locs id x
      (* cd' = cda ⟹ sck' = k ⟹ mem' = m*)
    assume a1: " load wn [] [] e⇩v' cd' sck' mem' e⇩v cd st g = Normal ((ev, cda, k, m), g') ∧  Denvalue e⇩v' $$ id = Some x"
    then show " Denvalue ev $$ id = Some x" using load.simps(4)[of wn e⇩v' cd' sck' mem' e⇩v cd st g] by (auto split:if_split_asm result.splits)
  qed
next
  case (32 i e cd st g)
  then show ?case by simp
next
  case (33 i r e cd st g)
  then show ?case by simp
next
  case (34 e cd st g)
  then show ?case by simp
qed

end

end