从板到可审计代码

板上的规则不是给模型看的提示词，而是一段可判定的声明式程序。既然是程序，就能编译：同一套规则，可以确定性地编译成一条可读的函数管线，或一串 SQL 视图——并附带一个证明：编译产物算出的结论，与板推导出的结论完全一致。

为什么编得动

规则之间互相读取对方的结论，构成一张依赖图。编译的调度就是这张图的拓扑排序：第几层算什么，由结构完全决定——没有搜索、没有启发式、没有猜，所以确定、可复现。

这件事成立的根本原因，是板故意停在可判定片段：规则只做关系连接、缺席检查（"没有某条材料"）与比较守卫，没有通用循环。加一个 while，表达力上去了，保真就没了——所以不加。这是立场，不是欠账。

同一套规则，两个目标

以一个订单处理规则包为例，六条规则：订单有没有对应客户、金额是否为正、无瑕疵即有效、有效且金额达标可加急。编译到 SQL 后，每个推导层是一张视图。下面是其中两层，由编译器真实生成，不是手写：

-- ── layer 2: invalid_order ──
CREATE VIEW "invalid_order" ("id", "reason") AS
  -- rule AX_BAD_CUSTOMER
  SELECT t0."id" AS "id", 'missing_customer' AS "reason"
  FROM "order" AS t0
  WHERE NOT EXISTS (SELECT 1 FROM "has_customer" AS n0 WHERE n0."order" = t0."id")
  UNION
  -- rule AX_BAD_AMOUNT
  SELECT t0."id" AS "id", 'nonpositive_amount' AS "reason"
  FROM "order" AS t0
  WHERE (t0."amount" <= 0);

-- ── layer 5: eligible_for_express ──
CREATE VIEW "eligible_for_express" ("id") AS
  -- rule AX_EXPRESS
  SELECT t0."id" AS "id"
  FROM "valid_order" AS t0,
       "order" AS t1
  WHERE t1."id" = t0."id"
    AND (t1."amount" >= 200);

对应关系一目了然："没有对应客户"编译成 NOT EXISTS，比较条件编译成 WHERE，同一个结论有两条规则来源就 UNION。另一个后端把每层编译成一个纯函数、依赖即输入，适合直接嵌进服务代码。两个后端读的是同一套规则、同一个分层、同一条片段边界。

保真证：两边必须算出同一批结论

能生成代码不稀奇，稀奇的是敢证明生成得对。每次编译配一条保真验证：同一批材料，一边走板的推导，一边真实执行编译产物，断言两边得到的结论集逐条相等。SQL 一侧不是"看形状像不像"——是在真实数据库引擎里建表、插入材料、跑视图、查结果，一行对一行比对。

上面的规则包配三张订单（一张合规、一张客户缺失、一张零元），板、函数管线、SQL 三路各自推出同样的 8 条结论——谁有效、谁作废、作废原因、谁可加急——两两相等。在此之上还有一致性加压：手选与合成的规则程序、再加 30 个随机生成的规则程序，三路全部零分歧。

诚实边界

编译覆盖的是可判定的推导主干：关系连接、缺席检查、比较守卫，以及精确聚合（求和/计数/最值，含分组与过滤）。以下构造被刻意拒绝——拒绝时明确报错，绝不输出一段"看起来对"的代码：

• 通用循环：终止性没有保证的程序，谈不上可审计。分支已由带守卫的规则与缺席检查覆盖，有界汇总已由聚合覆盖——拒绝通用循环不是能力缺口，是整个保真主张的前提；
• 求平均：要经过浮点除法，两侧可能出现看不见的分歧——宁可明确拒绝，并提示改用"总和＋个数"两条精确聚合替代；
• 递归规则、动作层（消耗/生产的状态变化）与产出新数值的算术规则：超出当前已证明的片段，一律明确拒绝，不做一半。

与"让模型直接写 SQL"的差别

让模型直接生成 SQL，没有任何正确性保证：生成的查询是否实现了意图，无从证明——而且错的时候看起来也很对。这里的次序不同：模型提出规则，板推导并认证，编译器把被认证的逻辑投影成代码，再用真实执行的保真验证钉住"投影没有失真"。每一步的信任来源都摆在明处。

对团队，这意味着：制度先在板上被裁决、被验证，然后变成一份可以 review、diff、进版本库、跑在真实数据库上的交付物。

现况

双后端编译、保真验证与三方一致性测试在核心引擎中已实现、自测全绿——本页的 SQL 与"8 条结论三路一致"即自测产物，非手写示意。作为云端能力尚未开放：今天云端开放的是板本身的推导与核对，见信任层与现况页。