Symbolic error tracing issue in recursive function for rosette synthesis

[sahilbhatia17]

We are trying to use Rosette for synthesis, specifically involving a recursive function that accepts a list of lists as input and performs certain operations using the current row and the next row. When we invoke the function with specific inputs, we obtain the correct result. However, when we invoke the function with symbolic inputs (using "take"), the symbolic error tracing produces an error, ultimately leading to a failure in our synthesis process. Below is a simplified version of our code.

#lang rosette
(require rosette/lib/angelic rosette/lib/match rosette/lib/synthax)
(require racket/pretty)

(define-symbolic test_arg0 integer?)
(define-symbolic test_arg1 integer?)
(define-symbolic test_arg2 integer?)
(define-symbolic test_arg3 integer?)
(define-symbolic test_arg4 integer?)
(define-symbolic test_arg5 integer?)
(define-symbolic test_arg6 integer?)
(define-symbolic test_arg7 integer?)
(define-symbolic test_arg_len integer?)
(define test_arg (take (list (list test_arg0 test_arg1 test_arg2 test_arg3) (list test_arg4 test_arg5 test_arg6 test_arg7)) test_arg_len))

(define (test inp)
    (if (<= (length inp) 1)
        '()
        (cons (+ 
                (list-ref (list-ref inp 0) 0) 
                (list-ref (list-ref inp 1) 0)
              ) 
              (test (list-tail inp 1)))
    ) 
)
(define expected (list 6 14 22))
(equal? (test (list (list 1 2 3 4) (list 5 6 7 8) (list 9 10 11 12) (list 13 14 15 16))) expected)
;this throws an error 
(test test_arg)

During the execution of (test test_arg), the symtrace encounters an error stating '[assert] list-ref: index is too large' on line 21. It appears that the error is related to accessing the next row in the function. Are there alternative approaches to accessing the next row within the function?

[sorawee]

Can you say more about "leading to a failure in our synthesis process"? The above code that you show doesn't have any synthesis query.

Not all errors appeared in the symbolic error tracer are your "fault." For example, it could contain errors that are generated from infeasible program state. Since these errors actually occur under symbolic evaluation, the symbolic error tracer is correct to log them. They simply might not be useful to you.

As far as I can tell, your program seems to work fine. For example, (solve (assert (equal? (test test_arg) (list 6)))) produces:

(model
 [test_arg0 6]
 [test_arg4 0]
 [test_arg_len 2])

which says that when test_arg0 is 6, test_arg4 is 0, and test_arg_len is 2, calling (test test_arg) will return (list 6).

[sahilbhatia17]

thank you for your response! We encountered an issue while attempting to verify a solution against a specification (invariant => post-condition). I have made updates to the code provided below, addressing the verification problem. Interestingly, even for an incorrect solution, the solver still returns unsat. For instance, in the code snippet below, the right-hand side of the implication uses "kernel2" in the test function, while the left-hand side utilizes "kernel1," yet the solver still returns unsat. The correct solution should involve the usage of "kernel1" in the test function. The only error we observe in the symtrace is [assert] list-ref: index is too large on (nested-ref-noerr inp 1)

#lang rosette
(require rosette/lib/angelic rosette/lib/match rosette/lib/synthax)
(require racket/pretty)

(define (list-ref-noerr l i)
  (if (&&  (>= i 0) (< i (length l))) (list-ref l i)
      0))

(define (list-tail-noerr l i)
  (if (&& (>= i 0) (<= i (length l))) (list-tail l i)
      (list)))

(define (list-take-noerr l i)
  (if (<= i 0) (list) (if (&& (>= i 0) (< i (length l))) (take l i) l )))

(define (nested-ref-noerr l i)
  (if (&&  (>= i 0) (< i (length l))) (list-ref l i)
      (list)))

(define (nested-take-noerr l i)
  (if (<= i 0) (list) (if (&& (>= i 0) (< i (length l))) (take l i) l )))

(define-symbolic test_arg0 integer?)
(define-symbolic test_arg1 integer?)
(define-symbolic test_arg2 integer?)
(define-symbolic test_arg3 integer?)
(define-symbolic test_arg4 integer?)
(define-symbolic test_arg5 integer?)
(define-symbolic test_arg6 integer?)
(define-symbolic test_arg7 integer?)
(define-symbolic test_arg_len integer?)
(define test_arg (take (list (list test_arg0 test_arg1 test_arg2 test_arg3) (list test_arg4 test_arg5 test_arg6 test_arg7)) test_arg_len))
(define-symbolic test_i3_0 integer?)
(define-symbolic test_i3_1 integer?)
(define-symbolic test_i3_2 integer?)
(define-symbolic test_i3_3 integer?)
(define-symbolic test_i3_4 integer?)
(define-symbolic test_i3_5 integer?)
(define-symbolic test_i3_6 integer?)
(define-symbolic test_i3_7 integer?)
(define-symbolic test_i3_len integer?)
(define test_i3 (take (list (list test_i3_0 test_i3_1 test_i3_2 test_i3_3) (list test_i3_4 test_i3_5 test_i3_6 test_i3_7)) test_i3_len))
(define-symbolic test_i4_3 integer?)
(define-symbolic test_i6_0 integer?)
(define-symbolic test_i6_1 integer?)
(define-symbolic test_i6_2 integer?)
(define-symbolic test_i6_3 integer?)
(define-symbolic test_i6_4 integer?)
(define-symbolic test_i6_5 integer?)
(define-symbolic test_i6_6 integer?)
(define-symbolic test_i6_7 integer?)
(define-symbolic test_i6_len integer?)
(define test_i67 (take (list (list test_i6_0 test_i6_1 test_i6_2 test_i6_3) (list test_i6_4 test_i6_5 test_i6_6 test_i6_7)) test_i6_len))

(define (test inp kernel)
    (if (<= (length inp) 1)
        '()
        (cons (+ 
         (* (list-ref-noerr (nested-ref-noerr inp 0) 0) (list-ref kernel 0))
         (* (list-ref-noerr (nested-ref-noerr inp 1) 0) (list-ref kernel 1))
              ) 
              (test (list-tail inp 1) kernel))
    ) 
)

(define kernel1 (list 1 1))
(define kernel2 (list 3 4))
(define verification-result
(verify
 (assert
 (=> 
    (&& 
        (equal? test_i67 test_i3_2 ) 
        (&& 
            (&& 
                (>= test_i4_3 0)
                (<= test_i4_3 (- (length test_arg) 1))
                (equal? test_i3 (test (nested-take-noerr test_arg (+ 1 test_i4_3) ) kernel1))
            ) 
            (! (< test_i4_3 (- (length test_arg ) 1 ) ) ) 
        ) 
    ) 
    (equal? test_i67 (test test_arg kernel2)) ) 
)
)
)

verification-result

[sorawee]

Right. In fact, you can replace (equal? test_i67 (test test_arg kernel2)) with #f, and the result will still be (unsat).

The reason is that you have (equal? test_i67 test_i3_2) as an antecedent of =>. The type of test_i67 is a list, but the type of test_i3_2 is an integer. So they will always not be equal, and so the => expression will always be true.

[sahilbhatia17]

Apologies for the confusion. There is a minor typo in the specification. Instead of (equal? test_i67 test_i3_2), it should be (equal? test_i67 test_i3). After fixing this issue, replacing the right-hand side (RHS) with #f does return a model. However, even with the incorrect kernel, the solver still returns unsat.

[sorawee]

The function test consumes inp, which is a list of list of integers, and kernel, which is a list of integers. It then produces a list of integers.

Meanwhile, test_i3 (and test_i67) is a list of list of integers.

So when you write (equal? test_i3 (test ...)), the answer will always be false, unless they are both empty.

If I adjust your program by replacing

(define test_i3 (take (list (list test_i3_0 test_i3_1 test_i3_2 test_i3_3) (list test_i3_4 test_i3_5 test_i3_6 test_i3_7)) test_i3_len))

....

(define test_i67 (take (list (list test_i6_0 test_i6_1 test_i6_2 test_i6_3) (list test_i6_4 test_i6_5 test_i6_6 test_i6_7)) test_i6_len))

with:

(define test_i3 (take (list test_i3_0 test_i3_1 test_i3_2 test_i3_3) test_i3_len))

....

(define test_i67 (take (list test_i6_0 test_i6_1 test_i6_2 test_i6_3) test_i6_len))

I get the expected counterexample.

[sahilbhatia17]

Thanks @sorawee! Indeed it was an issue of shape mismatch which was causing the verifier to return unsat on an incorrect solution.

We encountered another issue while attempting to perform synthesis with a recursive implementation of Convolution2D. Our Convolution2D function takes a 2D matrix as input, which we encode as a list of lists of integers. We have a list-take on the the number of rows to perform synthesis for all lists up to length 2. However, when we tried to add another list=take operation for variable number of columns in the inputs, our Convolution2D implementation hits the recursion bound. We do not observe this issue when the column lengths are fixed.

#lang rosette

(define fuel (make-parameter 64))
(define-syntax-rule
  (define-bounded (id param ...) body ...)
  (define (id param ...)
    (assert (> (fuel) 0) "Out of fuel.")
    (parameterize ([fuel (sub1 (fuel))])
      body ...)))

(define (list-ref-noerr l i)
  (if (&&  (>= i 0) (< i (length l))) (list-ref l i)
      0))

(define (nested-ref-noerr l i)
  (if (&&  (>= i 0) (< i (length l))) (list-ref l i)
      (list)))

(define (nested-prepend i l)
  (if (list? i)
    (if (> (length i ) 0)
    (append (list i) l) (append l i)) (append (list i) l) ))

(define-bounded (conv-inner inp kernel i j)
  (if   (>= j (- (length (nested-ref-noerr inp i)) 1))
        '()
        (cons  (+
                   (* (list-ref-noerr (nested-ref-noerr inp i) j) (list-ref-noerr (nested-ref-noerr kernel 0) 0))
                   (* (list-ref-noerr (nested-ref-noerr inp i) (+ j 1)) (list-ref-noerr (nested-ref-noerr kernel 0) 1))
                   (* (list-ref-noerr (nested-ref-noerr inp (+ i 1)) j) (list-ref-noerr (nested-ref-noerr kernel 1) 0))
                   (* (list-ref-noerr (nested-ref-noerr inp (+ i 1)) (+ j 1)) (list-ref-noerr (nested-ref-noerr kernel 1) 1))
                )  
                (conv-inner inp kernel i (+ j 1))
        )
    )
)

 (define-bounded (conv2d inp kernel)
  (define-bounded (conv2d-helper inp kernel i j)
    (if   (>= i (- (length inp) 1))
        '()
        (nested-prepend 
          (conv-inner inp kernel i j)
                     (conv2d-helper inp kernel (+ i 1) 0) ) ))
    (conv2d-helper inp kernel 0 0))

(define-symbolic test_arg0 integer?)
(define-symbolic test_arg1 integer?)
(define-symbolic test_arg2 integer?)
(define-symbolic test_arg3 integer?)
(define-symbolic test_arg4 integer?)
(define-symbolic test_arg5 integer?)
(define-symbolic test_arg6 integer?)
(define-symbolic test_arg7 integer?)
(define-symbolic test_arg8 integer?)
(define-symbolic test_arg9 integer?)
(define-symbolic test_arg10 integer?)
(define-symbolic test_arg11 integer?)
(define-symbolic test_arg_len integer?)
(define-symbolic test_arg_col integer?)

(define test_arg 
(take 
    (list 
        (take (list test_arg0 test_arg1 test_arg2 test_arg3) test_arg_col)
        (take (list test_arg4 test_arg5 test_arg6 test_arg7) test_arg_col)
        (take (list test_arg8 test_arg9 test_arg10 test_arg11) test_arg_col)
    )  
test_arg_len)
)
 (conv2d test_arg (list (list 1 2) (list 3 4)))

To debug the issue, we tried using (pretty-print-depth #f) to print the full expression. However, this did not provide the desired result. We are looking for suggestions on how to print the full expression to see the full computation and identify the cause of the recursion bound error.

Thank you in advance for any insights or suggestions on how to address this problem

[sorawee]

My understanding is that you get ... in the output, and wish to obtain the full output. Is that correct?

To force Rosette/Racket to fully print the output, set error-print-width with a large value.

But we do not recommend you to do that, because the term can be extremely large. If you really wish to see it, we recommend using the value browser to interactively navigate the structure.

[sorawee]

I will close this since the original issue is resolved.