GitHub

ADR-0076: Sealed-object GNU version-requirement inventory

Status: accepted
Date: 2026-08-09
Decision owners: NAUX architecture and x86-64 symbol-version boundary

Context

ADR-0075 proves that every transitive DT_NEEDED name has exactly one reviewed exact-byte provider inside the sealed object set. Name closure is still weaker than link compatibility. GNU ELF objects can attach version requirements to symbols through DT_VERNEED chains; ignoring those declarations would let a later boundary claim compatibility without knowing which provider/version contracts the object requests.

Decision drivers

  • Read only opaque bytes obtained from an independently verified ADR-0073 object set after fully replaying ADR-0075.
  • Use a decoder independent of ADR-0074 so one parser cannot certify both dependency names and version requirements.
  • Preserve exact Verneed and Vernaux chain order, offsets, hashes, flags, version indices, names, and provider bindings.
  • Every vn_file must name one ADR-0075 provider and must occur in the source provider’s admitted DT_NEEDED vector.
  • Validate every version-name hash with a sovereign ELF hash implementation.
  • Reject malformed, cyclic, overlapping, duplicate, ambiguous, unsupported, or unbounded chain structure.
  • Inventory requirements only. Do not claim that a provider defines a version or that any symbol can bind or relocate.

Considered options

Ask readelf, libelf, or the host loader

Rejected. External output or host resolution would become semantic authority and would not replay from the sealed bytes alone.

Reuse ADR-0074’s internal ELF decoder

Rejected. Reuse reduces code but correlates parser and virtual-address mapping bugs across the dependency and version boundaries.

Ignore version tables until relocation

Rejected. Relocation design would then begin from a falsely complete graph and mix inventory, provider definition, symbol selection, and mutation authority in one oversized trust boundary.

Parse requirements and definitions together

Rejected. A requirement is a fact about the requesting object; a definition is a separately reviewed fact about a provider. Keeping them separate makes the unsupported authority explicit and mutation tests narrower.

Independently inventory bounded requirement chains

Selected. Each canonical ADR-0075 provider is decoded once from its first sealed appearance. Duplicate appearances remain bound by ADR-0075’s exact digest rule. The result records requirements without resolving definitions or symbols.

Decision

Introduce a proof-only ordered evidence vector with one record per canonical ADR-0075 provider. The decoder independently validates ELF64 little-endian x86-64 ET_DYN identity, bounded program/load/dynamic structure, an unambiguous file-backed string table, and the paired presence or absence of DT_VERNEED plus DT_VERNEEDNUM.

Each present version-need table must contain the exact declared positive number of 16-byte Verneed records. Every record has version 1, a positive bounded auxiliary count, a canonical dependency name, an exact provider ordinal, and a nonzero next offset except for the final record. Each auxiliary chain contains the exact declared number of 16-byte Vernaux records, canonical unique version names, matching ELF hashes, supported flags, unique non-reserved version indices, and exact terminal structure. All record ranges are non-overlapping and all relative-offset arithmetic is checked.

Frozen limits

  • Linux x86-64 ELF64 little-endian ET_DYN objects only;
  • at most 65 canonical providers;
  • at most 64 program headers and 16 load segments per object;
  • at most 4,096 dynamic entries per object;
  • at most 64 version-need records and 64 auxiliaries per record;
  • at most 4,096 total auxiliary records across the closure;
  • at most 1 MiB dynamic string table and 256 bytes per name;
  • Verneed and Vernaux records are exactly 16 bytes;
  • vn_version = 1, supported vna_flags are none or weak, and version indices are non-reserved, non-hidden, and unique within one requesting object;
  • accepted ADR-0075 policy root 6835b65f73be7d214da23b20c92b93013ac02c5f3b96c4abf743cd503761bd56;
  • proof-only inventory; encoder policy remains 1.4.0.

Consequences

  • Positive: NAUX gains an exact byte-bound inventory of every GNU version requirement before attempting provider-definition or symbol resolution.
  • Positive: version-table chains replay after source deletion and without host loader, filesystem, external parser, or process state.
  • Positive: splitting requirements from definitions prevents inventory from minting compatibility authority.
  • Negative: ADR-0075 and the complete sealed-object chain are replayed before decoding, increasing verification work.
  • Negative: GNU versioning is platform-specific and does not cover alternative ELF conventions in this policy version.
  • Risk: correct requirement inventory does not prove provider definitions, exported symbol type/visibility, relocation compatibility, or initialization safety.
  • Open: provider version definitions, dynamic symbol inventory, symbol binding, relocation, mapping, initialization, and execution remain outside.

Acceptance gates

  1. The accepted three-provider closure reconstructs the exact loader, libgcc, and libc requirement vectors and binds every vn_file to one provider.
  2. Missing/extra/duplicate tags, bad counts, versions, hashes, flags, indices, names, offsets, cycles, overlaps, terminals, providers, records, roots, and locally resealed evidence fail closed.
  3. A requirement naming a closure provider absent from the requester’s DT_NEEDED vector fails closed.
  4. Source deletion cannot alter replay, and production imports no filesystem, process, loader, external ELF parser, native emitter, standalone/raw decoder, or measurement authority.
  5. Focused, workspace, strict lint, governance, refinement, format, shell, link, parity, and static-authority gates pass before acceptance.
  • ADR-0073 supplies immutable exact object bytes.
  • ADR-0074 supplies independent SONAME and DT_NEEDED facts.
  • ADR-0075 supplies the reviewed unique provider closure consumed here.

Acceptance record

Accepted on 2026-08-09 under dependency-version policy root 7c278cc0cdf40cc415cea91839434dfb4bcbd5305d2a6b73eb2cc41c22e45b32. The independently decoded three-provider closure contains three ordered Verneed records and twelve ordered Vernaux records. The loader has no requirements. Libgcc binds one GLIBC_2.3 requirement to the loader and seven ordered requirements to libc: GLIBC_ABI_DT_RELR, GLIBC_2.3.4, GLIBC_2.35, GLIBC_2.14, GLIBC_2.34, GLIBC_2.3.2, and GLIBC_2.2.5. Libc binds four ordered requirements to the loader: GLIBC_2.2.5, GLIBC_2.3, GLIBC_2.35, and GLIBC_PRIVATE.

Focused replay passes both canonical and locator/identity/ELF-drift tests. Decoder probes reject missing or mismatched tags and counts, unsupported versions, bad file/name offsets, zero auxiliary offsets, invalid ELF hashes, unsupported flags and reserved indices, broken chain terminals, and a syntactically valid closure provider absent from the requester’s exact DT_NEEDED vector. Evidence probes reject stale policy/closure bindings, count and record drift, and a deep auxiliary mutation after all local record and aggregate seals are recomputed. Canonical ADR-0074, ADR-0075, and ADR-0076 replay still succeeds after deleting the source bundle.

The full all-feature workspace exits successfully: the library suite reports 408 passed, zero failed, and six intentionally ignored tests; the ADR-0073 through ADR-0076 carrier reports two passed and zero failed. Strict Clippy, cargo check, format/diff, 22/22 governance, 8/8 strict refinement, all nine shell syntax checks, and 325 checked local Markdown targets with zero missing also pass. Production source imports no filesystem, path, process, native execution, standalone/raw image, host ELF parser, or dynamic-loader authority.

Acceptance grants no version-definition, requirement-to-definition matching, dynamic-symbol inventory, symbol binding, host resolution, mapping, relocation, initialization, execution, sandbox, timing, performance claim, or global encoder-policy authority.