buzz-conformance Trace Schema 全解析用运行时轨迹把多租户中继钉死在 TLA 规范上【免费下载链接】buzzA hive mind communication platform项目地址: https://gitcode.com/GitHub_Trending/buzz14/buzz导读crates/buzz-conformance/TRACE_SCHEMA.md定义了 Buzz 项目中运行时形式化合规runtime formal compliance网关的轨迹契约中继relay在 ingest/auth/read 接受-拒绝边界上逐决策发射TraceStep独立的回放检查器replay checker在不调用任何生产 reducer 的前提下用 Rust 重新实现的 TLANext关系逐条校验这些步骤。读完本文你将掌握轨迹步骤的字段结构与投影规则、九个动作TraceAction各自对应的规范行号、四条让网关咬合bite的失败模式以及 emitter / checker 双端的真实代码落点与 CI 验证命令。北极星原则不要问模型是否通过要问运行代码是否发射了模型可接受的轨迹整个网关的设计哲学浓缩为一句话见 TRACE_SCHEMA.mdDont ask did the model pass. Ask did the running code emit a trace the model accepts.这句话的含义是形式化规范docs/spec/MultiTenantRelay.tla由 TLC 机器校验而生产中继是另一套代码。二者之间的鸿沟由运行时轨迹来弥合——中继在 ingest/auth/read 接缝处为每个决策发射一条TraceStep检查器把轨迹回放一遍与规范Next关系的 Rust 重实现逐条比对。检查器不会调用任何生产 reducer避免用实现验证实现的同源谬误。该契约同时强调同步纪律schema 一旦变更本文档必须在同一个 commit 内变更SCHEMA_VERSION常量位于 crates/buzz-conformance/src/lib.rs 第 86 行当前为1。一条轨迹步骤长什么样TraceStep中继每做一次决策就发射一条步骤格式如下JSONC 示意{ schema: 1, action: { /* TraceAction — 见下文动作表 */ }, state: { resolved_community: uuid, // 来自 TenantContext::community() bound_host: host str, // 来自 TenantContext::host() actor: 16 hex // 认证公钥的前 16 位十六进制 } }在 Rust 类型系统中这条结构对应 lib.rs 中的TraceStepschema_version: u32— 当前恒为SCHEMA_VERSIONaction: TraceAction— 本次决策的动作state_after: AbstractState— 动作发生时实现所观察到的抽象状态检查器把它与独立计算出的模型状态比对。state 是投影状态projected state不是原始状态AbstractState刻意只携带规范Next与Inv_NonInterference需要推理的字段而不携带任何可反推出密钥、载荷或客户端输入的原始数据字段携带什么刻意不携带什么resolved_community服务端解析出的社区 UUID客户端声称的htag、事件 id、载荷bound_host来自解析器的不透明 host 字符串原始Host头字节actor认证公钥的前 16 位十六进制字符私钥、NIP-98 token、签名关于actor前缀有一个精心论证的取舍见 conformance/mod.rs 中actor_label的注释公钥本身对客户端而言已经是一个哈希Schnorr X-only截取前 16 个十六进制字符在等值判断上等价于完整公钥而中继现有日志早已打印完整公钥 hex——因此前缀不会泄露日志尚未泄露的信息同时避免了为观测代码引入哈希依赖。msg_id_label采用同样的逻辑取事件 id本身是 sha256前 16 位 hex。动作词汇表九个TraceAction变体TraceAction枚举镜像规范Next关系MultiTenantRelay.tla 第 933 行起每个变体都锚定规范中的精确行号。从源码结构看全部动作被划分为四个接缝seam写入接缝Write seamwrite_insert { msg_id, channel, claimed_community }— 规范WriteInsert约第 514 行。一次成功的按频道插入。行的社区按规范为ChannelCommunity(channel)由检查器从模型中查得因此动作上没有row_community字段。claimed_community客户端htag 声称的社区被单独记录好让检查器在客户端声称与ChannelCommunity(channel)不一致时咬合。write_insert_global { msg_id, claimed_community }— 规范WriteInsertGlobal约第 562 行。无频道写入DM、gift-wrap 等行的社区由bound_host经 host-community 映射推导动作上没有channel字段claimed_community同样保留以作审计。write_duplicate { msg_id, channel, claimed_community }— 规范WriteDuplicate约第 612 行。数据库返回已存在未新增任何行因为没有产生行所以没有row_community。读取接缝Read seamauth_check { channel, claimed_community, verdict }— 规范AuthCheck约第 794 行。M2/M8 突变专门针对这个动作。检查器强制要求Allow判定必须满足频道社区 resolved_communityhost-channel 栅栏且actor 对该频道拥有 scope。read_message_rows { channel, row_communities }— 规范ReadMessageRows约第 643 行。批量读取返回候选行。row_communities是不去重的Vec——检查器必须看到每一个泄露的标签而不是去重后的集合。read_by_id_rows { channel, row_communities }— 规范ReadByIdRows约第 681 行。搜索通道为每个重取的命中发出该动作。把搜索建模为read_message_rows候选 每个命中的read_by_id_rows使逐命中重授权对检查器可见。read_host_feed_rows { row_communities }— 规范ReadHostFeedRows。仅限 kinds 的 feed 读取社区由bound_host推导。错误接缝Error seamsanitized_error { reason }其中reason ∈ { restricted, invalid, server_error }— 规范Inv_SanitizedErrors、M6 突变约第 778 行。字母表是封闭的如果IngestError将来增加第四个变体conformance/mod.rs 中的sanitized_reason_for匹配会变成非穷尽non-exhaustiveCI 直接编译失败——错误桶的数量被编译期锁死。覆盖缺口Coverage breachimpl_bug { kind }— 这不是规范动作而是运行时见证witness关键接缝退出时没有记录任何其他动作。由EmitGuard::Drop在计数 tracer 计数为零时发射检查器将其视为覆盖缺口并 fail-closed。每个动作还暴露kind()方法返回稳定短字符串如write_insert供 fixture 声明与错误消息使用is_critical()恒为true——该接缝上的每个动作都是关键动作这正是覆盖缺口模式赖以成立的前提。三条承重投影规则这是文档中特别强调的承重load-bearing规则一个 buggy 中继如果对违规做了归一化normalize就能发射出看似在规范内的轨迹。检查器的立场是假定你没有归一化。claimed_community与resolved_community分开记录。两者一旦不一致规范说resolved 赢但轨迹必须同时展示二者M2声称驱动的认证才能咬合。row_communities是Vec而非Set且不按已解析租户过滤。结果集里若有两行属于不同社区检查器必须看到两个标签否则它无法对Inv_ReadConfinementfail-closed。注意 transitions.rs 中check_row_labels的实现即使 buggy 中继把同一外国行返回两次、或把外国标签去重到只剩一次检查器都会咬合——外国标签的存在就是整个门槛。SanitizedReason是三个元素的封闭字母表。中继的IngestError变体与其 1:1 映射第四个变体是 CI 失败而不是一个静默桶。Emitter 侧buzz-relay 的 conformance 模块发射器住在中继进程内职责是把实现的真实决策翻译成TraceStep。各文件分工如下文件发射什么crates/buzz-relay/src/conformance/mod.rs辅助函数 EmitGuardsanitized_reason_forcrates/buzz-relay/src/conformance/tracers.rsNoopTracer生产默认、JsonlTracercrates/buzz-relay/src/handlers/ingest.rsAuthCheck、WriteInsert、WriteInsertGlobal、WriteDuplicate、外层包装的SanitizedErrorcrates/buzz-relay/src/handlers/req.rs暂缓——作为增量补丁挂接在 Max 的 req.rs 工作之上关键实现细节state_for_request(tenant, actor)从TenantContext取resolved_community与bound_host服务端解析绝不来自客户端输入actor 取公钥前 16 位 hex。claimed_community_from_event从事件htag 解析客户端声称的社区 UUID。中继不信这个值做解析——解析只用服务端持有的 channel→community 映射分开记录才让 M2 咬合可见。project_row_communities按行自身channel_id投影每行的真实社区标签策略 (B) 护栏channel-scoped 行在communities_of_channels查找映射中查命中返回查得的标签未命中返回MissingLookup调用方必须当作覆盖缺口 fail-closed发射impl_bugchannel-less 行投影为 resolved 社区——这是诚实的投影而非同义反复社区全局行确实受租户作用域约束。区分依据是行自身的channel_id而非查询过滤器因此 channel-scoped 行无法伪装成 channel-less 逃过查找。EmitGuardRAII关键接缝当前为ingest_event入口处EmitGuard::arm包装 tracer 为计数 tracer接缝退出时若计数为零Drop向底层 tracer 发射合成impl_bug步骤。生产代码路径无需解除守卫——它照常调用tracer.record(...)包装器自动计数。CountingTracer::enabled必须转发给内层 tracer 而非继承true默认值包在NoopTracer上返回true会重新引入热路径开销包在真实 tracer 上返回false会让发射被跳过导致EmitGuard误报。sanitized_reason_forRejected → Invalid、AuthFailed → Restricted、Internal → ServerError1:1 穷尽映射。生产默认NoopTracer的enabled()返回false热路径上的发射器必须先查询它再构建发射输入尤其是读接缝独立于取数查询的communities_of_channels查找避免纯开销。JsonlTracer则把每个步骤序列化为一行 JSON 追加写入文件append truncate 语义见 tracers.rs。ingest_event的实际调用点ingest.rs 第 2124-2159 行附近展示了完整流程先state_for_request构造抽象状态再EmitGuard::arm成功路径上在dispatch_persistent_event的两个发射点分别发WriteInsert/WriteInsertGlobal/WriteDuplicate失败路径统一由外层包装把IngestError经sanitized_reason_for映射为SanitizedError。Checker 侧buzz-conformance 的回放引擎检查器是独立 crate刻意不导入buzz-relay、buzz-db、buzz-auth等任何生产 crate杜绝与发射器共享归一化 bug。文件分工文件职责crates/buzz-conformance/src/lib.rsschema Tracertraitcrates/buzz-conformance/src/transitions.rs规范Next关系的 Rust 重实现crates/buzz-conformance/src/checker.rs回放引擎IllegalTransition/StateMismatch/NonInterference/CoverageBreach类型独立性设计schema层刻意不复用buzz_core::CommunityId而是自建CommunityLabel新类型。原因有二见 lib.rs 第 46-77 行注释其一CommunityId有意没有FromUuid/Serialize/Deserialize防止客户端输入凭空制造社区 id——给它加 Serde 会在这道生产围栏上打洞其二schema 与生产类型零共享机械上杜绝 buggy 生产类型把 bug 洗进检查器。中继发射端在接缝处转换CommunityLabel::from_uuid(*tenant.community().as_uuid())。check_trace的四阶段流程checker.rs 中check_trace极简而 fail-fast任何一步失败立即返回Bootstrap以第一条步骤的state_after作为模型状态resolved_community/bound_host/actor。空轨迹直接判定CoverageBreach——接缝被触达却什么都没发射。Schema 版本检查每条步骤的schema_version必须等于SCHEMA_VERSION不一致视为IllegalTransition没有任何转换规则适用于异版本。逐步骤转换检查check_step先做普适的状态匹配resolved community / bound host / actor 不得中途翻转——否则就是StateMismatch说明租户上下文被中途重赋值再按动作类型做专属检查。覆盖检查Scenario::required_critical_actions中声明必须出现的动作种类若在轨迹中缺失返回CoverageBreach。Scenario提供unstructured(trace)不要求任何动作与require(kind)链式追加要求两个构造助手。动作专属检查的咬合点从 transitions.rs 的实现看每个动作的判定并非平均用力WriteInsert/WriteInsertGlobal/WriteDuplicate只做普适状态匹配。规范对claimed_community的态度是host wins忽略声称因此声称不一致在这个动作上允许——真正咬合它的是下一次读取的行标签。AuthCheckAllowclaimed_community ! resolved_community直接IllegalTransition——M2声称驱动认证与 M8A-host 驱动 B-channel 判定在此坍缩为Allow 伴随外国标签泄露。而Deny无论声称是否一致都是 in-spec 的规范把 Deny 建模为 catch-all故不咬。三个读取动作统一走check_row_labels任何行标签 ≠ resolved 社区即NonInterference规范Inv_NonInterference约第 983 行 /Inv_ReadConfinement约第 1003 行的直接翻译。SanitizedError检查 variant 属于封闭集合类型系统已保证检查近乎平凡。ImplBug无条件CoverageBreach。四种失败模式网关何时咬合check_trace在下列任一情形返回Err(CheckError)IllegalTransition— 动作在当前模型状态下不被允许例如AuthCheck { verdict: Allow, claimed ! resolved }——M2/M8 领地。StateMismatch—state_after与 bootstrapped 模型不一致请求中途被重赋 resolved community / bound host / actor。NonInterference—row_communities包含 resolved 社区以外的标签Inv_NonInterference/Inv_ReadConfinement。CoverageBreach— 轨迹中出现了ImplBug步骤、或场景要求的动作从未出现、或轨迹为空。每种失败模式在 checker.rs 的tests模块中都有单元测试证明网关会按预期咬合包括空轨迹咬CoverageBreach、跨社区行咬NonInterference、Allow 外国声称咬IllegalTransition、Deny 外国声称通过、状态中途翻转咬StateMismatch、ImplBug咬CoverageBreach、缺失必需动作咬CoverageBreach、以及三种SanitizedError单独出现均合规。测试与 CI把网关钉在门禁上LIMITS.md 给出了三条必须在每个 PR 保持绿色的测试面# 1. Schema checker 单元测试9 个直接覆盖转换规则 # 每个 TraceAction 变体都有通过用例和至少一个突变级咬合用例。 cargo test -p buzz-conformance --lib # 2. Replay fixtures5 个测试tests/fixtures/ 下提交了 JSONL 轨迹 # 测试先用类型化 Rust 重建每条轨迹、断言与提交文件逐字节一致 # schema 变更必须同步更新 fixtures再经 check_trace 回放 # - good.jsonl → Ok(()) # - bad_host_channel_mismatch.jsonl → IllegalTransition # - bad_coverage_breach.jsonl → CoverageBreach # - bad_foreign_row_leak.jsonl → NonInterference # - 空轨迹 → CoverageBreach # # 需要有意刷新 fixture 时 # BUZZ_CONFORMANCE_UPDATE1 cargo test -p buzz-conformance --test replay_fixtures cargo test -p buzz-conformance --test replay_fixtures # 3. EmitGuard 覆盖缺口自测2 个测试位于 # crates/buzz-relay/src/conformance/mod.rs证明 Drop guard 在 # 无发射到达 tracer 时记录 ImplBug、有发射时保持静默。 cargo test -p buzz-relay --lib conformance::合计9 5 2 16 个测试对 NI、IllegalTransition、CoverageBreach 三个闸门都有突变级咬合证明。除此之外tests/proptest_checker.rs 用 proptest 生成随机动作序列拓宽输入空间断言的是规范派生的不变量而非平行 oracle任何携带外国行标签的读取必须被拒、完全干净的轨迹必须被接受、Allow 外国声称必须咬、ImplBug必须咬、状态中途翻转必须咬且检查器永不 panic、结果确定。网关的边界它不是证明LIMITS.md 非常坦诚地划定了该网关不覆盖的范围避免把绿灯误读成形式化证明覆盖度 执行覆盖度只校验你实际跑过的执行。未执行的代码路径保持静默——这正是覆盖缺口模式承重的原因但覆盖缺口只能命中已武装的接缝新增端点若绕过EmitGuard::arm网关会失明靠 code review 兜底。投影读不到的数据层泄露若WHERE子句返回跨社区行而投影不读取足够信息则此处不显现。跨 pod 泄露harness 只追踪单进程多 pod 攻击NIP-98 跨 pod 重放等只在观察到的那个 pod 上显现。无时间属性规范与网关都不含时间并发/乱序下的 bug 不在此闸门范围内。Pubsub 扇出扇出不是规范动作泄露只出现在接收方的 ingest/read 轨迹中。类型级围栏违规CommunityId没有FromUuid由编译器保证不由本网关保证。规范本身的 bug检查器只是重实现了规范规范错了两边一起错——规范正确性由 TLC 机器校验承担。另一个关键事实网关是纯观测性的。Tracer NoopTracer生产默认时所有发射与守卫武装都是 no-op中继照常运行、照常决策——网关不向决策回馈任何信号关闭它只损失可观测性。文档还预告了下一道棘轮读接缝发射器落地 Eva 的集成分支后harness 将用每个请求一个JsonlTracer驱动既有 e2e 套件对每条捕获的轨迹断言check_trace。小结buzz-conformance的轨迹契约把形式化规范与生产实现之间的信任鸿沟收窄为一条可审计、可重放、可 fail-closed 的观测通道发射器只投影规范需要推理的抽象状态检查器用独立的 Rust 重实现裁决每一步EmitGuard与封闭错误字母表堵死静默漏发射与新错误桶两个退化方向而 16 个测试 proptest 不变量把每个闸门的咬合行为固化为 CI 事实。对任何想为多租户系统构建运行时形式化合规管线的团队这份 schema 与它的实现是一个可直接借鉴的完整范例。【免费下载链接】buzzA hive mind communication platform项目地址: https://gitcode.com/GitHub_Trending/buzz14/buzz创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考
