Why is this curried function unsafe?

[dvanhorn]

#lang racket
(require soft-contract/fake-contract)

(define ((g x) y) 0)

(provide/contract
 [g (->i ([x (>=/c 0)])
              [res ()
                   (->i ([y (>=/c 0)])
                        [res () any/c])])])

I don't understand the counterexample, either:

(blame
 (line 10 col 2)
 (violator
  :
  "/Users/dvanhorn/git/soft-contract/soft-contract/test/programs/safe/monotic.rkt")
 (contract
  from
  :
  "/Users/dvanhorn/git/soft-contract/soft-contract/test/programs/safe/monotic.rkt")
 (contracts : |(arity-includes/c 0)|)
 (values : (λ (x₁) … ‖ () ‖)))

[philnguyen]

This is not a satisfactory answer, but current ->i expects the dependency list to be exactly all arguments there are (also in the same order). Parts of the program make that assumption and give weird results otherwise. The following program is safe:

#lang racket

(define ((g x) y) 0)

(provide/contract
 [g (->i ([x (>=/c 0)])
              [res (x)
                   (->i ([y (>=/c 0)])
                        [res (y) any/c])])])

I'll try pushing ->i to full generality this week.

[dvanhorn]

I can live with this for now (I wish the tool signalled an error for an unsupported contract, instead of saying it doesn't verify).

So is there any hope for the following function to be verified?:

(define (f x) (* x 2))
(define ((g x) y)
  (cons (f x) (f y)))

(provide/contract
 [f ((>=/c 0) . -> . (>=/c 0))]
 [g (->i ([x (>=/c 0)])
         [res (x)
              (->i ([y (>=/c x)])
                   [res (y)
                        (λ (p)
                          (>= (cdr p) (car p)))])])])

[philnguyen]

There is. This function is not verifying because of several hard-coded heuristics that favor termination/performance aggressively. Most invariants between multiple values are dropped for allocated fields, and I overly filtered out cases to call out to Z3 and just returned don't know instead.

I'll fix this one soon once I've merge another branch doing some major refactorings.