# INVARIANTS — the guarantees and where they hold

> Each invariant: the statement as the code actually implements it, where it is
> **established** (written), and where it is **checked** (verified). Symbols are greppable
> and CI-verified. ADRs in `docs/adr/` carry the rationale.

## I1 — segment_hash binding

```
segment_hash = BLAKE3( header_hash ‖ record_hash ‖ toc_payload_hash )
  where header_hash      = blake3(canonical header bytes)
        record_hash      = blake3(record area)
        toc_payload_hash = compute_toc_payload_hash(toc_payload)
```

Concatenation order is exactly header → record → toc_payload (verified against source).

- **established:** `corecrux-segment/src/sealer.rs` (`seal_segment_v1_from_record_area`) and
  the mirror in `corecrux-segment/src/builder.rs` (`build_segment_v1`) — stored into
  `SegmentFooterV1.segment_hash`.
- **checked:** `corecrux-segment/src/decoder.rs` (`decode_segment_v1`, re-derives all four
  hashes; `SegmentError::CrcMismatch` on divergence) and
  `corecrux-storage/src/integrity.rs` (`verify_segment_hashes_all`, used by
  `corecruxctl verify-store --strict`).

## I2 — segment chain

```
seal(N).previous_segment_hash == seal(N-1).segment_hash   (within a shard)
seal(0).previous_segment_hash == None                     (first segment)
```

- **established:** `corecrux-storage/src/lib.rs` (`SegmentSealMaterialV1`, fields
  `segment_hash` / `previous_segment_seq` / `previous_segment_hash`) — populated on the
  append/seal path (`corecrux-storage/src/append.rs`), which links each seal to the
  highest-seq prior segment in the same shard. The receipt is signed by
  `sign_segment_seal_material` (`corecruxd/src/grpc.rs`).
- **checked:** `corecrux-storage/src/tests.rs`
  (`append_batch_seal_receipt_links_previous_segment_hash`); the `verify-store --strict`
  chain walk; `build_segment_seal_receipt` gates on both previous-link fields being present.

## I3 — fail-closed verification

```
report.ok  ⟺  canonical_hash_match && signature_valid && content_hash_match
```

A verification report is `ok` only if **all** component checks pass. A non-Ed25519
signature path yields `signature_valid = false` (fail-closed), not a skipped check.

- **enforced:** `corecrux-receipts/src/c2pa_manifest_v1.rs` (`verify_c2pa_manifest_v1`,
  report `C2paVerificationReportV1`). The same boolean-AND shape recurs in the MCP verify
  tools (`crux-mcp/src/tools/receipt_verify.rs`, `observations.rs`) and
  `corecruxctl/src/c2pa_x509.rs` (adds `&& chain_pass`).

## I4 — monotonic fact versioning

```
A new value for (entity, key) gets version = prev.version + 1, supersedes = prev.fact_id;
the predecessor is marked superseded_by (not deleted) and remains in history.
First version = 1.
```

- **established:** `corecrux-memory/src/fact_store.rs` — `build_fact` assigns the monotonic
  version + `supersedes` link; `store` → `supersede_prior_version` → `mark_superseded`
  flips the predecessor's `superseded_by` marker (journaled for restart survival). Both
  rows are retained in the store.
- **checked / observed:** recall filters on `superseded_by.is_none()` by default
  (`crux-mcp/src/tools/facts.rs`); `include_superseded=true` / `memory_view` expose the
  full chain. Tests: `store_same_key_auto_supersedes_prior_version_in_recall`,
  `auto_supersede_survives_replay`, `consolidate_facts_v1_supersedes_targets_without_deleting_history`.

## I5 — external witness anchoring

```
external_anchor_body commits to (field set includes): receipt_id, tenant_id, anchor_id,
actor_passport, transparency_log, log_url, leaf_hash, log_index, tree_size, root_hash,
and the RFC-6962 inclusion proof
```

An anchored CROWN chain head is bound to an external transparency-log entry: the inclusion
proof must verify leaf → root, and the anchor body commits to the proof, so neither can be
swapped independently.

- **established:** `corecrux-receipts/src/witness_v1.rs` (`build_external_anchor_body_v1`).
- **checked:** `verify_rfc6962_inclusion_proof_v1`; tests
  `rfc6962_inclusion_proof_verifies_two_leaf_tree`,
  `external_anchor_body_binds_inclusion_proof`, and the RFC-3161 variant
  `rfc3161_timestamp_body_binds_token_hash_and_imprint`.

## I6 — custody-proof export

An exported context bundle (facts + sessions + signed journal + receipt refs) is
passport-signed; verification is offline and fail-closed — any tampered component or signed
field fails the check.

- **established:** `corecruxctl/src/export.rs` (`run_context_export`).
- **checked:** `run_context_verify` (offline, no network); tests
  `context_export_round_trips_and_is_a_signed_custody_proof`,
  `tampered_component_fails_verification`, `tampered_signed_field_fails_signature`.
  The export → offline-verify → tamper-rejection cycle is a release-blocking CI gate.

## I7 — an absent signal is never a pass

```
value(check could not run)  ≠  value(check ran and passed)
```

A check that **could not be evaluated** must never return the value of a check that ran
and succeeded. This is the single most-repeated defect in this codebase: a two-round
coverage sweep in July 2026 found 28 pre-existing defects, and **19 of them were this one
bug** (ExecPlan `crux-pinned-defect-remediation-2026-07-31`). It reappears because the
lossy form is always the shorter one to write — `.unwrap_or(true)`, `is_none_or(...)`,
`.ok()`, an early `return Ok(())`, or simply not emitting the check at all.

Three sanctioned shapes, in order of preference:

1. **Add an explicit skipped state** — `checks_skipped: Vec<String>` on the report,
   listing checks that were *requested but not evaluable*. `ok` keeps its meaning, so an
   operator who deliberately verifies without an input is not broken; a caller that needs
   every requested check to have actually run gates on `ok && checks_skipped.is_empty()`.
   This is the house idiom. Use it wherever an operator could reasonably have omitted the
   input.
2. **Fail closed** — return an error. Correct only when the absent signal has *no*
   legitimate cause (a truncated log, an empty sample where the neighbouring call already
   hard-errors, a pagination field the protocol requires).
3. **Reconcile sent against acknowledged** — where a count exists on both sides, compare
   them rather than copying one across.

Two rules keep the mechanism honest:

- **Absent ≠ skipped.** An input class that is *wholly absent* means the caller never
  asked for that check; it must NOT be listed. A `checks_skipped` that is non-empty on
  every ordinary run is useless as a gate. Every fix in the ExecPlan above ships with a
  control test asserting the absent-input case is not flagged.
- **Only what the operator configured.** Tightening a check must not start requiring an
  input the operator never opted into — see `verify_jwt_hs256`, where `iss`/`aud` become
  required *only* when they are pinned.

- **established:** `checks_skipped` on `EvidenceVerifyReportV1`, `ControlVerifyReportV1`
  and `SnapshotVerifyReport` (`corecruxctl/src/evidence.rs`, `snapshot.rs`);
  `X509VerifyReport::checks_skipped` (`corecruxctl/src/c2pa_x509.rs`, the originating
  precedent — commit `5dd75fc`, `incident:2026-07-28`);
  `ScanDiagnostics::parse_failures` (`corecruxd/src/workspace_scan.rs`) for the scanner
  form; `AuthMode::parse` and `required_spec_claims` (`corecruxd/src/auth.rs`) for the
  fail-closed form.
- **checked:** the pin-inversion tests named in the ExecPlan's milestones, each paired
  with an absent-input control.

**Review checklist item.** On any verification, scan, or auth path, treat these as
requiring a written justification in review: `unwrap_or(true)`, `is_none_or(...)`,
`.ok()` discarding an error, `.filter(|_| …exists())`, an early `return Ok(())` on
missing input, and a check that is simply not pushed when its input is absent. A clippy
lint was considered and **rejected** as too blunt: every one of these is correct in the
majority of its uses (`is_none_or` on an optional filter bound, `.ok()` on a
best-effort log write), so a lint would train reviewers to `#[allow]` it rather than
read it. The signal is the *path*, not the combinator.

---

*The I1–I4 formulas are quoted from current source (the audit's guessed forms for I1 and I3
matched the implementation verbatim; I2/I4 field names confirmed exact). I5–I6 statements are
derived from the named builders/verifiers and their proving tests, not quoted formulas. I7 is
a codified defect class, not a code-derived formula.*