Runpack v6 and Offline Verification Architecture

Authority relation

For one accepted checkpoint H, the backend-neutral export authority exposes a coherent immutable prefix:

E_H = Export(AcceptedAuthority[<= H], Law, Retention, RunpackV6)

CurrentState(H)
    = Replay(AcceptedHistory[<= H])
    = Reconstruct(E_H)

decision-gate-core owns the accepted-run audit-export interface and sealed checkpoint/page projections. The in-memory and SQLite authorities implement that same relation. decision-gate-runpack owns format-v6 construction, nominal identities, deterministic object trees, and the immutable local repository. decision-gate-verifier owns the independent supplied-material reducer and exact claim report. MCP and CLI only compose these authorities.

Runpack-v6 subject

The manifest binds the format/canonicalization version, accepted authority domain, exact RunKey, scenario-law and Xarxa graph identities, accepted head, effective limit profiles, fixed tree parameters, and the roots of all twelve mandatory artifact families. Empty histories use a canonical empty-family root; family omission is not another spelling of empty.

The twelve families are scenario source, validated scenario law, effective profiles, run-allocation tombstone membership, creation receipt, accepted current state, accepted mutation records, accepted operation receipts, stage-open records, evaluation-attempt records, submission records, and committed intent records.

Objects are bounded canonical JSON. Leaves contain no more than 256 records or 32 MiB, index fanout is no more than 256, tree depth is no more than eight, and the manifest is no more than 256 KiB. Object identity binds format, artifact family, object kind, key/ordinal range, and canonical bytes. Manifest identity binds the complete manifest subject under the dg/runpack/v6 domain. Builders stream in bounded memory; representability is not defined by one monolithic bundle-size limit.

Runpack v5 and every older format reject at hostile rehydration. SQLite schema 11 is the only current local durable schema; schema 10 and older reject without migration or compatibility parsing.

Backend-neutral export

An export begins by capturing an AcceptedRunAuditCheckpoint. Every subsequent bounded page is tied to that checkpoint and may contain no record after its accepted head. Later accepted mutations therefore cannot change the exported subject. Page construction derives the continuation cursor from strictly ascending revision-bound rows; callers cannot independently assert a cursor, an after-checkpoint row, or an over-limit page. Attempt, submission, and intent projections retain their owning accepted revision, and intent families retain and revalidate the owning accepted-record identity. Memory captures the checkpoint while holding the run-cell authority; SQLite captures it transactionally and streams indexed immutable rows without holding a history-length transaction.

Normal export work is bounded by page, leaf, and index fanout. The status and mutation hot paths do not replay full history. A backend is not qualified by implementing the trait alone; it must pass the shared accepted-run and audit- export conformance suites for its declared durability profile.

Publication authority

The only supported OSS repository is local and capability-rooted. An operator admits one ambient root through platform_filesystem_authority::ExplicitAmbientAuthority; semantic and MCP code receive sealed relative targets, never arbitrary trusted paths.

Objects are published with create-new semantics. Existing objects are reused only after exact byte verification. The manifest is published last, so orphan objects do not make a runpack visible. Publication returns the closed knowledge family Published, AlreadyPresentExact, Conflict, Unavailable, Indeterminate, or IntegrityFailure.

There is no overwrite, deletion, caller-selected object key, arbitrary manifest name, network fetch, S3/object-store runtime, or generic resolver in the initial OSS profile. The secure local-filesystem claim is Linux-only, following the platform filesystem authority. Remote immutable publication is a deferred, independently specified DG-E/PF-08 capability.

Supplied-material verification

Verification consumes a complete in-memory bundle or an explicitly supplied local capability root, plus optional explicitly supplied supplemental bytes whose kind, digest, bound, and owning relation are validated. The verifier has no network, provider, MCP, SQLite, clock, ambient path, or runtime-acquisition dependency. A locator is not material; missing material yields an exact Unavailable claim and never triggers retrieval.

The supplemental-material boundary is presently a verifier-library seam, not a generic CLI directory option. Digest-bound bytes establish only content integrity. Until an external authority family owns a constructor that validates the exact witness syntax and relation, those bytes cannot satisfy authenticity, currentness, rollback, dispatch, deployment, or build-provenance claims. The CLI therefore does not expose a misleading --material-root argument.

The independent reducer does not trust the stored current state or call the production mutation finalizer. The verifier first completes the independent bounded object-tree integrity procedure for all twelve families; semantic malformation therefore cannot mask or reclassify the structural-integrity claim. It then reconstructs accepted history from canonical records and checks head/predecessor continuity, receipt and operation-family ownership, stage-open/attempt/submission indexes, intent ownership, acceptance-time stability, and equality with the stored current projection. It reuses RET, Xarxa, typed observation admission, and pure evaluation as named trusted mathematical bases rather than duplicating their laws.

MCP verification performs tool authorization, reads only the bounded canonical manifest to resolve the exact namespace, completes namespace authorization, and only then permits object-tree traversal and semantic replay. Unauthorized callers cannot spend the full verification budget or probe object availability.

The closed claim registry contains 29 dependency-ordered claims. Every report contains every registry row with one of Satisfied, Disproved, Unavailable, NotRequested, NotApplicable, Indeterminate, or VerifierFailure. Profiles select requested rows; they never collapse the report into an authoritative boolean. Dependency failure prevents a downstream positive result.

The default CompleteOfflineReplayV1 profile decides everything supported by the supplied material. Source authenticity, currentness, coherent rollback resistance, dispatch/effect recovery, deployment qualification, and external build provenance remain unavailable unless a separately qualified exact witness is supplied. PF-05 implements no signing authority and never converts digest consistency into authenticity.

Current evidence and nonclaims

Focused evidence covers canonical identity known-answer behavior, hostile manifest/object reconstruction, deterministic multi-level trees, local repository symlink and retained-byte substitution, exact budget exhaustion, claim dependency propagation, cryptographically self-consistent history/index/ current-state mutations, partial-publication failure, page-constructor falsification, verifier dependency exclusion, memory/SQLite export parity, and current outward-contract generation. Filesystem-authority failures other than proved absence are classified as integrity failures rather than ordinary material unavailability. The registered golden_runpack_cross_os proof reconstructs one deterministic in-memory accepted subject, performs supplied-material offline verification, and checks its exact canonical runpack-v6 identity through the generated proof catalog. The Kani harnesses for fixed-width decoding and checked tree/count arithmetic are present, but no DG Kani execution result is yet claimed. The repository already separates its production Rust 1.96 workspace from an isolated Kani 0.67.0 proof workspace generated for Kani’s bundled Rust 1.93 toolchain. The remaining PF-05 obligation is a DG-owned manifest/profile under that same materialized runner, complete harness enumeration, execution, and immutable result retention; the toolchain-version difference is not a blocker.

The golden proof has passed on the local Linux evidence path. The checked-in Ubuntu/Windows matrix has not yet produced an observed Windows result for this candidate, so cross-OS qualification remains open. The present SQLite 1/1,000/100,000 history diagnostics likewise do not close million-record streaming, peak-memory, or calibrated product-runner qualification.

PF-05 does not prove source truth, current authority, rollback protection, external effects, deployment isolation, remote repository correctness, or release readiness. Those remain exact later-profile claims.