# Theory Valuetypes

```section‹Value Types›

theory Valuetypes
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 Location = String.literal
type_synonym Valuetype = String.literal

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

(*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]

where

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 _ _ _ = 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

(*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)"

(*value "checkBool STR ''True''"*)

(*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
```