kadena-io / pact

The Pact Smart Contract Language
https://docs.kadena.io/build/pact
BSD 3-Clause "New" or "Revised" License
579 stars 100 forks source link

FV: Using time manipulated enforcements within a function that uses FV #1291

Closed EnoF closed 1 year ago

EnoF commented 1 year ago

Issue description

When using a function that enforces a parameters that are related to time, FV during verification does not handle time correctly causing the function to always fail within FV.

Steps to reproduce

(env-data 
  { 'ks: 
    { 'keys: 
      [ 'ns-pubkey ]
    }
  }
)
(env-keys ['ns-pubkey])
(begin-tx)
(define-namespace 'free (read-keyset 'ks) (read-keyset 'ks))
(commit-tx)
(env-data 
  { 'ks: 
    { 'keys: 
      [ 'pubkey ]
    }
  }
)
(begin-tx)
(namespace 'free)
(define-keyset "free.some-ks" (read-keyset 'ks))
(module test G
  (defcap G() (enforce-keyset "free.some-ks"))

  (defun test(from:time to:time)
    @model [
      (property (authorized-by "free.some-ks"))
    ]
    (with-capability (G)
      (enforce (>= (diff-time to from) (days 1.0)) "Needs to be 1 day difference")
    )
  )
)
(commit-tx)

(verify "free.test")

Expected Behavior

In this example I use authorized-by as a way to illustrate how verification fails because the function can never succeed. I expected this to succeed, but the function can never succeed.

Debug Information

I suspect that the time is converted to decimal/integer hence diff-time will never succeed.

Vacuous property encountered! There is no way for a transaction to succeed if this function is called from the top-level. Because all `property` expressions in Pact assume transaction success, in this case it would be possible to validate *any* `property`, even e.g. `false`.