From 65b5499652bd6d4cbb18e6b05151ef7a8e32b447 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Tue, 26 Nov 2024 14:14:26 +0000 Subject: [PATCH] archdoc/chap-encoding-sail: prettify & add props --- archdoc/chap-encoding-sail.tex | 50 ++++++++++++++++------------------ properties/props.sail | 25 ++++++++++------- 2 files changed, 38 insertions(+), 37 deletions(-) diff --git a/archdoc/chap-encoding-sail.tex b/archdoc/chap-encoding-sail.tex index 7b70eaa..a18a2ce 100644 --- a/archdoc/chap-encoding-sail.tex +++ b/archdoc/chap-encoding-sail.tex @@ -42,34 +42,30 @@ \section{SMT validation of properties of the capability encoding} Some helper functions are used in the Sail properties: -\medskip -\sailRISCVfn{encodeDecode} - -\medskip -\sailRISCVfn{capEncodable} - -The following functions have been checked to return true for all inputs. - -\medskip -\sailRISCVfn{prop\_decEnc} - -\medskip -\sailRISCVfn{prop\_andperms} +\begin{itemize} + \item \sailRISCVfn{encodeDecode} + \item \sailRISCVfn{capEncodable} +\end{itemize} -\medskip -\sailRISCVfn{prop\_setbounds} +The following nullary properties of the encoding hold. -\medskip -\sailRISCVfn{prop\_setbounds\_monotonic} +\begin{itemize} + \item \sailRISCVfn{prop\_nullzero} + \item \sailRISCVfn{prop\_null\_noperms} + \item \sailRISCVfn{prop\_mem\_root} + \item \sailRISCVfn{prop\_exe\_root} + \item \sailRISCVfn{prop\_seal\_root} +\end{itemize} -\medskip -\sailRISCVfn{prop\_setaddr} - -\medskip -\sailRISCVfn{prop\_repbounds\_c} - -\medskip -\sailRISCVfn{prop\_repbounds} +The following functions have been checked to return true for all inputs. -\medskip -\sailRISCVfn{prop\_crrl\_cram} \ No newline at end of file +\begin{itemize} + \item \sailRISCVfn{prop\_decEnc} + \item \sailRISCVfn{prop\_andperms} + \item \sailRISCVfn{prop\_setbounds} + \item \sailRISCVfn{prop\_setbounds\_monotonic} + \item \sailRISCVfn{prop\_setaddr} + \item \sailRISCVfn{prop\_repbounds\_c} + \item \sailRISCVfn{prop\_repbounds} + \item \sailRISCVfn{prop\_crrl\_cram} +\end{itemize} diff --git a/properties/props.sail b/properties/props.sail index 7f636d7..06ef9eb 100644 --- a/properties/props.sail +++ b/properties/props.sail @@ -19,7 +19,9 @@ $property * Check that null_cap as defined in the Sail encodes to all zeros. */ function prop_nullzero() -> bool = { - capEncodable(null_cap) & (capToBits(null_cap) == zeros()) & (null_cap.tag == false) + capEncodable(null_cap) + & (capToBits(null_cap) == zeros()) + & (null_cap.tag == false) } $property @@ -31,19 +33,22 @@ function prop_null_noperms() -> bool = { } $property -function prop_mem_root() -> bool = { - capEncodable(root_cap_mem) -} +/*! + * Check that [root_cap_mem] is encodable + */ +function prop_mem_root() -> bool = { capEncodable(root_cap_mem) } $property -function prop_exe_root() -> bool = { - capEncodable(root_cap_exe) -} +/*! + * Check that [root_cap_exe] is encodable + */ +function prop_exe_root() -> bool = { capEncodable(root_cap_exe) } $property -function prop_seal_root() -> bool = { - capEncodable(root_cap_seal) -} +/*! + * Check that [root_cap_seal] is encodable + */ +function prop_seal_root() -> bool = { capEncodable(root_cap_seal) } $property /*!