# Theory Preliminary_Library

theory Preliminary_Library
imports Main
begin

section ‹Preliminary Theories›
text ‹In this subsection, we provide the type and value system used by the CHERI-C Memory Model.
We also provide proofs for the conversion between large words (i.e. bits) and a list of bytes.
For primitive bytes that are not $U8_\tau$ or $S8_\tau$, we need to be able to convert between
their normal representation and list of bytes so that storing values work as intended.
The high-level detail is given in the paper~\cite{park_2022}.›
subsection ‹Types and Values›
text ‹We first formalise the capability type. We first define \textit{memory capabilities} as a record,
then we define \textit{tagged capabilities} by extending the record. We state the class
comp\_countable for future work, but countable is sufficient for the block\_id type.
For the permissions, we present only those used by the memory model.›
class comp_countable = countable + zero + ord

record ('a :: comp_countable) mem_capability =
block_id :: "'a" (* block_id *)
offset :: int (* offset/address *)
base :: nat (* metadata *)
len :: nat
perm_store :: bool
perm_cap_store :: bool
perm_cap_store_local :: bool
perm_global :: bool

record ('a :: comp_countable) capability = "'a mem_capability" +
tag :: bool (* tag *)

text ‹cctype corresponds to $\tau$ in the paper~\cite{park_2022}, where $\tau$ is the type system.›
datatype cctype =
Uint8
| Sint8
| Uint16
| Sint16
| Uint32
| Sint32
| Uint64
| Sint64
| Cap

text ‹$'a\ ccval$ corresponds to $\mathcal{V}_\mathcal{C}$ in the paper~\cite{park_2022}. $'a$ in
this instance must be countable. ›
datatype 'a ccval =
Uint8_v      "8 word"
| Sint8_v    "8 sword"
| Uint16_v   "16 word"
| Sint16_v   "16 sword"
| Uint32_v   "32 word"
| Sint32_v   "32 sword"
| Uint64_v   "64 word"
| Sint64_v   "64 sword"
| Cap_v      "'a capability"
| Cap_v_frag "'a capability" "nat"
| Undef

text ‹memval\_type infers the type of a value. ›
fun memval_type :: "'a ccval  cctype"
where
"memval_type v = (case v of
Uint8_v  _  Uint8
| Sint8_v  _  Sint8
| Uint16_v _  Uint16
| Sint16_v _  Sint16
| Uint32_v _  Uint32
| Sint32_v _  Sint32
| Uint64_v _  Uint64
| Sint64_v _  Sint64
| Cap_v    _  Cap
| Cap_v_frag _ _  Uint8)"

subsection ‹Primitive Value Conversion and Cast Proof›
text ‹In this subsection, we provide proofs for the conversion between words and list of words.
We also provide proofs that casting primitive values is correct. These will be used by the
\texttt{load} and \texttt{store} operations in the memory model.›
abbreviation encode_u8 :: "nat  8 word"
where
"encode_u8 x  word_of_nat x"

abbreviation decode_u8 :: "8 word  nat"
where
"decode_u8 b  unat b"

abbreviation encode_u8_list :: "8 word  8 word list"
where
"encode_u8_list w  [w]"

abbreviation decode_u8_list :: "8 word list  8 word"
where
"decode_u8_list ls  hd ls"

lemma encode_decode_u8_list:
"ls = [b]  ls = encode_u8_list (decode_u8_list ls)"
by simp

lemma decode_encode_u8_list:

by simp

lemma encode_decode_u8:
"w = encode_u8 (decode_u8 w)"
by simp

lemma decode_encode_u8:
assumes "i  2 ^ LENGTH(8) - 1"
shows "i = decode_u8 (encode_u8 i)"
by (metis assms le_unat_uoi unat_minus_one_word)

abbreviation u64_split :: "64 word  32 word list"
where
"u64_split x  (word_rsplit :: 64 word  32 word list) x"

abbreviation u32_split :: "32 word  16 word list"
where
"u32_split x  (word_rsplit :: 32 word  16 word list) x"

abbreviation u16_split :: "16 word  8 word list"
where
"u16_split x  (word_rsplit :: 16 word  8 word list) x"

abbreviation cat_u16 :: "8 word list  16 word"
where
"cat_u16 x  (word_rcat :: 8 word list  16 word) x"

abbreviation encode_u16 :: "nat  8 word list"
where
"encode_u16 x  u16_split (word_of_nat x)"

abbreviation decode_u16 :: "8 word list  nat"
where
"decode_u16 x  unat (cat_u16 x)"

lemma flatten_u16_length:
"length (u16_split vs) = 2"

lemma rsplit_rcat_eq:
assumes "LENGTH(('b::len)) mod LENGTH(('a::len)) = 0"
and "length w = LENGTH('b) div LENGTH('a)"
shows "(word_rsplit :: 'b word  'a word list) ((word_rcat :: 'a word list  'b word) w) = w"
by (simp add: assms mod_0_imp_dvd size_word.rep_eq word_rsplit_rcat_size)

lemma rsplit_rcat_u16_eq:
assumes "w = [a1, a2]"
shows "(word_rsplit :: 16 word  8 word list) ((word_rcat :: 8 word list  16 word) w) = w"
proof -
have l1: "length w * 8 = 16"
using assms by clarsimp
moreover have l2: "size ((word_rcat :: 8 word list  16 word) w) = 16"
using assms
from l1 l2 have "length w * 8 = size ((word_rcat :: 8 word list  16 word) w)"
by argo
thus ?thesis
by (metis l1 l2 len8 word_rsplit_rcat_size)
qed

lemma encode_decode_u16:
assumes "w = [a, b]"
shows "w = encode_u16 (decode_u16 w)"

lemma cat_flatten_u16_eq:
"cat_u16 (u16_split w) = w"

lemma decode_encode_u16:
assumes "i  2 ^ LENGTH(16) - 1"
shows "i = decode_u16 (encode_u16 i)"
by (metis assms cat_flatten_u16_eq le_unat_uoi unat_minus_one_word)

abbreviation flatten_u32 :: "32 word  8 word list"
where
"flatten_u32 x  (word_rsplit :: 32 word  8 word list) x"

abbreviation cat_u32 :: "8 word list  32 word"
where
"cat_u32 x  (word_rcat :: 8 word list  32 word) x"

abbreviation encode_u32 :: "nat  8 word list"
where
"encode_u32 x  flatten_u32 (word_of_nat x)"

abbreviation decode_u32 :: "8 word list  nat"
where
"decode_u32 i  unat (cat_u32 i)"

lemma flatten_u32_length:
"length (flatten_u32 vs) = 4"

lemma rsplit_rcat_u32_eq:
assumes "w = [a1, a2, b1, b2]"
shows "(word_rsplit :: 32 word  8 word list) ((word_rcat :: 8 word list  32 word) w) = w"
using rsplit_rcat_eq assms
by force

lemma encode_decode_u32:
assumes "w = [a1, a2, b1, b2]"
shows "w = encode_u32 (decode_u32 w)"
using assms

lemma cat_flatten_u32_eq:
"cat_u32 (flatten_u32 w) = w"

lemma decode_encode_u32:
assumes "i  2 ^ LENGTH(32) - 1"
shows "i = decode_u32 (encode_u32 i)"
by (metis assms le_unat_uoi unat_minus_one_word word_rcat_rsplit)

abbreviation flatten_u64 :: "64 word  8 word list"
where
"flatten_u64 x  (word_rsplit :: 64 word  8 word list) x"

abbreviation cat_u64 :: "8 word list  64 word"
where
"cat_u64 x  word_rcat x"

abbreviation encode_u64 :: "nat  8 word list"
where
"encode_u64 x  flatten_u64 (word_of_nat x)"

abbreviation decode_u64 :: "8 word list  nat"
where
"decode_u64 x  unat (cat_u64 x)"

lemma flatten_u64_length:
"length (flatten_u64 vs) = 8"

lemma encode_decode_u64:
assumes "w = [a1, a2, b1, b2, c1, c2, d1, d2]"
shows "w = encode_u64 (decode_u64 w)"
using assms

lemma cat_flatten_u64_eq:
"cat_u64 (flatten_u64 w) = w"

lemma decode_encode_u64:
assumes "i  2 ^ LENGTH(64) - 1"
shows "i = decode_u64 (encode_u64 i)"
by (metis assms le_unat_uoi unat_minus_one_word word_rcat_rsplit)

abbreviation encode_s8 :: "int  8 sword"
where
"encode_s8 x  word_of_int x"

abbreviation decode_s8 :: "8 sword  int"
where
"decode_s8 b  sint b"

abbreviation encode_s8_list :: "8 sword  8 word list"
where
"encode_s8_list w  [SCAST(8 signed  8) w]"

abbreviation decode_s8_list :: "8 word list  8 sword"
where
"decode_s8_list ls  UCAST(8  8 signed) (hd ls)"

lemma encode_decode_s8_list:
"ls = [b]  ls = encode_s8_list (decode_s8_list ls)"
by simp

lemma decode_encode_s8_list:

by simp

lemma encode_decode_s8:
"w = encode_s8 (decode_s8 w)"
by simp

lemma decode_encode_s8:
assumes "- (2 ^ (LENGTH(8) - 1))  i"
and "i < 2 ^ (LENGTH(8) - 1)"
shows "i = decode_s8 (encode_s8 i)"
by (metis assms More_Word.sint_of_int_eq len_signed)

abbreviation s64_split :: "64 sword  32 word list"
where
"s64_split x  (word_rsplit :: 64 sword  32 word list) x"

abbreviation s32_split :: "32 sword  16 word list"
where
"s32_split x  (word_rsplit :: 32 sword  16 word list) x"

abbreviation s16_split :: "16 sword  8 word list"
where
"s16_split x  (word_rsplit :: 16 sword  8 word list) x"

abbreviation cat_s16 :: "8 word list  16 sword"
where
"cat_s16 x  (word_rcat :: 8 word list  16 sword) x"

abbreviation encode_s16 :: "int  8 word list"
where
"encode_s16 x  s16_split (word_of_int x)"

abbreviation decode_s16 :: "8 word list  int"
where
"decode_s16 x  sint (cat_s16 x)"

lemma flatten_s16_length:
"length (s16_split vs) = 2"

lemma rsplit_rcat_s16_eq:
assumes "w = [a1, a2]"
shows "(word_rsplit :: 16 sword  8 word list) ((word_rcat :: 8 word list  16 sword) w) = w"
proof -
have l1: "length w * 8 = 16"
using assms by clarsimp
moreover have l2: "size ((word_rcat :: 8 word list  16 sword) w) = 16"
using assms
from l1 l2 have "length w * 8 = size ((word_rcat :: 8 word list  16 sword) w)"
by argo
thus ?thesis
qed

lemma encode_decode_s16:
assumes "w = [a, b]"
shows "w = encode_s16 (decode_s16 w)"

lemma cat_flatten_s16_eq:
"cat_s16 (s16_split w) = w"

lemma decode_encode_s16:
assumes "- (2 ^ (LENGTH(16) - 1))  i"
and "i < 2 ^ (LENGTH(16) - 1)"
shows "i = decode_s16 (encode_s16 i)"
by (metis assms cat_flatten_s16_eq len_signed sint_of_int_eq)

abbreviation flatten_s32 :: "32 sword  8 word list"
where
"flatten_s32 x  (word_rsplit :: 32 sword  8 word list) x"

abbreviation cat_s32 :: "8 word list  32 sword"
where
"cat_s32 x  (word_rcat :: 8 word list  32 sword) x"

abbreviation encode_s32 :: "int  8 word list"
where
"encode_s32 x  flatten_s32 (word_of_int x)"

abbreviation decode_s32 :: "8 word list  int"
where
"decode_s32 i  sint (cat_s32 i)"

lemma flatten_s32_length:
"length (flatten_s32 vs) = 4"

lemma rsplit_rcat_s32_eq:
assumes "w = [a1, a2, b1, b2]"
shows "(word_rsplit :: 32 sword  8 word list) ((word_rcat :: 8 word list  32 sword) w) = w"
using rsplit_rcat_eq assms
by force

lemma encode_decode_s32:
assumes "w = [a1, a2, b1, b2]"
shows "w = encode_s32 (decode_s32 w)"
using assms

lemma decode_encode_s32:
assumes "- (2 ^ (LENGTH(32) - 1))  i"
and "i < 2 ^ (LENGTH(32) - 1)"
shows "i = decode_s32 (encode_s32 i)"
by (metis assms len_signed sint_of_int_eq word_rcat_rsplit)

abbreviation flatten_s64 :: "64 sword  8 word list"
where
"flatten_s64 x  (word_rsplit :: 64 sword  8 word list) x"

lemma flatten_s64_length:
"length (flatten_s64 vs) = 8"

abbreviation cat_s64 :: "8 word list  64 sword"
where
"cat_s64 x  word_rcat x"

abbreviation encode_s64 :: "int  8 word list"
where
"encode_s64 x  flatten_s64 (word_of_int x)"

abbreviation decode_s64 :: "8 word list  int"
where
"decode_s64 x  sint (cat_s64 x)"

lemma encode_decode_s64:
assumes "w = [a1, a2, b1, b2, c1, c2, d1, d2]"
shows "w = encode_s64 (decode_s64 w)"
using assms

lemma decode_encode_s64:
assumes "- (2 ^ (LENGTH(64) - 1))  i"
and "i < 2 ^ (LENGTH(64) - 1)"
shows "i = decode_s64 (encode_s64 i)"
by (metis assms len_signed sint_of_int_eq word_rcat_rsplit)

definition word_of_integer :: "integer  'a::len word"
where
"word_of_integer x  word_of_int (int_of_integer x)"

definition sword_of_integer :: "integer  'a::len sword"
where
"sword_of_integer x  word_of_int (int_of_integer x)"

definition integer_of_word :: "'a::len word  integer"
where
"integer_of_word x  integer_of_int (uint x)"

definition integer_of_sword :: "'a::len sword  integer"
where
"integer_of_sword x  integer_of_int (sint x)"

lemma word_integer_eq:

unfolding word_of_integer_def integer_of_word_def
by (metis int_of_integer_of_int integer_of_int_eq_of_int word_uint.Rep_inverse')

lemma sword_integer_eq:

unfolding sword_of_integer_def integer_of_sword_def
by (metis int_of_integer_of_int integer_of_int_eq_of_int word_sint.Rep_inverse')

lemma integer_word_bounded_eq:
assumes "0  i"
assumes "i  2 ^ LENGTH('a::len) - 1"
shows "integer_of_word ((word_of_integer :: integer  'a word) i) = i"
unfolding integer_of_word_def word_of_integer_def
using assms
by (metis integer_less_eq_iff integer_of_int_eq_of_int minus_integer.rep_eq of_int_0_le_iff of_int_eq_1_iff of_int_eq_numeral_power_cancel_iff of_int_integer_of word_of_int_inverse zle_diff1_eq)

lemma integer_sword_bounded_eq:
assumes "- (2 ^ (LENGTH('a::len) - 1))  i"
and "i < 2 ^ (LENGTH('a) - 1)"
shows "integer_of_sword ((sword_of_integer :: integer  'a sword) i) = i"
unfolding integer_of_sword_def sword_of_integer_def
using signed_take_bit_int_eq_self assms
by (smt (verit) diff_numeral_special(11) int_of_integer_numeral integer_less_eq_iff integer_of_int_eq_of_int len_signed minus_integer.rep_eq numeral_power_eq_of_int_cancel_iff of_int_integer_of of_int_power_less_of_int_cancel_iff one_integer.rep_eq sint_of_int_eq uminus_integer.rep_eq)

definition word8_of_integer :: "integer  8 word"
where
"word8_of_integer  word_of_integer"

definition word16_of_integer :: "integer  16 word"
where
"word16_of_integer  word_of_integer"

definition word32_of_integer :: "integer  32 word"
where
"word32_of_integer  word_of_integer"

definition word64_of_integer :: "integer  64 word"
where
"word64_of_integer  word_of_integer"

definition integer_of_word8 :: "8 word  integer"
where
"integer_of_word8  integer_of_word"

definition integer_of_word16 :: "16 word  integer"
where
"integer_of_word16  integer_of_word"

definition integer_of_word32 :: "32 word  integer"
where
"integer_of_word32  integer_of_word"

definition integer_of_word64 :: "64 word  integer"
where
"integer_of_word64  integer_of_word"

lemma word8_integer_eq:

unfolding word8_of_integer_def integer_of_word8_def
using word_integer_eq
by blast

lemma word16_integer_eq:

unfolding word16_of_integer_def integer_of_word16_def
using word_integer_eq
by blast

lemma word32_integer_eq:

unfolding word32_of_integer_def integer_of_word32_def
using word_integer_eq
by blast

lemma word64_integer_eq:

unfolding word64_of_integer_def integer_of_word64_def
using word_integer_eq
by blast

lemma integer_word8_bounded_eq:
assumes "0  i"
and "i  2 ^ LENGTH(8) - 1"
shows
unfolding word8_of_integer_def integer_of_word8_def
using integer_word_bounded_eq assms
by blast

lemma integer_word16_bounded_eq:
assumes "0  i"
and "i  2 ^ LENGTH(16) - 1"
shows
unfolding word16_of_integer_def integer_of_word16_def
using integer_word_bounded_eq assms
by blast

lemma integer_word32_bounded_eq:
assumes "0  i"
and "i  2 ^ LENGTH(32) - 1"
shows
unfolding word32_of_integer_def integer_of_word32_def
using integer_word_bounded_eq assms
by blast

lemma integer_word64_bounded_eq:
assumes "0  i"
and "i  2 ^ LENGTH(64) - 1"
shows
unfolding word64_of_integer_def integer_of_word64_def
using integer_word_bounded_eq assms
by blast

definition sword8_of_integer :: "integer  8 sword"
where
"sword8_of_integer  sword_of_integer"

definition sword16_of_integer :: "integer  16 sword"
where
"sword16_of_integer  sword_of_integer"

definition sword32_of_integer :: "integer  32 sword"
where
"sword32_of_integer  sword_of_integer"

definition sword64_of_integer :: "integer  64 sword"
where
"sword64_of_integer  sword_of_integer"

definition integer_of_sword8 :: "8 sword  integer"
where
"integer_of_sword8  integer_of_sword"

definition integer_of_sword16 :: "16 sword  integer"
where
"integer_of_sword16  integer_of_sword"

definition integer_of_sword32 :: "32 sword  integer"
where
"integer_of_sword32  integer_of_sword"

definition integer_of_sword64 :: "64 sword  integer"
where
"integer_of_sword64  integer_of_sword"

lemma sword8_integer_eq:

unfolding sword8_of_integer_def integer_of_sword8_def
using sword_integer_eq
by blast

lemma sword16_integer_eq:

unfolding sword16_of_integer_def integer_of_sword16_def
using sword_integer_eq
by blast

lemma sword32_integer_eq:

unfolding sword32_of_integer_def integer_of_sword32_def
using sword_integer_eq
by blast

lemma sword64_integer_eq:

unfolding sword64_of_integer_def integer_of_sword64_def
using sword_integer_eq
by blast

lemma integer_sword8_bounded_eq:
assumes "- (2 ^ (LENGTH(8) - 1))  i"
and "i < 2 ^ (LENGTH(8) - 1)"
shows
unfolding sword8_of_integer_def integer_of_sword8_def
using integer_sword_bounded_eq assms
by metis

lemma integer_sword16_bounded_eq:
assumes "- (2 ^ (LENGTH(16) - 1))  i"
and "i < 2 ^ (LENGTH(16) - 1)"
shows
unfolding sword16_of_integer_def integer_of_sword16_def
using integer_sword_bounded_eq assms
by metis

lemma integer_sword32_bounded_eq:
assumes "- (2 ^ (LENGTH(32) - 1))  i"
and "i < 2 ^ (LENGTH(32) - 1)"
shows
unfolding sword32_of_integer_def integer_of_sword32_def
using integer_sword_bounded_eq assms
by metis

lemma integer_sword64_bounded_eq:
assumes "- (2 ^ (LENGTH(64) - 1))  i"
and "i < 2 ^ (LENGTH(64) - 1)"
shows
unfolding sword64_of_integer_def integer_of_sword64_def
using integer_sword_bounded_eq assms
by metis

lemmas flatten_types_length = flatten_u16_length flatten_s16_length flatten_u32_length flatten_s32_length flatten_u64_length flatten_s64_length

text ‹cast\_val is an executable code that ensures easy casting of values. This value cast function
is used within the Gillian
framework~\cite{old_gillian_2020, gillian_2021, maksimovic_2021, fragoso_2020}.›
definition cast_val ::
where
"cast_val s i
if s = STR ''uint8'' then integer_of_word8 (word8_of_integer i)
else if s = STR ''int8'' then integer_of_sword8 (sword8_of_integer i)
else if s = STR ''uint16'' then integer_of_word16 (word16_of_integer i)
else if s = STR ''int16'' then integer_of_sword16 (sword16_of_integer i)
else if s = STR ''uint32'' then integer_of_word32 (word32_of_integer i)
else if s = STR ''int32'' then integer_of_sword32 (sword32_of_integer i)
else if s = STR ''uint64'' then integer_of_word64 (word64_of_integer i)
else if s = STR ''int64'' then integer_of_sword64 (sword64_of_integer i)
else i"

end