P1 Lighthouse Contract

Status: active; R1-S8 finite standalone correctness accepted; Gate B/P1 open
Target: CoreVM0 + branch_mix_kernel
Projection: Futamura P1

1. Claim

The first projection is:

MIX(CoreVM0, static_branch_mix_bytecode)
    =
standalone_residual_branch_mix

The bytecode program and interpreter semantics are static. The input array and repetition count are dynamic.

Trace capture, runtime profile specialization, or manually constructing the expected residual loop does not satisfy this contract.

2. CoreVM0

CoreVM0 is a definitional stack-bytecode interpreter written in the admitted Core-N0 subset.

Required opcodes:

ConstI64
ConstF64
LoadArg
LoadLocal
StoreLocal
AddI64
SubI64
AddF64
SubF64
CmpLtI64
CmpGeI64
ArrayLenF64
ArrayGetF64
Jump
JumpIfFalse
ReturnF64

Each opcode has a versioned type, stack effect, numeric mode, error behavior, and control-flow rule.

ADR-0029 and ADR-0030 now implement the verified Rust seed, canonical full ProgramImage, raw-input admission boundary, and generic definitional P1V0 artifact. Bounded seed-vs-Core parity is green under corevm0_core_artifact_contract.md. This is the pre-P1 semantic gate. Gate A below still requires an independently admitted Residual Core produced by MIX; generic-interpreter parity alone is not Gate A.

ADR-0031 R1-S1 implements the bounded pure-scalar P1V0 polyvariant worklist. ADR-0032 R1-S2 extends that line through a separate identity with recursively pure Tuple/Sum partial values, known/unknown Sum control, alias-normalized flattened signatures, and bounded zero-residual helper result propagation on an explicit frame machine. Both slices publish only ordinary verifier-accepted Residual Core; the S1 identity remains frozen.

ADR-0033 R1-S3 now admits dynamic read-only Array, preserves Error and source region/effect signatures, and binds a concrete four-opcode Bounds CoreVM0 package through program/image/semantics identities. That accepted slice does not specialize the frozen branch-mix lighthouse.

ADR-0034 R1-S4 now specializes the frozen all-opcode branch-mix package using canonical static/helper summaries and an explicit recursive-state quotient. Its ordinary verified Residual Core passes a structural dispatch-erasure checker, and raw-input regenerative replay rejects artifact, evidence, and static-program substitutions. This is the structural-erasure/replay subgate. R1-S5 now closes the bounded three-engine Gate A evidence and the verified residual-SSA handoff under ADR-0035 and corevm0_gate_a_r1_s5_contract.md. Its fixed 51-case evidence is finite translation validation, not an infinite-domain theorem. Native output and Gates B/C remain open.

ADR-0036 R1-S6 now lowers that exact verified Core SSA envelope into a canonical target-independent Machine IR with its own verifier, bounded evaluator, source-bound regenerative replay, semantic identity, and hard limits. All 51 cases preserve exact outcomes and ordered effect traces across Residual Core, Core SSA, and Machine IR under core_machine_ir_r1_s6_contract.md. This closes the pre-native trust boundary only; it emits no target opcode, native byte, standalone artifact, or performance evidence.

ADR-0037 R1-S7a now lowers that exact source-bound Machine IR into a canonical Linux x86-64/SSE2 target plan and NAUX-owned position-independent bytes. It freezes the lighthouse ABI, stack-home and tail-transfer layout, checked Bounds templates, PcRel32 fixups, numeric state, target-plan evaluator, ordinary byte replay, source replay, identities, and hard limits. The same 51 cases preserve Machine-IR-versus-plan outcomes and ordered effects under x86_64_target_r1_s7a_contract.md. ADR-0044 now governs the current encoder policy 1.4.0: reachable-body DCE uses one-byte label tombstones, exact unique-predecessor one-operation superblocks keep typed scalar results in R8/XMM2, and every substitution or final copy is exact or falls back to the already validated ordinary encoding. This changes target realization and all downstream identities, not the target-plan semantics or upstream contracts. R1-S7a does not execute those bytes. R1-S7b owns W^X loading, exact entry/code binding, no-fallback evidence, and finite native correspondence. ADR-0038 and x86_64_native_runner_r1_s7b_contract.md freeze that next boundary. S7b-a now executes all 51 frozen cases through the source-bound W^X runner without fallback and matches Machine IR in-process. S7b-b now binds those executions to opaque Gate A cases, exact ABI/code/limit identities, nested execution/correspondence records, the exact manifest, and the locked ordered result 73ecf90e2fff7a36a6011e447c0982ca317f591aea45486f55c330d8dc12d22c. S7b-c now runs every case in a fresh child that independently rebuilds and source-replays the exact artifact, communicates through bounded canonical IPC, and is admitted only after normal exit plus parent-side target and Machine IR verification. Its isolated result is 7700c126528db9bbe810f5396129d155da407d365e1dfa12e346adfbd5df37e1. R1-S7b is complete. ADR-0039 and x86_64_standalone_r1_s8_contract.md now freeze the standalone correctness subgate: opaque S7b-bound authority, one direct linker-free ELF64 image per workload, a bounded syscall-only startup, exact dynamic I/O, independent reconstruction, and fresh-process 51-case correspondence. Its host-side protocol codec, opaque authority, typed/raw startup, deterministic direct-ELF writer, independent ELF parser, artifact identity, and authority-composed raw-image verifier are implemented. Both workload images pass live-authority reproduction, exhaustive startup and artifact mutation rejection, cross-profile rejection, direct smoke execution, and fresh-process ordered 51-case correspondence. ADR-0040 additionally seals the predecessor Core↔SSA and SSA↔Machine IR roots into inherited authority. The locked R1-S8 result is 22897dc524804625751f027a820bb75f4da3f7e77afca5183bc1522542418b85. R1-S8 is accepted at this finite correctness boundary; the controlled <= 2.0x performance gate remains open. Three policy-1.4.0 local observations, 4.822709x, 4.796549x, and 4.884944x, improve 16.78%–18.29% over policy 1.3.0 and span only about 1.85%. Local-only metadata, failed CV checks, and the missed threshold make all three ineligible to close Gate B.

3. Program

The static bytecode implements the semantic kernel of the existing bench_branch_mix workload:

state = 0
sum = 0.0

repeat reps:
    for value in input:
        state = state + 17
        if state >= 97:
            state = state - 97
        if state < 48:
            sum = sum + value
        else:
            sum = sum - value

return sum

Static:

opcode sequence;
constants 17, 97, and 48;
local layout and types;
stack effects;
branch targets;
bytecode length.

Dynamic:

read-only Array<F64>;
array length;
repetition count;
array values.

The harness must include zero length, zero repetitions, boundary state values, NaN, infinities, signed zero, and non-vector-length input cases permitted by the numeric contract.

4. Correctness relation

Gate A requires:

eval_CoreVM0(program, input)
≈
eval_ResidualCore(MIX(CoreVM0, program), input)

≈ preserves:

returned F64 under the strict numeric contract;
typed errors;
bounds behavior;
effect trace;
evaluation order;
logical alias behavior admitted by the subset.

Tests do not prove an infinite-domain theorem. Evidence must distinguish:

bounded exhaustive verification;
property/differential/fuzz evidence;
translation-validator guarantees;
any formal theorem actually established.

5. Required evidence

Correctness evidence:

opcode-level CoreVM0 unit tests;
Surface/VM workload oracle comparison;
CoreVM0 vs Residual Core differential tests;
bounded exhaustive cases for small arrays, values, and repetition counts;
deterministic property/fuzz corpus;
mutation-of-static-input negative tests;
numeric edge cases;
forged-certificate rejection tests.

No benchmark begins until Gate A is green.

6. Termination and budgets

The specialization request declares:

max_static_steps
max_unfold_depth
max_residual_nodes
max_specialized_versions
max_specialization_time

Exhaustion must:

residualize a semantically valid generic operation when the contract permits; or
fail with a typed specialization-budget result.

It must not hang, emit unverifiable Core, or silently invoke the existing trace JIT.

7. Structural certificate

The certificate is generated from verified Residual Core or verified SSA, not inferred only from machine bytes.

Required semantic fields:

schema
core_schema_version
source_program_hash
interpreter_semantics_hash
specializer_hash
specialization_policy_hash
residual_core_hash
residual_cfg_hash
translation_validator_version
numeric_contract_hash
ffi_contract_hashes
budget
budget_usage

For the frozen Core-N0 P1V0 interpreter semantics admitted into B0:

interpreter_semantics_hash =
d9911cf60e5afa54e271cdff274cde41b522a4a0c9855ccd6efbcd4e981909cc

The framing and profile vectors are normative in core_n0_interpreter_semantics_identity_v1.md. This locked identity is provenance, not proof that B0, a residualizer, or P1 already exists.

Required structural assertions:

contains_opcode_value             = false
contains_dispatch_switch          = false
calls_interpreter_entry            = false
calls_interpreter_step             = false
calls_generic_opcode_handler       = false
dynamic_program_counter            = false
unresolved_static_program_operand  = false
interpreter_fallback               = false

The independent checker recomputes hashes, verifies schemas and CFG, and rejects missing or unknown assertions.

Machine-code scanning and disassembly are secondary evidence.

8. Standalone requirement

Gate B requires the residual artifact to:

accept only declared dynamic inputs;
execute without CoreVM0 bytecode dispatch;
execute without the AST interpreter, bytecode interpreter, or trace JIT;
contain no link to a generic opcode handler;
preserve errors and bounds behavior;
fit declared residual node, code-size, and specialization budgets;
reproduce bit-for-bit when all hashed inputs and host target are identical.

9. Native provenance

The initial native path may reuse the NAUX-owned x86-64 instruction encoder. It must preserve provenance:

CoreVM0
→ binding-time analysis
→ residual Core
→ verified SSA
→ Machine IR
→ native bytes

The current trace JIT may donate:

encoder routines;
CPU feature detection;
executable-memory support;
parity cases;
branch-mix input;
baseline methodology.

It may not replace the binding-time analyzer or residualizer.

R1-S6 is the only canonical Machine IR input to this path. ADR-0037/R1-S7a freezes the x86-64 ABI and checked target-lowering relation and admits only its own re-encoded bytes. ADR-0038/R1-S7b now loads only the opaque source-bound artifact through a verifier-gated W^X runner and publishes process-isolated finite native correspondence. ADR-0039/R1-S8 requires an opaque authority derived from that complete package, copies the verified R1-S7a target blob exactly once into a direct ELF64 image, and independently reconstructs every startup and image byte without reopening raw-byte authority.

10. Baselines

The controlled comparison contains:

generic C and Rust CoreVM0 interpreters executing the static bytecode;
hand-specialized C and Rust implementations of the same branch-mix semantics;
NAUX-generated residual native code.

All implementations share:

input bytes and expected checksum;
strict I64/F64 contract;
bounds policy;
algorithm and operation order;
warmup and measurement policy;
CPU feature policy;
compiler flags recorded in the artifact.

Fast-math, undefined signed overflow, hidden precomputation, different allocation scope, or a different algorithm makes a row ineligible.

11. Performance gates

Gate B — Viability

Gate B is the conjunction of:

completed R1-S8 standalone correctness (artifact, independent verifier, and fixed 51-case direct-process correspondence); and
an eligible controlled run of that same standalone path at no more than 2.0x the hand-specialized runtime.

Milestones:

first native residual: no more than 2.0x the hand-specialized runtime;
mature residual: no more than 1.25x the hand-specialized runtime;
P1 graduation: within 10% of the hand-specialized runtime.

Gate C — Differentiation

At least one is required for the first public lighthouse result:

NAUX residual is at least 1.25x faster than the generic C/Rust engine; or
NAUX residual is within 10% of hand-specialized C/Rust while being generated from the generic interpreter.

The North Star graduation target requires both on a controlled eligible run.

12. Artifact

The claim bundle includes:

all source and Core artifacts;
static bytecode;
input generator and raw inputs;
expected outputs;
specializer request and certificate;
residual Core, SSA, Machine IR, native bytes, and disassembly;
generic and hand-specialized baselines;
build commands, tool hashes, and flags;
machine fingerprint;
raw samples and summary statistics;
independent verification command.

The bundle verifier is fail closed and operates without network access.

13. Definition of done

P1 lighthouse is complete only when:

CoreVM0 and the static program verify;
Gate A evidence is green;
structural certificate is independently accepted;
Gate B standalone requirements are met;
a controlled comparison satisfies Gate C;
the complete artifact reproduces from one clean source revision;
documentation does not describe a trace as a projection.