ADR-0039: Direct ELF64 Standalone Image and Libc-Free Startup

Status: accepted and implemented at the finite R1-S8 correctness boundary; Gate B performance remains open

Date: 2026-07-30

Historical scope: this record composed the then-current R1-S7a/R1-S7b identities without changing them. ADR-0042 later migrated the inherited target bytes and every derived identity together; the standalone schema, startup, ELF grammar, I/O relation, and correctness boundary remain unchanged.

Extends: ADR-0038 without changing, at this decision’s acceptance time, any frozen R1-S4, R1-S5, R1-S6, R1-S7a, or R1-S7b schema, policy, identity, byte, ABI, corpus, or hard limit

Normative contract: x86_64_standalone_r1_s8_contract.md

Context

ADR-0038 closes finite native correspondence for exact, source-bound R1-S7a bytes. Its accepted runner still lives inside a Rust seed process, maps code in memory, and publishes claim evidence through a dedicated Rust worker. It does not produce an executable file that the Linux kernel can load directly.

The next boundary must answer a narrower question than complete Gate B:

Can NAUX deterministically write and independently verify a direct Linux x86-64 executable which contains only a bounded startup and one exact R1-S7a target blob, accepts the declared dynamic input, invokes no interpreter or runtime helper, and preserves the frozen finite semantics when executed as its own process?

This boundary is named R1-S8. It is the standalone correctness subgate of Gate B. Gate B also has a performance requirement. R1-S8 therefore cannot make Gate B green until an eligible controlled comparison shows runtime no greater than 2.0x the hand-specialized baseline.

Decision drivers

• keep the complete specializer-to-native provenance chain authoritative;
• eliminate the Rust worker, in-memory loader, libc, system linker, dynamic linker, and generic interpreter from the emitted process image;
• make every emitted byte deterministic and independently reconstructable;
• keep the startup small, bounded, W^X, and specific to the lighthouse;
• admit dynamic input without embedding benchmark data in the executable;
• preserve exact F64 bits, canonical NaN, Bounds, and ordered effects;
• distinguish standalone correctness from performance and production sovereignty.

Options considered

Decision

1. Authority is opaque and inherited

The standalone writer accepts only an opaque, verified Gate-B seed authority formed from:

• one exact SourceBoundX64TargetArtifact;
• complete, independently replayed R1-S7b process evidence for the inferred Gate A workload;
• exact agreement on source Machine IR, target artifact, target plan, target code, canonical ABI, entry offset, lane count, workload, manifest, and native result identities.

The writer does not accept raw target bytes, a target artifact by itself, hashes supplied by a caller, a verifier boolean, a copied execution record, or the path to an S7b worker. The opaque authority remains finite-corpus authority. It is not converted into a general semantic theorem by R1-S8.

2. One direct ELF image per workload profile

R1-S8 emits exactly one workload profile per image:

0x0001  BranchMixF64R1
0x0002  BoundsF64R1

No emitted image contains a workload switch. The exact profile is bound into the startup plan, I/O contract, artifact identity, and execution evidence. The fixed corpus uses one BranchMix image for 46 cases and one Bounds image for 5 cases.

The file is a direct Linux x86-64 ELF64 ET_EXEC image at fixed virtual base 0x0000000000400000. It has exactly two program headers:

1. one PT_LOAD covering the complete file with PF_R | PF_X; and
2. one PT_GNU_STACK with PF_R | PF_W.

It has no section-header table, PT_INTERP, dynamic section, relocation table, symbol dependency, note, writable load segment, or second load segment. The Linux kernel ELF loader is the declared platform boundary. No assembler, object writer, system linker, dynamic linker, or libc participates in constructing or running the emitted image.

The exact file layout is:

0x0000..0x003f  ELF64 header
0x0040..0x0077  PT_LOAD program header
0x0078..0x00af  PT_GNU_STACK program header
0x00b0..0x00ff  zero padding
0x0100..         NAUX-owned startup bytes
align16          zero padding
target_offset..  one exact verified R1-S7a code blob
EOF              no trailing bytes

_start is file offset 0x100 and virtual address 0x400100. The target offset is the first 16-byte-aligned offset after the startup. The target blob is copied exactly once and is byte-for-byte equal to the source-bound R1-S7a blob. It is never re-encoded, patched, relocated, or duplicated by R1-S8.

3. Libc-free startup

The startup is generated from a separately verified bounded plan. It may use only these Linux x86-64 syscalls:

read          0
write         1
mmap          9
mprotect     10
munmap       11
exit_group  231

read is restricted to file descriptor 0 and write to file descriptor 1. The image does not write diagnostics to stderr. The memory path creates at most one anonymous private RW input mapping, converts each big-endian F64 word in place, changes the mapping to R, calls the exact target entry, and unmaps it before publishing output. No mapping is ever writable and executable.

Zero-element input uses the canonical null, zero-length descriptor and does not allocate a mapping. The startup consumes at most 512 bytes below the kernel entry stack pointer and has no allocator, TLS, global constructor, unwinder, callback, runtime helper, or fallback path.

The only target transfer is the single resolved startup-to-target entry fixup. On target return, the startup validates the complete native tag and payload before encoding output. It terminates with exit_group; it never returns from _start.

4. Exact bounded wire protocol

All integer fields are big-endian. The input is:

offset  size  field
0       8     ASCII "NAUXGBI1"
8       6     version: three u16 fields `(major=1, minor=0, patch=0)`
14      2     workload profile
16      8     array_elements: u64
24      8     repetitions: i64
32      8     payload_bytes: u64
40      ...   array_elements exact IEEE-754 u64 words

payload_bytes must equal array_elements * 8 without overflow. At most 1,048,576 elements and 8,388,608 payload bytes are admitted. The complete frame is at most 8,388,648 bytes. The producer must close input after the frame; truncation, trailing bytes, unknown profiles, wrong versions, cap violations, and inconsistent lengths fail closed.

For BranchMixF64R1, repetitions is the exact dynamic I64 parameter. For BoundsF64R1, it is reserved and must be zero; the frozen Bounds target owns its static accesses at indices zero and one. A profile field must equal the profile baked into the image.

Successful semantic execution writes exactly 40 bytes:

offset  size  field
0       8     ASCII "NAUXGBO1"
8       6     version: three u16 fields `(major=1, minor=0, patch=0)`
14      2     workload profile
16      4     outcome: u32
20      4     reserved zero
24      8     payload0
32      8     payload1

Outcome 0 is Return; for the frozen profiles payload0 is the exact canonical F64 result and payload1 is zero. Outcome 1 is Bounds and both payload words are zero. A semantic Bounds result is a successfully encoded outcome and exits zero.

The process exit policy is exact:

0   valid Return or Bounds frame was completely written
64  input/schema/profile/limit rejection
70  internal plan, target-tag, or canonical-payload invariant failure
71  mmap, mprotect, or munmap failure
74  truncated input or read/write failure

A signal, abnormal exit, timeout, unknown exit code, missing output, partial output, extra output, or any stderr is a failed case, never a skip.

5. Version and identity freeze

Every R1-S8-local artifact schema and policy is exactly 1.0.0, including:

• standalone artifact schema;
• ELF layout and writer policy;
• independent ELF verifier policy;
• startup-plan schema and planner policy;
• startup lowering and encoder policy;
• I/O-contract schema and policy;
• execution-record schema and policy;
• ordered execution-results policy.

The six-byte wire version is exactly 00 01 00 00 00 00.

R1-S8 uses only these new domain prefixes:

NAUX:x86-64:r1-s8:startup:plan:v1\0
NAUX:x86-64:r1-s8:startup:code:v1\0
NAUX:x86-64:r1-s8:io-contract:v1\0
NAUX:x86-64:r1-s8:elf-image:v1\0
NAUX:x86-64:r1-s8:artifact:v1\0
NAUX:x86-64:r1-s8:execution:record:v1\0
NAUX:x86-64:r1-s8:execution:results:v1\0

Canonical identity encoding is manual, length-delimited, and big-endian. The artifact identity binds all inherited source/target identities, exact versions and policies, profile, ELF fields, startup plan/code, target offset/length/hash, complete image length/hash, I/O contract, exact hard-limit and usage vectors, and explicit interpreter_dependency=false and fallback=false fields.

6. Hard limits

The exact v1 caps are:

The image must additionally satisfy:

image_bytes <= exact_target_bytes + 65,536

All inherited R1-S4, Core SSA, Machine IR, R1-S7a, and R1-S7b limits and usages are carried and rechecked exactly. Exact-cap cases are admitted; one-over cases fail closed. A later implementation may use less but cannot silently widen a v1 cap.

7. Independent verification and execution evidence

The independent verifier parses the complete file, recomputes every ELF field and identity, regenerates the startup plan and startup bytes from the opaque authority and profile, verifies the target blob against the source-bound R1-S7a artifact, and requires byte-for-byte equality with a freshly reconstructed image. Trusting writer flags, scanning only for symbol names, or accepting a matching whole-file hash is insufficient.

Claim-bearing execution launches the file directly as a fresh process, once per canonical case. It does not invoke the S7b worker or in-memory W^X runner. The parent independently evaluates the source-bound Machine IR and validates the exact output relation. The fixed ordered result covers all 46 BranchMix and 5 Bounds cases and rejects omission, duplication, reordering, profile substitution, input substitution, replay under another artifact, abnormal termination, and fallback.

Rust std may remain seed debt in the writer, verifier, and process harness. It is not present in the emitted ELF image. Kernel loading, raw Linux syscalls, and the host filesystem/process interface are declared platform boundaries, not third-party compiler or runtime dependencies.

8. Claim boundary

Passing R1-S8 permits only:

The exact verified R1-S7a lighthouse bytes were packaged once with a reproducible, NAUX-owned, libc-free startup into a direct ELF64 image; the image ran as a separate Linux process and preserved the fixed 51-case source-bound Machine IR relation without an interpreter or fallback.

R1-S8 does not establish Gate B by itself. Gate B remains open until the same eligible standalone path is measured under the frozen benchmark method at no more than 2.0x the hand-specialized runtime.

Rationale

1. A direct fixed-layout ET_EXEC file makes the kernel loader, rather than a Rust loader or a system linker, the only executable-image boundary.
2. One RX load segment plus an explicitly RW, non-executable stack avoids a writable/executable page and keeps the file grammar small.
3. Separate profile images prevent a new workload-dispatch mechanism from reappearing after structural interpreter dispatch was erased.
4. A large but bounded input protocol exercises actual dynamic data and avoids making a tiny test-only protocol the standalone contract.
5. Big-endian wire values make protocol identity host-independent; explicit in-place conversion preserves exact x86-64 F64 bits.
6. Opaque S7b authority prevents raw bytes or detached hashes from bypassing the validated Core-to-native chain.
7. Independent reconstruction is stronger than trusting metadata emitted by the same writer.
8. Keeping performance outside the R1-S8 correctness claim prevents a successful executable launch from being mislabeled Gate B viability.

Consequences

Positive:

• NAUX gains a precise, linker-free executable-image target;
• the emitted process contains no Rust startup, libc, dynamic loader, interpreter, trace JIT, worker protocol, or runtime callback;
• image layout, startup behavior, dynamic input, identities, and resource use are deterministic and bounded;
• the exact R1-S7a bytes remain the sole target-code authority;
• standalone failures become observable process failures without weakening the finite semantic relation.

Negative:

• v1 is fixed to Linux x86-64, ELF64, SSE2, and a non-PIE virtual base;
• the startup owns a dedicated input decoder and two profile-specific call shapes;
• the kernel loader and raw syscall ABI remain declared target dependencies;
• the seed writer/verifier/harness still depend on Rust/Cargo until later sovereignty work;
• no performance result follows from the artifact format alone.

Acceptance

R1-S8 implementation is accepted only when:

• the writer consumes only opaque, exact S7b-bound authority;
• two exact profile images independently verify and reproduce bit-for-bit;
• header, program-header, padding, startup, alignment, target, and EOF mutation suites fail closed;
• all policy/schema substitutions and exact-cap/one-over cases are tested;
• the emitted file has exactly the frozen ELF grammar and no interpreter, external symbol, relocation, dynamic-loader, libc, or fallback dependency;
• startup-plan and startup-byte regeneration rejects mutations independently;
• input protocol tests cover truncation at every field, trailing bytes, overflow, wrong profile/version, zero/max/one-over sizes, short reads, canonical F64 edge cases, and Bounds;
• output/exit tests reject every partial, extra, malformed, abnormal, diagnostic, and timeout case;
• every one of the fixed 51 cases runs in a fresh direct-ELF process and matches independent Machine IR evaluation;
• ordered execution evidence is sealed under the frozen domains;
• full workspace, strict validation, formatting, lint, and documentation audits pass;
• documentation continues to say Gate B is open until the <= 2.0x performance gate passes.

Non-claims

R1-S8 does not claim:

• infinite-domain equivalence or formally verified ELF/x86-64/Linux semantics;
• hostile-code sandboxing, hermetic execution, executable attestation, or replay freshness;
• PIE/ASLR, another ISA/OS/ABI, shared libraries, general FFI, arbitrary functions, multiple arrays, writable input, allocation by generated target code, or a general standard library;
• a self-contained NAUX compiler, dependency closure, P1/P2/P3, Projection Birth, Nauxogenesis, or removal of Rust/Cargo/egg seed debt;
• Gate B, Gate C, benchmark eligibility, performance leadership, or parity with C/C++ before their separate evidence gates pass.

Revisit triggers

A new ADR and append-only schema/policy/domain versions are required before changing:

• the ELF type, base, entry, headers, segment permissions, file layout, target placement, or section policy;
• workload profiles or runtime dispatch rules;
• startup syscall set, syscall argument restrictions, stack use, mapping state, target-call ABI, output decoding, or exit codes;
• input/output bytes, byte order, versions, limits, or EOF policy;
• any identity field, hash domain, canonical encoding, authority type, or independent replay rule;
• any hard cap, acceptance condition, or claim boundary;
• the separation between R1-S8 standalone correctness and Gate B <= 2.0x performance viability.