Soundness bug with for/and iteration

[jryans]

As part of exploring SCV for potential use in the future, I believe I encountered a soundness bug related to dependent contracts. Here is a minimised program to show the issue:

#lang racket

(define example
  (build-list 16 values))

(define (check-list input)
  ;; A real check would do something more interesting than `#f`
  (for/and ([_ input]) #f))

(define/contract (modify-list input)
  (->i ([input list?]) [result (input) (λ (res) (check-list res))])
  ;; A real modification would change something
  input)

(displayln (check-list (modify-list example)))

Running this in normal Racket shows a contract failure:

$ racket dependent-contract.rkt
modify-list: broke its own contract
  promised: ...endent-contract.rkt:11:39
  produced: '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)
  in: the result result of
      (->i
       ((input (listof any/c)))
       (result
        (input)
        (λ (res) (check-list res))))
  contract from: (function modify-list)
  blaming: (function modify-list)
   (assuming the contract is correct)
  at: /Users/jryans/Projects/Static Contract Verification/racket/dependent-contract.rkt:10:18
  context...:
   /Applications/Racket v8.8/collects/racket/contract/private/blame.rkt:346:0: raise-blame-error
   /Applications/Racket v8.8/collects/racket/contract/private/arr-i.rkt:961:8
   /Users/jryans/Projects/Static Contract Verification/racket/dependent-contract.rkt:15:0
   body of "/Users/jryans/Projects/Static Contract Verification/racket/dependent-contract.rkt"

SCV though believes it is safe:

$ raco scv dependent-contract.rkt
Safe

It's possible I've misunderstood something here... My apologies if so!

I'd really like to make use of SCV if possible, so it would be great to understand what's happened here in more detail. 😄

[philnguyen]

It looks like there's a bug in either parsing or executing the for/and loop. raco scv-ing The following will print out that it thinks the loop returns #t instead of #f. It probably thinks it only executes 0 iteration for some reason:

(define/contract x none/c
  (for/and ([_ (list 1)]) #f))

[jryans]

Ah thanks, it does indeed seem like the handling of for/and is the actual issue here somehow.

Is there perhaps some specialised parsing / execution of the for iteration forms somewhere in SCV that needs extending / fixing then? It's a bit hard to search for a basic keyword like for... 😅

I'd like to attempt fixing this issue (as a way of better understanding SCV's codebase). If there are any hints you can offer on roughly where to look, that would be quite helpful.