msgexchange-v2/docs/invariants.md

前提、不变量与声明边界

本文件是三件东西的唯一出处：

• 前提 PRE-x：由外部提供、我们无法单方保证的事实。前提失效时不变量必须整体重估。
• 不变量 INV-x：本系统自己保证的性质。变更用「追加 + 作废」（INV-7 → [作废 by INV-7b]），不静默改写。
• 声明边界 CLM-x：每条对外主张依赖哪些 PRE/INV、当前可否声明、挂起原因（[G-x] 缺口 / [Q-x] 待确认）。

验证映射在本文件 §4，是验收口径的唯一清单；代码与测试只做证据，不在此重复叙述。

1. 前提（外部提供）

编号	前提	若不成立的影响	状态
PRE-1	信箱消费权排他：同一时刻只有一个系统有权处理、打标、判定可清除（迁移期由切流规程保证单一权威写者）	水位、身份去重、清除前提全部失效	[待确认]（切流由运维规程保证，上线前另立）
PRE-2	ID 单调 + 可见时延上界：见 C-1/C-2	水位只能当快路径提示；空洞老化阈值无依据；不能声明发现完整性	[待确认 Q2]
PRE-3	ID 空间不复位、不复用、不回退：见 C-3	水位（不可逆单游标）之后的行永久不可见	[待确认 Q2]
PRE-4	报文的 DATE_RECEIVED 时钟基准可解释（偏斜在有界范围内）	跨系统时间比较（RECEIVED_AT 与本地 NOW）会提前或推迟判定	[待确认 Q7]
PRE-5	单活动实例运行（信箱读取不加锁、水位是单行覆盖写）	水位互相覆盖、空洞计时失真	[我们自证]（部署约束，见 architecture）
PRE-6	信箱与自有 PG 之间没有跨库事务	回填、水位推进、清除都不能声称原子	[我们自证]（架构事实）
PRE-7	报文不可变：同一业务身份的重发必为同一内容：见 C-4	上游改发会被判为重复并静默跳过	[待确认 Q15]
PRE-8	FLID 在保留期内不复用：见 C-21	「保留最新版本」的合并规则可能压掉新航班事件，旧 tombstone 可能删掉在用航班	[待确认 Q16]

2. 不变量

A. 管道

• INV-1 五个独立事实互不替代：落信 / 入队 / 处理完成 / 已回填 / 投递确认各有独立证据，前一个不蕴含后一个。
• INV-2 水位与入队同事务：不允许出现「水位已推进、消息未入队」的持久化状态；水位只增不减，遇空洞即停，只有判定为永久空洞才放行，且放行只跳过空洞本身、不越过任何已存在的行。
• INV-3 队头唯一：任一时刻只有一个可执行队头（最小未完成 MSG_ID，PENDING 与 FAILED 都占位）；FAILED 未退避到期时后续消息不得越过。
• INV-4 只领取已发现的行：主泵只领 MSG_ID ≤ W；水位之外的行只可能来自兼容入口，必须等水位追平后按序处理。
• INV-5 发现与处理互不阻塞：收报只看 ID > W，不以处理标记为谓词；终态而未回填的行不阻断后续消息的发现。
• INV-6 处理终态不可逆：已提交的 SUCCEEDED 不因回填或投递失败回改。
• INV-7 处理标记单调：任何路径只把空标记写成已处理值，不回撤、不覆盖。
• INV-8 回填只针对终态（PENDING / FAILED 永不写标记）；「还欠一次回填」的事实与终态由同一条语句落库，不存在第二处落账。
• INV-9 一信一行、一身份一记录：PROC_STATE 按 MSG_ID 唯一；同一业务身份至多绑定一条有效处理记录。
• INV-10 对外投递至少一次；端到端恰好一次不在交付范围。

B. 航班域（定义处；flight-state.md 只引编号）

• INV-11 自有 PG 的航班当前态是唯一权威；信箱、Kafka、展示视图都不是权威。
• INV-12 FLID 唯一；已写入非空的 OPERATION_DAY 不可改变。
• INV-13 每个航班每次成功状态写入单调推进 STATE_VERSION；重复消息不重复推进。
• INV-14 报文未携带的字段不被隐式清空；集合按完整合并结果写入，保留输入顺序与源序号。
• INV-15 缺席于某个日计划不构成删除理由；删除只由 FDEL 或受控历史清理触发。
• INV-16 外部副作用（回填、Kafka 投递、出站信箱）失败可重试，但不回滚已提交的本地业务结果。
• INV-17 状态变更、待发事件、处理终态与回填意图在同一 PG 事务内原子提交。
• INV-18 航班表的写者集合是「主泵处理器」与「历史清理」；两者必须互斥（同一 PIPELINE_LOCK，或清理在同一事务内复查判据后再删除），不得出现清理删除与处理器更新同一 FLID 的竞态。[实现核对待确认，关联 ACM2-30]
• INV-19 整包校验失败或运营日冲突时整包不落地，既有状态与版本保持不变。
• INV-20 处理器幂等：同一消息重复执行只产生一次业务效果。身份唯一只防「重复记录」，不防「重新执行」；29 类 FLOP 幂等矩阵补全前，本条不可声明。[G-FLOP-IDEMPOTENT]

3. 声明边界

编号	主张	依赖	当前可否声明	挂起原因
CLM-1	严格 FIFO：迟到的小 ID 不会越序	PRE-2、PRE-3、Q2	不可	发现完整性依赖库方承诺；窗口补偿扫描（G1）未交付
CLM-2	迟到报文不丢（可被发现并处置）	G1	不可	G1 未交付；现有阶段 0 只读检测仅计数告警，不补入队
CLM-3	重放不产生重复业务副作用	INV-20、G-FLOP-IDEMPOTENT	不可	29 类 FLOP 幂等矩阵未补全；重放不恢复历史顺序
CLM-4	回填不会被短暂故障放弃：最终打标，或进入可对账的放弃清单	INV-8、C-5、C-8	可声明（有条件）	条件：R 之前不放弃；MISSING_ROW 立即放弃并告警；放弃行须经人工对账才可用于清除判定（C-8）。原文保留另见 CLM-5
CLM-5	重放窗口内原文仍可读	C-6、C-7、Q7、Q9	不可	清除语义与保留期未确认；「打标即清除」下无补救
CLM-6	单实例内严格 FIFO	PRE-5、INV-3	可（限于单活动实例）	—
CLM-7	事件投递在同一 FLID 内保序	INV-10、投递设计	可（跨 FLID 不承诺）	实现当前按目标级全序投递，收敛到按 FLID 属投递改造，关联 ACM2-34
CLM-8	出站交付承诺只到「落信」	C-24、Q10	可（仅落信语义）	消费方与 ACK 列语义未确认
CLM-9	处理标记延迟由调度周期决定（≤30 秒）	—	不可	30 秒只是扫描调度周期；批次积压、单行超时与历史作业都会延长实际延迟

4. 验证映射

每条不变量至少一条证据；「缺口」表示尚无回归。测试名以仓库现状为准，新增测试按此表补位。

不变量	场景	证据 / 缺口
INV-1	五事实互不替代：入队不引用标记、回填不引用投递、投递不引用回填	缺口（需接口级断言）
INV-2	重复扫描、入队中断	不重复入队、不丢记录；InboxPollerTest
INV-2	空洞老化与重置	阈值内不推进、不越过入队；超期只放行空洞本身；旧空洞补齐后新空洞获得完整窗口
INV-2	水位写入与入队同事务	缺口（需真实 PG 事务用例，关联 ACM2-39）
INV-3 / CLM-1	较小 ID 迟到	缺口基线已固定：InboxPollerTest 钉住「水位越过后到达的较小 ID 不被发现」；补偿扫描交付前禁止任何「迟到不越序」的验收声明
INV-4	兼容入口与空洞并发	兼容入口登记的行超出水位、主泵不领取；PipelineSmokeTest「compat injected high id is not claimed until the watermark catches up」
INV-3	队头失败、退避及作业竞争	消息不越队；到期后恢复；作业不使消息无限饥饿
INV-5	终态未回填不阻断发现	缺口（补齐后应断言发现谓词不引用处理状态）
INV-6	投递失败后终态不变	缺口
INV-7	回填四种结果	写入成功 / 早已标记（不覆盖、记成功）/ 信箱行不存在（立即放弃并告警，不得视为已标记）/ 暂时故障持续到 R 仍未打标（停止自动重试，可人工恢复）
INV-7	RECEIVED_AT 为 NULL	超期分支仍成立且不导致标记提前写入——判据是本地 ENQUEUED_AT，与库方时钟及 NULL 无关
INV-8	PG 提交失败、信箱回填失败	事件、终态与回填意图一起回滚；已提交结果只补写标记，不重放业务；中间态永不补写
INV-8	非业务型终态	不触碰航班表 / MSG_EVENT，只写 PROC_STATE，且终态与回填意图同语句生效
INV-9	同身份多条记录、失败后重试、归档后重复	只产生一次有效业务处理，不把自身重试判为重复
INV-10	投递确认丢失、批次失败、次数耗尽	允许可识别的重发、保持目标顺序、整批退避并保留死信
INV-11	权威唯一	缺口（展示视图与缓存不得成为写入或对账来源）
INV-12 / INV-13	PG 事务失败、快照重复或迟到	整体回滚重试、不重复推进版本、不回退状态、不误删增量航班
INV-12	运营日冲突	整包 DEAD(PROTOCOL)，既有状态与版本不变
INV-14 / INV-19	整包协议拒绝（声明数不符、缺载荷）	整包不落地、整体回滚、既有状态不变
INV-15	缺席不删除	缺口（F-del 与清理路径分别断言）
INV-18	清理与处理并发	缺口：需断言删除与处理同一 FLID 时互斥（关联 ACM2-30）
INV-20 / CLM-3	重放同一条消息	缺口：29 类 FLOP 幂等矩阵未补全
CLM-4	放弃行与清除前提	断言放弃行不写标记、不被当作已打标（关联 ACM2-36）
CLM-9	回填/积压完成时限	缺口：需要「最老待回填年龄」「扫描积压」「作业心跳」指标（关联 ACM2-38）
—	请求超时、无匹配 RESP、时间单位不一致	不误用迟到应答、不提前完成请求
—	stub 误配置、重复实例、停机中断	生产拒绝不安全启动，工作线程能正确退出

5. 缺口索引与 Plane 的关系

本表是缺口标记的唯一清单：其他文档只在相应位置写 [G-x]，不解释、不记进度；工作进度在 Plane（ACM2）。

缺口	含义	影响
G1	窗口补偿扫描未实现（Plane ACM2-41）：水位越过后的迟到小 ID 没有补入队机制	CLM-1、CLM-2
G-IGNORE	忽略规则（LDM/REGN/RSTA/EROR）未实现（US-04）	INV-19 的忽略分支；合法忽略报文当前按 UNSUPPORTED 处理
G-RESP-GUARD	RESP 应答守卫未实现，当前与 DNLD 无差别进入快照写入	请求匹配闭环；C-23
G-REQ-TRACK	REQ_TRACK 无运行时协调器：出站适配、请求编码、超时与应答匹配未实现	US-08；C-24
G-PROC-HST	PROC_STATE_HST 未建表，终态归档未落地	US-11；归档能力
G-FLOP-IDEMPOTENT	29 类 FLOP 幂等矩阵未补全	INV-20、CLM-3
G-EVENT-RETENTION	MSG_EVENT 已发送行的保留期与清理作业未实现	outbox 有界性
G-BACKFILL-BACKOFF	回填独立退避键（backfill-backoff-ms / -cap-ms）未实现，暂沿用处理退避表	回填重试节奏
G-KAFKA-D3	kafka.producers.default.max-in-flight 默认 5，与架构决策 D3 要求的 1 不一致	投递幂等前提
G-JOB-HEARTBEAT	作业心跳、扫描积压、实际回填延迟指标未实现	CLM-9；回填可观测性
G-REPLAY-CHANNEL	「打标即清除」语义下的独立原文保留通道未设计	CLM-5

G1 沿用 Plane 既有编号（ACM2-41）；其余为文档内稳定标记，与 Plane 工作项的对应关系在 Plane 侧维护。