Unexpected 'free variable' in formal verification when using zip

[thomashoneyman]

I am encountering an unexpected 'free variable' error in formal verification in a module that uses the zip function. Potentially related to #1250 but not fixed by #1251. This is on Pact 4.8.

(module zip-m GOV
  (defcap GOV () true)
  (defun try-zip ()
    (zip (+) [1] [2])))

(verify "zip-m")

The repl output is:

λ pact zip.repl
zip.repl:3:2:OutputFailure: invariant violation: free variable unexpectedly found
Load successful

I tried some alternatives, too. Extract the inline (+) to be a named function has the same issue:

module zip-m GOV
  (defcap GOV () true)

  (defun try-zip ()
    (zip (add) [1] [2]))

  (defun add (a:integer b:integer)
    (+ a b))
)
(verify "zip-m")

So does using an explicit lambda:

(module zip-m GOV
  (defcap GOV () true)
  (defun try-zip ()
    (zip (lambda (a b) (+ a b)) [1] [2]))
)
(verify "zip-m")

However, replacing zip with a map over an enumerate does work, but it's pretty ugly:

module zip-m GOV
  (defcap GOV () true)
  (defun try-zip ()
    (let
      ((listA:[integer] [1])
       (listB:[integer] [2]))
    (map
      (lambda (ix) (+ (at ix listA) (at ix listB)))
      (enumerate 0 (- (length listA) 1)))))
)
(verify "zip-m")

Ideally I could use zip in my module and still be able to use formal verification.

[thomashoneyman]

Actually, even replacing with a map over enumerate doesn't work once you introduce a @model to the function as well:

(module zip-m GOV
  (defcap GOV () true)
  (defun try-zip (listA:[integer] listB:[integer])
    @model [ (property (= (length listA) (length listB))) ]
    (enforce (= (length listA) (length listB)) "list length differs")
    (map
      (lambda (ix) (+ (at ix listA) (at ix listB)))
      (enumerate 0 (- (length listA) 1))))
)
(verify "zip-m")

This code just hangs forever.

[rsoeldner]

Unfortunately, I can confirm this bug 👍 Thank you for the report @thomashoneyman