# Theory CHERI_C_Concrete_Memory_Model

theory CHERI_C_Concrete_Memory_Model
imports "Preliminary_Library"
"Separation_Algebra.Separation_Algebra"
"Containers.Containers"
"HOL-Library.Mapping"
"HOL-Library.Code_Target_Numeral"
begin
section ‹CHERI-C Error System›
text ‹In this section, we formalise the error system used by the memory model.›
text ‹Below are coprocessor 2 excessptions thrown by the hardware.
BadAddressViolation is not a coprocessor 2 exception but remains one given by the hardware.
This corresponds to CapErr in the paper~\cite{park_2022}.›