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 的竞态。
• INV-19 整包校验失败或运营日冲突时整包不落地，既有状态与版本保持不变。
• INV-20 处理器幂等：同一消息重复执行只产生一次业务效果。身份唯一只防「重复记录」，不防「重新执行」；29 类 FLOP 幂等矩阵补全前，本条不可声明。[G-FLOP-IDEMPOTENT]
• INV-21 MAFL 是派生投影：内容恒等于「STATE = ACTIVE 且 MAID = 主航班 FLID」的子航班集合（元素 FLID + FLNO，按 FLID 升序），不落库、不从入站解析；自引用与悬挂引用不入投影。
• INV-22 子航班集合变化必须使涉及的主航班在同一事务内推进 STATE_VERSION 并登记主航班事件；投影只进不退，版本不推进即被下游丢弃。

3. 声明边界

编号	主张	依赖	当前可否声明	挂起原因
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 秒只是扫描调度周期；批次积压、单行超时与历史作业都会延长实际延迟
CLM-10	容量量级假设（单实例、入站日消息量千级到万级、单报文 ≤ 10⁴ 字节）	—	不可	未实测，无生产负载数据；解除条件：取得现役信箱日量、峰值与单报文上限后重估

4. 验证映射

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

不变量	场景	证据 / 缺口
INV-1	五事实互不替代：入队不引用标记、回填不引用投递、投递不引用回填	缺口（需接口级断言）
INV-2	重复扫描、入队中断	不重复入队、不丢记录；InboxPollerTest
INV-2	空洞老化与重置	阈值内不推进、不越过入队；超期只放行空洞本身；旧空洞补齐后新空洞获得完整窗口
INV-2	水位写入与入队同事务	缺口（需真实 PG 事务用例，关联 ACM2-39）
INV-3	较小 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-19	整包协议拒绝（声明数不符、运营日冲突）	DEAD(PROTOCOL)，整包不落地、整体回滚、既有状态不变
INV-15	缺席不删除	缺口（F-del 与清理路径分别断言）
INV-16	外部副作用失败后本地结果不变	待核对
INV-17	业务型终态四件套同事务	待核对；真实 PG 用例待补（ACM2-39）
INV-18	清理与处理并发	HistorySweepJobTest（归档后被主泵更新的航班不删除、不发 tombstone）+ HistorySweepPurgePgTest（删除阶段失败时 tombstone 与删除整体回滚）
INV-20 / CLM-3	重放同一条消息	缺口：29 类 FLOP 幂等矩阵未补全
INV-21	MAFL 投影与 ACTIVE 子航班集合一致（子航班删除后退出、自引用与悬挂引用不入、顺序确定）	缺口：投影未实现（[G-MAFL]）
INV-22	子航班新增、删除、MAID 迁移时主航班版本与事件	缺口：主/共享级联未实现（[G-MAFL]）
CLM-4	放弃行与清除前提	断言放弃行不写标记、不被当作已打标（关联 ACM2-36）
CLM-9	回填/积压完成时限	指标已就位：msgx.pipeline.job.heartbeat_age_seconds / ticks.total / failures.total / last_sweep_selected 与 msgx.pipeline.backfill.oldest_unmarked_seconds（关联 ACM2-38）；实际延迟仍需现场数据，CLM-9 不可声明
—	请求超时、无匹配 RESP、时间单位不一致	不误用迟到应答、不提前完成请求
—	stub 误配置、重复实例、停机中断	生产拒绝不安全启动，工作线程能正确退出

5. 缺口索引与 Plane 的关系

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

缺口	含义	影响
G-IGNORE	忽略规则（LDM/REGN/RSTA/EROR）未实现	US-04；合法忽略报文当前按 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）未实现，当前为代码内硬编码（取值见 reference）	回填重试节奏
G-KAFKA-D3	kafka.producers.default.max-in-flight 与 D3 要求的 1 不一致（取值见 reference）	投递幂等前提
G-REPLAY-CHANNEL	「打标即清除」语义下的独立原文保留通道未设计	CLM-5
G-MAFL	主航班 MAFL 派生投影及主/共享原子级联未实现（规则见 INV-21/INV-22）；MAFL 不是 SIS/XML 入站字段	航班完整态；删除与重建
G-SRVT-VIPF	SIS/XML 的 SRVT、VIPF 无界集合尚未映射到持久化明细；wire/domain 只保留出现事实与原始内容，不参与合并与投递（清空语义见 Q13）	航班完整态；无损字段保存
G-COMPAT-HTTP	compat 入口仍未实现 Q3 定案后的 ResponseDto、媒体类型、字符集、失败响应与请求体上限	C-28；US-02
G-REQ-OPEN-UNIQUE	REQ_TRACK 尚无约束开放态 (REQ_TYPE, OPERATION_DAY, SENDER) 唯一性的部分索引	US-08；G-REQ-TRACK

缺口标记与 Plane 工作项的对应关系在 Plane 侧维护。