用 SMT 求解纯目标

EN | 中文

上一节结束时，纯化交出的是普通逻辑目标：reversereverse 循环头部的列表等式 l = REVERSE [] ++ ll = REVERSE [] ++ l，以及——完成数组示例之后——clearclear 中的索引边界与 replace_inthreplace_inth 等式。等式、整数运算，以及关于它们的量化事实，正是 SMT 求解器擅长处理的内容。本节把 C* 的证明层连接到 Z3，用 SMT_TACSMT_TAC 解决这些目标，并组装出完整的三步流水线——此后两个示例的程序点上，除调用流水线之外不再有任何证明步骤。

配置 Z3

SMT 用户库通过 Z3 的 C API 调用求解器，因此需要安装带 C 头文件与链接库的 Z3；安装方式因平台而异。安装后，在仓库根目录的 cstar.tomlcstar.toml 中将构建系统指向它：


cflags = "-I/path/to/z3/include"
link_flags = "-L/path/to/z3/lib -lz3"


cflags = "-I/path/to/z3/include"
link_flags = "-L/path/to/z3/lib -lz3"

/path/to/z3/path/to/z3 是机器上实际路径的占位符；当 Z3 位于编译器的默认搜索路径中时，只需 link_flags = "-lz3"link_flags = "-lz3"（cstar_examplescstar_examples 仓库默认即如此配置）。检查环境最快的方式，是验证最终完成的示例：


cstarc verify strategy_demo/examples/reverse.c
cstarc verify strategy_demo/examples/clear.c


cstarc verify strategy_demo/examples/reverse.c
cstarc verify strategy_demo/examples/clear.c

`SMT_TACSMT_TAC`


PROOF gnode SMT_TAC(gnode gn);


PROOF gnode SMT_TAC(gnode gn);

SMT_TACSMT_TAC 把当前的普通 HOL 目标交给已初始化的 SMT 用户库。如果 Z3 判定目标有效，它就求解当前 gnodegnode；如果翻译失败、求解器无法判定，或目标本身无效，则目标保持开放，供用户继续处理。

PURIFY_TACPURIFY_TAC、POST_PURIFY_TACPOST_PURIFY_TAC 与 SMT_TACSMT_TAC 全部就位后，本部分的流水线便归并为一个可复用函数：


PROOF thm solve_vc_auto(term vc) {
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  SMT_TAC(g);
  return gnode_prove(root);
}


PROOF thm solve_vc_auto(term vc) {
  gnode root = gnode_new_with_ccl(vc);
  gnode g = PURIFY_TAC(root);
  g = POST_PURIFY_TAC(g);
  SMT_TAC(g);
  return gnode_prove(root);
}

在每一个需要重建不变式或后置条件状态的程序点上，模式都相同：读取符号状态、构造蕴含、提交证明得到的定理：


PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}


PROOF {
  term st = cst_get_symbolic_state();
  term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}

完成版的 strategy_demo/examples/reverse.cstrategy_demo/examples/reverse.c——与 reverse_clean.creverse_clean.c 相同的函数，但删去了那条巨大断言——在三个位置调用它：循环前建立不变式、循环体末尾重建不变式，以及循环之后把状态转换为 returnreturn 所需的形状：


PROOF {
  term st = cst_get_symbolic_state();
  term return_ready = `exists t_v v_v w_v.
    data_at p__addr Tptr p__pre **
    data_at w__addr Tptr w_v **
    data_at v__addr Tptr v_v **
    data_at t__addr Tptr t_v **
    sll w_v (REVERSE l)
  `;
  term vc = `${st:hprop} |-- ${return_ready:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}


PROOF {
  term st = cst_get_symbolic_state();
  term return_ready = `exists t_v v_v w_v.
    data_at p__addr Tptr p__pre **
    data_at w__addr Tptr w_v **
    data_at v__addr Tptr v_v **
    data_at t__addr Tptr t_v **
    sll w_v (REVERSE l)
  `;
  term vc = `${st:hprop} |-- ${return_ready:hprop}`;
  cst_set_symbolic_state(solve_vc_auto(vc));
}

一如既往，状态从不被直接修改：solve_vc_autosolve_vc_auto 返回一条蕴含定理，cst_set_symbolic_statecst_set_symbolic_state 将其提交。

告诉求解器必要的列表知识

SMT 求解器擅长等式、整数运算和量词——但对 REVERSEREVERSE 的 HOL 定义和 REVERSE_REVERSEREVERSE_REVERSE 定理，Z3 并不具备内建知识。 smt_add_axiomsmt_add_axiom 把这些已经证明的定理作为背景知识提供给后续 SMT 调用；reverse.creverse.c 在加载时一次性安装它们：


PROOF static int install_smt(void) {
  smt_init();
  smt_register_seq_handler();
  type_pair_list int_inst = (type_pair_list)vector_create();
  vector_add(&int_inst, ((type_pair){`:int`, `:A`}));
  thm reverse_def_int = gen_all_rule(
    inst_type_rule(int_inst, get_REVERSE()));
  thm reverse_reverse_int = gen_all_rule(inst_type_rule(
    int_inst, get_theorem_by_name("REVERSE_REVERSE")));
  smt_add_axiom(reverse_def_int);
  smt_add_axiom(reverse_reverse_int);
  return 0;
}
PROOF static int _install_smt = install_smt();


PROOF static int install_smt(void) {
  smt_init();
  smt_register_seq_handler();
  type_pair_list int_inst = (type_pair_list)vector_create();
  vector_add(&int_inst, ((type_pair){`:int`, `:A`}));
  thm reverse_def_int = gen_all_rule(
    inst_type_rule(int_inst, get_REVERSE()));
  thm reverse_reverse_int = gen_all_rule(inst_type_rule(
    int_inst, get_theorem_by_name("REVERSE_REVERSE")));
  smt_add_axiom(reverse_def_int);
  smt_add_axiom(reverse_reverse_int);
  return 0;
}
PROOF static int _install_smt = install_smt();

核心调用是 smt_add_axiomsmt_add_axiom：其参数是一条定理，定理的结论将成为求解器可用的背景知识。定理的假设会先被卸除，但自由项变量不会被全称化——因此需要显式调用 gen_all_rulegen_all_rule。此外还需要一个技术步骤：单态化（monomorphization）。 HOL 列表定理在元素类型 AA 上是多态的，而当前翻译不支持 HOL 多态；inst_type_ruleinst_type_rule 先把 AA 固定为此处实际使用的 intint，再把定理交给求解器。

`term_to_z3term_to_z3` 内部

SMT_TACSMT_TAC 位于 userlib/smt/smt.cuserlib/smt/smt.c，其核心并不神秘：递归查看 HOL 项的形状，构建语义上对应的 Z3 AST。 term_to_z3term_to_z3 的主体可以概括为：


Z3_ast term_to_z3(Z3_context ctx, term tm) {
  if (is_int(tm))
    return Z3_mk_int(ctx, dest_int(tm), Z3_mk_int_sort(ctx));
  if (is_forall(tm)) {
    /* 翻译绑定变量的类型，递归进入主体，构建 Z3 forall */
  }
  if (is_exists(tm)) {
    /* 类似地，构建 Z3 exists */
  }
  if (is_var(tm)) {
    /* 自由变量变为同名、同类型的 Z3 常量 */
  }
  if (is_const(tm) || is_comb(tm))
    return smt_app_to_z3(ctx, tm);
  return NULL;
}


Z3_ast term_to_z3(Z3_context ctx, term tm) {
  if (is_int(tm))
    return Z3_mk_int(ctx, dest_int(tm), Z3_mk_int_sort(ctx));
  if (is_forall(tm)) {
    /* 翻译绑定变量的类型，递归进入主体，构建 Z3 forall */
  }
  if (is_exists(tm)) {
    /* 类似地，构建 Z3 exists */
  }
  if (is_var(tm)) {
    /* 自由变量变为同名、同类型的 Z3 常量 */
  }
  if (is_const(tm) || is_comb(tm))
    return smt_app_to_z3(ctx, tm);
  return NULL;
}

应用（application）按头部常量分发：==>==> 变为 Z3_mk_impliesZ3_mk_implies，/\/\ 变为 Z3_mk_andZ3_mk_and，整数 ++、--、**、<<、<=<= 映射到相应的 Z3 运算。类型可翻译的其他函数则作为未解释函数（uninterpreted function）处理；smt_add_axiomsmt_add_axiom 添加的定理用来约束它们的行为。由 smt_register_seq_handlersmt_register_seq_handler 注册的处理器还会把列表词汇映射到 Z3 的序列理论——NILNIL 映射为空序列、CONSCONS 与 APPENDAPPEND 映射为序列拼接、inthinth 映射为序列索引、类型 (A)list(A)list 映射为序列类型——因此列表目标不至于完全停留在未解释状态。

最后，求解器断言背景知识与目标的否定。如果 Z3 报告不可满足（unsatisfiable），则反模型（countermodel）不存在，目标有效，SMT_TACSMT_TAC 据此求解该 gnodegnode。

完成 `clearclear`

数组示例 strategy_demo/examples/clear.cstrategy_demo/examples/clear.c 把 00 写入数组的每一个元素。上一节的策略已经覆盖其空间推理；仍然开放的是纯推理的剩余部分，其内容围绕 replace_inthreplace_inth——上一节 int_array_with_holeint_array_with_hole 的规则引入逻辑列表中的函数。 strategy_demo/array/lemmas.cstrategy_demo/array/lemmas.c 中证明的三条引理，准确刻画了一次更新对读取和长度的影响：


|- forall i v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     inth i (replace_inth i v l) = v
|- forall i j v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     0i <= j ==> j < ilength l ==> ~(j = i) ==>
     inth j (replace_inth i v l) = inth j l
|- forall i v:int. forall l:(int)list.
     ilength (replace_inth i v l) = ilength l


|- forall i v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     inth i (replace_inth i v l) = v
|- forall i j v:int. forall l:(int)list.
     0i <= i ==> i < ilength l ==>
     0i <= j ==> j < ilength l ==> ~(j = i) ==>
     inth j (replace_inth i v l) = inth j l
|- forall i v:int. forall l:(int)list.
     ilength (replace_inth i v l) = ilength l

clear.cclear.c 安装数组策略、把这三条引理注册为 SMT 背景知识，然后仅靠循环体末尾的一个证明块完成验证：


PROOF static int _strategy_demo_array = install_strategy_demo_array();
PROOF static int install_clear_smt_axioms(void) {
  smt_add_axiom(replace_inth_at());
  smt_add_axiom(replace_inth_other());
  smt_add_axiom(replace_inth_length());
  return 0;
}
PROOF static int _clear_smt_axioms = install_clear_smt_axioms();
void clear(int *to, int len)
  [[cst::require(`exists l.
    fact(0i <= len && len <= 100i) **
    fact(ilength l == len) **
    int_array to 0i len l
  `)]]
  [[cst::ensure(`exists l.
    fact(forall i. 0i <= i && i < len ==> inth i l = 0i) **
    int_array to 0i len l
  `)]]
{
  int i = 0;
  PROOF term loop_inv = `exists i_v l.
    fact(0i <= i_v && i_v <= len__pre &&
         0i <= len__pre && len__pre <= 100i && ilength l == len__pre) **
    fact(forall j. 0i <= j && j < i_v ==> inth j l = 0i) **
    data_at to__addr Tptr to__pre **
    data_at len__addr Tint len__pre **
    data_at i__addr Tint i_v **
    int_array to__pre 0i len__pre l
  `;
  while (i < len)
    [[cst::invariant(loop_inv)]]
  {
    to[i] = 0;
    i = i + 1;
    PROOF {
      term st = cst_get_symbolic_state();
      term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
      cst_set_symbolic_state(solve_vc_auto(vc));
    }
  }
}


PROOF static int _strategy_demo_array = install_strategy_demo_array();
PROOF static int install_clear_smt_axioms(void) {
  smt_add_axiom(replace_inth_at());
  smt_add_axiom(replace_inth_other());
  smt_add_axiom(replace_inth_length());
  return 0;
}
PROOF static int _clear_smt_axioms = install_clear_smt_axioms();
void clear(int *to, int len)
  [[cst::require(`exists l.
    fact(0i <= len && len <= 100i) **
    fact(ilength l == len) **
    int_array to 0i len l
  `)]]
  [[cst::ensure(`exists l.
    fact(forall i. 0i <= i && i < len ==> inth i l = 0i) **
    int_array to 0i len l
  `)]]
{
  int i = 0;
  PROOF term loop_inv = `exists i_v l.
    fact(0i <= i_v && i_v <= len__pre &&
         0i <= len__pre && len__pre <= 100i && ilength l == len__pre) **
    fact(forall j. 0i <= j && j < i_v ==> inth j l = 0i) **
    data_at to__addr Tptr to__pre **
    data_at len__addr Tint len__pre **
    data_at i__addr Tint i_v **
    int_array to__pre 0i len__pre l
  `;
  while (i < len)
    [[cst::invariant(loop_inv)]]
  {
    to[i] = 0;
    i = i + 1;
    PROOF {
      term st = cst_get_symbolic_state();
      term vc = `${st:hprop} |-- ${loop_inv:hprop}`;
      cst_set_symbolic_state(solve_vc_auto(vc));
    }
  }
}

一次循环体执行可按以下顺序解读：

符号执行准备执行 to[i] = 0to[i] = 0，需要目标单元的 data_atdata_at；
数组规则 00 从 int_arrayint_array 中切出该单元，留下 int_array_with_holeint_array_with_hole——它的两条 inferinfer 检查都能通过，因为不变式的事实给出了 0 <= i_v0 <= i_v 与 i_v < len__prei_v < len__pre；
写入执行，该单元的值变为 00；
重建不变式时，规则 11 把左侧的空穴与右侧的目标 int_arrayint_array 匹配，将目标改写为一个存在变量 vv、索引 ii 处的 data_atdata_at，以及等式 l2 = replace_inth (i - x) v l1l2 = replace_inth (i - x) v l1；
通用 data_atdata_at 策略把刚写入的单元与这个 data_atdata_at 消去，实例化 v = 0v = 0；
规则 22 适用于两侧直接出现同一区段 int_arrayint_array 的状态，消去空间谓词，留下列表等式；
POST_PURIFY_TACPOST_PURIFY_TAC 得到普通逻辑目标，SMT_TACSMT_TAC 再利用 replace_inthreplace_inth 引理证明已清零前缀扩大了一个单元，同时长度与边界事实保持不变。

循环入口和循环之后的后置条件完全不需要证明块：策略注册之后，引擎自行卸除了这些义务。

自动化的局限

小结

SMT_TACSMT_TAC 把普通 HOL 目标连同已注册的背景定理翻译到 Z3，断言目标的否定，并把不可满足性解读为有效性，从而解决目标；其裁决被直接信任，并受求解器超时限制。
smt_add_axiomsmt_add_axiom 把已证明的 HOL 定理转化为求解器的背景知识；多态的列表定理在提交给求解器之前，先用 inst_type_ruleinst_type_rule 单态化，并用 gen_all_rulegen_all_rule 全称化。
term_to_z3term_to_z3 递归地把项形状映射为 Z3 AST，按头部常量分发应用，可翻译但含义未知的函数保留为未解释函数；序列处理器把列表词汇映射到 Z3 的序列理论。
solve_vc_autosolve_vc_auto——纯化、后纯化、SMT——在 reversereverse 的三个程序点和 clearclear 的一个程序点上卸除了全部剩余义务；上一节的策略与本节的求解器构成了全部证明。
策略内部的 inferinfer 检查与 SMT_TACSMT_TAC 处于不同层次：前者在 QCP 内部决定局部的规则适用性，后者在 C* 证明层解决整个纯目标。