Skip to content

Bind format 3 integrity to charged streaming spans and explicit identity domains - #84

Draft
afflom wants to merge 6 commits into
v01/owned-wire-emitterfrom
v01/integrity-format3
Draft

afflom wants to merge 6 commits into
v01/owned-wire-emitterfrom
v01/integrity-format3

Conversation

@afflom

@afflom afflom commented Nov 4, 2026 •

Copy link
Copy Markdown
Member

Format 3/machine 1 now selects the distinct STREAM-MAX-v1 integrity construction through a typed charged-span adapter. Format 2/CHAIN-v1 meanings remain unchanged. Nonempty producer spans transfer one owned image ticket through consumption or cancellation; finalization reserves the 32-byte output before component completion and publishes one owned digest ticket. Input, ordered-basis and checkpoint purposes have explicit profile-specific domains. No mandatory certification metadata is added to ordinary archives.

The source includes checked runtime preimage fences, fixed six-byte archive-prefix validation across arbitrary partitions, digest comparison, exact root aggregates, nine helper refinement lemmas and two ownership boundary lemmas. Collision candidates remain untrusted until successful SHA computations independently validate them; no SHA injectivity or reduction-completeness claim is made. Core/search continue to own the shared canonical semantic cost profile and refinement.

Validation: 20 independent identity fixtures, 60 span partitions, ten raw-byte owned reconstructions, six source positive controls, five ownership negatives and ten collision-candidate controls passed generated-model diagnostics. An extra-root defect and false digest-equality defect fail their owning controls; restored observations match. Importer tests reject changed, truncated and missing evidence. Qualification uses an isolated language-1.2 copy with saved official compiler 71defb4; original release locks and Core sources remain unchanged.

Full diagnostic verification of the exact final source fails LLV7013: certificate A for Core.RuntimeSequence.step, relation __rel_16, is rejected by the kernel for deep recursion. An earlier factored controlled-probe snapshot reports LLS8002: 5,107,159 certificate bytes above the unchanged4,194,304-byte limit, before axiom audit. A narrower step request reused stale dependency annotations and is discarded as current-branch evidence. Current sources are AST-matched to the final frozen diagnostic copy apart from semantic-module version. Full pinned release acceptance, integrated BinaryProgram execution, universal ownership transition refinement and complete engine-to-trace collision reduction remain unqualified. See validation/integrity/binding-evidence.json and docs/governance/integrity-binding.md. This is progress toward #43; it does not close the issue or qualify v0.1. No merge or tag is requested.

Reconciled onto integration3c8fca4; all existing Core sources are preserved. All27 xtask tests, five importer tests, model projections and rustfmt pass locally. Diagnostic Heap/RuntimeValue/RuntimeSequence/HeapAudit dependencies remain byte-identical to the initially diagnosed d402e3d snapshot. The inherited source-authority audit still reports docs/implementation/runtime-admission.md missing its non-authority marker.

@afflom
afflom force-pushed the v01/integrity-format3 branch from 38230ed to 13485ea Compare November 4, 2026 22:10
Merge the preceding chain head into v01/integrity-format3 and carry this
lane's unintegrated changes forward in SDK 1.2 form.
@afflom
afflom changed the base branch from v01/product-integration to v01/owned-wire-emitter November 6, 2026 06:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant