Canonical x86-64 Target R1-S7a Contract

Status: implemented and validated; raw bytes emitted but not executed

Stage: Roadmap Stage 3 / checked target encoding before native execution

Decision: ADR-0037

Current encoder decision: ADR-0044

Historical predecessor encoder decision: ADR-0042

1. Purpose

R1-S7a defines the first canonical x86-64 target-specific trust boundary after the verified R1-S6 Machine IR handoff.

It gives:

Residual Core
  + canonical Core SSA
  + canonical Machine IR
  → x86-64 target plan
  → raw position-independent code bytes

a closed target envelope, deterministic physical layout, exact ABI, owned instruction encoding, internal rel32 fixups, ordinary verification, composed source replay, target-plan evaluation, and hard resource limits.

R1-S7a emits raw bytes but does not execute them. R1-S7b owns verifier-gated W^X loading and finite native execution correspondence. Neither package may borrow correctness from the trace JIT.

2. Claim boundaries

R1-S7 keeps four claims separate:

X1  source-bound Machine-IR-to-target-plan lowering
X2  deterministic target-plan encoding, fixup resolution, ordinary
    verification, and complete source replay
X3  bounded Machine-IR-versus-target-plan evaluator correspondence
X4  verifier-gated native execution correspondence

R1-S7a contains X1, X2, and X3. R1-S7b contains X4.

Passing X1 cannot compensate for a verifier, encoding, or plan-evaluator failure. Passing X1 through X3 proves neither that the raw bytes have executed nor that real x86-64 execution agrees with Machine IR. Passing X4 on a finite corpus is still not a standalone, performance, or infinite-domain claim.

All X1-X3 implementation and locked-vector statements remain pending until the exit conditions in section 18 are met.

3. Authoritative source admission

The authoritative R1-S7a lowerer accepts:

source Residual Core artifact
source canonical Core SSA artifact
source canonical Machine IR artifact

It must first call:

verify_machine_ir_source(machine_ir, source_ssa, source_core)

That operation composes the R1-S5 Core/SSA source verifier with the R1-S6 SSA/Machine-IR replay. Ordinary verification of the three artifacts in isolation is insufficient.

The Machine IR schema must remain:

naux-machine-ir@0.1.0
lowering policy 1.0.0

R1-S7a adds this narrower target predicate:

types:
  Unit | Bool | I64 | F64 | F64Array

effects:
  [] | [Bounds]

instructions:
  Move
  I64Binary(Add | Sub | Mul, Wrapping)
  F64Binary(Add | Sub)
  I64Compare(LessThan | GreaterOrEqual)
  ArrayLenF64
  ArrayGetF64Checked

terminators:
  Return | Branch | TailCall

The complete translation fails closed on:

• direct Call;
• Saturating or any future integer mode;
• checked I64;
• any other type, effect, instruction, terminator, or fallback form;
• an entry signature needing more than five physical input lanes.

No unsupported form becomes a helper call, interpreter call, trace exit, deoptimization edge, or untyped target operation.

4. Schema, policies, and target descriptor

The current accepted identities are:

schema name               naux-x86-64-target
schema version            0.1.0
target lowering policy    1.0.0
encoder policy            1.4.0
target-plan domain        NAUX:x86-64:r1-s7a:plan:v1\0
code domain               NAUX:x86-64:r1-s7a:code:v1\0
artifact domain           NAUX:x86-64:r1-s7a:artifact:v1\0

These names and versions become normative only when implementation locks them before R1-S7a exit. Changing any accepted schema, lowering rule, frame rule, ABI rule, instruction template, fixup rule, or limit requires a new policy or schema identity.

The target descriptor is exact:

isa                  X86_64
environment          LinuxUserspace
host_abi             SystemVAMD64
byte_order           Little
pointer_width_bits    64
feature_level         BaselineSse2
mxcsr                 0x00001f80
code_model            PositionIndependentSingleBlob

The following never enter this identity:

• current load address;
• executable-memory address;
• process pointer values;
• host CPU model or fingerprint;
• CPUID results;
• ASLR state;
• Rust type layout;
• system assembler or linker output.

5. Canonical artifact shape

The canonical artifact contains at least:

schema
target_lowering_policy
encoder_policy
target_descriptor
entry_abi
numeric_contract
limits

source_core_hash
source_ssa_hash
source_machine_ir_hash

frame_layout
ordered target functions
ordered target blocks
ordered source-origin target operations
ordered labels
ordered fixups
entry_offset = 0

plan_hash
code_hash
final_code_bytes
artifact_hash

source_core_hash, source_ssa_hash, and source_machine_ir_hash must equal the exact identities in the opaque R1-S6 source-bound view.

The target plan and final bytes are both canonical fields. Neither is an unhashed cache of the other.

6. Physical values

6.1 Scalar values

Unit  = one u64 word equal to 0
Bool  = one u64 word equal to 0 or 1
I64   = one u64 word containing the exact two's-complement bits
F64   = one u64 word containing IEEE-754 binary64 bits

Non-canonical Bool or Unit values reject.

Every F64 constant entering the target plan already has canonical R1-S6 identity. Every observable NaN result is:

0x7ff8_0000_0000_0000

Signed zero is never normalized.

6.2 Read-only F64 arrays

F64Array = {
  data: u64,
  length: u64
}

data is the address of element zero. length counts F64 elements. The descriptor itself occupies sixteen bytes and has eight-byte alignment.

Invocation admission requires:

length <= i64::MAX
length * 8 does not overflow
data + length * 8 does not overflow
length > 0 implies data != 0
the span is readable and immutable for the invocation

The descriptor does not carry capacity, allocator identity, RC state, ownership bits, a vtable, or a hidden runtime pointer.

ArrayLenF64 reads only the length word.

ArrayGetF64Checked(array, index) expands in this semantic order:

1. obtain the array descriptor;
2. obtain the signed I64 index;
3. reject a negative index;
4. reject an index greater than or equal to length;
5. calculate data + index * 8;
6. perform exactly one eight-byte element read.

Steps 3 and 4 dominate step 6 in the target plan and encoded control flow. Failure performs no data read and transfers to the canonical Bounds epilogue.

R1-S7a does not prove arbitrary host memory is valid. R1-S7b must define the trusted caller and host-admission boundary before invoking raw code.

7. Entry ABI and outcomes

7.1 Input lanes

Entry parameters flatten in source order:

At most five lanes are accepted. They are assigned in order to:

lane 0  RDI
lane 1  RSI
lane 2  RDX
lane 3  RCX
lane 4  R8

The hidden output pointer is assigned to the next unused register from the same sequence extended with R9.

Examples:

(F64Array, I64)
  RDI=array.data, RSI=array.length, RDX=value, RCX=output

(F64Array)
  RDI=array.data, RSI=array.length, RDX=output

No stack input argument, varargs convention, aggregate host layout, or arbitrary C function signature is admitted. F64 parameters use integer lanes containing raw bits; they do not use the System V XMM argument class.

7.2 Output area

The hidden output pointer names two writable, eight-byte-aligned u64 words and must not overlap any admitted immutable input span.

EAX contains exactly one outcome tag:

0  Return
1  Bounds

The payload is:

The payload is written exactly once at the terminal semantic exit. A caller must inspect the outcome tag before interpreting it.

7.3 System V obligations

The entry:

• receives a System V-aligned stack;
• preserves all System V nonvolatile GPRs;
• uses no red zone;
• returns with RSP restored exactly;
• does not promise unwind metadata or asynchronous signal recovery;
• uses no external call.

8. Register authority

The complete physical-register authority is:

RDI and RSI carry entry lanes. They are read only while all entry lanes are stored and are not used afterward. No other physical register is writable.

Virtual registers are never silently assigned a physical register. A later allocation policy needs a new ADR and target policy.

The verifier rejects:

• an unlisted writable register;
• an attempt to retain a semantic value only in scratch state across a target operation boundary;
• a use of a scratch value after its fixed template lifetime;
• an indirect call or jump;
• syscall, int, iret, privileged instructions, x87, AVX, or FMA.

9. Frame and home layout

After the prologue, RSP is stable. Frame offsets are unsigned byte offsets from that stable RSP.

The header is:

offset 0..3    saved caller MXCSR
offset 4..7    canonical MXCSR value 0x00001f80
offset 8..15   hidden output pointer
offset 16..31  reserved zero padding

The maximum overlaid home area starts at offset 32.

For each function:

1. parameters are visited in dense register order;
2. instruction results continue in dense register order;
3. every value begins at the next eight-byte-aligned offset;
4. Unit/Bool/I64/F64 reserve eight bytes;
5. F64Array reserves sixteen bytes;
6. the function home extent is rounded to eight bytes.

All function home maps use the same home-area base and may overlay one another. The global home extent is the maximum function extent.

The outgoing tail-argument area starts at:

align8(32 + max_function_home_extent)

Its size is the maximum flattened byte size of any TailCall argument vector. The full frame size is:

align16(outgoing_base + max_tail_argument_extent)

Every extent calculation uses checked arithmetic. Every frame access must fit completely within its declared section. Header, home, outgoing, and padding ranges may not overlap contrary to this layout.

10. Proper tail transfer

For:

TailCall(target, arguments)

the encoder must:

1. validate exact arity, types, homes, target entry, outgoing extent, and every traversed intermediate tail edge before it can affect encoding;
2. symbolically compose through transitive empty tail entries before any destructive copy, retaining the original route on cycle, exhausted budget, or missing/ambiguous typed-home substitution;
3. accept a changed composed route only when its final parallel copy has a deterministic acyclic destructive schedule; otherwise retain the complete original route;
4. erase exact typed identity arguments;
5. for an acyclic remainder, write a destination only after its old words are absent from every remaining source;
6. for a cyclic remainder, stage every non-identity source in the non-aliasing outgoing area before committing any destination;
7. thread transitive empty exact-identity tail targets and transfer control by internal jmp rel32.

Unit contributes its canonical zero home but no ABI lane. F64Array pointer and length are loaded before either destination word is overwritten.

This policy handles:

• identical caller and callee homes;
• cycles in parameter permutation;
• duplicate source operands;
• constants mixed with registers;
• self tail recursion;
• tail calls among the 121 frozen branch-mix variants.

No native return address or additional frame is created. Direct Call is outside R1-S7a.

10.1 Policy 1.4 reachable one-operation superblocks

Encoder policy 1.4.0 is the current deterministic realization policy. It preserves the target plan, target schema, lowering policy, ABI, frame layout, source origins, Bounds ordering, and all upstream semantic identities while adding:

• reachability reconstruction from the same transformed successor relation used by emission;
• one-byte NOP tombstones for unreachable and consumed bodies so every declared label retains a unique in-blob instruction boundary;
• exact one-operation superblocks only across a reachable target with one reachable predecessor;
• typed encoder-internal result residency in R8 for Unit/Bool/I64 and XMM2 for F64;
• exact, unique typed substitution through crossed parameter homes;
• a proven acyclic destructive-copy schedule before final materialization;
• complete fallback to the already validated ordinary encoding on planning or optimized-emission refusal.

Array-producing operations and checked array reads remain memory-resident. Cycles, ambiguous or unbound substitutions, parameter/result aliasing, overlapping destinations, stale register generations, unsupported types, and non-unique predecessors refuse the superblock path. Policy 1.3.0 remains a historical evidence line and is not reinterpreted as policy 1.4.0.

11. Target operation set

The canonical plan has no arbitrary raw-instruction node. Its closed semantic macro-operation set is:

TargetMove
TargetI64Binary(Add | Sub | Mul, Wrapping)
TargetF64Binary(Add | Sub, StrictSse2)
TargetI64Compare(LessThan | GreaterOrEqual, Signed)
TargetArrayLenF64
TargetArrayGetF64Checked

TargetReturn
TargetBranch
TargetTailTransfer

Prologue, terminal Return, terminal Bounds, labels, and alignment are generated structural operations with fixed identities.

Every operation records its exact source origin:

MachineFunctionId
MachineBlockId
instruction index or terminator

Generated operations use one of these canonical origins:

EntryPrologue
ReturnEpilogue
BoundsEpilogue
AlignmentPadding

Origins are ordered, encoded, and verified. They are diagnostics and provenance, not permission to omit the source-bound replay.

11.1 Fixed instruction-template families

The owned encoder may emit only the exact families required by the operations:

• prologue/epilogue push, mov, sub, add, pop, ret;
• integer mov, add, sub, two-operand imul, cmp, test, setcc, movzx, and required bitwise classification operations;
• scalar SSE2 movq, movsd, addsd, and subsd;
• stmxcsr and ldmxcsr;
• direct near jcc rel32 and jmp rel32;
• verified base-plus-index-times-eight F64 loads.

There is one encoding template per admitted operation case and per explicitly versioned structural realization. Within the selected policy template, the encoder does not choose a host-dependent shorter instruction, feature alternative, or unlisted peephole sequence. Policy 1.4.0 superblock composition is part of the canonical encoder identity; it is not an ambient peephole choice.

Exact byte goldens for every template are required before exit.

12. Numeric contract

Wrapping I64 Add/Sub/Mul use the low 64 result bits. Comparisons are signed. Bool results are explicitly zero-extended to canonical 0 or 1.

The prologue:

stmxcsr saved_slot
store 0x00001f80 in canonical_slot
ldmxcsr canonical_slot

Both semantic exits execute:

ldmxcsr saved_slot

before restoring the frame and returning.

The canonical MXCSR means:

• round to nearest, ties to even;
• floating exceptions masked;
• denormals-are-zero disabled;
• flush-to-zero disabled.

F64 Add/Sub occur in original program order through scalar SSE2. There is no reassociation. Final F64 result classification preserves all non-NaN bits and maps every NaN to 0x7ff8_0000_0000_0000.

MXCSR flags are not part of Core observable behavior. The caller’s complete MXCSR value is restored, so target execution does not leak its internal flags.

13. Labels, code layout, and fixups

Labels are dense and ordered:

1. entry prologue;
2. functions by MachineFunctionId;
3. blocks by canonical stored block order;
4. generated local labels in source-origin and role order;
5. Return epilogue;
6. Bounds epilogue.

Every label has exactly one definition at an instruction boundary.

Under encoder policy 1.4.0, an unreachable or superblock-consumed body keeps one deterministic NOP at its label. These tombstones exist only to preserve unique label offsets and are unreachable from admitted live fixups. They do not restore the omitted body or add a semantic operation to the target plan.

The encoder uses fixed-width near control transfers. It never relaxes to a short branch. The only fixup is:

PcRel32 {
  patch_offset: u32,
  target_label: TargetLabelId,
  addend: i32  // exactly zero in v0.1
}

Fixups are strictly increasing by patch_offset. The four-byte placeholder is zero before resolution. Resolution computes:

displacement =
  label_offset(target_label) - (patch_offset + 4)

The result must fit signed i32. The final four bytes are its exact little-endian representation.

The final artifact retains the fixup records even though all internal displacements are resolved. A verifier reconstructs the placeholder image, re-lays out labels, reapplies every fixup, and compares the final image.

No fixup may target:

• an offset inside an instruction;
• alignment data;
• an address outside the code blob;
• an external symbol;
• an absolute process address.

The code blob is position-independent and requires no load-time relocation.

14. Canonical encoding and identity

Metadata uses manual big-endian scalar encoding:

lengths             checked u32
versions            u16,u16,u16
identifiers         u32
limits/counts       declared u32 or u64 width
frame offsets       u32
hashes              exact 32 bytes
variant tags        fixed u8

Ordered vectors retain stored order. Strings are fixed contract strings or length-capped UTF-8 fields. Diagnostics must not echo attacker-sized strings.

Raw code is encoded as:

code_length:u32
code_bytes:[u8; code_length]

without endian conversion.

The identities are:

plan_hash =
  SHA-256(plan_domain || canonical_plan_bytes)

code_hash =
  SHA-256(code_domain || code_length || final_code_bytes)

artifact_hash =
  SHA-256(artifact_domain || canonical_complete_artifact_bytes)

Canonical plan bytes include the target descriptor, entry manifest, frame/home layouts, ordered operations/origins, and ordered labels. They exclude the fixup table, final code bytes, and every declared hash. This prevents a circular plan identity.

The complete bytes include:

• target and ABI descriptors;
• policies and exact limits;
• three source hashes;
• entry manifest and entry offset;
• frame and home layouts;
• ordered operations and origins;
• labels and fixups;
• plan hash and code hash;
• final code bytes.

Host maps, debug formatting, target load address, Rust enum discriminants, and map iteration order are forbidden.

15. Resource limits

R1-S7a encodes this exact normative target limit vector:

The complete vector is encoded before plan and artifact identity. The focused suite directly exercises representative one-over and accounting-overflow cases; ordinary verification enforces every field.

Preflight must run before attacker-proportional plan allocation, semantic encoding, byte emission, or diagnostic construction. All accounting uses checked arithmetic or a fail-closed overflow marker.

The code-byte cap is far below 2 GiB, so an admitted internal rel32 target must fit by layout; each displacement is still checked individually.

16. Ordinary verification

verify_x86_64_target_r1_s7a must be independent of lowerer state and check:

Envelope

• exact schema and policies;
• exact target, ABI, feature, pointer-width, endian, code-model, and MXCSR descriptor;
• exact final limit vector;
• non-zero source Core, SSA, and Machine IR hashes;
• exact plan, code, and complete-artifact hashes.

Shape and physical authority

• non-empty program and exact entry;
• dense ordered functions, blocks, virtual-register homes, origins, and labels;
• exact type widths and canonical values;
• aligned, non-overlapping, in-frame home/header/outgoing ranges;
• exact maximum extents and 16-byte frame size;
• entry lane derivation and output-register placement;
• only admitted target operations and scratch registers;
• no direct call, indirect control, external operation, fallback, or raw-byte escape.

Semantics-bearing target invariants

• exact operation/result types;
• wrapping arithmetic and signed compare modes;
• scalar SSE2 F64 mode and canonical result classification;
• branch condition is canonical Bool;
• every array load is dominated by its exact checked-access template;
• every Bounds edge reaches the terminal Bounds epilogue;
• every tail transfer preserves simultaneous-assignment semantics: an accepted destructive schedule keeps all old sources live, while a cyclic schedule fully stages before any callee-home write;
• Return and Bounds write canonical outcome payloads and restore MXCSR.

Encoding and fixups

• label definitions are unique instruction boundaries;
• control targets are valid;
• fixups are the only zero placeholders and are ordered, non-overlapping, and in range;
• exact rel32 reconstruction;
• deterministic re-layout and re-encoding;
• every final byte matches the re-encoded image;
• no trailing, unexplained, or unreachable data bytes;
• no write outside the invocation frame or the exact output payload;
• all caps and the diagnostic sentinel.

Success returns an opaque local verified view. Callers cannot construct it.

17. Source-bound replay and plan evaluation

17.1 Composed replay

verify_x86_64_target_source must:

1. call verify_machine_ir_source(machine_ir, source_ssa, source_core);
2. ordinarily verify the supplied target artifact;
3. compare all three source hashes;
4. rerun target source-envelope admission;
5. regenerate the complete frame and home layout;
6. regenerate the exact plan, labels, fixups, and raw bytes;
7. compare plan bytes, raw code bytes, every table, and every hash;
8. return an opaque Core/SSA/Machine-IR/x86-64 source-bound view.

Changing only copied source hashes cannot create this view. A resealed target behavior change must fail step 7.

17.2 Target-plan evaluator

The R1-S7a evaluator:

• ordinarily verifies or consumes the opaque source-bound view;
• models typed stack homes rather than host addresses;
• represents F64Array as an immutable logical sequence;
• uses an explicit current function/block state;
• performs tail transfer by stage/commit/frame reuse;
• counts deterministic execution work;
• returns typed outcomes and an ordered effect trace.

The comparison relation is:

evaluate_source_bound_machine_ir(machine, input)
≈
evaluate_source_bound_x86_64_plan(target, input)

≈ preserves:

• exact Unit/Bool/I64;
• exact non-NaN F64 bits;
• canonical NaN;
• exact F64Array descriptor behavior where admitted;
• wrapping arithmetic;
• branch and tail-transfer order;
• Bounds outcome and ordered [Bounds] trace.

The plan evaluator does not execute raw x86-64 code. Its work count is non-semantic telemetry and need not equal Machine IR work.

The fixed R1-S6 manifest remains:

branch_mix      46 cases
ordered Bounds   5 cases
total           51 cases

No case may be omitted, reordered, skipped, timed out, or silently delegated to another engine.

18. Required evidence and exit

R1-S7a is implemented and validated against the bounded evidence below.

Positive evidence

• identical source-bound inputs produce identical plans, layouts, fixups, bytes, and hashes;
• the exact frozen branch-mix and ordered-Bounds artifacts lower;
• ordinary verification and composed source replay accept both;
• every admitted target operation and encoder template has a byte golden;
• wrapping Add/Sub/Mul and F64 Add/Sub have edge evidence;
• signed comparisons, Bool canonicalization, and both branch directions pass;
• zero/non-zero array length, negative index, exact-last index, and one-past index pass;
• TailCall argument permutations, duplicates, constants, and self recursion preserve simultaneous constant-stack transfer;
• Return and Bounds outcome payloads are canonical;
• MXCSR save/install/restore templates encode exactly;
• all 51 cases pass Machine-IR-versus-plan correspondence.

Negative evidence

• invalid source binding or unsupported source form;
• direct Call, Saturating/Checked I64, excess entry lanes;
• altered schema, target, ABI, feature, endian, pointer width, MXCSR, policy, any final limit, or any source hash;
• sparse/reordered/duplicate/missing home, function, block, origin, or label;
• wrong home width, alignment, offset, overlap, extent, frame size, or output register;
• forbidden register, operation, memory authority, external call, indirect control, absolute address, syscall, x87, AVX, or arbitrary byte node;
• missing/reordered Bounds check or a load reachable before it;
• an invalid destructive-copy dependency order, premature overwrite of a live source, incomplete cyclic staging, invalid composition route, or wrong target;
• wrong Return/Bounds tag or payload;
• non-canonical Unit, Bool, F64 NaN, or changed signed zero;
• changed operation, instruction template, immediate, code byte, entry offset, label, fixup target, fixup order, displacement, or trailing byte;
• a fully resealed behavior mutation under source replay;
• one-over/overflow work, frame, staging, operation, label, fixup, code, semantic-byte, plan-execution, and diagnostic boundaries.

Representative cap evidence does not imply a fixture for every cap. The final contract must distinguish enforced caps from directly exercised one-over fixtures.

Locked vectors

The current encoder-policy-1.4.0 branch-mix target output is:

source Core             fd90f6b16813a851aea7b1151a2df9ad87f9a9bfb8e994a5797407700f9fb2e9
source SSA              f31be2b773f263db5257fabc0e86a5572d5585b15c3b71b0d73ad6198b62630d
source Machine IR       1b1e303af18630fb6249b8427f25ce9ce17b05718679f097fcf5afffd0782b0f
target plan             86bb51383c27517fa98ec8d58f3d2d77970b61a468ef31d66defa3352190c6bd
raw code                ef32051c5c7af81365eee82664636f0a82bef5b1de3a8e3dcc07c2c207d7ce54
complete artifact       a642bcc02f2ea3566b0d5f275780e5cbbefe007b46a0eaa5578f3f680f838e95
plan bytes              34,742
complete semantic bytes 38,558
raw code bytes          3,097
shape                   functions=121 blocks=139 operations=162
                        labels=142 fixups=51
operation counts        Move=0 Add=5 Sub=2 Mul=0 FAdd=1 FSub=1
                        Lt=2 Ge=7 Len=3 Get=2 Return=3 Branch=9 Tail=127
frame                   header=32 homes=104 outgoing=96 total=240

The current encoder-policy-1.4.0 ordered-Bounds target output is:

source Core             4102a323b6e0165457abd636f2252c3299b7ac88848b1f155cbb38983a8294a5
source SSA              009e1eacbec8d2c5fc0363b753de6defc96073cbb413f87dc4db046ccc10f2c6
source Machine IR       758468a489dcd5ba2c55477a9d916530dd8c571e8dc4402194d73f3bdc6785e0
target plan             ca769f57312c92eff2d3ae9339b890b5e595685cbcde8f012c0fcffc568aaf97
raw code                c80220666bc16c99bd2c2a0570e418cc47462e0cdf8c7483530a8c7c149fee19
complete artifact       06e8a4cd6d1a7df57229180248c9f0040c9aa7781e1f38dea60e3f6a8f1c6251
plan bytes              1,653
complete semantic bytes 2,356
raw code bytes          488
shape                   functions=9 blocks=9 operations=11
                        labels=12 fixups=9
operation counts        Move=0 Add=0 Sub=0 Mul=0 FAdd=0 FSub=0
                        Lt=0 Ge=0 Len=0 Get=2 Return=1 Branch=0 Tail=8
frame                   header=32 homes=56 outgoing=48 total=144

The current fixed 51-case target correspondence result is:

51-case result hash     fe9cbcaf67798b502e8405eecb0228b7453d39427e97e4d404c7cd1356c8c49d

Accepted proof-only prospective shared-join vector

ADR-0049 adds a target-profile/Gate B schema-1.5.0, proof-policy-1.4.0 shadow realization without changing any encoder-policy-1.4.0 vector above:

baseline bytes / atoms         3,097 / 179
candidate bytes / atoms        3,214 / 199
bytes added / removed          117 / 0
labels / candidate fixups      142 / 51
body replicas                  11
shared-authority atoms         31
candidate weighted bytes       2,574,710,635
candidate code hash            0e392caf51dbc65f9e36e08c678118e78b8f6aed90bf1df0edbf4b5c6a5f5173
prospective realization hash   5f9b86ddb38f2b2a58f22cc4adb2bc4589f4f86ecf7d7fdae175204ae9266e15
Gate B schema-1.5 profile hash 2e7a1265e526d01697038fd7b0fac69258b9a17ce7362f063c3132551a78eb47

Every candidate span, declared label, tombstone, and fixup has one canonical owner, and independent replay reconstructs exact execution authority and weighted totals. The shadow buffer is discarded and is never returned, loaded, executed, packaged, timed, or selected. This vector is structural realization evidence, not a policy-1.5 artifact or performance claim. It also does not independently decode the machine semantics of cloned register and register-tail templates; that is a required successor gate before candidate selection can be proposed.

Historical encoder-policy-1.3.0 vectors

The following tables are retained as immutable predecessor evidence. They are not the current target authority and must not be mixed with policy-1.4.0 native, process, or standalone records.

The historical frozen branch-mix target output was:

source Core             fd90f6b16813a851aea7b1151a2df9ad87f9a9bfb8e994a5797407700f9fb2e9
source SSA              f31be2b773f263db5257fabc0e86a5572d5585b15c3b71b0d73ad6198b62630d
source Machine IR       1b1e303af18630fb6249b8427f25ce9ce17b05718679f097fcf5afffd0782b0f
target plan             49c53bda191214b2478d8f8f4e792807c994bc25c38fa6fb619c41e53cf25e42
raw code                f9cae8855bb39f74e38594272be92ebac5f6df2f3575652c361c444becd1efaf
complete artifact       057d8c9003db4b62ad35631435b2788e0efa7f3683987e62242063be02aa32b1
plan bytes              34,742
complete semantic bytes 44,863
raw code bytes          8,070
shape                   functions=121 blocks=139 operations=162
                        labels=142 fixups=162
operation counts        Move=0 Add=5 Sub=2 Mul=0 FAdd=1 FSub=1
                        Lt=2 Ge=7 Len=3 Get=2 Return=3 Branch=9 Tail=127
frame                   header=32 homes=104 outgoing=96 total=240

The historical ordered-Bounds target output was:

source Core             4102a323b6e0165457abd636f2252c3299b7ac88848b1f155cbb38983a8294a5
source SSA              009e1eacbec8d2c5fc0363b753de6defc96073cbb413f87dc4db046ccc10f2c6
source Machine IR       758468a489dcd5ba2c55477a9d916530dd8c571e8dc4402194d73f3bdc6785e0
target plan             fa413db5d8007b53de2aa5a75691e13f122d139a2adc90da4e97175ac25d84bb
raw code                a483a013abb4bb18ebfd7b67485b0ed48dcbd41a2cd090f57172ae40d72eb376
complete artifact       8b225ffe68fa57a171bf95eca85f88799ee0fdb44b04b6b5d7afa33da00090db
plan bytes              1,653
complete semantic bytes 2,654
raw code bytes          726
shape                   functions=9 blocks=9 operations=11
                        labels=12 fixups=14
operation counts        Move=0 Add=0 Sub=0 Mul=0 FAdd=0 FSub=0
                        Lt=0 Ge=0 Len=0 Get=2 Return=1 Branch=0 Tail=8
frame                   header=32 homes=56 outgoing=48 total=144

The historical fixed 51-case target correspondence record/results hash was:

51-case result hash     99e3b27435dd5e3fb2aac7e3d71233b897670ae45fd7001855ba49ddeec3d9cf

Its manual domain-separated encoding binds canonical case order, every input hash, source Machine IR identity, target-plan identity, exact F64/Bounds outcomes, and ordered effects. Engine-local work counters are deliberately excluded as non-semantic telemetry.

Historical focused implementation evidence at R1-S7a acceptance (later raw proof additions do not rewrite this frozen snapshot):

integration suite     naux-lang/tests/core_x64_target_r1_s7a.rs
integration result    9 passed; 0 failed; 0 ignored
raw encoder unit      25 passed; 0 failed; 0 ignored
corpus                branch_mix=46 Bounds=5 total=51

The integration suite covers deterministic lowering and source replay, resealed-behavior rejection, exact work exhaustion, ambient-MXCSR install/restore, representative plan/code/fixup/ABI/frame mutations, unsupported direct/saturating operations, wrapping multiplication, branch and ordered Bounds behavior, locked template/code identities, frozen lighthouse shapes, and ordered finite correspondence evidence. This is representative mutation evidence, not a fixture-per-bullet proof of the entire rejection surface.

Repository gates

• focused R1-S7a tests;
• every R1-S1 through R1-S6 frozen test;
• strict Phase-1 proof suite;
• full workspace tests;
• strict Clippy and formatting;
• whitespace and Markdown-link audit.

19. R1-S7b handoff

R1-S7b may consume only:

SourceBoundX86_64TargetArtifact

It must not accept raw code bytes, a local-only verified target, or copied hashes.

The runner contract must add:

• host input admission;
• verifier-gated memory allocation;
• write-only construction followed by read-execute protection;
• no writable-executable interval;
• copy and post-copy code hashing;
• exact entry offset and ABI invocation;
• normal semantic Return/Bounds containment;
• caller MXCSR restoration checks;
• an execution record binding the exact code hash;
• native-versus-Machine-IR correspondence on the fixed corpus;
• explicit no-fallback evidence.

R1-S7b is not implemented merely because existing trace-JIT executable-memory support can run x86-64 bytes.

20. Non-claims

R1-S7a does not establish:

• execution of the emitted bytes;
• general lowering of every valid R1-S6 Machine IR;
• direct calls, returning call frames, saturating/checked I64, stack arguments, or a general FFI ABI;
• register allocation, spilling, coalescing, vectorization, or optimization;
• an ELF object, executable, linker, loader, symbol resolver, debug/unwind format, runtime, standard library, or syscall layer;
• raw-pointer safety, hostile-process containment, or signal semantics;
• another OS, ISA, code model, or CPU feature level;
• implementation-diverse or formally verified x86-64 semantics;
• standalone viability, Gate B, Gate C, benchmark eligibility, performance leadership, Futamura P1/P2, Projection Birth, Nauxogenesis, or removal of Rust/Cargo/egg.