Proof Diagnostic Evidence Spine

proof_diagnostic_evidence_spine sits before formal proof work and recomputes which earlier diagnostic records may count as evidence, writing a board of accepted and rejected checks with reasons. proof_diagnostic_evidence_spine is the component that sits one step before formal proof work and decides which diagnostic records are allowed to count as evidence. It reads the records left by earlier formal-math evaluation and premise-retrieval steps, recomputes whether each one actually holds, and writes a board that lists which checks were accepted, which were rejected, and why.

Rather than trust a row's self-declared pass, it resolves and re-hashes the named files and opens the cited result records, so a pass means evidence is present and coupled, not correct mathematics. It exists because a diagnostic record can lie by omission. A check row can name a real failure-taxonomy report and a real result record, declare itself passing, and be believed on its own word. This component does not trust that word. It resolves the files the row names, re-hashes them, opens the result records the row cites, and only then decides. A pass here means the named evidence is present and coupled. It does not mean the underlying mathematics is correct.

metadata-only diagnostic evidence records

The output is a metadata-only record set carrying no proof or provider-output body, because the component judges and arranges existing records rather than running a proof checker itself. The result is a metadata-only set of records: proof-evidence checks, a model-output data policy result, a diagnostic board, and a fixture sign-off record. None of them carry a proof body or a provider output body. The component arranges and judges existing records. It never runs a proof checker itself.

Purpose

Evidence inflation is cheap to write: trusting a row's own expected_result label would let a drifted digest, an unrelated result record, or a mislabelled check pass silently. The problem is evidence inflation. A row that says "this check passed" is cheap to write and expensive to trust. If the spine accepted the row's own expected_result label, a drifted digest, a result record that never mentions the ref it claims, or a check labelled as failure-taxonomy evidence while pointing at an unrelated file would all pass silently.

Rederiving the verdict, not reading labels

The component asks per row whether the check recomputes against the system it names, ignoring the fixture's pass label because the label is the thing under suspicion. The component answers one question per row: does this check recompute against the system it names, or is it asserting more than its refs support. A loose gate that reads labels fails because the label is the thing under suspicion. The spine ignores the fixture's pass label and rederives the verdict.

How it works

Two entry points and the shared pipeline

run drives the base fixture and run_evidence_bundle the exported bundle with added artifact checks, both scanning inputs, running the validators in order, and merging observed negative cases before writing records. The runtime is src/microcosm_core/organs/proof_diagnostic_evidence_spine.py. Two entry points drive it. run handles the base fixture. run_evidence_bundle handles the exported evidence bundle and adds copied-artifact and source-body checks. Both load their inputs, run a secret-exclusion scan over them, call the validators below in order, merge the negative cases each validator observed, then write the records.

The per-check verdict in _classify_evidence_check

_classify_evidence_check resolves and re-hashes each source ref, confirms every cited result record truly references it, applies a semantic floor, and accepts only when all of that holds with no negative code declared. The core of a per-check verdict is _classify_evidence_check. For each source_ref on a check row it resolves a real public file with _resolve_public_ref, hashes the bytes with _sha256_file, and compares that hash to the expected digest the module holds in SOURCE_DIGESTS. It opens each result record anchor and confirms the result record payload actually contains the source ref and its digest, so a check is result record-backed only when the result record it cites genuinely references it. On top of that it applies a semantic floor through _check_semantic_floor: a check whose id mentions failure_taxonomy must resolve to a source carrying a failure-taxonomy report and a result record carrying a failure-mode ledger; a graph_update check needs graph-update candidates with ids and a matching anchor. The row is accepted only when every source resolves, every digest matches, every cited result record backs the ref, the semantic floor is satisfied, and no expected-negative error code is declared.

Running the classifier over every check

validate_evidence_receipts runs the classifier over every check, stamps any self-declared pass label as non-authoritative, and reports its own verdict as accepted ids or a recompute-failed finding. validate_evidence_receipts runs that classifier over every check. It records legacy_expected_result_label_present and stamps any such label as ignored_non_authoritative_fixture_label, then reports the verdict it computed itself. Accepted checks land in accepted_check_ids, rejected ones become an EVIDENCE_RECEIPT_ANCHOR_RECOMPUTE_FAILED finding with its rejection reasons.

Advisory metadata kept, authority denied

validate_provider_payload_policy rejects any provider or oracle row carrying a forbidden body key or claiming oracle authority, while a clean row keeps its advisory metadata under a one-sided retain-metadata, deny-authority rule. validate_provider_payload_policy handles provider and oracle advisory rows. It walks each payload with _forbidden_body_key_paths looking for any key in FORBIDDEN_BODY_KEYS, a fixed list that includes proof_body, ground_truth_proof, provider_output_body, oracle_payload_body, and prompt. A row with a forbidden key, or one that claims oracle authority, is rejected and kept as a regression fixture. A clean row keeps its advisory metadata and is marked advisory_metadata_preserved. The rule is one-sided: metadata is retained, authority is denied.

Rejecting authority upgrades, keeping stale coupling

validate_authority_ceiling rejects a board's source-authority and a check's runtime-correctness upgrades, while validate_stale_source_coupling keeps a drifted fingerprint as evidence and marks it stale. validate_authority_ceiling rejects two upgrade attempts. A diagnostic board that sets claims_source_authority produces DIAGNOSTIC_BOARD_AUTHORITY_UPGRADE. A passing check that sets claims_runtime_correctness produces EVIDENCE_PASS_OVERCLAIMS_RUNTIME_CORRECTNESS. validate_stale_source_coupling keeps a drifted fingerprint as evidence rather than dropping it, emitting PROOF_RECEIPT_SOURCE_COUPLING_STALE and setting source_fingerprint_status to stale.

Digest-checking the copied Ring2 artifacts

On the bundle path, validate_copied_macro_body_artifacts re-hashes each copied Ring2 artifact and passes only when all thirteen targets are present and digest-matched, blocking on any mismatch. On the bundle path, validate_copied_macro_body_artifacts re-hashes each copied Ring2 runtime artifact against PUBLIC_RING2_ARTIFACT_IMPORTS. It passes only when all thirteen expected targets are declared, present, and digest-matched under either the exact-copy or the source-faithful public-light-edit policy. Any missing file or digest mismatch blocks the status.

flowchart TD Check["Check row source_refs, receipt_anchor_refs, source_digest_refs"] Resolve["Resolve each source ref re-hash file (sha256)"] Result record["Open result record anchor does it contain this ref and digest?"] Floor["Semantic floor failure-taxonomy / graph-update source and result record match"] Accept["Accepted verdict recomputed"] Reject["Rejected, kept as diagnostic evidence"] Board["diagnostic board evidence accounting only"] Check --> Resolve --> Result record --> Floor Floor -->|all agree| Accept Floor -->|any mismatch| Reject Accept --> Board Reject --> Board

Negative cases

Six negative inputs the run must observe

The fixture declares six negative inputs the run must observe, each mapped to its error codes, and the run blocks if any is missing. The fixture declares the negative cases the run must observe, listed in EXPECTED_NEGATIVE_CASES. A run is blocked if any of them is missing:

• provider_proof_body_payload_rejected: a model-output data carrying a forbidden proof body, giving FORBIDDEN_PROOF_BODY and PROVIDER_PAYLOAD_NOT_AUTHORITY.
• oracle_payload_claims_authority_rejected: an oracle payload claiming authority, giving ORACLE_PAYLOAD_BODY_FORBIDDEN and ORACLE_PAYLOAD_NOT_AUTHORITY.
• evidence_receipt_missing_required_fields: a result record lacking a validator id or scope boundary, giving MISSING_VALIDATOR_ID and MISSING_RECEIPT_ANTI_CLAIM.
• diagnostic_board_claims_source_authority: giving DIAGNOSTIC_BOARD_AUTHORITY_UPGRADE.
• stale_proof_receipt_source_coupling: a drifted source fingerprint, giving PROOF_RECEIPT_SOURCE_COUPLING_STALE.
• passing_check_overclaims_runtime_correctness: giving EVIDENCE_PASS_OVERCLAIMS_RUNTIME_CORRECTNESS.

Prior Art Grounding

Assurance cases and provenance discipline

The component follows assurance-case practice, tying evidence to a claim and its limits, and borrows result record discipline from GSN, W3C PROV, and observability, treating a diagnostic as an evidence cell rather than a proof. The component follows assurance-case practice: evidence is tied to a claim, its assumptions, and its limits before it is treated as support. NASA's Goal Structuring Notation example for spacecraft assurance frames assurance as model-structured evidence rather than document-level persuasion, NTRS 20160005295. The result record discipline also borrows from W3C PROV and from observability practice, where a diagnostic artifact is an evidence cell with provenance and not a proof of correctness.

Validation Result record Path

Fixture and bundle validation commands

Run these from the repository root. Neither command mutates a durable record or a generated projection: Run these from the repository root. Neither command mutates a durable record or a generated projection:

./repo-pytest tests/test_proof_diagnostic_evidence_spine.py -q --basetemp=/tmp/microcosm_proof_diagnostic_evidence_spine_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

What a pass means

Clearing this validation shows the fixture's expected refusals all fired, but proves nothing about the underlying mathematics or any provider's authority. A pass means the observed negative cases match EXPECTED_NEGATIVE_CASES. It does not establish formal-result correctness or provider authority.