BLOGE
0.9.8-RC1在线版 · 事实校验 2026-09-15 · English
第 28 章 —— 有限属性验证与有用反例
本章承诺： 探索声明过的有限贷款风险域，分清 sample failure、relation counterexample 和 value-shrink，重放 BLOGE 的确定性收缩轨迹，并判断更小反例何时仍需业务评审。
学习目标
- 定义附着在既有 Case 与 Expectations 上的 bounded generator。
- 区分失败 sample、relation counterexample 与 value-shrink 结果。
- 把预算耗尽和 shrink 不完整读成非通过结果。
- 让 Oracle 保持足够独立，真正能挑战 candidate。
五个 sample 比一个例子回答得多，却仍不是证明
贷款团队已经信任三个命名 Case，但担心 risk-score 边界。他们保留 auto-approve 作为锚点，只把 given.context.riskScore 替换为五个声明值。
schemaVersion: 1
propertySetId: loan-risk-boundaries
scenario: loan-approval.scenario.yaml
rootSeed: 11
sampleBudget: 5
generator:
generatorId: risk-scores
requirementRef: LOAN-DECISION-001
caseId: auto-approve
contextKey: riskScore
integerRange: {minimum: 10, maximum: 90, step: 20}
expectationIds: [decision-valid, risk-score-recorded]
relations:
- relationId: risk-never-decreases
kind: NON_DECREASING
actual: {kind: BUSINESS_OUTPUT, outputId: computedRiskScore}
VerificationPropertyReport property = verifier.verifyProperties(propertyPath);
每个 sample 仍执行锚点 Case 的全部非诊断 Expectation。rootSeed 让受支持的样本选择和顺序可重复，但不控制客户 Operator 内的时钟、随机数、网络状态或环境读取。结论只能覆盖五个声明点，不能写成“全部整数风险分”。
三种失败回答三个不同问题
| Evidence object | 失败对象 | 如何变小 |
|---|---|---|
| sample | 一个生成输入下的普通业务 Expectations | value shrink 可重跑 候选 |
| relation counterexample | 已执行 samples 之间的 relation | 选择更小的 sample ID 子集 |
| property report | 任一必要 sample、relation 或 shrink protocol | 聚合 status 和稳定 reason codes |
relation 的 shrinkTrace 不会发明输入。monotonicity 失败可以把执行集合缩到第一对能证明倒置的 sample。value shrink 不同：它在一个无 relation 的 sample 已失败后执行新的候选。
重放真实整数 shrink
对 maximumAttempts: 64 的无 relation 整数 plan，RC1 测试 deterministicallyShrinksAnIntegerFailureByReexecutingCandidates 连续两次观察到完全相同的序列：
1,000,000 → 0 → 1 → 2 → 4 → 8 → 16 → 32 → 64 → 128
第一个值是原始失败 sample。候选从零开始，再尝试同号二次幂。只有复现原始有序 reason codes 的候选才算有效。测试重跑整段实验，同时比较观察顺序和候选 context digest；两轮完全一致。
最后接纳的候选并不是“数学意义上最小的坏贷款”，只是当前候选顺序与失败等价规则产生的 minimal witness。
缩小 counterexample 不等于升级 Oracle
假设 [10, 30, 50, 70, 90] 得到 [10, 30, 80, 70, 90]。每个 sample 都可能通过本地 shape 检查，但 NON_DECREASING 会因 80 → 70 反向而失败。relation counterexample 可以只留下这两个 sample ID。
这对 sample 是诊断资产，不会自动成为新的 Golden Case。业务 Owner 仍要判断 relation 是否正确、生成 context 是否合规，以及约简输入是否值得获得一个批准过的 expected answer。
Shrink 可能结束却没有可用最小值
- 原始 sample 通过时，BLOGE 不尝试 shrink。
- 尝试预算耗尽且仍有候选时，结果是
INCOMPLETE / RESOURCE_LIMIT_EXCEEDED。 - 没有候选复现原始有序 reason codes 时，结果是
INCOMPLETE / PROPERTY_SHRINK_INCOMPLETE。 - 候选因另一原因失败时，它不是同一 bug 的 evidence。
这些结果都不能改写为业务 PASS。“诊断没有完成”和“已经验证正确”方向相反。
让裁判留在 candidate 之外
verifyOracleIndependence(Path) 分别报告三个可检查事实：
CONTENT_BOUND：批准 Oracle 的字节匹配 catalog digest。OWNER_SEPARATED：catalog 的 owner 标签不同；这是声明，不是身份认证。REFERENCE_MODEL：绑定实现可在 child JVM 中运行，并检查其内容闭包与 candidate runtime、Operator 字节的关系。
evidence reader 只可重跑该 reference model，不运行 candidate Operators 或客户 bootstrap。字节不相交识别不了复制过的决策逻辑，所以概念独立性和 owner 身份仍是外部治理问题。
实验：把一次倒置变成评审卡
- 运行五分值 plan，保存 sample IDs、outputs、root seed 和 receipt。
- 只引入一处阈值倒置，保持其他输入固定。
- 记录失败 relation 及其最小 sample-ID 子集。
- 用独立的无 relation plan 触发 value shrink，不要混用两种机制。
- 把完整候选顺序复制到评审卡。
- 请业务 Owner 判断约简 witness 是否合法、有意义、值得进入 governed Case。
- 恢复实现，确认 property 与原 Case 都重新通过。
现实迁移：缩小物流事件顺序错误
在物流追踪中，对有限事件序列声明 deliveredAt >= shippedAt。一旦某个序列违反
关系，就在保留原 seed 和候选顺序的前提下，把它缩成最小可重放事件对。缩短后的
轨迹只帮助诊断；它是否是合法、值得治理的 Case，仍由物流业务负责人判断。
本章边界
- Bounded property verification 只覆盖声明的有限 plan，不代表无限域或统计置信度。
- Relation reduction 在已执行 samples 中选择；value shrink 会创建并重跑候选。
- 确定性 shrink 只表示搜索顺序可复现，不表示全局最小业务输入。
- Oracle 字节隔离是有用 evidence，不证明人员独立或概念原创。
实验验收卡
- 预期与观察： 有限域找到反例并把整数失败缩小到可评审候选。
- 失败与恢复： 把 Oracle 放进 candidate 或让 shrink 停滞；恢复外部裁判和停止 reason。
- 证明边界： 证明给定生成器与边界内性质，不是全域证明。
- 练习合同： 一个性质和有限域；只改边界；交付 seed、反例、shrink 轨迹；候选稳定可重放即停止。
小结
Property verification 把一个命名 Case 扩成受控有限实验。counterexample 找到小而明确的已观察关系失败，value shrink 重跑候选并留下更小的可复现 witness。下一章会检查：文件、receipt、source 或 runtime context 改变后，这些结果还剩多 少信任。
下一章：第 29 章——从报告到 Source-bound Evidence
Coding Agent: Open the versioned task guide.