proof(verifier-spec): ADR-0005 — MkTrustedFixture audit boundary (closes #103)

[hyperpolymath]

Summary

Closes #103 by taking path (3) from the issue's three closure paths — an explicit ADR pinning MkTrustedFixture as the formal audit boundary for VerifierAccepts / SourceAccepts.

PR #79 (06ec00e) landed TOTAL bodies for VerifierSpecAgreement and SourceVerifierAgreement. What remained per #103: the trust-injection moment (every VADifferential / SADifferential ultimately routes through MkTrustedFixture) needed a load-bearing, named, cross-referenced specification rather than an inline docstring.

What lands

docs/decisions/0005-trustedfixture-audit-boundary.adoc (new ADR, Accepted)

Pins three inspection invariants every MkTrustedFixture m construction site is audited against:

• I1 Provenance — (trustedFixtureName, trustedFixtureId) must correspond to an existing row in crates/typed-wasm-verify/tests/cross_compat.rs.
• I2 Witness fidelity — trustedWitness : FunctionsAccepted m.functions must be the structural witness the harness's ACCEPT verdict establishes; rejected fixtures yield no MkTrustedFixture.
• I3 Module shape — the indexing ModuleSummary must mirror the harness's ModuleSummary reconstruction for the same fixture bytes (function order + decoded ownership intents).

Also names the supersession path: a future WasmCert-Isabelle tie-back (issue #103 path 1) or constructive Rust-verifier soundness (issue #103 path 2) would each ship as a fresh ADR superseding 0005 by collapsing the audit boundary into a constructive proof.

docs/decisions/README.adoc

Index row for ADR-0005 + 1-line owner-line header normalisation (hook compliance).

src/abi/TypedWasm/ABI/VerifierSpec.idr

6-line docstring addition near MkTrustedFixture cross-referencing ADR-0005 so a reader landing on the record's definition can find the invariants without rediscovering them. Single grep point for trust injections preserved: `git grep MkTrustedFixture`. Same 1-line owner-line normalisation as #152's Epistemic.idr (parenthetical removal only; no licence change, no SPDX change; owner-approved via AskUserQuestion mid-session).

PROOF-NEEDS.md

New RECONCILIATION 2026-06-02 banner recording the closure with the I1/I2/I3 summary and the supersession note. Matches the convention of the prior RECONCILIATION 2026-05-27 (post-A10 items 7 + 8 bodies closed) banner. Same 3-line owner-line header normalisation already landed on #153's branch.

Stacking

This PR is stacked on #152 (proof/epistemic-fresh-pin-102) — base set accordingly. Reason: #152 contains the HEAD build fix for composeWitnessLegacyAgree; #103's docstring edit on VerifierSpec.idr requires a clean package build to land. The incremental diff (visible here) is only the ADR + cross-references — 4 files / +351 lines / -2 lines.

When #152 merges, this PR will rebase forward to main and be a 1-commit fast-forward.

What this is not

• Not a constructive proof of Rust-verifier soundness. The Rust verifier remains the trusted base for the differential path; ADR-0005 pins the audit story for that trust, not its discharge.
• Not a change to any Idris2 type. PR proof: total bodies for VerifierSpecAgreement + SourceVerifierAgreement (items 7 + 8) #79's record shape remains canonical.
• Not a gate on the structural path. VAStructural and SAStructural continue to inject zero trust.

Test plan

• src/abi/TypedWasm/ABI/VerifierSpec.idr type-checks rc=0 in isolation (idris2 --check).
• Whole-package build rc=0, 22/22 modules, 0 errors (only pre-existing shadowing warnings).
• No believe_me / assert_total / postulate / sorry / assert_smaller introduced.
• %default total preserved across the arc.
• No SPDX-License-Identifier line changed in any file. Owner-attribution normalisation only on files where the pre-commit hook required it (parenthetical removal — same micro-pattern as proof(epistemic): pin Fresh to FieldVersion (A14, closes #102) + composeWitness fix #152's Epistemic.idr and docs(proof-needs): 2026-06-02 reconciliation — five silent P0/P1 closures + A14 (#102) #153's PROOF-NEEDS.md).
• CI green on stacked head.

Cross-references

• Closes Proof bodies for VerifierSpecAgreement / SourceVerifierAgreement (statements landed in #79; bodies are long-tail) #103.
• Refs proof: total bodies for VerifierSpecAgreement + SourceVerifierAgreement (items 7 + 8) #79 — statement-level landing of agreement records (commit 06ec00e).
• Refs proof: items 7+8 — design pass + first concrete structural agreement witnesses (stacked on #72) #74 — superseded alternative design (RegisteredFixture GADT + Maybe-returning bridges); composable add-on if a fixture-table module is ever wanted.
• Refs Epistemic.idr: Fresh and ExplicitSync constructors lack FieldVersion pinning (residual gap after A11) #102, proof(epistemic): pin Fresh to FieldVersion (A14, closes #102) + composeWitness fix #152, docs(proof-needs): 2026-06-02 reconciliation — five silent P0/P1 closures + A14 (#102) #153 — companion proof work in flight (this PR stacks on proof(epistemic): pin Fresh to FieldVersion (A14, closes #102) + composeWitness fix #152).

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 108 issues detected

Severity	Count
🔴 Critical	1
🟠 High	6
🟡 Medium	101

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in c5-regenerate.yml",
    "type": "missing_timeout_minutes",
    "file": "c5-regenerate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "missing_timeout_minutes",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in dogfood-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "dogfood-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in e2e.yml",
    "type": "missing_timeout_minutes",
    "file": "e2e.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence