Open thomashoneyman opened 7 months ago
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.
Unfortunately, I can confirm this bug :+1: Thank you for the report @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.The repl output is:
I tried some alternatives, too. Extract the inline (+) to be a named function has the same issue:
So does using an explicit lambda:
However, replacing
zip
with a map over an enumerate does work, but it's pretty ugly:Ideally I could use
zip
in my module and still be able to use formal verification.