pact-lang - 正式验证因 Pact 而变慢？

Question

我打算在我的智能合约中实现这段代码：

(defun absBug:integer (num:integer)
 ;; This property fails
 @model [(property (>= result 0))]
 (if (= (- (* (- num 6) (+ num 11)) (* 42 num)) (* (* 64 7) 52270780833))
     (- 1)
     (abs num)
 )

我想知道，由于我正在实施形式验证，一旦我将此合约部署到任何链上，是否会有任何延迟或减速？还是计算完成一次并存储起来？

（我知道我的代码会吐出正确的答案，事后我必须调整）

标签： pact-lang

Answer 1

不，它不会影响延迟或链上的任何其他性能。

形式验证的目的是证明合约是无缺陷且可部署的，因此它是在部署之前运行而不是在链上运行。

仅供参考，当您在pact-web上开发时，它默认运行形式验证。但是，如果您在您的机器上本地开发合约，您需要运行 (verify 'contract-name) 来运行形式验证，这是所有计算发生的时候。