Canonical x86-64 Native Runner R1-S7b Contract

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

Stage: Roadmap Stage 3 / native correctness before standalone Gate B

Decision: ADR-0038

Predecessor: x86_64_target_r1_s7a_contract.md

1. Purpose and exact claim

R1-S7b is the first execution boundary for canonical NAUX-generated bytes.

It must establish:

eval_MachineIR(source-bound artifact, input)
≈
execute_native(exact verified R1-S7a bytes, admitted host input)

for the fixed bounded corpus, while preserving exact non-NaN F64 bits, canonical NaN, terminal Bounds, ordered effects, ABI behavior, code identity, and caller numeric state.

The relation is finite translation validation, not an infinite-domain theorem. R1-S7b does not itself establish standalone Gate B or performance. For the S7b-c process form, this claim is conditional on the trusted canonical-worker operational precondition in section 12.1; the process receipt is not executable attestation.

2. Claim split

R1-S7a  target plan + checked raw bytes + plan correspondence
R1-S7b  verifier-gated byte execution + native correspondence
Gate B  standalone artifact and bounded viability
Gate C  controlled performance differentiation
P1      Gate A + structural erasure + Gate B + Gate C + reproduction

No result from a later-looking bridge JIT path can satisfy an earlier missing gate.

Implementation is split without splitting the final claim:

R1-S7b-a  safe in-process artifact/input/W^X/ABI/output runner
R1-S7b-b  canonical execution and correspondence evidence identities
R1-S7b-c  process-isolated fixed 51-case replay and locked results

S7b-a, S7b-b, and S7b-c are implemented. The process-isolated corpus and all R1-S7b acceptance evidence are locally validated; standalone Gate B remains separate and open.

Current implementation evidence:

runner module          naux-lang/src/core/x64_native.rs
IPC/process modules    x64_native_ipc.rs + x64_native_process.rs
worker binary          naux-r1-s7b-worker
focused suites         core_x64_native_r1_s7b + core_x64_native_process_r1_s7bc
                       + core_x64_native_ipc_adversarial_r1_s7bc
focused result         10 S7b-a/b tests + 4 S7b-c integration tests; all pass
native corpus          branch_mix=46 Bounds=5 total=51
manifest hash          0c4e4e796d60d571c874fd37b87e0418e1240f469a03672a6a4af4a4047b4e8f
encoder authority     R1-S7a policy 1.4.0
S7b-b results hash     73ecf90e2fff7a36a6011e447c0982ca317f591aea45486f55c330d8dc12d22c
S7b-c isolated hash    7700c126528db9bbe810f5396129d155da407d365e1dfa12e346adfbd5df37e1
execution mode         one independently regenerating child per canonical case

The canonical W^X mapping shim calls no libc wrapper or bridge-JIT loader API. It uses the owned raw syscall path, checks both copied code hashes, exercises all lane counts through R9, preserves altered caller MXCSR, decodes every admitted result family, and matches Machine IR on all 51 frozen cases without fallback. The surrounding Rust seed binary still uses std and its platform runtime; this is not libc-free standalone closure. S7b-b now adds an opaque case-aware invocation boundary, canonical ABI and exact limit identities, nested execution/correspondence seals, exact Gate A manifest admission, per-workload target consistency, mutation rejection, and the locked result above. S7b-c adds one dedicated worker process per case, bounded canonical IPC, parent-side artifact/ABI/entry/lane verification, independent Machine IR evaluation, fault/timeout admission, and a distinct isolated result identity. This completes only finite native correctness; it does not produce a standalone NAUX executable.

3. Exact host descriptor

The only v1 host is:

Admission compares this descriptor with the exact R1-S7a artifact before any mapping is allocated. No CPUID-selected encoder, AVX/FMA path, relaxed F64 mode, alternate OS ABI, or host-dependent code rewrite exists in v1.

4. Runner input authority

The authoritative API consumes an opaque:

SourceBoundX64TargetArtifact

That view can only be produced by complete R1-S7a verification and source replay. The runner must not expose a parallel constructor from:

• &[u8];
• X64TargetArtifact;
• VerifiedX64TargetArtifact;
• a code/plan/artifact hash tuple;
• an address and length;
• an existing trace-JIT executable.

Before allocation, the runner checks:

• exact R1-S7a schema, lowering policy, encoder policy, ABI, and hard limits;
• entry_offset == 0 and lies inside the non-empty code blob;
• exact plan, code, and complete-artifact identities from the opaque view;
• exact source Machine IR identity;
• code length within the inherited 64 MiB cap;
• the fixed runner policy and host descriptor.

5. Typed host invocation

5.1 Safe values

The public invocation boundary is typed:

Unit
Bool
I64
F64Bits
BorrowedF64Array

BorrowedF64Array is created from an immutable borrowed slice. The runner derives its pointer and length and retains the borrow for the whole call. A public caller cannot provide an unchecked data,length pair.

Input arity and types must exactly match entry_abi.parameter_types.

5.2 Canonical scalar lanes

Unit  contributes no entry lane
Bool  contributes one lane equal to 0 or 1
I64   contributes exact two's-complement bits
F64   contributes exact IEEE-754 bits
Array contributes data then element length

The flattening order and maximum five lanes are inherited unchanged from R1-S7a. F64 inputs remain integer-lane bit patterns.

5.3 Array admission

For each borrowed F64 array:

length <= i64::MAX
length * 8 does not overflow
data + length * 8 does not overflow
length > 0 implies data != 0
the span remains immutable and alive through native return

The runner additionally proves that its two-word output area does not overlap any non-empty input span. At most two array inputs can fit the five-lane ABI.

5.4 Canonical input identity

Claim-bearing evidence uses the existing Gate A case input_hash. A general safe invocation is deliberately not claim-bearing. The S7b-b case-aware API regenerates the supplied Gate A case hash, derives the complete typed argument vector from that case, runs the safe runner, and returns an opaque case-execution value. Only that opaque value can enter the canonical execution record sealer. A caller cannot pair arbitrary arguments with a separately supplied case hash.

Raw process addresses never enter canonical input identity.

6. Output ownership and decoding

The runner owns:

align8 OutputArea {
  word0: u64,
  word1: u64,
}

It initializes both words with a noncanonical sentinel before entry. On normal return it accepts only:

EAX=0  Return
EAX=1  Bounds

Payload validation is exact:

An array result must match one complete admitted input descriptor. The runner returns the corresponding safe borrow/owned semantic handle, never a new safe slice built from an unknown native pointer.

Unknown tags, sentinel residue, non-zero reserved words, noncanonical Bool, noncanonical NaN, or a foreign/partial array descriptor fail closed.

Bounds produces exactly one ordered Error(Bounds) effect. Return produces no effect.

7. Linux syscall shims

The R1-S7b W^X mapping path owns this minimal x86-64 Linux syscall shim:

mmap      9
mprotect 10
munmap   11

The S7b-c parent additionally owns the process-containment calls:

kill      62
waitid   247

Both shims use the Linux x86-64 syscall register ABI directly. The mapping shim calls no libc wrapper, declares no libc symbol, and depends on no libc crate or bridge-JIT FFI API. The process shim observes the direct child with WEXITED|WNOHANG|WNOWAIT before killing its process group, which prevents PID/PGID reuse between observation and group termination.

Every raw return in [-4095, -1] is an error. Syscall errors are typed by operation and raw errno for diagnostics, but errno is non-semantic telemetry.

Generated target code itself contains no syscall; all five calls belong to the Rust seed loader/process harness.

8. Mapping state machine

The only legal state trace is:

0 Unmapped
1 ReadWrite
2 ReadExecute
3 Unmapped

Detailed algorithm:

1. Reject an empty or oversized code blob.
2. mmap(NULL, code_len, READ|WRITE, PRIVATE|ANONYMOUS, -1, 0).
3. Reject a syscall error or null mapping.
4. Copy exactly code_len verified bytes once.
5. Read back and hash exactly code_len bytes.
6. Require the copied hash to equal the artifact code hash.
7. mprotect(mapping, code_len, READ|EXECUTE).
8. Read back and hash exactly code_len RX bytes.
9. Require the RX hash to equal both copied and artifact code hashes.
10. Enter exactly mapping + entry_offset.
11. On normal semantic return, munmap(mapping, code_len).

Forbidden:

• WRITE|EXECUTE in any syscall;
• a second code mapping;
• relocation or patching after copy;
• changing RX back to writable;
• executing before both hash checks;
• entering an interior/caller-selected offset;
• retaining a callable pointer after unmap;
• treating unmap failure as a successful evidence record.

RAII may guarantee best-effort unmap on a pre-entry error. A claim-bearing record is published only after the required final unmap succeeds.

9. Fixed entry dispatch

The runner implements exactly six System V function signatures:

0 lanes: (out)
1 lane : (a0, out)
2 lanes: (a0, a1, out)
3 lanes: (a0, a1, a2, out)
4 lanes: (a0, a1, a2, a3, out)
5 lanes: (a0, a1, a2, a3, a4, out)

Every argument is an integer register-sized word; out is the final declared register through R9. The chosen template must equal the artifact lane count and output register.

There is no variadic function pointer, stack argument, transmuted arbitrary signature, external call, callback, unwind, or fallback.

10. MXCSR and processor state

Before entry the runner records the complete caller MXCSR. The R1-S7a prologue must save it and install 0x00001f80; every semantic Return/Bounds epilogue must restore it.

Immediately after normal native return, the runner records MXCSR again and requires exact equality with the caller value. This is tested with a deliberately noncanonical caller rounding mode as well as the normal mode.

The runner itself does not normalize the caller MXCSR to hide a target bug. Process registers, flags, stack address, ASLR, and timestamps are not semantic evidence.

The general safe runner continues to accept and restore an altered valid caller MXCSR. Canonical S7b-b claim records are narrower: immediately before the native invocation the evidence emitter must establish the target value 0x00001f80, and the execution-record sealer rejects any other starting value. This makes the locked corpus identity reproducible while preserving the separate altered-caller restoration test.

11. Execution and correspondence identities

11.1 Versions and domains

S7b-b freezes these exact version triples:

runner schema          0.1.0
runner policy          1.0.0
syscall policy         1.0.0
entry-dispatch policy  1.0.0
evidence schema        1.0.0
process schema         1.0.0
process policy         1.0.0
IPC schema             1.0.0

Manual big-endian encodings use these separate non-empty domains:

canonical ABI          NAUX:x86-64:r1-s7b:abi:v1\0
native execution       NAUX:x86-64:r1-s7b:execution:record:v1\0
native correspondence  NAUX:x86-64:r1-s7b:correspondence:record:v1\0
native corpus results  NAUX:x86-64:r1-s7b:correspondence:results:v1\0
IPC success record     NAUX:x86-64:r1-s7b:ipc:record:v1\0
process receipt        NAUX:x86-64:r1-s7b:process:receipt:v1\0
isolated results       NAUX:x86-64:r1-s7b:process:results:v1\0

Rust enum discriminants, struct layout, debug output, map iteration, raw addresses, PID, and syscall return addresses are forbidden from identity. The process/IPC domains are distinct from every S7b-b semantic domain.

11.2 Native execution record

The semantic execution record contains:

schema/policies
exact v1 limit vector
target artifact hash
target plan hash
target code hash
source Machine IR hash
entry offset
canonical ABI hash
canonical input hash
copied RW code hash
read-back RX code hash
actual entry-lane count
mapping-state tags [Unmapped,RW,RX,Unmapped]
MXCSR before
MXCSR after
native outcome
ordered effects
fallback=false
record hash

For claim records, MXCSR before and after are both exactly 0x00001f80. Altered-caller runs remain safe-runner restoration evidence but cannot be sealed into the fixed result identity. Addresses and errno do not enter this record.

11.3 Correspondence record

For every canonical case:

case ordinal
input hash
source Machine IR hash
target artifact/code hashes
Machine IR observation
native observation
native execution record hash
correspondence record hash

Machine IR and native observations must be identical after canonical NaN classification. Engine-local work is excluded.

11.4 Result hash

The result hash:

• includes the exact corpus manifest hash and record count;
• requires ordinals exactly 0..50;
• includes ordered correspondence record hashes;
• rejects omission, duplication, permutation, or a changed target identity within either workload (branch_mix and Bounds retain their distinct canonical artifacts);
• is separate from R1-S7a plan-correspondence result hash.

The current policy-1.4.0 S7b-b vectors are:

branch canonical ABI     ab26fb28cfa96a592aa653e7f21dd0273ca3dd0852fd4f7792e0792a77e143f6
branch execution record  f1cb4fe7dd9ebcb68a9e074600dca0ed30df7e922fdabfdeb74077f83a39d960
branch correspondence    7e930116fc944609f60a353c7a8765804a355e4f38d495a39203f04dbc55fed2
Bounds canonical ABI     1b840fdf4f4bfb3d2bb4b47486ca2b7707d4d2b87017ed29af8928dac0055ecf
Bounds execution record  0d77cc2def6e1479ddb1d9fb8a7e5a0c55a15e565c3f31867ba08bbe94fd6a2f
Bounds correspondence    1bf46e6d2bf164197e5999b71f4101ad9d2d1e80853af7208feb6c9a825dbc49
fixed corpus results     73ecf90e2fff7a36a6011e447c0982ca317f591aea45486f55c330d8dc12d22c

The representative branch vector is case 0; the Bounds vector is case 46. These are in-process S7b-b identity vectors, not S7b-c containment evidence.

The historical encoder-policy-1.3.0 S7b-b vectors are retained below and are superseded as current authority:

branch canonical ABI     ab26fb28cfa96a592aa653e7f21dd0273ca3dd0852fd4f7792e0792a77e143f6
branch execution record  2a2b67b9e65f4c644936a4a52b6d7da3fc4172c9b33e9cfd5e2f0771dd7ce36d
branch correspondence    8f3e58004cba6fbba3b6019ba057f8afbb1eb8d90a4162f1d185540627a3ea3f
Bounds canonical ABI     1b840fdf4f4bfb3d2bb4b47486ca2b7707d4d2b87017ed29af8928dac0055ecf
Bounds execution record  82a954ecc3ed79ee97800065dd591c06b880c049f095a48bf42816cc18e2543b
Bounds correspondence    2d32c87906aa8816b83588e68a14c569e13ab26bb36feffab63f200b64acb4ff
fixed corpus results     1d1134bd2cd01161c9437a2b0676a01d0844f9d747e168c72bba350dcbb3614c

They must not be combined with policy-1.4.0 target or standalone evidence.

12. Process-isolated evidence harness

The public safe runner may execute in the current trusted process. The fixed claim-bearing corpus must execute through a parent/child harness:

1. parent selects one canonical case and expected artifact;
2. child regenerates or receives only canonical non-pointer case data;
3. child independently obtains the opaque source-bound artifact;
4. child runs one native invocation and serializes one bounded record;
5. parent accepts only normal exit plus one complete canonical record;
6. parent seals the correspondence record and aggregate result hash.

A signal, abnormal status, timeout, missing/trailing bytes, invalid record, wrong case, or fallback is a failed case. The parent never interprets partial child output as semantic evidence.

The timeout is containment telemetry, not a semantic result and not a proof of termination.

S7b-c freezes a 30,000 ms per-case timeout policy. The parent uses std::process::Command, never raw post-fork Rust execution. It pipes and concurrently drains bounded stdout/stderr, places each worker in a fresh process group, kills that group after direct-child exit or timeout, bounds the wait for reader completion and reap, and performs no retry. A debug probe proves that an in-group descendant inheriting both pipes is terminated without hanging the parent.

12.1 Worker launcher trust boundary

The public process APIs accept a caller-supplied worker_path. R1-S7b v1 does not canonicalize that path, pin an inode, hash or sign the worker executable, measure its loader or shared objects, or authenticate its build provenance. The focused integration suite supplies Cargo’s absolute CARGO_BIN_EXE_naux-r1-s7b-worker path; supplying the reviewed canonical worker is an operational precondition of claim-bearing use.

Canonical runs remove NAUX_S7B_WORKER_DEBUG_PROBE, but otherwise inherit the parent working directory, environment, credentials, namespaces, filesystem view, and dynamic-loader policy. Process-group isolation, bounded pipes, timeout, kill, and reap are fault-containment mechanics; they do not make that launch environment hermetic or trusted.

The parent verifies the returned frame against independently regenerated cases, target identities, ABI/entry/lane binding, and Machine IR observations. This proves that an accepted frame conforms to the frozen protocol and semantic relation. It does not cryptographically attest which executable produced the frame, prove that a hostile replacement worker actually entered the claimed native bytes, or provide freshness against replay of the deterministic corpus. Those conclusions rely on the trusted canonical-worker precondition. Executable measurement, hermetic launch, nonce-bound freshness, or remote attestation require a new policy and are outside R1-S7b.

The child receives exactly one canonical decimal case ordinal. It regenerates the manifest and the selected workload, independently rebuilds R1-S4→R1-S5→R1-S6→R1-S7a, source-replays the target, establishes claim MXCSR, executes exactly once, and writes one frame then EOF.

The parent establishes the same canonical MXCSR only around its independent Machine IR oracle and restores the complete preexisting caller value through an RAII guard. The child-side frame primitive uses the same save/restore discipline, so even diagnostic library use cannot silently change the calling thread’s numeric environment.

The canonical big-endian success frame binds:

IPC schema and process policy
exact Gate A manifest hash
case ordinal
bounded body length
complete native execution-record fields and semantic seal
outer IPC frame seal

Before correspondence sealing, the parent independently verifies the nested seal, canonical input, target artifact/plan/code/source identities, canonical ABI hash, exact entry offset, and exact entry-lane count. It then evaluates Machine IR itself. Child-supplied behavior never becomes the Machine IR oracle.

The current policy-1.4.0 S7b-c vectors are:

case 0 IPC frame       73656da5263d0b2f948af0d65b70e62ef9a2de784c5007418fbeec806dd02511
case 0 receipt         649f8a0dcfde3ef8241a6c088c2be699b00ff9b3d4288dd197e1d02333f38c36
case 46 IPC frame      bac6b841c3df6343b81e31254c09ebfb4b5683eabbed89b1d282dfbff2803a58
case 46 receipt        7e573ecb93cd365c966232c402059de1431e5cd815c24e2de7f647a350496fa1
isolated corpus result 7700c126528db9bbe810f5396129d155da407d365e1dfa12e346adfbd5df37e1

The nested semantic corpus result is the current S7b-b hash 73ecf90e2fff7a36a6011e447c0982ca317f591aea45486f55c330d8dc12d22c; process containment does not rewrite semantic identity.

The historical encoder-policy-1.3.0 S7b-c vectors are:

case 0 IPC frame       562a35da8259821fb1973917a44d9e07f56d6c621770e7250e45940f0726da70
case 0 receipt         217149a689f03a33cb909db26317b3d884cbcb2826399a03a60c1f0f0e053857
case 46 IPC frame      65f4cf0bd00f41091c5b6ef08e349bb7bacdc7ff894bd19cc02155762823be73
case 46 receipt        bc52759a7b4e785ab239d6a5b8cc7cfb878e30e4e1347cb620c300a8a7fd3b8b
isolated corpus result 4b3c0e30c330cc4d1e8429d87074d394d4de955c343434c51549220b5ee4dc96

The historical nested semantic corpus result was the S7b-b hash 1d1134bd2cd01161c9437a2b0676a01d0844f9d747e168c72bba350dcbb3614c; these values remain predecessor evidence only.

13. Exact v1 limits

S7b-b freezes and encodes this exact vector in every execution record:

The inherited target code cap cannot be widened by the runner. S7b-b mutation evidence rejects a changed limit vector. S7b-c exercises the IPC-facing exact 16,384-byte boundary and 16,385-byte rejection, interprets Diagnostics as newline-delimited stderr records, accepts at most 128 for bounded collection, and rejects every diagnostic on a successful claim record. Total captured diagnostic bytes are separately capped at 16,384.

14. Fail-closed errors

Typed errors distinguish at least:

UnsupportedHost
InvalidSourceBoundArtifact
HostDescriptorMismatch
InputArityMismatch
InputTypeMismatch
NonCanonicalInput
InputSpanOverflow
InputOutputOverlap
CodeLimit
MappingFailed
CopyHashMismatch
ProtectFailed
RxHashMismatch
EntryAbiMismatch
UnknownOutcomeTag
NonCanonicalOutput
ForeignArrayResult
MxcsrNotRestored
UnmapFailed
NativeFault
NativeTimeout
FallbackObserved
EvidenceMismatch
LimitExceeded
MetricOverflow

No error silently evaluates the target plan, bridge VM, interpreter, or trace JIT.

15. Required positive evidence

• exact host and source-bound artifact admission;
• RW copy hash and RX read-back hash equal locked code identity;
• mapping trace is exactly Unmapped→RW→RX→Unmapped;
• all six lane-count dispatch templates use the declared output register;
• Unit/Bool/I64/F64/F64Array Return payload decoding;
• canonical NaN and signed-zero preservation;
• zero/non-zero arrays and zero/non-zero repetitions;
• negative, exact-last, and one-past Bounds behavior;
• both branch directions and proper tail-loop execution;
• caller MXCSR restoration from normal and altered caller modes;
• no fallback/callback/external symbol;
• all 51 cases match source-bound Machine IR;
• deterministic record/result hashes and process-isolated replay.

16. Required negative evidence

• raw/local-only target admission attempts;
• wrong host, schema, policy, target, ABI, feature, entry, or code identity;
• changed byte before copy, after copy, or claimed in a record;
• empty/oversized mapping and syscall failure;
• any requested RWX state, skipped protection, state reordering, or second mapping;
• wrong lane count/output register/function signature;
• wrong input arity/type, noncanonical Bool, span overflow, null non-empty array, and output overlap;
• unknown outcome, residue sentinel, wrong reserved word, noncanonical Bool or NaN, and foreign array result;
• changed caller MXCSR on Return or Bounds;
• omitted/reordered/duplicated/mixed-artifact corpus records;
• signal, abnormal child exit, timeout, malformed IPC, and fallback;
• every representative one-over/overflow boundary.

A fully resealed behavior mutation must either fail source replay before allocation or produce a different locked native results identity.

17. Repository gates

The S7b-b focused suite is green with ten tests, including the exact 51-case package and failures for case mutation, limit widening, copied-code identity, claim MXCSR, fallback, semantic mismatch, omission, permutation, manifest, input, per-workload target, ABI/entry/lane binding, and result-seal mutations.

The four-test S7b-c focused suite is green. Its locked replay covers all 51 fresh child processes; the remaining process and adversarial-codec tests lock representative IPC/receipt and isolated-result vectors and reject signal, nonzero exit, timeout, inherited-pipe descendants, empty, malformed, truncated, concatenated, trailing, wrong-case, exact-limit-invalid, one-over, diagnostic-count/byte overflow, valid-frame-then-signal, and valid-frame-then-abnormal-exit cases. Independently resealed mutations cover header identities, declared body lengths, all mapping tags, outcome/effect tags, mapping/effect counts, fallback, the nested execution seal, and every strict frame prefix. Fast unit tests separately cover receipt omission/order/input/seal/frame binding mutations and exact capture boundaries.

R1-S7b exit evidence now includes:

• focused syscall/mapping/input/ABI/output/evidence tests;
• process-isolated fixed 51-case native correspondence;
• every R1-S1 through R1-S7a frozen test;
• strict Phase-1 proof suite;
• full workspace tests;
• strict Clippy and formatting;
• whitespace and Markdown-link audit.

The full workspace and strict quality/proof gates pass locally. R1-S7b is implemented and validated at its declared finite boundary. Gate B remains open.

18. Non-claims

R1-S7b does not establish:

• safety for arbitrary machine code or hostile process memory;
• recovery from a native fault inside the same process;
• a general sandbox or security boundary;
• worker-executable identity, build-provenance attestation, hermetic environment isolation, or replay freshness;
• another OS/ISA/ABI or feature-selected code;
• direct calls, stack arguments, external symbols, callbacks, runtime helpers, allocation, writable arrays, or general FFI;
• object/executable writing, linking, loading from disk, startup, syscalls from generated code, standard library, or standalone Gate B;
• benchmark eligibility, performance leadership, Gate C, Futamura P1/P2, Projection Birth, dependency closure, or Nauxogenesis.

19. Gate B handoff

Gate B may consume only an R1-S7b native-correspondence package whose exact target, code, runner, and result identities verify.

Gate B must separately add:

• a standalone artifact format;
• NAUX-owned object/executable writing and loading policy;
• startup and declared dynamic-input interface;
• bounded specialization/code growth and reproducibility;
• removal of interpreter/bridge process dependencies;
• standalone execution evidence.

Native correctness in an in-memory Rust seed runner is necessary but not sufficient for Gate B.

20. Revisit triggers

ADR-0038 and a new append-only runner schema/policy are required before any change listed in its revisit section. No implementation may widen a locked limit or claim set while retaining the R1-S7b v1 identities.