section ‹Contracts›
theory Contracts
  imports Environment
begin

subsection ‹Syntax of Contracts›

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

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

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

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

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

subsection ‹State›

type_synonym Gas = nat

record State =   
  accounts :: Accounts
  stack :: Stack
  memory :: MemoryT
  storage :: "Address → StorageT"
  gas :: Gas

lemma all_gas_le:
  assumes "gas x<(gas y::nat)"
      and "∀z. gas z < gas y ⟶ P z ⟶ Q z"
    shows "∀z. gas z ≤ gas x ∧ P z ⟶ Q z" using assms by simp

lemma all_gas_less:
  assumes "∀z. gas z < gas y ⟶ P z"
      and "gas x≤(gas y::nat)"
    shows "∀z. gas z < gas x ⟶ P z" using assms by simp

definition incrementAccountContracts :: "Address → State → State"
  where "incrementAccountContracts ad st = st (accounts := (accounts st)(ad := (accounts st ad)(contracts := Suc (contracts (accounts st ad)))))"

declare incrementAccountContracts_def [solidity_symbex]

lemma incrementAccountContracts_type[simp]:
  "type (accounts (incrementAccountContracts ad st) ad') = type (accounts st ad')"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_bal[simp]:
  "bal (accounts (incrementAccountContracts ad st) ad') = bal (accounts st ad')"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_stack[simp]:
  "stack (incrementAccountContracts ad st) = stack st"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_memory[simp]:
  "memory (incrementAccountContracts ad st) = memory st"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_storage[simp]:
  "storage (incrementAccountContracts ad st) = storage st"
  using incrementAccountContracts_def by simp

lemma incrementAccountContracts_gas[simp]:
  "gas (incrementAccountContracts ad st) = gas st"
  using incrementAccountContracts_def by simp

lemma gas_induct:
  assumes "∧s. ∀s'. gas s' < gas s ⟶ P s' ==> P s"
  shows "P s" using assms by (rule Nat.measure_induct[of "λs. gas s"])

definition emptyStorage :: "Address → StorageT"
where
  "emptyStorage _ = {$$}"

declare emptyStorage_def [solidity_symbex]

abbreviation mystate::State
  where "mystate ≡ (
    accounts = emptyAccount,
    stack = emptyStore,
    memory = emptyStore,
    storage = emptyStorage,
    gas = 0
  )"

datatype Ex = Gas | Err

subsection ‹Contracts›

text ‹
 A contract consists of methods, functions, and storage variables.

 A method is a triple consisting of
 ▪ A list of formal parameters
 ▪ A flag to signal external methods
 ▪ A statement


 A function is a pair consisting of
 ▪ A list of formal parameters
 ▪ A flag to signal external functions
 ▪ An expression
 ›
datatype(discs_sels) Member = Method "(Identifier × Type) list × bool × S"
                | Function "(Identifier × Type) list × bool × E"
                | Var STypes

text ‹
 A procedure environment assigns a contract to an address.
 A contract consists of
 ▪ An assignment of contract to identifiers
 ▪ A constructor
 ▪ A fallback statement which is executed after money is beeing transferred to the contract.

 \url{https://docs.soliditylang.org/en/v0.8.6/contracts.html#fallback-function}
 ›

type_synonym Contract = "(Identifier, Member) fmap × ((Identifier × Type) list × S) × S"

type_synonym Environment_P = "(Identifier, Contract) fmap"

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

declare init_def [solidity_symbex]

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

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

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

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

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

lemma init_s23[simp]:
  assumes "fmlookup ct i = Some (Function f)"
  shows "init ct i e = e"
  using assms init_def by auto

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

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

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

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

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

lemma ffold_init_ad[simp]: "address (ffold (init ct) e xs) = address e"
  using ffold_init_ad_same by simp

lemma ffold_init_sender[simp]: "sender (ffold (init ct) e xs) = sender e"
  using ffold_init_ad_same by simp

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

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

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

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

lemma ffold_init_fmdom: 
  assumes "fmlookup ct i = Some (Var tp)"
      and "i |∉| fmdom (denvalue e)"
    shows "fmlookup (denvalue (ffold (init ct) e (fmdom ct))) i = Some (Storage tp, Storeloc i)"
proof -
  from assms(1) have "i |∈| fmdom ct" by (rule Finite_Map.fmdomI)
  then show ?thesis using ffold_init_fmap[OF assms] by simp
qed

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

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

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

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

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

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

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

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

lemma bind_case_contract_cong [fundef_cong]:
  assumes "x = x'"
      and "∧a. x = Method a ==> f a s = f' a s"
      and "∧a. x = Function a ==> g a s = g' a s"
      and "∧a. x = Var a ==> h a s = h' a s"
    shows "(case x of Method a → f a | Function a → g a | Var a → h a) s
         = (case x' of Method a → f' a | Function a → g' a | Var a → h' a) s"
  using assms by (cases x, auto)

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

end