GitHub

ADR-0077: Sealed-object GNU version-definition inventory

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

Context

ADR-0076 proves which GNU symbol versions each object requests from each exact reviewed direct dependency. A requested name is not proof that its provider defines that version. GNU ELF providers describe their version namespaces with DT_VERDEF chains, but consulting the host loader or merging definitions with symbol selection would silently expand a proof-only boundary into linking authority.

Decision drivers

  • Read only opaque bytes obtained from an independently verified ADR-0073 object set after fully replaying ADR-0075 and ADR-0076.
  • Use a decoder independent of ADR-0074 and ADR-0076 so no shared parser can certify dependency identity, requirements, and definitions.
  • Preserve exact Verdef and Verdaux order, offsets, versions, flags, indices, hashes, primary names, and parent/dependency names.
  • Validate each definition hash against its primary name with a sovereign ELF hash implementation.
  • Distinguish the base definition from ordinary definitions and reject duplicate indices, primary names, malformed ancestry, and unsupported flags.
  • Inventory definitions only. Do not match requirements, enumerate dynamic symbols, select a definition for a symbol, or relocate code.

Considered options

Ask readelf, libelf, or the host loader

Rejected. Their interpretation would become non-replayable semantic authority and could disagree with the exact sealed deployment bytes.

Reuse the ADR-0076 decoder

Rejected. Sharing layout and dynamic-table parsing would correlate a single bug across the requirement and definition sides of a later compatibility proof.

Match ADR-0076 requirements while decoding definitions

Rejected. Inventory and compatibility are different judgments. A combined boundary would hide whether a failure came from malformed provider evidence or from a missing requested version.

Defer definitions until dynamic-symbol resolution

Rejected. Symbol resolution would start from an unproved provider namespace and combine table parsing, version compatibility, visibility, type, and relocation authority in one oversized step.

Independently inventory bounded definition chains

Selected. Each canonical ADR-0075 provider is decoded once from its first sealed appearance. Exact definition records are sealed without interpreting their relationship to ADR-0076 requirements or dynamic symbols.

Decision

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

Each present table contains the exact declared positive number of 20-byte Verdef records. Every record uses the current revision, has a positive bounded auxiliary count, a supported flag set, a canonical unique index and primary name, and exact terminal structure. Its nonzero vd_aux leads to exactly the declared number of ordered 8-byte Verdaux records. The first auxiliary is the definition’s primary name and must match vd_hash; later auxiliaries are preserved as ordered parent/dependency names without claiming that their graph is semantically complete. 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 256 version-definition records per object;
  • at most 64 auxiliaries per definition and 8,192 total auxiliaries;
  • at most 1 MiB dynamic string table and 256 bytes per name;
  • Verdef records are exactly 20 bytes and Verdaux records exactly 8 bytes;
  • vd_version = 1; supported flags are base and weak, separately or combined;
  • exactly one base definition is allowed when definitions are present; its index is global index 1, its primary name equals the provider SONAME, and it has no parent auxiliary;
  • every non-base index is in [2, 0xfeff]; indices and primary names are unique within one provider;
  • accepted ADR-0076 policy root 7c278cc0cdf40cc415cea91839434dfb4bcbd5305d2a6b73eb2cc41c22e45b32;
  • proof-only inventory; encoder policy remains 1.4.0.

Consequences

  • Positive: NAUX gains exact byte-bound provider namespaces before attempting any requirement compatibility or dynamic-symbol judgment.
  • Positive: definition chains replay after source deletion without filesystem, host loader, external parser, or process state.
  • Positive: independent requirement and definition decoders permit a later cross-proof to detect disagreement rather than inheriting one parser’s bug.
  • Negative: the full predecessor chain and a third ELF decoder increase verification work and implementation size.
  • Negative: GNU version definitions remain platform-specific and do not cover alternative ELF versioning conventions.
  • Risk: a valid definition inventory does not prove that any dynamic symbol is exported under that index or that any relocation can bind.
  • Open: requirement-to-definition matching, .gnu.version and .dynsym inventory, visibility/type binding, relocation, mapping, initialization, and execution remain outside.

Acceptance gates

  1. The accepted three-provider closure reconstructs exact loader, libgcc, and libc version-definition and auxiliary vectors from sealed bytes.
  2. Missing/extra/duplicate tags, bad counts, revisions, flags, indices, hashes, names, auxiliary offsets, chain offsets, cycles, overlaps, terminals, base identity, roots, records, and locally resealed evidence fail closed.
  3. Definition indices and primary names are unique; the base record is exact; the first auxiliary matches vd_hash; ordered parent names remain sealed.
  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-0075 supplies the canonical unique providers decoded here.
  • ADR-0076 supplies the independently replayed requirement evidence and remains semantically separate from definitions.

Acceptance record

Accepted on 2026-08-10 under dependency-definition policy root f447533303533aca4f761a202aafecdff11a428b48aa3b51fa7bd81cda9172ce. The independent decoder reconstructs 70 exact ordered Verdef records and 131 exact ordered Verdaux records across the three canonical providers. The loader contributes 7 definitions and 12 auxiliaries, libgcc contributes 16 and 30, and libc contributes 47 and 89. Every object has exactly one base record at index 1 with its exact SONAME; all remaining indices and primary names are unique. The complete loader, GCC, GLIBC, ABI, and private primary-name vectors are locked, and every ordered linear parent or parentless terminal shape is replayed.

Decoder probes reject missing, duplicate, or mismatched dynamic tags; truncated or excessive counts; unsupported revisions and flags; missing base authority; reserved and duplicate indices; zero auxiliary counts/offsets; bad primary hashes and name offsets; broken auxiliary/definition terminals; overlapping record ranges; a locally coherent base rename; and invalid base identity. Evidence probes reject stale policy, closure, and ADR-0076 roots, count/object/ auxiliary drift, and a deep primary-name mutation after all local record, object, and aggregate seals are recomputed. Canonical ADR-0074 through ADR-0077 replay still succeeds after deleting the source bundle.

The all-feature workspace exits successfully: the library suite reports 408 passed, zero failed, and six intentionally ignored tests; the ADR-0073 through ADR-0077 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 329 local Markdown targets across 145 project files 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 requirement-to-definition matching, dynamic-symbol or .gnu.version inventory, symbol binding, host resolution, mapping, relocation, initialization, execution, sandbox, timing, performance claim, or global encoder-policy authority.