ADR-0038: Verifier-Gated W^X Native Runner

Status: accepted; R1-S7b-a/b/c implemented and locally validated

Date: 2026-07-29

Historical scope: this extension left the then-current ADR-0037 policy-1.0.0 bytes unchanged. ADR-0042 later migrated the encoder and every derived identity together while preserving this runner’s schema, ABI, verification relation, and W^X rules.

Extends: ADR-0037 without changing, at this decision’s acceptance time, the frozen R1-S7a target schema, lowering policy, encoder policy, ABI, code bytes, identities, or hard limits

Context

ADR-0037/R1-S7a now closes this checked boundary:

source-bound Machine IR
  → canonical Linux x86-64/SSE2 target plan
  → NAUX-owned position-independent bytes

The bytes are re-encoded and source-replayed, but deliberately unexecuted. Calling the target-plan evaluator “native execution” would be false. Reusing the bridge trace-JIT loader would also weaken the new trust boundary because that loader accepts a different IR, owns a different ABI, can call runtime helpers, and is not source-bound to the R1-S7a artifact.

R1-S7b must answer one narrower question:

Do the exact verified R1-S7a bytes, entered through their exact ABI on an admitted Linux x86-64 host, preserve the source-bound Machine IR outcome and ordered effects on the fixed finite corpus?

This is native correctness evidence. It is not yet standalone Gate B, performance evidence, Futamura P1, or production sovereignty closure.

Options considered

Decision

1. Input authority

The native runner accepts only:

SourceBoundX64TargetArtifact

It never accepts raw bytes, an X64TargetArtifact, a local-only verified view, copied hashes, a trace-JIT executable, or a caller-selected entry address.

The runner reads code bytes, entry offset, ABI, result type, plan/code/artifact hashes, and source Machine IR identity only through that opaque view.

2. Platform boundary

R1-S7b v1 is exactly:

architecture    x86-64
operating system Linux
calling ABI     NauxLighthouseSysV1
feature floor   SSE2
code model      one position-independent blob

The bridge implementation uses a small NAUX-owned raw Linux x86-64 syscall shim for mmap, mprotect, and munmap. S7b-c separately owns raw kill and waitid calls for process-group containment and race-free exit observation. These paths do not import the trace-JIT loader or call libc wrappers. Rust/rustc/Cargo remain acknowledged seed debt; the syscall ABI is the accepted platform boundary under INV-003.

3. W^X state machine

One mapping follows exactly:

Unmapped
  → ReadWrite
  → ReadExecute
  → Unmapped

The runner:

1. rechecks the opaque artifact and exact host descriptor;
2. allocates anonymous private RW memory with no execute permission;
3. copies exactly the verified code length;
4. hashes the copied bytes and compares the locked code hash;
5. changes the same mapping to RX;
6. hashes the readable RX bytes again;
7. enters only mapping_base + entry_offset;
8. unmaps on every normal result or pre-entry error.

No state grants write and execute simultaneously. No post-RX patching, relocation, lazy binding, adaptive rewrite, or fallback is permitted.

4. Host input boundary

The safe runner API accepts typed borrowed values, not arbitrary host descriptors. It derives the flattened integer lanes itself.

For F64Array, it derives data and length from an immutable borrowed slice, checks the complete R1-S7a span rules, and keeps the owner alive for the invocation. The output area is runner-owned, two words, eight-byte aligned, and disjoint from every input span.

Parameter count, flattened lanes, canonical Unit/Bool/F64 bits, result type, and output register must match the exact target entry ABI.

5. Entry and numeric state

The runner has six fixed System V entry templates, one for each admitted lane count 0..=5. The output pointer occupies the exact next register declared by R1-S7a. There is no variadic call, stack argument, C aggregate ABI, or caller-selected function signature.

Immediately around entry, the runner records caller MXCSR. The native blob must return with the complete caller MXCSR restored. The fixed target prologue/epilogue remains responsible for installing 0x00001f80 while executing.

Only native tag Return=0 and Bounds=1 are admitted. The runner validates the complete two-word payload before converting it to a typed semantic outcome. Unknown tags and noncanonical payloads fail closed.

6. Native execution evidence

Each execution record binds:

runner schema and policy
target artifact hash
target plan hash
verified code hash
source Machine IR hash
entry offset and ABI hash
canonical input hash
pre-RX copied-code hash
post-RX code hash
native outcome and ordered effects
caller MXCSR before and after
mapping-state trace
fallback = false

Manual domain-separated encoding produces a record hash. A separate order-sensitive result hash covers the fixed 51-case corpus. Machine-IR and native observations must match under the same exact-bits/canonical-NaN/Bounds relation used by R1-S7a.

Loader syscall numbers, addresses, wall-clock timeout, PID, ASLR, and engine-local work are telemetry and do not enter semantic result identity.

7. Crash boundary

The library runner is for trusted, verifier-produced artifacts and safe borrowed inputs. It cannot convert a synchronous native fault into a Rust error in the same process.

Therefore claim-bearing corpus evidence runs each native invocation in a dedicated child process controlled by a parent harness. A signal, abnormal exit, timeout, missing record, or truncated record is a failed case, never a skip or fallback. This is test containment, not a claim that arbitrary malicious machine code is sandboxed.

The parent accepts a caller-supplied worker path. It authenticates neither the worker executable nor its build provenance, loader, shared objects, inherited working directory, or inherited environment. Canonical execution removes the debug-probe variable, but is not a hermetic launch. Consequently the reviewed naux-r1-s7b-worker executable in a controlled environment is an explicit operational precondition. Frame seals and deterministic receipts validate protocol and semantic binding; they are not executable attestation, proof that a hostile substitute entered the claimed bytes, or freshness against frame replay.

8. Claim boundary

Passing R1-S7b under the trusted canonical-worker operational precondition permits only:

The exact R1-S7a code bytes executed natively and matched source-bound Machine IR on the declared finite corpus with verifier-gated W^X loading and no fallback.

It does not establish:

• an ELF/object writer, linker, startup runtime, or standalone executable;
• general safety for hostile pointers or arbitrary raw bytes;
• worker-executable identity, hermetic launch, build-provenance attestation, or replay freshness;
• infinite-domain equivalence or formally verified x86-64 semantics;
• Gate B viability, Gate C performance, performance leadership, or P1;
• removal of Rust/Cargo/egg debt or Nauxogenesis.

Rationale

1. Artifact-only admission preserves the full Core→SSA→Machine IR→target provenance chain at the first executable boundary.
2. A dedicated raw-syscall mapping shim prevents bridge JIT or libc-wrapper behavior from becoming accidental loader authority. The surrounding Rust seed process remains platform-runtime debt; long-term libc-free closure is still a Gate B/sovereignty obligation.
3. W^X plus pre/post protection hashing proves which immutable bytes were entered.
4. Fixed lane-count templates make the nonstandard lighthouse ABI explicit and auditable.
5. Child-process evidence converts faults and hangs into failed cases without pretending an in-process signal recovery scheme is sound.
6. Separating native correctness from standalone viability and performance keeps every later claim falsifiable.

Consequences

Positive:

• the first native invocation remains source-bound and fallback-free;
• the loader has no assembler, linker, libc wrapper, runtime callback, or JIT dependency;
• mapping state, copied bytes, entry identity, ABI, outcome, and numeric-state restoration become independently checkable evidence;
• the exact same frozen 51 cases extend through a real processor.

Negative:

• Linux x86-64 receives a dedicated implementation and evidence harness;
• the six entry templates duplicate a small amount of ABI code;
• child-process corpus execution is slower than an in-process test;
• faults before record publication yield only containment metadata;
• Rust remains the seed used to build the runner.

Acceptance

Implementation progress

R1-S7b-a now implements:

• opaque SourceBoundX64TargetArtifact admission;
• typed CoreValue input flattening and borrowed immutable F64-array spans;
• a NAUX-owned inline-assembly Linux x86-64 syscall shim for mmap, mprotect, and munmap;
• exact RW copy/hash → RX read-back/hash → entry → unmap sequencing;
• all six 0..=5 integer-lane entry templates, including R9 output;
• canonical Unit/Bool/I64/F64/F64Array/Bounds decoding;
• full caller-MXCSR equality checks and explicit no-fallback records.

R1-S7b-b now implements:

• an opaque case-aware runner that regenerates the Gate A input hash and derives the actual native arguments from the canonical case;
• exact 1.0.0 evidence, runner, syscall, and entry-dispatch policy identities plus the frozen eleven-field limit vector;
• manual big-endian, domain-separated canonical ABI, execution-record, correspondence-record, and ordered corpus-result identities;
• canonical exact-bit/canonical-NaN/Bounds observations with exact ordered effects and nested record verification;
• exact 51-case manifest/ordinal/input admission and one stable target identity per workload;
• mutation rejection for hashes, case binding, limits, mapping/code state, claim MXCSR, fallback, semantic observations, corpus order/count, manifest, mixed workload targets, and aggregate seal.

At this decision’s policy-1.0.0 acceptance, the focused ten-test S7b-a/b suite passed and the in-process result was 5b55f00ad40bb3f30514742aa9f4c0739de187090f609a1fdf43806bd3b615b3. R1-S7b-c now adds:

• a dedicated naux-r1-s7b-worker child for each canonical case;
• child-side independent R1-S4→S7a regeneration and source replay;
• a distinct big-endian, 16 KiB-bounded IPC domain with nested and outer seals;
• concurrent bounded pipe draining, a fresh process group, a frozen 30-second timeout, group kill plus bounded waits for reader/reap completion, and no retry;
• parent-side independent Machine IR evaluation and exact target, ABI, entry, and lane binding for the untrusted child record;
• typed rejection of signal, abnormal exit, timeout, missing, malformed, truncated, concatenated, trailing, oversized, diagnostic-overflow, wrong-case, and fallback evidence;
• locked historical policy-1.0.0 process vectors and isolated corpus result 9c3379f3d4f50dd88af459c435471efe37c9d5ad7abdd3c6ad7c3e765425f073.

ADR-0042 and the normative runner contract publish the migrated policy-1.3.0 identities. Within this historical acceptance state, the semantic result remained unchanged by process containment. R1-S7b is implemented and locally validated because:

• the normative runner contract and exact policies/limits are implemented;
• non-Linux/non-x86-64 hosts fail closed without compiling an executable path;
• only an opaque source-bound R1-S7a view reaches allocation;
• the raw syscall shim is independent of libc and the bridge JIT;
• exact RW→RX→unmapped transitions and both copied-code hashes are checked;
• all six lane-count entry templates have focused evidence;
• typed input/output admission and caller MXCSR restoration are tested;
• changed byte/hash/entry/ABI/mapping state/input/output/fallback records fail;
• the fixed 51 cases pass Machine-IR-versus-native correspondence in the process-isolated harness;
• record/result vectors and representative failure vectors are locked;
• all predecessor and repository quality gates remain green;
• documentation continues to label standalone Gate B, performance, P1, and sovereignty closure as open.

Revisit trigger

A new ADR and append-only runner policy are required before:

• another OS, ISA, calling convention, feature profile, or code model;
• stack arguments, direct calls, external symbols, callbacks, syscalls from generated code, or runtime allocation;
• post-load patching, dynamic linking, object/executable loading, or multiple code mappings;
• writable arrays, aliasing output with input, or a raw-pointer public API;
• executable measurement, hermetic worker launch, nonce-bound freshness, or remote attestation;
• claiming process sandboxing, standalone viability, or performance.

Related decisions

• ADR-0008 defines sovereignty above the ISA/firmware/syscall boundary.
• ADR-0036 defines the source-bound target-independent Machine IR.
• ADR-0037 defines the only target artifact and ABI accepted here.
• The normative details are in ../x86_64_native_runner_r1_s7b_contract.md.