GitHub

ADR-0068: Sovereign enveloped-image finite native correctness

Status: accepted
Date: 2026-08-03
Decision owners: NAUX architecture and x86-64 execution boundary

Context

ADR-0067 accepts a complete self-owned x86-64 code image whose entry adapter, internal body, return path, Bounds path, rel32 graph, ABI state, and both predecessor projections independently replay. It deliberately grants no authority to map or execute those bytes.

The historical R1-S7b runner proves that the old raw target executes the frozen finite corpus, but importing that runner would make it the execution owner of the new sovereign image. ADR-0068 must establish a new authority boundary whose only code input is an opaque VerifiedX64TailEnvelopedImage witness.

Decision drivers

  • Execute only the exact verified ADR-0067 identity and entry point.
  • Own a minimal Linux x86-64 syscall and ABI-dispatch implementation without importing historical raw/native/process/standalone helpers.
  • Enforce one-way Unmapped -> RW -> RX -> Unmapped lifecycle with no RWX state, hash both mapped states, and fail closed on teardown.
  • Derive every argument lane and output interpretation from the verified target ABI; admit no fallback engine or callback.
  • Compare native outcomes and ordered effects against the ordinary verified target-plan evaluator over the frozen 51-case Gate A corpus.
  • Seal exact case/input/image/mapping/MXCSR/outcome evidence independently from host addresses, PIDs, and timing.
  • Keep process isolation, standalone artifacts, timing, claims, and global policy selection closed. Encoder policy remains 1.4.0.

Considered options

Call the historical R1-S7b runner with substituted bytes

Rejected. It would import legacy target-byte and execution authority rather than prove the new artifact boundary.

Reuse only the historical mapping helper

Rejected. The W^X lifecycle, hash stages, teardown semantics, and entry dispatch are part of this decision and must be locally owned and auditable.

Execute only one BranchMix smoke case

Rejected. It would demonstrate viability but not finite correspondence across numeric edges, branch directions, repetitions, NaN, and ordered Bounds cases.

New direct runner plus sealed finite correspondence

Accepted for implementation. In-process execution is the smallest authority increase after ADR-0067. Process containment remains a separate successor.

Decision

Introduce a sovereign x64_tail_enveloped_native module.

Execution admission

The runner accepts only:

  1. a target that passes the ordinary R1-S7a verifier;
  2. an opaque verified ADR-0067 witness bound to that exact target identity;
  3. typed CoreValue arguments matching the exact target entry manifest.

It rechecks the final image/code identity, nonempty bounded code extent, exact entry point, canonical zero-to-five input-lane order, hidden output-pointer register, two-word output area, and borrowed-array span safety before mapping.

Self-owned W^X lifecycle

One invocation owns exactly one anonymous private mapping. A new local Linux x86-64 syscall implementation performs:

  1. mmap as read/write, never executable;
  2. exact byte copy and ADR-0067-domain hash readback;
  3. mprotect to read/execute, never writable;
  4. second ADR-0067-domain hash readback;
  5. exact ABI call at the verified entry point;
  6. caller MXCSR comparison;
  7. mandatory munmap before returning any semantic result.

The mapping owner performs best-effort cleanup on unwinding, but successful evidence requires explicit teardown. A syscall failure, wrong hash, invalid entry, malformed output, foreign array result, or MXCSR drift returns no successful execution witness.

Finite correspondence

The correspondence emitter regenerates the canonical 51-case Gate A manifest. BranchMix cases select the exact verified BranchMix target/image pair; Bounds cases select the exact verified ordered-Bounds pair. For every case it:

  • regenerates and checks the canonical input hash;
  • derives the exact typed arguments;
  • evaluates the ordinary verified target plan under the canonical budget;
  • invokes the sovereign ADR-0067 runner;
  • compares return bits with canonical NaN handling, typed Bounds outcome, and exact ordered effect trace;
  • seals the case ordinal, workload, input hash, target/image/code identities, entry/lanes, RW/RX hashes, mapping trace, MXCSR, outcome/effects, teardown, and fallback=false.

The aggregate evidence binds the canonical corpus manifest and ordered record hashes. Verification regenerates the manifest and every semantic oracle result; it never trusts supplied observation ordering or record seals alone.

Authority boundary

This ADR admits finite in-process native correctness only. A malformed machine image can still fault the hosting process; therefore arbitrary/untrusted image execution and process containment remain closed. No standalone, ELF, timing, performance claim, or encoder-policy selection authority is granted.

Frozen limits

  • Linux x86-64 only, exactly one mapping per invocation;
  • at most 128 MiB mapping, five input lanes, two borrowed F64 arrays, two output words, four mapping-state events, one semantic effect, 64 records, and exactly 51 admitted finite-corpus records;
  • canonical execution budget derived from the existing Gate A/target-plan contract, never caller-selected for accepted evidence;
  • bounded canonical evidence encoding and checked arithmetic for every span, offset, length, count, and work metric.

Consequences

  • The sovereign path can prove that its exact complete image runs correctly on the frozen finite corpus without borrowing legacy execution authority.
  • The unsafe surface is explicit and small: local syscalls, function-pointer dispatch, borrowed array spans, and result decoding.
  • Process isolation is the mandatory next authority step before hostile fault containment or standalone composition.
  • Correctness evidence is not cycle, throughput, or performance evidence.

Acceptance gates

  1. Unit/Bool/I64/F64/F64Array returns, zero through five lanes, both branch directions, ordered Bounds, array identity, and caller MXCSR restoration pass through the new exact ADR-0067 image with no fallback.
  2. All 51 canonical cases preserve exact target-plan outcome bits, canonical NaN, Bounds, and ordered effects; the ordered aggregate identity is locked.
  3. RW and RX hashes equal the verified ADR-0067 code hash, lifecycle is exactly Unmapped/RW/RX/Unmapped, entry point is exact, and teardown is mandatory.
  4. Wrong target/image/entry/input/type/lane/span/output/hash/MXCSR/lifecycle, locally resealed record, reordered/duplicated/missing case, and aggregate mutation fails closed.
  5. Production imports no historical raw/native/process/standalone/measurement helper and exposes no fallback, generic byte execution, or executable image constructor.
  6. Focused, public-boundary, full-workspace, strict lint, governance, refinement, format/diff, and static authority gates pass.
  7. The ADR-0057 through ADR-0067 predecessor vector is migrated only through its dated correctness errata; target identities and encoder policy 1.4.0 remain unchanged, while process/standalone/timing/claim authority remains closed.

Accepted evidence

The canonical 51-case finite correspondence is accepted under evidence root defef43d36e6eb01d21ef5cb3a2f89d74b675fff42a819e940aec9cbbd29e3d2. All 51 records replay the ordinary verified target-plan oracle exactly, carry fallback=false, perform mandatory teardown, and preserve ordered effects and exact result bits including the loop-carried IEEE-754 edge 0x8000000000000004. Native execution enters under target-canonical MXCSR, while scoped restoration preserves the embedding thread’s ambient MXCSR even when the Rust oracle has changed sticky flags.

RW and RX readback hashes equal the independently verified ADR-0067 code hash; the mapping trace is exactly Unmapped -> RW -> RX -> Unmapped, never RWX. Opaque verifier replay succeeds, while a locally resealed semantic mutation is rejected by regenerated oracle evidence. Production imports no historical raw/process/standalone/measurement helper, exposes no raw-byte execution or fallback path, and keeps global encoder policy 1.4.0.

This is finite native-correctness and W^X lifecycle evidence. It is not process containment, arbitrary-program correctness, cycle, throughput, or performance evidence.