1 files changed, 104 insertions, 0 deletions
diff --git a/proofs/lfsc/signatures/util_defs.plf b/proofs/lfsc/signatures/util_defs.plf
new file mode 100644
index 000000000..5639cc54e
--- /dev/null
+++ b/proofs/lfsc/signatures/util_defs.plf
@@ -0,0 +1,104 @@
+; depends: core_defs.plf
+
+; This file contains utilities used throughout the proof signatures.
+
+; A "flag" is a Boolean value.
+(declare flag type)
+(declare tt flag)
+(declare ff flag)
+
+; "Ok" is a unit value, used to indicate that e.g. a side condition ran successfully.
+(declare Ok type)
+(declare ok Ok)
+
+; A pair of terms.
+(declare termPair type)
+(declare pair (! first term (! second term termPair)))
+
+; Bits, used to represent bit-vectors
+(declare bit type)
+(declare b0 bit)
+(declare b1 bit)
+
+; A bit-vector, which is a list of bits. Used to represent a value of bit-vector type.
+(declare bitvec type)
+(declare bvn bitvec)
+(declare bvc (! b bit (! v bitvec bitvec)))
+
+;; ---- Side conditions
+
+; Get the argument from an f-application t, fail if t is not an f-application.
+(program getarg ((f term) (t term)) term
+  (match t ((apply t1 t2) (ifequal t1 f t2 (fail term)))))
+
+; Get the argument from an f-application t, return the term t itself if it is not an f-application.
+(program try_getarg ((f term) (t term)) term
+  (match t ((apply t1 t2) (ifequal t1 f t2 t)) (default t)))
+
+; Convert to original form.
+; This replaces the Skolems that occur in `t` with their witness terms provided
+; that the witness term of `t` is *not* an application of the witness
+; quantifier. In other words, Skolem variables whose witness terms have
+; witness quantification are left unchanged; all others are converted. This
+; method is commonly used to recovert the "unpurified" version of a term, so
+; that certain reasoning steps e.g. witness sharing (see Reynolds et al
+; FMCAD 2020) can be justified.
+(program sc_to_original ((t term)) term
+  (match t
+    ((apply t1 t2) (apply (sc_to_original t1) (sc_to_original t2)))
+    ((skolem w)
+      ; witness terms stay beneath skolems, other terms are converted
+      (match w
+        ((apply w1 w2)
+          (match w1
+            ((f_witness v s) t)
+            (default w)))
+        (default w)))
+    (default t)
+  ))
+
+; Make a skolem, which ensures that the given term is in original form. For
+; consistency, we require that the witness term for all Skolems are in
+; original form. Failure to use this side condition when introducing fresh
+; Skolems will result in proofs failing to check due to mismatched uses of
+; Skolem variables in conclusions.
+(program sc_mk_skolem ((t term)) term (skolem (sc_to_original t)))
+
+;; ---- Proof rules
+
+; "proof-let", which is used to introduce a variable corresponding to the
+; conclusion of a proof. For example:
+;   `(plet _ _ P (\ u Q))`
+; is a proof where the variable `u` has type `(holds g)`, where `g` is
+; the conclusion of proof `P`. Notice that `u` can be freely used in `Q`. We
+; use this rule whenever a proof is used multiple times in a scope, for the
+; purposes of compressing the size of proofs.
+
+(declare plet (! f term
+              (! g term
+              (! p (holds g)
+              (! u (! v (holds g) (holds f)) 
+                (holds f))))))
+
+; "scope", which defines a proof under an assumption. This introduces an
+; assumption that can be used in a child proof, and concludes a disjunction
+; having that assumption. For example:
+;   `(scope _ g (\ u Q))`
+; is a proof where the variable `u` has type `(holds g)`, which can be freely
+; used in `Q`. If `Q` has type `(holds f)`, the above has type
+; `(holds (or (not g) f))`, in other words, either the assumption `g` does not
+; hold, or `f` holds.
+; Note that this assumes f is in n-ary, null-terminated form (see
+; nary_programs.plf).
+; This rule corresponds to the cvc5 internal calculus rule "SCOPE".
+
+(declare scope (! f term
+               (! g term
+               (! u (! v (holds g) (holds f))
+                  (holds (or (not g) f))))))
+
+; "trust", which is used when the proof of a given fact `f` was not provided
+; by the solver. Any LFSC proof with trust indicates that the proof was
+; incomplete.
+
+(declare trust (! f term (holds f)))