跳转至

重建义务账本

build_reconstruction_obligation_ledger 将经过认证的证据记录转换为确定性的重建声明列表。同一工作流可通过以下方式使用:

  • MCP 工具:build_reconstruction_obligation_ledger
  • CLI 命令:rea build-reconstruction-obligation-ledger

该账本在设计上刻意保守。静态 Application Graph 事实会创建候选义务,但并不证明运行时或进程行为。只有当某个清单绑定提供了唯一所有者、所有必需的解析器/模式/领域类型、每个必需的用例夹具,以及一个权威性与原始观察相当的通过验证器时,必需义务才会关闭。该验证器必须枚举义务 ID,并且其结果必须存在于输入的证据包中。矛盾、重复的定义或所有者、残余未知项、缺失的依赖项以及不可用的权威,都会使义务保持未关闭或失败状态。

原始进程权威要求观察到带有受支持的进程捕获提供程序和有效捕获载荷的 controlled-replay 证据。单独匹配的操作或谓词并不能确立该权威,即便对于已审阅义务和清单原始用例也是如此。

每个夹具和验证器证明都必须将其结果绑定到正在评估的确切所有者实现摘要和义务修订版本。关于调用方生成的契约,请参阅 证明适用性。

完整 CLI 请求

这个空请求对于检查客户端集成非常有用。它是有效的,并返回一个包含零义务的 unknown 账本;缺少源证据绝不会宣称关闭:

rea build-reconstruction-obligation-ledger \
  '{
    "evidence_bundle": {
      "artifacts": [],
      "providers": [],
      "environments": [],
      "scenarios": [],
      "captures": [],
      "unknowns": [],
      "records": []
    },
    "reviewed_obligations": [],
    "manifest": {
      "bindings": [],
      "contradictions": []
    }
  }' \
  --json

对于实际调查,请从会话中导出一个证据包并替换空包。Application Graph 和进程捕获记录会自动生成保守的候选义务。当这些来源未体现某个必需声明时,请添加已审阅义务。

已审阅义务示例

下面的每个示例都是一个完整的 reviewed_obligations 元素。请将示例 Evidence ID 替换为 evidence_bundle.records 中已有的经过认证的审阅记录。稳定的 ID 和版本使变更可被审阅。

CLI 解析

{
  "obligation_id": "cli.config.invalid-option",
  "obligation_version": 1,
  "title": "Reject an invalid configuration option with the supported CLI error",
  "application_layer": "cli",
  "family": "argument-parsing",
  "target": {
    "artifact_sha256": null,
    "application_node_id": null,
    "semantic_node_id": null,
    "location": "rea --unknown-option"
  },
  "required": true,
  "required_case_kinds": ["positive", "negative", "malformed"],
  "required_original_authority": "process",
  "required_fixture_authority": "packaged-process",
  "required_verifier_authority": "packaged-process",
  "requires_parser_type": true,
  "dependency_obligation_ids": [],
  "residual_unknown_ids": [],
  "unavailable_authority": [],
  "required_next_evidence": ["Capture the installed CLI for all three cases."],
  "disposition": "active",
  "review_evidence_ids": [
    "ev_aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"
  ]
}

协议处理程序

{
  "obligation_id": "protocol.rpc.cancel",
  "obligation_version": 1,
  "title": "Cancel an in-flight request and emit one terminal response",
  "application_layer": "protocol",
  "family": "request-response",
  "target": {
    "artifact_sha256": null,
    "application_node_id": null,
    "semantic_node_id": null,
    "location": "JSON-RPC request cancellation"
  },
  "required": true,
  "required_case_kinds": ["positive", "negative", "malformed", "cancellation"],
  "required_original_authority": "external",
  "required_fixture_authority": "protocol",
  "required_verifier_authority": "protocol",
  "requires_parser_type": true,
  "dependency_obligation_ids": [],
  "residual_unknown_ids": [],
  "unavailable_authority": [],
  "required_next_evidence": [
    "Record request, cancellation, and terminal response IDs."
  ],
  "disposition": "active",
  "review_evidence_ids": [
    "ev_bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb"
  ]
}

Electron 启动与后台行为

{
  "obligation_id": "electron.background.startup",
  "obligation_version": 1,
  "title": "Start the background process before exposing the renderer bridge",
  "application_layer": "electron",
  "family": "startup",
  "target": {
    "artifact_sha256": null,
    "application_node_id": null,
    "semantic_node_id": null,
    "location": "main process startup"
  },
  "required": true,
  "required_case_kinds": ["positive", "negative", "teardown"],
  "required_original_authority": "runtime",
  "required_fixture_authority": "renderer",
  "required_verifier_authority": "renderer",
  "requires_parser_type": false,
  "dependency_obligation_ids": [],
  "residual_unknown_ids": [],
  "unavailable_authority": [],
  "required_next_evidence": [
    "Observe main/renderer ordering and application shutdown."
  ],
  "disposition": "active",
  "review_evidence_ids": [
    "ev_cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc"
  ]
}

持久化迁移

{
  "obligation_id": "persistence.profile.migrate-v2",
  "obligation_version": 1,
  "title": "Migrate a version-one profile without losing unknown fields",
  "application_layer": "persistence",
  "family": "migration",
  "target": {
    "artifact_sha256": null,
    "application_node_id": null,
    "semantic_node_id": null,
    "location": "profile schema v1 to v2"
  },
  "required": true,
  "required_case_kinds": ["positive", "negative", "malformed"],
  "required_original_authority": "runtime",
  "required_fixture_authority": "integration",
  "required_verifier_authority": "integration",
  "requires_parser_type": true,
  "dependency_obligation_ids": [],
  "residual_unknown_ids": [],
  "unavailable_authority": [],
  "required_next_evidence": [
    "Compare pre-migration and committed storage snapshots."
  ],
  "disposition": "active",
  "review_evidence_ids": [
    "ev_dddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddddd"
  ]
}

原生 ABI

{
  "obligation_id": "native-abi.helper.status",
  "obligation_version": 1,
  "title": "Preserve the helper status-code and output-buffer contract",
  "application_layer": "native-abi",
  "family": "ffi",
  "target": {
    "artifact_sha256": null,
    "application_node_id": null,
    "semantic_node_id": null,
    "location": "helper_status(const uint8_t *, size_t, uint8_t *, size_t *)"
  },
  "required": true,
  "required_case_kinds": ["positive", "negative", "malformed"],
  "required_original_authority": "process",
  "required_fixture_authority": "native-abi",
  "required_verifier_authority": "native-abi",
  "requires_parser_type": true,
  "dependency_obligation_ids": [],
  "residual_unknown_ids": [],
  "unavailable_authority": [],
  "required_next_evidence": [
    "Run the ABI harness against the shipped and reconstructed libraries."
  ],
  "disposition": "active",
  "review_evidence_ids": [
    "ev_eeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeeee"
  ]
}

清单与闭包

清单绑定指明一个所有者以及调用方提供的 owner_sha256。original_cases 和重建夹具列表都必须以经过认证的、可比较的证据覆盖每一个 required_case_kinds 值。当 requires_parser_type 为 true 时,parser_type 是必需的。

账本不会读取 module_path、执行 verifier.command,也不会计算实现摘要。所有者字段并未说明摘要涵盖的是模块字节、符号表示,还是多文件实现。证明生成者必须记录确切的哈希输入以及任何规范化方式,以便其他验证者能够重现该承诺;仅凭路径或符号名无法定义该承诺。

{
  "obligation_id": "protocol.rpc.cancel",
  "owner": {
    "module_path": "src/protocol/requestRouter.ts",
    "symbol": "cancelRequest",
    "owner_sha256": "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff"
  },
  "parser_type": {
    "parser": "parseCancelRequest",
    "schema": "cancelRequestSchema",
    "domain_type": "CancelRequest"
  },
  "original_cases": [
    {
      "kind": "positive",
      "evidence_id": "ev_6666666666666666666666666666666666666666666666666666666666666666",
      "location": "/captures/positive"
    },
    {
      "kind": "negative",
      "evidence_id": "ev_7777777777777777777777777777777777777777777777777777777777777777",
      "location": "/captures/negative"
    },
    {
      "kind": "malformed",
      "evidence_id": "ev_8888888888888888888888888888888888888888888888888888888888888888",
      "location": "/captures/malformed"
    },
    {
      "kind": "cancellation",
      "evidence_id": "ev_9999999999999999999999999999999999999999999999999999999999999999",
      "location": "/captures/cancellation"
    }
  ],
  "fixtures": [
    {
      "fixture_id": "rpc.cancel.positive",
      "case_kind": "positive",
      "authority": "protocol",
      "evidence_ids": [
        "ev_1111111111111111111111111111111111111111111111111111111111111111"
      ]
    },
    {
      "fixture_id": "rpc.cancel.negative",
      "case_kind": "negative",
      "authority": "protocol",
      "evidence_ids": [
        "ev_2222222222222222222222222222222222222222222222222222222222222222"
      ]
    },
    {
      "fixture_id": "rpc.cancel.malformed",
      "case_kind": "malformed",
      "authority": "protocol",
      "evidence_ids": [
        "ev_3333333333333333333333333333333333333333333333333333333333333333"
      ]
    },
    {
      "fixture_id": "rpc.cancel.cancellation",
      "case_kind": "cancellation",
      "authority": "protocol",
      "evidence_ids": [
        "ev_4444444444444444444444444444444444444444444444444444444444444444"
      ]
    }
  ],
  "verifier": {
    "verifier_id": "rpc.cancel.conformance",
    "claim_id": "protocol.rpc.cancel.v1",
    "command": "npm run test:protocol -- cancel",
    "authority": "protocol",
    "status": "pass",
    "result_evidence_id": "ev_5555555555555555555555555555555555555555555555555555555555555555",
    "enumerated_obligation_ids": ["protocol.rpc.cancel"],
    "nondeterminism": {
      "mode": "partial-order",
      "specification": "cancel precedes the single terminal response"
    }
  }
}

就绪的账本要求所有保留的证据引用都能在包中得到解析,包括可选用例种类上的引用。未解析的引用仍会在账本中可见并产生诊断信息;它们无法关闭义务。一个通过的单元测试不能关闭 packaged-process 义务。仅静态的源代码无法关闭运行时或进程声明。将声明标记为 blocked 或 out-of-scope 只会记录该处置状态,而不会默默将其计为已验证。

证明适用性

请将三项检查分开:

  • 真实性: 保留的证据通过其完整性检查。
  • 权威性: 观察结果具有声明所要求的种类和强度。
  • 适用性: 证明描述的是当前正在评估的实现和义务修订版本。

证明生成者提供带有谓词类型 rea.reconstruction-proof、操作 verify_reconstruction_obligations 以及以下 normalized_result 结构的观察证据,该结构由 reconstructionObligationProofSchema 定义。REA 评估保留的结果;此操作标签不会暴露证明执行器,也不会运行清单命令。

{
  "bindings": [
    {
      "obligation_id": "protocol.rpc.cancel",
      "obligation_version": 1,
      "owner_sha256": "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
      "fixtures": [
        {
          "fixture_id": "fixture.cancel.positive",
          "case_kind": "positive",
          "passed": true
        }
      ],
      "verifiers": [
        {
          "verifier_id": "verifier.cancel",
          "claim_id": "claim.cancel",
          "passed": true
        }
      ]
    }
  ]
}

owner_sha256 与实现所有者在清单中提供的小写 64 位十六进制 SHA-256 承诺相同。证明生成者根据上文所述的相同文档化输入和规范化方式计算该值;REA 会比较这些承诺,而不会重新计算它们。证明的 obligation_version 必须与被评估的义务版本完全一致,包括对生成的义务也是如此。在修订已审查的需求时,应增加该版本。

在单个匹配的义务/所有者/修订绑定中,fixture 证明必须指定精确的 (fixture_id, case_kind) 对,verifier 证明必须指定精确的 (verifier_id, claim_id) 对。每个选中的声明都必须报告 passed: true;匹配的失败声明不能被重复的通过声明所掩盖。声明可以共享记录,但来自不同绑定的身份或结果永远不会被合并。fixture 和 verifier 的证据权威还必须满足现有的权威要求。

更改所有者摘要或义务版本会使保留的证明不再适用。身份缺失(包括遗留的 ID 数组证明记录)会使账本保持开放,并产生 inapplicable-fixture-proof 或 inapplicable-verifier-proof;详细信息可区分格式错误或缺失的元数据(invalid-proof)、owner-mismatch、revision-mismatch 和 claim-mismatch。适用的虚假结果会产生 fixture-failed 或 verifier-failed,并导致所需的账本失败。未知、不受支持或被跳过的 verifier 声明会产生 verifier-unavailable,并使闭合保持开放。在实现或需求变更后,应替换 fixture 和 verifier 的证据。旧证据仍然是有效的溯源,但不能确立当前的适用性。

summary 对义务进行计数。by_status、by_application_layer 和 by_source_state 将每个义务放入恰好一个桶中。by_evidence_authority 根据义务 authority_references 中的证据 authority 对义务进行分组:一个义务在其引用的每个不同 authority 下各计数一次,因此这些计数可能超过 total。引用自身的 state 和义务的 source_state 不影响其 authority 桶。

工具内联返回每个义务。其 ledger_id 和 closure_digest 标识完整结果,包括汇总、报告、所有权和依赖关系图、证据链接及局限性。新的 closure_digest 标识已更改的账本;它并不证明 verifier 已再次运行。适用性对照保留证明的显式绑定进行检查。

对于具有显式 verifier 契约和包证明类型的命名边界,请参阅重建覆盖范围。

本页原文 Markdown:在 AtomGit 查看·内容源自开源项目 rea2/rea