Add experimental IxBy execution backends and repair Aiur let hoisting

[johnchandlerburnham]

Summary

Introduce IxBy as an experimental functional bytecode execution layer, with a
pure Lean reference model and three bounded Aiur/FRI interpreters. Each fixed
interpreter profile proves execution of different guest programs under the same
interpreter key. Also repair a shared Aiur let-hoisting bug discovered by object
interpreter differential tests, and regenerate the affected native kernels.

This is an experimental implementation and proof checkpoint, not certified
compilation from Ixon or a complete AIR-to-reference soundness theorem. Guest
programs are hand-authored. The ISA, profiles, wire format, and proof parameters
are not production commitments.

The branch is rebased onto main at 72238a58, with tip 306a5d75. Seven commits
separate the shared compiler repair, initial IxBy implementation, generated
kernels, and subsequent proof checkpoints. The rebased tree is byte-for-byte
identical to the saved, tested pre-rebase checkpoint.

No Flock-specific implementation, CLI, fixtures, dependencies, Compilatrix
changes, or production claim-format changes are included. Rust changes relative
to main are confined to the three regenerated files in crates/ixvm-codegen/src.

Implementation

• Functional reference semantics: immutable values and locals, constructor
  cases, direct/self/tail calls, explicit continuations, and reference
  PAP/application semantics. Evaluation is total and fuel-bounded, with checked
  determinism, fuel-extension, and conditional composition results.
• Crypto reference and artifacts: pure Word32, Goldilocks/extension-field,
  byte, and BLAKE3 operations; strict bounded profile/program/value codecs; and
  domain-separated profile/program/input/output commitments. Checked byte
  execution is connected to the functional reference semantics.
• Constrained execution: the interpreters authenticate raw program/input
  bytes, admit the whole image, execute it, serialize the actual terminal value,
  and check the expected output commitment. Unused code is admitted too. Decoded
  tables, execution traces, object pointers, ranks, and output values are not
  supplied as execution advice.
• Verifier interface: verification binds the caller's expected statement
  without rerunning reference execution or receiving execution advice. The
  adapter retains native-execution preflight and bounded proof decoding with
  exact reserialization checks.

Backend	Constrained execution coverage	Proved workloads / guest images
Scalar	Straight-line code and 20 scalar primitives	39 / 26
Control	Branches, calls/returns, recursion, tail calls, bounded continuations	50 / 40
Objects	Immutable constructors, projections, constructor cases, shared values	66 / 55

The object suite includes recursive list map and tail fold. Constructor identity
uses the full 40-byte name. Computed ranks and bounded field-list traversal
support finite-value representation; external input/output tree limits are
separate from intermediate object bounds. Each backend has its own profile/key,
reused across its guest images. Changing capacities can change the key.

Kernel-checked proof components

The proof modules now extend beyond conditional frame/heap representation to
contracts for concrete memory and actual compiled parser components:

• Concrete value/list layouts, successful reconstruction, immutable Store
  preservation, and checked constructor-table binding.
• Actual byte/u32/ten-limb identity readers, exact semantic ID comparison,
  bounded duplicate traversal, and complete bounded constructor-declaration
  parsing, including field-count and duplicate rejection.
• The recursive raw-advice reader and loader: successful loading establishes
  genuine bytes and preserves prior reads/I/O under explicit metadata, address,
  length, and allocation bounds.
• Program magic/revision and constructor/function-count prefixes, function and
  block headers, exact zero-count Nil stores, and continuation handoffs.
• Complete field/scalar and local/literal/erased leaf-operand readers. The actual
  field guard accepts precisely canonical eight-byte Goldilocks encodings;
  Boolean and field-component rejection, five/six-field layouts, u32 local-index
  bounds, actual Call behavior, and loader-to-operand composition are checked.

Structural certificates bind the relevant bytecode bodies, operations, dispatch
edges, return layouts, and required same-toplevel callees. Tests cover both full
compilation and pruned, relocated function indices. The latest checkpoint adds
67 public kernel-checked lemmas: 27 for code headers and 40 for scalars/operands.
The audited proofs use only Lean's standard logical axioms, with no proof holes,
custom axioms, native_decide, or proof-limit overrides in these new modules.

These contracts concern the Lean bytecode evaluator. Their byte-range, metadata,
capacity, and frame premises are explicit; loader composition discharges the
genuine-byte premise at identified prefixes. They do not assume or establish
complete instruction/table admission, canonical whole-program binding, compiler
correctness, or native/gadget/trace/AIR soundness. Errors carry no state, so the
parser contracts do not claim rollback on failure.

Shared Aiur compiler repair

Object differential testing exposed an assertion bypass: hoisting a
continuation's shadowing binding could change which variable an earlier
assertion checked. The original IxBy entry consequently accepted trailing
program bytes in compiled execution while source execution rejected them.

The repair makes caller/callee renaming collision-free, preserves shared pattern
bindings, sequences complete strict arguments left to right, and keeps
assertions, I/O, and debug operations before their continuations. Ordered
statement lets also preserve lowering of guarded inlined branches. The object
entry uses its original shadowed names again and rejects trailing bytes without
a local naming workaround.

Focused regressions compare explicit expected results/errors across original
source, normalized source, bytecode evaluation, and native execution, with
successful cases also proved, serialized, and independently verified. This is
regression coverage, not a formal compiler-refinement proof.

All three checked-in Rust kernels (aiur_ixvm.rs, aiur_multi_stark.rs, and
aiur_ix_aggr.rs) are regenerated. The rebase's sole conflict was the generated
IxVM kernel; regenerating from the rebased Lean sources resolved it.

Rollout: rebuild affected compiled circuits and proving/verifying keys.
The source repair does not retroactively fix old bytecode or old keys, and
unchanged wire revisions do not imply artifact compatibility.

Validation

The rebased tree passes a warning-free build and all 25,383 targeted IxBy
runtime checks, including full proving for all three backends:

Coverage	Checks
Reference / crypto / codec	263
Scalar / control / objects, including FRI proving	971
Concrete memory / constructor-table tests	317
Compiled parser certificates and contracts	23,832
Total	25,383

Parser coverage includes certificate mutations, exact codec agreement,
canonical field/Boolean rejection, local bounds, full-field pointers, padding,
truncation and malformed cells, fuel and Call boundaries, duplicate IDs,
allocation/deduplication, and loader composition. Forged non-byte memory tests
document the genuine-byte premise; they are not native/AIR soundness claims.

Additional validation of the shared repair and main integration passed:

• 2,064 hoisting/Aiur checks on the isolated branch, including 619 focused checks
  and 37 proof roundtrips, plus existing cross-engine/hash/cost/recursive-verifier
  coverage.
• Rebuilt IxVM kernel/adversarial/native-parity tests and current-main cost pins.
• All seven release ixvm-codegen tests.
• ix codegen --check for all three generated kernels, repeated after rebasing.

The latest proof additions introduce no new FRI workloads. Historical timing and
proof-size observations remain labeled as historical; no new isolated
performance claim is made. Repeated runs and theorem counts are not added to the
runtime-test total. These are local validation results; full GitHub CI and review
remain separate merge gates.

Reproduce

lake build --wfail ix IxTests AiurHoistingTests \
  Ix.Ixby.Aiur.ObjectsCodeHeaders Ix.Ixby.Aiur.ObjectsScalars \
  Ix.Ixby.Aiur.ObjectsOperands
RAYON_NUM_THREADS=8 .lake/build/bin/IxTests \
  ixby ixby-crypto ixby-codec ixby-objects-memory ixby-objects-table ixby-objects-parser
RAYON_NUM_THREADS=8 .lake/build/bin/IxTests --ignored \
  ixby-aiur-prove ixby-control-prove ixby-objects-prove
RAYON_NUM_THREADS=8 .lake/build/bin/AiurHoistingTests --prove --regression
RAYON_NUM_THREADS=8 .lake/build/bin/IxTests --ignored ixvm
.lake/build/bin/ix codegen --check
cargo test --release -p ixvm-codegen

Review focus and follow-up

The highest-impact review area is the shared hoisting repair: scope hygiene,
strict-argument effect ordering, and continuation/return behavior. The generated
kernel content check and rebuilt native parity are essential companion checks.
For the proof modules, review the exact certificate boundaries and remaining
premises rather than treating representation alone as execution verification.

Follow-up work remains explicitly outside this experimental checkpoint:

• Operand-list and instruction proofs, complete recursive block/function tables,
  cross-table validation, and authenticated canonical whole-program binding.
• Initialization and complete interpreter-transition invariants, remaining
  resource-bound discharge, general codec inverse/injectivity results, and full
  compiler/gadget/hash/trace/AIR refinement and malicious-witness auditing.
• Constrained closures/PAPs, general application, guest byte values, and the
  remaining crypto primitives. Broader reference support does not imply
  constrained support; Nat/String and caseNat remain outside the crypto profile.
• Compilatrix lowering and source-value/ABI correspondence, a Flock IxBy
  interpreter, terminal compression, and production activation.

Proof parameters and capacities are test-only, not deployment security
recommendations. The low-level native prover can still panic on execution
errors; negative fixtures stop at native execution, and this PR does not change
that API contract.

Further detail:
IxBy overview,
encoding,
and object backend and proof boundaries.