Kadena Pact Property Check

Question

The Pact Language has a property system. The call to create-account should fail for accounts shorter than 3 and longer than 256 chars. However, I couldn't make it work.

This is the result of REPL unit test.

I was expecting the create-account call with a name shorter than 3 chars to fail.

"FAILURE: empty account names fail to create: expected failure, got result = "Write succeeded""
"FAILURE: account names not >= 3 chars fail: expected failure, got result = "Write succeeded""
"FAILURE: account names not <= 256 chars fail: expected failure, got result = "Write succeeded""

create-account function with validate-id

  (defun create-account:string
    ( account:string
      guard:guard )

    @doc " Create a new account. "

    @model [ (property (valid-account-id account)) ]
    (enforce-reserved account guard)

    (insert token-table account
      { "balance" : 0.0
      , "guard"   : guard
      }
    )
  )

This is the model definition

(module k-token GOVERNANCE

  @doc "K token smart contract"

  @model
    [ (defproperty conserves-mass (amount:decimal)
        (= (column-delta token-table 'balance) 0.0))

      (defproperty valid-account-id (accountId:string)
        (and
          (>= (length accountId) 3)
          (<= (length accountId) 256)))
    ]

score 1 · Answer 1 · answered Nov 19 '22 at 13:36

Properties and models are not used on-chain... They are just only for formal verification.

Your create-account should call a function to verify the account string. You can look at the coin module and its function (validate-account)as an example.

Kudos to Pascal3125 on Kadena discord channel.

Kadena Pact Property Check

1 Answers1