search

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

Verify DEBUG feature is not working #1306

Closed d3mage closed 9 months ago

d3mage commented 11 months ago

Issue description

Documentation regarding the verify function states that

If DEBUG is set to true, write debug output to “pact-verify-MODULE” directory"

I have run verify function with DEBUG set to true on my module. Indeed, it has created a folder pact-verify-free.module-name, but the folder was completely empty.

Steps to reproduce

Run verify function with DEBUG flag set to true

Expected Behavior

Created a new folder with debug output

Debug Information

Pact v.4.9

rsoeldner commented 11 months ago

@d3mage thank you for bringing this up. Can you please provide more context, such as the contract you try to verify, does the verification succeed or fail, etc.

d3mage commented 11 months ago

@rsoeldner I have tried it with multiple files - but none of them work. I launch the verification from .repl file. It successfully completes verification and finds the issues.

rsoeldner commented 11 months ago

@d3mage, I'm not able to reproduce this:

pact> (module test G (defcap G () true) (defun test () @model[(property (= result 0))] 0))
"Loaded module test, hash vgTEIbHuMNv4KsNS1YNLWa_LfrlNyP9rBlg7-BXT2z0"
pact> (verify 'test true)
"Verification of test succeeded"

successfully creates a directory, including files:

> ls pact-verify-test/
property-test-CheckDefun-satisfaction.smt  property-test-CheckDefun-validation.smt

Can you please verify, that you have z3 available? Additionally, it would be good if you try the example above.

d3mage commented 11 months ago

@rsoeldner I can confirm that the example you've provided me with works on my side. image

rsoeldner commented 11 months ago

Great, can you send me a reference (gist, repo, ..) to a module which does not work?

d3mage commented 11 months ago

@rsoeldner https://gist.github.com/d3mage/e62261c77faa607022d506024865699d

rsoeldner commented 9 months ago

@d3mage Thank you and excuse the late answer. I've just checked - you missed adding any @model annotation. Without this, you are actually not going to prove something. You can find some introduction here: https://docs.kadena.io/pact/reference/property-checking

I'm going to close this issue. Feel free to re-open it in case something is still unclear or bring up your question on Discord.