GitHub

ADR-0051: Sealed Non-Executable Encoder-Policy-1.5 Candidate Capsule

Status: accepted for the sealed non-executable capsule boundary; encoder policy 1.5 remains closed until the later correctness, identity-migration, and performance gates below are accepted

Date: 2026-08-02

Visibility: private NAUX architecture/governance record. This ADR is not public roadmap material.

Related: ADR-0037, ADR-0038, ADR-0039, ADR-0041, ADR-0044, ADR-0049, ADR-0050

Extends: ADR-0050’s accepted proof-only candidate semantics with a durable, independently regenerable artifact identity

Preserves: canonical Typed Core, SSA, Machine IR, target-plan semantics, policy-1.4 lowering and execution authority, ABI, benchmark policy, native runner, process worker, standalone writer, and every accepted policy-1.4 identity

Context

ADR-0049 and ADR-0050 establish a complete physical receipt and a bounded implementation-diverse semantic proof for the current shared-join candidate. The raw encoder nevertheless keeps candidate bytes in a private transient RawProspectiveShadow and discards them when profiling finishes. This is the correct proof-only boundary, but it provides no durable object whose complete identity can be migrated through later native, process, and standalone gates.

Selecting the transient bytes directly would bypass the existing trust chain. The native runner accepts only a SourceBoundX64TargetArtifact, obtained by verifying policy 1.4 and replaying the complete Machine-IR-to-target translation. Merely changing the encoder version or copying the candidate code would make plan, label, fixup, code, semantic, execution-record, standalone-authority, and ELF identities disagree.

NAUX therefore needs an intermediate authority object: durable enough to identify and independently replay the exact candidate, but structurally incapable of entering executable memory.

Decision drivers

  • A proof receipt must not implicitly grant execution permission.
  • Candidate construction must start from a verified, source-bound policy-1.4 artifact and accepted profile evidence.
  • Candidate bytes, labels, fixups, policy version, and all hashes must be one sealed identity.
  • Verification must regenerate the raw shadow from the baseline target; it must not trust copied candidate fields or a self-resealed claim.
  • Any missing, incomplete, mismatched, over-limit, or unsupported evidence must preserve the exact policy-1.4 path.
  • No native mapping, function-pointer conversion, process worker, ELF image, timing sample, or performance claim may consume the capsule.
  • The implementation remains NAUX-owned and adds no assembler, linker, decoder, solver, or other third-party dependency.

Considered options

1. Flip the global encoder constant to 1.5

This would silently change every downstream identity and permit unreviewed candidate execution. It also gives no exact fallback object. Rejected.

2. Let the native runner consume shadow bytes plus a code hash

A code hash alone omits target policy, label/fixup layout, source provenance, and proof identity. It would create a second, weaker native entry path. Rejected.

3. Materialize a normal X64TargetArtifact and reuse policy-1.4 source

verification

The existing verifier correctly requires exact policy-1.4 source replay, so a policy-1.5 artifact must not masquerade as its result. Weakening that verifier would weaken already accepted artifacts. Rejected.

4. Introduce a sealed non-executable candidate capsule

The capsule can bind the complete candidate while remaining a distinct type that no execution API accepts. Fresh replay can validate it before later gates add narrowly scoped conversion authority. Accepted for implementation.

Decision

1. Separate capsule type

The policy-1.5 candidate is represented by a dedicated capsule, not by a SourceBoundX64TargetArtifact. Its canonical payload binds:

capsule schema and policy
baseline target semantic/plan/code identities
source Core/SSA/Machine-IR identities
profile schema and proof-policy identities
Gate B evidence root
prospective realization root
candidate encoder policy 1.5.0
candidate target artifact semantic/plan/code identities
candidate labels, retained rel32 fixups, and code through artifact identity

The candidate target program retains the baseline semantic plan, ABI, limits, entry, frame, functions, and source hashes. Only the encoder policy, physical label offsets, fixups, code, and derived identities may differ.

2. Construction order

Construction must perform these steps in order:

  1. consume an already verified and source-bound policy-1.4 target;
  2. validate the profile identity against that exact baseline;
  3. require complete structural and machine-semantic prospective evidence;
  4. replay policy-1.4 raw encoding and compare it with the baseline;
  5. regenerate the transient candidate from that replay;
  6. compare candidate code hash, label receipts, fixup receipts, sizes, and realization root with the supplied evidence;
  7. build a policy-1.5 program from the immutable semantic plan and regenerated physical output;
  8. derive fresh plan, code, semantic, and capsule hashes; and
  9. immediately run the independent capsule verifier before returning it.

No caller-supplied byte vector is a construction input.

3. Verification order

Verification first revalidates the source-bound policy-1.4 baseline, then validates caps and non-zero identities, replays the prospective realization, reconstructs the complete expected candidate and capsule, and finally compares every field. Recomputing only the outer seal cannot make modified evidence or candidate bytes valid.

4. Non-execution invariant

This ADR does not add a conversion from the capsule to SourceBoundX64TargetArtifact, ExecutableMemory, the native runner, the native process worker, standalone authority, startup/ELF construction, or Gate B measurement. Public inspection may expose immutable identity and code bytes, but no accepted execution API consumes the capsule.

5. Exact fallback

Policy 1.4 remains the sole selected encoder and executable artifact. Any policy-1.5 capsule construction or verification error returns an error and leaves the baseline artifact untouched. There is no partially populated capsule, mixed physical layout, or automatic retry with candidate bytes.

The eventual selection rule must be explicit:

all policy-1.5 admission gates accepted -> select a verified candidate
anything else                         -> exact policy-1.4 artifact

6. Staged admission after the capsule

The capsule is necessary but insufficient for encoder-policy admission. Later work under this ADR must separately add and accept:

  1. finite 51-case target-plan/native correspondence for the candidate;
  2. process-isolated native correspondence and fault containment;
  3. standalone authority, startup, ELF, and 51-case process correspondence with migrated identities;
  4. fresh matched Gate B timing with the candidate selected before timing;
  5. the existing stability and <= 2.0x claim policy; and
  6. explicit promotion of encoder policy 1.5 only after all preceding gates.

Proof-profile weighting is not a timing result and cannot satisfy item 4.

Scope explicitly excluded from the first implementation slice

  • W^X mapping or execution of candidate bytes;
  • native/process/standalone/ELF identity migration;
  • Gate B timing or a performance claim;
  • changing the global X64_TARGET_ENCODER_POLICY_VERSION from 1.4.0;
  • general register allocation, spilling, vectorization, or new optimization classes; and
  • third-party tooling or proof dependencies.

Validation required before capsule-boundary acceptance

  1. deterministic capsule construction from a source-bound target and matching profile evidence;
  2. exact candidate bytes, labels, fixups, policy, and hashes match fresh raw replay;
  3. candidate plan differs from baseline only in the declared physical/policy fields;
  4. baseline, profile, realization, source, code, label, fixup, policy, and capsule mutations fail closed;
  5. self-resealing an altered capsule cannot bypass fresh regeneration;
  6. incomplete semantic proof, missing shadow, unsupported composition, and cap failures yield no capsule;
  7. policy-1.4 artifact and all executable identities remain byte-identical;
  8. no execution or packaging module imports or consumes the candidate type;
  9. focused tests plus full debug/release, strict, Clippy, format, and diff gates pass; and
  10. a fresh frozen Gate B profile regenerates the expected candidate capsule identity before this ADR becomes accepted.

All ten capsule-boundary items are accepted. The frozen candidate retains the ADR-0050 prospective code and realization roots while introducing distinct target-artifact and capsule domains:

prospective code hash    0e392caf51dbc65f9e36e08c678118e78b8f6aed90bf1df0edbf4b5c6a5f5173
realization hash         172b508e9648501162e28274afa3bcec0632f9cb3212e38f2b87b21ad7516198
policy-1.5 plan hash     f2145ac06a2c0cb789aced9a8751f6c6cbe8ddc14575a4ccbfa5b47f3fd9c5bd
target code-domain hash  ea1646e517562e42b2469420d6e4b4e16d86dcc9458ab03363acac60aa02b991
target semantic hash     4a290fde1eaf4c0df98383818af4a18b531ae6d86f5d859926e63f4620fde99c
candidate capsule hash   12fce4c6336b3c34a34ad05961b4fb75ae45427ca7b75b7bace98efdab886d24

The target code-domain hash intentionally differs from the prospective code hash although both cover the same 3,214 bytes: domain separation prevents a proof-only candidate digest from being confused with a target artifact code identity.

Focused construction/replay tests pass 2/2 and reject self-resealed profile root, byte, label, fixup, realization-receipt, semantic-completeness, zero-root, and cross-source mutations. The ordinary policy-1.4 verifier rejects the candidate policy by construction. The explicit ignored release gate regenerated the 2,526,207,757-step Gate B profile twice and passed 1/1 in 286.83 seconds. Full debug and release workspace suites, strict refinement 8/8, governance 22/22, Clippy with warnings denied, format, diff, and the static no-execution-consumer audit pass.

One first saturated release-suite run observed the pre-existing standalone timeout fixture return a different fail-closed containment classification. The fixture then passed three isolated release reruns, and the complete unchanged release command passed on immediate full rerun. No candidate code entered that fixture or any process path.

Consequences

Positive

  • Candidate identity becomes durable without widening the executable trust boundary.
  • Later migrations receive one exact, replayable source of candidate bytes.
  • The policy-1.4 fallback stays structurally explicit and unchanged.
  • Self-resealed candidate mutations remain insufficient.

Negative

  • Policy 1.5 still cannot run after this accepted first slice.
  • The candidate duplicates one physical target payload inside a sealed research artifact.
  • Frozen regenerative verification remains expensive because it must rebuild the canonical Gate B evidence.
  • Native, process, standalone, and measurement identities still require separate migrations.

Reversibility

The capsule is additive and has no execution consumer. It can be rejected or superseded without changing the accepted policy-1.4 target, native runner, or standalone artifacts.