Proving properties about unbounded sequences

[will62794]

I am curious about the general capability of Z3 to prove properties about unbounded sequences and, more specifically, are there preferred encoding schemes to optimize for this. This question is motivated by some work on verifying certain types of distributed protocols, but I have been experimenting with some abstract examples to get a sense of what Z3 can do here.

Below is a basic first example where I try to prove that if a sequence S of non-negative integers is monotonic (i.e. non-decreasing), and we append a new entry to this sequence that equals the last element of S + 1, then the resulting sequence should also be monotonic. This is just a toy example to use as a baseline for understanding what Z3 can/cannot handle in this domain.

(set-logic ALL)
(declare-const curr (Seq Int))
(declare-const next (Seq Int))

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))

; Sequence monotonicity (nondecreasing) predicate.
; Encoded in terms of 'seq.foldl'.
(define-fun isMonotonicFold ((S (Seq Int))) Bool
    (second (seq.foldl 
                (lambda 
                    ((S (Pair Int Bool)) (x Int)) 
                    (mk-pair x (and (second S) (>= x (first S))))
                ) (mk-pair 0 true) S))
)

; Sequence monotonicity (nondecreasing) predicate.
; Encoded in terms of quantifiers over sequence indices.
(define-fun isMonotonicQuant ((S (Seq Int))) Bool
    (forall ((i Int) (j Int))
        (=> 
            (and (< j (seq.len S)) (< i j) (>= i 0))
            (<= (seq.nth S i) (seq.nth S j))
        )
    )
)

; All elements of 'curr' are >= 0.
(assert (seq.foldl (lambda ((S Bool) (x Int)) (and S (>= x 0))) true curr))

; Define 'next' in terms of 'curr' i.e. 'next' is constructed by appending
; to 'curr' the last element of 'curr' + 1. 
; This should imply that 'next' is monotonic if 'curr' was monotonic.
(assert (= next 
    (seq.++ 
        curr 
        (seq.unit (+ 1 (seq.nth curr (- (seq.len curr) 1)))) 
    )))

; Lower bound on length.
(assert (> (seq.len curr) 0))

; Define max upper bound on sequence length.
(declare-const max_len Int)
(assert (= max_len 15))

(echo "-- FOLD")
(push 1)

    ; Assert that the 'curr' is monotonic and try to prove that there are no 
    ; violations to monotonicity in next state.
    ; (FOLD based version)
    (assert (isMonotonicFold curr))
    (assert (not (isMonotonicFold next)))

    ; Try solving with large but finite sequence length upper bound.
    (push 1)
    (echo "# (finite bound)")
    (assert (<= (seq.len curr) max_len))
    (assert (<= (seq.len next) max_len))
    (check-sat)
    (get-info :all-statistics)
    (pop 1)

    ; Try solving with no sequence length upper bound.
    (echo "# (unbounded)")
    (check-sat)
    (get-info :all-statistics)
(pop 1)


(echo "-- QUANTIFIED")
(push 1)

    ; Assert that the 'curr' is monotonic and try to prove that there are no 
    ; violations to monotonicity in next state.
    ; (QUANTIFIED version)
    (assert (isMonotonicQuant curr))
    (assert (not (isMonotonicQuant next)))

    ; Try solving with large but finite sequence length upper bound.
    (push 1)
    (echo "# (finite bound)")
    (assert (<= (seq.len curr) max_len))
    (assert (<= (seq.len next) max_len))
    (check-sat)
    (get-info :all-statistics)
    (pop 1)

    ; Try solving with no sequence length upper bound.
    (echo "# (unbounded)")
    (check-sat)
    (get-info :all-statistics)
(pop 1)

As part of the above test, I defined the monotonicity predicate both in terms of seq.foldl and also using quantifiers over sequence indices. So, the above script tests 4 cases i.e, using the seq.foldl version with and without finite bounds on the sequence length, and using the quantified variant with/without finite bounds.

Running this on a 2020 M1 Macbook (Z3 version 4.12.2) with

z3 -t:30000 seq.smt 

gives the following results (omitting the extra info from (get-info :all-statistics)):

-- FOLD
# (finite bound)
unsat
 :time                        0.24)
# (unbounded)
unknown
 :time                        30.01)
-- QUANTIFIED
# (finite bound)
unknown
 :time                        30.00)
# (unbounded)
unknown
 :time                        30.01)

So, initially, it seems that Z3 has little issue proving this for some reasonable finite bound, using the fold-based encoding. If I reduce the max_len bound to around 10, it can also prove the quantified version in a second or so. I have not tried running this test for longer timeout bounds, which I can do, but I wanted to first see if this is generally the suggested way to encode this kind of problem to give the best chance of getting a proof, before running more thorough experiments.

The Z3 sequences guide mentions that

The decision procedure for map and fold behaves similar to recursive function unfolding, thus they are mostly effective when there is a finite satisfying model or the proof of unsatisfiability does not require inventing auxiliary inductive relations.

so it seemed this may be an indication that getting full proofs for unbounded sequences is not generally a strength of Z3 in its current form, but I wasn't sure.

Any suggestions or general advice on this problem would be appreciated.