Формальная проверка замедлилась с Пактом?

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)
 )

Мне было интересно, так как я внедряю формальную проверку, будут ли задержки или замедление, когда я разверну этот контракт в какой-либо цепочке? Или расчет выполняется один раз и сохраняется в будущем?

(я знаю, что мой код выдает правильный ответ, который я должен был бы изменить после факта)

Answer 1

Нет, это не влияет на задержку или любую другую производительность в цепочке.

Цель формальной проверки - доказать, что контракт не содержит ошибок и может быть развернут, следовательно, он запускается до развертывания, а нев цепочке.

К вашему сведению, когда вы разрабатываете на pact-web , по умолчанию выполняется формальная проверка.Однако, если вы локально разрабатываете контракт на своем компьютере, вам нужно будет запустить (проверить 'имя-контракта), чтобы запустить формальную проверку, и тогда все вычисления будут выполнены.