Add experimental IxBy execution backends and repair Aiur let hoisting

.github/workflows/ci.yml

@@ -36,6 +36,10 @@ jobs:
       # lean-action builds above — fails CI.
       - name: Build all targets
         run: lake lint -- --wfail -v
+      - name: Check IxBy theorem trust manifest
+        run: lake build --wfail Ix.Ixby.Audit Tests.Ixby.Audit
+      - name: Check pure Stage 2 component trust manifest
+        run: lake build --wfail Ix.MultiStark.Verify.Audit Tests.MultiStark.Verify.Audit
       - name: Check codegen'd IxVM kernel is up to date
         run: lake exe ix codegen --check
       - name: Check Lean versions match for Ix and compiler bench
@@ -114,6 +118,60 @@ jobs:
         with:
           rust-version: ${{ env.RUST_VERSION }}
 
+  # The generic interpreter's gate library is an independent Cargo workspace.
+  stage3-core:
+    runs-on: warp-ubuntu-latest-x64-8x
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v7
+      - uses: ./.github/actions/setup-rust-toolchain
+        with:
+          cache-workspaces: flock-stage3
+      - name: Check Stage 3 formatting
+        run: cargo fmt --manifest-path flock-stage3/Cargo.toml --all -- --check
+      - name: Check Stage 3 lints
+        run: cargo clippy --release --locked --manifest-path flock-stage3/Cargo.toml --workspace --all-targets -- -D warnings
+      - name: Test Stage 3 native gates
+        run: cargo test --release --locked --manifest-path flock-stage3/Cargo.toml --workspace
+      - name: Prove retained and generic-component conformance circuits
+        if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch'
+        env:
+          RAYON_NUM_THREADS: 8
+        run: |
+          ulimit -v 33554432
+          timeout 300 cargo test --release --locked --manifest-path flock-stage3/Cargo.toml --workspace -- --ignored --skip ixby::exec::proof_tests:: --test-threads=1
+      - name: Prove direct generic scalar executions
+        if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch'
+        env:
+          RAYON_NUM_THREADS: 4
+        run: |
+          ulimit -v 33554432
+          timeout 600 cargo test --release --locked --manifest-path flock-stage3/Cargo.toml --workspace ixby::exec::proof_tests:: -- --ignored --test-threads=1
+
+  # The isolated terminal workspace is not part of root Cargo operations.
+  # These are native core regressions, not the full closed IxBy proof gate.
+  stage4-core:
+    runs-on: warp-ubuntu-latest-x64-8x
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v7
+      - uses: ./.github/actions/setup-rust-toolchain
+        with:
+          cache-workspaces: flock-stage4
+      - name: Check Stage 4 formatting
+        run: cargo fmt --manifest-path flock-stage4/Cargo.toml --all -- --check
+      - name: Check Stage 4 lints
+        run: cargo clippy --release --locked --manifest-path flock-stage4/Cargo.toml --workspace --all-targets -- -D warnings
+      - name: Test Stage 4 native core
+        run: cargo test --release --locked --manifest-path flock-stage4/Cargo.toml --workspace
+      - name: Verify generic Exec replay across guests
+        if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch'
+        env:
+          RAYON_NUM_THREADS: 4
+        run: |
+          ulimit -v 33554432
+          timeout 180 cargo test --release --locked --manifest-path flock-stage4/Cargo.toml -p ixby-stage4-exec native::tests::different_guests_have_identical_complete_replay_topology -- --ignored --test-threads=1
+
   # Compile and link the opt-in backend without requiring a GPU. Runtime and
   # proof-byte equivalence are covered by multi-stark's NVIDIA smoke suite.
   cuda-compile:

.github/workflows/merge-tests.yml

@@ -35,6 +35,13 @@ jobs:
             kind: lake
             runner: warp-ubuntu-latest-x64-32x
             test_args: --ignored decompile
+          - name: Lake ignored tests (IxBy proving)
+            kind: lake
+            runner: warp-ubuntu-latest-x64-16x
+            test_args: >-
+              --ignored
+              aiur-hoisting-prove ixby-aiur-prove
+              ixby-control-prove ixby-objects-prove stage2-codec-real stage2-wrapper-real
           - name: Lake ignored tests (misc)
             kind: lake
             runner: warp-ubuntu-latest-x64-32x

Cargo.toml

@@ -10,10 +10,9 @@ members = [
   "crates/ixon",
   "crates/kernel",
 ]
-# `zisk/` and `sp1/` are their own Cargo workspaces (guest + host) built via
-# the respective zkVM toolchains; excluded so host workspace ops don't pick
-# them up.
-exclude = ["zisk", "sp1", "multi-stark"]
+# Separate proving workspaces have independent toolchains/dependency graphs;
+# exclude them so ordinary host workspace operations do not build them.
+exclude = ["zisk", "sp1", "multi-stark", "flock-stage3", "flock-stage4"]
 resolver = "2"
 
 [profile.dev]

Ix/Ixby.lean

@@ -0,0 +1,15 @@
+module
+public import Ix.Ixby.Basic
+public import Ix.Ixby.Primitive
+public import Ix.Ixby.Validate
+public import Ix.Ixby.Eval
+public import Ix.Ixby.Composition
+public import Ix.Ixby.Profile
+public import Ix.Ixby.Codec
+public import Ix.Ixby.Commitment
+public import Ix.Ixby.Claim
+
+/-! Functional IxBy semantics, experimental crypto codecs and commitments.
+The first proving backend is a separate `Ix.Ixby.Aiur` import so this logical
+surface stays independent of the proving FFI. This is not a production IxVM
+claim implementation or a certified Compilatrix target. -/

Ix/Ixby/Aiur.lean

@@ -0,0 +1,99 @@
+module
+public import Ix.Ixby.Aiur.Objects
+public import Ix.Aiur.Protocol
+public import Ix.Aiur.Compiler
+
+/-! Experimental host interface to the fixed-profile IxBy Aiur interpreters. Kept
+separate from `Ix.Ixby` so the logical specification does not import an FFI
+proof oracle. This is not a production proof/claim format or source bridge. -/
+
+public section
+
+namespace Ix.Ixby.AiurBackend
+
+/-- Eight little-endian 32-bit limbs per digest. Each limb embeds injectively
+in Goldilocks; packing an arbitrary eight-byte chunk would not. -/
+def digestFields (digest : Commitment.Digest) : Array Aiur.G :=
+  (Array.range 8).map fun i =>
+    .ofNat (natOfBytesLE (digest.bytes.extract (i * 4) (i * 4 + 4)))
+
+def statementFields (statement : Commitment.Statement) : Array Aiur.G :=
+  digestFields statement.profile ++ digestFields statement.program ++
+    digestFields statement.input ++ digestFields statement.output
+
+/-- Raw advice intentionally performs no host admission: the circuit must
+establish bounds, canonical decoding, execution, and commitment binding. -/
+def artifactAdvice (programBytes inputBytes : Codec.Bytes) : Aiur.IOBuffer :=
+  (default : Aiur.IOBuffer).extend 0 #[0] (programBytes.map Aiur.G.ofUInt8)
+    |>.extend 1 #[0] (inputBytes.map Aiur.G.ofUInt8)
+
+structure System where
+  compiled : Aiur.CompiledToplevel
+  system : Aiur.AiurSystem
+  entry : Aiur.Bytecode.FunIdx
+
+/-- Shared adapter for the experimental interpreter entrypoints. -/
+private def buildSystem (source : Aiur.Source.Toplevel) (entryName : Lean.Name)
+    (commitment : Aiur.CommitmentParameters) (fri : Aiur.FriParameters) :
+    Except String System := do
+  let compiled ← source.compile
+  let some entry := compiled.getFuncIdx entryName
+    | throw s!"missing IxBy entrypoint {entryName}"
+  return ⟨compiled, Aiur.AiurSystem.build compiled.bytecode commitment fri, entry⟩
+
+/-- Explicit backend parameters: callers choose a test or reviewed security
+policy. The same compiled system is reused for different guest programs. -/
+def System.buildScalar (commitment : Aiur.CommitmentParameters)
+    (fri : Aiur.FriParameters) : Except String System := do
+  buildSystem (← scalarToplevel) `ixby_scalar_exec commitment fri
+
+/-- The control slice has its own fixed profile and key; guest function/block
+tables and dynamic call stacks do not participate in compiling that key. -/
+def System.buildControl (commitment : Aiur.CommitmentParameters)
+    (fri : Aiur.FriParameters) : Except String System := do
+  buildSystem (← controlToplevel) `ixby_control_exec commitment fri
+
+/-- Structured values have a separate fixed profile/key. Physical object
+pointers, ranks, and constructor tables are not public/advice inputs. -/
+def System.buildObjects (commitment : Aiur.CommitmentParameters)
+    (fri : Aiur.FriParameters) : Except String System := do
+  buildSystem (← objectsToplevel) `ixby_objects_exec commitment fri
+
+def System.claim (backend : System) (expected : Commitment.Statement) : Array Aiur.G :=
+  Aiur.buildClaim backend.entry (statementFields expected) #[]
+
+def System.execute (backend : System) (expected : Commitment.Statement)
+    (programBytes inputBytes : Codec.Bytes) :
+    Except String (Array Aiur.G × Aiur.IOBuffer × Array Aiur.QueryCount) :=
+  backend.compiled.bytecode.execute backend.entry (statementFields expected)
+    (artifactAdvice programBytes inputBytes)
+
+def System.prove (backend : System) (expected : Commitment.Statement)
+    (programBytes inputBytes : Codec.Bytes) : Except String Aiur.Proof := do
+  -- The current native prove FFI can abort on execution failure. Preflight
+  -- turns malformed advice into an ordinary error; it does not replace any
+  -- circuit check, and verification still needs neither advice nor execution.
+  let _ ← backend.execute expected programBytes inputBytes
+  let (claim, proof, _) ← backend.system.prove backend.entry (statementFields expected)
+    (artifactAdvice programBytes inputBytes)
+  unless claim == backend.claim expected do throw "IxBy prover returned an unexpected claim"
+  return proof
+
+/-- Verifies the caller's expected statement, never an unchecked statement
+returned by a prover. Does not need artifact bytes or rerun the evaluator. -/
+def System.verify (backend : System) (expected : Commitment.Statement)
+    (proof : Aiur.Proof) : Except String Unit :=
+  backend.system.verify (backend.claim expected) proof
+
+/-- Checked untrusted proof decoding; this is only native Aiur serialization,
+not a new IxBy artifact envelope or production deployment policy. The existing
+native decoder permits trailing bytes; exact canonical reserialization rejects
+them here. The size cap is local transport policy, not part of Exec semantics. -/
+def System.verifyBytes (backend : System) (expected : Commitment.Statement)
+    (bytes : ByteArray) : Except String Unit := do
+  if bytes.size > 64 * 1024 * 1024 then throw "IxBy experimental proof byte limit"
+  let proof ← Aiur.Proof.ofBytesChecked bytes
+  unless proof.toBytes == bytes do throw "IxBy noncanonical or trailing proof bytes"
+  backend.verify expected proof
+
+end Ix.Ixby.AiurBackend