pact
pact copied to clipboard
kadena-io
Vacuous property warning in fungible-v2 for upcoming 4.6.0 release
While testing #1133 I noticed that the upcoming 4.6.0 release (ie. 64d5845) is reporting a number of output failures in formal verification, (perhaps related to #627 and #623) in the fungible-v2 contract. Specifically, with a local copy of fungible-v2.pact I am seeing:
fungible-v2.pact:89:24:OutputFailure: 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`.
fungible-v2.pact:90:24:OutputFailure: 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`.
fungible-v2.pact:91:24:OutputFailure: 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`.
fungible-v2.pact:92:24:OutputFailure: 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`.
fungible-v2.pact:93:24:OutputFailure: 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`.
The offending lines are in (transfer-crosschain):
https://github.com/kadena-io/KIPs/blob/8ec1b7c6e2596778e169182339eeda7acbae4abc/kip-0005/fungible-v2.pact#L73-L95
I'm seeing this when attempting to validate my own token that implements fungible-v2. However, I've noticed that attempting to verify the coin-v5.pact contract is producing a whole bunch of verification failures on the master branch. Not sure if y'all are aware of it, but if not — it's worth a look!
@thomashoneyman, great you brought this one up. We are currently working on this, see https://github.com/kadena-io/chainweb-node/pull/1595.
Especially, the transfer-crosschain requires sender != receiver, which is not a correct property (https://github.com/kadena-io/KIPs/blob/8ec1b7c6e2596778e169182339eeda7acbae4abc/kip-0005/fungible-v2.pact#L92).
We started addressing this in the KIP-0019: https://github.com/kadena-io/KIPs/pull/43