Theory Statements

section ‹Statements›
theory Statements
  imports Environment StateMonad
begin

subsection ‹Syntax›

subsubsection ‹Expressions›
datatype L = Id Identifier
           | Ref Identifier "E list"
and      E = INT nat int
           | UINT nat int
           | ADDRESS String.literal
           | BALANCE E
           | THIS
           | SENDER
           | VALUE
           | TRUE
           | FALSE
           | LVAL L
           | PLUS E E
           | MINUS E E
           | EQUAL E E
           | LESS E E
           | AND E E
           | OR E E
           | NOT E
           | CALL Identifier "E list"
           | ECALL E Identifier "E list" E

subsubsection ‹Statements›
datatype S = SKIP
           | BLOCK "(Identifier × Type) × (E option)" S
           | ASSIGN L E
           | TRANSFER E E
           | COMP S S
           | ITE E S S
           | WHILE E S
           | INVOKE Identifier "E list"
           | EXTERNAL E Identifier "E list" E

abbreviation
  "vbits≡{8,16,24,32,40,48,56,64,72,80,88,96,104,112,120,128,
          136,144,152,160,168,176,184,192,200,208,216,224,232,240,248,256}"

lemma vbits_max[simp]:
  assumes "b1 ∈ vbits"
    and "b2 ∈ vbits"
  shows "(max b1 b2) ∈ vbits"
proof -
  consider (b1) "max b1 b2 = b1" | (b2) "max b1 b2 = b2" by (metis max_def)
  then show ?thesis
  proof cases
    case b1
    then show ?thesis using assms(1) by simp
  next
    case b2
    then show ?thesis using assms(2) by simp
  qed
qed

lemma vbits_ge_0: "(x::nat)∈vbits ⟹ x>0" by auto

subsection ‹Contracts›

text ‹
  A contract consists of methods or storage variables.
  A method is a triple consisting of
  \begin{itemize}
    \item A list of formal parameters
    \item A statement
    \item An optional return value
  \end{itemize}
›

datatype Member = Method "(Identifier × Type) list × S × E option"
                  | Var STypes

text ‹
  A procedure environment assigns a contract to an address.
  A contract consists of
  \begin{itemize}
    \item An assignment of members to identifiers
    \item An optional fallback statement which is executed after money is beeing transferred to the contract.
  \end{itemize}
  \url{https://docs.soliditylang.org/en/v0.8.6/contracts.html#fallback-function}
›

type_synonym EnvironmentP = "(Address, (Identifier, Member) fmap × S) fmap"

definition init::"(Identifier, Member) fmap ⇒ Identifier ⇒ Environment ⇒ Environment"
  where "init ct i e = (case fmlookup ct i of
                                Some (Var tp) ⇒ updateEnvDup i (Storage tp) (Storeloc i) e
                               | _ ⇒ e)"

lemma init_s11[simp]:
  assumes "fmlookup ct i = Some (Var tp)"
  shows "init ct i e = updateEnvDup i (Storage tp) (Storeloc i) e"
  using assms init_def by simp

lemma init_s12[simp]:
  assumes "i |∈| fmdom (denvalue e)"
  shows "init ct i e = e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis using init_def by simp
next
  case (Some a)
  then show ?thesis
  proof (cases a)
    case (Method x1)
    with Some show ?thesis using init_def by simp
  next
    case (Var tp)
    with Some have "init ct i e = updateEnvDup i (Storage tp) (Storeloc i) e" using init_def by simp
    moreover from assms have "updateEnvDup i (Storage tp) (Storeloc i) e = e" by auto
    ultimately show ?thesis by simp
  qed
qed

lemma init_s13[simp]:
  assumes "fmlookup ct i = Some (Var tp)"
      and "¬ i |∈| fmdom (denvalue e)"
  shows "init ct i e = updateEnv i (Storage tp) (Storeloc i) e"
  using assms init_def by auto

lemma init_s21[simp]:
  assumes "fmlookup ct i = None"
  shows "init ct i e = e"
  using assms init_def by auto

lemma init_s22[simp]:
  assumes "fmlookup ct i = Some (Method m)"
  shows "init ct i e = e"
  using assms init_def by auto

lemma init_commte: "comp_fun_commute (init ct)"
proof
  fix x y
  show "init ct y ∘ init ct x = init ct x ∘ init ct y"
  proof
    fix e
    show "(init ct y ∘ init ct x) e = (init ct x ∘ init ct y) e"
    proof (cases "fmlookup ct x")
      case None
      then show ?thesis by simp
    next
      case s1: (Some a)
      then show ?thesis
      proof (cases a)
        case (Method x1)
        with s1 show ?thesis by simp
      next
        case v1: (Var tp)
        then show ?thesis
        proof (cases "x |∈| fmdom (denvalue e)")
          case True
          with s1 v1 have *: "init ct x e = e" by auto
          then show ?thesis
          proof (cases "fmlookup ct y")
            case None
            then show ?thesis by simp
          next
            case s2: (Some a)
            then show ?thesis
            proof (cases a)
              case (Method x1)
              with s2 show ?thesis by simp
            next
              case v2: (Var tp')
              then show ?thesis
              proof (cases "y |∈| fmdom (denvalue e)")
                case t1: True
                with s1 v1 True s2 v2 show ?thesis by fastforce
              next
                define e' where "e' = updateEnv y (Storage tp') (Storeloc y) e"
                case False
                with s2 v2 have "init ct y e = e'" using e'_def by auto
                with s1 v1 True e'_def * show ?thesis by auto
              qed
            qed
          qed
        next
          define e' where "e' = updateEnv x (Storage tp) (Storeloc x) e"
          case f1: False
          with s1 v1 have *: "init ct x e = e'" using e'_def by auto
          then show ?thesis
          proof (cases "fmlookup ct y")
            case None
            then show ?thesis by simp
          next
            case s3: (Some a)
            then show ?thesis
            proof (cases a)
              case (Method x1)
              with s3 show ?thesis by simp
            next
              case v2: (Var tp')
              then show ?thesis
              proof (cases "y |∈| fmdom (denvalue e)")
                case t1: True
                with e'_def have "y |∈| fmdom (denvalue e')" by simp
                with s1 s3 v1 f1 v2 show ?thesis using e'_def by fastforce
              next
                define f' where "f' = updateEnv y (Storage tp') (Storeloc y) e"
                define e'' where "e'' = updateEnv y (Storage tp') (Storeloc y) e'"
                case f2: False
                with s3 v2 have **: "init ct y e = f'" using f'_def by auto
                show ?thesis
                proof (cases "y = x")
                  case True
                  with s3 v2 e'_def have "init ct y e' = e'" by simp
                  moreover from s3 v2 True f'_def have "init ct x f' = f'" by simp
                  ultimately show ?thesis using True by simp
                next
                  define f'' where "f'' = updateEnv x (Storage tp) (Storeloc x) f'"
                  case f3: False
                  with f2 have "¬ y |∈| fmdom (denvalue e')" using e'_def by simp
                  with s3 v2 e''_def have "init ct y e' = e''" by auto
                  with * have "(init ct y ∘ init ct x) e = e''" by simp
                  moreover have "init ct x f' = f''"
                  proof -
                    from s1 v1 have "init ct x f' = updateEnvDup x (Storage tp) (Storeloc x) f'" by simp
                    moreover from f1 f3 have "x |∉| fmdom (denvalue f')" using f'_def by simp
                    ultimately show ?thesis using f''_def by auto
                  qed
                  moreover from f''_def e''_def f'_def e'_def f3 have "Some f'' = Some e''" using env_reorder_neq by simp
                  ultimately show ?thesis using ** by simp
                qed
              qed
            qed
          qed
        qed
      qed
    qed
  qed
qed

lemma init_address[simp]:
  "address (init ct i e) = address e ∧ sender (init ct i e) = sender e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis by simp
next
  case (Some a)
  show ?thesis
  proof (cases a)
    case (Method x1)
    with Some show ?thesis by simp
  next
    case (Var tp)
    with Some show ?thesis using updateEnvDup_address updateEnvDup_sender by simp
  qed 
qed

lemma init_sender[simp]:
"sender (init ct i e) = sender e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis by simp
next
  case (Some a)
  show ?thesis
  proof (cases a)
    case (Method x1)
    with Some show ?thesis by simp
  next
    case (Var tp)
    with Some show ?thesis using updateEnvDup_sender by simp
  qed 
qed

lemma init_svalue[simp]:
"svalue (init ct i e) = svalue e"
proof (cases "fmlookup ct i")
  case None
  then show ?thesis by simp
next
  case (Some a)
  show ?thesis
  proof (cases a)
    case (Method x1)
    with Some show ?thesis by simp
  next
    case (Var tp)
    with Some show ?thesis using updateEnvDup_svalue by simp
  qed 
qed

lemma ffold_init_ad_same[rule_format]: "∀e'. ffold (init ct) e xs = e' ⟶ address e' = address e ∧ sender e' = sender e ∧ svalue e' = svalue e"
proof (induct xs)
  case empty
  then show ?case by (simp add: ffold_def)
next
  case (insert x xs)
  then have *: "ffold (init ct) e (finsert x xs) =
    init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp
  show ?case
  proof (rule allI[OF impI])
    fix e' assume **: "ffold (init ct) e (finsert x xs) = e'"
    with * obtain e'' where ***: "ffold (init ct) e xs = e''" by simp
    with insert have "address e'' = address e ∧ sender e'' = sender e ∧ svalue e'' = svalue e" by blast
    with * ** *** show "address e' = address e ∧ sender e' = sender e ∧ svalue e' = svalue e" using init_address init_sender init_svalue by metis
  qed
qed

lemma ffold_init_dom:
  "fmdom (denvalue (ffold (init ct) e xs)) |⊆| fmdom (denvalue e) |∪| xs"
proof (induct "xs")
  case empty
  then show ?case
  proof
    fix x
    assume "x |∈| fmdom (denvalue (ffold (init ct) e {||}))"
    moreover have "ffold (init ct) e {||} = e"
      using FSet.comp_fun_commute.ffold_empty[OF init_commte, of ct e] by simp
    ultimately show "x |∈| fmdom (denvalue e) |∪| {||}" by simp
  qed
next
  case (insert x xs)
  then have *: "ffold (init ct) e (finsert x xs) =
    init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp

  show ?case
  proof
    fix x' assume "x' |∈| fmdom (denvalue (ffold (init ct) e (finsert x xs)))"
    with * have **: "x' |∈| fmdom (denvalue (init ct x (ffold (init ct) e xs)))" by simp
    then consider "x' |∈| fmdom (denvalue (ffold (init ct) e xs))" | "x'=x"
    proof (cases "fmlookup ct x")
      case None
      then show ?thesis using that ** by simp
    next
      case (Some a)
      then show ?thesis
      proof (cases a)
        case (Method x1)
        then show ?thesis using Some ** that by simp
      next
        case (Var x2)
        show ?thesis
        proof (cases "x=x'")
          case True
          then show ?thesis using that by simp
        next
          case False
          then have "fmlookup (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs))) x' = fmlookup (denvalue (ffold (init ct) e xs)) x'" using updateEnvDup_dup by simp
          moreover from ** Some Var have ***:"x' |∈| fmdom (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs)))" by simp
          ultimately have "x' |∈| fmdom (denvalue (ffold (init ct) e xs))" by (simp add: fmlookup_dom_iff)
          then show ?thesis using that by simp
        qed
      qed
    qed
    then show "x' |∈| fmdom (denvalue e) |∪| finsert x xs"
    proof cases
      case 1
      then show ?thesis using insert.hyps by auto
    next
      case 2
      then show ?thesis by simp
    qed
  qed
qed

lemma ffold_init_fmap: 
  assumes "fmlookup ct i = Some (Var tp)"
      and "i |∉| fmdom (denvalue e)"
  shows "i|∈|xs ⟹ fmlookup (denvalue (ffold (init ct) e xs)) i = Some (Storage tp, Storeloc i)"
proof (induct "xs")
  case empty
  then show ?case by simp
next
  case (insert x xs)
  then have *: "ffold (init ct) e (finsert x xs) =
    init ct x (ffold (init ct) e xs)" using FSet.comp_fun_commute.ffold_finsert[OF init_commte] by simp

  from insert.prems consider (a) "i |∈| xs" | (b) "¬ i |∈| xs ∧ i = x" by auto
  then show "fmlookup (denvalue (ffold (init ct) e (finsert x xs))) i = Some (Storage tp, Storeloc i)"
  proof cases
    case a
    with insert.hyps(2) have "fmlookup (denvalue (ffold (init ct) e xs)) i = Some (Storage tp, Storeloc i)" by simp
    moreover have "fmlookup (denvalue (init ct x (ffold (init ct) e xs))) i = fmlookup (denvalue (ffold (init ct) e xs)) i"
    proof (cases "fmlookup ct x")
      case None
      then show ?thesis by simp
    next
      case (Some a)
      then show ?thesis
      proof (cases a)
        case (Method x1)
        with Some show ?thesis by simp
      next
        case (Var x2)
        with Some have "init ct x (ffold (init ct) e xs) = updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs)" using init_def[of ct x "(ffold (init ct) e xs)"] by simp
        moreover from insert a have "i≠x" by auto
        then have "fmlookup (denvalue (updateEnvDup x (Storage x2) (Storeloc x) (ffold (init ct) e xs))) i = fmlookup (denvalue (ffold (init ct) e xs)) i" using updateEnvDup_dup[of x i] by simp
        ultimately show ?thesis by simp
      qed
    qed
    ultimately show ?thesis using * by simp
  next
    case b
    with assms(1) have "fmlookup ct x = Some (Var tp)" by simp
    moreover from b assms(2) have "¬ x |∈| fmdom (denvalue (ffold (init ct) e xs))" using ffold_init_dom by auto
    ultimately have "init ct x (ffold (init ct) e xs) = updateEnv x (Storage tp) (Storeloc x) (ffold (init ct) e xs)" by auto
    with b * show ?thesis by simp
  qed
qed

text‹The following definition allows for a more fine-grained configuration of the 
     code generator.
›
definition ffold_init::"(String.literal, Member) fmap ⇒ Environment ⇒ String.literal fset ⇒ Environment" where
          ‹ffold_init ct a c = ffold (init ct) a c›
declare ffold_init_def [simp]

lemma ffold_init_code [code]:
     ‹ffold_init ct a c = fold (init ct) (remdups (sorted_list_of_set (fset c))) a›
  using  comp_fun_commute_on.fold_set_fold_remdups ffold.rep_eq 
            ffold_init_def init_commte sorted_list_of_fset.rep_eq 
            sorted_list_of_fset_simps(1)
  by (metis comp_fun_commute.comp_fun_commute comp_fun_commute_on.intro order_refl)

lemma bind_case_stackvalue_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀v. x = KValue v ⟹ f v s = f' v s"
      and "⋀p. x = KCDptr p ⟹ g p s = g' p s"
      and "⋀p. x = KMemptr p ⟹ h p s = h' p s"
      and "⋀p. x = KStoptr p ⟹ i p s = i' p s"
    shows "(case x of KValue v ⇒ f v | KCDptr p ⇒ g p | KMemptr p ⇒ h p | KStoptr p ⇒ i p) s
         = (case x' of KValue v ⇒ f' v | KCDptr p ⇒ g' p | KMemptr p ⇒ h' p | KStoptr p ⇒ i' p) s"
  using assms by (cases x, auto)

lemma bind_case_type_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀t. x = Value t ⟹ f t s = f' t s"
      and "⋀t. x = Calldata t ⟹ g t s = g' t s"
      and "⋀t. x = Memory t ⟹ h t s = h' t s"
      and "⋀t. x = Storage t ⟹ i t s = i' t s"
    shows "(case x of Value t ⇒ f t | Calldata t ⇒ g t | Memory t ⇒ h t | Storage t ⇒ i t ) s
         = (case x' of Value t ⇒ f' t | Calldata t ⇒ g' t | Memory t ⇒ h' t | Storage t ⇒ i' t) s"
  using assms by (cases x, auto)

lemma bind_case_denvalue_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a. x = (Stackloc a) ⟹ f a s = f' a s"
      and "⋀a. x = (Storeloc a) ⟹ g a s = g' a s"
    shows "(case x of (Stackloc a) ⇒ f a | (Storeloc a) ⇒ g a) s
         = (case x' of (Stackloc a) ⇒ f' a | (Storeloc a) ⇒ g' a) s"
  using assms by (cases x, auto)

lemma bind_case_mtypes_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a t. x = (MTArray a t) ⟹ f a t s = f' a t s"
      and "⋀p. x = (MTValue p) ⟹ g p s = g' p s"
    shows "(case x of (MTArray a t) ⇒ f a t | (MTValue p) ⇒ g p) s
         = (case x' of (MTArray a t) ⇒ f' a t | (MTValue p) ⇒ g' p) s"
  using assms by (cases x, auto)

lemma bind_case_stypes_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a t. x = (STArray a t) ⟹ f a t s = f' a t s"
      and "⋀a t. x = (STMap a t) ⟹ g a t s = g' a t s"
      and "⋀p. x = (STValue p) ⟹ h p s = h' p s"
    shows "(case x of (STArray a t) ⇒ f a t | (STMap a t) ⇒ g a t | (STValue p) ⇒ h p) s
         = (case x' of (STArray a t) ⇒ f' a t | (STMap a t) ⇒ g' a t | (STValue p) ⇒ h' p) s"
  using assms by (cases x, auto)

lemma bind_case_types_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a. x = (TSInt a) ⟹ f a s = f' a s"
      and "⋀a. x = (TUInt a) ⟹ g a s = g' a s"
      and "x = TBool ⟹ h s = h' s"
      and "x = TAddr ⟹ i s = i' s"
    shows "(case x of (TSInt a) ⇒ f a | (TUInt a) ⇒ g a | TBool ⇒ h | TAddr ⇒ i) s
         = (case x' of (TSInt a) ⇒ f' a | (TUInt a) ⇒ g' a | TBool ⇒ h' | TAddr ⇒ i') s"
  using assms by (cases x, auto)

lemma bind_case_contract_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a. x = Method a ⟹ f a s = f' a s"
      and "⋀a. x = Var a ⟹ g a s = g' a s"
    shows "(case x of (Method a) ⇒ f a | (Var a) ⇒ g a) s
         = (case x' of (Method a) ⇒ f' a | (Var a) ⇒ g' a) s"
  using assms by (cases x, auto)

lemma bind_case_memoryvalue_cong [fundef_cong]:
  assumes "x = x'"
      and "⋀a. x = MValue a ⟹ f a s = f' a s"
      and "⋀a. x = MPointer a ⟹ g a s = g' a s"
    shows "(case x of (MValue a) ⇒ f a | (MPointer a) ⇒ g a) s
         = (case x' of (MValue a) ⇒ f' a | (MPointer a) ⇒ g' a) s"
  using assms by (cases x, auto)

abbreviation lift ::
  "(E ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (Stackvalue * Type, Ex, State) state_monad)
  ⇒ (Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option)
  ⇒ E ⇒ E ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (Stackvalue * Type, Ex, State) state_monad"
where
  "lift expr f e1 e2 ep e cd ≡
    (do {
      kv1 ← expr e1 ep e cd;
      (case kv1 of
        (KValue v1, Value t1) ⇒ (do
          {
            kv2 ← expr e2 ep e cd;
            (case kv2 of
              (KValue v2, Value t2) ⇒
                (case f t1 t2 v1 v2 of
                  Some (v, t) ⇒ return (KValue v, Value t)
                | None ⇒ throw Err)
            | _ ⇒ (throw Err::(Stackvalue * Type, Ex, State) state_monad))
          })
      | _ ⇒ (throw Err::(Stackvalue * Type, Ex, State) state_monad))
    })"

abbreviation gascheck ::
  "(State ⇒ Gas) ⇒ (unit, Ex, State) state_monad"
where
  "gascheck check ≡
  do {
    g ← (applyf check::(Gas, Ex, State) state_monad);
    (assert Gas (λst. gas st ≤ g) (modify (λst. st ⦇gas:=gas st - g⦈)::(unit, Ex, State) state_monad))
  }"

subsection ‹Semantics›

datatype LType = LStackloc Location
               | LMemloc Location
               | LStoreloc Location


locale statement_with_gas =
  fixes costs :: "S⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Gas"
    and costse :: "E⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Gas"
  assumes while_not_zero[termination_simp]: "⋀e ep cd st ex s0. 0 < (costs (WHILE ex s0) ep e cd st) "
      and call_not_zero[termination_simp]: "⋀e ep cd st i ix. 0 < (costse (CALL i ix) ep e cd st)"
      and ecall_not_zero[termination_simp]: "⋀e ep cd st a i ix val. 0 < (costse (ECALL a i ix val) ep e cd st)"
      and invoke_not_zero[termination_simp]: "⋀e ep cd st i xe. 0 < (costs (INVOKE i xe) ep e cd st)"
      and external_not_zero[termination_simp]: "⋀e ep cd st ad i xe val. 0 < (costs (EXTERNAL ad i xe val) ep e cd st)"
      and transfer_not_zero[termination_simp]: "⋀e ep cd st ex ad. 0 < (costs (TRANSFER ad ex) ep e cd st)"
begin

function msel::"bool ⇒ MTypes ⇒ Location ⇒ E list ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (Location * MTypes, Ex, State) state_monad"
     and ssel::"STypes ⇒ Location ⇒ E list ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (Location * STypes, Ex, State) state_monad"
     and lexp :: "L ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (LType * Type, Ex, State) state_monad"
     and expr::"E ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (Stackvalue * Type, Ex, State) state_monad"
     and load :: "bool ⇒ (Identifier × Type) list ⇒ E list ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ State ⇒ Environment ⇒ CalldataT ⇒ (Environment × CalldataT × State, Ex, State) state_monad"
     and rexp::"L ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (Stackvalue * Type, Ex, State) state_monad"
     and stmt :: "S ⇒ EnvironmentP ⇒ Environment ⇒ CalldataT ⇒ (unit, Ex, State) state_monad"
where
  "msel _ _ _ [] _ _ _ st = throw Err st"
| "msel _ (MTValue _) _ _ _ _ _ st = throw Err st"
| "msel _ (MTArray al t) loc [x] ep env cd st =
    (do {
      kv ← expr x ep env cd;
      (case kv of
        (KValue v, Value t') ⇒
          (if less t' (TUInt 256) v (ShowLint al) = Some (ShowLbool True, TBool)
            then return (hash loc v, t)
            else throw Err)
      | _ ⇒ throw Err)
    }) st"
(*
  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) ep env cd st =
    (do {
      kv ← expr x ep env cd;
      (case kv of
        (KValue v, Value t') ⇒
          (if less t' (TUInt 256) v (ShowLint al) = Some (ShowLbool True, TBool)
            then do {
              s ← applyf (λst. if mm then memory st else cd);
              (case accessStore (hash loc v) s of
                Some (MPointer l) ⇒ msel mm t l (y#ys) ep env cd
              | _ ⇒ throw Err)
            } else throw Err)
      | _ ⇒ throw Err)
    }) st"
| "ssel tp loc Nil _ _ _ st = return (loc, tp) st"
| "ssel (STValue _) _ (_ # _) _ _ _ st = throw Err st"
| "ssel (STArray al t) loc (x # xs) ep env cd st =
    (do {
      kv ← expr x ep env cd;
      (case kv of
        (KValue v, Value t') ⇒
          (if less t' (TUInt 256) v (ShowLint al) = Some (ShowLbool True, TBool)
            then ssel t (hash loc v) xs ep env cd
            else throw Err)
      | _ ⇒ throw Err)
    }) st"
| "ssel (STMap _ t) loc (x # xs) ep env cd st =
    (do {
      kv ← expr x ep env cd;
      (case kv of
        (KValue v, _) ⇒ ssel t (hash loc v) xs ep env cd
      | _ ⇒ throw Err)
    }) st"
| "lexp (Id i) _ e _ st =
    (case fmlookup (denvalue e) i of
      Some (tp, (Stackloc l)) ⇒ return (LStackloc l, tp)
    | Some (tp, (Storeloc l)) ⇒ return (LStoreloc l, tp)
    | _ ⇒ throw Err) st"
| "lexp (Ref i r) ep e cd st =
    (case fmlookup (denvalue e) i of
      Some (tp, Stackloc l) ⇒
        do {
          k ← applyf (λst. accessStore l (stack st));
          (case k of
            Some (KCDptr _) ⇒ throw Err
          | Some (KMemptr l') ⇒
            (case tp of
              Memory t ⇒
                do {
                  (l'', t') ← msel True t l' r ep e cd;
                  return (LMemloc l'', Memory t')
                }
            | _ ⇒ throw Err)
          | Some (KStoptr l') ⇒
            (case tp of
              Storage t ⇒
                do {
                  (l'', t') ← ssel t l' r ep e cd;
                  return (LStoreloc l'', Storage t')
                }
            | _ ⇒ throw Err)
          | Some (KValue _) ⇒ throw Err
          | None ⇒ throw Err)
        }
      | Some (tp, Storeloc l) ⇒
          (case tp of
            Storage t ⇒
              do {
                (l', t') ← ssel t l r ep e cd;
                return (LStoreloc l', Storage t')
              }
          | _ ⇒ throw Err)
      | None ⇒ throw Err) st"
| "expr (E.INT b x) ep e cd st =
    (do {
      gascheck (costse (E.INT b x) ep e cd);
      (if (b ∈ vbits)
        then (return (KValue (createSInt b x), Value (TSInt b)))
        else (throw Err))
    }) st"
| "expr (UINT b x) ep e cd st =
    (do {
      gascheck (costse (UINT b x) ep e cd);
      (if (b ∈ vbits)
        then (return (KValue (createUInt b x), Value (TUInt b)))
        else (throw Err))
  }) st"
| "expr (ADDRESS ad) ep e cd st =
    (do {
      gascheck (costse (ADDRESS ad) ep e cd);
      return (KValue ad, Value TAddr)
    }) st"
| "expr (BALANCE ad) ep e cd st =
    (do {
      gascheck (costse (BALANCE ad) ep e cd);
      kv ← expr ad ep e cd;
      (case kv of
        (KValue adv, Value TAddr) ⇒
          return (KValue (accessBalance (accounts st) adv), Value (TUInt 256))
      | _ ⇒ throw Err)
    }) st"
| "expr THIS ep e cd st =
    (do {
      gascheck (costse THIS ep e cd);
      return (KValue (address e), Value TAddr)
    }) st"
| "expr SENDER ep e cd st =
    (do {
      gascheck (costse SENDER ep e cd);
      return (KValue (sender e), Value TAddr)
    }) st"
| "expr VALUE ep e cd st =
    (do {
      gascheck (costse VALUE ep e cd);
      return (KValue (svalue e), Value (TUInt 256))
    }) st"
| "expr TRUE ep e cd st =
    (do {
      gascheck (costse TRUE ep e cd);
      return (KValue (ShowLbool True), Value TBool)
    }) st"
| "expr FALSE ep e cd st =
    (do {
      gascheck (costse FALSE ep e cd);
      return (KValue (ShowLbool False), Value TBool)
    }) st"
| "expr (NOT x) ep e cd st =
    (do {
      gascheck (costse (NOT x) ep e cd);
      kv ← expr x ep e cd;
      (case kv of
        (KValue v, Value t) ⇒
          (if v = ShowLbool True
            then expr FALSE ep e cd
            else (if v = ShowLbool False
              then expr TRUE ep e cd
              else throw Err))
      | _ ⇒ throw Err)
    }) st"
| "expr (PLUS e1 e2) ep e cd st = (gascheck (costse (PLUS e1 e2) ep e cd) ⤜ (λ_. lift expr add e1 e2 ep e cd)) st"
| "expr (MINUS e1 e2) ep e cd st = (gascheck (costse (MINUS e1 e2) ep e cd) ⤜ (λ_. lift expr sub e1 e2 ep e cd)) st"
| "expr (LESS e1 e2) ep e cd st = (gascheck (costse (LESS e1 e2) ep e cd) ⤜ (λ_. lift expr less e1 e2 ep e cd)) st"
| "expr (EQUAL e1 e2) ep e cd st = (gascheck (costse (EQUAL e1 e2) ep e cd) ⤜ (λ_. lift expr equal e1 e2 ep e cd)) st"
| "expr (AND e1 e2) ep e cd st = (gascheck (costse (AND e1 e2) ep e cd) ⤜ (λ_. lift expr vtand e1 e2 ep e cd)) st"
| "expr (OR e1 e2) ep e cd st = (gascheck (costse (OR e1 e2) ep e cd) ⤜ (λ_. lift expr vtor e1 e2 ep e cd)) st"
| "expr (LVAL i) ep e cd st =
    (do {
      gascheck (costse (LVAL i) ep e cd);
      rexp i ep e cd
    }) st"
(* 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

TODO: Functions with no return value should be able to execute
*)
| "expr (CALL i xe) ep e cd st =
    (do {
      gascheck (costse (CALL i xe) ep e cd);
      (case fmlookup ep (address e) of
         Some (ct, _) ⇒
           (case fmlookup ct i of
             Some (Method (fp, f, Some x)) ⇒
               let e' = ffold_init ct (emptyEnv (address e) (sender e) (svalue e)) (fmdom ct)
               in (do {
                 st' ← applyf (λst. st⦇stack:=emptyStore⦈);
                 (e'', cd', st'') ← load False fp xe ep e' emptyStore st' e cd;
                 st''' ← get;
                 put st'';
                 stmt f ep e'' cd';
                 rv ← expr x ep e'' cd';
                 modify (λst. st⦇stack:=stack st''', memory := memory st'''⦈);
                 return rv
               })
           | _ ⇒ throw Err)
       | None ⇒ throw Err)
    }) st"
| "expr (ECALL ad i xe val) ep e cd st =
    (do {
      gascheck (costse (ECALL ad i xe val) ep e cd);
      kad ← expr ad ep e cd;
      (case kad of
        (KValue adv, Value TAddr) ⇒
        (case fmlookup ep adv of
           Some (ct, _) ⇒
             (case fmlookup ct i of
               Some (Method (fp, f, Some x)) ⇒
               (do {
                 kv ← expr val ep e cd;
                 (case kv of
                   (KValue v, Value t) ⇒
                     let e' = ffold_init ct (emptyEnv adv (address e) v) (fmdom ct)
                     in (do {
                       st' ← applyf (λst. st⦇stack:=emptyStore, memory:=emptyStore⦈);
                       (e'', cd', st'') ← load True fp xe ep e' emptyStore st' e cd;
                       st''' ← get;
                       (case transfer (address e) adv v (accounts st'') of
                         Some acc ⇒
                           do {
                             put (st''⦇accounts := acc⦈);
                             stmt f ep e'' cd';
                             rv ← expr x ep e'' cd';
                             modify (λst. st⦇stack:=stack st''', memory := memory st'''⦈);
                             return rv
                          }
                       | None ⇒ throw Err)
                     })
                 | _ ⇒ throw Err)
               })
             | _ ⇒ throw Err)
        | None ⇒ throw Err)
      | _ ⇒ throw Err)
    }) st"
| "load cp ((ip, tp)#pl) (e#el) ep ev' cd' st' ev cd st =
    (do {
      (v, t) ← expr e ep ev cd;
      st'' ← get;
      put st';
      (cd'', ev'') ← decl ip tp (Some (v,t)) cp cd (memory st'') cd' ev';
      st''' ← get;
      put st'';
      load cp pl el ep ev'' cd'' st''' ev cd
    }) st"
| "load _ [] (_#_) _ _ _ _ _ _ st = throw Err st"
| "load _ (_#_) [] _ _ _ _ _ _ st = throw Err st"
| "load _ [] [] _ ev' cd' st' ev cd st = return (ev', cd', st') st"
(*TODO: Should be possible to simplify*)
| "rexp (Id i) ep e cd st =
    (case fmlookup (denvalue e) i of
      Some (tp, Stackloc l) ⇒
        do {
          s ← applyf (λst. accessStore l (stack st));
          (case s 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 (Storage (STValue t), Storeloc l) ⇒
      do {
        so ← applyf (λst. fmlookup (storage st) (address e));
        (case so of
          Some s ⇒ return (KValue (accessStorage t l s), Value t)
        | None ⇒ throw Err)
      }
    | Some (Storage (STArray x t), Storeloc l) ⇒ return (KStoptr l, Storage (STArray x t))
    | _ ⇒ throw Err) st"
| "rexp (Ref i r) ep e cd st =
    (case fmlookup (denvalue e) i of
      Some (tp, (Stackloc l)) ⇒
        do {
          kv ← applyf (λst. accessStore l (stack st));
          (case kv of
            Some (KCDptr l') ⇒
              (case tp of
                Calldata t ⇒
                  do {
                    (l'', t') ← msel False t l' r ep e cd;
                    (case t' of
                      MTValue t'' ⇒
                        (case accessStore l'' cd of
                          Some (MValue v) ⇒ return (KValue v, Value t'')
                        | _ ⇒ throw Err)
                    | MTArray x t'' ⇒
                        (case accessStore l'' cd of
                          Some (MPointer p) ⇒ return (KCDptr p, Calldata (MTArray x t''))
                        | _ ⇒ throw Err))
                  }
              | _ ⇒ throw Err)
          | Some (KMemptr l') ⇒
              (case tp of
                Memory t ⇒
                do {
                  (l'', t') ← msel True t l' r ep e cd;
                  (case t' of
                    MTValue t'' ⇒
                    do {
                      mv ← applyf (λst. accessStore l'' (memory st));
                      (case mv of
                        Some (MValue v) ⇒ return (KValue v, Value t'')
                      | _ ⇒ throw Err)
                    }
                  | MTArray x t'' ⇒
                    do {
                      mv ← applyf (λst. accessStore l'' (memory st));
                      (case mv of
                        Some (MPointer p) ⇒ return (KMemptr p, Memory (MTArray x t''))
                      | _ ⇒ throw Err)
                    }
                  )
                }
              | _ ⇒ throw Err)
          | Some (KStoptr l') ⇒
              (case tp of
                Storage t ⇒
                do {
                  (l'', t') ← ssel t l' r ep e cd;
                  (case t' of
                    STValue t'' ⇒
                      do {
                        so ← applyf (λst. fmlookup (storage st) (address e));
                        (case so of
                          Some s ⇒ return (KValue (accessStorage t'' l'' s), Value t'')
                        | None ⇒ throw Err)
                      }
                  | STArray _ _ ⇒ return (KStoptr l'', Storage t')
                  | STMap _ _ ⇒ return (KStoptr l'', Storage t'))
                }
              | _ ⇒ throw Err)
          | _ ⇒ throw Err)
        }
    | Some (tp, (Storeloc l)) ⇒
        (case tp of
          Storage t ⇒
          do {
            (l', t') ← ssel t l r ep e cd;
            (case t' of
              STValue t'' ⇒
                do {
                  so ← applyf (λst. fmlookup (storage st) (address e));
                  (case so of
                    Some s ⇒ return (KValue (accessStorage t'' l' s), Value t'')
                  | None ⇒ throw Err)
                }
            | STArray _ _ ⇒ return (KStoptr l', Storage t')
            | STMap _ _ ⇒ return (KStoptr l', Storage t'))
          }
        | _ ⇒ throw Err)
    | None ⇒ throw Err) st"
| "stmt SKIP ep e cd st = gascheck (costs SKIP ep e cd) st"
| "stmt (ASSIGN lv ex) ep env cd st =
    (do {
      gascheck (costs (ASSIGN lv ex) ep env cd);
      re ← expr ex ep env cd;
      (case re of
        (KValue v, Value t) ⇒
          do {
            rl ← lexp lv ep env cd;
            (case rl of
              (LStackloc l, Value t') ⇒ 
                (case convert t t' v of
                   Some (v', _) ⇒ modify (λst. st ⦇stack := updateStore l (KValue v') (stack st)⦈)
                 | None ⇒ throw Err)
            | (LStoreloc l, Storage (STValue t')) ⇒
                (case convert t t' v of
                  Some (v', _) ⇒
                    do {
                      so ← applyf (λst. fmlookup (storage st) (address env));
                      (case so of
                        Some s ⇒ modify (λst. st⦇storage := fmupd (address env) (fmupd l v' s) (storage st)⦈)
                      | None ⇒ throw Err)
                  }
                | None ⇒ throw Err)
            | (LMemloc l, Memory (MTValue t')) ⇒
                (case convert t t' v of
                  Some (v', _) ⇒ modify (λst. st⦇memory := updateStore l (MValue v') (memory st)⦈)
                | None ⇒ throw Err)
            | _ ⇒ throw Err)
          }
        | (KCDptr p, Calldata (MTArray x t)) ⇒
          do {
            rl ← lexp lv ep env cd;
            (case rl of
              (LStackloc l, Memory _) ⇒ modify (λst. st ⦇stack := updateStore l (KCDptr p) (stack st)⦈)
            | (LStackloc l, Storage _) ⇒
                do {
                  sv ← applyf (λst. accessStore l (stack st));
                  (case sv of
                    Some (KStoptr p') ⇒
                      do {
                        so ← applyf (λst. fmlookup (storage st) (address env));
                        (case so of
                          Some s ⇒ 
                            (case cpm2s p p' x t cd s of
                              Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
                            | None ⇒ throw Err)
                        | None ⇒ throw Err)
                    }
                  | _ ⇒ throw Err)
                }
             | (LStoreloc l, _) ⇒
                do {
                  so ← applyf (λst. fmlookup (storage st) (address env));
                  (case so of
                    Some s ⇒ 
                      (case cpm2s p l x t cd s of
                         Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
                       | None ⇒ throw Err)
                  | None ⇒ throw Err)
                }
             | (LMemloc l, _) ⇒
                do {
                  cs ← applyf (λst. cpm2m p l x t cd (memory st));
                  (case cs of
                    Some m ⇒ modify (λst. st ⦇memory := m⦈)
                  | None ⇒ throw Err)
                }
             | _ ⇒ throw Err)
          }
        | (KMemptr p, Memory (MTArray x t)) ⇒
            do {
              rl ← lexp lv ep env cd;
              (case rl of
                (LStackloc l, Memory _) ⇒ modify (λst. st⦇stack := updateStore l (KMemptr p) (stack st)⦈)
              | (LStackloc l, Storage _) ⇒
                  do {
                    sv ← applyf (λst. accessStore l (stack st));
                    (case sv of
                      Some (KStoptr p') ⇒
                      do {
                        so ← applyf (λst. fmlookup (storage st) (address env));
                        (case so of
                          Some s ⇒ 
                            do {
                              cs ← applyf (λst. cpm2s p p' x t (memory st) s);
                              (case cs of
                              Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
                            | None ⇒ throw Err)
                            }
                        | None ⇒ throw Err)
                      }
                    | _ ⇒ throw Err)
                  }
              | (LStoreloc l, _) ⇒
                  do {
                    so ← applyf (λst. fmlookup (storage st) (address env));
                    (case so of
                      Some s ⇒ 
                        do {
                          cs ← applyf (λst. cpm2s p l x t (memory st) s);
                          (case cs of
                            Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
                          | None ⇒ throw Err)
                        }
                    | None ⇒ throw Err)
                  }
              | (LMemloc l, _) ⇒ modify (λst. st ⦇memory := updateStore l (MPointer p) (memory st)⦈)
              | _ ⇒ throw Err)
            }
        | (KStoptr p, Storage (STArray x t)) ⇒
            do {
              rl ← lexp lv ep env cd;
              (case rl of
                (LStackloc l, Memory _) ⇒
                  do {
                    sv ← applyf (λst. accessStore l (stack st));
                    (case sv of
                      Some (KMemptr p') ⇒
                        do {
                          so ← applyf (λst. fmlookup (storage st) (address env));
                          (case so of
                            Some s ⇒ 
                              do {
                                cs ← applyf (λst. cps2m p p' x t s (memory st));
                                (case cs of
                                  Some m ⇒ modify (λst. st⦇memory := m⦈)
                                | None ⇒ throw Err)
                              }
                          | None ⇒ throw Err)
                        }
                    | _ ⇒ throw Err)
                  }
              | (LStackloc l, Storage _) ⇒ modify (λst. st⦇stack := updateStore l (KStoptr p) (stack st)⦈)
              | (LStoreloc l, _) ⇒
                  do {
                    so ← applyf (λst. fmlookup (storage st) (address env));
                    (case so of
                      Some s ⇒ 
                        (case copy p l x t s of
                          Some s' ⇒ modify (λst. st ⦇storage := fmupd (address env) s' (storage st)⦈)
                        | None ⇒ throw Err)
                     | None ⇒ throw Err)
                  }
              | (LMemloc l, _) ⇒
                  do {
                    so ← applyf (λst. fmlookup (storage st) (address env));
                    (case so of
                      Some s ⇒ 
                        do {
                          cs ← applyf (λst. cps2m p l x t s (memory st));
                          (case cs of
                            Some m ⇒ modify (λst. st⦇memory := m⦈)
                          | None ⇒ throw Err)
                        }
                    | None ⇒ throw Err)
                  }
              | _ ⇒ throw Err)
            }
        | (KStoptr p, Storage (STMap t t')) ⇒
            do {
              rl ← lexp lv ep env cd;
              (case rl of
                (LStackloc l, _) ⇒ modify (λst. st⦇stack := updateStore l (KStoptr p) (stack st)⦈)
              | _ ⇒ throw Err)
            }
        | _ ⇒ throw Err)
    }) st"
| "stmt (COMP s1 s2) ep e cd st =
    (do {
      gascheck (costs (COMP s1 s2) ep e cd);
      stmt s1 ep e cd;
      stmt s2 ep e cd
    }) st"
| "stmt (ITE ex s1 s2) ep e cd st =
    (do {
      gascheck (costs (ITE ex s1 s2)  ep e cd);
      v ← expr ex ep e cd;
      (case v of
        (KValue b, Value TBool) ⇒
            (if b = ShowLbool True
              then stmt s1 ep e cd
              else stmt s2 ep e cd)
      | _ ⇒ throw Err)
    }) st"
| "stmt (WHILE ex s0) ep e cd st =
    (do {
      gascheck (costs (WHILE ex s0) ep e cd);
      v ← expr ex ep e cd;
      (case v of
        (KValue b, Value TBool) ⇒
          (if b = ShowLbool True
            then do {
              stmt s0 ep e cd;
              stmt (WHILE ex s0) ep e cd
            }
            else return ())
      | _ ⇒ throw Err)
    }) st"
| "stmt (INVOKE i xe) ep e cd st =
    (do {
      gascheck (costs (INVOKE i xe) ep e cd);
      (case fmlookup ep (address e) of
          Some (ct, _) ⇒
            (case fmlookup ct i of
              Some (Method (fp, f, None)) ⇒
                 (let e' = ffold_init ct (emptyEnv (address e) (sender e) (svalue e)) (fmdom ct)
                 in (do {
                    st' ← applyf (λst. (st⦇stack:=emptyStore⦈));
                    (e'', cd', st'') ← load False fp xe ep e' emptyStore st' e cd;
                    st''' ← get;
                    put st'';
                    stmt f ep e'' cd';
                    modify (λst. st⦇stack:=stack st''', memory := memory st'''⦈)
                  }))
            | _ ⇒ throw Err)
        | None  ⇒ throw Err)
    }) st"
(*External Method calls allow to send some money val with it*)
(*However this transfer does NOT trigger a fallback*)
| "stmt (EXTERNAL ad i xe val) ep e cd st =
    (do {
      gascheck (costs (EXTERNAL ad i xe val) ep e cd);
      kad ← expr ad ep e cd;
      (case kad of
        (KValue adv, Value TAddr) ⇒
          (case fmlookup ep adv of
            Some (ct, fb) ⇒
              (do {
                kv ← expr val ep e cd;
                (case kv of
                  (KValue v, Value t) ⇒
                    (case fmlookup ct i of
                      Some (Method (fp, f, None)) ⇒
                      let e' = ffold_init ct (emptyEnv adv (address e) v) (fmdom ct)
                      in (do {
                        st' ← applyf (λst. st⦇stack:=emptyStore, memory:=emptyStore⦈);
                        (e'', cd', st'') ← load True fp xe ep e' emptyStore st' e cd;
                        st''' ← get;
                        (case transfer (address e) adv v (accounts st'') of
                          Some acc ⇒
                            do {
                              put (st''⦇accounts := acc⦈);
                              stmt f ep e'' cd';
                              modify (λst. st⦇stack:=stack st''', memory := memory st'''⦈)
                            }
                          | None ⇒ throw Err)
                       })
                    | None ⇒
                      do {
                        st' ← get;
                        (case transfer (address e) adv v (accounts st') of
                          Some acc ⇒
                            do {
                              st'' ← get;
                              modify (λst. st⦇accounts := acc,stack:=emptyStore, memory:=emptyStore⦈);
                              stmt fb ep (emptyEnv adv (address e) v) cd;
                              modify (λst. st⦇stack:=stack st'', memory := memory st''⦈)
                            }
                        | None ⇒ throw Err)
                      }
                    | _ ⇒ throw Err)
                | _ ⇒ throw Err)
              })
          | None ⇒ throw Err)
      | _ ⇒ throw Err)
    }) st"
| "stmt (TRANSFER ad ex) ep e cd st =
    (do {
      gascheck (costs (TRANSFER ad ex) ep e cd);
      kv ← expr ex ep e cd;
      (case kv of
        (KValue v, Value t) ⇒
          (do {
            kv' ← expr ad ep e cd;
            (case kv' of
              (KValue adv, Value TAddr) ⇒
                (do {
                  acs ← applyf accounts;
                  (case transfer (address e) adv v acs of
                    Some acc ⇒ (case fmlookup ep adv of
                                  Some (ct, f) ⇒
                                    let e' = ffold_init ct (emptyEnv adv (address e) v) (fmdom ct)
                                    in (do {
                                      st' ← get;
                                      modify (λst. (st⦇accounts := acc, stack:=emptyStore, memory:=emptyStore⦈));
                                      stmt f ep e' emptyStore;
                                      modify (λst. st⦇stack:=stack st', memory := memory st'⦈)
                                    })
                                | None ⇒ modify (λst. (st⦇accounts := acc⦈)))
                  | None ⇒ throw Err)
                })
            | _ ⇒ throw Err)
          })
      | _ ⇒ throw Err)
    }) st"
| "stmt (BLOCK ((id0, tp), ex) s) ep ev cd st =
    (do {
      gascheck (costs (BLOCK ((id0, tp), ex) s) ep ev cd);
      (case ex of
         None ⇒ (do {
           mem ← applyf memory;
           (cd', e') ← decl id0 tp None False cd mem cd ev;
           stmt s ep e' cd'
         })
       | Some ex' ⇒ (do {
           (v, t) ← expr ex' ep ev cd;
           mem ← applyf memory;
           (cd', e') ← decl id0 tp (Some (v, t)) False cd mem cd ev;
           stmt s ep e' cd'
         }))
    }) st"
  by pat_completeness auto

subsection ‹Gas Consumption›

lemma lift_gas:
  assumes "lift expr f e1 e2 ep e cd st = Normal ((v, t), st4')"
      and "⋀st4' v4 t4. expr e1 ep e cd st = Normal ((v4, t4), st4') ⟹ gas st4' ≤ gas st"
      and "⋀x1 x y xa ya x1a x1b st4' v4 t4. expr e1 ep e cd st = Normal (x, y)
            ⟹ (xa, ya) = x
            ⟹ xa = KValue x1a
            ⟹ ya = Value x1b
            ⟹ expr e2 ep e cd y = Normal ((v4, t4), st4')
          ⟹ gas st4' ≤ gas y"
      shows "gas st4' ≤ gas st"
proof (cases "expr e1 ep e cd st")
  case (n a st')
  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 ep e cd st'")
          case r2: (n a' st'')
          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 "gas st4'≤gas st''" by simp
                    moreover from assms n Pair KValue Value r2 p2 v2 t2 Some have "gas st''≤gas st'" by simp
                    moreover from assms n Pair KValue Value r2 p2 v2 t2 Some have "gas st'≤gas st" by simp
                    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_lexp_expr_load_rexp_stmt_dom_gas:
    "msel_ssel_lexp_expr_load_rexp_stmt_dom (Inl (Inl (c1, t1, l1, xe1, ep1, ev1, cd1, st1)))
      ⟹ (∀l1' t1' st1'. msel c1 t1 l1 xe1 ep1 ev1 cd1 st1 = Normal ((l1', t1'), st1') ⟶ gas st1' ≤ gas st1)"
    "msel_ssel_lexp_expr_load_rexp_stmt_dom (Inl (Inr (Inl (t2, l2, xe2, ep2, ev2, cd2, st2))))
      ⟹ (∀l2' t2' st2'. ssel t2 l2 xe2 ep2 ev2 cd2 st2 = Normal ((l2', t2'), st2') ⟶ gas st2' ≤ gas st2)"
    "msel_ssel_lexp_expr_load_rexp_stmt_dom (Inl (Inr (Inr (l5, ep5, ev5, cd5, st5))))
      ⟹ (∀l5' t5' st5'. lexp l5 ep5 ev5 cd5 st5 = Normal ((l5', t5'), st5') ⟶ gas st5' ≤ gas st5)"
    "msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (e4, ep4, ev4, cd4, st4))))
      ⟹ (∀st4' v4 t4. expr e4 ep4 ev4 cd4 st4 = Normal ((v4, t4), st4') ⟶ gas st4' ≤ gas st4)"
    "msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inr (lcp, lis, lxs, lep, lev0, lcd0, lst0, lev, lcd, lst))))
      ⟹ (∀ev cd st st'. load lcp lis lxs lep lev0 lcd0 lst0 lev lcd lst = Normal ((ev, cd, st), st') ⟶ gas st ≤ gas