1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
; 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)))
; Returns term t if v1 = v2, and term s otherwise.
(program mpz_ifequal ((v1 mpz) (v2 mpz) (t term) (s term)) term
(mp_ifzero (mp_add (mp_neg v1) v2) t s)
)
;; ---- 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)))
|
