search

kadena-io / pact

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

Vacuous property warning in fungible-v2 for upcoming 4.6.0 release #1136

Open thomashoneyman opened 1 year ago

thomashoneyman commented 1 year ago

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!

jwiegley commented 1 year ago

Thanks, @thomashoneyman! Pinging @rsoeldner

rsoeldner commented 1 year ago

@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).

rsoeldner commented 1 year ago

We started addressing this in the KIP-0019: https://github.com/kadena-io/KIPs/pull/43