⑤ 验证体系、实验编排与复现

reharness 的验证哲学：每个声明都有机器可查的证据。验证分三层 —— 单元 oracle（QA）、运行时比对（QEMU/trace）、编排门禁（experiment runner）。

5.1 实验编排：manifest → runner（src/experiment_*.py）

Manifest（experiment_manifest.py，555 行）

实验只能声明 manifest 里的设备/编译/测试/trace 事实 —— runner 不按驱动名或源码内容推断子系统（防过拟合）。manifest 由 10 个规格类组成：

SourceSpec        # 源码 + SHA
CompileSpec       # 编译命令/上下文
PciIdentity       # PCI ID（ahci/sodaville 等）
SafetyPolicy      # 运行时安全策略（probe 不触发 DMA 风暴等）
QemuPolicy        # QEMU 参数策略
RuntimeSpec       # 运行时适配器策略
TestSpec          # 测试用例
TraceSpec         # trace 规范化/掩码配置
IterationLimits   # LLM 修复轮数上限
ExperimentManifest# 聚合 + canonical digest（_parse_mask/_parse_pci_value 严格解析）

manifest_digest 对 manifest 做 canonical JSON 摘要 —— 实验可复现的锚点。

协议（experiment_protocol.py）

阶段记录与反馈的严格 schema：FailureClass（枚举失败类别）、StageRecord（每阶段产物/状态）、Feedback（回送给合成器的结构化错误）、TraceEvent / TraceDivergence、compare_traces。所有文档校验拒绝未知字段（_check_unknown）。

Runner（experiment_runner.py）

适配器协议定义六个阶段接口：

Extractor        # 提取证据（RIS/dspec/facts）
PiBridge         # LLM 合成候选（synthesis.py + tools/pi）
Compiler         # 编译候选
ContractVerifier # generation contract 校验（op_id + digest exactly-once）
RuntimeRunner    # 运行（QEMU / 原生）
TraceComparator  # trace 比对

ExperimentRunner.run 编排闭环：编译/运行/trace 失败 → 结构化 Feedback 回送 → _repair 迭代 → 只有通过 frozen contract 才原子替换候选（_verify_contract）。每轮状态持久化为 StageRecord，输出 evidence、候选代码、阶段记录与 trace。

5.2 trace 协议与比对（trace_protocol.py，460 行）

TraceEvent：事件模型（phase/op/addr/value/width…），from_dict/to_dict 严格校验。
normalize_trace：支持 value_mask（忽略易变值位，如 DMA 状态）与 address_mask（忽略地址低/高位）—— 由 manifest 的 TraceSpec 配置。
normalize_function_name：函数名规范化（manifest 级映射）。
first_divergence / compare_runs / compare_traces：逐事件比对，报告第一个发散点 + 上下文（context=3），输出 TraceComparison（reason 字段解释差异）。
parse_trace_text：解析 harness 打印的 [trace N] R/W addr = value 文本流 → TraceRun。

比对语义（cli.py 的 _is_subsequence 注释）：无条件的 RIS op 必须按序出现在运行时 trace 里，条件 op 可交错 —— 序列等价而非严格逐条相等。

5.3 QA oracle 家族（qa/verification/）

Oracle	验证什么
`generated_c_ast_oracle.py`	生成 C 的 AST 级 receipt 校验：悬空 receipt、错误 primitive kind/width/endianness/W1C、RMW ownership、未锚定额外 MMIO —— 全部拒绝
`linux_registration_ast_oracle.py`	Linux 生成代码的 required-subset leaf AST + registration AST（C20）
`backend_lowering_oracle.py / plan.py`	按 lowering plan 对账 authorized/blocked 操作（DWC2: 3182 lowered + 426 loop-blocked 等）
`clock_arithmetic_oracle.py`	clock 公式变异检测：Highbank 22 个算术 oracle 用例，三类公式 mutation 全检出
`ris_mutation_oracle.py`	对 RIS 做变异（删 op/改地址/改值），验证 trace oracle 能发现
`ris_trace_oracle.py`	RIS 序列 ↔ 运行时 trace 一致性
`ftgpio_trace_oracle.py`	gpio-ftgpio010 结构化 Formal RIS + 真实 gpiolib exerciser：6/6 模块、7/7 调用、13/13 ops、8/8 寄存器偏移
`c67x00_hpi_trace_oracle.py`	C67X00 HPI：32/32 computed address 安全 lowering；5 个 primitive、4 个 differential case、4 类 mutation
`dwapb_banked_oracle.py`	DW APB multi-bank 地址
`reliability_report.py`	机器可读 scoped RIS reliability 报告（C15: 5/19 strict）
`check_generalization_guard.py`	CI 门禁：zero-shot holdout 驱动的专用标识出现在 src/ → 失败（防 hardcode）
`run_zero_shot_holdout.py / run_matrix.py / run_multisource_matrix.py`	冻结矩阵运行器（结果进 research/experiments/results/*.json）

5.4 QEMU 运行时验证

edu：值级 oracle —— 合成驱动在 QEMU 里跑，寄存器读写值与原始行为逐一对账。
gpio-ftgpio010：结构化 Formal RIS + 精确函数边界 + 真实 gpiolib exerciser 的 probe/callback MMIO oracle。
qa/native-tests/（edu_trace_test / gpio_trace_test）：原生 trace 测试二进制；scripts/qemu/ + run_qemu_experiments.sh 编排整套可复现 QEMU 套件；结果 research/experiments/results/qemu.json。
initramfs/rootfs 由 artifacts/initramfs/ 提供，静态链接 libc/工具链 —— 完全可再生成（git 不追踪 binary）。

5.5 strict readiness：诚实性的总闸

whole_program_complete = linked analysis ∧ 调用语义 ∧ CFG ∧ 路径
                         ∧ 访问 ∧ 值 ∧ 循环 ∧ evidence 的严格 gate 合取

任何一项不满足 → strict = false。当前状态（README C19/C20）：

矩阵	Harness	Bare-metal	Linux
C19 冻结矩阵（strict）	4/19	4/19	0/19
后续进展（PLAN.md）	7/19	7/19	5/19
zero-shot v1（编译）	12/12
zero-shot v1（strict）	7/12	7/12	5/12（三后端共同 5/12）

值得注意：strict 数字远低于「编译通过」数字 —— 这是刻意的。编译通过只说明语法/类型对，strict 要求整程序语义证明。论文里这是核心论点：「能编译」≠「证明等价」。

5.6 复现流程（REPRO.md）

./run.sh test                                        # 205 项测试
python3 qa/verification/check_generalization_guard.py
python3 qa/verification/run_zero_shot_holdout.py
python3 qa/verification/run_matrix.py
python3 qa/verification/run_multisource_matrix.py
python3 qa/verification/run_clock_model_boundary.py
python3 qa/verification/c67x00_hpi_trace_oracle.py --output research/experiments/results/c67x00-hpi-oracle.json
python3 qa/verification/reliability_report.py --output research/experiments/results/reliability.json
./run.sh qemu-experiments
python3 tools/reporting/generate_paper_results.py      # 论文表格 ← JSON 自动生成
(cd research/paper && latexmk -pdf -interaction=nonstopmode -halt-on-error paper.tex)

权威结果全部落在 research/experiments/results/*.json，generated_results.tex 自动生成、不手改 —— 论文数字与代码状态单源同步。

5.7 反过拟合机制（零样本）

benchmarks/drivers/holdout/zero-shot-v1.json 冻结 12 个从未用于实现的驱动。
CI 的 generalization guard 检查：这些驱动的专用标识出现在 src/extractor/ 或 src/generator/ → 测试失败。
首个跨驱动 RIS blocker 是 5 个案例共有的 call_context；virtio-input 不伪装成 MMIO（config/virtqueue 建模为 subsystem state）。

教程完。六章走完：语言 → 提取 → 语义 → 生成 → 验证。想深入任一部分，docs/ 下的架构文档（c24–c27：transaction IR / regmap / i2c / mfd lowering）和里程碑（c10–c23）是最佳下一站。