GitHub

ADR-0078: Exact GNU version requirement-to-definition compatibility admission

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

Context

ADR-0076 independently inventories the ordered version names each reviewed object requests from each direct provider. ADR-0077 independently inventories the version namespaces those exact providers define. Neither boundary compares the two sides. A later linker cannot safely inspect dynamic symbols until NAUX has first proved that every strong requested namespace exists uniquely in the provider already admitted by the sealed dependency closure.

Decision drivers

  • Replay ADR-0076 and ADR-0077 in full before trusting either evidence vector.
  • Match only the exact provider ordinal already bound by ADR-0076; never search the host, global closure, filesystem, loader cache, or alternative providers.
  • Bind exact version names and sovereign ELF hashes while preserving requester, requirement, auxiliary, provider, and definition order/identity.
  • Require one and only one definition for every strong requirement.
  • Fail closed on weak requirements until weak-version fallback semantics have a separate decision and oracle.
  • Produce a proof-only compatibility ledger. Do not inspect .dynsym, .gnu.version, relocations, symbol visibility, or symbol types.

Considered options

Let the host loader decide compatibility

Rejected. Host search paths, cache state, replacement objects, and loader policy would become unsealed semantic authority.

Match by name across the complete closure

Rejected. It could satisfy a requirement from the wrong provider and erase the direct DT_NEEDED binding proven by ADR-0076.

Treat weak requirements as ordinary strong requirements

Rejected. That would be stricter than GNU weak-version semantics without recording the semantic difference, and it could later be misrepresented as loader equivalence.

Implement weak fallback immediately

Rejected. Weak fallback interacts with dynamic-symbol and unversioned-symbol selection, which remain outside this boundary.

Combine compatibility with dynamic-symbol inventory

Rejected. Namespace existence and per-symbol binding are different judgments. Combining them would obscure the authority ceiling and enlarge adversarial state before either layer is independently stable.

Emit an exact proof-only compatibility ledger

Selected. Strong requirement names are joined only to primary definition names in their exact providers. Both source record hashes and every selected target field are sealed into an independently regenerable ledger.

Decision

Introduce an ordered compatibility evidence vector with one object record per canonical requester and one binding per ADR-0076 Vernaux auxiliary. Before emission, replay ADR-0077, which itself replays the complete ADR-0073 through ADR-0076 chain. For each requirement auxiliary:

  1. require vna_flags = 0 in policy version 1.0;
  2. select only the exact provider ordinal already sealed in its parent ADR-0076 requirement;
  3. find exactly one ADR-0077 definition whose primary name and sovereign ELF hash equal the requested name and hash;
  4. seal requester/requirement/auxiliary ordinals and evidence hashes, provider ordinal and evidence hash, definition ordinal/index/flags/name/hash and evidence hash, plus one domain-separated binding hash;
  5. preserve complete requester and requirement order without sorting or deduplication.

Verification preflights bounded shape and all predecessor roots, then regenerates the complete ledger from independently verified predecessors and requires exact equality.

Frozen limits

  • at most 65 requester/provider objects;
  • at most 64 requirement records per requester;
  • at most 64 auxiliaries per requirement;
  • at most 4,096 total compatibility bindings;
  • exact UTF-8/ASCII names inherited from ADR-0076/0077, at most 256 bytes;
  • weak requirements are refused in policy version 1.0;
  • accepted ADR-0076 policy root 7c278cc0cdf40cc415cea91839434dfb4bcbd5305d2a6b73eb2cc41c22e45b32;
  • accepted ADR-0077 policy root f447533303533aca4f761a202aafecdff11a428b48aa3b51fa7bd81cda9172ce;
  • proof-only admission; encoder policy remains 1.4.0.

Consequences

  • Positive: every strong GNU version requirement is proven present in the exact reviewed provider before NAUX inspects any symbol table.
  • Positive: disagreement between the independent requirement and definition decoders becomes an explicit fail-closed compatibility error.
  • Positive: the cross-proof is path-free, byte-free, deterministic, bounded, and cheap relative to the predecessor ELF decoders.
  • Negative: objects containing weak requirements remain unsupported even when a host loader could execute them.
  • Negative: verification replays the full predecessor chain before joining evidence.
  • Risk: namespace compatibility does not prove that any requested dynamic symbol exists under that namespace.
  • Open: weak fallback, .dynsym, .gnu.version, symbol visibility/type, relocation, mapping, initialization, and execution remain outside.

Acceptance gates

  1. The accepted fixture produces exactly twelve bindings in requester and requirement order: eight from libgcc and four from libc.
  2. Every binding selects the expected loader or libc definition ordinal/index, exact primary name/hash/flags, and both predecessor record hashes.
  3. Weak, missing, duplicate, wrong-provider, wrong-name/hash/index/flag/order, stale-root, count, record, and locally resealed evidence mutations fail closed.
  4. Production source imports no filesystem, path, process, loader, external ELF parser, native emitter, standalone/raw decoder, mapping, relocation, or measurement authority.
  5. Focused, workspace, strict lint, governance, refinement, format, shell, link, parity, and static-authority gates pass before acceptance.
  • ADR-0075 supplies exact unique provider identity.
  • ADR-0076 supplies ordered strong/weak requirement facts and exact provider ordinals.
  • ADR-0077 supplies independent provider definition namespaces.

Acceptance record

Accepted on 2026-08-10 under dependency-compatibility policy root 017832c19b76fc994f2840423fdee0411893a5c9c21e808f1ee5979e39f7c84e. The exact ordered ledger contains twelve strong bindings: eight requested by libgcc and four requested by libc. Libgcc binds GLIBC_2.3 to loader definition index 3 and its remaining seven names to libc indices 44, 7, 36, 18, 35, 5, and 2 in requirement order. Libc binds GLIBC_2.2.5, GLIBC_2.3, GLIBC_2.35, and GLIBC_PRIVATE to loader indices 2, 3, 6, and 7. Every binding retains exact requester, requirement, auxiliary, provider, and definition ordinals; both predecessor object hashes; exact primary names, ELF hashes, indices, flags; and domain-separated local seals.

Join probes reject weak requirements, absent definitions, wrong primary hashes, ambiguous matches, and exact-name matches found only in a different provider. The locked fixture intentionally contains GLIBC_2.3 in more than one provider, proving that provider ordinal is semantic rather than a search hint. Evidence probes reject stale policy/version/definition roots, count, object, binding, and order drift. A deep mutation substitutes a different valid definition from the same provider and recomputes the binding, object, and aggregate seals; independent regeneration still rejects it. Canonical ADR-0074 through ADR-0078 replay succeeds after deleting the source bundle.

The focused ADR-0078 carrier passes in 360.42 seconds. The all-feature workspace exits successfully: the library suite reports 408 passed, zero failed, and six intentionally ignored tests; the ADR-0073 through ADR-0078 carrier reports two passed and zero failed in 323.64 seconds. Strict Clippy, cargo check, format/diff, 22/22 governance, 8/8 strict refinement, and all nine shell syntax checks pass. All 334 local Markdown targets across 145 project files resolve with zero missing. Production source imports no filesystem, path, process, object-byte, native execution, standalone/raw image, host-loader, symbol-selection, or relocation authority.

Acceptance grants no weak-version fallback, dynamic-symbol or .gnu.version inventory, symbol selection/binding, host resolution, mapping, relocation, initialization, execution, sandbox, timing, performance claim, or global encoder-policy authority.