Theory Weakest_Precondition

theory Weakest_Precondition
  imports Solidity_Main
begin

section ‹Setup for Monad VCG›

lemma wpstackvalue[wprule]:
  assumes "⋀v. a = KValue v ⟹ wp (f v) P E s"
      and "⋀p. a = KCDptr p ⟹ wp (g p) P E s"
      and "⋀p. a = KMemptr p ⟹ wp (h p) P E s"
      and "⋀p. a = KStoptr p ⟹ wp (i p) P E s"
    shows "wp (case a of KValue v ⇒ f v | KCDptr p ⇒ g p | KMemptr p ⇒ h p | KStoptr p ⇒ i p) P E s"
using assms by (simp add: stackvalue.split[of "λx. wp x P E s"])

lemma wpmtypes[wprule]:
  assumes "⋀i m. a = MTArray i m ⟹ wp (f i m) P E s"
      and "⋀t. a = MTValue t ⟹ wp (g t) P E s"
    shows "wp (case a of MTArray i m ⇒ f i m | MTValue t ⇒ g t) P E s"
using assms by (simp add: mtypes.split[of "λx. wp x P E s"])

lemma wpstypes[wprule]:
  assumes "⋀i m. a = STArray i m ⟹ wp (f i m) P E s"
      and "⋀t t'. a = STMap t t' ⟹ wp (g t t') P E s"
      and "⋀t. a = STValue t ⟹ wp (h t) P E s"
shows "wp (case a of STArray i m ⇒ f i m | STMap t t' ⇒ g t t' | STValue t ⇒ h t) P E s"
using assms by (simp add: stypes.split[of "λx. wp x P E s"])

lemma wptype[wprule]:
  assumes "⋀v. a = Value v ⟹ wp (f v) P E s"
      and "⋀m. a = Calldata m ⟹ wp (g m) P E s"
      and "⋀m. a = type.Memory m ⟹ wp (h m) P E s"
      and "⋀t. a = type.Storage t ⟹ wp (i t) P E s"
shows "wp (case a of Value v ⇒ f v | Calldata m ⇒ g m | type.Memory m ⇒ h m | type.Storage s ⇒ i s) P E s"
  using assms by (simp add: type.split[of "λx. wp x P E s"])

lemma wptypes[wprule]:
assumes "⋀x. a= TSInt x ⟹ wp (f x) P E s"
    and "⋀x. a = TUInt x ⟹ wp (g x) P E s"
    and "a = TBool ⟹ wp h P E s"
    and "a = TAddr ⟹ wp i P E s"
  shows "wp (case a of TSInt x ⇒ f x | TUInt x ⇒ g x | TBool ⇒ h | TAddr ⇒ i) P E s"
using assms by (simp add: types.split[of "λx. wp x P E s"])

lemma wpltype[wprule]:
  assumes "⋀l. a=LStackloc l ⟹ wp (f l) P E s"
      and "⋀l. a = LMemloc l ⟹ wp (g l) P E s"
      and "⋀l. a = LStoreloc l ⟹ wp (h l) P E s"
    shows "wp (case a of LStackloc l ⇒ f l | LMemloc l ⇒ g l | LStoreloc l ⇒ h l) P E s"
using assms by (simp add: ltype.split[of "λx. wp x P E s"])

lemma wpdenvalue[wprule]:
  assumes "⋀l. a=Stackloc l ⟹ wp (f l) P E s"
      and "⋀l. a=Storeloc l ⟹ wp (g l) P E s"
    shows "wp (case a of Stackloc l ⇒ f l | Storeloc l ⇒ g l) P E s"
  using assms by (simp add:denvalue.split[of "λx. wp x P E s" f g a])

section ‹Calculus›

subsection ‹Hoare Triples›

context statement_with_gas
begin

type_synonym state_predicate = "accounts × stack × memoryT × (address ⇒ storageT) ⇒ bool"

definition validS :: "state_predicate ⇒ s ⇒ state_predicate ⇒ (ex ⇒ bool) ⇒ bool" 
  ("⦃_⦄⇩S/ _ /(⦃_⦄⇩S,/ ⦃_⦄⇩S)")
where
  "⦃P⦄⇩S s ⦃Q⦄⇩S,⦃E⦄⇩S ≡
     ∀st. P (Accounts st, Stack st, Memory st, Storage st)
     ⟶ (∀ev cd. case stmt s ev cd st of
           Normal (_,st') ⇒ Q (Accounts st', Stack st', Memory st', Storage st')
         | Exception e ⇒ E e)"

definition wpS :: "s ⇒ (state ⇒ bool) ⇒ (ex ⇒ bool) ⇒ environment ⇒ calldataT ⇒ state ⇒ bool"
  where "wpS s P E ev cd st ≡ wp (λst. stmt s ev cd st) (λ_. P) E st"

lemma wpS_valid:
  assumes "⋀ev cd (st::state). P (Accounts st, Stack st, Memory st, Storage st) ⟹ wpS s (λst. Q (Accounts st, Stack st, Memory st, Storage st)) E ev cd st"
  shows "⦃P⦄⇩S s ⦃Q⦄⇩S,⦃E⦄⇩S"
  unfolding validS_def
  using assms unfolding wpS_def wp_def by simp

lemma valid_wpS:
  assumes "⦃P⦄⇩S s ⦃Q⦄⇩S,⦃E⦄⇩S"
  shows "⋀ev cd st. P (Accounts st, Stack st, Memory st, Storage st) ⟹ wpS s (λst. Q (Accounts st, Stack st, Memory st, Storage st)) E ev cd st"
  unfolding wpS_def wp_def using assms unfolding validS_def by simp

subsection ‹Skip›

lemma wp_Skip:
  assumes "P (st⦇Gas := state.Gas st - costs SKIP ev cd st⦈)"
      and "E Gas"
    shows "wpS SKIP P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(1))
  apply wp
  using assms by simp+

subsection ‹Assign›

lemma wp_Assign1:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KValue rx ∧ is_LStackloc lx"
      and "⋀v t g l t' g' v'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KValue v,Value t), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStackloc l, Value t'), g');
            convert t t' v = Some v'⟧
          ⟹ P (st⦇Gas := g', Stack:=updateStore l (KValue v') (Stack st)⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign2:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KValue rx ∧ is_LStoreloc lx"
      and "⋀v t g l t' g' v'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KValue v,Value t), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStoreloc l, type.Storage (STValue t')), g');
            convert t t' v = Some v'⟧
          ⟹ P (st⦇Gas := g', Storage:=(Storage st) (Address ev := (fmupd l v' (Storage st (Address ev))))⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign3:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KValue rx ∧ is_LMemloc lx"
      and "⋀v t g l t' g' v'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KValue v, Value t), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LMemloc l, type.Memory (MTValue t')), g');
            convert t t' v = Some v'⟧
          ⟹ P (st⦇Gas := g', Memory:=updateStore l (MValue v') (Memory st)⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign4:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KCDptr rx ∧ is_LStackloc lx ∧ is_Memory ly"
      and "⋀p x t g l t' g' p' m' sv'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KCDptr p, Calldata (MTArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStackloc l, type.Memory t'), g');
            t' = MTArray x t;
            accessStore l (state.Stack st) = Some (KMemptr p');
            sv' = updateStore l (KMemptr (ShowL⇩n⇩a⇩t (Toploc (state.Memory st)))) (state.Stack st);
            cpm2m p (ShowL⇩n⇩a⇩t (Toploc (state.Memory st))) x t cd (snd (allocate(state.Memory st))) = Some m'⟧
          ⟹ P (st⦇Gas := g', Memory := m', Stack := sv'⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign5:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KCDptr rx ∧ is_LStackloc lx ∧ is_Storage ly"
      and "⋀p x t g l t' g' p' s'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KCDptr p, Calldata (MTArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStackloc l, type.Storage t'), g');
            accessStore l (Stack st) = Some (KStoptr p');
            cpm2s p p' x t cd (Storage st (Address ev)) = Some s'⟧
          ⟹ P (st⦇Gas := g', Storage:=(Storage st) (Address ev := s')⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign6:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KCDptr rx ∧ is_LStoreloc lx"
      and "⋀p x t g l t' g' s'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KCDptr p, Calldata (MTArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStoreloc l, t'), g');
            cpm2s p l x t cd (Storage st (Address ev)) = Some s'⟧
          ⟹ P (st⦇Gas := g', Storage:=(Storage st) (Address ev := s')⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign7:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KCDptr rx ∧ is_LMemloc lx"
      and "⋀p x t g l t' g' m m'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KCDptr p, Calldata (MTArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LMemloc l, type.Memory t'), g');
            t' = MTArray x t;
            cpm2m p (ShowL⇩n⇩a⇩t (Toploc (state.Memory st))) x t cd (snd (allocate(state.Memory st))) = Some m;
            m' = updateStore l (MPointer (ShowL⇩n⇩a⇩t (Toploc (state.Memory st)))) m⟧
          ⟹ P (st⦇Gas := g', Memory := m'⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign8:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KMemptr rx ∧ is_LStackloc lx ∧ is_Memory ly"
      and "⋀p x t g l t' g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KMemptr p, type.Memory (MTArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStackloc l, type.Memory t'), g')⟧
          ⟹ P (st⦇Gas := g', Stack:=updateStore l (KMemptr p) (Stack st)⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign9:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KMemptr rx ∧ is_LStackloc lx ∧ is_Storage ly"
      and "⋀p x t g l t' g' p' s'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KMemptr p, type.Memory (MTArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStackloc l, type.Storage t'), g');
            accessStore l (Stack st) = Some (KStoptr p');
            cpm2s p p' x t (Memory st) (Storage st (Address ev)) = Some s'⟧
          ⟹ P (st⦇Gas := g', Storage:=(Storage st) (Address ev := s')⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign10:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KMemptr rx ∧ is_LStoreloc lx"
      and "⋀p x t g l t' g' s'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KMemptr p, type.Memory (MTArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStoreloc l, t'), g');
            cpm2s p l x t (Memory st) (Storage st (Address ev)) = Some s'⟧
          ⟹ P (st⦇Gas := g', Storage:=(Storage st) (Address ev := s')⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign11:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KMemptr rx ∧ is_LMemloc lx"
      and "⋀p x t g l t' g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KMemptr p, type.Memory (MTArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LMemloc l, t'), g')⟧
          ⟹ P (st⦇Gas := g', Memory:=updateStore l (MPointer p) (Memory st)⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign12:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KStoptr rx ∧ (∃rt. ry = type.Storage rt ∧ is_STArray rt) ∧ is_LStackloc lx ∧ is_Memory ly"
      and "⋀p x t g l t' g' p' m sv'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KStoptr p, type.Storage (STArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStackloc l, type.Memory t'), g');
            cps2mTypeCompatible (STArray x t) t';
            accessStore l (state.Stack st) = Some (KMemptr p');
            sv' = updateStore l (KMemptr (ShowL⇩n⇩a⇩t (Toploc (state.Memory st)))) (state.Stack st);
            cps2m p (ShowL⇩n⇩a⇩t (Toploc (state.Memory st))) x t (state.Storage st (Address ev)) (snd (allocate(state.Memory st))) = Some m⟧
          ⟹ P (st⦇Gas := g', Memory := m, Stack := sv'⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign13:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KStoptr rx ∧ (∃rt. ry = type.Storage rt ∧ is_STArray rt) ∧ is_LStackloc lx ∧ is_Storage ly"
      and "⋀p x t g l t' g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KStoptr p, type.Storage (STArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStackloc l, type.Storage t'), g')⟧
          ⟹ P (st⦇Gas := g', Stack:=updateStore l (KStoptr p) (Stack st)⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign14:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KStoptr rx ∧ is_LStoreloc lx"
      and "⋀p x t g l t' g' s'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KStoptr p, type.Storage (STArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStoreloc l, t'), g');
            copy p l x t (Storage st (Address ev)) = Some s'⟧
          ⟹ P (st⦇Gas := g', Storage:=(Storage st) (Address ev := s')⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign15:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KStoptr rx ∧ is_LMemloc lx"
      and "⋀p x t g l t' g' m m'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KStoptr p, type.Storage (STArray x t)), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LMemloc l, type.Memory t'), g');
            cps2mTypeCompatible (STArray x t) t';
            cps2m p (ShowL⇩n⇩a⇩t (Toploc (state.Memory st))) x t (state.Storage st (Address ev)) (snd (allocate(state.Memory st))) = Some m;
            m' = updateStore l (MPointer (ShowL⇩n⇩a⇩t (Toploc (state.Memory st)))) m⟧
          ⟹ P (st⦇Gas := g', Memory := m'⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

lemma wp_Assign16:
  fixes ex ev cd st lv
  defines "ngas ≡ state.Gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀rx ry g lx ly g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((lx,ly), g')⟧
          ⟹ is_KStoptr rx ∧ (∃rt. ry = type.Storage rt ∧ is_STMap rt) ∧ is_LStackloc lx"
      and "⋀p t t' g l t'' g'.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((KStoptr p, type.Storage (STMap t t')), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Normal ((LStackloc l, t''), g')⟧
          ⟹ P (st⦇Gas := g', Stack:=updateStore l (KStoptr p) (Stack st)⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := ngas⦈) ngas = Exception e ⟹ E e"
      and "⋀rx ry g e.
            ⟦expr ex ev cd (st⦇Gas := ngas⦈) ngas = Normal ((rx,ry), g);
            lexp lv ev cd (st⦇Gas := g⦈) g = Exception e⟧
          ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "wpS (ASSIGN lv ex) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(2))
  apply wp
  using assms unfolding ngas_def by fastforce+

subsection ‹Composition›

lemma wp_Comp:
  assumes "wpS s1 (wpS s2 P E ev cd) E ev cd (st⦇Gas := state.Gas st - costs (COMP s1 s2) ev cd st⦈)"
      and "E Gas"
    shows "wpS (COMP s1 s2) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(3))
  apply wp
  using assms unfolding wpS_def wp_def by simp_all

subsection ‹Conditional›

lemma wp_ITE:
  fixes ex s1 s2 ev cd st
  defines "nGas ≡ state.Gas st - costs (ITE ex s1 s2) ev cd st"
  assumes "⋀g. expr ex ev cd (st⦇Gas := nGas⦈) nGas = Normal ((KValue ⌈True⌉, Value TBool), g) ⟹ wpS s1 P E ev cd (st⦇Gas := g⦈)"
      and "⋀g. expr ex ev cd (st⦇Gas := nGas⦈) nGas = Normal ((KValue ⌈False⌉, Value TBool), g) ⟹ wpS s2 P E ev cd (st⦇Gas := g⦈)"
      and "⋀e. expr ex ev cd (st⦇Gas := nGas⦈) nGas = Exception e ⟹ E e"
      and "E Gas"
      and "E Err"
    shows "wpS (ITE ex s1 s2) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(4))
  apply wp
  using assms unfolding wpS_def by (simp_all)

subsection ‹While Loop›

lemma wp_While[rule_format]:
    fixes iv::"accounts × stack × memoryT × (address ⇒ storageT) ⇒ bool"
      and ex sm ev cd
  defines "nGas st ≡ state.Gas st - costs (WHILE ex sm) ev cd st"
  assumes "⋀st g. ⟦iv (Accounts st, Stack st, Memory st, Storage st); expr ex ev cd (st⦇Gas := nGas st⦈) (nGas st) = Normal ((KValue ⌈False⌉, Value TBool), g)⟧ ⟹ P (st⦇Gas := g⦈)"
      and "⋀st g. ⟦iv (Accounts st, Stack st, Memory st, Storage st); expr ex ev cd (st⦇Gas := nGas st⦈) (nGas st) = Normal ((KValue ⌈True⌉, Value TBool), g)⟧ ⟹ wpS sm (λst. iv (Accounts st, Stack st, Memory st, Storage st)) E ev cd (st⦇Gas:=g⦈)"
      and "⋀st e. ⟦expr ex ev cd (st⦇Gas := nGas st⦈) (nGas st) = Exception e⟧ ⟹ E e"
      and "⋀st e. stmt sm ev cd st = Exception e ⟹ E e"
      and "E Err"
      and "E Gas"
    shows "iv (Accounts st, Stack st, Memory st, Storage st) ⟶ wpS (WHILE ex sm) P E ev cd st"
proof (induction st rule:gas_induct)
  case (1 st)
  show ?case
  unfolding wpS_def wp_def
  proof (split result.split, rule conjI; rule allI; rule impI)
    fix x1 assume *: "local.stmt (WHILE ex sm) ev cd st = Normal x1"
    then obtain b g where **: "expr ex ev cd (st⦇Gas := state.Gas st - costs (WHILE ex sm) ev cd st⦈) (state.Gas st - costs (WHILE ex sm) ev cd st) = Normal ((KValue b, Value TBool), g)" by (simp only: stmt.simps, simp split:if_split_asm result.split_asm prod.split_asm stackvalue.split_asm type.split_asm types.split_asm)
    with * consider (t) "b = ShowL⇩b⇩o⇩o⇩l True" | (f) "b = ShowL⇩b⇩o⇩o⇩l False" by (simp add:stmt.simps split:if_split_asm result.split_asm prod.split_asm stackvalue.split_asm type.split_asm types.split_asm)
    then show "iv (Accounts st, Stack st, Memory st, Storage st) ⟶ (case x1 of (r, s') ⇒ P s')"
    proof cases
      case t
      then obtain st' where ***: "stmt sm ev cd (st⦇Gas := g⦈) = Normal ((), st')" using * ** by (auto simp add:stmt.simps split:if_split_asm result.split_asm)
      then have ****: "local.stmt (WHILE ex sm) ev cd st' = Normal x1" using * ** t by (simp add:stmt.simps split:if_split_asm)
      show ?thesis
      proof
        assume "iv (Accounts st, Stack st, Memory st, Storage st)"
        then have "wpS sm (λst. iv (Accounts st, Stack st, Memory st, Storage st)) E ev cd (st⦇Gas:=g⦈)" using nGas_def assms(3) ** t by auto
        then have "iv (Accounts st', Stack st', Memory st', Storage st')" unfolding wpS_def wp_def using *** by (simp split:result.split_asm)+
        moreover have "state.Gas st ≥ costs (WHILE ex sm) ev cd st" using * by (simp add:stmt.simps split:if_split_asm)
        then have "state.Gas st' < state.Gas st" using stmt_gas[OF ***] msel_ssel_expr_load_rexp_gas(3)[OF **] while_not_zero[of ex sm ev cd st] by simp
        ultimately have "wpS (WHILE ex sm) P E ev cd st'" using 1 by simp
        then show "(case x1 of (r, s') ⇒ P s')" unfolding wpS_def wp_def using **** `state.Gas st' < state.Gas st` by auto
      qed
    next
      case f
      show ?thesis
      proof
        assume "iv (Accounts st, Stack st, Memory st, Storage st)"
        then have "P (st⦇Gas := g⦈)" using ** nGas_def assms(2) f by simp
        moreover have "x1 = ((),st⦇Gas := g⦈)" using * ** f by (simp add:stmt.simps true_neq_false[symmetric] split:if_split_asm)
        moreover have "g ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF **] by simp
        ultimately show "case x1 of (r, s') ⇒ P s'" by (auto split:prod.split)
      qed
    qed
  next
    fix e
    assume 0: "local.stmt (WHILE ex sm) ev cd st = Exception e"
    then show "iv (Accounts st, Stack st, Memory st, Storage st) ⟶ E e"
    proof (cases rule: whileE)
      case Gas
      then show ?thesis using assms(7) by simp
    next
      case Err
      then show ?thesis using assms(6) by simp
    next
      case Exp
      then show ?thesis using assms(4) nGas_def by simp
    next
      case (Stm g)
      then show ?thesis using assms(5) by auto
    next
      case (While g st')
      show ?thesis
      proof
        assume *: "iv (Accounts st, Stack st, state.Memory st, state.Storage st)"
        then have "iv (Accounts st', Stack st', state.Memory st', state.Storage st')" using assms(3)[OF *] unfolding wpS_def wp_def by (simp add:While(2,3) nGas_def split:result.split_asm prod.split_asm)
        moreover have "state.Gas st' < state.Gas st" using nGas_def[of st] while_not_zero[of ex sm ev cd st] stmt_gas[OF While(3)] msel_ssel_expr_load_rexp_gas(3)[OF While(2)] While(1) by simp
        ultimately have "wpS (WHILE ex sm) P E ev cd st'" using 1 by simp
        then show "E e" unfolding wpS_def wp_def by (simp add: While(4) split: result.split_asm prod.split_asm)
      qed
    qed
  qed
qed

subsection ‹Blocks›

lemma wp_blockNone:
    fixes id0 tp stm ev cd st
  defines "nGas ≡ state.Gas st - costs (BLOCK (id0, tp, None) stm) ev cd st"
  assumes "⋀cd' mem' sck' e'. decl id0 tp None False cd (Memory st) (Storage st (Address ev))
           (cd, Memory st, Stack st, ev) = Some (cd', mem', sck', e')
          ⟹ wpS stm P E e' cd' (st⦇Gas := nGas, Stack := sck', Memory := mem'⦈)"
      and "E Gas"
      and "E Err"
    shows "wpS (BLOCK (id0, tp, None) stm) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(9))
  apply wp
  using assms unfolding wpS_def by simp_all

lemma wp_blockSome:
    fixes id0 tp ex' stm ev cd st
  defines "nGas ≡ state.Gas st - costs (BLOCK (id0, tp, Some ex') stm) ev cd st"
  assumes "⋀v t g' cd' mem' sck' e'.
         ⟦expr ex' ev cd (st⦇Gas := nGas⦈) nGas = Normal ((v, t), g');
          decl id0 tp (Some (v,t)) False cd (Memory st) (Storage st (Address ev)) (cd, Memory st, Stack st, ev) = Some (cd', mem', sck', e')⟧
        ⟹ wpS stm P E e' cd' (st⦇Gas := g', Stack := sck', Memory := mem'⦈)"
      and "⋀e. expr ex' ev cd (st⦇Gas := nGas⦈) nGas = Exception e ⟹ E e"
      and "E Gas"
      and "E Err"
    shows "wpS (BLOCK (id0, tp, Some ex') stm) P E ev cd st"
  unfolding wpS_def
  apply (subst stmt.simps(10))
  apply wp
  using assms unfolding wpS_def by (simp_all)

end

subsection ‹External method invocation›

locale Calculus = statement_with_gas +
  fixes cname::Identifier
    and members:: "(Identifier, member) fmap"
    and const::"(Identifier × type) list × s"
    and fb :: s
assumes C1: "ep $$ cname = Some (members, const, fb)"
begin

text ‹
  The rules for method invocations is provided in the context of four parameters:
  ▪ @{term_type cname}: The name of the contract to be verified
  ▪ @{term_type members}: The member variables of the contract to be verified
  ▪ @{term const}: The constructor of the contract to be verified
  ▪ @{term fb}: The fallback method of the contract to be verified

In addition @{thm[source] C1} assigns members, constructor, and fallback method to the contract address.
›

text ‹
  An invariant is a predicate over two parameters:
  ▪ The private store of the contract
  ▪ The balance of the contract
›

type_synonym invariant = "storageT ⇒ int ⇒ bool"

subsection ‹Method invocations and transfer›

definition Qe
  where "Qe ad iv st ≡
    (∀mid fp f ev.
       members $$ mid = Some (Method (fp,True,f)) ∧
       Address ev ≠ ad
      ⟶ (∀adex cd st' xe val g v t g' v' e⇩l cd⇩l k⇩l m⇩l g'' acc.
            g'' ≤ state.Gas st ∧
            Type (acc ad) = Some (atype.Contract cname) ∧
            expr adex ev cd (st'⦇Gas := state.Gas st' - costs (EXTERNAL adex mid xe val) ev cd st'⦈) (state.Gas st' - costs (EXTERNAL adex mid xe val) ev cd st') = Normal ((KValue ad, Value TAddr), g) ∧
            expr val ev cd (st'⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
            convert t (TUInt b256) v = Some v' ∧
            load True fp xe (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore emptyStore emptyTypedStore ev cd (st'⦇Gas := g'⦈) g' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g'') ∧
            transfer (Address ev) ad v' (Accounts (st'⦇Gas := g''⦈)) = Some acc ∧
            iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')
           ⟶ wpS f (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l (st'⦇Gas := g'', Accounts:= acc, Stack := k⇩l, Memory := m⇩l⦈)))"

definition Qi
  where "Qi ad pre post st ≡
   (∀mid fp f ev.
     members $$ mid = Some (Method (fp,False,f)) ∧
     Address ev = ad
    ⟶ (∀cd st' i xe e⇩l cd⇩l k⇩l m⇩l g.
          g ≤ state.Gas st ∧
          load False fp xe (ffold (init members) (emptyEnv ad cname (Sender ev) (Svalue ev)) (fmdom members)) emptyTypedStore emptyStore (Memory st') ev cd (st'⦇Gas := state.Gas st' - costs (INVOKE i xe) ev cd st'⦈) (state.Gas st' - costs (INVOKE i xe) ev cd st') = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g) ∧
          pre mid (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)), Storage st' ad, e⇩l, cd⇩l, k⇩l, m⇩l)
         ⟶ wpS f (λst. post mid (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l (st'⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈)))"

definition Qfi
  where "Qfi ad pref postf st ≡
   (∀ev. Address ev = ad
    ⟶ (∀ex cd st' adex cc v t g g' v' acc.
          g' ≤ state.Gas st ∧
          expr adex ev cd (st'⦇Gas := state.Gas st' - cc⦈) (state.Gas st' - cc) = Normal ((KValue ad, Value TAddr), g) ∧
          expr ex ev cd (st'⦇Gas := g⦈) g= Normal ((KValue v, Value t), g') ∧
          convert t (TUInt b256) v = Some v' ∧
          transfer (Address ev) ad v' (Accounts st') = Some acc ∧
          pref (ReadL⇩i⇩n⇩t (Bal (acc ad)), Storage st' ad)
         ⟶ wpS fb (λst. postf (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore (st'⦇Gas := g', Accounts := acc, Stack:=emptyStore, Memory:=emptyTypedStore⦈)))"

definition Qfe
  where "Qfe ad iv st ≡
   (∀ev. Address ev ≠ ad
    ⟶ (∀ex cd st' adex cc v t g g' v' acc.
          g' ≤ state.Gas st ∧
          Type (acc ad) = Some (atype.Contract cname) ∧
          expr adex ev cd (st'⦇Gas := state.Gas st' - cc⦈) (state.Gas st' - cc) = Normal ((KValue ad, Value TAddr), g) ∧
          expr ex ev cd (st'⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
          convert t (TUInt b256) v = Some v' ∧
          transfer (Address ev) ad v' (Accounts st') = Some acc ∧
          iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')
         ⟶ wpS fb (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore (st'⦇Gas := g', Accounts := acc, Stack:=emptyStore, Memory:=emptyTypedStore⦈)))"

lemma safeStore[rule_format]:
  fixes ad iv
  defines "aux1 st ≡ ∀st'::state. state.Gas st' < state.Gas st ⟶ Qe ad iv st'"
      and "aux2 st ≡ ∀st'::state. state.Gas st' < state.Gas st ⟶ Qfe ad iv st'"
    shows "∀st'. Address ev ≠ ad ∧ Type (Accounts st ad) = Some (atype.Contract cname) ∧ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad))) ∧
            stmt f ev cd st = Normal ((), st') ∧ aux1 st ∧ aux2 st
           ⟶ iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
proof (induction rule:stmt.induct[where ?P="λf ev cd st. ∀st'. Address ev ≠ ad ∧ Type (Accounts st ad) = Some (atype.Contract cname) ∧ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad))) ∧ stmt f ev cd st = Normal ((), st') ∧ aux1 st ∧ aux2 st ⟶ iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"])
  case (1 ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and *: "local.stmt SKIP ev cd st = Normal ((), st')"
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using skip[OF *] by simp
  qed
next
  case (2 lv ex ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume "Address ev ≠ ad" and "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and 3: "stmt (ASSIGN lv ex) ev cd st = Normal ((), st')"
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" by (cases rule: assign[OF 3]; simp)
  qed
next
  case (3 s1 s2 ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume l1: "Address ev ≠ ad" and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" and l2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and l3: "stmt (COMP s1 s2) ev cd st = Normal ((), st')" and 4:"aux1 st" and 5:"aux2 st"
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
    proof  (cases rule: comp[OF l3])
      case (1 st'')
      moreover have *:"assert Gas (λst. costs (COMP s1 s2) ev cd st < state.Gas st) st = Normal ((), st)" using l3 by (simp add:stmt.simps split:if_split_asm)
      moreover from l2 have "iv (Storage (st⦇Gas := state.Gas st - costs (COMP s1 s2) ev cd st⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := state.Gas st - costs (COMP s1 s2) ev cd st⦈) ad)))" by simp
      moreover have **:"state.Gas (st⦇Gas:= state.Gas st - costs (COMP s1 s2) ev cd st⦈) ≤ state.Gas st" by simp
      then have "aux1 (st⦇Gas:= state.Gas st - costs (COMP s1 s2) ev cd st⦈)" using 4 unfolding aux1_def using all_gas_less[OF _ **,of "λst. Qe ad iv st"] by blast
      moreover have "aux2 (st⦇Gas:= state.Gas st - costs (COMP s1 s2) ev cd st⦈)" using 5 unfolding aux2_def using all_gas_less[OF _ **,of "λst. Qfe ad iv st"] by blast
      ultimately have "iv (Storage st'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st'' ad)))" using 3(1) C1 l1 l12 by auto
      moreover from l12 have "Type (Accounts st'' ad) = Some (atype.Contract cname)" using atype_same[OF 1(2), of ad "atype.Contract cname"] l12 by auto
      moreover have **:"state.Gas st'' ≤ state.Gas st" using stmt_gas[OF 1(2)] by simp
      then have "aux1 st''" using 4 unfolding aux1_def using all_gas_less[OF _ **,of "λst. Qe ad iv st"] by blast
      moreover have "aux2 st''" using 5 unfolding aux2_def using all_gas_less[OF _ **,of "λst. Qfe ad iv st"] by blast
      ultimately show ?thesis using 3(2)[OF * _ 1(2), of "()"] 1(3) C1 l1 by simp
    qed
  qed
next
  case (4 ex s1 s2 ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume l1: "Address ev ≠ ad" and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" and l2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and l3: "stmt (ITE ex s1 s2) ev cd st = Normal ((), st')" and l4:"aux1 st" and l5:"aux2 st"
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
    proof (cases rule: ite[OF l3])
      case (1 g)
      moreover from l2 have "iv (Storage (st⦇Gas :=g⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g⦈) ad)))" by simp
      moreover from l12 have "Type (Accounts (st⦇Gas:= g⦈) ad) = Some (atype.Contract cname)" using atype_same[OF 1(3), of ad "atype.Contract cname"] l12 by auto
      moreover have **:"state.Gas (st⦇Gas:= g⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] by simp
      then have "aux1 (st⦇Gas:= g⦈)" using l4 unfolding aux1_def using all_gas_less[OF _ **,of "λst. Qe ad iv st"] by blast
      moreover have "aux2 (st⦇Gas:= g⦈)" using l5 unfolding aux2_def using all_gas_less[OF _ **,of "λst. Qfe ad iv st"] by blast
      ultimately show ?thesis using 4(1) l1 by simp
    next
      case (2 g)
      moreover from l2 have "iv (Storage (st⦇Gas := g⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g⦈) ad)))" by simp
      moreover from l12 have "Type (Accounts (st⦇Gas:= g⦈) ad) = Some (atype.Contract cname)" using atype_same[OF 2(3), of ad "atype.Contract cname"] l12 by auto
      moreover have **:"state.Gas (st⦇Gas:= g⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 2(2)] by simp
      then have "aux1 (st⦇Gas:= g⦈)" using l4 unfolding aux1_def using all_gas_less[OF _ **,of "λst. Qe ad iv st"] by blast
      moreover have "aux2 (st⦇Gas:= g⦈)" using l5 unfolding aux2_def using all_gas_less[OF _ **,of "λst. Qfe ad iv st"] by blast
      ultimately show ?thesis using 4(2) l1 true_neq_false by simp
    qed
  qed
next
  case (5 ex s0 ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume l1: "Address ev ≠ ad" and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" and l2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and l3: "stmt (WHILE ex s0) ev cd st = Normal ((), st')" and l4:"aux1 st" and l5:"aux2 st"
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
    proof (cases rule: while[OF l3])
      case (1 g st'')
      moreover from l2 have "iv (Storage (st⦇Gas :=g⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g⦈) ad)))" by simp
      moreover have *:"state.Gas (st⦇Gas:= g⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] by simp
      then have "aux1 (st⦇Gas:= g⦈)" using l4 unfolding aux1_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by blast
      moreover have "aux2 (st⦇Gas:= g⦈)" using l5 unfolding aux2_def using all_gas_less[OF _ *,of "λst. Qfe ad iv st"] by blast
      ultimately have "iv (Storage st'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st'' ad)))" using 5(1) l1 l12 by simp
      moreover from l12 have "Type (Accounts st'' ad) = Some (atype.Contract cname)" using atype_same[OF 1(3), of ad "atype.Contract cname"] l12 by auto
      moreover have **:"state.Gas st'' ≤ state.Gas st" using stmt_gas[OF 1(3)] * by simp
      then have "aux1 st''" using l4 unfolding aux1_def using all_gas_less[OF _ **,of "λst. Qe ad iv st"] by blast
      moreover have "aux2 st''" using l5 unfolding aux2_def using all_gas_less[OF _ **,of "λst. Qfe ad iv st"] by blast
      ultimately show ?thesis using 5(2) 1(1,2,3,4) l1 by simp
    next
      case (2 g)
      then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using l2 by simp
    qed
  qed
next
  case (6 i xe ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume 1: "Address ev ≠ ad" and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" and 2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and 3: "local.stmt (INVOKE i xe) ev cd st = Normal ((), st')" and 4:"aux1 st" and 5:"aux2 st"
    from 3 obtain ct fb' fp f e⇩l cd⇩l k⇩l m⇩l g st''
      where l0: "costs (INVOKE i xe) ev cd st < state.Gas st"
      and l1: "ep $$ Contract ev = Some (ct, fb')"
      and l2: "ct $$ i = Some (Method (fp, False, f))"
      and l3: "load False fp xe (ffold (init ct) (emptyEnv (Address ev) (Contract ev) (Sender ev) (Svalue ev)) (fmdom ct)) emptyTypedStore emptyStore (Memory (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈)) ev cd (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) (state.Gas st - costs (INVOKE i xe) ev cd st) = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g)"
      and l4: "stmt f e⇩l cd⇩l (st⦇Gas:= g, Stack:=k⇩l, Memory:=m⇩l⦈) = Normal ((), st'')"
      and l5: "st' = st''⦇Stack:=Stack st⦈"
      using invoke by blast
    from 3 have *:"assert Gas (λst. costs (INVOKE i xe) ev cd st < state.Gas st) st = Normal ((), st)" by (simp add:stmt.simps split:if_split_asm)
    moreover have **: "modify (λst. st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) st = Normal ((), st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈)" by simp
    ultimately have "∀st'. Address e⇩l ≠ ad ∧ iv (Storage (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈) ad))) ∧ local.stmt f e⇩l cd⇩l (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈) = Normal ((), st') ∧ aux1 (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈) ∧ aux2 (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈) ⟶
      iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 6[OF * **] l1 l2 l3 l12 by (simp split:if_split_asm result.split_asm prod.split_asm option.split_asm)
    moreover have "Address (ffold (init ct) (emptyEnv (Address ev) (Contract ev) (Sender ev) (Svalue ev)) (fmdom ct)) = Address ev" using ffold_init_ad_same[of ct "(emptyEnv (Address ev) (Contract ev) (Sender ev) (Svalue ev))"] unfolding emptyEnv_def by simp
    with 1 have "Address e⇩l ≠ ad" using msel_ssel_expr_load_rexp_gas(4)[OF l3] by simp
    moreover from 2 have "iv (Storage (st⦇Gas:= g, Stack:=k⇩l, Memory:=m⇩l⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas:= g, Stack:=k⇩l, Memory:=m⇩l⦈) ad)))" by simp
    moreover have *:"state.Gas (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(4)[OF l3] by auto
    then have "aux1 (st⦇Gas:= g, Stack:=k⇩l, Memory:=m⇩l⦈)" using 4 unfolding aux1_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by blast
    moreover have *:"state.Gas (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(4)[OF l3] by auto
    then have "aux2 (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈)" using 5 unfolding aux2_def using all_gas_less[OF _ *,of "λst. Qfe ad iv st"] by blast
    ultimately have "iv (Storage st'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st'' ad)))" using l4 C1 by auto
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using l5  by simp
  qed
next
  case (7 ad' i xe val ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume l1: "Address ev ≠ ad"
      and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" 
      and l2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))"
      and 3: "local.stmt (EXTERNAL ad' i xe val) ev cd st = Normal ((), st')"
      and 4: "aux1 st" and 5:"aux2 st"
    show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
    proof (cases rule: external[OF 3])
      case (1 adv c g ct cn fb' v t g' v' fp f e⇩l cd⇩l k⇩l m⇩l g'' acc st'')
      then show ?thesis
      proof (cases "adv = ad")
        case True
        moreover from this have "cname = c" using l12 1(4) by simp
        moreover from this have "members = ct" using C1 1(5) by simp
        moreover have "state.Gas st ≥  costs (EXTERNAL ad' i xe val) ev cd st" using 3 by (simp add:stmt.simps split:if_split_asm)
        then have "g'' < state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] msel_ssel_expr_load_rexp_gas(3)[OF 1(6)] msel_ssel_expr_load_rexp_gas(4)[OF 1(9)] external_not_zero[of ad' i xe val ev cd st] by auto
        then have "Qe ad iv (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈)" using 4 unfolding aux1_def by simp
        moreover have "g'' ≤ state.Gas (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈)" by simp
        moreover from l12 have "Type (acc ad) = Some (atype.Contract cname)" using transfer_type_same[OF 1(10)] by simp
        moreover have "i |∈| fmdom members" using 1(8) `members = ct` by (simp add: fmdomI)
        moreover have "members $$ i = Some (Method (fp,True,f))" using 1(8) `members = ct` by simp
        moreover have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')"
        proof -
          have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" using l2 by simp
          moreover have "ReadL⇩i⇩n⇩t (Bal (acc ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) + ReadL⇩i⇩n⇩t v'" using transfer_add[OF 1(10)] l1 True by simp
          ultimately show ?thesis by simp
        qed
        ultimately have "wpS f (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈)" unfolding Qe_def using l1 l12 1(2) 1(6-10) by simp
        moreover have "stmt f e⇩l cd⇩l (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) = Normal ((), st'')" using 1(11) by simp
        ultimately show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" unfolding wpS_def wp_def using 1(12) by simp
      next
        case False

        from 3 have *:"assert Gas (λst. costs (EXTERNAL ad' i xe val) ev cd st < state.Gas st) st = Normal ((), st)" by (simp add:stmt.simps split:if_split_asm)
        moreover have **: "modify (λst. st⦇Gas := state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) st = Normal ((), st⦇Gas := state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈)" by simp
        ultimately have "∀st'. Address e⇩l ≠ ad ∧ Type (acc ad) = Some (atype.Contract cname) ∧ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad))) ∧ local.stmt f e⇩l cd⇩l (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) = Normal ((), st') ∧ aux1 (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) ∧ aux2 (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) ⟶ iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 7(1)[OF * **] 1 by simp
        moreover have "Address (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) = adv" using ffold_init_ad_same[of ct "(emptyEnv adv c (Address ev) v)"] unfolding emptyEnv_def by simp
        with False have "Address e⇩l ≠ ad" using msel_ssel_expr_load_rexp_gas(4)[OF 1(9)] by simp
        moreover have "Bal (acc ad) = Bal ((Accounts st) ad)" using transfer_eq[OF 1(10)] False l1 by simp
        then have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)))" using l2 by simp
        moreover have "Type (acc ad) = Some (atype.Contract cname)" using transfer_type_same l12 1(10) by simp
        moreover have *:"state.Gas (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] msel_ssel_expr_load_rexp_gas(3)[OF 1(6)] msel_ssel_expr_load_rexp_gas(4)[OF 1(9)] by auto
        then have "aux1 (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈)" using 4 unfolding aux1_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by blast
        moreover have "aux2 (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈)" using 5 unfolding aux2_def using all_gas_less[OF _ *,of "λst. Qfe ad iv st"] by blast
        ultimately have "iv (Storage st'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st'' ad)))" using 1(11) by simp
        then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 1(12) by simp
      qed
    next
      case (2 adv c g ct cn fb' v t g' v' acc st'')
      then show ?thesis
      proof (cases "adv = ad")
        case True
        moreover have "state.Gas st ≥  costs (EXTERNAL ad' i xe val) ev cd st" using 3 by (simp add:stmt.simps split:if_split_asm)
        then have "state.Gas (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) < state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 2(2)] msel_ssel_expr_load_rexp_gas(3)[OF 2(6)] external_not_zero[of ad' i xe val ev cd st] by simp
        then have "Qfe ad iv (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using 5 unfolding aux2_def by simp
        moreover have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')"
        proof -
          have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" using l2 by simp
          moreover have "ReadL⇩i⇩n⇩t (Bal (acc ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) + ReadL⇩i⇩n⇩t v'" using transfer_add[OF 2(9)] l1 True by simp
          ultimately show ?thesis by simp
        qed
        moreover have "g' ≤ state.Gas (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" by simp
        moreover from l12 have "Type (acc ad) = Some (atype.Contract cname)" using transfer_type_same[OF 2(9)] by simp
        ultimately have "wpS fb (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" unfolding Qfe_def using l1 l12 2(2) 2(6-9) by blast
        moreover have "stmt fb (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) = Normal ((), st'')"
        proof -
          from True have "cname = c" using l12 2(4) by simp
          moreover from this have "fb'=fb" using C1 2(5) by simp
          moreover from True `cname = c` have "members = ct" using C1 2(5) by simp
          ultimately show ?thesis using 2(10) True by simp
        qed
        ultimately show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" unfolding wpS_def wp_def using 2(11) by simp
      next
        case False

        from 3 have *:"assert Gas (λst. costs (EXTERNAL ad' i xe val) ev cd st < state.Gas st) st = Normal ((), st)" by (simp add:stmt.simps split:if_split_asm)
        then have "∀st'. Address (ffold (init ct) (emptyEnv adv c (Address ev) v) (fmdom ct)) ≠ ad ∧
          Type (acc ad) = Some (atype.Contract cname) ∧
          iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad))) ∧
          local.stmt fb' (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) emptyTypedStore (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) = Normal ((), st') ∧ aux1 (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) ∧ aux2 (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)
          ⟶ iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 7(2)[OF *] 2 by simp
        moreover from False have "Address (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) ≠ ad" using ffold_init_ad_same[where ?e="⦇Address = adv, Contract = c, Sender = Address ev, Svalue = v, Denvalue = {$$}⦈" and ?e'="ffold (init ct) (emptyEnv adv c (Address ev) v) (fmdom ct)"] unfolding emptyEnv_def by simp
        moreover have "Bal (acc ad) = Bal ((Accounts st) ad)" using transfer_eq[OF 2(9)] False l1 by simp
        then have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)))"
          using l2 by simp
        moreover have "Type (acc ad) = Some (atype.Contract cname)" using transfer_type_same l12 2(9) by simp
        moreover have *:"state.Gas (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 2(2)] msel_ssel_expr_load_rexp_gas(3)[OF 2(6)] by simp
        then have "aux1 (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using 4 unfolding aux1_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by blast
        moreover have "aux2 (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using 5 unfolding aux2_def using all_gas_less[OF _ *,of "λst. Qfe ad iv st"] by blast
        ultimately have "iv (Storage st'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st'' ad)))" using 2(10) by simp
        then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 2(11) by simp
      qed
    qed
  qed
next
  case (8 ad' ex ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume l1: "Address ev ≠ ad" and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" and l2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and 3: "local.stmt (TRANSFER ad' ex) ev cd st = Normal ((), st')" and 4:"aux1 st" and 5:"aux2 st"
    show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
    proof (cases rule: transfer[OF 3])
      case (1 v t g adv c g' v' acc ct cn f st'')
      then show ?thesis
      proof (cases "adv = ad")
        case True
        moreover have "state.Gas st ≥  costs (TRANSFER ad' ex) ev cd st" using 3 by (simp add:stmt.simps split:if_split_asm)
        then have "state.Gas (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) < state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] msel_ssel_expr_load_rexp_gas(3)[OF 1(3)] transfer_not_zero[of ad' ex ev cd st] by auto
        then have "Qfe ad iv (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using 5 unfolding aux2_def by simp
        moreover have "Sender (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) ≠ ad" using l1 ffold_init_ad_same[where ?e = "(emptyEnv adv c (Address ev) v')" and ?e'="ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)"] unfolding emptyEnv_def by simp
        moreover have "Svalue (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) = v'" using ffold_init_ad_same[where ?e = "(emptyEnv adv c (Address ev) v')" and ?e'="ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)", of ct "fmdom ct"] unfolding emptyEnv_def by simp
        moreover have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')"
        proof -
          have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" using l2 by simp
          moreover have "ReadL⇩i⇩n⇩t (Bal (acc ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) + ReadL⇩i⇩n⇩t v'" using transfer_add[OF 1(7)] l1 True by simp
          ultimately show ?thesis by simp
        qed
        moreover have "g' ≤ state.Gas (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" by simp
        moreover from l12 have "Type (acc ad) = Some (atype.Contract cname)" using transfer_type_same[OF 1(7)] by simp
        ultimately have "wpS fb (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" unfolding Qfe_def using l1 l12 1(2-7) by blast
        moreover have "stmt fb (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) = Normal ((), st'')"
        proof -
          from True have "cname = c" using l12 1(5) by simp
          moreover from this have "f=fb" using C1 1(6) by simp
          moreover from True `cname = c` have "members = ct" using C1 1(6) by simp
          ultimately show ?thesis using 1(8) True by simp
        qed
        ultimately show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" unfolding wpS_def wp_def using 1(9) by simp
      next
        case False

        from 3 have *:"assert Gas (λst. costs (TRANSFER ad' ex) ev cd st < state.Gas st) st = Normal ((), st)" by (simp add:stmt.simps split:if_split_asm)
        then have "∀st'. Address (ffold (init ct) (emptyEnv adv c (Address ev) v) (fmdom ct)) ≠ ad ∧
          Type (acc ad) = Some (atype.Contract cname) ∧
          iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad))) ∧
          local.stmt f (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) emptyTypedStore (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) = Normal ((), st') ∧
          aux1 (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) ∧ aux2 (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)
          ⟶ iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 8(1)[OF *] 1 by simp
        moreover from False have "Address (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) ≠ ad" using ffold_init_ad_same[of ct "emptyEnv adv c (Address ev) v"] unfolding emptyEnv_def by simp
        moreover have "Bal (acc ad) = Bal ((Accounts st) ad)" using transfer_eq[OF 1(7)] False l1 by simp
        then have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)))"
          using l2 by simp
        moreover have "Type (acc ad) = Some (atype.Contract cname)" using transfer_type_same l12 1(7) by simp
        moreover have *:"state.Gas (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] msel_ssel_expr_load_rexp_gas(3)[OF 1(3)] by simp
        then have "aux1 (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using 4 unfolding aux1_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by blast
        moreover have "aux2 (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using 5 unfolding aux2_def using all_gas_less[OF _ *,of "λst. Qfe ad iv st"] by blast
        ultimately have "iv (Storage st'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st'' ad)))" using 1(8) C1 by simp
        then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 1(9) by simp
      qed
    next
      case (2 v t g adv g' v' acc)
      moreover from 2(5) have "adv ≠ ad" using C1 l12 by auto
      then have "Bal (acc ad) = Bal (Accounts st ad)" using transfer_eq[OF 2(6)] l1 by simp
      ultimately show ?thesis using l2 by simp
    qed
  qed
next
  case (9 id0 tp s ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume l1: "Address ev ≠ ad" and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" and l2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and l3: "stmt (BLOCK (id0, tp, None) s) ev cd st = Normal ((), st')" and 4:"aux1 st" and 5:"aux2 st"
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
    proof  (cases rule: blockNone[OF l3])
      case (1 cd' mem' sck' e')
      moreover from l2 have "iv (Storage (st⦇Gas := state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st, Stack := sck', Memory := mem'⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st, Stack := sck', Memory := mem'⦈) ad)))" by simp
      moreover have *:"state.Gas (st⦇Gas:= state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st, Stack := sck', Memory := mem'⦈) ≤ state.Gas st" by simp
      then have "aux1 (st⦇Gas:= state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st, Stack := sck', Memory := mem'⦈)" using 4 unfolding aux1_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by blast
      moreover have "aux2 (st⦇Gas:= state.Gas st - costs (BLOCK (id0, tp, None) s) ev cd st, Stack := sck', Memory := mem'⦈)" using 5 unfolding aux2_def using all_gas_less[OF _ *,of "λst. Qfe ad iv st"] by blast
      moreover have "Address e' ≠ ad" using decl_env[OF 1(2)] l1 by simp
      ultimately show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 9(1) l12 by simp
    qed
  qed
next
  case (10 id0 tp ex' s ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume l1: "Address ev ≠ ad" and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" and l2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and l3: "stmt (BLOCK (id0, tp, Some ex') s) ev cd st = Normal ((), st')" and 4:"aux1 st" and 5:"aux2 st"
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
    proof  (cases rule: blockSome[OF l3])
      case (1 v t g cd' mem' sck' e')
      moreover from l2 have "iv (Storage (st⦇Gas := g, Stack := sck', Memory := mem'⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g, Stack := sck', Memory := mem'⦈) ad)))" by simp
      moreover have *:"state.Gas (st⦇Gas:= g, Stack := sck', Memory := mem'⦈) ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] by simp
      then have "aux1 (st⦇Gas:= g, Stack := sck', Memory := mem'⦈)" using 4 unfolding aux1_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by blast
      moreover have "aux2 (st⦇Gas:= g, Stack := sck', Memory := mem'⦈)" using 5 unfolding aux2_def using all_gas_less[OF _ *,of "λst. Qfe ad iv st"] by blast
      moreover have "Address e' ≠ ad" using decl_env[OF 1(3)] l1 by simp
      ultimately show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))" using 10(1) l12 by simp
    qed
  qed
next
  case (11 i xe val ev cd st)
  show ?case
  proof (rule allI, rule impI, (erule conjE)+)
    fix st' assume l1: "Address ev ≠ ad" and l12:"Type (Accounts st ad) = Some (atype.Contract cname)" and l2: "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" and l3: "stmt (NEW i xe val) ev cd st = Normal ((), st')" and 4:"aux1 st" and 5:"aux2 st"
    then show "iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
    proof  (cases rule: new[OF l3])
      case (1 v t g ct cn fb e⇩l cd⇩l k⇩l m⇩l g' acc st'' v')
      define adv where "adv = hash_version (Address ev) (ShowL⇩n⇩a⇩t (Contracts (Accounts (st⦇state.Gas := state.Gas st - costs (NEW i xe val) ev cd st⦈) (Address ev))))"
      define st0 where "st0 = st⦇state.Gas := state.Gas st - costs (NEW i xe val) ev cd st⦈"
      define st1 where "st1 = st⦇state.Gas := g, Accounts := (Accounts st)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage := (state.Storage st)(adv := {$$})⦈"
      define st''' where "st''' = st⦇state.Gas := g', Accounts := (Accounts st)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage := (state.Storage st)(adv := {$$}), Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈"

      have a1: "assert Gas (λst. costs (NEW i xe val) ev cd st < state.Gas st) st = Normal ((), st)"
        using 1(1) by simp
      have a2: "modify (λst. st⦇state.Gas := state.Gas st - costs (NEW i xe val) ev cd st⦈) st = Normal ((), st0)"
        using st0_def by simp
      have a3: "applyf (λst. hash_version (Address ev) (ShowL⇩n⇩a⇩t (Contracts (Accounts st (Address ev))))) st0 = Normal (adv, st0)"
        using adv_def st0_def by simp
      have a4: "assert Err (λst. Type (Accounts st adv) = None) st0 = Normal ((), st0)"
        using 1(2) adv_def st0_def by simp
      have a5: "toState (expr val ev cd) st0 = Normal ((KValue v, Value t), st0⦇state.Gas := g⦈)"
        using 1(3) st0_def by simp
      have a6: "(case (KValue v, Value t) of (KValue v, Value t) ⇒ return (v, t) | _ ⇒ throw Err) (st0⦇state.Gas := g⦈) = Normal ((v, t), st0⦇state.Gas := g⦈)"
        by simp
      have a7: "option Err (λ_. convert t (TUInt b256) v) (st0⦇state.Gas := g⦈) = Normal (v', st0⦇state.Gas := g⦈)"
        using 1(4) by simp
      have a8: "option Err (λ_. ep $$ i) (st0⦇state.Gas := g⦈) = Normal ((ct, cn, fb), st0⦇state.Gas := g⦈)"
        using 1(5) by simp
      have a9: "modify (λst. st⦇Accounts := (Accounts st)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage := (state.Storage st)(adv := {$$})⦈) (st0⦇state.Gas := g⦈) = Normal ((), st1)"
        using st0_def st1_def by simp
      define e' where "e' = ffold_init ct (emptyEnv adv i (Address ev) v') (fmdom ct)"
      have a10: "toState (load True (fst cn) xe e' emptyTypedStore emptyStore emptyTypedStore ev cd) st1 = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), st1⦇state.Gas := g'⦈)"
        using 1(6) st1_def e'_def adv_def st0_def by simp
      have a11: "option Err (λst. transfer (Address ev) adv v' (Accounts st)) (st1⦇state.Gas := g'⦈) = Normal (acc, st1⦇state.Gas := g'⦈)"
        using 1(7) st1_def adv_def by simp
      have a12: "applyf (λst. (Stack st, state.Memory st)) (st1⦇state.Gas := g'⦈) = Normal ((Stack st, state.Memory st), st1⦇state.Gas := g'⦈)"
        using st1_def by simp
      have a13: "modify (λst. st⦇Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) (st1⦇state.Gas := g'⦈) = Normal ((), st''')"
        using st'''_def st1_def by simp

      have "∀st'. Address e⇩l ≠ ad ∧
        Type (Accounts st''' ad) = Some (atype.Contract cname) ∧
        iv (state.Storage st''' ad) ⌈Bal (Accounts st''' ad)⌉ ∧
        local.stmt (snd cn) e⇩l cd⇩l st''' = Normal ((), st') ∧ aux1 st''' ∧ aux2 st''' ⟶
        iv (state.Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
        using 11[OF a1 a2 a3 a4 a5 a6 refl a7 a8 refl refl a9 e'_def a10 refl refl refl a11 a12 refl a13] by simp
      moreover have "Address e⇩l ≠ ad"
      proof -
        have "Address e⇩l = adv" using msel_ssel_expr_load_rexp_gas(4)[OF 1(6)] adv_def by simp
        moreover have "adv ≠ ad" using l12 1(2) adv_def by auto
        ultimately show ?thesis by simp
      qed
      moreover have "Type (Accounts st''' ad) = Some (atype.Contract cname)"
      proof -
        have "adv ≠ ad" using l12 1(2) adv_def by auto
        then have "Type (Accounts st ad) = Type (acc ad)" using transfer_type_same[OF 1(7)] adv_def by simp
        then show ?thesis using l12 st'''_def by simp
      qed
      moreover have "iv (Storage st''' ad) ⌈Bal (Accounts st''' ad)⌉"
      proof -
        have "adv ≠ ad" using l12 1(2) adv_def by auto
        then have "Bal (Accounts st ad) = Bal (Accounts st''' ad)" using transfer_eq[OF 1(7), of ad] l1 using st'''_def adv_def by simp
        moreover have "Storage st ad = Storage st''' ad" using st'''_def `adv ≠ ad` by simp
        ultimately show ?thesis using l2 by simp
      qed
      moreover have "local.stmt (snd cn) e⇩l cd⇩l st''' = Normal ((), st'')" using 1(8) st'''_def adv_def by simp
      moreover have "aux1 st'''"
      proof -
        have *: "state.Gas st''' ≤ state.Gas st" unfolding st'''_def using msel_ssel_expr_load_rexp_gas(3)[OF 1(3)] msel_ssel_expr_load_rexp_gas(4)[OF 1(6)] by auto
        then show ?thesis using 4 unfolding aux1_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by simp
      qed
      moreover have "aux2 st'''"
      proof -
        have *: "state.Gas st''' ≤ state.Gas st" unfolding st'''_def using msel_ssel_expr_load_rexp_gas(3)[OF 1(3)] msel_ssel_expr_load_rexp_gas(4)[OF 1(6)] by auto
        then show ?thesis using 5 unfolding aux2_def using all_gas_less[OF _ *,of "λst. Qe ad iv st"] by simp
      qed
      ultimately have "iv (Storage st'' ad) ⌈Bal (Accounts st'' ad)⌉" by simp
      moreover have "Storage st'' ad = Storage st' ad" using 1(9) by simp
      moreover have "Bal (Accounts st'' ad) = Bal (Accounts st' ad)" using 1(9) by simp
      ultimately show ?thesis by simp
    qed
  qed
qed

type_synonym precondition = "int × storageT × environment × (mtypes,memoryvalue) typedstore × stackvalue store × (mtypes,memoryvalue) typedstore ⇒ bool"
type_synonym postcondition = "int × storageT ⇒ bool"

text ‹
  The following lemma can be used to verify (recursive) internal or external method calls and transfers executed from **inside** (@{term "Address ev = ad"}).
  In particular the lemma requires the contract to be annotated as follows:
  ▪ Pre/Postconditions for internal methods
  ▪ Invariants for external methods 

  The lemma then requires us to verify the following:
  ▪ Postconditions from preconditions for internal method bodies.
  ▪ Invariants hold for external method bodies.

  To this end it allows us to assume the following:
  ▪ Preconditions imply postconditions for internal method calls.
  ▪ Invariants hold for external method calls for other Contracts external methods.
›

definition Pe
  where "Pe ad iv st ≡
    (∀ev ad' i xe val cd.
       Address ev = ad ∧
       (∀adv c g v t g' v'.
         expr ad' ev cd (st⦇Gas := state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) (state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g) ∧
         adv ≠ ad ∧
         Type (Accounts st adv) = Some (atype.Contract c) ∧
         c |∈| fmdom ep ∧
         expr val ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
         convert t (TUInt b256) v = Some v'
        ⟶ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v'))
      ⟶ wpS (EXTERNAL ad' i xe val) (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) ev cd st)"

definition Pi
  where "Pi ad pre post st ≡
    (∀ev i xe cd.
       Address ev = ad ∧
       Contract ev = cname ∧
       (∀fp e⇩l cd⇩l k⇩l m⇩l g.
         load False fp xe (ffold (init members) (emptyEnv ad (Contract ev) (Sender ev) (Svalue ev)) (fmdom members)) emptyTypedStore emptyStore (Memory st) ev cd (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) (state.Gas st - costs (INVOKE i xe) ev cd st) = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g)
        ⟶ pre i (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad, e⇩l, cd⇩l, k⇩l, m⇩l))
    ⟶ wpS (INVOKE i xe) (λst. post i (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) ev cd st)"

definition Pfi
  where "Pfi ad pref postf st ≡
   (∀ev ex ad' cd.
     Address ev = ad ∧
     (∀adv g.
       expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)
      ⟶ adv = ad) ∧
     (∀g v t g'.
       expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue ad, Value TAddr), g) ∧
       expr ex ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g')
      ⟶ pref (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad))
    ⟶ wpS (TRANSFER ad' ex) (λst. postf (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) ev cd st)"

definition Pfe
  where "Pfe ad iv st ≡
     (∀ev ex ad' cd.
       Address ev = ad ∧
       (∀adv g.
         expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)
        ⟶ adv ≠ ad) ∧
       (∀adv g v t g' v'.
         expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g) ∧
         adv ≠ ad ∧
         expr ex ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
         convert t (TUInt b256) v = Some v'
        ⟶ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v'))
      ⟶ wpS (TRANSFER ad' ex) (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) ev cd st)"

lemma wp_external_invoke_transfer:  
    fixes pre::"Identifier ⇒ precondition"
      and post::"Identifier ⇒ postcondition"
      and pref::"postcondition"
      and postf::"postcondition"
      and iv::"invariant"
    assumes assm: "⋀st::state.
    ⟦∀st'::state. state.Gas st' ≤ state.Gas st ∧ Type (Accounts st' ad) = Some (atype.Contract cname)
        ⟶ Pe ad iv st' ∧ Pi ad pre post st' ∧ Pfi ad pref postf st' ∧ Pfe ad iv st'⟧
    ⟹ Qe ad iv st ∧ Qi ad pre post st ∧ Qfi ad pref postf st ∧ Qfe ad iv st"
    shows "Type (Accounts st ad) = Some (atype.Contract cname) ⟶ Pe ad iv st ∧ Pi ad pre post st ∧ Pfi ad pref postf st ∧ Pfe ad iv st"
proof (induction st rule: gas_induct)
  case (1 st)
  show ?case unfolding Pe_def Pi_def Pfi_def Pfe_def
  proof elims
    fix ev::environment and ad' i xe val cd
    assume a00: "Type (Accounts st ad) = Some (atype.Contract cname)"
       and a0: "Address ev = ad"
       and a1: "∀adv c g v t g' v'.
          local.expr ad' ev cd (st⦇Gas := state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈)
           (state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st) =
          Normal ((KValue adv, Value TAddr), g) ∧
          adv ≠ ad ∧
          Type (Accounts st adv) = Some (atype.Contract c) ∧
          c |∈| fmdom ep ∧
          local.expr val ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
          convert t (TUInt b256) v = Some v'
      ⟶ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v')"
    show "wpS (EXTERNAL ad' i xe val) (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) ev cd st" unfolding wpS_def wp_def
    proof (split result.split; split prod.split; rule conjI; (rule allI)+; (rule impI)+)
      fix x1 x1a s''''''
      assume "x1 = (x1a, s'''''')" and 2: "local.stmt (EXTERNAL ad' i xe val) ev cd st = Normal x1"
      then have "local.stmt (EXTERNAL ad' i xe val) ev cd st = Normal (x1a, s'''''')" by simp
      then show "iv (Storage s'''''' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts s'''''' ad)))"
      proof (cases rule: external)
        case (Some adv0 c0 g0 ct0 cn0 fb0 v0 t0 g0' v0' fp0 f0 e⇩l0 cd⇩l0 k⇩l0 m⇩l0 g0'' acc0 st0'')
        moreover have "iv (Storage st0'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st0'' ad)))"
        proof -
          from Some(3) have "adv0 ≠ ad" using a0 by simp
          then have "Address e⇩l0 ≠ ad" using msel_ssel_expr_load_rexp_gas(4)[OF Some(9)] ffold_init_ad_same[of ct0 "(emptyEnv adv0 c0 (Address ev) v0')" "(fmdom ct0)" "(ffold (init ct0) (emptyEnv adv0 c0 (Address ev) v0) (fmdom ct0))"] unfolding emptyEnv_def by simp
          moreover have "Type (Accounts (st⦇Gas := g0'', Accounts := acc0, Stack := k⇩l0, Memory := m⇩l0⦈) ad) = Some (atype.Contract cname)" using transfer_type_same[OF Some(10)] a00 by simp
          moreover have "iv (Storage (st⦇Gas := g0'', Accounts := acc0, Stack := k⇩l0, Memory := m⇩l0⦈) ad)
                        (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g0'', Accounts := acc0, Stack := k⇩l0, Memory := m⇩l0⦈) ad)))"
          proof -
            from Some(5) have "c0 |∈| fmdom ep" by (rule fmdomI)
            with a0 a1 Some `adv0 ≠ ad` have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v0')" by simp
            moreover have "ReadL⇩i⇩n⇩t (Bal (acc0 ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v0'" using transfer_sub[OF Some(10)] a0 `adv0 ≠ ad` by simp
            ultimately show ?thesis by simp
          qed
          moreover have "∀st'::state. state.Gas st' < state.Gas (st⦇Gas := g0'', Accounts := acc0, Stack := k⇩l0, Memory := m⇩l0⦈) ⟶
              (∀mid fp f ev.
                members $$ mid = Some (Method (fp, True, f)) ∧
                Address ev ≠ ad
               ⟶ (∀adex cd st0 xe val g v t g' v' e⇩l cd⇩l k⇩l' m⇩l' g'' acc.
                     g'' ≤ state.Gas st' ∧
                     Type (acc ad) = Some (atype.Contract cname) ∧
                     local.expr adex ev cd (st0⦇Gas := state.Gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0⦈) (state.Gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0) = Normal ((KValue ad, Value TAddr), g) ∧
                     local.expr val ev cd (st0⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
                     convert t (TUInt b256) v = Some v' ∧
                     local.load True fp xe (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore emptyStore emptyTypedStore ev cd (st0⦇Gas := g'⦈) g' = Normal ((e⇩l, cd⇩l, k⇩l', m⇩l'), g'') ∧
                     transfer (Address ev) ad v' (Accounts (st0⦇Gas := g''⦈)) = Some acc ∧
                     iv (Storage st0 ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')
                    ⟶  wpS f (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l (st0⦇Gas := g'', Accounts := acc, Stack := k⇩l', Memory := m⇩l'⦈)))" (is "∀st'. ?left st' ⟶ ?right st'")
          proof (rule allI,rule impI)
            fix st'::state
            assume "state.Gas st' < state.Gas (st⦇Gas := g0'', Accounts := acc0, Stack := k⇩l0, Memory := m⇩l0⦈)"
            then have "state.Gas st' < state.Gas st" using msel_ssel_expr_load_rexp_gas(4)[OF Some(9)] msel_ssel_expr_load_rexp_gas(3)[OF Some(2)] msel_ssel_expr_load_rexp_gas(3)[OF Some(6)] by auto
            then show "?right st'" using assm[OF all_gas_le[OF `state.Gas st' < state.Gas st` "1.IH"], THEN conjunct1] unfolding Qe_def by simp
          qed
          moreover have "∀st'::state. state.Gas st' < state.Gas (st⦇Gas := g0'', Accounts := acc0, Stack := k⇩l0, Memory := m⇩l0⦈) ⟶
              (∀ev. Address ev ≠ ad
               ⟶ (∀ex cd st0 adex cc v t g g' v' acc.
                     g' ≤ state.Gas st' ∧
                     Type (acc ad) = Some (atype.Contract cname) ∧
                     expr adex ev cd (st0⦇Gas := state.Gas st0 - cc⦈) (state.Gas st0 - cc) = Normal ((KValue ad, Value TAddr), g) ∧
                     expr ex ev cd (st0⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
                     convert t (TUInt b256) v = Some v' ∧
                     transfer (Address ev) ad v' (Accounts st0) = Some acc ∧
                     iv (Storage st0 ad) (⌈Bal (acc ad)⌉ - ⌈v'⌉) ⟶
                     wpS fb (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err)
                      (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore
                      (st0⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)))" (is "∀st'. ?left st' ⟶ ?right st'")
          proof (rule allI,rule impI)
            fix st'::state
            assume l0: "state.Gas st' < state.Gas (st⦇Gas := g0'', Accounts := acc0, Stack := k⇩l0, Memory := m⇩l0⦈)"
            then have "state.Gas st' < state.Gas st" using msel_ssel_expr_load_rexp_gas(4)[OF Some(9)] msel_ssel_expr_load_rexp_gas(3)[OF Some(2)] msel_ssel_expr_load_rexp_gas(3)[OF Some(6)] by auto
            then show "?right st'" using assm[OF all_gas_le[OF `state.Gas st' < state.Gas st` "1.IH"], THEN conjunct2, THEN conjunct2, THEN conjunct2] unfolding Qfe_def by simp
          qed
          ultimately show ?thesis using safeStore[of e⇩l0 ad "st⦇Gas := g0'', Accounts := acc0, Stack := k⇩l0, Memory := m⇩l0⦈" iv f0 cd⇩l0 st0''] Some unfolding Qe_def Qfe_def by blast
        qed
        ultimately show ?thesis by simp
      next
        case (None adv0 c0 g0 ct0 cn0 fb0' v0 t0 g0' v0' acc0 st0'')
        moreover have "iv (Storage s'''''' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts s'''''' ad)))"
        proof -
          from None have "adv0 ≠ ad" using a0 by auto
          then have "Address (ffold (init ct0) (emptyEnv adv0 c0 (Address ev) v0') (fmdom ct0)) ≠ ad" using ffold_init_ad_same[where ?e="⦇Address = adv0, Contract = c0, Sender = Address ev, Svalue = v0', Denvalue = {$$}⦈" and e'="ffold (init ct0) (emptyEnv adv0 c0 (Address ev) v0') (fmdom ct0)"] unfolding emptyEnv_def by simp
          moreover have "Type (Accounts (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ad) = Some (atype.Contract cname)" using transfer_type_same[OF None(9)] a00 by simp
          moreover have "iv (Storage (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ad)))"
          proof -
            from None(5) have "c0 |∈| fmdom ep" by (rule fmdomI)
            with a0 a1 None `adv0 ≠ ad` have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v0')" by simp
            moreover have "ReadL⇩i⇩n⇩t (Bal (acc0 ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v0'" using transfer_sub[OF None(9)] a0 `adv0 ≠ ad` by simp
            ultimately show ?thesis by simp
          qed
          moreover have "∀st'::state. state.Gas st' < state.Gas (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ⟶
              (∀mid fp f ev.
                members $$ mid = Some (Method (fp, True, f)) ∧
                Address ev ≠ ad
               ⟶ (∀adex cd st0 xe val g v t g' v' e⇩l cd⇩l k⇩l' m⇩l' g'' acc.
                     g'' ≤ state.Gas st' ∧
                     Type (acc ad) = Some (atype.Contract cname) ∧
                     local.expr adex ev cd (st0⦇Gas := state.Gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0⦈) (state.Gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0) = Normal ((KValue ad, Value TAddr), g) ∧
                     local.expr val ev cd (st0⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
                     convert t (TUInt b256) v = Some v' ∧
                     local.load True fp xe (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore emptyStore emptyTypedStore ev cd (st0⦇Gas := g'⦈) g' = Normal ((e⇩l, cd⇩l, k⇩l', m⇩l'), g'') ∧
                     transfer (Address ev) ad v' (Accounts (st0⦇Gas := g''⦈)) = Some acc ∧
                     iv (Storage st0 ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')
                    ⟶  wpS f (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l (st0⦇Gas := g'', Accounts := acc, Stack := k⇩l', Memory := m⇩l'⦈)))" (is "∀st'. ?left st' ⟶ ?right st'")
          proof (rule allI,rule impI)
            fix st'::state
            assume "state.Gas st' < state.Gas (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈)"
            then have "state.Gas st' < state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF None(2)] msel_ssel_expr_load_rexp_gas(3)[OF None(6)] by auto
            then show "?right st'" using assm[OF all_gas_le[OF `state.Gas st' < state.Gas st` "1.IH"], THEN conjunct1] unfolding Qe_def by simp
          qed
          moreover have "∀st'::state. state.Gas st' < state.Gas (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ⟶
              (∀ev. Address ev ≠ ad
               ⟶ (∀ex cd st0 adex cc v t g g' v' acc.
                     g' ≤ state.Gas st' ∧
                     Type (acc ad) = Some (atype.Contract cname) ∧
                     expr adex ev cd (st0⦇Gas := state.Gas st0 - cc⦈) (state.Gas st0 - cc) = Normal ((KValue ad, Value TAddr), g) ∧
                     expr ex ev cd (st0⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
                     convert t (TUInt b256) v = Some v' ∧
                     transfer (Address ev) ad v' (Accounts st0) = Some acc ∧
                     iv (Storage st0 ad) (⌈Bal (acc ad)⌉ - ⌈v'⌉) ⟶
                     wpS fb (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err)
                      (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore
                      (st0⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)))" (is "∀st'. ?left st' ⟶ ?right st'")
          proof (rule allI,rule impI)
            fix st'::state
            assume l0: "state.Gas st' < state.Gas (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈)"
            then have "state.Gas st' < state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF None(2)] msel_ssel_expr_load_rexp_gas(3)[OF None(6)] by auto
            then show "?right st'" using assm[OF all_gas_le[OF `state.Gas st' < state.Gas st` "1.IH"], THEN conjunct2, THEN conjunct2, THEN conjunct2] unfolding Qfe_def by simp
          qed                                                                                                                                                                                                                                                                                                            
          ultimately have "iv (Storage st0'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st0'' ad)))" using safeStore[of "ffold (init ct0) (emptyEnv adv0 c0 (Address ev) v0') (fmdom ct0)" ad "st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈" iv fb0' emptyTypedStore "st0''"] None unfolding Qe_def Qfe_def by blast
          then show ?thesis using None(11) by simp
        qed
        ultimately show ?thesis by simp
      qed
    next
      fix e
      assume "local.stmt (EXTERNAL ad' i xe val) ev cd st = Exception e"
      show "e = Gas ∨ e = Err" using ex.nchotomy by simp
    qed
  next
    fix ev ex ad' cd
    assume a00: "Type (Accounts st ad) = Some (atype.Contract cname)"
      and a0: "Address ev = ad"
      and a1: "∀adv g. local.expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g) ⟶ adv ≠ ad"
      and a2: "∀adv g v t g' v'.
          local.expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g) ∧
          adv ≠ ad ∧
          local.expr ex ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
          convert t (TUInt b256) v = Some v' ⟶
          iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v')"
    show "wpS (TRANSFER ad' ex) (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) ev cd st"
      unfolding wpS_def wp_def
    proof (split result.split; split prod.split; rule conjI; (rule allI)+; (rule impI)+)
      fix x1 x1a s''''''
      assume "x1 = (x1a, s'''''')" and "local.stmt (TRANSFER ad' ex) ev cd st = Normal x1"
      then have 2: "local.stmt (TRANSFER ad' ex) ev cd st = Normal (x1a, s'''''')" by simp
      then show "iv (Storage s'''''' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts s'''''' ad)))"
      proof (cases rule: transfer)
        case (Contract v0 t0 g0 adv0 c0 g0' v0' acc0 ct0 cn0 f0 st0'')
        moreover have "iv (Storage s'''''' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts s'''''' ad)))"
        proof -
          from Contract have "adv0 ≠ ad" using a1 by auto
          then have "Address (ffold (init ct0) (emptyEnv adv0 c0 (Address ev) v0') (fmdom ct0)) ≠ ad" using a0 ffold_init_ad_same[where ?e'="ffold (init ct0) (emptyEnv adv0 c0 (Address ev) v0') (fmdom ct0)"] unfolding emptyEnv_def by simp
          moreover have "Type (Accounts (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ad) = Some (atype.Contract cname)" using transfer_type_same[OF Contract(7)] a00 by simp
          moreover have "iv (Storage (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ad)))"
          proof -
            from a0 a2 Contract `adv0 ≠ ad` have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v0')" by blast
            moreover have "ReadL⇩i⇩n⇩t (Bal (acc0 ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v0'" using transfer_sub[OF Contract(7)] a0 `adv0 ≠ ad` by simp
            ultimately show ?thesis by simp
          qed
          moreover have "∀st'::state. state.Gas st' < state.Gas (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ⟶ Qe ad iv st'"
          proof (rule allI,rule impI)
            fix st'::state
            assume "state.Gas st' < state.Gas (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈)"
            then have "state.Gas st' < state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF Contract(2)] msel_ssel_expr_load_rexp_gas(3)[OF Contract(3)] by auto
            then show "Qe ad iv st'" using assm[OF all_gas_le[OF `state.Gas st' < state.Gas st` "1.IH"], THEN conjunct1] by simp
          qed
          moreover have "∀st'::state. state.Gas st' < state.Gas (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈) ⟶
              (∀ev. Address ev ≠ ad
               ⟶ (∀ex cd st0 adex cc v t g g' v' acc.
                     g' ≤ state.Gas st' ∧
                     Type (acc ad) = Some (atype.Contract cname) ∧
                     expr adex ev cd (st0⦇Gas := state.Gas st0 - cc⦈) (state.Gas st0 - cc) = Normal ((KValue ad, Value TAddr), g) ∧
                     expr ex ev cd (st0⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
                     convert t (TUInt b256) v = Some v' ∧
                     transfer (Address ev) ad v' (Accounts st0) = Some acc ∧
                     iv (Storage st0 ad) (⌈Bal (acc ad)⌉ - ⌈v'⌉) ⟶
                     wpS fb (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err)
                      (ffold (init members) (emptyEnv ad cname (Address ev) v') (fmdom members)) emptyTypedStore
                      (st0⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)))" (is "∀st'. ?left st' ⟶ ?right st'")
          proof (rule allI,rule impI)
            fix st'::state
            assume l0: "state.Gas st' < state.Gas (st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈)"
            then have "state.Gas st' < state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF Contract(2)] msel_ssel_expr_load_rexp_gas(3)[OF Contract(3)] by auto
            then show "?right st'" using assm[OF all_gas_le[OF `state.Gas st' < state.Gas st` "1.IH"], THEN conjunct2, THEN conjunct2, THEN conjunct2] unfolding Qfe_def by simp
          qed
          ultimately have "iv (Storage st0'' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st0'' ad)))" using safeStore[of "ffold (init ct0) (emptyEnv adv0 c0 (Address ev) v0') (fmdom ct0)" ad "st⦇Gas := g0', Accounts := acc0, Stack := emptyStore, Memory := emptyTypedStore⦈" iv f0 emptyTypedStore "st0''"] Contract unfolding Qe_def Qfe_def by blast
          then show ?thesis using Contract(9) by simp
        qed
        ultimately show ?thesis by simp
      next
        case (EOA v0 t0 g0 adv0 g0' v0' acc0)
        moreover have "iv (Storage (st⦇Gas := g0', Accounts := acc0⦈) ad) (ReadL⇩i⇩n⇩t (Bal (Accounts (st⦇Gas := g0', Accounts := acc0⦈) ad)))"
        proof -
          from EOA have "adv0 ≠ ad" using a1 by auto
          with a0 a2 EOA have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v0')" by blast
          moreover have "ReadL⇩i⇩n⇩t (Bal (acc0 ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v0'" using transfer_sub[OF EOA(6)] a0 `adv0 ≠ ad` by simp
          ultimately show ?thesis by simp
        qed
        ultimately show ?thesis by simp
      qed
    next
      fix e
      assume "local.stmt (TRANSFER ad' ex) ev cd st = Exception e"
      show "e = Gas ∨ e = Err" using ex.nchotomy by simp
    qed
  next
    fix ev i xe cd fp
    assume a0: "Type (Accounts st ad) = Some (atype.Contract cname)"
       and ad_ev: "Address ev = ad"
       and a1: "Contract ev = cname"
       and pre: "∀fp e⇩l cd⇩l k⇩l m⇩l g.
          local.load False fp xe (ffold (init members) (emptyEnv ad (Contract ev) (Sender ev) (Svalue ev)) (fmdom members)) emptyTypedStore emptyStore (Memory st) ev cd (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) (state.Gas st - costs (INVOKE i xe) ev cd st) =
          Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g) ⟶
          pre i (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad, e⇩l, cd⇩l, k⇩l, m⇩l)"
    show "wpS (INVOKE i xe) (λst. post i (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) ev cd st"
      unfolding wpS_def wp_def
    proof (split result.split; split prod.split; rule conjI; (rule allI)+; (rule impI)+)
      fix x1 x1a st'
      assume "x1 = (x1a, st')"
         and *: "local.stmt (INVOKE i xe) ev cd st = Normal x1"
      then have "local.stmt (INVOKE i xe) ev cd st = Normal (x1a, st')" by simp
      then show "post i (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)), Storage st' ad)"
      proof (cases rule: invoke)
        case (1 ct fb fp f e⇩l cd⇩l k⇩l m⇩l g st'')
        have "post i (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)), Storage st' ad)"
        proof -
          from * have "state.Gas st > costs (INVOKE i xe) ev cd st" by (simp add:stmt.simps split:if_split_asm)
          then have "state.Gas (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) < state.Gas st" using invoke_not_zero[of i xe ev cd st] by simp

          from a1 have "ct = members" using 1(2) C1 by simp
          then have **: "local.load False fp xe (ffold (init members) (emptyEnv ad (Contract ev) (Sender ev) (Svalue ev)) (fmdom members)) emptyTypedStore
          emptyStore (Memory st) ev cd (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈)
          (state.Gas st - costs (INVOKE i xe) ev cd st) =
          Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g)" using 1(4) ad_ev by simp
          moreover from 1(2,3) have ***: "members $$ i = Some (Method (fp, False, f))" using ad_ev `ct = members` by simp
          ultimately have "pre i (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad, e⇩l, cd⇩l, k⇩l, m⇩l)" using pre by blast
          moreover have "g ≤ state.Gas (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈)" using msel_ssel_expr_load_rexp_gas(4)[OF 1(4),THEN conjunct1] by simp
          ultimately have "wpS f (λst. post i (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l
            (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈)" using assm[OF all_gas_le[OF `state.Gas (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) < state.Gas st` "1.IH"], THEN conjunct2, THEN conjunct1] ** *** ad_ev a1 unfolding Qi_def by simp
          then show ?thesis unfolding wpS_def wp_def using 1(5,6) by simp
        qed
        then show ?thesis by simp
      qed
    next
      fix e
      assume "local.stmt (INVOKE i xe) ev cd st = Exception e"
      show "e = Gas ∨ e = Err" using ex.nchotomy by simp
    qed
  next
    fix ev ex ad' cd
    assume a0: "Type (Accounts st ad) = Some (atype.Contract cname)"
      and ad_ev: "Address ev = ad"
      and a1: "∀adv g.
          local.expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈)
           (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g) ⟶ adv = ad"
      and a2: "∀g v t g'.
          local.expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈)
           (state.Gas st - costs (TRANSFER ad' ex) ev cd st) =
          Normal ((KValue ad, Value TAddr), g) ∧
          local.expr ex ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ⟶
          pref (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)"
    show "wpS (TRANSFER ad' ex) (λst. postf (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) ev cd st"
      unfolding wpS_def wp_def
    proof (split result.split; split prod.split; rule conjI; (rule allI)+; (rule impI)+)
      fix x1 x1a st'
      assume "x1 = (x1a, st')" and "local.stmt (TRANSFER ad' ex) ev cd st = Normal x1"
      then have 2: "local.stmt (TRANSFER ad' ex) ev cd st = Normal (x1a, st')" by simp
      then show "postf (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)), Storage st' ad)"
      proof (cases rule: transfer)
        case (Contract v t g adv c g' v' acc ct cn f st'')
        moreover from Contract have "adv = ad" using a1 by auto
        ultimately have "pref (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)" using ad_ev a2 by auto
        moreover have "ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) = ReadL⇩i⇩n⇩t (Bal (acc ad))" using transfer_same[OF Contract(7)] `adv = ad` ad_ev by simp
        ultimately have "pref (ReadL⇩i⇩n⇩t (Bal (acc ad)), Storage st ad)" by simp
        moreover from a0 have "c = cname" using Contract(5) `adv = ad` by simp
        then have "ct = members" and "f = fb" using C1 Contract(6) by simp+
        moreover have "state.Gas st ≥ costs (TRANSFER ad' ex) ev cd st" using 2 by (simp add:stmt.simps split:if_split_asm)
        then have "state.Gas (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) < state.Gas st" using transfer_not_zero[of ad' ex ev cd st] by simp
        moreover have "g' ≤ state.Gas (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈)" using msel_ssel_expr_load_rexp_gas(3)[OF Contract(2)] msel_ssel_expr_load_rexp_gas(3)[OF Contract(3)] by simp
        ultimately have "wpS fb (λst. postf (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err)
          (ffold (init members) (emptyEnv ad c (Address ev) v') (fmdom members)) emptyTypedStore
          (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using assm[OF all_gas_le[OF `state.Gas (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) < state.Gas st` "1.IH"], THEN conjunct2, THEN conjunct2, THEN conjunct1] ad_ev Contract `adv = ad` `c = cname` unfolding Qfi_def by blast
        with `ct = members` `f=fb` have "postf (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)), Storage st' ad)" unfolding wpS_def wp_def using Contract(8,9) `adv = ad` by simp
        then show ?thesis by simp
      next
        case (EOA v t g adv g' acc)
        then show ?thesis using a0 a1 by simp
      qed
    next
      fix e
      assume "local.stmt (TRANSFER ad' ex) ev cd st = Exception e"
      show "e = Gas ∨ e = Err" using ex.nchotomy by simp
    qed
  qed
qed

text ‹
  Refined versions of @{thm[source] wp_external_invoke_transfer}.
›

lemma wp_transfer_ext[rule_format]:
  assumes "Type (Accounts st ad) = Some (atype.Contract cname)"
      and "⋀st::state. ⟦∀st'::state. state.Gas st' ≤ state.Gas st ∧ Type (Accounts st' ad) = Some (atype.Contract cname) ⟶ Pe ad iv st' ∧ Pi ad pre post st' ∧ Pfi ad pref postf st' ∧ Pfe ad iv st'⟧
                    ⟹ Qe ad iv st ∧ Qi ad pre post st ∧ Qfi ad pref postf st ∧ Qfe ad iv st"
    shows "(∀ev ex ad' cd.
       Address ev = ad ∧
       (∀adv g.
         expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)
        ⟶ adv ≠ ad) ∧
       (∀adv g v t g' v'.
         expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g) ∧
         adv ≠ ad ∧
         expr ex ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
         convert t (TUInt b256) v = Some v'
        ⟶ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v'))
      ⟶ wpS (TRANSFER ad' ex) (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) ev cd st)"
proof -
  from wp_external_invoke_transfer have "Pfe ad iv st" using assms by blast
  then show ?thesis using Pfe_def by simp
qed

lemma wp_external[rule_format]:
  assumes "Type (Accounts st ad) = Some (atype.Contract cname)"
     and "⋀st::state. ⟦∀st'::state. state.Gas st' ≤ state.Gas st ∧ Type (Accounts st' ad) = Some (atype.Contract cname)⟶ Pe ad iv st' ∧ Pi ad pre post st' ∧ Pfi ad pref postf st' ∧ Pfe ad iv st'⟧
                    ⟹ Qe ad iv st ∧ Qi ad pre post st ∧ Qfi ad pref postf st ∧ Qfe ad iv st"
  shows "(∀ev ad' i xe val cd.
       Address ev = ad ∧
       (∀adv c g v t g' v'.
         expr ad' ev cd (st⦇Gas := state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) (state.Gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g) ∧
         adv ≠ ad ∧
         Type (Accounts st adv) = Some (atype.Contract c) ∧
         c |∈| fmdom ep ∧
         expr val ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
         convert t (TUInt b256) v = Some v'
        ⟶ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) - ReadL⇩i⇩n⇩t v'))
      ⟶ wpS (EXTERNAL ad' i xe val) (λst. iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))) (λe. e = Gas ∨ e = Err) ev cd st)"
proof -
  from wp_external_invoke_transfer have "Pe ad iv st" using assms by blast
  then show ?thesis using Pe_def by simp
qed

lemma wp_invoke[rule_format]:
  assumes "Type (Accounts st ad) = Some (atype.Contract cname)"
      and "⋀st::state. ⟦∀st'::state. state.Gas st' ≤ state.Gas st ∧ Type (Accounts st' ad) = Some (atype.Contract cname) ⟶ Pe ad iv st' ∧ Pi ad pre post st' ∧ Pfi ad pref postf st' ∧ Pfe ad iv st'⟧
                    ⟹ Qe ad iv st ∧ Qi ad pre post st ∧ Qfi ad pref postf st ∧ Qfe ad iv st"
  shows "(∀ev i xe cd.
       Address ev = ad ∧
       Contract ev = cname ∧
       (∀fp e⇩l cd⇩l k⇩l m⇩l g.
         load False fp xe (ffold (init members) (emptyEnv ad (Contract ev) (Sender ev) (Svalue ev)) (fmdom members)) emptyTypedStore emptyStore (Memory st) ev cd (st⦇Gas := state.Gas st - costs (INVOKE i xe) ev cd st⦈) (state.Gas st - costs (INVOKE i xe) ev cd st) = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g)
        ⟶ pre i (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad, e⇩l, cd⇩l, k⇩l, m⇩l))
    ⟶ wpS (INVOKE i xe) (λst. post i (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) ev cd st)"
proof -
  from wp_external_invoke_transfer have "Pi ad pre post st" using assms by blast
  then show ?thesis using Pi_def by simp
qed

lemma wp_transfer_int[rule_format]:
  assumes "Type (Accounts st ad) = Some (atype.Contract cname)"
      and "⋀st::state. ⟦∀st'::state. state.Gas st' ≤ state.Gas st ∧ Type (Accounts st' ad) = Some (atype.Contract cname) ⟶ Pe ad iv st' ∧ Pi ad pre post st' ∧ Pfi ad pref postf st' ∧ Pfe ad iv st'⟧
                    ⟹ Qe ad iv st ∧ Qi ad pre post st ∧ Qfi ad pref postf st ∧ Qfe ad iv st"
    shows "(∀ev ex ad' cd.
     Address ev = ad ∧
     (∀adv g.
       expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue adv, Value TAddr), g)
      ⟶ adv = ad) ∧
     (∀g v t g'.
       expr ad' ev cd (st⦇Gas := state.Gas st - costs (TRANSFER ad' ex) ev cd st⦈) (state.Gas st - costs (TRANSFER ad' ex) ev cd st) = Normal ((KValue ad, Value TAddr), g) ∧
       expr ex ev cd (st⦇Gas := g⦈) g = Normal ((KValue v, Value t), g')
      ⟶ pref (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad))
    ⟶ wpS (TRANSFER ad' ex) (λst. postf (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)), Storage st ad)) (λe. e = Gas ∨ e = Err) ev cd st)"
proof -
  from wp_external_invoke_transfer have "Pfi ad pref postf st" using assms by blast
  then show ?thesis using Pfi_def by simp
qed

definition constructor :: "((String.literal, String.literal) fmap ⇒ int ⇒ bool) ⇒ bool"
  where "constructor iv ≡ (∀acc g'' m⇩l k⇩l cd⇩l e⇩l g' t v v' xe i cd val st ev adv st0.
    st0 = st⦇Gas := state.Gas st - costs (NEW i xe val) ev cd st⦈ ∧
    adv = hash_version (Address ev) (ShowL⇩n⇩a⇩t (Contracts (Accounts st0 (Address ev)))) ∧
    Type (Accounts st0 adv) = None ∧
    expr val ev cd st0 (state.Gas st0) = Normal ((KValue v, Value t), g') ∧
    convert t (TUInt b256) v = Some v' ∧
    load True (fst const) xe (ffold (init members) (emptyEnv adv cname (Address ev) v') (fmdom members)) emptyTypedStore emptyStore emptyTypedStore ev cd (st0⦇Gas := g', Accounts := (Accounts st0)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract cname), Contracts = 0⦈), Storage:=(Storage st0)(adv := {$$})⦈) g' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g'') ∧
    transfer (Address ev) adv v' ((Accounts st0)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract cname), Contracts = 0⦈)) = Some acc
    ⟶ wpS (snd const) (λst. iv (Storage st adv) ⌈Bal (Accounts st adv)⌉) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l
        (st0⦇Gas := g'', Storage:=(Storage st0)(adv := {$$}), Accounts := acc, Stack:=k⇩l, Memory:=m⇩l⦈))"

lemma invariant_rec:
  fixes iv ad
  assumes "∀ad (st::state). Qe ad iv st"
      and "∀ad (st::state). Qfe ad iv st"
      and "constructor iv"
      and "Address ev ≠ ad"
      and "Type (Accounts st ad) = Some (atype.Contract cname) ⟶ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))"
    shows "∀(st'::state). stmt f ev cd st = Normal ((), st') ∧ Type (Accounts st' ad) = Some (atype.Contract cname)
            ⟶ iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
  using assms(4-)
proof (induction rule:stmt.induct)
  case (1 ev cd st)
  show ?case
  proof elims
    fix st'
    assume *: "stmt SKIP ev cd st = Normal ((), st')"
       and "Type (Accounts st' ad) = Some (atype.Contract cname)"
    then show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉" using 1 skip[OF *] by simp
  qed
next
  case (2 lv ex ev cd st)
  show ?case
  proof elims
    fix st'
    assume *: "stmt (ASSIGN lv ex) ev cd st = Normal ((), st')"
       and "Type (Accounts st' ad) = Some (atype.Contract cname)"
    then show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉" using 2 by (cases rule: assign[OF *];simp)
  qed
next
  case (3 s1 s2 ev cd st)
  show ?case
  proof elims
    fix st'
    assume *: "stmt (COMP s1 s2) ev cd st = Normal ((), st')"
       and **: "Type (Accounts st' ad) = Some (atype.Contract cname)"
      show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule: comp[OF *])
      case (1 st'')
      moreover from 3(4) have "Type (Accounts (st⦇Gas := state.Gas st - costs (COMP s1 s2) ev cd st⦈) ad) = Some (atype.Contract cname) ⟶ iv (Storage (st⦇Gas := state.Gas st - costs (COMP s1 s2) ev cd st⦈) ad) ⌈Bal (Accounts (st⦇Gas := state.Gas st - costs (COMP s1 s2) ev cd st⦈) ad)⌉" by auto
      ultimately have "Type (Accounts st'' ad) = Some (atype.Contract cname) ⟶ iv (Storage st'' ad) ⌈Bal (Accounts st'' ad)⌉" using 3(1)[OF _ _ 3(3)] by fastforce
      then show ?thesis using 3(2)[OF _ _ _ 3(3)] 1 ** by fastforce
    qed
  qed
next
  case (4 ex s1 s2 ev cd st)
  show ?case
  proof elims
    fix st'
    assume a1: "local.stmt (ITE ex s1 s2) ev cd st = Normal ((), st')"
       and a2: "Type (Accounts st' ad) = Some (atype.Contract cname)"
      show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule:ite[OF a1])
      case (1 g)
      have "∀st'. local.stmt s1 ev cd (st⦇Gas := g⦈) = Normal ((), st') ∧
          Type (Accounts st' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
        apply (rule 4(1)) using 1 4(3) 4(4) by auto
      then show ?thesis using a2 1(3) by blast
    next
      case (2 g)
      have "∀st'. local.stmt s2 ev cd (st⦇Gas := g⦈) = Normal ((), st') ∧
          Type (Accounts st' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
        apply (rule 4(2)) using 2 4(3) 4(4) true_neq_false[symmetric] by auto
      then show ?thesis using a2 2(3) by blast
    qed
  qed
next
  case (5 ex s0 ev cd st)
  show ?case
  proof elims
    fix st'
    assume a1: "local.stmt (WHILE ex s0) ev cd st = Normal ((), st')"
       and a2: "Type (Accounts st' ad) = Some (atype.Contract cname)"
      show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule:while[OF a1])
      case (1 g st'')
      have "∀st'. local.stmt s0 ev cd (st⦇Gas := g⦈) = Normal ((), st') ∧
          Type (Accounts st' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
        apply (rule 5(1)) using 1 5(3) 5(4) by auto
      then have *: "Type (Accounts st'' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st'' ad) ⌈Bal (Accounts st'' ad)⌉" using 1(3) by simp
      have "∀st'. local.stmt (WHILE ex s0) ev cd st'' = Normal ((), st') ∧
          Type (Accounts st' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
        apply (rule 5(2)) using 1 5(3) 5(4) * by auto
      then show ?thesis using a2 1(4) by blast
    next
      case (2 g)
      then show ?thesis using a2 5(4) by simp
    qed
  qed
next
  case (6 i xe ev cd st)
  show ?case
  proof elims
    fix st'
    assume a1: "local.stmt (INVOKE i xe) ev cd st = Normal ((), st')"
       and a2: "Type (Accounts st' ad) = Some (atype.Contract cname)"
    show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule:invoke[OF a1])
      case (1 ct fb fp f e⇩l cd⇩l k⇩l m⇩l g st'')
      from 6(2) have "ad ≠ Address e⇩l" using msel_ssel_expr_load_rexp_gas(4)[OF 1(4)] ffold_init_ad by simp
      have "∀st'. local.stmt f e⇩l cd⇩l (st⦇Gas := g, Stack := k⇩l, Memory := m⇩l⦈) = Normal ((), st') ∧ Type (Accounts st' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉" apply (rule 6(1)) using 1 6(3) `ad ≠ Address e⇩l` by auto
      then show ?thesis using a2 1(5,6) by auto
    qed
  qed
next
  case (7 adex i xe val ev cd st)
  show ?case
  proof elims
    fix st'
    assume a1: "local.stmt (EXTERNAL adex i xe val) ev cd st = Normal ((), st')"
       and a2: "Type (Accounts st' ad) = Some (atype.Contract cname)"
    show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule:external[OF a1])
      case (1 adv c g ct cn fb' v t g' v' fp f e⇩l cd⇩l k⇩l m⇩l g'' acc st'')
      then show ?thesis
      proof (cases "adv = ad")
        case True
        then have "Type (acc ad) = Some (atype.Contract c)" using transfer_type_same[OF 1(10)] 1(4) by auto
        moreover from `Type (acc ad) = Some (atype.Contract c)` have "Type (Accounts st' ad) = Some (atype.Contract c)" using atype_same[OF 1(11)] 1(12) by simp
        then have "c = cname" using a2 by simp
        moreover from `c = cname` have "ct = members" using 1 C1 by simp
        moreover have "g'' ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] msel_ssel_expr_load_rexp_gas(3)[OF 1(6)] msel_ssel_expr_load_rexp_gas(4)[OF 1(9)] by linarith
        moreover have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')"
        proof -
          from `c = cname` have "Type (Accounts st ad) = Some (atype.Contract cname)" using 1(4) True by simp
          have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" using 7(4) `Type (Accounts st ad) = Some (atype.Contract cname)` by simp
          moreover have "ReadL⇩i⇩n⇩t (Bal (acc ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) + ReadL⇩i⇩n⇩t v'" using transfer_add[OF 1(10)] 7(3) True by simp
          ultimately show ?thesis by simp
        qed
        ultimately have "wpS f (λst. iv (Storage st ad) ⌈Bal (Accounts st ad)⌉) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l
        (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈)" using 1 True  using assms(1) 1(8) 7(3) unfolding Qe_def by simp
        then show ?thesis unfolding wpS_def wp_def using 1(11,12) by simp
      next
        case False
        then have *: "ad ≠ Address e⇩l" using msel_ssel_expr_load_rexp_gas(4)[OF 1(9)] ffold_init_ad by simp
        moreover have **:"Type (acc ad) = Some (atype.Contract cname) ⟶ iv (Storage st ad) ⌈Bal (acc ad)⌉"
        proof
          assume "Type (acc ad) = Some (atype.Contract cname)"
          then have "Type (Accounts st ad) = Some (atype.Contract cname)" using transfer_type_same[OF 1(10)] by simp
          then have "iv (Storage st ad) ⌈Bal (Accounts st ad)⌉" using 7(4) by simp
          moreover have "Bal (acc ad) = Bal (Accounts st ad)" using transfer_eq[OF 1(10)] 7(3) False by simp
          ultimately show "iv (Storage st ad) ⌈Bal (acc ad)⌉" by simp
        qed
        ultimately have "∀st'. local.stmt f e⇩l cd⇩l (st⦇Gas := g'', Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) = Normal ((), st') ∧
         Type (Accounts st' ad) = Some (atype.Contract cname) ⟶  iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
          using 7(1) 1 by auto
        then show ?thesis using a2 1(11,12) by simp
      qed
    next
      case (2 adv c g ct cn fb' v t g' v' acc st'')
      then show ?thesis
      proof (cases "adv = ad")
        case True
        then have "Type (acc ad) = Some (atype.Contract c)" using transfer_type_same[OF 2(9)] 2(4) by auto
        moreover from `Type (acc ad) = Some (atype.Contract c)` have "Type (Accounts st' ad) = Some (atype.Contract c)" using atype_same[OF 2(10)] 2(11) by simp
        then have "c = cname" using a2 by simp
        moreover from `c = cname` have "ct = members" and "fb'=fb" using 2 C1 by simp+
        moreover have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')"
        proof -
          from `c = cname` have "Type (Accounts st ad) = Some (atype.Contract cname)" using 2(4) True by simp
          then have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" using 7(4) by simp
          moreover have "ReadL⇩i⇩n⇩t (Bal (acc ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) + ReadL⇩i⇩n⇩t v'" using transfer_add[OF 2(9)] 7(3) True by simp
          ultimately show "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')" by simp
        qed
        moreover have "g' ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 2(2)] msel_ssel_expr_load_rexp_gas(3)[OF 2(6)] by linarith
        ultimately have "wpS fb' (λst. iv (Storage st ad) ⌈Bal (Accounts st ad)⌉) (λe. e = Gas ∨ e = Err)
          (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) emptyTypedStore
          (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using assms(2) 7(3) 2 True unfolding Qfe_def by simp
        then show ?thesis unfolding wpS_def wp_def using 2(10,11) by simp
      next
        case False
        moreover have **:"Type (acc ad) = Some (atype.Contract cname) ⟶ iv (Storage st ad) ⌈Bal (acc ad)⌉"
        proof
          assume "Type (acc ad) = Some (atype.Contract cname)"
          then have "Type (Accounts st ad) = Some (atype.Contract cname)" using transfer_type_same[OF 2(9)] by simp
          then have "iv (Storage st ad) ⌈Bal (Accounts st ad)⌉" using 7(4) by simp
          moreover have "Bal (acc ad) = Bal (Accounts st ad)" using transfer_eq[OF 2(9)] 7(3) False by simp
          ultimately show "iv (Storage st ad) ⌈Bal (acc ad)⌉" by simp
        qed
        ultimately have "∀st'. local.stmt fb' (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) emptyTypedStore (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) = Normal ((), st') ∧
         Type (Accounts st' ad) = Some (atype.Contract cname) ⟶  iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
          using 7(2) 2 by auto
        then show ?thesis using a2 2(10,11) by simp
      qed
    qed
  qed
next
  case (8 ad' ex ev cd st)
  show ?case
  proof elims
    fix st'
    assume a1: "local.stmt (TRANSFER ad' ex) ev cd st = Normal ((), st')"
       and a2: "Type (Accounts st' ad) = Some (atype.Contract cname)"
    show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule:transfer[OF a1])
      case (1 v t g adv c g' v' acc ct cn f st'')
      then show ?thesis
      proof (cases "adv = ad")
        case True
        then have "Type (acc ad) = Some (atype.Contract c)" using transfer_type_same[OF 1(7)] 1(5) by auto
        moreover from `Type (acc ad) = Some (atype.Contract c)` have "Type (Accounts st' ad) = Some (atype.Contract c)" using atype_same[OF 1(8)] 1(9) by simp
        then have "c = cname" using a2 by simp
        moreover from `c = cname` have "ct = members" and "f=fb" using 1 C1 by simp+
        moreover have "g' ≤ state.Gas st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] msel_ssel_expr_load_rexp_gas(3)[OF 1(3)] by linarith
        moreover have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')"
        proof -
          from `c = cname` have "Type (Accounts st ad) = Some (atype.Contract cname)" using 1(5) True by simp
          then have "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))" using 8(3) by simp
          moreover have "ReadL⇩i⇩n⇩t (Bal (acc ad)) = ReadL⇩i⇩n⇩t (Bal (Accounts st ad)) + ReadL⇩i⇩n⇩t v'" using transfer_add[OF 1(7)] 8(2) True by simp
          ultimately show "iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (acc ad)) - ReadL⇩i⇩n⇩t v')" by simp
        qed
        ultimately have "wpS f (λst. iv (Storage st ad) ⌈Bal (Accounts st ad)⌉) (λe. e = Gas ∨ e = Err)
          (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) emptyTypedStore
          (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈)" using assms(2) 8(2) 1 True unfolding Qfe_def by simp
        then show ?thesis unfolding wpS_def wp_def using 1(8,9) by simp
      next
        case False
        moreover have "Type (acc ad) = Some (atype.Contract cname) ⟶ iv (Storage st ad) ⌈Bal (acc ad)⌉"
        proof
          assume "Type (acc ad) = Some (atype.Contract cname)"
          then have "Type (Accounts st ad) = Some (atype.Contract cname)" using transfer_type_same[OF 1(7)] by simp
          then have "iv (Storage st ad) ⌈Bal (Accounts st ad)⌉" using 8(3) by simp
          moreover have "Bal (acc ad) = Bal (Accounts st ad)" using transfer_eq[OF 1(7)] 8(2) False by simp
          ultimately show "iv (Storage st ad) ⌈Bal (acc ad)⌉" by simp
        qed
        ultimately have "∀st'. local.stmt f (ffold (init ct) (emptyEnv adv c (Address ev) v') (fmdom ct)) emptyTypedStore
          (st⦇Gas := g', Accounts := acc, Stack := emptyStore, Memory := emptyTypedStore⦈) = Normal ((), st') ∧ Type (Accounts st' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉" using 8(1) 1 by auto
        then show ?thesis using a2 1(8, 9) by simp
      qed
    next
      case (2 v t g adv g' v' acc)
      then show ?thesis
      proof (cases "adv = ad")
        case True
        then show ?thesis using 2(5,7) a2 transfer_type_same[OF 2(6)] by simp
      next
        case False
        then have "Bal (acc ad) = Bal (Accounts st ad)" using transfer_eq[OF 2(6)] 8(2) by simp
        moreover have "Type (Accounts st ad) = Some (atype.Contract cname)" using transfer_type_same[OF 2(6)] 2(7) a2 by simp
        then have "iv (Storage st ad) ⌈Bal (Accounts st ad)⌉" using 8(3) by simp
        ultimately show ?thesis using 2(7) by simp
      qed
    qed
  qed
next
  case (9 id0 tp s e cd st)
  show ?case
  proof elims
    fix st'
    assume a1: "local.stmt (BLOCK (id0, tp, None) s) e cd st = Normal ((), st')"
       and a2: "Type (Accounts st' ad) = Some (atype.Contract cname)"
    show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule:blockNone[OF a1])
      case (1 cd' mem' sck' e')
      have "Address e' = Address e" using decl_env[OF 1(2)] by simp
      have "∀st'. local.stmt s e' cd' (st⦇Gas := state.Gas st - costs (BLOCK (id0, tp, None) s) e cd st, Stack := sck',
           Memory := mem'⦈) = Normal ((), st') ∧
          Type (Accounts st' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
        apply (rule 9(1)) using 1 9(2,3) `Address e' = Address e` by auto
      then show ?thesis using a2 1(3) by blast
    qed
  qed
next
  case (10 id0 tp ex' s e cd st)
  show ?case
  proof elims
    fix st'
    assume a1: "local.stmt (BLOCK (id0, tp, Some ex') s) e cd st = Normal ((), st')"
       and a2: "Type (Accounts st' ad) = Some (atype.Contract cname)"
    show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule:blockSome[OF a1])
      case (1 v t g cd' mem' sck' e')
      have "Address e' = Address e" using decl_env[OF 1(3)] by simp
      have "∀st'. local.stmt s e' cd' (st⦇Gas := g, Stack := sck', Memory := mem'⦈) = Normal ((), st') ∧
          Type (Accounts st' ad) = Some (atype.Contract cname) ⟶
          iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
        apply (rule 10(1)) using 1 10(2,3) `Address e' = Address e` by auto
      then show ?thesis using a2 1(4) by blast
    qed
  qed
next
  case (11 i xe val e cd st)
  show ?case
  proof elims
    fix st'
    assume a1: "local.stmt (NEW i xe val) e cd st = Normal ((), st')"
       and a2: "Type (Accounts st' ad) = Some (atype.Contract cname)"
    show "iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
    proof (cases rule:new[OF a1])
      case (1 v t g ct cn fb' e⇩l cd⇩l k⇩l m⇩l g' acc st'' v')
      define adv where "adv = hash_version (Address e) ⌊Contracts (Accounts (st⦇Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) (Address e))⌋"
      then have "Address e⇩l = adv" using msel_ssel_expr_load_rexp_gas(4)[OF 1(6)] by simp
      then show ?thesis
      proof (cases "adv = ad")
        case True
        then show ?thesis
        proof (cases "i = cname")
          case t0: True
          then have "ct = members" and "cn = const" and "fb' = fb" using 1(5) C1 by simp+
          then have "wpS (snd const) (λst. iv (Storage st adv) ⌈Bal (Accounts st adv)⌉) (λe. e = Gas ∨ e = Err) e⇩l cd⇩l
            (st⦇Gas := g', Storage:=(Storage st)(adv := {$$}), Accounts := acc, Stack:=k⇩l, Memory:=m⇩l⦈)"
            using assms(3) 11(3) 1 True adv_def t0 unfolding constructor_def by auto
          then have "iv (Storage st'' adv) ⌈Bal (Accounts st'' adv)⌉" unfolding wpS_def wp_def using 1(8) `cn = const` adv_def by simp
          then show ?thesis using 1(9) True by simp
        next
          case False
          moreover have "Type (Accounts st' ad) = Some (atype.Contract i)"
          proof -
            from `adv = ad` have "Type (((Accounts st) (adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈)) ad) = Some (atype.Contract i)" by simp
            then have "Type (acc ad) = Some (atype.Contract i)" using transfer_type_same[OF 1(7)] adv_def by simp
            then have "Type (Accounts st'' ad) = Some (atype.Contract i)" using atype_same[OF 1(8)] adv_def by simp
            then show ?thesis using 1(9) by simp
          qed
          ultimately show ?thesis using a2 by simp
        qed
      next
        case False
        define st0 where "st0 = st⦇Gas := state.Gas st - costs (NEW i xe val) e cd st⦈"
        define st1 where "st1 = st⦇Gas := g, Accounts := (Accounts st)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage := (Storage st)(adv := {$$})⦈"
        define st2 where "st2 = st1⦇Gas := g'⦈"
        define st3 where "st3 = st2⦇Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈"

        have aux1: "Type (acc ad) = Some (atype.Contract cname) ⟶ iv (Storage (st⦇Storage:=(Storage st)(adv := {$$}), Accounts:=acc⦈) ad) ⌈Bal (acc ad)⌉"
        proof
          assume "Type (acc ad) = Some (atype.Contract cname)"
          then have "Type (((Accounts st) (adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈)) ad) = Some (atype.Contract cname)"
            using transfer_type_same[OF 1(7)] adv_def by simp
          then have "Type ((Accounts st) ad) = Some (atype.Contract cname)" using False by simp
          then have "iv (Storage st ad) ⌈Bal (Accounts st ad)⌉" using 11(3) by simp
          then have "iv (Storage (st⦇Storage:=(Storage st)(adv := {$$})⦈) ad) ⌈Bal (Accounts st ad)⌉" using False by simp
          then show "iv (Storage (st⦇Storage:=(Storage st)(adv := {$$}), Accounts:=acc⦈) ad) ⌈Bal (acc ad)⌉"
            using transfer_eq[OF 1(7)] adv_def 11(2) False by simp
        qed

        have b1: "assert Gas (λst. costs (NEW i xe val) e cd st < state.Gas st) st = Normal ((), st)" using 1(1) by simp
        have b2: "modify (λst. st⦇Gas := state.Gas st - costs (NEW i xe val) e cd st⦈) st = Normal ((), st0)" using st0_def by simp
        have b3: "applyf (λst. hash_version (Address e) ⌊Contracts (Accounts st (Address e))⌋) st0 = Normal (adv, st0)" using adv_def st0_def by simp
        have b4: "assert Err (λst. Type (Accounts st adv) = None) st0 = Normal ((), st0)" using 1(2) st0_def adv_def by simp
        have b5: "toState (expr val e cd) st0 = Normal ((KValue v, Value t), st0⦇Gas := g⦈)" using 1(3) st0_def by simp
        have b6: "(case (KValue v, Value t) of (KValue v, Value t) ⇒ return (v, t) | _ ⇒ throw Err) (st0⦇Gas := g⦈) = Normal ((v, t), st0⦇Gas := g⦈)" by simp
        then have b7: "return (v, t) (st0⦇Gas := g⦈) = Normal ((v, t), st0⦇Gas := g⦈)" by simp
        have b8: "option Err (λ_. convert t (TUInt b256) v) (st0⦇Gas := g⦈) = Normal (v', st0⦇Gas := g⦈)" using 1(4) by simp
        have b9: "option Err (λ_. ep $$ i) (st0⦇Gas := g⦈) = Normal ((ct, cn, fb'), st0⦇Gas := g⦈)" using 1(5) by simp
        have b10: "modify (λst. st⦇Accounts := (Accounts st)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage := (Storage st)(adv := {$$})⦈) (st0⦇Gas := g⦈) = Normal ((), st1)" using st1_def st0_def by simp
        have b11: "toState
     (local.load True (fst cn) xe (ffold_init ct (emptyEnv adv i (Address e) v') (fmdom ct)) emptyTypedStore emptyStore
       emptyTypedStore e cd)
     st1 = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), st2)" using 1(6) st1_def st2_def st0_def adv_def by simp
        have b12: "option Err (λst. transfer (Address e) adv v' (Accounts st)) st2 = Normal (acc, st2)" using 1(7) st2_def st1_def st0_def adv_def by simp
        have b13: "applyf (λst. (Stack st, Memory st)) st2 = Normal ((Stack st, Memory st), st2)" 
          using st1_def st2_def by auto
        have b14: "modify (λst. st⦇Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈) st2 = Normal ((), st3)" using st3_def by simp

        (* Show st3 equals the state where stmt is executed in 1(8) *)
        have st3_eq: "st3 = st⦇Gas := g', Accounts := (Accounts st)(adv := ⦇Bal = ShowL⇩i⇩n⇩t 0, Type = Some (atype.Contract i), Contracts = 0⦈), Storage := (Storage st)(adv := {$$}), Accounts := acc, Stack := k⇩l, Memory := m⇩l⦈"
          using st3_def st2_def st1_def by simp

        have "Address e⇩l ≠ ad" using `Address e⇩l = adv` False by simp
        moreover have "Type (Accounts st3 ad) = Some (atype.Contract cname) ⟶ iv (Storage st3 ad) ⌈Bal (Accounts st3 ad)⌉"
          using aux1 st3_def st2_def st1_def st0_def by simp
        ultimately have stmt_ih: "∀st'. stmt (snd cn) e⇩l cd⇩l st3 = Normal ((), st') ∧ Type (Accounts st' ad) = Some (atype.Contract cname) ⟶ iv (Storage st' ad) ⌈Bal (Accounts st' ad)⌉"
          using 11(1)[OF b1 b2 b3 b4 b5 b6 refl b8 b9 refl refl b10 refl b11 refl refl refl b12 b13 refl b14] by blast

        (* Now use st3_eq to connect to 1(8) *)
        have "stmt (snd cn) e⇩l cd⇩l st3 = Normal ((), st'')" using 1(8) st3_eq 
          using adv_def by fastforce
        moreover have "Type (Accounts st'' ad) = Some (atype.Contract cname)" using 1(9) a2 adv_def by auto
        ultimately show ?thesis using stmt_ih 1(9) by simp
      qed
    qed
  qed
qed

theorem invariant:
  fixes iv ad
  assumes "∀ad (st::state). Qe ad iv st"
      and "∀ad (st::state). Qfe ad iv st"
      and "constructor iv"
      and "∀ad. Type (Accounts st ad) = Some (atype.Contract cname) ⟶ iv (Storage st ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st ad)))"
    shows "∀(st'::state) ad. stmt f ev cd st = Normal ((), st') ∧ Type (Accounts st' ad) = Some (atype.Contract cname) ∧ Address ev ≠ ad
            ⟶ iv (Storage st' ad) (ReadL⇩i⇩n⇩t (Bal (Accounts st' ad)))"
  using assms invariant_rec by blast
end

context Calculus
begin

  named_theorems external
  named_theorems internal

  section ‹Verification Condition Generator›
  
  text ‹
    To use the verification condition generator first invoke the following rule on the original Hoare triple:
  ›
  method vcg_valid =
    rule wpS_valid,
    erule conjE,
    simp
  
  method external uses cases =
    unfold Qe_def,
    elims,
    (erule cases;simp)
  
  method fallback uses cases =
    unfold Qfe_def,
    elims,
    rule cases,
    simp
  
  method constructor uses cases =
    unfold constructor_def,
    elims,
    rule cases,
    simp
  
  text ‹
    Then apply the correct rules from the following set of rules.
  ›
  
  subsection ‹Skip›
  
  method vcg_skip =
    rule wp_Skip;(solve simp)?
  
  subsection ‹Assign›
  
  method vcg_assign uses wp_rule expr_rule lexp_rule =
    rule wp_rule,
    simp add: expr_rule lexp_rule,
    simp

  subsection ‹Composition›
  
  method vcg_comp =
    rule wp_Comp; simp

  subsection ‹Blocks›
  
  method vcg_block_some =
    rule wp_blockSome; simp
end

locale VCG = Calculus +
  fixes iv::invariant
    and pref::"postcondition"
    and postf::"postcondition"
    and pre::"Identifier ⇒ precondition"
    and post::"Identifier ⇒ postcondition"
begin

subsection ‹Transfer›
text ‹
  The following rule can be used to verify an invariant for a transfer statement.
  It requires four term parameters:
  ▪ @{term[show_types] "iv::invariant"}: Invariant
  ▪ @{term[show_types] "pref::postcondition"}: Precondition for fallback method called internally
  ▪ @{term[show_types] "postf::postcondition"}: Postcondition for fallback method called internally
  ▪ @{term[show_types] "pre::Identifier ⇒ precondition"}: Preconditions for internal methods
  ▪ @{term[show_types] "post::Identifier ⇒ postcondition"}: Postconditions for internal methods


  In addition it requires 8 facts:
  ▪ @{term fallback_int}: verifies *postcondition* for body of fallback method invoked *internally*.
  ▪ @{term fallback_ext}: verifies *invariant* for body of fallback method invoked *externally*.
  ▪ @{term cases_ext}: performs case distinction over *external* methods of atype.Contract @{term ad}.
  ▪ @{term cases_int}: performs case distinction over *internal* methods of atype.Contract @{term ad}.
  ▪ @{term cases_fb}: performs case distinction over *fallback* method of atype.Contract @{term ad}.
  ▪ @{term different}: shows that Address of environment is different from @{term ad}.
  ▪ @{term invariant}: shows that invariant holds *before* execution of transfer statement.


  Finally it requires two lists of facts as parameters:
  ▪ @{term external}: verify that the invariant is preserved by the body of external methods.
  ▪ @{term internal}: verify that the postcondition holds after executing the body of internal methods.
›

method vcg_prep =
  (rule allI)+,
  rule impI,
  (erule conjE)+

method vcg_body uses fallback_int fallback_ext cases_ext cases_int cases_fb =
  (rule conjI)?,
  match conclusion in
    "Qe _ _ _" ⇒
      ‹unfold Qe_def,
       vcg_prep,
       erule cases_ext;
        (simp,vcg_prep,
         rule external;
           solve ‹assumption | simp›)›
  ¦ "Qi _ _ _ _" ⇒
      ‹unfold Qi_def,
       vcg_prep,
       erule cases_int;
        (simp,vcg_prep,
         rule internal;
           solve ‹assumption | simp›)›
  ¦ "Qfi _ _ _ _" ⇒
      ‹unfold Qfi_def,
       rule allI,
       rule impI,
       rule cases_fb;
        (simp,vcg_prep,
         rule fallback_int;
           solve ‹assumption | simp›)›
  ¦ "Qfe _ _ _" ⇒
      ‹unfold Qfe_def,
       rule allI,
       rule impI,
       rule cases_fb;
        (simp,vcg_prep,
         rule fallback_ext;
           solve ‹assumption | simp›)›

method decl_load_rec for ad::address and e::environment uses eq decl load empty init =
  match premises in
    d: "decl _ _ _ _ _ _ _ (_, _, _, e') = Some (_, _, _, e)" for e'::environment ⇒
        ‹decl_load_rec ad e' eq:trans_sym[OF eq decl[OF d]] decl:decl load:load empty:empty init:init›
  ¦ l: "load _ _ _ (ffold (init members) (emptyEnv ad cname (Address e') v) (fmdom members)) _ _ _ _ _ _ _ = Normal ((e, _, _, _), _)" for e'::environment and v ⇒
        ‹rule
          trans[
            OF eq
            trans[
              OF load[OF l]
              trans[
                OF init[of (unchecked) members "emptyEnv ad cname (Address e') v" "fmdom members"]
                empty[of (unchecked) ad cname "Address e'" v]]]]›

method sameaddr for ad::address =
  match conclusion in
    "Address e = ad" for e::environment ⇒
      ‹decl_load_rec ad e eq:refl[of "Address e"] decl:decl_env[THEN conjunct1] load:msel_ssel_expr_load_rexp_gas(4)[THEN conjunct2, THEN conjunct1] init:ffold_init_ad empty:emptyEnv_address›

lemma eq_neq_eq_imp_neq:
  "x = a ⟹ b ≠ y ⟹ a = b ⟹ x ≠ y" by simp

method sender for ad::address =
  match conclusion in
    "adv ≠ ad" for adv::address ⇒
      ‹match premises in
        a: "Address e' ≠ ad" and e: "expr SENDER e _ _ _ = Normal ((KValue adv, Value TAddr), _)" for e::environment and e'::environment ⇒
          ‹rule local.eq_neq_eq_imp_neq[OF expr_sender[OF e] a],
           decl_load_rec ad e eq:refl[of "Sender e"] decl:decl_env[THEN conjunct2, THEN conjunct1] load:msel_ssel_expr_load_rexp_gas(4)[THEN conjunct2, THEN conjunct2, THEN conjunct1] init:ffold_init_sender empty:emptyEnv_sender››

method vcg_init for ad::address uses invariant =
  elims,
  sameaddr ad,
  sender ad,
  (rule invariant; assumption)

method vcg_transfer_ext for ad::address
  uses fallback_int fallback_ext cases_ext cases_int cases_fb invariant =
  rule wp_transfer_ext[where pref = pref and postf = postf and pre = pre and post = post and iv=iv],
  solve simp,
  (vcg_body fallback_int:fallback_int fallback_ext:fallback_ext cases_ext:cases_ext cases_int:cases_int cases_fb:cases_fb)+,
  vcg_init ad invariant:invariant

end

end