如何在形式化验证模型中为conserves-mass属性排除创世铸造函数？

需求说明 #

我需要在形式化验证模型中，把创世铸造相关的函数（比如示例里的transfer-create）排除在conserves-mass属性的校验范围之外。

现有代码示例 #

(module account GOVERNANCE 
@doc "Account doc"  
@model
[ (defproperty conserves-mass
    (= (column-delta ledger 'balance ) 0.0))]
...
(defun transfer-create:string
    ( sender:string
      receiver:string
      receiver-guard:guard
      amount:decimal )
@doc "create account when transfer doc"
@model [ (property conserves-mass)] <- 我想在这里排除铸造相关逻辑

...

参考示例困惑 #

我看到过一段使用except逻辑的代码，但无法理解其工作机制，也没能成功实现，且官方文档中无相关说明：

@model
[
...
 ; every function should conserve mass except for the admin fund-account,
 ; and debit / credit which should be private
 (property conserves-mass
   {'except: [fund-account, debit, credit]})
...
]

解决方案 #

正确的实现方式是在模块级的@model定义中使用except参数，而非在函数级@model中添加属性，具体操作如下：

修改模块级的defproperty定义，将需要排除的创世铸造函数（如transfer-create）加入except列表：

(module account GOVERNANCE 
@doc "Account doc"  
@model
[ (defproperty conserves-mass
    (= (column-delta ledger 'balance ) 0.0)
    {'except: [transfer-create]})] ; 在此添加需排除的函数名
...
(defun transfer-create:string
    ( sender:string
      receiver:string
      receiver-guard:guard
      amount:decimal )
@doc "create account when transfer doc"
@model [] ; 移除此处的conserves-mass属性，或留空即可

...

逻辑说明 #

• 模块级的defproperty默认会对所有带@model注解的函数生效
• {'except: [函数名列表]}参数用于指定无需应用该属性校验的函数
• 如果在函数级@model中手动添加(property conserves-mass)，会覆盖模块级的排除规则，因此必须移除函数级的该属性

内容的提问来源于stack exchange，提问作者slaanesh