Theory Valuetypes

section‹Value Types›

theory Valuetypes
imports ReadShow
begin

fun iter :: "(int ⇒ 'b ⇒ 'b) ⇒ 'b ⇒ int ⇒ 'b"
where
  "iter f v x = (if x ≤ 0 then v  
                 else f (x-1) (iter f v (x-1)))"

fun iter' :: "(int ⇒ 'b ⇒ 'b option) ⇒ 'b ⇒ int ⇒ 'b option"
where
  "iter' f v x = (if x ≤ 0 then Some v
                  else case iter' f v (x-1) of
                          Some v' ⇒ f (x-1) v'
                        | None ⇒ None)"

type_synonym Address = String.literal
type_synonym Location = String.literal
type_synonym Valuetype = String.literal

(*Covered*)
datatype Types = TSInt nat
               | TUInt nat
               | TBool
               | TAddr

(*Covered*)
definition createSInt :: "nat ⇒ int ⇒ Valuetype"
where
  "createSInt b v =
    (if v ≥ 0
      then ShowL⇩i⇩n⇩t (-(2^(b-1)) + (v+2^(b-1)) mod (2^b))
      else ShowL⇩i⇩n⇩t (2^(b-1) - (-v+2^(b-1)-1) mod (2^b) - 1))"

declare createSInt_def [solidity_symbex]

lemma upper_bound:
  fixes b::nat
    and c::int
  assumes "b > 0"
      and "c < 2^(b-1)"
    shows "c + 2^(b-1) < 2^b"
proof -
  have a1: "⋀P. (∀b::nat. P b) ⟹ (∀b>0. P ((b-1)::nat))" by simp
  have b2: "∀b::nat. (∀(c::int)<2^b. (c + 2^b) < 2^(Suc b))" by simp
  show ?thesis using a1[OF b2] assms by simp
qed

lemma upper_bound2:
  fixes b::nat
      and c::int
    assumes "b > 0"
      and "c < 2^b"
      and "c ≥ 0"
    shows "c - (2^(b-1)) < 2^(b-1)"
proof -
  have a1: "⋀P. (∀b::nat. P b) ⟹ (∀b>0. P ((b-1)::nat))" by simp
  have b2: "∀b::nat. (∀(c::int)<2^(Suc b). c≥0 ⟶ (c - 2^b) < 2^b)" by simp
  show ?thesis using a1[OF b2] assms by simp
qed

lemma upper_bound3:
  fixes b::nat
    and v::int
      defines "x ≡ - (2 ^ (b - 1)) + (v + 2 ^ (b - 1)) mod 2 ^ b"
    assumes "b>0"
    shows "x < 2^(b-1)"
  using upper_bound2 assms by auto

lemma lower_bound:
    fixes b::nat
  assumes "b>0"
    shows "∀(c::int) ≥ -(2^(b-1)). (-c + 2^(b-1) - 1 < 2^b)"
proof -
  have a1: "⋀P. (∀b::nat. P b) ⟹ (∀b>0. P ((b-1)::nat))" by simp
  have b2: "∀b::nat. ∀(c::int) ≥ -(2^b). (-c + (2^b) - 1) < 2^(Suc b)" by simp
  show ?thesis using a1[OF b2] assms by simp
qed

lemma lower_bound2:
  fixes b::nat
    and v::int
      defines "x ≡ 2^(b - 1) - (-v+2^(b-1)-1) mod 2^b - 1"
    assumes "b>0"
    shows "x ≥ - (2 ^ (b - 1))"
  using upper_bound2 assms by auto

lemma createSInt_id_g0:
    fixes b::nat
      and v::int
  assumes "v ≥ 0"
      and "v < 2^(b-1)"
      and "b > 0"
    shows "createSInt b v = ShowL⇩i⇩n⇩t v"
proof -
  from assms have "v + 2^(b-1) ≥ 0" by simp
  moreover from assms have "v + (2^(b-1)) < 2^b" using upper_bound[of b] by auto
  ultimately have "(v + 2^(b-1)) mod (2^b) = v + 2^(b-1)" by simp
  moreover from assms have "createSInt b v=ShowL⇩i⇩n⇩t (-(2^(b-1)) + (v+2^(b-1)) mod (2^b))" unfolding createSInt_def by simp
  ultimately show ?thesis by simp
qed

lemma createSInt_id_l0:
    fixes b::nat
      and v::int
  assumes "v < 0"
      and "v ≥ -(2^(b-1))"
      and "b > 0"
    shows "createSInt b v = ShowL⇩i⇩n⇩t v"
proof -
  from assms have "-v + 2^(b-1) - 1 ≥ 0" by simp
  moreover from assms have "-v + 2^(b-1) - 1 < 2^b" using lower_bound[of b] by auto 
  ultimately have "(-v + 2^(b-1) - 1) mod (2^b) = (-v + 2^(b-1) - 1)" by simp
  moreover from assms have "createSInt b v= ShowL⇩i⇩n⇩t (2^(b-1) - (-v+2^(b-1)-1) mod (2^b) - 1)" unfolding createSInt_def by simp
  ultimately show ?thesis by simp
qed

lemma createSInt_id:
    fixes b::nat
      and v::int
  assumes "v < 2^(b-1)"
      and "v ≥ -(2^(b-1))"
      and "b > 0"
    shows "createSInt b v = ShowL⇩i⇩n⇩t v" using createSInt_id_g0 createSInt_id_l0 assms unfolding createSInt_def by simp

(*Covered*)
definition createUInt :: "nat ⇒ int ⇒ Valuetype"
  where "createUInt b v = ShowL⇩i⇩n⇩t (v mod (2^b))"

declare createUInt_def[solidity_symbex]

lemma createUInt_id:
  assumes "v ≥ 0"
      and "v < 2^b"
    shows "createUInt b v =  ShowL⇩i⇩n⇩t v"
unfolding createUInt_def by (simp add: assms(1) assms(2))

definition createBool :: "bool ⇒ Valuetype"
where
  "createBool b = ShowL⇩b⇩o⇩o⇩l b"

declare createBool_def [solidity_symbex]

definition createAddress :: "Address ⇒ Valuetype"
where
  "createAddress ad = ad"

declare createAddress_def [solidity_symbex]

definition checkSInt :: "nat ⇒ Valuetype ⇒ bool"
where
  "checkSInt b v = ((foldr (∧) (map is_digit (String.explode v)) True) ∧(ReadL⇩i⇩n⇩t v ≥ -(2^(b-1)) ∧ ReadL⇩i⇩n⇩t v < 2^(b-1)))"

declare checkSInt_def [solidity_symbex]

definition checkUInt :: "nat ⇒ Valuetype ⇒ bool"
where
  "checkUInt b v = ((foldr (∧) (map is_digit (String.explode v)) True) ∧ (ReadL⇩i⇩n⇩t v ≥ 0 ∧ ReadL⇩i⇩n⇩t v < 2^b))"
declare checkUInt_def  [solidity_symbex]

fun convert :: "Types ⇒ Types ⇒ Valuetype ⇒ Valuetype option"
where
  "convert (TSInt b1) (TSInt b2) v =
    (if b1 ≤ b2
      then Some v
      else None)"
| "convert (TUInt b1) (TUInt b2) v =
    (if b1 ≤ b2
      then Some v
      else None)"
| "convert (TUInt b1) (TSInt b2) v =
    (if b1 < b2
      then Some v
      else None)"
| "convert TBool TBool v = Some v"
| "convert TAddr TAddr v = Some v"
| "convert _ _ _ = None"

lemma convert_id[simp]:
  "convert tp tp kv = Some kv"
    by (metis Types.exhaust convert.simps(1) convert.simps(2) convert.simps(4) convert.simps(5) order_refl)

(*Covered informally*)
fun olift ::
  "(int ⇒ int ⇒ int) ⇒ Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "olift op (TSInt b1) (TSInt b2) v1 v2 =
    Some (createSInt (max b1 b2) (op ⌈v1⌉ ⌈v2⌉), TSInt (max b1 b2))"
| "olift op (TUInt b1) (TUInt b2) v1 v2 =
    Some (createUInt (max b1 b2) (op ⌈v1⌉ ⌈v2⌉), TUInt (max b1 b2))"
| "olift op (TSInt b1) (TUInt b2) v1 v2 =
    (if b2 < b1
      then Some (createSInt b1 (op ⌈v1⌉ ⌈v2⌉), TSInt b1)
      else None)"
| "olift op (TUInt b1) (TSInt b2) v1 v2 =
    (if b1 < b2
      then Some (createSInt b2 (op ⌈v1⌉ ⌈v2⌉), TSInt b2)
      else None)"
| "olift _ _ _ _ _ = None"

(*Covered*)
fun plift ::
  "(int ⇒ int ⇒ bool) ⇒ Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "plift op (TSInt b1) (TSInt b2) v1 v2 = Some (createBool (op ⌈v1⌉ ⌈v2⌉), TBool)"
| "plift op (TUInt b1) (TUInt b2) v1 v2 = Some (createBool (op ⌈v1⌉ ⌈v2⌉), TBool)"
| "plift op (TSInt b1) (TUInt b2) v1 v2 =
    (if b2 < b1
      then Some (createBool (op ⌈v1⌉ ⌈v2⌉), TBool)
      else None)"
| "plift op (TUInt b1) (TSInt b2) v1 v2 =
    (if b1 < b2
      then Some (createBool (op ⌈v1⌉ ⌈v2⌉), TBool)
      else None)" 
| "plift _ _ _ _ _ = None"

(*Covered*)
definition add :: "Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "add = olift (+)"

(*Covered informally*)
definition sub :: "Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "sub = olift (-)"

(*Covered informally*)
definition equal :: "Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "equal = plift (=)"

(*Covered informally*)
definition less :: "Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "less = plift (<)"


(*Covered informally*)
definition leq :: "Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "leq = plift (≤)"

declare add_def sub_def equal_def leq_def less_def [solidity_symbex]

(*Covered*)
fun vtand :: "Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "vtand TBool TBool a b =
    (if a = ShowL⇩b⇩o⇩o⇩l True ∧ b = ShowL⇩b⇩o⇩o⇩l True then Some (ShowL⇩b⇩o⇩o⇩l True, TBool)
    else Some (ShowL⇩b⇩o⇩o⇩l False, TBool))"
| "vtand _ _ _ _ = None"

(*Covered informally*)
fun vtor :: "Types ⇒ Types ⇒ Valuetype ⇒ Valuetype ⇒ (Valuetype * Types) option"
where
  "vtor TBool TBool a b =
    (if a = ShowL⇩b⇩o⇩o⇩l False ∧ b = ShowL⇩b⇩o⇩o⇩l False
      then Some (ShowL⇩b⇩o⇩o⇩l False, TBool)
      else Some (ShowL⇩b⇩o⇩o⇩l True, TBool))"
| "vtor _ _ _ _ = None"

definition checkBool :: "Valuetype  ⇒ bool"
where
  "checkBool v = (if (v = STR ''True'' ∨ v = STR ''False'') then True else False)"

declare checkBool_def [solidity_symbex]

definition checkAddress :: "Valuetype  ⇒ bool"
  where
    "checkAddress v = (if (size v = 42 ∧ ((String.explode v !1) = CHR ''x'')) then True else False)"

declare checkAddress_def [solidity_symbex]

(*value "checkBool STR ''True''"*)
(*value "checkAddress STR ''0x0000000000000000000000000000000000000000''"*)

(*Covered informally*)
primrec ival :: "Types ⇒ Valuetype"
where
  "ival (TSInt x) = ShowL⇩i⇩n⇩t 0"
| "ival (TUInt x) = ShowL⇩i⇩n⇩t 0"
| "ival TBool = ShowL⇩b⇩o⇩o⇩l False"
| "ival TAddr = STR ''0x0000000000000000000000000000000000000000''"


declare convert.simps [simp del, solidity_symbex add]
declare olift.simps [simp del, solidity_symbex add]
declare plift.simps [simp del, solidity_symbex add]
declare vtand.simps [simp del, solidity_symbex add]
declare vtor.simps [simp del, solidity_symbex add]

end