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 = Memory m ⟹ wp (h m) P E s"
      and "⋀t. a = Storage t ⟹ wp (i t) P E s"
shows "wp (case a of Value v ⇒ f v | Calldata m ⇒ g m | Memory m ⇒ h m | 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›

type_synonym State_Predicate = "Accounts × Stack × MemoryT × (Address ⇒ StorageT) ⇒ bool"

definition validS :: "State_Predicate ⇒ (unit, Ex ,State) state_monad ⇒ State_Predicate ⇒ (Ex ⇒ bool) ⇒ bool" 
  (‹⦃_⦄⇩S/ _ /(⦃_⦄⇩S,/ ⦃_⦄⇩S)›)
where
  "⦃P⦄⇩S f ⦃Q⦄⇩S,⦃E⦄⇩S ≡
     ∀st. P (accounts st, stack st, memory st, storage st)
     ⟶ (case f st of
           Normal (_,st') ⇒ gas st' ≤ gas st ∧ Q (accounts st', stack st', memory st', storage st')
         | Exception e ⇒ E e)"

definition wpS :: "(unit, Ex ,State) state_monad ⇒ (State ⇒ bool) ⇒ (Ex ⇒ bool) ⇒ State ⇒ bool"
  where "wpS f P E st ≡ wp f (λ_ st'. gas st' ≤ gas st ∧ P st') E st"

lemma wpS_valid:
  assumes "⋀st::State. P (accounts st, stack st, memory st, storage st) ⟹ wpS f (λst. Q (accounts st, stack st, memory st, storage st)) E st"
  shows "⦃P⦄⇩S f ⦃Q⦄⇩S,⦃E⦄⇩S"
  unfolding validS_def
  using assms unfolding wpS_def wp_def by simp

lemma valid_wpS:
  assumes "⦃P⦄⇩S f ⦃Q⦄⇩S,⦃E⦄⇩S"
  shows "⋀st. P (accounts st, stack st, memory st, storage st) ⟹ wpS f (λst. Q (accounts st, stack st, memory st, storage st))E st"
  unfolding wpS_def wp_def using assms unfolding validS_def by simp

context statement_with_gas
begin

subsection ‹Skip›

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

subsection ‹Assign›

lemma wp_Assign:
  fixes ex ev cd st lv
  defines "ngas ≡ gas st - costs (ASSIGN lv ex) ev cd st"
  assumes "⋀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');
             g' ≤ gas st;
             convert t t' v = Some v'⟧
           ⟹ P (st⦇gas := g', stack:=updateStore l (KValue v') (stack st)⦈)"
      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, Storage (STValue t')), g');
             g' ≤ gas st;
             convert t t' v = Some v'⟧
           ⟹ P (st⦇gas := g', storage:=(storage st) (address ev := (fmupd l v' (storage st (address ev))))⦈)"
      and "⋀v t g l t' g' v' vt.
             ⟦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, Memory (MTValue t')), g');
             g' ≤ gas st;
             convert t t' v = Some v'⟧
           ⟹ P (st⦇gas := g', memory:=updateStore l (MValue v') (memory st)⦈)"
      and "⋀p x t g l t' g' p' 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 ((LStackloc l, Memory t'), g');
             g' ≤ gas st;
             accessStore l (stack st) = Some (KMemptr p');
             cpm2m p p' x t cd (memory st) = Some m'⟧
           ⟹ P (st⦇gas := g', memory:=m'⦈)"
      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, Storage t'), g');
             g' ≤ gas st;
             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 "⋀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');
             g' ≤ gas st;
             cpm2s p l x t cd (storage st (address ev)) = Some s'⟧
           ⟹ P (st⦇gas := g', storage:=(storage st) (address ev := s')⦈)"
      and "⋀p x t g l t' g' 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, t'), g');
             g' ≤ gas st;
             cpm2m p l x t cd (memory st) = Some m'⟧
           ⟹ P (st⦇gas := g', memory:=m'⦈)"
      and "⋀p x t g l t' g'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KMemptr p, Memory (MTArray x t)), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Memory t'), g');
             g' ≤ gas st⟧
           ⟹ P (st⦇gas := g', stack:=updateStore l (KMemptr p) (stack st)⦈)"
      and "⋀p x t g l t' g' p' s'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KMemptr p, Memory (MTArray x t)), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Storage t'), g');
             g' ≤ gas st;
             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 "⋀p x t g l t' g' s'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KMemptr p, Memory (MTArray x t)), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStoreloc l, t'), g');
             g' ≤ gas st;
             cpm2s p l x t (memory st) (storage st (address ev)) = Some s'⟧
           ⟹ P (st⦇gas := g', storage:=(storage st) (address ev := s')⦈)"
      and "⋀p x t g l t' g'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KMemptr p, Memory (MTArray x t)), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LMemloc l, t'), g');
             g' ≤ gas st⟧
           ⟹ P (st⦇gas := g', memory:=updateStore l (MPointer p) (memory st)⦈)"
      and "⋀p x t g l t' g' p' m'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KStoptr p, Storage (STArray x t)), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Memory t'), g');
             g' ≤ gas st;
             accessStore l (stack st) = Some (KMemptr p');
             cps2m p p' x t (storage st (address ev)) (memory st) = Some m'⟧
           ⟹ P (st⦇gas := g', memory:=m'⦈)"
      and "⋀p x t g l t' g'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KStoptr p, Storage (STArray x t)), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Storage t'), g');
             g' ≤ gas st⟧
           ⟹ P (st⦇gas := g', stack:=updateStore l (KStoptr p) (stack st)⦈)"
      and "⋀p x t g l t' g' s'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KStoptr p, Storage (STArray x t)), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStoreloc l, t'), g');
             g' ≤ gas st;
             copy p l x t (storage st (address ev)) = Some s'⟧
           ⟹ P (st⦇gas := g', storage:=(storage st) (address ev := s')⦈)"
      and "⋀p x t g l t' g' m'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KStoptr p, Storage (STArray x t)), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LMemloc l, t'), g');
             g' ≤ gas st;
             cps2m p l x t (storage st (address ev)) (memory st) = Some m'⟧
           ⟹ P (st⦇gas := g', memory:=m'⦈)"
      and "⋀p t t' g l t'' g'.
             ⟦expr ex ev cd (st⦇gas := ngas⦈) ngas = Normal ((KStoptr p, Storage (STMap t t')), g);
             lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, t''), g');
             g' ≤ gas st⟧
           ⟹ P (st⦇gas := g', stack:=updateStore l (KStoptr p) (stack st)⦈)"
      and "E Gas"
      and "E Err"
    shows "wpS (λs. stmt (ASSIGN lv ex) ev cd s) P E st"
  apply (subst stmt.simps(2))
  unfolding wpS_def
  apply wp
  apply (simp_all add: Ex.induct[OF assms(18,19)])
proof -
  fix a g aa b v t ab ga ac ba l t' v'
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
     and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
     and "a = (KValue v, Value t)"
     and "aa = KValue v"
     and "b = Value t"
     and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Value t'), ga)"
     and "ab = (LStackloc l, Value t')"
     and "ac = LStackloc l"
     and "ba = Value t'"
     and "convert t t' v = Some v'"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, stack := updateStore l (KValue v') (stack st)⦈)" using assms(2) unfolding ngas_def by simp
next
  fix a g aa b v t ab ga ac ba l MTypes t' v'
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
     and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
     and "a = (KValue v, Value t)"
     and "aa = KValue v"
     and "b = Value t"
     and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LMemloc l, Memory (MTValue t')), ga)"
     and "ab = (LMemloc l, Memory (MTValue t'))"
     and "ac = LMemloc l"
     and "ba = Memory (MTValue t')"
     and "MTypes = MTValue t'"
     and "convert t t' v = Some v'"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, memory := updateStore l (MValue v') (memory st)⦈)" using assms(4) unfolding ngas_def by simp
next
  fix a g aa b v t ab ga ac ba l ta Types v'
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
     and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KValue v, Value t), g)"
     and "a = (KValue v, Value t)"
     and "aa = KValue v"
     and "b = Value t"
     and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStoreloc l, Storage (STValue Types)), ga)"
     and "ab = (LStoreloc l, Storage (STValue Types))"
     and "ac = LStoreloc l"
     and "ba = Storage (STValue Types)"
     and "ta = STValue Types"
     and "convert t Types v = Some v'"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, storage := (storage st) (address ev := fmupd l v' (storage st (address ev)))⦈)" using assms(3) unfolding ngas_def by simp
next
  fix a g aa b p MTypes x t ab ga ac xa l MTypesa y literal ya
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
     and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
     and "a = (KCDptr p, Calldata (MTArray x t))"
     and "aa = KCDptr p"
     and "b = Calldata (MTArray x t)"
     and "MTypes = MTArray x t"
     and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Memory MTypesa), ga)"
     and "ab = (LStackloc l, Memory MTypesa)"
     and "ac = LStackloc l"
     and "xa = Memory MTypesa"
     and "accessStore l (stack st) = Some (KMemptr literal)"
     and "y = KMemptr literal"
     and "cpm2m p literal x t cd (memory st) = Some ya"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, memory := ya⦈)" using assms(5) unfolding ngas_def by simp
next
     fix a g aa b p MTypes x t ab ga ac xa l ta y literal ya
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
     and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
     and "a = (KCDptr p, Calldata (MTArray x t))"
     and "aa = KCDptr p"
     and "b = Calldata (MTArray x t)"
     and "MTypes = MTArray x t"
     and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Storage ta), ga)"
     and "ab = (LStackloc l, Storage ta)"
     and "ac = LStackloc l"
     and "xa = Storage ta"
     and "accessStore l (stack st) = Some (KStoptr literal)"
     and "y = KStoptr literal"
     and "cpm2s p literal x t cd (storage st (address ev)) = Some ya"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, storage := (storage st) (address ev := ya)⦈)" using assms(6) unfolding ngas_def by simp
next
  fix a g aa b p MTypes x t ab ga ac xa l y
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
     and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
     and "a = (KCDptr p, Calldata (MTArray x t))"
     and "aa = KCDptr p"
     and "b = Calldata (MTArray x t)"
     and "MTypes = MTArray x t"
     and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LMemloc l, xa), ga)"
     and "ab = (LMemloc l, xa)"
     and "ac = LMemloc l"
     and "cpm2m p l x t cd (memory st) = Some y"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, memory := y⦈)" using assms(8) unfolding ngas_def by simp
next
  fix a g aa b p MTypes x t ab ga ac xa l y
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
     and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KCDptr p, Calldata (MTArray x t)), g)"
     and "a = (KCDptr p, Calldata (MTArray x t))"
     and "aa = KCDptr p"
     and "b = Calldata (MTArray x t)"
     and "MTypes = MTArray x t"
     and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStoreloc l, xa), ga)"
     and "ab = (LStoreloc l, xa)"
     and "ac = LStoreloc l"
     and "cpm2s p l x t cd (storage st (address ev)) = Some y"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, storage := (storage st) (address ev := y)⦈)" using assms(7) unfolding ngas_def by simp
next
  fix a g aa b p MTypes x t ab ga ac xa l MTypesa
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
    and "a = (KMemptr p, Memory (MTArray x t))"
    and "aa = KMemptr p"
    and "b = Memory (MTArray x t)"
    and "MTypes = MTArray x t"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Memory MTypesa), ga)"
    and "ab = (LStackloc l, Memory MTypesa)"
    and "ac = LStackloc l"
    and "xa = Memory MTypesa"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, stack := updateStore l (KMemptr p) (stack st)⦈)" using assms(9) unfolding ngas_def by simp
next
  fix a g aa b p MTypes x t ab ga ac xa l ta y literal ya
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
    and "a = (KMemptr p, Memory (MTArray x t))"
    and "aa = KMemptr p"
    and "b = Memory (MTArray x t)"
    and "MTypes = MTArray x t"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Storage ta), ga)"
    and "ab = (LStackloc l, Storage ta)"
    and "ac = LStackloc l"
    and "xa = Storage ta"
    and "accessStore l (stack st) = Some (KStoptr literal)"
    and "y = KStoptr literal"
    and "cpm2s p literal x t (memory st) (storage st (address ev)) = Some ya"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, storage := (storage st) (address ev := ya)⦈)" using assms(10) unfolding ngas_def by simp
next
  fix a g aa b p MTypes x t ab ga ac xa l
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
    and "a = (KMemptr p, Memory (MTArray x t))"
    and "aa = KMemptr p"
    and "b = Memory (MTArray x t)"
    and "MTypes = MTArray x t"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LMemloc l, xa), ga)"
    and "ab = (LMemloc l, xa)"
    and "ac = LMemloc l"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, memory := updateStore l (MPointer p) (memory st)⦈)" using assms(12) unfolding ngas_def by simp
next
  fix a g aa b p MTypes x t ab ga ac xa l y
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KMemptr p, Memory (MTArray x t)), g)"
    and "a = (KMemptr p, Memory (MTArray x t))"
    and "aa = KMemptr p"
    and "b = Memory (MTArray x t)"
    and "MTypes = MTArray x t"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStoreloc l, xa), ga)"
    and "ab = (LStoreloc l, xa)"
    and "ac = LStoreloc l"
    and "cpm2s p l x t (memory st) (storage st (address ev)) = Some y"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, storage := (storage st) (address ev := y)⦈)" using assms(11) unfolding ngas_def by simp
next
  fix a g aa b p t x ta ab ga ac xa l MTypes y literal ya
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x ta)), g)"
    and "a = (KStoptr p, Storage (STArray x ta))"
    and "aa = KStoptr p"
    and "b = Storage (STArray x ta)"
    and "t = STArray x ta"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Memory MTypes), ga)"
    and "ab = (LStackloc l, Memory MTypes)"
    and "ac = LStackloc l"
    and "xa = Memory MTypes"
    and "accessStore l (stack st) = Some (KMemptr literal)"
    and "y = KMemptr literal"
    and "cps2m p literal x ta (storage st (address ev)) (memory st) = Some ya"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, memory := ya⦈)" using assms(13) unfolding ngas_def by simp
next
 fix a g aa b p t x ta ab ga ac xa l tb
 assume "costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x ta)), g)"
    and "a = (KStoptr p, Storage (STArray x ta))"
    and "aa = KStoptr p"
    and "b = Storage (STArray x ta)"
    and "t = STArray x ta"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, Storage tb), ga)"
    and "ab = (LStackloc l, Storage tb)"
    and "ac = LStackloc l"
    and "xa = Storage tb"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, stack := updateStore l (KStoptr p) (stack st)⦈)" using assms(14) unfolding ngas_def by simp
next
 fix a g aa b p t x ta ab ga ac xa l y
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x ta)), g)"
    and "a = (KStoptr p, Storage (STArray x ta))"
    and "aa = KStoptr p"
    and "b = Storage (STArray x ta)"
    and "t = STArray x ta"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LMemloc l, xa), ga)"
    and "ab = (LMemloc l, xa)"
    and "ac = LMemloc l"
    and "cps2m p l x ta (storage st (address ev)) (memory st) = Some y"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, memory := y⦈)" using assms(16) unfolding ngas_def by simp
next
 fix a g aa b p t x ta ab ga ac xa l y
  assume "costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STArray x ta)), g)"
    and "a = (KStoptr p, Storage (STArray x ta))"
    and "aa = KStoptr p"
    and "b = Storage (STArray x ta)"
    and "t = STArray x ta"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStoreloc l, xa), ga)"
    and "ab = (LStoreloc l, xa)"
    and "ac = LStoreloc l"
    and "copy p l x ta (storage st (address ev)) = Some y"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, storage := (storage st) (address ev := y)⦈)" using assms(15) unfolding ngas_def by simp
next
 fix a g aa b p t ta t' ab ga ac x l
  assume "   costs (ASSIGN lv ex) ev cd st < gas st"
    and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ASSIGN lv ex) ev cd st⦈) (gas st - costs (ASSIGN lv ex) ev cd st) = Normal ((KStoptr p, Storage (STMap ta t')), g)"
    and "a = (KStoptr p, Storage (STMap ta t'))"
    and "aa = KStoptr p"
    and "b = Storage (STMap ta t')"
    and "t = STMap ta t'"
    and **: "local.lexp lv ev cd (st⦇gas := g⦈) g = Normal ((LStackloc l, x), ga)"
    and "ab = (LStackloc l, x)"
    and "ac = LStackloc l"
  moreover have "ga ≤ gas st"
  proof -
    have "ga ≤ g" using lexp_gas[OF **] by simp
    also have "… ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    finally show ?thesis .
  qed
  ultimately show "ga ≤ gas st ∧ P (st⦇gas := ga, stack := updateStore l (KStoptr p) (stack st)⦈)" using assms(17) unfolding ngas_def by simp
qed

subsection ‹Composition›

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

subsection ‹Conditional›

lemma wp_ITE:
  assumes "⋀g g'. expr ex ev cd (st⦇gas := g⦈) g = Normal ((KValue ⌈True⌉, Value TBool), g') ⟹ wpS (stmt s1 ev cd) P E (st⦇gas := g'⦈)"
      and "⋀g g'. expr ex ev cd (st⦇gas := g⦈) g = Normal ((KValue ⌈False⌉, Value TBool), g') ⟹ wpS (stmt s2 ev cd) P E (st⦇gas := g'⦈)"
      and "E Gas"
      and "E Err"
    shows "wpS (λs. stmt (ITE ex s1 s2) ev cd s) P E st"
  apply (subst stmt.simps(4))
  unfolding wpS_def
  apply wp
  apply (simp_all add: Ex.induct[OF assms(3,4)])
  proof -
    fix a g aa ba b v
    assume "costs (ITE ex s1 s2) ev cd st < gas st"
       and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ITE ex s1 s2) ev cd st⦈) (gas st - costs (ITE ex s1 s2) ev cd st) = Normal ((KValue ⌈True⌉, Value TBool), g)"
       and "a = (KValue ⌈True⌉, Value TBool)"
       and "aa = KValue ⌈True⌉" and "ba = Value TBool" and "v = TBool" and "b = ⌈True⌉"
    then have "wpS (stmt s1 ev cd) P E (st⦇gas := g⦈)" using assms(1) by simp
    moreover have "g ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    ultimately show "wp (local.stmt s1 ev cd) (λ_ st'. gas st' ≤ gas st ∧ P st') E (st⦇gas := g⦈)"
      unfolding wpS_def wp_def by (simp split:result.split_asm prod.split_asm)
  next
    fix a g aa ba b v
    assume "costs (ITE ex s1 s2) ev cd st < gas st"
       and *: "local.expr ex ev cd (st⦇gas := gas st - costs (ITE ex s1 s2) ev cd st⦈) (gas st - costs (ITE ex s1 s2) ev cd st) = Normal ((KValue ⌈False⌉, Value TBool), g)"
       and "a = (KValue ⌈False⌉, Value TBool)"
       and "aa = KValue ⌈False⌉" and "ba = Value TBool" and "v = TBool" and "b = ⌈False⌉"
    then have "wpS (stmt s2 ev cd) P E (st⦇gas := g⦈)" using assms(2) by simp
    moreover have "g ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF *] by simp
    ultimately show "wp (local.stmt s2 ev cd) (λ_ st'. gas st' ≤ gas st ∧ P st') E (st⦇gas := g⦈)"
      unfolding wpS_def wp_def by (simp split:result.split_asm prod.split_asm)
  qed

subsection ‹While Loop›

lemma wp_While[rule_format]:
    fixes iv::"Accounts × Stack × MemoryT × (Address ⇒ StorageT) ⇒ bool"
  assumes "⋀a k m s st g. ⟦iv (a, k, m, s); expr ex ev cd (st⦇gas := gas st - costs (WHILE ex sm) ev cd st⦈) (gas st - costs (WHILE ex sm) ev cd st) = Normal ((KValue ⌈False⌉, Value TBool), g)⟧ ⟹ P (st⦇gas := g⦈)"
      and "⋀a k m s st g. ⟦iv (a, k, m, s); expr ex ev cd (st⦇gas := gas st - costs (WHILE ex sm) ev cd st⦈) (gas st - costs (WHILE ex sm) ev cd st) = Normal ((KValue ⌈True⌉, Value TBool), g)⟧ ⟹ wpS (stmt sm ev cd) (λst. iv (accounts st, stack st, memory st, storage st)) E (st⦇gas:=g⦈)"
      and "E Err"
      and "E Gas"
    shows "iv (accounts st, stack st, memory st, storage st) ⟶ wpS (λs. stmt (WHILE ex sm) ev cd s) P E 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 := gas st - costs (WHILE ex sm) ev cd st⦈) (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') ⇒ gas s' ≤ gas st ∧ 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 (local.stmt sm ev cd) (λst. iv (accounts st, stack st, memory st, storage st)) E (st⦇gas:=g⦈)" using assms(2) ** 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 "gas st ≥ costs (WHILE ex sm) ev cd st" using * by (simp add:stmt.simps split:if_split_asm)
        then have "gas st' < 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 (local.stmt (WHILE ex sm) ev cd) P E st'" using 1 by simp
        then show "(case x1 of (r, s') ⇒ gas s' ≤ gas st ∧ P s')" unfolding wpS_def wp_def using **** `gas st' < 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 ** assms(1) 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 ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF **] by simp
        ultimately show "case x1 of (r, s') ⇒ gas s' ≤ gas st ∧ P s'" by (auto split:prod.split)
      qed
    qed
  next
    fix x2
    show "iv (accounts st, stack st, memory st, storage st) ⟶ E x2" using assms(3,4) Ex.nchotomy by metis
  qed
qed

subsection ‹Blocks›

lemma wp_blockNone:
  assumes "⋀cd' mem' sck' e'. decl id0 tp None False cd (memory (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) stm) ev cd st⦈)) (storage (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) stm) ev cd st⦈))
           (cd, memory (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) stm) ev cd st⦈), stack (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) stm) ev cd st⦈), ev) = Some (cd', mem', sck', e')
          ⟹ wpS (stmt stm e' cd') P E (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) stm) ev cd st, stack := sck', memory := mem'⦈)"
      and "E Gas"
      and "E Err"
    shows "wpS (λs. stmt (BLOCK ((id0, tp), None) stm) ev cd s) P E st"
  unfolding wpS_def wp_def
proof ((split result.split | split prod.split)+, rule conjI; (rule allI | rule impI)+)
  fix x1 x1a x2
  assume "x1 = (x1a, x2)"
    and "local.stmt (BLOCK ((id0, tp), None) stm) ev cd st = Normal x1"
  then have "local.stmt (BLOCK ((id0, tp), None) stm) ev cd st = Normal (x1a, x2)" by simp
  then show "gas x2 ≤ gas st ∧ P x2"
  proof (cases rule: blockNone)
    case (1 cd' mem' sck' e')
    then show ?thesis using assms(1)[OF 1(2)] unfolding wpS_def wp_def by auto
  qed
next
  fix e
  assume "local.stmt (BLOCK ((id0, tp), None) stm) ev cd st = Exception e"
  show "E e" using assms(2,3) by (induction rule: Ex.induct)
qed

lemma wp_blockSome:
  assumes "⋀v t g' cd' mem' sck' e'.
        ⟦ expr ex' ev cd (st⦇gas := gas st - costs (BLOCK ((id0, tp), Some ex') stm) ev cd st⦈) (gas st - costs (BLOCK ((id0, tp), Some ex') stm) ev cd st) = Normal ((v, t), g');
          g' ≤ gas st - costs (BLOCK ((id0, tp), Some ex') stm) ev cd st;
          decl id0 tp (Some (v,t)) False cd (memory st) (storage st) (cd, memory st, stack st, ev) = Some (cd', mem', sck', e')⟧
        ⟹ wpS (stmt stm e' cd') P E (st⦇gas := g', stack := sck', memory := mem'⦈)"
      and "E Gas"
      and "E Err"
    shows "wpS (λs. stmt (BLOCK ((id0, tp), Some ex') stm) ev cd s) P E st"
  unfolding wpS_def wp_def
proof ((split result.split | split prod.split)+, rule conjI; (rule allI | rule impI)+)
  fix x1 x1a x2
  assume "x1 = (x1a, x2)"
    and "local.stmt (BLOCK ((id0, tp), Some ex') stm) ev cd st = Normal x1"
  then have "local.stmt (BLOCK ((id0, tp), Some ex') stm) ev cd st = Normal (x1a, x2)" by simp
  then show "gas x2 ≤ gas st ∧ P x2"
  proof (cases rule: blockSome)
    case (1 v t g cd' mem' sck' e')
    moreover have "g ≤ gas st - costs (BLOCK ((id0, tp), Some ex') stm) ev cd st" using msel_ssel_expr_load_rexp_gas(3)[OF 1(2)] by simp
    ultimately show ?thesis using assms(1)[OF 1(2)] unfolding wpS_def wp_def by auto
  qed
next
  fix e
  assume "local.stmt (BLOCK ((id0, tp), Some ex') stm) ev cd st = Exception e"
  show "E e" using assms(2,3) by (induction rule: Ex.induct)
qed

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'' ≤ gas st ∧
            type (acc ad) = Some (Contract cname) ∧
            expr adex ev cd (st'⦇gas := gas st' - costs (EXTERNAL adex mid xe val) ev cd st'⦈) (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 256) v = Some v' ∧
            load True fp xe (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore emptyStore emptyStore 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 (stmt f e⇩l cd⇩l) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) (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 ≤ gas st ∧
          load False fp xe (ffold (init members) (emptyEnv ad cname (sender ev) (svalue ev)) (fmdom members)) emptyStore emptyStore (memory st') ev cd (st'⦇gas := gas st' - costs (INVOKE i xe) ev cd st'⦈) (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 (stmt f e⇩l cd⇩l) (λst. post mid (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err) (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' ≤ gas st ∧
          expr adex ev cd (st'⦇gas := gas st' - cc⦈) (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 256) v = Some v' ∧
          transfer (address ev) ad v' (accounts st') = Some acc ∧
          pref (ReadL⇩i⇩n⇩t (bal (acc ad)), storage st' ad)
         ⟶ wpS (λs. stmt fb (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore s) (λst. postf (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err) (st'⦇gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore⦈)))"

definition Qfe
  where "Qfe ad iv st ≡
   (∀ev. address ev ≠ ad
    ⟶ (∀ex cd st' adex cc v t g g' v' acc.
          g' ≤ gas st ∧
          type (acc ad) = Some (Contract cname) ∧
          expr adex ev cd (st'⦇gas := gas st' - cc⦈) (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 256) 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 (λs. stmt fb (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore s) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) (st'⦇gas := g', accounts := acc, stack:=emptyStore, memory:=emptyStore⦈)))"

lemma safeStore[rule_format]:
  fixes ad iv
  defines "aux1 st ≡ ∀st'::State. gas st' < gas st ⟶ Qe ad iv st'"
      and "aux2 st ≡ ∀st'::State. gas st' < gas st ⟶ Qfe ad iv st'"
    shows "∀st'. address ev ≠ ad ∧ type (accounts st ad) = Some (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 (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 (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 < gas st) st = Normal ((), st)" using l3 by (simp add:stmt.simps split:if_split_asm)
      moreover from l2 have "iv (storage (st⦇gas := gas st - costs (COMP s1 s2) ev cd st⦈) ad) (ReadL⇩i⇩n⇩t (bal (accounts (st⦇gas := gas st - costs (COMP s1 s2) ev cd st⦈) ad)))" by simp
      moreover have **:"gas (st⦇gas:= gas st - costs (COMP s1 s2) ev cd st⦈) ≤ gas st" by simp
      then have "aux1 (st⦇gas:= 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:= 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 (Contract cname)" using atype_same[OF 1(2), of ad "Contract cname"] l12 by auto
      moreover have **:"gas st'' ≤ 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 (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 (Contract cname)" using atype_same[OF 1(3), of ad "Contract cname"] l12 by auto
      moreover have **:"gas (st⦇gas:= g⦈) ≤ 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 (Contract cname)" using atype_same[OF 2(3), of ad "Contract cname"] l12 by auto
      moreover have **:"gas (st⦇gas:= g⦈) ≤ 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 (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 *:"gas (st⦇gas:= g⦈) ≤ 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 (Contract cname)" using atype_same[OF 1(3), of ad "Contract cname"] l12 by auto
      moreover have **:"gas st'' ≤ 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 (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 < 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)) emptyStore emptyStore (memory (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈)) ev cd (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) (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 < gas st) st = Normal ((), st)" by (simp add:stmt.simps split:if_split_asm)
    moreover have **: "modify (λst. st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) st = Normal ((), st⦇gas := 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 *:"gas (st⦇gas := g, stack := k⇩l, memory := m⇩l⦈) ≤ 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 *:"gas (st⦇gas := g, stack := k⇩l, memory := m⇩l⦈) ≤ 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 (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 "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'' < 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'' ≤ gas (st⦇gas := g'', accounts := acc, stack := k⇩l, memory := m⇩l⦈)" by simp
        moreover from l12 have "type (acc ad) = Some (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 (local.stmt f e⇩l cd⇩l) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) (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 < gas st) st = Normal ((), st)" by (simp add:stmt.simps split:if_split_asm)
        moreover have **: "modify (λst. st⦇gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) st = Normal ((), st⦇gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈)" by simp
        ultimately have "∀st'. address e⇩l ≠ ad ∧ type (acc ad) = Some (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 (Contract cname)" using transfer_type_same l12 1(10) by simp
        moreover have *:"gas (st⦇gas := g'', accounts := acc, stack := k⇩l, memory := m⇩l⦈) ≤ 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 "gas st ≥  costs (EXTERNAL ad' i xe val) ev cd st" using 3 by (simp add:stmt.simps split:if_split_asm)
        then have "gas (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) < 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 := emptyStore⦈)" 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' ≤ gas (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)" by simp
        moreover from l12 have "type (acc ad) = Some (Contract cname)" using transfer_type_same[OF 2(9)] by simp
        ultimately have "wpS (local.stmt fb (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)" 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)) emptyStore (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) = 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 < 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 (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)) emptyStore (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) = Normal ((), st') ∧ aux1 (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) ∧ aux2 (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)
          ⟶ 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 (Contract cname)" using transfer_type_same l12 2(9) by simp
        moreover have *:"gas (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) ≤ 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 := emptyStore⦈)" 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 := emptyStore⦈)" 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 (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 "gas st ≥  costs (TRANSFER ad' ex) ev cd st" using 3 by (simp add:stmt.simps split:if_split_asm)
        then have "gas (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) < 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 := emptyStore⦈)" 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' ≤ gas (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)" by simp
        moreover from l12 have "type (acc ad) = Some (Contract cname)" using transfer_type_same[OF 1(7)] by simp
        ultimately have "wpS (local.stmt fb (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)" 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)) emptyStore (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) = 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 < 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 (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)) emptyStore (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) = Normal ((), st') ∧
          aux1 (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) ∧ aux2 (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)
          ⟶ 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 (Contract cname)" using transfer_type_same l12 1(7) by simp
        moreover have *:"gas (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) ≤ 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 := emptyStore⦈)" 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 := emptyStore⦈)" 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 (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 := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st, stack := sck', memory := mem'⦈) ad) (ReadL⇩i⇩n⇩t (bal (accounts (st⦇gas := gas st - costs (BLOCK ((id0, tp), None) s) ev cd st, stack := sck', memory := mem'⦈) ad)))" by simp
      moreover have *:"gas (st⦇gas:= gas st - costs (BLOCK ((id0, tp), None) s) ev cd st, stack := sck', memory := mem'⦈) ≤ gas st" by simp
      then have "aux1 (st⦇gas:= 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:= 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 (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 *:"gas (st⦇gas:= g, stack := sck', memory := mem'⦈) ≤ 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 (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'')
      moreover define adv where "adv = hash (address ev) ⌊contracts (accounts (st⦇gas := gas st - costs (NEW i xe val) ev cd st⦈) (address ev))⌋"
      moreover define st''' where "st''' = (st⦇gas := gas st - costs (NEW i xe val) ev cd st, gas := g', accounts := (accounts st)(adv := ⦇bal = ShowL⇩i⇩n⇩t 0, type = Some (Contract i), contracts = 0⦈), storage := (storage st)(adv := {$$}), accounts := acc, stack := k⇩l, memory := m⇩l⦈)"
      ultimately have "∀st'. address e⇩l ≠ ad ∧
        type (accounts st''' ad) = Some (Contract cname) ∧
        iv (storage st''' ad) ⌈bal (accounts st''' ad)⌉ ∧
        local.stmt (snd cn) e⇩l cd⇩l st''' = Normal ((), st') ∧ aux1 st''' ∧ aux2 st''' ⟶
        iv (storage st' ad) ⌈bal (accounts st' ad)⌉"
        using 11 by simp
      moreover have "address e⇩l ≠ ad"
      proof -
        have "address e⇩l = adv" using msel_ssel_expr_load_rexp_gas(4)[OF 1(5)] 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 (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(6)] 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(6), 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(7) st'''_def adv_def by simp
      moreover have "aux1 st'''"
      proof -
        have *: "gas st''' ≤ 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(5)] 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 *: "gas st''' ≤ 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(5)] 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(8) by simp
      moreover have "bal (accounts st'' ad) = bal (accounts st' ad)" using 1(8) by simp
      ultimately show ?thesis by simp
    qed
  qed
qed

type_synonym Precondition = "int × StorageT × Environment × Memoryvalue Store × Stackvalue Store × Memoryvalue Store ⇒ 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 := gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) (gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g) ∧
         adv ≠ ad ∧
         type (accounts st adv) = Some (Contract c) ∧
         c |∈| fmdom ep ∧
         expr val ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
         convert t (TUInt 256) v = Some v'
        ⟶ iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)) - ReadL⇩i⇩n⇩t v'))
      ⟶ wpS (λs. stmt (EXTERNAL ad' i xe val) ev cd s) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) 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)) emptyStore emptyStore (memory st) ev cd (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) (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 (λs. stmt (INVOKE i xe) ev cd s) (λst. post i (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err) st)"

definition Pfi
  where "Pfi ad pref postf st ≡
   (∀ev ex ad' cd.
     address ev = ad ∧
     (∀adv g.
       expr ad' ev cd (st⦇gas := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 (λs. stmt (TRANSFER ad' ex) ev cd s) (λst. postf (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err) st)"

definition Pfe
  where "Pfe ad iv st ≡
     (∀ev ex ad' cd.
       address ev = ad ∧
       (∀adv g.
         expr ad' ev cd (st⦇gas := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 256) v = Some v'
        ⟶ iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)) - ReadL⇩i⇩n⇩t v'))
      ⟶ wpS (λs. stmt (TRANSFER ad' ex) ev cd s) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) 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. gas st' ≤ gas st ∧ type (accounts st' ad) = Some (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 (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 (Contract cname)"
       and a0: "address ev = ad"
       and a1: "∀adv c g v t g' v'.
          local.expr ad' ev cd (st⦇gas := gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈)
           (gas st - costs (EXTERNAL ad' i xe val) ev cd st) =
          Normal ((KValue adv, Value TAddr), g) ∧
          adv ≠ ad ∧
          type (accounts st adv) = Some (Contract c) ∧
          c |∈| fmdom ep ∧
          local.expr val ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
          convert t (TUInt 256) v = Some v'
      ⟶ iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)) - ReadL⇩i⇩n⇩t v')"
    show "wpS (local.stmt (EXTERNAL ad' i xe val) ev cd) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) 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 "gas s'''''' ≤ gas st ∧ 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 (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. gas st' < 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'' ≤ gas st' ∧
                     type (acc ad) = Some (Contract cname) ∧
                     local.expr adex ev cd (st0⦇gas := gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0⦈) (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 256) v = Some v' ∧
                     local.load True fp xe (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore emptyStore emptyStore 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 (local.stmt f e⇩l cd⇩l) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) (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 "gas st' < gas (st⦇gas := g0'', accounts := acc0, stack := k⇩l0, memory := m⇩l0⦈)"
            then have "gas st' < 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 `gas st' < gas st` "1.IH"], THEN conjunct1] unfolding Qe_def by simp
          qed
          moreover have "∀st'::State. gas st' < 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' ≤ gas st' ∧
                     type (acc ad) = Some (Contract cname) ∧
                     expr adex ev cd (st0⦇gas := gas st0 - cc⦈) (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 256) v = Some v' ∧
                     transfer (address ev) ad v' (accounts st0) = Some acc ∧
                     iv (storage st0 ad) (⌈bal (acc ad)⌉ - ⌈v'⌉) ⟶
                     wpS (local.stmt fb (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore)
                      (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err)
                      (st0⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)))" (is "∀st'. ?left st' ⟶ ?right st'")
          proof (rule allI,rule impI)
            fix st'::State
            assume l0: "gas st' < gas (st⦇gas := g0'', accounts := acc0, stack := k⇩l0, memory := m⇩l0⦈)"
            then have "gas st' < 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 `gas st' < 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
        moreover have "gas st0'' ≤ gas st" using msel_ssel_expr_load_rexp_gas(4)[OF Some(9),THEN conjunct1] msel_ssel_expr_load_rexp_gas(3)[OF Some(2)] msel_ssel_expr_load_rexp_gas(3)[OF Some(6)] stmt_gas[OF Some(11)] by simp
        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 := emptyStore⦈) ad) = Some (Contract cname)" using transfer_type_same[OF None(9)] a00 by simp
          moreover have "iv (storage (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈) ad) (ReadL⇩i⇩n⇩t (bal (accounts (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈) 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. gas st' < gas (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈) ⟶
              (∀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'' ≤ gas st' ∧
                     type (acc ad) = Some (Contract cname) ∧
                     local.expr adex ev cd (st0⦇gas := gas st0 - costs (EXTERNAL adex mid xe val) ev cd st0⦈) (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 256) v = Some v' ∧
                     local.load True fp xe (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore emptyStore emptyStore 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 (local.stmt f e⇩l cd⇩l) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) (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 "gas st' < gas (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈)"
            then have "gas st' < 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 `gas st' < gas st` "1.IH"], THEN conjunct1] unfolding Qe_def by simp
          qed
          moreover have "∀st'::State. gas st' < gas (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈) ⟶
              (∀ev. address ev ≠ ad
               ⟶ (∀ex cd st0 adex cc v t g g' v' acc.
                     g' ≤ gas st' ∧
                     type (acc ad) = Some (Contract cname) ∧
                     expr adex ev cd (st0⦇gas := gas st0 - cc⦈) (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 256) v = Some v' ∧
                     transfer (address ev) ad v' (accounts st0) = Some acc ∧
                     iv (storage st0 ad) (⌈bal (acc ad)⌉ - ⌈v'⌉) ⟶
                     wpS (local.stmt fb (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore)
                      (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err)
                      (st0⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)))" (is "∀st'. ?left st' ⟶ ?right st'")
          proof (rule allI,rule impI)
            fix st'::State
            assume l0: "gas st' < gas (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈)"
            then have "gas st' < 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 `gas st' < 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 := emptyStore⦈" iv fb0' emptyStore "st0''"] None unfolding Qe_def Qfe_def by blast
          then show ?thesis using None(11) by simp
        qed
        moreover have "gas st0'' ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF None(2)] msel_ssel_expr_load_rexp_gas(3)[OF None(6)] stmt_gas[OF None(10)] by simp
        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 (Contract cname)"
      and a0: "address ev = ad"
      and a1: "∀adv g. local.expr ad' ev cd (st⦇gas := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 256) v = Some v' ⟶
          iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)) - ReadL⇩i⇩n⇩t v')"
    show "wpS (local.stmt (TRANSFER ad' ex) ev cd) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) 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 "gas s'''''' ≤ gas st ∧ 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 := emptyStore⦈) ad) = Some (Contract cname)" using transfer_type_same[OF Contract(7)] a00 by simp
          moreover have "iv (storage (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈) ad) (ReadL⇩i⇩n⇩t (bal (accounts (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈) 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. gas st' < gas (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈) ⟶ Qe ad iv st'"
          proof (rule allI,rule impI)
            fix st'::State
            assume "gas st' < gas (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈)"
            then have "gas st' < 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 `gas st' < gas st` "1.IH"], THEN conjunct1] by simp
          qed
          moreover have "∀st'::State. gas st' < gas (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈) ⟶
              (∀ev. address ev ≠ ad
               ⟶ (∀ex cd st0 adex cc v t g g' v' acc.
                     g' ≤ gas st' ∧
                     type (acc ad) = Some (Contract cname) ∧
                     expr adex ev cd (st0⦇gas := gas st0 - cc⦈) (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 256) v = Some v' ∧
                     transfer (address ev) ad v' (accounts st0) = Some acc ∧
                     iv (storage st0 ad) (⌈bal (acc ad)⌉ - ⌈v'⌉) ⟶
                     wpS (local.stmt fb (ffold (init members) (emptyEnv ad cname (address ev) v') (fmdom members)) emptyStore)
                      (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err)
                      (st0⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)))" (is "∀st'. ?left st' ⟶ ?right st'")
          proof (rule allI,rule impI)
            fix st'::State
            assume l0: "gas st' < gas (st⦇gas := g0', accounts := acc0, stack := emptyStore, memory := emptyStore⦈)"
            then have "gas st' < 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 `gas st' < 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 := emptyStore⦈" iv f0 emptyStore "st0''"] Contract unfolding Qe_def Qfe_def by blast
          then show ?thesis using Contract(9) by simp
        qed
        moreover have "gas st0'' ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF Contract(2)] msel_ssel_expr_load_rexp_gas(3)[OF Contract(3)] stmt_gas[OF Contract(8)] by simp
        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
        moreover have "g0' ≤ gas st" using msel_ssel_expr_load_rexp_gas(3)[OF EOA(2)] msel_ssel_expr_load_rexp_gas(3)[OF EOA(3)] by simp
        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 (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)) emptyStore emptyStore (memory st) ev cd (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) (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 (local.stmt (INVOKE i xe) ev cd) (λst. post i (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err) 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 "gas st' ≤ gas st ∧ 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 "gas st > costs (INVOKE i xe) ev cd st" by (simp add:stmt.simps split:if_split_asm)
          then have "gas (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) < 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)) emptyStore
          emptyStore (memory st) ev cd (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈)
          (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 ≤ gas (st⦇gas := 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 (local.stmt f e⇩l cd⇩l) (λst. post i (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err)
            (st⦇gas := g, stack := k⇩l, memory := m⇩l⦈)" using assm[OF all_gas_le[OF `gas (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) < 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
        moreover have "gas st' ≤ gas st" using msel_ssel_expr_load_rexp_gas(4)[OF 1(4),THEN conjunct1] stmt_gas[OF 1(5)] 1(6) by simp
        ultimately 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 (Contract cname)"
      and ad_ev: "address ev = ad"
      and a1: "∀adv g.
          local.expr ad' ev cd (st⦇gas := gas st - costs (TRANSFER ad' ex) ev cd st⦈)
           (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 := gas st - costs (TRANSFER ad' ex) ev cd st⦈)
           (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 (local.stmt (TRANSFER ad' ex) ev cd) (λst. postf (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err) 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 "gas st' ≤ gas st ∧ 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 "gas st ≥ costs (TRANSFER ad' ex) ev cd st" using 2 by (simp add:stmt.simps split:if_split_asm)
        then have "gas (st⦇gas := gas st - costs (TRANSFER ad' ex) ev cd st⦈) < gas st" using transfer_not_zero[of ad' ex ev cd st] by simp
        moreover have "g' ≤ gas (st⦇gas := 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 (local.stmt fb (ffold (init members) (emptyEnv ad c (address ev) v') (fmdom members)) emptyStore)
          (λst. postf (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err)
          (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)" using assm[OF all_gas_le[OF `gas (st⦇gas := gas st - costs (TRANSFER ad' ex) ev cd st⦈) < 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 "gas st' ≤ gas (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) ∧ 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
        moreover from this have "gas st' ≤ gas st" using `g' ≤ gas (st⦇gas := gas st - costs (TRANSFER ad' ex) ev cd st⦈)` by auto
        ultimately 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 (Contract cname)"
      and "⋀st::State. ⟦∀st'::State. gas st' ≤ gas st ∧ type (accounts st' ad) = Some (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 := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 256) v = Some v'
        ⟶ iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)) - ReadL⇩i⇩n⇩t v'))
      ⟶ wpS (λs. stmt (TRANSFER ad' ex) ev cd s) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) 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 (Contract cname)"
     and "⋀st::State. ⟦∀st'::State. gas st' ≤ gas st ∧ type (accounts st' ad) = Some (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 := gas st - costs (EXTERNAL ad' i xe val) ev cd st⦈) (gas st - costs (EXTERNAL ad' i xe val) ev cd st) = Normal ((KValue adv, Value TAddr), g) ∧
         adv ≠ ad ∧
         type (accounts st adv) = Some (Contract c) ∧
         c |∈| fmdom ep ∧
         expr val ev cd (st⦇gas := g⦈) g = Normal ((KValue v, Value t), g') ∧
         convert t (TUInt 256) v = Some v'
        ⟶ iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)) - ReadL⇩i⇩n⇩t v'))
      ⟶ wpS (λs. stmt (EXTERNAL ad' i xe val) ev cd s) (λst. iv (storage st ad) (ReadL⇩i⇩n⇩t (bal (accounts st ad)))) (λe. e = Gas ∨ e = Err) 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 (Contract cname)"
      and "⋀st::State. ⟦∀st'::State. gas st' ≤ gas st ∧ type (accounts st' ad) = Some (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)) emptyStore emptyStore (memory st) ev cd (st⦇gas := gas st - costs (INVOKE i xe) ev cd st⦈) (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 (λs. stmt (INVOKE i xe) ev cd s) (λst. post i (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err) 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 (Contract cname)"
      and "⋀st::State. ⟦∀st'::State. gas st' ≤ gas st ∧ type (accounts st' ad) = Some (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 := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 := gas st - costs (TRANSFER ad' ex) ev cd st⦈) (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 (λs. stmt (TRANSFER ad' ex) ev cd s) (λst. postf (ReadL⇩i⇩n⇩t (bal (accounts st ad)), storage st ad)) (λe. e = Gas ∨ e = Err) 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 xe i cd val st ev adv.
    adv = hash (address ev) (ShowL⇩n⇩a⇩t (contracts (accounts st (address ev)))) ∧
    type (accounts st adv) = None ∧
    expr val ev cd (st⦇gas := gas st - costs (NEW i xe val) ev cd st⦈) (gas st - costs (NEW i xe val) ev cd st) = Normal ((KValue v, Value t), g') ∧
    load True (fst const) xe (ffold (init members) (emptyEnv adv cname (address ev) v) (fmdom members)) emptyStore emptyStore emptyStore ev cd (st⦇gas := g'⦈) g' = Normal ((e⇩l, cd⇩l, k⇩l, m⇩l), g'') ∧
    transfer (address ev) adv v (accounts (st⦇accounts := (accounts st)(adv := ⦇bal = ShowL⇩i⇩n⇩t 0, type = Some (Contract i), contracts = 0⦈)⦈)) = Some acc
    ⟶ wpS (local.stmt (snd const) e⇩l cd⇩l) (λst. iv (storage st adv) ⌈bal (accounts st adv)⌉) (λe. e = Gas ∨ e = Err)
        (st⦇gas := g'', storage:=(storage st)(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 (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 (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 (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 (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 (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 := gas st - costs (COMP s1 s2) ev cd st⦈) ad) = Some (Contract cname) ⟶ iv (storage (st⦇gas := gas st - costs (COMP s1 s2) ev cd st⦈) ad) ⌈bal (accounts (st⦇gas := gas st - costs (COMP s1 s2) ev cd st⦈) ad)⌉" by auto
      ultimately have "type (accounts st'' ad) = Some (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (Contract c)" using transfer_type_same[OF 1(10)] 1(4) by auto
        moreover from `type (acc ad) = Some (Contract c)` have "type (accounts st' ad) = Some (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'' ≤ 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 (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 (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 (local.stmt f e⇩l cd⇩l) (λst. iv (storage st ad) ⌈bal (accounts st ad)⌉) (λe. e = Gas ∨ e = Err)
        (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 (Contract cname) ⟶ iv (storage st ad) ⌈bal (acc ad)⌉"
        proof
          assume "type (acc ad) = Some (Contract cname)"
          then have "type (accounts st ad) = Some (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 (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 (Contract c)" using transfer_type_same[OF 2(9)] 2(4) by auto
        moreover from `type (acc ad) = Some (Contract c)` have "type (accounts st' ad) = Some (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 (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' ≤ 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 (local.stmt fb' (ffold (init ct) (emptyEnv adv c (address ev) v') (fmdom ct)) emptyStore) (λst. iv (storage st ad) ⌈bal (accounts st ad)⌉) (λe. e = Gas ∨ e = Err)
        (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)" 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 (Contract cname) ⟶ iv (storage st ad) ⌈bal (acc ad)⌉"
        proof
          assume "type (acc ad) = Some (Contract cname)"
          then have "type (accounts st ad) = Some (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)) emptyStore (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) = Normal ((), st') ∧
         type (accounts st' ad) = Some (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 (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 (Contract c)" using transfer_type_same[OF 1(7)] 1(5) by auto
        moreover from `type (acc ad) = Some (Contract c)` have "type (accounts st' ad) = Some (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' ≤ 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 (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 (local.stmt f (ffold (init ct) (emptyEnv adv c (address ev) v') (fmdom ct)) emptyStore) (λst. iv (storage st ad) ⌈bal (accounts st ad)⌉) (λe. e = Gas ∨ e = Err)
        (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈)" 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 (Contract cname) ⟶ iv (storage st ad) ⌈bal (acc ad)⌉"
        proof
          assume "type (acc ad) = Some (Contract cname)"
          then have "type (accounts st ad) = Some (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)) emptyStore
          (st⦇gas := g', accounts := acc, stack := emptyStore, memory := emptyStore⦈) = Normal ((), st') ∧ type (accounts st' ad) = Some (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 (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 (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 := gas st - costs (BLOCK ((id0, tp), None) s) e cd st, stack := sck',
           memory := mem'⦈) = Normal ((), st') ∧
          type (accounts st' ad) = Some (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 (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 (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 (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'')
      define adv where "adv = hash (address e) ⌊contracts (accounts (st⦇gas := 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(5)] 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(4) C1 by simp+
          then have "wpS (local.stmt (snd const) e⇩l cd⇩l) (λst. iv (storage st adv) ⌈bal (accounts st adv)⌉) (λe. e = Gas ∨ e = Err)
                      (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(7) `cn = const` adv_def by simp
          then show ?thesis using 1(8) True by simp
        next
          case False
          moreover have "type (accounts st' ad) = Some (Contract i)"
          proof -
            from `adv = ad` have "type (((accounts st) (adv := ⦇bal = ShowL⇩i⇩n⇩t 0, type = Some (Contract i), contracts = 0⦈)) ad) = Some (Contract i)" by simp
            then have "type (acc ad) = Some (Contract i)" using transfer_type_same[OF 1(6)] adv_def by simp
            then have "type (accounts st'' ad) = Some (Contract i)" using atype_same[OF 1(7)] adv_def by simp
            then show ?thesis using 1(8) by simp
          qed
          ultimately show ?thesis using a2 by simp
        qed
      next
        case False
        moreover have *: "type (acc ad) = Some (Contract cname) ⟶ iv (storage (st⦇storage:=(storage st)(adv := {$$}), accounts:=acc⦈) ad) ⌈bal (acc ad)⌉"
        proof
          assume "type (acc ad) = Some (Contract cname)"
          then have "type (((accounts st) (adv := ⦇bal = ShowL⇩i⇩n⇩t 0, type = Some (Contract i), contracts = 0⦈)) ad) = Some (Contract cname)" using transfer_type_same[OF 1(6)] adv_def by simp
          then have "type ((accounts st) ad) = Some (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(6)] adv_def 11(2) False by simp
        qed
        ultimately have "∀st'. stmt (snd cn) e⇩l cd⇩l (st⦇gas := g', storage := (storage st) (adv := {$$}), accounts := acc, stack := k⇩l, memory := m⇩l⦈) = Normal ((), st') ∧
             type (accounts st' ad) = Some (Contract cname) ⟶ iv (storage st' ad) ⌈bal (accounts st' ad)⌉"
          using 11(1)[where ?s'k4="st⦇gas := g', storage := (storage st) (adv := {$$}), accounts := acc, stack := k⇩l, memory := m⇩l⦈"]
            1 adv_def `address e⇩l = adv` False * by auto
        moreover have "type (accounts st'' ad) = Some (Contract cname)" using 1(8) a2 adv_def by auto
        ultimately show ?thesis using a2 1(6,7,8) adv_def 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. address ev ≠ ad ∧ type (accounts st ad) = Some (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 (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 mcontract
  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
  
  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›
  
  text ‹
    The weakest precondition for assignments generates a lot of different cases.
    However, usually only one of them is required for a given situation.
  
    The following rule eliminates the wrong cases by proving that they lead to a contradiction.
    It requires two facts to be provided:
    ▪ @{term expr_rule}: should be a theorem which evaluates the expression part of the assignment
    ▪ @{term lexp_rule}: should be a theorem which evaluates the left hand side of the assignment
  
  
    Both theorems should assume a corresponding loading of parameters and all declarations which happen before the assignment.
  ›
  
  method vcg_insert_expr_lexp for ex::E and lv::L uses expr_rule lexp_rule =
    match premises in
      expr: "expr ex _ _ _ _ = _" and
      lexp: "lexp lv _ _ _ _ = _" ⇒
        ‹insert expr_rule[OF expr] lexp_rule[OF lexp]›
  
  method vcg_insert_decl for ex::E and lv::L uses expr_rule lexp_rule =
    match premises in
      decl: "decl _ _ _ _ _ _ _ _ = _" (multi) ⇒
        ‹vcg_insert_expr_lexp ex lv expr_rule:expr_rule[OF decl] lexp_rule:lexp_rule[OF decl]›
    ¦ _ ⇒
        ‹vcg_insert_expr_lexp ex lv expr_rule:expr_rule lexp_rule:lexp_rule›
  
  method vcg_insert_load for ex::E and lv::L uses expr_rule lexp_rule =
    match premises in
      load: "load _ _ _ _ _ _ _ _ _ _ _ = _" ⇒
        ‹vcg_insert_decl ex lv expr_rule:expr_rule[OF load] lexp_rule:lexp_rule[OF load]›
    ¦ _ ⇒
        ‹vcg_insert_decl ex lv expr_rule:expr_rule lexp_rule:lexp_rule›
  
  method vcg_assign uses expr_rule lexp_rule =
    match conclusion in
      "wpS (stmt (ASSIGN lv ex) _ _) _ _ _" for lv ex ⇒
        ‹rule wp_Assign; 
          (solve ‹(rule FalseE, simp,
            (vcg_insert_load ex lv expr_rule:expr_rule lexp_rule:lexp_rule)), simp›
         | solve simp)?›,
        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 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] "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 contract @{term ad}.
  ▪ @{term cases_int}: performs case distinction over *internal* methods of contract @{term ad}.
  ▪ @{term cases_fb}: performs case distinction over *fallback* method of 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;
        (vcg_prep,
         rule external;
           solve ‹assumption | simp›)›
  ¦ "Qi _ _ _ _" ⇒
      ‹unfold Qi_def,
       vcg_prep,
       erule cases_fb;
        (vcg_prep,
         rule internal;
           solve ‹assumption | simp›)›
  ¦ "Qfi _ _ _ _" ⇒
      ‹unfold Qfi_def,
       rule allI,
       rule impI,
       rule cases_int;
        (vcg_prep,
         rule fallback_int;
           solve ‹assumption | simp›)›
  ¦ "Qfe _ _ _" ⇒
      ‹unfold Qfe_def,
       rule allI,
       rule impI,
       rule cases_int;
        (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],
  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