Unable to use (diff-time) in formal verification as a property, contrary to documentation

[thomashoneyman]

Issue description

The Pact documentation notes that diff-time can be used in properties. However, if I attempt to use it in a property as in the below snippet:

(module diff-time-fv GOV
  (defcap GOV () true)
  (defconst EPOCH:time (parse-time "%s" "0"))
  (defun later-than-epoch (timestamp:time)
    @model [(property (>= (diff-time timestamp EPOCH) 0.0))]
    (>= (diff-time timestamp EPOCH) 0.0))
)
(verify "diff-time-fv")

Then I receive the following error:

:OutputFailure: diff-time.repl:5:22: could not parse (>= (diff-time timestamp EPOCH) 0.0): in (diff-time timestamp EPOCH), couldn't find property named diff-time

If I don't use diff-time in the property, I get an warning simply for using diff-time in the body of a function that has a @model:

(module diff-time-fv GOV
  (defcap GOV () true)
  (defconst EPOCH:time (parse-time "%s" "0"))
  (defun later-than-epoch (timestamp:time)
    @model [(property (> 1 0))]
    (>= (diff-time timestamp EPOCH) 0.0))
)
(verify "diff-time-fv")

This produces the following warning:

diff-time.repl:6:8:OutputWarning: Unsupported operation: diff-time: substituting 0.0

This is on Pact 4.8.

[rsoeldner]

@thomashoneyman, thank you for the report.

I can confirm, that you currently can't use diff-time inside the property annotation due to a missing translation, which I've added here: #1349

Is there any reason why you use Pact 4.8, and not a more recent version, i.e. Pact 4.10? The second example is working, as expected, in 4.10.

[thomashoneyman]

Thanks! No particular reason to be on 4.8, just haven’t yet updated to 4.10. So no worries on the second one.