Split property helpers to their own file

Makefile

@@ -318,7 +318,7 @@ c_emulator/cheri_riscv_rvfi_%: generated_definitions/c/riscv_rvfi_model_%.c $(SA
 	$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(SAIL_RISCV_DIR)/c_emulator/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
 
 latex: $(SAIL_SRCS) Makefile
-	$(SAIL) -latex -latex_prefix sailRISCV -o sail_latex_riscv $(SAIL_SRCS) properties/props.sail
+	$(SAIL) -latex -latex_prefix sailRISCV -o sail_latex_riscv $(SAIL_SRCS) properties/proplib.sail properties/props.sail
 
 generated_definitions/isabelle/$(ARCH)/ROOT: handwritten_support/ROOT
 	mkdir -p generated_definitions/isabelle/$(ARCH)

properties/Makefile

@@ -5,12 +5,13 @@ SRCS+=${TOP}/sail-riscv/model/riscv_xlen32.sail
 SRCS+=${TOP}/src/cheri_prelude.sail
 SRCS+=${TOP}/src/cheri_types.sail
 SRCS+=${TOP}/src/cheri_cap_common.sail
+SRCS+=proplib.sail
 SRCS+=props.sail
 
 all: generate_smt run_smt
 
 generate_smt:
-	sail -smt ${SRCS}
+	sail ${SAIL_FLAGS} -smt ${SRCS}
 
 run_smt:
 	@failure=0; \

properties/proplib.sail

@@ -0,0 +1,32 @@
+
+
+/* Syntactic sugar */
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+val operator --> : forall ('p 'q: Bool). (bool('p), bool('q)) -> bool('p --> 'q)
+function operator --> (p, q) = not_bool(p) | q
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+val operator <--> : forall ('p 'q: Bool). (bool('p), bool('q)) -> bool('p <--> 'q)
+function operator <--> (p, q) = (p --> q) & (q --> p)
+
+/* Useful functions */
+
+/*!
+ * THIS is a helper function to compress and then decompress a Capability.
+ * The [Capability] struct can hold non-encodable values therefore some
+ * properties encode then decode a Capability to check the effect that
+ * compression / decompression has. In general the bounds, address and tag
+ * should be unaffected but the permissions and otype might change.
+ */
+function encodeDecode(c : Capability) -> Capability =  capBitsToCapability(c.tag, capToBits(c))
+
+/*!
+ * THIS is a helper to check that the given Capability is unaffected by
+ * compression / decompression.
+ */
+function capEncodable(c : Capability) -> bool = c == encodeDecode(c)

properties/props.sail

@@ -1,36 +1,3 @@
-
-
-/* Syntactic sugar */
-
-infixr 1 -->
-
-type operator -->('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
-val operator --> : forall ('p 'q: Bool). (bool('p), bool('q)) -> bool('p --> 'q)
-function operator --> (p, q) = not_bool(p) | q
-
-infix 1 <-->
-
-type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
-val operator <--> : forall ('p 'q: Bool). (bool('p), bool('q)) -> bool('p <--> 'q)
-function operator <--> (p, q) = (p --> q) & (q --> p)
-
-/* Useful functions */
-
-/*!
- * THIS is a helper function to compress and then decompress a Capability.
- * The [Capability] struct can hold non-encodable values therefore some
- * properties encode then decode a Capability to check the effect that
- * compression / decompression has. In general the bounds, address and tag
- * should be unaffected but the permissions and otype might change.
- */
-function encodeDecode(c : Capability) -> Capability =  capBitsToCapability(c.tag, capToBits(c))
-
-/*!
- * THIS is a helper to check that the given Capability is unaffected by
- * compression / decompression.
- */
-function capEncodable(c : Capability) -> bool = c == encodeDecode(c)
-
 // $property
 /*
  * THIS is not actually an invariant but is useful for characterising unusable