GitHub

ADR-0052: Finite Policy-1.5 Candidate Native-Correctness Admission

Status: accepted for the finite in-process native-correctness boundary; process, standalone, ELF, timing, claim, and global policy-1.5 selection remain closed

Date: 2026-08-02

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

Related: ADR-0035, ADR-0036, ADR-0037, ADR-0038, ADR-0044, ADR-0049, ADR-0050, ADR-0051

Extends: ADR-0051 with the first deliberately narrow execution consumer for a verified policy-1.5 capsule

Preserves: encoder policy 1.4 as the sole globally selected policy; ordinary source-bound native execution; process, standalone, ELF, measurement, and claim authority; every accepted policy-1.4 identity

Context

ADR-0051 seals a complete policy-1.5 candidate but intentionally gives it no execution consumer. The next ordered admission step must answer one finite question: do the exact candidate bytes preserve canonical Machine-IR behavior for the already frozen 51-case Gate A corpus?

The candidate exists only for the BranchMix target. The five Bounds cases belong to a different target for which no policy-1.5 realization was proved. Those cases must therefore traverse the unchanged source-bound policy-1.4 path. This makes fallback an observed part of the finite admission contract, not an undocumented convenience.

The existing public native runner accepts only SourceBoundX64TargetArtifact. Weakening that type or pretending the policy-1.5 artifact was produced by policy-1.4 source replay would break the accepted trust boundary. Conversely, copying the W^X loader into a candidate module would create a second executable-memory implementation and enlarge the trusted computing base.

Decision drivers

  • Only a freshly verified ADR-0051 capsule may supply candidate bytes.
  • Candidate authority must be consumable only by the finite correctness orchestrator, never by a general public execution function.
  • The canonical Gate A manifest, case order, inputs, workload split, and Machine-IR evaluator must be regenerated internally.
  • All 46 BranchMix cases must execute policy 1.5; all five Bounds cases must execute the exact source-bound policy-1.4 fallback.
  • Candidate and fallback records must be domain-separated and identity-bound.
  • RW-copy and RX-readback hashes, W^X trace, MXCSR restoration, ABI, outcomes, and effect traces remain mandatory evidence.
  • Any candidate verification, execution, identity, or correspondence failure rejects the complete admission atomically. It cannot alter global selection.
  • This gate grants no process, standalone, ELF, timing, performance-claim, or general encoder-selection authority.
  • The implementation remains NAUX-owned and introduces no dependency.

Considered options

1. Change the global encoder policy to 1.5 and rerun existing tests

This would select the candidate before its downstream identities and failure boundaries were admitted. It also would not seal which cases used fallback. Rejected.

2. Convert the capsule to SourceBoundX64TargetArtifact

Policy 1.5 was not produced by the accepted policy-1.4 source verifier. Such a conversion would either be false or require weakening that verifier. Rejected.

3. Add a public execute_candidate(bytes, args) entry point

This would turn a finite proof capability into general native authority and would admit caller-provided bytes. Rejected.

4. Duplicate the executable-memory loader in a candidate module

This preserves type separation but creates a second mmap/mprotect/call/unmap TCB that can diverge from ADR-0038. Rejected.

5. Add an internal verified-artifact seam to the existing W^X runner

The public source-bound entry remains unchanged. One crate-private function accepts only the opaque verified capsule witness and delegates to the same bounded W^X implementation. Only the finite admission owner calls it. The result is sealed under a new candidate-correctness domain. Accepted.

6. Require child-process isolation in this first candidate execution gate

This gives stronger crash containment, but it also requires a new IPC protocol and independent child reconstruction/verification identity before the candidate has any finite native evidence. ADR-0051 already orders process isolation after finite native correspondence. Deferred to the immediate next gate; no process claim may rely on this ADR.

Decision

1. Narrow execution capability

The native module may expose one crate-private function whose parameter is VerifiedX64TargetPolicy15CandidateCapsule. It performs the same ABI checks, code caps, RW copy, copy hash, RX transition, readback hash, call discipline, MXCSR check, and unmap as the ordinary ADR-0038 runner.

The function is not re-exported from core, does not accept raw bytes or an unverified capsule, and cannot produce a source-bound artifact. Static audits must show that only the finite candidate-correctness module consumes it.

2. Fixed selection table

The gate regenerates the exact 51-case manifest and both lighthouse packages. Selection is a total function of the frozen workload tag:

BranchMix              -> verified policy-1.5 candidate (46 cases)
BoundsOrderedArrayGet  -> source-bound policy-1.4 target (5 cases)
anything else          -> reject

There is no caller override, runtime profile decision, automatic retry, or mixed target within a case.

3. Machine-IR reference and candidate evidence

For every case the owning lighthouse package independently evaluates its source-bound Machine IR under the existing Gate A budget. Native execution is normalized with the existing bit-exact/canonical-NaN/Bounds contract.

Each record seals at least:

candidate-correctness schema and policy
case ordinal, workload, selection, and canonical input hash
source Machine-IR identity
baseline target identity
executed target semantic/plan/code identities
candidate capsule identity (BranchMix) or explicit fallback marker (Bounds)
RW-copy and RX-readback code identities
mapping trace, MXCSR before/after, and input-lane count
Machine-IR and native normalized observations
per-record hash

The aggregate seals the canonical manifest, exact order, branch candidate identity, both baseline target identities, selection counts, all record hashes, and an order-sensitive results hash.

4. Verification and atomic failure

Public emission first independently verifies the capsule through the complete ADR-0051 replay, then executes all 51 cases. Public verification repeats capsule verification and reconstructs the expected finite evidence before comparison. A self-resealed mutation cannot become authority.

No selection state is written. Any error returns no evidence, and the global encoder constant and all ordinary execution/package paths remain policy 1.4. The word “fallback” in this ADR means preservation of that unchanged authority; it does not permit hiding a failed BranchMix candidate run by retrying it.

5. Explicitly excluded authority

Acceptance of this ADR does not authorize:

  • candidate execution through the public native runner;
  • candidate process workers or IPC;
  • standalone startup, ELF construction, or standalone correspondence;
  • Gate B timing, performance ratios, or claim admission;
  • global or per-program policy-1.5 selection outside this exact gate; or
  • changing X64_TARGET_ENCODER_POLICY_VERSION from 1.4.0.

Validation required before acceptance

  1. A freshly verified capsule is the only source of BranchMix candidate code.
  2. Exactly 51 canonical cases are emitted in ordinal order: 46 candidate and five policy-1.4 fallback records.
  3. Every record has Machine-IR/native parity under the frozen numeric/effect contract.
  4. Candidate records bind the ADR-0051 capsule and policy-1.5 target identities; fallback records bind the unchanged Bounds policy-1.4 identity.
  5. RW, RX, W^X, ABI, input-lane, MXCSR, source, plan, code, and artifact checks fail closed.
  6. Wrong order, workload, selection, input, observation, count, target, candidate, manifest, result, and self-resealed mutations fail replay.
  7. Candidate verification or execution failure returns no partial evidence and does not change global policy or accepted policy-1.4 identities.
  8. The ordinary source verifier and public native runner still reject or cannot accept the candidate type.
  9. Static import audit finds no candidate consumer in process, standalone, ELF, startup, or measurement modules, and only one crate-private native execution consumer.
  10. Focused tests, complete debug/release workspace suites, strict refinement, governance, Clippy with warnings denied, format, and diff gates pass.
  11. An explicit release-mode regenerative gate emits and independently verifies the frozen 51-case evidence before this ADR becomes accepted.

All eleven validation items are accepted. The frozen finite admission vector is:

ordered corpus cases             51
policy-1.5 BranchMix executions  46
policy-1.4 Bounds fallbacks        5
candidate capsule hash   12fce4c6336b3c34a34ad05961b4fb75ae45427ca7b75b7bace98efdab886d24
candidate target hash    4a290fde1eaf4c0df98383818af4a18b531ae6d86f5d859926e63f4620fde99c
candidate plan hash      f2145ac06a2c0cb789aced9a8751f6c6cbe8ddc14575a4ccbfa5b47f3fd9c5bd
candidate code hash      ea1646e517562e42b2469420d6e4b4e16d86dcc9458ab03363acac60aa02b991
correctness results hash 35018ad7571de6e946f70dd5db237e8a52024447bcce013d65228aaba5e361ba

The finite emitter executes candidate bytes only after receiving the opaque verified capsule witness. It uses the existing W^X mapper, installs canonical MXCSR for each admission invocation, restores the caller state, and records the exact Unmapped -> RW -> RX -> Unmapped trace plus both copy/readback hashes. The five Bounds cases execute through a separate crate-private wrapper around the unchanged source-bound policy-1.4 case runner.

The structural verifier independently rebuilds both lighthouse source packages before checking every record. Self-resealed selection, order, observation, capsule, input, target, manifest, count, and aggregate-result mutations fail closed. The public verifier then regenerates and executes the complete expected 51-case evidence, so a structurally plausible forged record still cannot become authority.

Focused admission tests pass 2/2; the explicit ignored release gate passes 1/1 in 455.78 seconds. That gate regenerates the full Gate B profile/candidate three times and executes two complete 51-case native passes for emission and independent replay. Complete debug and release workspace suites, strict refinement 8/8, governance 22/22, Clippy with warnings denied, format, diff, and static consumer audits pass. The static audit finds one policy-1.5 execution call site, inside this finite admission owner; no process, standalone, ELF, startup, or measurement module imports it.

Encoder policy remains globally 1.4.0. This accepted evidence is explicitly not process containment, standalone correctness, timing, or a performance claim.

Consequences

Positive

  • Policy 1.5 gains its first real execution evidence without becoming a generally selected encoder.
  • The old W^X implementation remains the sole executable-memory TCB.
  • The workload split and exact policy-1.4 fallback become seal-visible.
  • Later process admission receives one finite identity to migrate rather than an unstructured collection of test results.

Negative

  • Candidate native execution is initially in-process and therefore is not a fault-containment claim.
  • Independent public replay regenerates the expensive Gate B profile.
  • A second correspondence schema is required because the ordinary native evidence intentionally accepts only policy 1.4 source-bound artifacts.
  • Policy 1.5 remains unusable by applications after this gate.

Reversibility

The gate is additive and writes no selection state. It can be rejected or superseded by removing its private consumer and evidence domain without changing policy-1.4 execution. Any later process or standalone migration must use a new ADR rather than retroactively broadening this one.