Add experimental IxBy execution backends and repair Aiur let hoisting

[johnchandlerburnham]

Add IxBy as an experimental functional-bytecode execution layer, with a pure
Lean reference model, bounded Aiur/FRI and native Flock interpreters, explicit
execution/public-claim contracts, and a generic Stage 4 compression prototype.
The branch also implements and refines a pure, claim-bound Stage 2 verifier.

The latest checkpoint adds strict intake of the compiler's original
IXBF/IXFI/IXFO artifacts and constrained, source-authenticated whole-grammar
dispatch for an explicit small-file class. It is a foundation for proving the
real Init execution, not a completed Init execution proof.

This is experimental implementation and proof evidence, not production
activation, certified Compilatrix lowering, a native/AIR-to-reference soundness
theorem, or a complete terminal SNARK. Backend setups depend on approved
capacities and implementations, not the guest image or execution witness.
Changing a setup class requires an explicit key/identity upgrade.

This description covers jcb/ixby through 5d08f030, relative to main at
58eb0977. The shared Aiur let-hoisting repair and regenerated native kernels
are already in that base; the current PR retains the extended hoisting
regressions, rather than introducing those compiler/kernel changes again.

Lean semantics, Aiur execution, and trust boundaries

• Pure functional semantics cover immutable values and locals, constructors,
  direct/self/tail calls, explicit continuations, closures/PAPs and application.
  Evaluation is total and fuel-bounded, with determinism, fuel-extension, and
  conditional composition results.
• Canonical profile/program/value codecs and domain-separated commitments bind
  exact admitted bytes. Experimental Exec statements distinguish execution from
  source-level Eval; the public-result adapter binds the caller's canonical
  closed CheckEnv claim and approved profile/image, while keeping the input
  commitment private at the terminal boundary.
• Three bounded Aiur interpreters authenticate program/input bytes, admit unused
  code as well as executed code, execute, and serialize the actual terminal
  value. Their earlier proof checkpoint covers 39 scalar, 50 control, and 66
  object workloads, with a fixed key per backend class.
• Kernel-checked components cover concrete memory/store representations,
  constructor identities and uniqueness, actual compiled readers and loader
  prefixes, code headers, canonical scalars, and leaf operands. Ordered-frame
  and first-order decoded-control rules connect finite traces to byte execution
  under explicit instruction, operand, codec, and representation premises.
• Exact theorem/import audit gates cover 333 IxBy public roots and 279 pure
  Stage 2 verifier roots, including negative audit regressions. These checks
  do not turn component contracts into compiler or native-constraint refinement.

The pure Stage 2 implementation includes canonical key/proof/claim codecs,
key and sparse-shape admission, transcript/PoW, AIR/logUp/OOD, shared Merkle
multiproofs, PCS reduction, and complete FRI verification. Independent typed
and byte-level relations establish deterministic soundness and completeness
for the admitted bounded classes. The source wrapper fixes the configuration,
derives the exact native statement, and returns the original public claim only
on success. This does not approve an arbitrary key, establish the aggregate
program's interpretation of Ixon claims, or prove cryptographic soundness.

See the IxBy overview,
Exec contract,
and Stage 2 verifier boundaries.

Native Stage 3 execution

The independent flock-stage3 workspace connects constrained canonical byte
admission, instruction/operand dispatch, complete bounded machine transitions,
exact fuel and halting, derived output serialization, and the full
profile/program/input/output commitment chain.

Explicit setup classes support:

• Scalar/control execution and all 35 existing crypto-v0 primitives, including
  immutable byte values and guest BLAKE3.
• Immutable constructors, projections, constructor cases, and canonical tree I/O.
• Revision-1 exact bounded Nats, all seven Nat primitives, and caseNat, without
  conflating Nats with wrapping Word32 values.
• Closures/PAPs, let/tail application, under/exact/over-application, and mixed
  caller-resume/apply-rest continuations. Optional exact Nats compose with this
  setup; Strings remain outside native Exec admission.

Fresh verifier processes receive only the approved setup, externally expected
statement digest, and proof. They do not receive private artifacts or rerun
guest execution to admit proofs. Negative tests include locally recomputed,
valid gate rows whose substitutions must fail global wiring, as well as
changed statements, malformed envelopes, and cross-setup substitution.

Representative completed native proof checkpoints include 39 scalar cases,
21 constructor cases, 30 exact-Nat cases, and 27 application cases under their
respective fixed setups. The application corpus produces 405,243-byte Exec
proofs and rejects three recomputed capture/argument/continuation substitutions.
Its optional-Nat execution differentials are not a complete application/Nat
proof corpus.

The packed-word BLAKE3 implementation is an explicit backend/key upgrade, with
all 39 scalar cases also proved under that setup. The legacy backend and older
factory identities remain distinct and unchanged. Current factories remain
small bounded prototypes: at most four functions, 64 transitions, and 512-byte
program/I/O buffers. Those bounds are not full-guest or production approvals.

See the native workspace
and application proof evidence.

Original-wire intake and authenticated dispatch

This is the newest implementation layer and remains separate from native Exec
admission:

• A strict host loader preserves exact IXBF format-1/semantics-0 program bytes
  and IXFI/IXFO transports, arbitrary-precision metadata, complete typed syntax,
  canonical encodings, and whole-image/value validation. The read-only
  ixby-ixbf-inspect CLI always reports proving_admitted: false; its inventory
  is not execution evidence or a trusted circuit-admission oracle.
• Constrained components cover exact u128 header metadata, canonical Nats up to
  4,096 physical bits, all thirteen record decoders, reference/arity components,
  complete program/value-forest grammar control, checked payload spans, the
  actual guest Nat limit, and streaming strict UTF-8.
• Original-byte windows are authenticated with constrained raw BLAKE3 chunk
  paths. A separate final-chunk path binds the claimed file length.
• The fixed dispatcher derives decoder selection, bounds, byte requests, and
  cursor updates from carried state. All decoder paths are emitted; no host AST,
  event schedule, Nat byte length, or acceptance bit selects the active decoder.
  A final Done row requires exact EOF and exhausted grammar obligations.
• A separate exact 64-bit global-fuel component proves conservation/exhaustion
  accounting. It does not yet consume actual segmented-VM transition wires or
  upgrade the old Exec fuel/profile boundary.

The source-bound whole-grammar proof class fixes 1,024 bytes, 32 dispatcher
steps, and 4,096 physical Nat bits. It hashes one private buffer once and reuses
the same authenticated byte wires for every request. Eight Program/Input/Output
proofs verify in fresh processes, each 381,732 bytes; six locally recomputed
forgeries reject at wiring. The verifier receives externally expected digest,
context, and final-state words plus proof, without source files or a native
parser. This component has its own strict envelope and transcript domains;
it is not an Exec proof.

AST-free row differentials additionally cover 81 independent compiler programs
and the exact retained Init artifacts: a 1,002,355-byte program with 681
functions and 37,879 dispatcher steps, a 9,611,120-byte input, and a 49-byte
output. These are relation/differential checks, not a source-authenticated
full-Init proof. The earlier 5,372,353,187-transition native Init run is also
runtime evidence, not a Flock proof.

Remaining links include authenticated typed registry materialization,
ownership/ordered coverage/forward-reference and full semantic checks, scalable
shared chunk authentication, and the raw-file-digest-to-Exec commitment bridge.
Matching a host transcode or a sample output does not establish those links.

See the dispatcher contract and evidence
and the full-guest scaling gates.

Generic Stage 4 prototype

The independent flock-stage4 workspace imports reusable trace/R1CS/KZG-FFLONK
cores and adds generic Exec replay. Proof-free compilers reconstruct the full
verifier topology and exact setup-owned table programs before a guest or proof
exists. The closed compositions constrain every deferred table claim and bind
the expected public-result digest; root-conditional diagnostics remain clearly
separate.

Exact structural/cofactor representations, packed hash tables, reusable
constrained F128 operand preparation, and polynomial-range carry constraints
reduce costs under explicit composition identities. Streaming setup and
assignment checking retain canonical relation identities and reject partial
results, exceeded budgets, and observer failures. File-key storage derives C0
and sigma evaluations from authenticated coefficients/permutation data while
preserving key and proof equivalence in the checked small cases.

The completed 2026-09-13 tiny-class run checked every one of 757,209,570 R1CS
constraints in a real replay assignment and counted 1,042,919,351 PLONK
constraint rows, fitting the supported 2^30 domain for that explicit
composition. This supersedes earlier rejected-prefix censuses only for that
class. It uses a 64-byte program, 32-byte I/O, and four transitions—not the
larger native setup or Init.

No full terminal PLONK arena/key/SRS was materialized and no complete Stage 4
proof was produced. The modeled arena is still about 271.7 GiB, and key plus
SRS payload about 688 GiB before scratch. Complete resource admission and an
isolated full-relation proof remain open. A 992-byte FFLONK body from existing
small/component proofs does not establish a compact generic terminal proof.

See Stage 4 results and limitations.

Validation

Latest local release validation for this checkpoint:

Check	Result
Stage 3 workspace	223 passed; 38 opt-in/ignored
Stage 4 workspace	266 passed; 39 opt-in/ignored
Complete original-wire codec regression	All 17 opt-in tests passed; 66 honest proofs verified and 51 locally recomputed forgeries rejected at wiring
Both native workspaces	Formatting and release Clippy on all targets passed with warnings denied
Commit preparation	Staged diff whitespace check passed

The combined codec regression includes external corpus/Init differentials and
the new dispatcher proofs; it is not 17 distinct execution-proof classes.
Resource measurements are labeled per command in the component documents;
overlapping local runs are not exclusive-host benchmarks.

Earlier documented checkpoints include 25,383 targeted Lean/IxBy runtime
checks and full Aiur proving, the pure Stage 2 native differentials, the native
Exec proof corpora, and the complete small-class Stage 4 assignment check.
Those historical results are not claimed as newly rerun by this commit.
Full GitHub CI and review remain separate merge gates.

Representative reproduction commands:

cargo test --release --locked --manifest-path flock-stage3/Cargo.toml --workspace -- --test-threads=1
cargo test --release --locked --manifest-path flock-stage4/Cargo.toml --workspace -- --test-threads=1
cargo fmt --manifest-path flock-stage3/Cargo.toml --all -- --check
cargo fmt --manifest-path flock-stage4/Cargo.toml --all -- --check
cargo clippy --release --locked --manifest-path flock-stage3/Cargo.toml --workspace --all-targets -- -D warnings
cargo clippy --release --locked --manifest-path flock-stage4/Cargo.toml --workspace --all-targets -- -D warnings

RAYON_NUM_THREADS=4 cargo test --release --locked \
  --manifest-path flock-stage3/Cargo.toml -p ixby-flock \
  ixby::ixbf_decode::dispatch::proof_tests:: -- --ignored --nocapture --test-threads=1

lake build --wfail Ix.Ixby.Audit Tests.Ixby.Audit \
  Ix.MultiStark.Verify.Audit Tests.MultiStark.Verify.Audit
lake test --wfail -- ixby-flock-applications
lake test --wfail -- stage2-codec stage2-claim stage2-key stage2-transcript \
  stage2-shape stage2-ood stage2-mmcs stage2-fri stage2-pcs stage2-source

The full ixby::ixbf_decode:: ignored selection also requires the four explicit
retained-fixture environment variables documented in
the record regression guide.
Heavy proof/census jobs are separately opt-in and need their documented
memory/time admission; the commands above do not certify those resource budgets.

Scope and review priorities

Both experimental native workspaces are excluded from the root Cargo workspace.
Flock remains pinned to b310f35f35f68095537150a1c8c0a43caca9a29e; root dependency
pins and production claim semantics are unchanged. No Compilatrix changes,
production activation, or paid-resource expansion is included. Prototype
capacities and proof parameters are not deployment security recommendations.

Review the exact statement/setup identities, whole-image and source-byte
binding, cross-table/state wiring, canonical encodings and final EOF/halting
conditions, and the explicit premises of each Lean theorem. Local gate
validity, native agreement, or a component proof must not substitute for the
missing end-to-end relation.

Follow-up remains: source/image/ABI certification and native constraint
refinement; complete original-wire semantic admission; streaming witnesses and
scalable authenticated code/memory; complete execution segments with actual
VM-derived global fuel and sound composition; the full pinned Init Stage 3
proof; and resource-admitted terminal materialization/proving with isolated
verification and no root sidecars.