ADR-0075: Reviewed transitive-declaration closure admission
Status: accepted
Date: 2026-08-09
Decision owners: NAUX architecture and x86-64 dependency-closure boundary
Context
ADR-0074 independently reconstructs the exact DT_SONAME and ordered
DT_NEEDED vector of every sealed ADR-0073 object. That inventory exposes a
graph, but it does not prove that the sealed set contains an externally
reviewed, non-ambiguous byte provider for every requested name. Inferring
closure merely because a matching string happens to occur would let observed
host state mint authority.
Decision drivers
- Closure authority must originate in a caller-supplied, externally reviewed, canonical SONAME/digest/ordered-edge graph.
- Every graph node must bind one exact ADR-0073 object digest and every graph
edge must bind one exact ADR-0074
DT_NEEDEDordinal. - Canonical provider order is first appearance in the sealed object vector.
- Repeated appearances of one SONAME may collapse only when their object digest and all closure-relevant dynamic facts agree exactly.
- Missing, extra, duplicate, reordered, ambiguous, digest-conflicting, or locally resealed review/evidence records must fail closed.
- Admission proves closure inside the reviewed sealed set only. It must not reproduce or claim host-loader search and selection semantics.
Considered options
Ask the host loader to resolve every name
Rejected. Search paths, caches, namespaces, environment, distribution policy, and mutable filesystem state would become semantic authority.
Treat every observed SONAME as an implicitly approved provider
Rejected. Observation is not review. This would allow the candidate bundle to define its own acceptance policy.
Key providers by pathname or declaration ordinal
Rejected. Pathnames are locators rather than byte identity, while declaration ordinals duplicate the accepted loader and do not express graph identity.
Deduplicate every repeated SONAME unconditionally
Rejected. Two objects may claim one SONAME while containing different bytes or different dependency/hardening facts. Silent collapse would erase ambiguity.
Compare an external canonical graph with an independently derived graph
Selected. Admission first fully replays ADR-0074, derives providers in exact first-appearance order, rejects conflicting repeated identities, resolves each ordered edge to one unique derived provider, and then requires exact equality with the externally reviewed expectation.
Decision
Introduce a proof-only closure expectation whose ordered provider records bind exact SONAME, exact SHA-256 object identity, and exact ordered dependency names. Expectation construction validates canonical names, bounded cardinalities, unique edges, unique provider SONAMEs, and domain-separated hashes without reading the object set.
Closure admission independently verifies ADR-0074 and derives a canonical
provider vector from its records plus ADR-0073 object digests. A repeated
SONAME must have the same digest, ordered needed vector, DT_FLAGS, and
DT_FLAGS_1; otherwise admission rejects the set as ambiguous. Every needed
name must select exactly one canonical provider. The resulting evidence binds
the reviewed expectation root, predecessor evidence root, provider source
ordinals, first dynamic-record root, exact byte digest, ordered edges, resolved
provider ordinals, flags, and aggregate counts.
Frozen limits
- schema and policy version 1.0.0;
- at most 65 canonical providers and 65 source appearances;
- at most 4,096 total ordered closure edges;
- at most 256 printable non-space ASCII bytes per SONAME, with no slash or backslash;
- provider order is exact first appearance in ADR-0074;
- dependency names are ordered and unique within each provider;
- duplicate provider SONAMEs are forbidden in the reviewed expectation;
- accepted ADR-0074 dynamic policy root
7083c3d4b4d4afed21023448d8a16b066558a6e3f17969835e1a87892a3d371f; - proof-only closure admission; encoder policy remains
1.4.0.
Consequences
- Positive: every admitted transitive declaration has exactly one reviewed byte-identity provider inside the immutable object set.
- Positive: the accepted duplicate loader appearances collapse transparently only because their exact digest and dynamic facts agree.
- Positive: closure replay remains independent of filesystem paths, loader caches, environment, namespaces, and process state.
- Negative: verification fully replays all predecessor boundaries and rebuilds the graph; work is linear in appearances plus edges.
- Negative: any dependency outside the explicitly reviewed sealed set is a hard failure, even if the host could resolve it.
- Risk: internal declaration closure is not proof that the host loader would choose these objects or that their symbols, versions, and relocations fit.
- Open: symbol/version requirements, resolution semantics, mapping, relocation, initialization, execution, sandboxing, and launch observation remain outside.
Acceptance gates
- The four-object accepted vector collapses to three canonical providers and resolves all three ordered edges to exact reviewed digests.
- Missing, extra, duplicate, reordered, edge-drifted, digest-conflicting, root, record, aggregate, and locally resealed mutations fail closed.
- Source deletion cannot alter closure verification.
- Production imports no filesystem/path resolver, process launcher, loader, external ELF parser, native emitter, standalone/raw decoder, or measurement authority.
- Focused, workspace, strict lint, governance, format, shell, link, parity, and static-authority gates pass before acceptance.
Related decisions
- ADR-0072 establishes external review as the source of declaration authority.
- ADR-0073 supplies immutable exact object identities.
- ADR-0074 supplies the independently reconstructed SONAME and ordered-edge inventory.
Accepted evidence
The reviewed closure-admission policy is accepted under root
6835b65f73be7d214da23b20c92b93013ac02c5f3b96c4abf743cd503761bd56.
It binds schema/policy 1.0.0, the accepted ADR-0074 root, all provider,
appearance, edge, and name limits, and ten named capabilities covering external
review, predecessor replay, canonical provider construction, exact digest and
edge binding, ambiguity rejection, evidence replay, and the proof-only
authority ceiling.
The accepted deployment vector contains four source appearances collapsed in
first-appearance order to three canonical providers: loader ordinals [0, 3],
libgcc_s.so.1 ordinal [1], and libc.so.6 ordinal [2]. Its three ordered
edges resolve as libgcc_s.so.1 -> [libc.so.6, ld-linux-x86-64.so.2] and
libc.so.6 -> [ld-linux-x86-64.so.2]. Both loader appearances collapse only
because their exact object digest and dynamic facts agree.
Focused ADR-0073/0074/0075 tests pass 2/2. Missing, extra, duplicate, reordered, edge-drifted, digest-drifted, stale-root, stale-count, stale-record, and locally resealed evidence mutations fail closed. A real second valid ELF object claiming the loader SONAME with a different exact digest is admitted by the byte and dynamic boundaries but rejected by closure admission. Deleting the complete reviewed source bundle does not change closure verification.
The complete workspace passes 408 library tests with zero failures and six
explicit release-only ignores plus every enabled integration and doc test.
Governance passes 22/22, strict refinement passes 8/8, all nine shell scripts
parse, repository-local Markdown targets pass with zero missing, and strict
Clippy, format, diff hygiene, and static-import gates pass. The existing
nom 1.2.4 future-incompatibility notice remains dependency debt outside this
proof-only Core boundary and is not a compiler warning.
Acceptance proves one reviewed exact-byte provider inside the sealed set for every transitive declaration. It does not reproduce host-loader selection or grant symbol/version resolution, mapping, relocation, initialization, execution, sandbox, timing, performance-claim, or global encoder-policy authority.