Skip to content
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

FV: Unable to use (fold) in @model Property Definitions #1361

Open
chicodias opened this issue May 6, 2024 · 0 comments
Open

FV: Unable to use (fold) in @model Property Definitions #1361

chicodias opened this issue May 6, 2024 · 0 comments

Comments

@chicodias
Copy link

Issue Description

The fold function fails to parse when used within a @model property definition in Pact, as demonstrated in the module A below. Replacing fold with and logical operators in module B works as expected. Documentation for fold usage can be found here.

Steps to Reproduce

Failing Scenario: Module A with fold

  1. Code:
    (module A G
      @model
      [
        (defproperty test-prop
          (cond1:bool cond2:bool cond3:bool)
          (fold (and) true [cond1 cond2 cond3])
        )
      ]
    
      (defcap G() true)
    
      (defun T(v1:bool v2:bool v3:bool)
        @model [ (property (test-prop v1 v2 v3))]
        true)
    )
    
    (verify "A")
  2. Verification Output:
    "Verification of A failed"
    :OutputFailure: test.pact:20:23: could not parse (test-prop v1 v2 v3): in (fold (and) true [cond1,cond2,cond3]), couldn't find property named fold
    

Working Scenario: Module B with and

  1. Code:
    (module B G
      @model
      [
        (defproperty test-prop
          (cond1:bool cond2:bool cond3:bool)
          (and (and cond1 cond2) cond3)
        )
      ]
    
      (defcap G() true)
    
      (defun T(v1:bool v2:bool v3:bool)
        @model [ (property (test-prop v1 v2 v3))]
        true)
    )
    
    (verify "B")
  2. Verification Output:
    "Verification of B succeeded"
    test2.pact:18:23:OutputFailure: Invalidating model found in B.T
      Program trace:
        entering function B.T with arguments
          v1 = False
          v2 = False
          v3 = False
    
          returning with False
    

Expected Behavior

The fold function should be parsed correctly and utilized in property definitions within @model blocks, as per its documentation.

Actual Behavior

The use of fold results in a parsing error during the verification process, whereas using nested and operators does not cause any parsing issues and behaves as expected.

Debug Information

  • Pact Version: 4.11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant