kadena-io / pact

The Pact Smart Contract Language
https://pact-language.readthedocs.io/en/stable/
BSD 3-Clause "New" or "Revised" License
580 stars 100 forks source link

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

Open chicodias opened 3 months ago

chicodias commented 3 months ago

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