Canonical x86-64 Standalone R1-S8 Contract

Status: implemented and finite-accepted; Gate B performance remains open

Stage: Roadmap Stage 3 / Gate B standalone correctness subgate

Decision: ADR-0039

Predecessor: x86_64_native_runner_r1_s7b_contract.md

1. Purpose

R1-S8 freezes the first direct executable-image boundary for the P1 lighthouse:

verified R1-S7b workload authority
  → canonical startup plan
  → canonical startup bytes
  → direct ELF64 image containing one exact R1-S7a target blob
  → Linux process execution
  → independent Machine-IR correspondence evidence

The exact bounded claim is:

eval_MachineIR(source-bound workload, input)
≈
execve(canonical_standalone_ELF, canonical_input_frame)

for the frozen 51-case Gate A corpus. The relation preserves exact non-NaN F64 bits, canonical output NaN, terminal Bounds, ordered effects, exact profile and input identity, normal process termination, and absence of fallback.

R1-S8 is a standalone correctness subgate. It is not complete Gate B. Gate B remains open until an eligible controlled performance run of this same standalone path is no slower than 2.0x the hand-specialized baseline.

2. Claim decomposition

R1-S7a  source-bound target plan + checked position-independent bytes
R1-S7b  verifier-gated native execution + finite process correspondence
R1-S8a  opaque standalone authority + canonical ELF/startup artifact
R1-S8b  independent artifact regeneration and mutation rejection
R1-S8c  direct-process I/O + fixed 51-case standalone correspondence
Gate B  R1-S8 complete + eligible standalone runtime <= 2.0x hand-specialized
Gate C  controlled performance differentiation
P1      all semantic, erasure, standalone, performance, and reproduction gates

No in-memory runner result, emitted file alone, launch alone, or benchmark alone can satisfy the complete R1-S8 relation.

3. Platform and workload profiles

The only v1 platform is:

There are exactly two workload profile tags:

One ELF image binds exactly one profile. A BranchMix image cannot admit a Bounds input and a Bounds image cannot admit a BranchMix input. The startup contains no workload dispatch, generic opcode handler, bytecode program, or interpreter entry.

The repetitions wire field is a dynamic I64 only for BranchMixF64R1. It is reserved and must be zero for BoundsF64R1. The Bounds program retains its frozen static ordered reads at indices zero and one; the five cases vary only the admitted array.

4. Upstream authority

4.1 Required opaque view

The R1-S8 writer consumes an opaque verified authority. That authority can be constructed only by independently checking:

• one complete R1-S4 → R1-S5 Core SSA → R1-S6 Machine IR → R1-S7a target chain;
• one exact source-bound target artifact for the inferred workload;
• every canonical R1-S7b process record for that workload;
• the exact Gate A manifest membership and order;
• complete equality of source Machine IR, target artifact, target plan, verified target code, ABI, entry offset, input-lane count, workload, runner, and native result identities.

The authority borrows or otherwise remains lifetime-bound to the artifacts and evidence it authenticates. It does not expose a constructor from:

• raw or copied target bytes;
• a target artifact without source replay;
• a semantic, plan, code, ABI, or result hash tuple;
• an execution record detached from its aggregate evidence;
• a caller assertion that verification passed;
• a worker path, process result, pointer, or entry address.

4.2 Finite scope

The authority proves only that the exact workload package passed the frozen finite S7b boundary. It does not authorize another workload, an altered ABI, an arbitrary input domain, or a general x86-64 correctness claim.

4.3 Inherited identities

R1-S8 carries without reinterpretation:

Gate A manifest and workload identity
R1-S4 residual artifact and structural-erasure identity
R1-S5 Core SSA artifact and correspondence identity
R1-S6 Machine IR artifact and correspondence identity
R1-S7a target schema, policies, plan, code, artifact, ABI, and source replay
R1-S7b runner, correspondence, process, IPC, record, and results identities
all exact inherited hard-limit and usage vectors

A mismatch at any inherited field is an authority-construction failure. Verified, domain-separated, order-sensitive aggregate result roots are the canonical transitive carriers of predecessor record identities. R1-S8 must regenerate and verify their complete ordered leaf evidence through the live opaque authority; it must not duplicate those leaf vectors in the artifact under an alternate encoding.

4.4 Sealed predecessor correspondence roots

ADR-0040 closes the two correspondence identities that previously existed only as test assertions:

R1-S5 Core↔SSA
18db0347094dfad000e7a6401cd1d989edd57f44bd0b31a9544d80f3803ba58b

R1-S6 SSA↔Machine IR
3cc7cbd876531ea6f88c56f50c851eb168ac76afe2d9a05ae6835687bf411205

Both are independently regenerated over the exact ordered 51-case corpus. The inherited envelope carries each schema, policy, manifest, result root, fixed limit vector, record count, and cross-profile lineage. Its canonical manual big-endian width is exactly 2,984 bytes.

5. R1-S8 versions and domains

5.1 Version tuple

Every new schema or policy introduced by R1-S8 has semantic version:

major = 1
minor = 0
patch = 0

This applies to:

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

The version occupies six bytes in both wire headers as three big-endian u16 values:

00 01  00 00  00 00

The printable policy name 1.0.0 and the six-byte wire encoding denote the same version but are not interchangeable encodings.

5.2 Hash domains

The only new R1-S8 domains are the exact NUL-terminated byte strings:

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

Every identity uses manual canonical encoding with:

• the exact domain first;
• big-endian integer fields;
• explicit enum tags;
• big-endian lengths before variable data;
• no Rust layout, serde, JSON, platform usize, debug text, or filesystem metadata;
• exact EOF after the declared fields.

A domain substitution, field omission, duplicate field, alternate order, noncanonical enum, trailing byte, or schema/policy substitution fails closed.

6. Exact ELF64 grammar

All ELF multibyte values are little-endian, as required by the declared target. The file begins with one exact 64-byte ELF header.

6.1 ELF header

Extended numbering is forbidden.

6.2 Program header zero

Program header zero is the only load segment:

The ELF header, both program headers, startup, alignment padding, and target blob all reside in this read/execute segment. There is no writable load segment and no zero-fill tail.

6.3 Program header one

Program header one is:

An executable stack is forbidden.

6.4 Forbidden ELF content

The complete file contains no:

second PT_LOAD
PT_INTERP
PT_DYNAMIC
PT_TLS
section header or section-name table
dynamic symbol or string table
relocation section or runtime relocation
GNU property/note dependency
build ID
import, export, undefined symbol, or symbol-version requirement
linker-injected startup
trailing overlay

External inspection tools are optional diagnostics. readelf, objdump, the system assembler, and the system linker are not acceptance authorities.

7. Canonical file layout

The file layout is exact:

file offset       contents
0x0000..0x003f    ELF64 header
0x0040..0x0077    PT_LOAD
0x0078..0x00af    PT_GNU_STACK
0x00b0..0x00ff    exactly 80 zero bytes
0x0100..S         canonical startup code
S..T              zero alignment padding
T..EOF            one exact R1-S7a target blob

Definitions:

startup_offset = 0x100
target_offset  = align_up(startup_offset + startup_code_bytes, 16)
image_bytes    = target_offset + target_code_bytes
entry_vaddr    = 0x400000 + startup_offset
target_vaddr   = 0x400000 + target_offset

S..T contains between zero and fifteen zero bytes. Integer overflow in any offset, virtual address, size, or alignment computation is a typed failure. The exact EOF is the last byte of the target blob.

The target region must be byte-for-byte equal to the complete verified R1-S7a blob. It appears exactly once. R1-S8 cannot decode and re-encode it, adjust its entry, change an internal PcRel32, append data to it, relax a branch, patch a constant, or select another feature path.

The only R1-S8 target-entry fixup resolves one startup call rel32 to:

target_vaddr + inherited_target_entry_offset

The inherited entry offset, canonical ABI, input lane count, output register, result type, code hash, target plan hash, artifact hash, and source Machine IR hash are rechecked before this fixup is admitted.

8. Startup plan and encoding

8.1 Plan authority

The startup is not an opaque hand-written byte vector. A canonical startup planner derives a bounded typed plan solely from:

• the opaque workload authority;
• exact R1-S8 versions and policies;
• the baked profile;
• the frozen I/O contract and hard limits;
• the calculated target offset and verified inherited entry ABI.

The plan explicitly represents:

process-entry admission
exact input-header read
magic/version/profile validation
checked element and payload-size arithmetic
optional input mapping
exact payload read and EOF validation
in-place big-endian u64 conversion
RW-to-R protection transition
typed target ABI preparation
one direct target call
native tag/payload validation
input unmap
exact output-frame construction
complete output write
typed exit

It contains no arbitrary address, external symbol, caller-selected syscall, interpreter operation, worker invocation, helper callback, or fallback edge.

8.2 Deterministic encoder

The NAUX-owned startup encoder:

• accepts only a verifier-accepted startup plan;
• emits only the frozen Linux x86-64 instruction subset needed by that plan;
• owns every label and PcRel32 fixup;
• uses checked signed-displacement and size arithmetic;
• emits no relocation record;
• resolves the single target call only after final target placement;
• emits byte-identical output for identical authority and profile.

The startup plan hash and startup code hash use distinct domains. A matching code hash does not substitute for plan verification.

8.3 Startup stack

At _start, the kernel-owned entry stack is the only writable stack. The startup:

• verifies argc == 1;
• does not read argument text, environment strings, auxiliary-vector values, current directory, wall clock, randomness, locale, or host CPU dispatch;
• preserves the kernel stack allocation;
• aligns target entry as required by NauxLighthouseSysV1;
• uses no more than 512 bytes below the original entry stack pointer;
• stores only bounded header, output, call, and scratch state there;
• never treats untrusted payload length as a stack allocation size;
• never returns from _start.

An extra command-line argument is input-policy rejection. Environment entries may exist, but their bytes and order are unobserved and cannot affect semantic output.

9. Syscall and memory contract

9.1 Complete syscall set

Only these raw Linux x86-64 syscall numbers may be emitted:

The startup invokes the syscall instruction directly. It does not call a libc wrapper, vDSO function, PLT entry, runtime helper, signal handler, or interpreter.

read retries EINTR and accumulates short successful reads. write retries EINTR and accumulates short successful writes. A zero-byte read before the declared frame is complete is truncation. After the exact payload, the startup requires one further read to return EOF; any byte is trailing-input rejection. The producer must therefore close stdin after its one frame.

Raw syscall returns in [-4095, -1] are errors. Errno, syscall count, mapping address, PID, ASLR placement, and retry count are diagnostics, not semantic identity fields.

9.2 Input mapping state

For a non-empty payload, the only legal input state trace is:

Unmapped
  → mmap(RW, PRIVATE|ANONYMOUS)
  → complete read
  → in-place u64 byte swap
  → mprotect(R)
  → target call/return
  → munmap
  → Unmapped

The mapping:

• is requested without a fixed address;
• has exact declared payload length, subject to kernel page rounding;
• is never executable;
• is never written after the successful mprotect;
• stays alive and immutable for the complete target call;
• is the only runtime input mapping;
• is unmapped before successful output is published.

For zero elements, the canonical target descriptor is data=0,length=0; the mapping trace remains Unmapped and no memory syscall is made.

A normal error after mapping performs the required unmap before exit. An unmap failure is exit 71 and cannot publish a successful output.

10. Input frame

10.1 Exact bytes

The canonical input has a 40-byte header followed by zero or more exact F64 bit words:

The payload contains raw IEEE-754 binary64 encodings. Input NaN payloads, signed zero, infinities, subnormals, and ordinary values cross the wire without canonicalization. Each u64 is converted to x86-64 byte order in place before the mapping becomes read-only.

10.2 Admission

Input admission requires:

magic == "NAUXGBI1"
version == (1, 0, 0)
profile is 1 or 2
profile == image_profile
array_elements <= 1,048,576
payload_bytes == checked_mul(array_elements, 8)
payload_bytes <= 8,388,608
40 + payload_bytes <= 8,388,648
Bounds implies repetitions == 0
exact payload present
exact EOF follows payload

BranchMix accepts every I64 bit pattern in repetitions; its source-bound semantics determine the result. The startup must not silently clamp, reinterpret, precompute, or reject a value admitted by the typed source contract.

Unknown profile, wrong baked profile, version drift, arithmetic overflow, one-over limits, inconsistent payload length, extra argument, or trailing input exits 64 without stdout. Premature EOF or a read failure exits 74 without stdout.

11. Target call

The startup derives target lanes from the verified inherited ABI:

BranchMixF64R1:
  Array<F64> data
  Array<F64> element length
  repetitions I64
  runner-owned two-word output pointer

BoundsF64R1:
  Array<F64> data
  Array<F64> element length
  runner-owned two-word output pointer

The exact registers and output-register position remain those of the frozen NauxLighthouseSysV1 ABI. They are not duplicated as caller-supplied configuration.

Before the call, the startup initializes both target output words to the frozen noncanonical sentinel, establishes the required stack alignment, and supplies no stack argument. It calls exactly:

image_base + target_offset + inherited_entry_offset

The target must return normally with its complete required numeric state restored. A native fault, signal, non-return, stack corruption, ABI mismatch, unknown native tag, sentinel residue in a field whose admitted semantic value cannot equal that sentinel, noncanonical Bool/tag/payload, foreign array descriptor, or unexpected effect is a failed execution. The first ReturnF64 word may legitimately equal the finite sentinel bit pattern; the required zero second word still proves the complete two-word result shape.

For the two v1 profiles, the only admitted target results are:

Return(F64)
Bounds with exactly one ordered Error(Bounds) effect

12. Output frame and process status

12.1 Exact output

A valid semantic outcome is encoded into exactly 40 bytes:

The outcome grammar is:

Input NaNs retain their payload until evaluated. The inherited R1-S7a target canonicalizes a returned NaN exactly once at its semantic output boundary. The startup independently requires that canonical target payload and then serializes it without a second normalization. No other result bit is changed.

The startup writes the frame only after:

• native result and effects validate;
• the complete input mapping is unmapped;
• every output field has its canonical value.

No error path may write a prefix of a success frame intentionally. A kernel write failure may leave an externally observed partial frame; the parent rejects it.

12.2 Exit codes

The only normal exit codes are:

Bounds is a semantic result and therefore emits outcome tag 1 and exits 0.

exit_group is the only emitted termination syscall. If it unexpectedly returns, execution must enter a fixed abnormal trap; it cannot fall through to target bytes or report success.

12.3 Parent admission

A claim-bearing parent accepts a case only if:

process exited normally with code 0
stdout length == 40
stdout decodes canonically and reaches exact EOF
output profile == baked image profile == case workload
stderr length == 0
no timeout, signal, crash, kill, or abnormal status
output ≈ independently evaluated source-bound Machine IR outcome

Any unknown exit code, missing frame, truncation, trailing stdout, noncanonical NaN, nonzero reserved field, payload mismatch, stderr byte, timeout, or abnormal status fails the case. There is no retry, fallback, or skip.

13. Artifact and identities

13.1 Standalone artifact

The sealed standalone artifact binds at least:

artifact schema = 1.0.0
ELF writer/layout/verifier policies = 1.0.0
startup plan/lowering/encoder policies = 1.0.0
I/O schema/policy = 1.0.0
all inherited R1-S4/S5/S6/S7a/S7b identities
workload profile
complete canonical ABI hash
entry offset and input-lane count
startup plan hash
startup code length and hash
ELF base, entry, header values, and program-header values
target file offset and virtual address
target code length and exact inherited code hash
complete image length and ELF-image hash
hard-limit vector and exact usage vector
interpreter_dependency = false
external_symbol_dependency = false
dynamic_loader_dependency = false
system_linker_dependency = false
fallback = false
artifact hash

All fields before the final artifact hash participate in the artifact identity. A boolean declaration is not proof of absence; section 15 defines the structural check.

13.2 Image identity

The ELF-image hash covers every file byte from offset zero through exact EOF, including:

• all ELF header bytes;
• both program headers;
• fixed zero padding;
• startup bytes;
• alignment zeros;
• the exact target blob.

Filesystem path, inode, permissions, owner, timestamps, mount, parent PID, ASLR input address, and launch duration do not enter image identity. The claim harness separately requires an executable file mode and controlled launch path.

13.3 Reproducibility

For identical verified upstream authority, profile, policies, and limit vector:

startup_plan_bytes identical
startup_code_bytes identical
target_offset identical
complete_ELF_bytes identical
every R1-S8 identity identical

No timestamp, random seed, build path, host address, iteration order, linker default, environment value, or CPU feature probe may affect the artifact.

14. Independent artifact verification

The authoritative verifier consumes the opaque upstream authority and raw ELF bytes. It does not consume a writer-created “verified” flag.

It must independently:

1. revalidate the complete opaque authority and inherited identities;
2. enforce exact file and overhead limits before allocation;
3. parse every ELF header and program-header field with checked arithmetic;
4. require exact two-header grammar, permissions, offsets, sizes, and EOF;
5. verify both zero-padding regions;
6. derive the baked workload profile from the authority and artifact;
7. regenerate and verify the startup plan;
8. independently encode the startup and require exact byte equality;
9. recompute the aligned target offset;
10. compare the sole target slice byte-for-byte with the inherited R1-S7a code and reject duplication;
11. validate the single startup-to-target fixup and inherited entry ABI;
12. recompute startup, I/O, image, and complete artifact identities;
13. carry and compare all inherited and R1-S8 limit/usage vectors;
14. publish an opaque verified standalone view only after exact EOF.

The verifier must reject mutations to every fixed field, every startup byte, both padding ranges, target placement, target byte, length, identity, profile, version, cap, usage, or trailing byte.

Whole-file hashing alone is insufficient. External ELF parsing alone is insufficient. Reusing writer offsets without recalculation is insufficient.

The accepted startup verifier owns complete frozen byte tables for both profiles and compares every byte before its independent structural decoding, fixup checks, syscall-site checks, and SHA oracle. It does not call the production startup emitter to obtain expected bytes. Exhaustive single-byte-mutation tests reject every position in both startup images.

15. Interpreter-dependency absence

The interpreter_dependency=false claim is accepted only from the conjunction of:

1. the upstream opaque authority proves the exact R1-S4 residual structurally erased opcode values, dispatch, interpreter entry/step, generic opcode handlers, dynamic program counter, unresolved static program operands, and fallback;
2. R1-S5 and R1-S6 replay preserve that exact residual provenance;
3. R1-S7a contributes the sole exact target blob;
4. independent ELF verification proves the remainder is exactly the verified bounded startup and zero padding;
5. the ELF has no dynamic loader, import, relocation, external symbol, runtime callback, second code body, or embedded S7b worker;
6. direct execution invokes neither the AST/bytecode interpreter, trace JIT, S7b W^X runner, nor generic CoreVM0 handler.

A byte scan for the word “interpreter”, absence of symbol names, a small file, or a writer-provided boolean cannot satisfy this condition.

The startup is glue for process entry and declared dynamic I/O. It may not evaluate CoreVM0 opcodes, select a program, perform specialization, call the Rust seed, or repair/fallback from target behavior.

16. Hard limits

The exact R1-S8 v1 limit vector is:

Additional exact relation:

elf_image_bytes <= inherited_target_code_bytes_used + 65,536

All R1-S4 residual, Core SSA, Machine IR, R1-S7a target, and R1-S7b process limits/usages are embedded and compared exactly. They are neither replaced by the new image cap nor rounded to it.

Admission uses exact values, not saturating arithmetic. Exact-cap vectors are positive tests. Every independently constructible one-over dimension is a negative test. Budget exhaustion is a typed failure and cannot emit a partial artifact.

Successful claim execution requires exactly zero stderr bytes even though the parent bounds captured failure diagnostics to 16,384 bytes and 128 newline-delimited records.

17. Direct execution evidence

17.1 Per-case record

One R1-S8 execution record binds:

execution schema/policy = 1.0.0
case ordinal and total
Gate A manifest, workload, case, and input hashes
all inherited source and target identities
standalone artifact and complete ELF-image hashes
baked profile and I/O-contract hash
exact canonical input-frame hash
normal exit code
exact canonical output frame and hash
decoded semantic outcome and ordered effects
independent Machine IR outcome and ordered effects
stdout/stderr lengths
timeout/fault/abnormal flags
interpreter_dependency = false
fallback = false
record hash

PID, process address, mapping address, elapsed wall time, retry count, errno text, temporary path, and parent diagnostics are non-semantic telemetry.

17.2 Ordered result

The ordered result:

• contains exactly ordinals 0..50;
• contains 46 BranchMix records followed by the frozen 5 Bounds records in exact Gate A manifest order;
• requires each ordinal exactly once;
• binds both independently verified ELF artifact identities;
• binds the complete ordered list of record hashes;
• uses NAUX:x86-64:r1-s8:execution:results:v1\0;
• rejects omission, duplication, reordering, mixed manifests, profile swap, image swap, case substitution, or result replay.

17.3 Process containment

Each case launches its profile image in a fresh process. The parent:

• supplies exactly one canonical input frame and closes stdin;
• captures stdout and stderr concurrently under the frozen bounds;
• enforces the 30,000 ms timeout;
• kills and reaps the complete failed child boundary;
• never retries a failed case;
• independently decodes output and evaluates Machine IR;
• creates a record only after all admission checks pass.

This containment converts a fault or hang into a failed case. It is not a sandbox or proof that hostile machine code cannot affect the host.

18. Required test matrix

18.1 ELF writer/verifier

Tests must include:

• exact locked header/program-header/layout vectors for both profiles;
• deterministic rebuilds across repeated runs;
• independent regeneration of startup plan, startup bytes, target placement, image bytes, and identities;
• mutation of every fixed ELF field;
• zero-padding, alignment-padding, startup, target-first/middle/last-byte, and EOF mutations;
• inserted PT_INTERP, writable/executable load, executable stack, extra program header, section header, relocation-like trailing data, and target duplication rejection;
• wrong upstream artifact, source, workload, ABI, entry, lane count, profile, target code, result evidence, version, domain, limit, and usage rejection;
• exact-cap and one-over tests for every reachable cap.

18.2 I/O protocol

Tests must include:

• round trip for both profiles;
• empty, maximum, and maximum-plus-one arrays;
• every header-field truncation and payload truncation;
• short reads, EINTR, read failure, closed input, and one trailing byte;
• wrong magic, every version component, unknown/wrong profile, inconsistent payload length, multiplication/total-length overflow, and nonzero Bounds repetitions;
• negative/zero/positive BranchMix repetitions admitted according to source semantics;
• negative zero, both infinities, subnormals, ordinary values, many NaN payloads, and canonical output NaN;
• every output truncation, trailing byte, outcome, reserved, payload, and profile mutation;
• short writes and write failure.

18.3 Startup/process failures

Tests must reject:

• extra argv;
• mapping, protection, and unmapping errors;
• a write after input becomes read-only;
• target call before protection;
• unknown target tag or noncanonical payload;
• signal, abort, abnormal exit, unknown exit, missing output, extra output, nonempty stderr, and timeout;
• a valid output followed by abnormal termination;
• output before required unmap;
• any S7b worker/loader or interpreter/fallback route.

The implementation locks these paths with structural startup control-flow evidence and raw-ELF process fixtures. Process fixtures cover timeout, SIGKILL, SIGABRT, normal-zero with missing/trailing output, nonempty stderr, valid output followed by abnormal exit, unknown exit 127, and a forked descendant retaining inherited pipes. They use raw syscalls and no shell or external compiler.

18.4 Semantic acceptance

The exact 51-case corpus must:

• execute one fresh direct ELF process per case;
• exercise both baked profile images;
• preserve all canonical Gate A input hashes;
• match independent Machine IR exact bits/canonical NaN/Bounds/effect order;
• publish a stable ordered R1-S8 result hash;
• remain green under the full workspace, all features, strict proof, formatting, lint, link, and documentation audits.

The implementation’s current encoder-policy-1.4.0 locked identities are:

BranchMix artifact
f1951da3deafa4119c56cec8a91721bc83630ff5f3c48c60d6f4f56cadd19a47

Bounds artifact
f6271787b782f0177ac067086db9525f985b2eb2b87b4a60ce031974454ee664

ordered R1-S8 result
22897dc524804625751f027a820bb75f4da3f7e77afca5183bc1522542418b85

These vectors become R1-S8 acceptance evidence only when the full gate suite is green; copying them is not verification.

The historical encoder-policy-1.3.0 vectors remain frozen predecessor evidence:

BranchMix artifact
25a3bddd07cb9b62e01183167e3d76e32fdfc913c08b502712f2648f5d1edf74

Bounds artifact
3a6e467798d8642d6899d6f97e13b28457dc3eef49982dfbb21e6612ea600f72

ordered R1-S8 result
36bd1ee505aa2e2ba4a860df3d743b6c26d9c4b7442d7b8ba385449412232877

They must not authorize a policy-1.4.0 image or correspondence record.

19. Gate B handoff

R1-S8 completion establishes that the lighthouse residual is a reproducible, directly loadable, interpreter-free, libc-free standalone process image over the fixed corpus.

It does not complete Gate B. Gate B requires all R1-S8 acceptance evidence plus:

eligible controlled standalone benchmark
same semantic workload and dynamic input
same operation order and numeric policy
recorded machine/compiler/baseline identities
NAUX standalone runtime <= 2.0x hand-specialized runtime

Startup, I/O, process creation, mapping, and teardown accounting must be reported explicitly. A benchmark may separately report steady-state kernel time, but cannot hide the declared standalone cost when making the Gate B claim. ADR-0041 and gate_b_standalone_measurement_contract.md now freeze the precise measurement method and accounting policy. Three current policy-1.4.0 local observations measure 4.822709x, 4.796549x, and 4.884944x, improving 16.78%–18.29% over policy 1.3.0 with about 1.85% across the ratios. None is claim-admissible: all are local-only, fail at least one CV check, and miss the <= 2.0x threshold. An eligible <= 2.0x result remains outstanding.

The later mature target <= 1.25x and P1 graduation target within 10% remain separate milestones. Neither is implied by the first Gate B viability pass.

20. Seed and sovereignty accounting

After R1-S8, the emitted ELF itself contains:

no Rust runtime
no Cargo/rustc dependency
no egg
no libc
no system linker output
no dynamic loader
no generic interpreter
no trace JIT
no S7b worker or in-memory loader

The current writer, independent verifier, corpus harness, and the tool that launches the ELF may still be Rust/Cargo seed code. This remains explicit dependency debt. R1-S8 is not Nauxogenic closure and does not make the seed discardable.

The accepted external platform boundary is:

Linux kernel ELF64 loader
Linux x86-64 raw syscall ABI
host filesystem and process-launch facility used by the seed harness

No third-party compiler component may become part of the artifact grammar or runtime image.

21. Non-claims

R1-S8 does not establish:

• correctness beyond the frozen finite corpus;
• formal ELF, Linux, syscall, or x86-64 semantics;
• safety or containment for arbitrary hostile code/input;
• executable authentication, hermetic launch, environment attestation, replay freshness, or a general sandbox;
• PIE, ASLR for the text image, another base, another ISA/OS/ABI, AVX/FMA dispatch, general functions, multiple arrays, writable arrays, target allocation, callbacks, FFI, threads, async, exceptions, or a standard library;
• a general-purpose linker, loader, object format, package manager, debugger, or profiler;
• complete Gate B, Gate C, public benchmark eligibility, performance leadership, C/C++ parity, Futamura P1/P2/P3, Projection Birth, Nauxogenesis, or Rust/Cargo/egg dependency closure.

22. Revisit rule

Any change to an upstream authority requirement, profile, version, domain, ELF byte, header count, segment permission, base, entry, layout, startup operation, syscall, call ABI, I/O byte, exit status, identity field, limit, acceptance relation, or claim boundary requires:

1. a new ADR;
2. append-only schemas and policies;
3. new hash domains;
4. new locked artifact and execution vectors;
5. independent replay and mutation evidence;
6. explicit migration without reinterpreting any R1-S8 v1 artifact.

Performance work may optimize the inherited target or introduce a successor startup only through a new source-bound target/policy line. It may not mutate an R1-S8 v1 image while retaining its identities or describe R1-S8 standalone correctness as complete Gate B.