docs: clarify evidence applicability and boundary limitations

docs/client-configuration.md

@@ -248,6 +248,20 @@ standalone CLI check.
 
 ## Codex and Devin
 
+REA manages its launcher and selected provider settings in the client
+registration. Codex's server and per-tool approval policies are user choices.
+Current limitation: doctor rejects nested `[mcp_servers.rea.tools.<name>]`
+approval tables as an invalid registration
+([#3862](https://github.com/morluto/rea/issues/3862)), and setup refresh rebuilds
+the REA entry without those tables or `default_tools_approval_mode`
+([#3863](https://github.com/morluto/rea/issues/3863)). Preserving unrelated server
+entries, valid environment overrides, and positive timeouts does not establish
+preservation of these policy fields. Do not rerun setup solely to clear this
+diagnostic. If a refresh is needed, back up the configuration and restore the
+policy fields from that backup or the reported recovery snapshot before
+restarting Codex. The per-tool table can still cause the doctor diagnostic
+after restoration.
+
 Codex treats an unset or empty `CODEX_HOME` as `~/.codex`. Its MCP server
 registration supports `startup_timeout_sec` for connection initialization and
 `tool_timeout_sec` for each tool call. New REA registrations use a 30-second

docs/installation.md

@@ -60,7 +60,10 @@ Before applying changes, REA checks your current configuration. The plan lists:
 
 Malformed or unsafe existing configuration blocks the whole transaction before
 Hopper installation or any file write. Declining or pressing Ctrl-C makes no
-changes. Agent configuration writes preserve unrelated entries and comments,
+changes. Client configuration files and bundled skill files have separate
+publication and recovery paths; the guarantees in this paragraph apply to
+client configuration. See [skill destinations](#skill-destinations) for skill
+rollback limits. Agent configuration writes preserve unrelated entries and comments,
 create backups, stage changes in a private directory, and verify their result.
 Before publication, they refuse detected changes to the selected configuration.
 Replacement uses an explicit destination under the selected canonical parent;
@@ -85,6 +88,11 @@ Setup also retains valid environment overrides in REA's existing server entry,
 such as `REA_MCP_INPUT_SCHEMA_PROFILE`, `REA_MCP_OUTPUT_SCHEMA_PROFILE`, and
 `REA_MCP_MAX_RESPONSE_BYTES`.
 Detected provider settings replace only matching environment keys.
+Setup manages REA's launcher, selected provider settings, and supported timeout
+defaults. Client approval policies remain user choices, but the current Codex
+refresh drops those policies inside the REA entry; see the
+[Codex preservation limitation](client-configuration.md#codex-and-devin) before
+refreshing a customized registration.
 Setup and doctor report a malformed REA environment map or invalid runtime
 setting before setup writes files. Repair the named setting in the client
 configuration; setup does not silently discard the rest of the map.
@@ -162,6 +170,15 @@ paths as `unmanaged`, names the affected paths, and provides those alternatives;
 an unreadable skill identity remains `unknown`. Uninstall retains and reports
 files it cannot safely remove, including their ownership manifest.
 
+The skill installer backs up changed existing files and verifies the installed
+bytes. Its current rollback restores or removes files by pathname without
+checking that they are still the files published by that installation attempt.
+If another writer changes a skill file during a failed installation, rollback
+can overwrite that edit or remove a replacement first-install file
+([#5928](https://github.com/morluto/rea/issues/5928)). Avoid editing managed skill
+files or running another skill installer while setup is applying them. This
+limitation does not apply to the client-configuration rollback described above.
+
 `rea setup --skill-client claude_code --yes --json` refreshes and verifies the
 selected skill destination independently of MCP registration selection. The
 final `doctor.scope.skill_clients` records which skill destinations were

docs/javascript-application-workflows.md

@@ -412,8 +412,13 @@ when the object is an array element, nested inside mixed object/array
 containers, or assigned to a previously declared identifier. Saving the getter
 result in an alias does not make its old field values immutable. Known array
 indices include holes; an element after a spread has only a minimum possible
-index. Unrelated properties and known array prefixes remain precise, and a
-getter read without a write does not invalidate the receiver's fields.
+index. For these returned-reference writes, unrelated properties and known
+array prefixes remain precise. Getter invocation has separate effects: a
+property read can invoke a getter that mutates its receiver without any write
+through the returned value. Current analysis can miss these invocation effects
+and retain a stale receiver-field literal
+([#6669](https://github.com/morluto/rea/issues/6669)); absence of a later write
+does not establish getter purity.
 Nested callable returns are not assigned to their parent callable. Projected
 graph observations carry source ranges but never source text.
 

docs/javascript-artifact-reconstruction.md

@@ -642,6 +642,13 @@ execution and memory limits continue to determine examined coverage. Raising onl
 a node capacity does not raise the unknown capacity. Graphs without unknown
 omissions omit this optional coverage field, preserving their existing identities.
 
+These node and unknown capacities bound retained graph projection. Parsing,
+static analysis and semantic fact construction precede that projection for an
+admitted source. Lowering the capacities can reduce projection and retention
+work, but does not bound upstream semantic-analysis time or memory. Select fewer
+`source_paths` to reduce the sources analyzed; heap and deadline controls set
+separate resource failure boundaries with the runtime-specific limits above.
+
 While sources remain, the sequential worker reserves one next compact static
 checkpoint at its 8 MiB bound with the same 6x retention expansion used at
 admission. Earlier checkpoints are already charged to retained bytes; the

docs/mcp-contracts.md

@@ -1165,13 +1165,14 @@ block sizes and successor relationships. Text from different provider
 identities remains unknown.
 
 The `references` dimension preserves each edge's direction, endpoint identity
-and available kind facts. Within one artifact it compares exact raw endpoint
-coordinates, including the address space; hexadecimal case and zero padding
-do not change identity. Resolving an endpoint to a containing procedure does
-not replace the raw coordinate. Unparseable coordinates stay unknown.
+and available kind facts. When the subject digests match, the current comparator
+uses exact raw endpoint coordinates, including the address space; hexadecimal
+case and zero padding do not change identity. Resolving an endpoint to a
+containing procedure does not replace the raw coordinate. Unparseable
+coordinates stay unknown.
 
-Across artifacts, reference endpoints use stable procedure names. Missing or
-address-generated names remain unknown. A name observed at multiple procedure
+When the subject digests differ, reference endpoints use stable procedure names.
+Missing or address-generated names remain unknown. A name observed at multiple procedure
 entries retains its label constraint but cannot establish equal endpoints.
 Pairing preserves duplicate counts and considers alternative compatible
 pairings; array order never identifies an edge. Compatible records with
@@ -1179,6 +1180,20 @@ unknown endpoint identity or kind facts remain `unknown`. Independent known
 facts that contradict every possible pairing still establish `changed`.
 Source Evidence retains the original addresses, names and unavailable facts.
 
+Coordinate identity requires a common executable context: artifact identity,
+selected image or architecture slice, address space, and applicable load mapping.
+Equal coordinates in different slices of one container do not establish equal
+endpoints. The current digest-only selection does not enforce that context and
+can report references unchanged across distinct slices
+([#6502](https://github.com/morluto/rea/issues/6502)).
+
+The `calls` dimension separately compares direction and procedure names without
+retaining endpoint addresses. Distinct same-named procedures can therefore
+compare unchanged ([#6853](https://github.com/morluto/rea/issues/6853)). Check
+the source dossiers' endpoint identities before using either affected dimension
+as a reconstruction proof; another dimension reporting a change does not repair
+the selected dimension's false equality.
+
 ### Comparison input shapes
 
 `compare_web_captures` accepts exactly one of two input shapes:

docs/reconstruction-obligation-ledgers.md

@@ -17,6 +17,11 @@ input Evidence bundle. Contradictions, duplicate definitions or owners,
 residual unknowns, missing dependencies, and unavailable authority keep closure
 open or failed.
 
+Current proof qualification does not bind a passing record to the owner's
+implementation digest or obligation revision. Read the
+[proof applicability limitation](#proof-applicability) before relying on
+`verified` or `ready` after either changes.
+
 ## Complete CLI request
 
 This empty request is useful for checking client integration. It is valid and
@@ -225,11 +230,18 @@ sample Evidence ID with an authenticated review record already present in
 
 ## Manifest and closure
 
-A manifest binding names one owner and its exact implementation digest. Both
+A manifest binding names one owner and a caller-supplied `owner_sha256`. Both
 `original_cases` and the reconstruction fixture list must cover every
 `required_case_kinds` value with authenticated, comparable Evidence.
 `parser_type` is mandatory when `requires_parser_type` is true.
 
+The ledger does not read `module_path`, execute `verifier.command`, or compute
+the implementation digest. The owner fields do not specify whether the digest
+covers module bytes, a symbol representation, or a multi-file implementation.
+The proof producer must document the exact hashed inputs and any canonicalization
+so another verifier can reproduce that commitment; a path or symbol name alone
+does not define it.
+
 ```json
 {
   "obligation_id": "protocol.rpc.cancel",
@@ -322,6 +334,26 @@ A green unit test cannot close a `packaged-process` obligation. A static-only
 source cannot close a runtime or process claim. Marking a claim `blocked` or
 `out-of-scope` records the disposition but does not silently count it as verified.
 
+### Proof applicability
+
+Keep three checks separate:
+
+- **Authenticity:** the retained Evidence passes its integrity checks.
+- **Authority:** the observation has the kind and strength required by the claim.
+- **Applicability:** the proof describes the implementation and obligation
+  revision currently being evaluated.
+
+Current qualification checks authority, passing status and enumerated IDs, but
+does not compare proof identity with `owner_sha256` or `obligation_version`.
+Changing those fields while retaining old proof can therefore leave the result
+`verified` and `ready` ([#6854](https://github.com/morluto/rea/issues/6854)).
+Until that binding is enforced, clear the manifest binding's `verifier` after
+an implementation or requirement revision changes and replace stale fixture
+and verifier Evidence with proof for the new inputs. With `verifier: null`, the
+required obligation cannot be verified and carries `missing-verifier`; an
+authenticated old record alone does not establish applicability to the changed
+implementation.
+
 The `summary` counts obligations. `by_status`, `by_application_layer`, and
 `by_source_state` place each obligation in exactly one bucket.
 `by_evidence_authority` groups obligations by the Evidence `authority` of their
@@ -331,7 +363,9 @@ obligation's `source_state` do not affect its authority bucket.
 
 The tool returns every obligation inline. Its `ledger_id` and `closure_digest`
 identify the complete result, including summaries, reports, ownership and
-dependency graphs, Evidence links, and limitations.
+dependency graphs, Evidence links, and limitations. A new `closure_digest`
+identifies a changed ledger; it does not establish that a verifier ran again or
+that retained proof applies to the new owner or obligation revision.
 
 For named boundaries with explicit verifier contracts and package-proof kinds,
 see [reconstruction coverage](reconstruction-coverage.md).

docs/testing.md

@@ -277,6 +277,13 @@ distinct pair that would collapse if representation tags or scope were lost.
 For learned identifiers, cover conflicting pairs and reused values in different
 collections; mappings must remain one-to-one within their declared scope.
 
+For coverage propagation, compare the same returned rows under complete and
+incomplete examination. If a row exists on the left but is missing from a fully
+examined compatible right inventory, removal can be established. If the right
+side examined only eight of ten applicable records, or returns only one page,
+the same missing row remains unknown unless separate evidence proves absence.
+Assert the structured coverage and comparison status as well as the explanation.
+
 For format compatibility, identify the producer revision that establishes each
 rule. Include an accepted boundary case beside the rejected case so a stricter
 parser cannot pass by refusing both. Keep source-derived behavior, synthetic

docs/tool-design.md

@@ -203,6 +203,15 @@ completeness from examined records and exhaustiveness, rather than diagnostic
 prose or an empty failure list. Preserve observations independently of cleanup
 success.
 
+For example, if ten applicable records are discovered, eight are examined, and
+five are returned, the five returned records do not establish complete coverage
+of the ten. Keep discovered, applicable, examined, and retained scope distinct.
+A filtered page can be complete for its selection while the parent inventory
+remains partial. Carry the upstream coverage and unresolved reasons through
+filtering and paging; an item missing from that page is not proved absent from
+the target. Structured completeness and absence fields must agree with the
+stated limitations.
+
 Update canonical contracts, output schemas, examples, generated artifacts, and
 relevant docs together. Verify converted advertised schemas and success,
 malformed, unavailable, cancellation, and partial outcomes through affected

docs/user-visible-errors.csv

@@ -32,7 +32,7 @@ harm_rank,location,trigger,current_copy,user_risk,proposed_replacement,implement
 24.9,src/server/registerInvestigationTools.ts:call path unknown,Call-path workflow remains incomplete,Call path START_ADDRESS → GOAL_ADDRESS is STATUS,Persists binary addresses and internal status wording,Can the requested call path be established from complete analysis?,implemented,verified by focused unresolved call-path MCP test
 24.91,src/server/registerInvestigationTools.ts:static runtime unknown,Static/runtime correlation remains incomplete,Static/runtime correlation result EVIDENCE_ID is STATUS,Persists internal evidence identifier,Does runtime behavior match the available static analysis?,implemented,verified by focused unresolved static/runtime MCP test
 24.92,src/server/registerInvestigationTools.ts:reconstruction unknown,Reconstruction verification retains unknown claims,Reconstruction SPECIFICATION_HASH has unknown claims,Persists internal hash,Does the reconstruction satisfy every declared claim?,implemented,verified by focused unknown reconstruction MCP test
-24.93,src/server/registerFunctionComparisonTool.ts:probe rationale,Function comparison is incomplete,Capture complete dossiers with equal providers and analysis limits.,Exposes provider architecture and gives ambiguous equality guidance,"Capture complete dossiers for both functions under the same target context and analysis limits.",implemented,verified by focused function-comparison MCP test
+24.93,src/server/registerFunctionComparisonTool.ts:probe rationale,Function comparison is incomplete,Capture complete dossiers with equal providers and analysis limits.,Exposes provider architecture and gives ambiguous equality guidance,"Capture complete dossiers for both functions under the same target context.",implemented,Source and assertion inspected: tests/boundary/mcp/functionComparisonMcp.test.ts; test not rerun for this documentation change
 24.95,incur:CLI argument validation,Caller omits or mistypes a command argument,VALIDATION_ERROR with raw Zod Details and fieldErrors including code/path/expected/received,Exposes validator representation and buries the useful correction,"REA could not read the command arguments. Check the named argument and its expected type, then try again.",implemented,verified by sanitizer unit tests and real dispatcher missing-argument test
 25,src/application/ReferenceSourceImport.ts:cancelled,Reference-source import is cancelled,Reference source import cancelled,No recovery timing guidance,"Reference source import was cancelled. Start it again when ready.",implemented,focused assertions passed
 26,src/application/ReferenceSourceImportPolicy.ts:invalid-limits,Configured import limits are not positive integers,Import limits must be positive integers,Fixed importer ceilings prevented full source imports,"Removed fixed byte, entry, depth, and path limits.",removed,verified by greater-than-10000 entry and greater-than-16-MiB regressions
@@ -71,10 +71,10 @@ harm_rank,location,trigger,current_copy,user_risk,proposed_replacement,implement
 58,src/application/SetupHost.ts:unsupported Node,Runtime version cannot run setup,"Install Node.js 22.x (>=22.23.4), 24.x (>=24.22.1), or 26.12.1+ and rerun setup.",Low risk; exact dependency and retry,Keep current copy,unchanged,verified by setup host tests
 59,src/application/SetupPlan.ts:unsupported macOS,"macOS version is missing, unparseable, or older than 12",Upgrade to macOS 12 or newer.,Low risk; exact support floor,Keep current copy,unchanged,verified by setup unit test
 60,src/application/SetupPlan.ts:unsupported Linux,Linux distribution is outside supported set,"Automated Hopper setup requires an x86_64 host running Ubuntu 24.04+, Fedora 41+, Nobara 44+, Arch Linux, CachyOS, or Omarchy; configure an existing supported provider instead.",Low risk; exact supported alternatives,Keep current copy,unchanged,verified by setup unit test
-61,src/application/process/ProcessCli.ts:readJson read,Process scenario or evidence file cannot be read,Raw filesystem exception through CLI framework,Can expose local paths/codes and no recovery,"Process input file could not be read. Check that the path exists and is readable.",implemented,verified by focused CLI test
+61,src/application/process/ProcessCli.ts:readJson read,Process scenario or evidence path is missing or is not a regular file,Raw filesystem exception through CLI framework,Lacks actionable recovery; preserve caller-selected paths and filesystem failure details,"Process input file could not be read: {path} ({detail}). Check the reported filesystem constraint and retry.",implemented,Source and missing-path assertion inspected: tests/boundary/filesystem/processCliFileInput.test.ts; test not rerun for this documentation change
 62,src/application/JsonInputFile.ts:memory admission,Projected process JSON value exceeds available heap headroom,Insufficient heap headroom to materialize the complete JSON value,Heap admission depends on live runtime capacity rather than a fixed 64 MiB file limit,"Provide a smaller valid JSON value. For Evidence workflows, re-analyze a smaller selection of the original target and use its complete Evidence; splitting JSON text or trimming Evidence fields does not produce valid workflow input.",implemented,Source verified against shared JSON reader and recovery constant; former fixed-size refusal is superseded
-63,src/application/process/ProcessCli.ts:readJson parse,Process scenario or evidence file is malformed JSON,Raw JSON parser exception through CLI framework,Can expose parser implementation and lacks recovery,"Process input file is not valid JSON. Repair the file, then try again.",implemented,verified by focused CLI test
-64,src/application/process/ProcessCli.ts:capture scenario parse,Scenario fails Process Capture schema,Raw Zod validation exception through CLI framework,Exposes schema internals and field paths without stable recovery,"Process scenario is invalid. Check its required fields and limits, then try again.",implemented,verified by focused CLI test
+63,src/application/process/ProcessCli.ts:readJson parse,Process scenario or evidence file is malformed JSON or invalid UTF-8,Raw JSON parser exception through CLI framework,Lacks actionable recovery; preserve the selected path and failure detail,"Process input file is not valid UTF-8 JSON: {path} ({detail}). Repair the file, then try again.",implemented,Source and malformed-JSON/UTF-8 assertions inspected: tests/boundary/filesystem/processCliFileInput.test.ts; test not rerun for this documentation change
+64,src/application/process/ProcessCli.ts:capture scenario parse,Scenario fails Process Capture schema,Raw Zod validation exception through CLI framework,Unstructured schema details obscure actionable field errors,"Analysis input is invalid. Check the arguments and try again.",implemented,Source and scenario-validation assertion inspected: tests/boundary/filesystem/processCliFileInput.test.ts; structured issues retain field paths; test not rerun for this documentation change
 66,src/application/process/ProcessCli.ts:wrong evidence,Comparison receives valid Evidence from another workflow,Expected REA process capture Evidence,Uses internal schema name and does not explain recovery,"Capture evidence is not from the current process-capture workflow. Create new capture evidence, then try again.",implemented,verified by focused CLI test
 67,src/application/process/ProcessCli.ts:unexpected,Unexpected parser/comparison/canonicalization failure escapes expected classifications,Raw thrown exception through CLI framework,Can expose stack or internal invariant,"Message keeps the sanitized cause. Remediation: Do not repeat this command. Tell the user the process command could not complete and ask them to check the input files, then run `rea doctor`.",implemented,verified by direct unexpected-cause projection test
 68,src/server/registerEvidenceTools.ts:object guard,Validated provider-tool input is unexpectedly not an object,Provider tool input was not an object,Exposes provider architecture and implies caller can fix impossible state,Remove the impossible duplicate guard and parse through the declared JSON-object schema.,removed,verified by typecheck and MCP integration tests