Vacuous property warning in fungible-v2 for upcoming 4.6.0 release

[thomashoneyman]

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]

Thanks, @thomashoneyman! Pinging @rsoeldner

[rsoeldner]

@thomashoneyman, great you brought this one up.
We are currently working on this, see kadena-io/chainweb-node#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]

We started addressing this in the KIP-0019: kadena-io/KIPs#43