Formal Verification: Multiple tables with multiple input variables

[EnoF]

It seems like when I'm doing a formal verification of a function involving multiple tables with multiple input variables the verification times out. See the following test:

(load "root/fungible-v2.pact")
(load "root/fungible-xchain-v1.pact")
(load "root/coin-v5.pact")

(module test GOVERNANCE
 (defcap GOVERNANCE() true)

  (defschema stake-schema
    owner:string
    stake:decimal
    stakers:integer
    balance:decimal)
  (deftable stake-table:{stake-schema})

  (defschema stakers-schema
    stake:string
    staker:string
    amount:decimal)
  (deftable stakers-table:{stakers-schema})

 (use coin)

 (defun refund-staker(name:string staker:string)
    @model [
      (property (!= name ""))
      (property (!= staker ""))
      (property (= 0.0 (at 'balance (read stake-table name 'before))))
    ]

    (with-read stakers-table (get-stake-id name staker)
      { "amount" := amount }
      (with-read stake-table name
        { "stakers" := stakers
        , "owner"   := owner
        , "balance" := balance }
        (let ((refund-amount (/ balance stakers))
              (stake-escrow:string (get-stake-id name owner)))
          (update stake-table name
            { "stakers" : (- stakers 1)
            , "balance" : (- balance 1.0) })
          (coin.transfer stake-escrow staker 1.0)))))

  (defun get-stake-id(stake:string staker:string)
    (format "{}-{}" [staker stake]))
)

(verify 'test)

If I extract the id used for:

(with-read stakers-table (get-stake-id name staker)
; and
(stake-escrow:string (get-stake-id name owner))

It can perform the verification:

(load "root/fungible-v2.pact")
(load "root/fungible-xchain-v1.pact")
(load "root/coin-v5.pact")

(module test GOVERNANCE
 (defcap GOVERNANCE() true)

  (defschema stake-schema
    owner:string
    stake:decimal
    stakers:integer
    balance:decimal)
  (deftable stake-table:{stake-schema})

  (defschema stakers-schema
    stake:string
    staker:string
    amount:decimal)
  (deftable stakers-table:{stakers-schema})

 (use coin)

 (defun refund-staker(name:string staker:string staker-id:string stake-escrow:string)
    @model [
      (property (!= name ""))
      (property (!= staker ""))
      (property (= 0.0 (at 'balance (read stake-table name 'before))))
    ]

    (with-read stakers-table staker-id
      { "amount" := amount }
      (with-read stake-table name
        { "stakers" := stakers
        , "owner"   := owner
        , "balance" := balance }
        (let ((refund-amount (/ balance stakers)))
          (update stake-table name
            { "stakers" : (- stakers 1)
            , "balance" : (- balance 1.0) })
          (coin.transfer stake-escrow staker 1.0)))))

  (defun get-stake-id(stake:string staker:string)
    (format "{}-{}" [staker stake]))
)

(verify 'test)

It seems like it is calculating too many paths for this function to test?

[rsoeldner]

I'm not able to reproduce the timeout. Do you receive an SMT error?

Additionally, I looked at the contract and was not able to understand the property you want to verify.

The function properties are evaluated assuming the function succeeds., see here for the documentation.

Specifically, this means that you have to justify the properties you state. See below where the verification passed (ignoring the stated property is struggle to understand):

(load "fungible-v2.pact")
(load "fungible-xchain-v1.pact")
(load "coin-v5.pact")

(module test GOVERNANCE
 (defcap GOVERNANCE() true)

  (defschema stake-schema
    owner:string
    stake:decimal
    stakers:integer
    balance:decimal)
  (deftable stake-table:{stake-schema})

  (defschema stakers-schema
    stake:string
    staker:string
    amount:decimal)
  (deftable stakers-table:{stakers-schema})

 (use coin)

 (defun refund-staker(name:string staker:string)
    @model [
      (property (!= name ""))
      (property (!= staker ""))
      ;(property (= 0.0 (at 'balance (read stake-table name 'before))))
      ;                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ This one
    ]

    (enforce (!= name "") "not empty name")
    (enforce (!= staker "") "not empty staker")

    (with-read stakers-table (get-stake-id name staker)
      { "amount" := amount }
      (with-read stake-table name
        { "stakers" := stakers
        , "owner"   := owner
        , "balance" := balance }
        (let ((refund-amount (/ balance stakers))
              (stake-escrow:string (get-stake-id name owner)))
          (update stake-table name
            { "stakers" : (- stakers 1)
            , "balance" : (- balance 1.0) })
          (coin.transfer stake-escrow staker 1.0)))))

  (defun get-stake-id(stake:string staker:string)
    (format "{}-{}" [staker stake]))
)

(verify 'test)

Is the property you want to express: After the function refund-staker succeeded, the staker has a balance of 0?

[emilypi]

Verification timeout, as we've seen in the past, can be a consequence of Z3 lib version. Could you post which version you have on PATH?

[EnoF]

@emilypi My z3 verions was:

z3 --version
Z3 version 4.8.12 - 64 bit

@rsoeldner after reviewing my test I think I should have written this to express better what I wanted to verify:

(defun refund-staker(name:string staker:string staker-id:string stake-escrow:string)
    @model [
      (property (!= name ""))
      (property (!= staker ""))
      (property (when (row-exists stake-table name 'before) (= 0.0 (at 'balance (read stake-table name 'before)))))
    ]

The intention is to test that the amount staked by the staker is 0.0 if it exists. To ensure that every staker only stakes once on a stake. With that said, this still results in a SMT resolver timeout.

[EnoF]

If I add an invariant check on the table, it resolves within time (granted fails as expected, but resolves):

(defschema stake-schema
    @model [
      (invariant (>= balance 0.0))
    ]
    owner:string
    stake:decimal
    stakers:integer
    balance:decimal)
  (deftable stake-table:{stake-schema})

[rsoeldner]

@EnoF is this resolved?