④ 三后端生成器（generator/）

生成器把 .ris + .dspec + .bind 变成可编译的 C。三个后端共享 common.py 的 lowering 基础设施，各自实现发射策略：

4.1 绑定层：.bind 把语义映射到后端

artifacts/output/portable-gpio-pl061/gpio-pl061.bind 三段式设计 —— 一个文件描述三个后端：

backend harness for device gpio-pl061 {
  type DeviceState -> "struct gpio_pl061"
  type MmioBase -> "uintptr_t"
  map dev.base -> "dev->base"
  map MmioRead(B4) -> "harness_read32"     -- MMIO 访问映射到仿真器
  map MmioWrite(B4) -> "harness_write32"
}

backend baremetal for device gpio-pl061 {
  export read_config as "gpio-pl061_read_config"   -- 导出为独立符号
  map MmioRead(B1) -> "mmio_read8"                -- 宽度分派
  map MmioRead(B2) -> "mmio_read16"
  map MmioRead(B4) -> "mmio_read32"
}

backend linux for device gpio-pl061 {
  include <linux/io.h>
  include <linux/platform_device.h>
  type MmioBase -> "void __iomem *"
  type LogicalIRQ -> "struct irq_data *"
  callback gpio_chip.get_direction = pl061_get_direction   -- 回调表槽位 → 函数
  callback irq_chip.irq_set_type = pl061_irq_type
  callback amba_driver.probe = pl061_probe
  map MmioRead(B4) -> "readl"                   -- 内核访问器
  map MmioWrite(B4) -> "writel"
}

同一份 DeviceSpec，三个后端各取所需：harness 只关心 MMIO 映射；baremetal 导出函数符号；linux 填 callback 表并选择内核访问器 —— 语义（做什么）与绑定（怎么做）彻底分离。

4.2 生成契约与 lowering receipt（核心机制）

生成 C 里每个 Read/Write/RMW 都必须携带 op_id + canonical digest：

• 契约来源：generation-contract.json（extractor 产出）逐操作列出 op_id、claim scope、readiness —— 是确定性后端和 LLM 共同遵守的「操作清单」。
• receipt 形态（C17）：公共 harness/baremetal lowering 为每个访问发射 __rh_op_<op_id> LabelStmt + direct CompoundStmt，libclang oracle 逐标签核对。
• exactly-once 校验：独立 oracle 拒绝 missing、duplicate、unknown、rejected、kind mismatch、digest drift —— 证明「RIS 里的每个访问在生成代码里恰好出现一次」。C16 起该 verifier 强制接入 LLM 初次生成与每轮修复；候选只有通过 frozen contract 才会原子替换当前 C。
• RMW 区分：contract 区分 write_from_read（数据流合成的 RMW，读来自前置 Read，lowering 不再重复读硬件）与 intrinsic_rmw（update-bits 风格，自身拥有一次读+写）—— 修复了旧生成器重复读硬件的 bug（common.py: lowering_recipes 的 docstring 明说）。

4.3 共享 lowering（common.py，856 行）

• expr_to_c（来自 formal.py）：Expr 代数 → C 表达式文本，含常量折叠后的输出。
• value_var_names / _vars_in_expr：收集值/守卫/Computed 地址里引用的标识符 —— 生成器据此推断需要声明哪些局部变量。
• transaction_local_decls：为事务 op 声明 opaque handle（void *）与 buffer/标量局部 —— 源事务 handle 刻意不透明，后端 ABI 持有 transport 模型。
• _called_names_in_text：识别文本里的函数调用（含 read_poll_timeout 这类把访问器当参数传的宏），避免把函数名误当标量变量。

4.4 harness 后端（harness.py + 真实产物）

生成的 userspace harness（generated/harness.c 节选）：

/* Auto-generated userspace harness for gpio-pl061 (reharness) */
#include <stdint.h>
#include <stdio.h>
#define readl(a) harness_read32((uintptr_t)(a))     -- 内核访问器 → 仿真器
#define readb(a) ((uint8_t)harness_read32((uintptr_t)(a)))
#define writel(v, a) harness_write32((uint32_t)(v), (uintptr_t)(a))
#define mdelay(n) (0)                               -- 内核 API 桩

#define MMIO_SIZE 0x1000
static uint32_t mmio_region[MMIO_SIZE / 4];         -- 4KB 仿真内存
static unsigned long trace_count = 0;

static inline uint32_t harness_read32(uintptr_t a) {
    uint32_t v = mmio_region[(a & 0xfff) / 4];
    printf("[trace %lu] R 0x%03lx = 0x%08x\n", trace_count++, (a & 0xfff), v);
    return v;
}
static inline void harness_write32(uint32_t v, uintptr_t a) {
    printf("[trace %lu] W 0x%03lx = 0x%08x\n", trace_count++, (a & 0xfff), v);
    mmio_region[(a & 0xfff) / 4] = v;
}
#define GPIODIR 0x400                               -- 寄存器偏移常量
#define GPIOIS  0x404

设计要点：trace 即产物 —— harness 的每次 MMIO 访问都打印 [trace N] R/W addr = value，这就是 runtime trace 的来源，直接与 trace_protocol.py 的比对逻辑对接（原驱动 trace vs 候选 trace 逐事件 diff）。

4.5 bare-metal 后端

最小抽象层：mmio_read8/16/32、mmio_write8/16/32 由平台实现；export 把每个 FunctionSpec 导出为独立符号（gpio-pl061_probe 等），供裸机测试框架直接调用 —— 没有内核 API、没有回调表。

4.6 Linux 内核后端（linux.py，2,925 行）

最复杂的后端，职责分层：

• Kbuild 上下文：生成 Makefile + module_init/module_exit + 精确对象路径，用真实 .o.cmd 上下文编译（19/19 里 Linux 18/19，唯一失败的 sdhci-esdhc-mcf 因 Coldfire 平台宏 ESDHC_DEFAULT_QUIRKS 未编译，保留明确日志）。
• 回调注册：把 .bind 的 callback 映射填进真实结构体 —— GPIO 动态 gpio_irq_chip.init_hw 绑定按字段语义归类；clock provider 保留多套 clk_ops；Sodaville PCI ID + 12-line GPIO 行为 + mask/unmask/EOI lifecycle 由版本化源码保守恢复。
• registration identity attestation（C20）：对生成代码做独立 required-subset leaf AST 与 registration AST oracle —— 依据实际 generated-C artifact SHA、Kbuild .o.cmd、操作集合、callback/function USR、typed field、registration call 与 module-init root 重建「有效身份链」。
• 分域建模：SDHCI accessor/ops table、virtio config/virtqueue 分域记录；GPIO gpio_generic_chip_config 合成；subsystem_runner.py（434 行）承载子系统级运行器（如 gpiolib exerciser）。

4.7 LLM 合成：可选的第二路径

LLM 不是确定性测试/矩阵/QEMU 结果的依赖，但闭环实验里它是候选生成器：

• synthesis.py（249 行）：把 bundle（RIS + dspec + bind + facts）组包喂给外部模型，解析候选 C。
• tools/pi/：Pi coding-agent 作为 synthesizer，通过 REHARNESS_LLM_CMD 接入（本地 Node 依赖）。
• experiment_runner.py 的 PiBridge adapter：提取 → 合成 → 编译 → 契约校验 → 运行 → trace 比对，任何失败以结构化 Feedback 回送，迭代修复；候选只有通过 frozen contract 才原子替换。