archdoc/chap-encoding-sail: prettify & add props

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}
+\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}

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
 /*!