-
Notifications
You must be signed in to change notification settings - Fork 102
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Vacuous property warning in fungible-v2 for upcoming 4.6.0 release #1136
Labels
FV
Formal verification
Comments
Thanks, @thomashoneyman! Pinging @rsoeldner |
@thomashoneyman, great you brought this one up. Especially, the |
We started addressing this in the KIP-0019: kadena-io/KIPs#43 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 offungible-v2.pact
I am seeing: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!The text was updated successfully, but these errors were encountered: