Notes
定理证明草稿：简单流水线不变量骨架
目标陈述（非形式）
两级流水线寄存器 v0, v1（valid）与数据 d0, d1。若某拍 v1 为真，则存在更早拍使对应数据从输入端进入且未被冲刷。
不变量候选
I1：¬v0 → 气泡规则允许的后继I2：v1 → d1曾在上游 valid 时被采样- 复位后首拍：
¬v0 ∧ ¬v1
证明草稿结构
- 复位情形：直接得
I1 ∧ I2。 - 归纳步：按 stall / flush / fire 分案。
- flush 案需证明 valid 被清零，旧数据不再声称有效。
theorem pipeline_invariant :
∀ s, reachable s → I1 s ∧ I2 s := by
intro s hr
-- induction on reachable; cases on fire/stall/flush
sorry下一步
- 把状态机写成可执行的小步语义。
- 先在模型检测里找反例，再搬进定理证明器，避免空证明。
- 相关论文卡片见
/papers（模型检测与定理证明分工）。