GitHub

ADR-0079: Independent dynamic-symbol extent and GNU version-index inventory

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

Context

ADR-0076 and ADR-0077 independently inventory the GNU version namespaces requested and defined by every exact object in the reviewed dependency closure. ADR-0078 proves that every strong request exists uniquely in its already admitted provider. NAUX still has no authority to say how many dynamic symbols an object contains, which bytes constitute each symbol, or which local version index accompanies a symbol. Granting symbol lookup or relocation authority before those facts are independently bounded would silently delegate semantics to section headers, a host ELF library, or the dynamic loader.

ELF does not provide a DT_SYMCOUNT tag. A System V hash table exposes an exact nchain, while a GNU hash table encodes its symbol extent through symoffset, ordered buckets, and terminating chains. The accepted Arch Linux fixture uses GNU hash tables without System V hash tables, so refusing GNU-only objects would stop the sovereign dependency path at the very boundary it must own.

Decision drivers

  • Derive a finite symbol extent without trusting ELF section headers or host loader behavior.
  • Independently decode both System V and GNU hash layouts and require their extents to agree when both exist.
  • Reconstruct GNU buckets, chains, bloom words, and name hashes from the decoded symbols rather than trusting a terminal-bit scan alone.
  • Require one exact 24-byte Elf64_Sym record and one parallel 16-bit GNU version entry for every admitted symbol ordinal.
  • Resolve only local version-index meaning against accepted ADR-0076/0077 evidence. Do not select a provider symbol or satisfy a relocation.
  • Preserve complete byte/order/provenance evidence under explicit hard limits.

Considered options

Trust .dynsym and .gnu.version section sizes

Rejected. Section headers are not required for runtime loading and remain outside the accepted program-header/dynamic-table authority.

Use only DT_HASH.nchain

Rejected. It gives a simple exact extent where present, but every object in the locked fixture is GNU-hash-only.

Treat the highest GNU chain terminal as sufficient proof

Rejected. A malformed table can terminate early, route a bucket into another bucket’s chain, omit symbols, or carry names whose GNU hashes disagree with the claimed topology.

Infer extent from the address of the following dynamic table

Rejected. Inter-table padding is not a semantic symbol count, address ordering is not guaranteed, and a later layout change would alter authority.

Decode symbols and perform lookup/binding in one boundary

Rejected. Inventory, lookup order, visibility, type compatibility, interposition, weak fallback, and relocation are distinct judgments with different adversarial surfaces.

Emit an exact proof-only symbol/version inventory

Selected. Hash-table structure establishes the policy extent; complete hash-table reconstruction, symbol decoding, and version-index replay prove the inventory without granting any consumer binding authority.

Decision

Introduce one independently verified evidence object per canonical ADR-0075 provider. Before reading any new fact, replay ADR-0078 and therefore the full ADR-0073 through ADR-0077 chain.

For each object:

  1. require exactly one DT_SYMTAB, DT_SYMENT, DT_STRTAB, and DT_STRSZ;
  2. require DT_SYMENT = 24 and translate all virtual addresses only through admitted read-only PT_LOAD coverage;
  3. independently decode at least one of DT_HASH or DT_GNU_HASH;
  4. derive the exact policy symbol count from System V nchain or from the terminal extent of a structurally valid GNU bucket/chain table, and require equality when both tables exist;
  5. decode exactly that many ordered Elf64_Sym records, with ordinal zero the all-zero STN_UNDEF record, bounded names in the accepted string table, admitted binding/type/visibility encodings, and no SHN_XINDEX escape;
  6. recompute every accepted System V or GNU symbol hash and reconstruct the complete bucket/chain topology. For GNU hash, also reconstruct the exact bloom words and require the unhashed prefix/non-local hashed suffix implied by symoffset (the prefix may also contain undefined global symbols);
  7. require exactly one DT_VERSYM table and decode exactly one little-endian version word per admitted symbol ordinal;
  8. split each word into the hidden bit and 15-bit local index. Indices 0 and 1 are reserved local/global identities and cannot carry the hidden bit;
  9. for every index from 2 through 0x7eff, require exactly one namespace target: an undefined symbol must reference one ADR-0076 auxiliary in the current requester’s inventory, while a defined symbol must reference one ADR-0077 definition in the current provider;
  10. seal raw field values, exact names/hashes, classified definition state, version target identity, per-record evidence, per-object evidence, both predecessor roots, and one domain-separated aggregate root.

Verification preflights counts and all predecessor identities, independently replays both hash formats, regenerates every symbol/version record from the opaque sealed object, and requires byte-for-byte evidence equality. It never uses readelf, section headers, a host ELF parser, filesystem paths, or dynamic loader APIs in production.

Frozen limits

  • at most 65 provider objects;
  • at most 4,096 dynamic symbols per object and 16,384 in the closure;
  • exactly 24 bytes per Elf64_Sym and 2 bytes per version entry;
  • at most 4,096 System V buckets and chains per object;
  • at most 4,096 GNU buckets, 512 64-bit bloom words, and 4,096 GNU chains per object;
  • string-table extent at most 1 MiB and each decoded symbol name at most 256 bytes, inherited from the accepted ELF/string policy;
  • STN_UNDEF ordinal zero is bytewise zero;
  • accepted symbol bindings: local, global, weak, and GNU unique;
  • accepted symbol types: no-type, object, function, section, file, common, TLS, and GNU IFUNC; all other encodings fail closed;
  • accepted visibility encodings: default, internal, hidden, and protected with all reserved st_other bits zero;
  • SHN_XINDEX and unsupported reserved section indices fail closed;
  • accepted ADR-0078 policy root 017832c19b76fc994f2840423fdee0411893a5c9c21e808f1ee5979e39f7c84e;
  • proposed ADR-0079 policy root d39244c89aad35ab8c0d617a6688e4a3c19acbd8029306e5d42070bdfec07758;
  • proof-only admission; encoder policy remains 1.4.0.

Consequences

  • Positive: later lookup logic receives an exact, ordered, replayable symbol universe instead of probing object memory or host loader state.
  • Positive: GNU-only objects are supported without weakening the no-section- authority rule.
  • Positive: malformed extents, buckets, chains, bloom filters, names, symbol fields, version words, and namespace references fail before binding exists.
  • Positive: version-index collisions between definition and requirement spaces remain scoped by defined/undefined symbol state.
  • Negative: complete hash reconstruction adds linear admission work and a larger proof ledger.
  • Negative: unusual but loader-tolerated noncanonical hash layouts or reserved symbol encodings are intentionally refused by policy version 1.0.
  • Risk: exact inventory still says nothing about lookup precedence, interposition, weak fallback, visibility/type compatibility, or relocation.
  • Open: symbol selection, GNU-unique process scope, IFUNC execution, TLS, copy relocation, mapping, initialization, and final loader equivalence remain separate decisions.

Acceptance gates

  1. Lock exact per-provider symbol counts, System V/GNU hash shapes, and total symbol/version counts for the reviewed fixture.
  2. Lock every ordered symbol field, exact bounded name/hash, version word, hidden state, and exact ADR-0076/0077 namespace target where required.
  3. Missing, duplicate, mismatched, truncated, excessive, early-terminal, cross-bucket, bloom, name/hash, STN_UNDEF, info/other/shndx, count, version-index, stale-root, reorder, and locally resealed mutations fail closed.
  4. A coherent mutation that substitutes a different valid symbol/version target and recomputes every local seal still fails independent regeneration.
  5. Canonical replay succeeds after source-path deletion; production source has no filesystem, section-header, host parser/loader, symbol-selection, relocation, mapping, native, timing, or claim authority.
  6. Focused, workspace, strict lint, governance, refinement, format, shell, link, source-deletion, parity, and static-authority gates pass before acceptance.
  • ADR-0076 supplies undefined-symbol version-index namespaces.
  • ADR-0077 supplies defined-symbol version-index namespaces.
  • ADR-0078 proves every strong requested namespace exists in its exact admitted provider.

Acceptance record

Accepted on 2026-08-10 under dependency-symbol policy root d39244c89aad35ab8c0d617a6688e4a3c19acbd8029306e5d42070bdfec07758. The exact GNU-hash-only fixture contains 3,455 ordered dynamic symbols and the same number of parallel version words: loader contributes 40, libgcc 226, and libc 3,189. Their exact (symbol count, symoffset, bloom words, buckets, chains) shapes are (40, 1, 4, 71, 39), (226, 28, 32, 389, 198), and (3189, 22, 512, 1009, 3167). Every Elf64_Sym field, bounded name, System V and GNU name hash, version word/hidden bit, namespace kind and exact ADR-0076/0077 target evidence hash is retained in order under local, per-object, and aggregate seals.

The independent decoder reconstructs every GNU bloom word, bucket, and chain from the retained symbol names after deriving the candidate extent. It accepts the real GNU unhashed prefix, including undefined global symbols before symoffset, while requiring every hashed-suffix symbol to be non-local. System V nchain decoding and exact hash reconstruction are implemented and must cross-check the GNU extent when both formats exist; the locked fixture itself contains no DT_HASH tables.

Raw probes reject missing/duplicate/mismatched symbol and hash tags; noncanonical DT_SYMENT; zero, excessive, or malformed bucket/bloom/extent fields; invalid bloom shifts; bloom, bucket, hash-chain, and terminal drift; broken STN_UNDEF; invalid name offsets/bytes, binding, type, visibility, and section indices; hidden reserved and reserved version indices. Evidence probes reject stale policy/compatibility roots, totals, object/symbol/hash records, and a coherent alternate valid definition target after the symbol, object, and aggregate seals are fully recomputed. Canonical ADR-0074 through ADR-0079 replay succeeds after deleting the source bundle.

The final all-feature workspace exits successfully. The library suite reports 410 passed, zero failed, and six intentionally ignored tests in 435.22 seconds; the ADR-0073 through ADR-0079 carrier reports two passed and zero failed in 422.23 seconds; the process-isolation carrier reports three passed and zero failed in 289.68 seconds. Strict Clippy with warnings denied, cargo check, 22/22 governance, 8/8 strict refinement, all nine shell syntax checks, format/diff, Markdown links, locked hash-shape tests, production static- authority inspection, and exact source-deletion replay pass.

Acceptance grants no root-worker symbol inventory, symbol lookup, selection, interposition, binding, weak fallback, visibility/type compatibility, relocation, mapping, initialization, IFUNC/TLS execution, sandbox, standalone, timing, performance claim, or global encoder-policy authority.