Aiur test pipeline: proving/execution split, unconstrained-op typing, full cross-engine coverage

[arthurpaulino]

Restructures the Aiur test suites around what each execution mode actually
checks, closes a type-level soundness hole in the unconstrained ops, and
brings every Aiur bytecode op up to 4-way engine coverage — which
immediately caught and fixed four real bugs.

Closes #454

Suite split: aiur-prove / aiur-cross

• aiur-prove (renamed from aiur) is now the proving suite: 29
  cases, each pinning a distinct constraint, selector-gating, or
  lookup-argument configuration — the things execution never evaluates.
  Its toplevel is pruned to functions reachable from those cases, and the
  minimal covering set of paths keeps proofs while redundant path
  variants moved to aiur-cross (down from ~70 proofs originally).
• aiur-cross is the compiler/interpreter suite: every case runs
  4-way agreement — Source.Eval (reference), Aiur.Interpret
  (debug interpreter), Bytecode.Eval, and the native Rust executor —
  on both values and IOBuffer, plus negative-path agreement (all four
  engines must reject: assert mismatch, range-check failure,
  non-exhaustive match, missing IO key, OOB IO read). The toplevel is
  compiled once instead of once per case.
• aiur-hashes proves only boundary sizes (blake3 0/1088, sha256
  0/65 — one small and one multi-chunk per distinct wide circuit); the
  other 25 sizes execute against the Rust reference. The interpreter now
  also runs the smallest hash sizes and rbtree-map.
• Test FRI parameters drop the proof-of-work grinding (2^20 hashing per
  proof, testing nothing) and use numQueries := 64, matching the
  Rust-side unit tests.
• AiurTestCase ergonomics: .prove / .interp / .exec constructors
  with a label parameter; executionOnly renamed to withProof.
• The ixvm codegen-parity gate reuses the kernelChecks cases, removing
  a duplicated per-constant witness-building pass (~5.6s of setup).

Bugs found by the new agreement matrix

The two Lean evaluators had only ever been compared against each other;
the interpreter and native executor had never joined the comparison. The
4-way matrix exposed:

1. Source.Eval: .ret evaluated as a normal value, so return
   inside a non-tail match arm fed the continuation instead of exiting
   the function. Fixed with an earlyReturn sentinel on the error track,
   unwrapped at the function boundary.
2. Bytecode.Eval: Ctrl.return was handled identically to
   Ctrl.yield, running matchContinue continuations after a
   function-level return. Same sentinel fix, mirroring the Rust
   executor's continuation-stack truncation.
3. Interpret.runFunction: missed the .ret catch for the entry
   function itself ("unexpected return").
4. G.ofNat narrowed through toUInt64 before reducing mod p, so
   any field op whose intermediate exceeds 2^64 — Mul products,
   Add/Sub carries, and therefore G.pow/G.inverse — wrapped mod
   2^64 instead of mod p. All three Lean evaluators agreed with each
   other and diverged only from the native executor. Fixed by reducing in
   Nat before narrowing.

Unconstrained ops: advice must not type as u8

u8's contract is "known to be range-checked", but the unconstrained
ops returned prover advice typed as bytes, upheld by caller discipline
only:

• unconstrained_big_uint_div_mod now has a fixed signature
  (bigUintDivModResultTyp in the checker): inputs must be a pointer to
  a list datatype instantiated at [U8; 8] (e.g. KLimbs), and each
  result is the same datatype at [G; 8]. Non-conforming inputs fail
  with a dedicated checker error. Kernel-side, klimbs_range_check
  (check-and-discard) becomes glimbs_to_klimbs: the u8_range_check
  outputs are what mint the u8 limbs — the only door from advice back
  into KLimbs.
• unconstrained_g_to_bytes returns [G; 8] for the same reason;
  its consumers (idx_to_u64 in the IxVM ingress, gl_to_bytes in the
  MultiStark verifier) mint bytes from their range-check outputs.

to_field is an erased coercion, so the g_to_bytes change leaves the
compiled bytecode byte-identical. The div_mod kernel restructure shifted
nine FFT pins and the shard pin marginally down (re-measured and
re-pinned; codegen regenerated, parity green).

unconstrained_big_uint_div_mod implemented in the Lean evaluators

Previously stubbed with an error in all three Lean engines — the last
op without cross-engine coverage. All three now mirror
crates/aiur/src/execute.rs exactly: width-10 limb-chain walk (tag
0 = Cons / 1 = Nil, per-byte range checks, cycle-bounded), Nat
division (which gives the runtime's b = 0 → (0, a) convention for
free), and canonical rebuild in the Rust builder's allocation order with
content dedup. Shared limb codecs live in Goldilocks.lean with proven
termination. Source.Eval's store/load arms are refactored onto shared
storeValue/loadValue helpers, and the Semantics files no longer
use panicking accessors — this code is slated for formal verification.

Coverage: divmod_test (plain / unit divisor / zero divisor / two-limb
dividend) and hint_test (g_to_bytes recomposition + canonicality on
p−1, g_inverse on 7 and 0) run 4-way agreement in aiur-cross and one
proof each in aiur-prove.

Quick suites promoted to primary

aiur-prove (~11s), aiur-hashes (4s), rbtree-map (2s),
multi-stark (2s), and recursive-verifier (3s — its "~1.5 min"
comment was stale) now run by default as primaryRunners: deferred IO
actions, so their setup doesn't execute at module initialization for
unrelated invocations. Runner names work as filter args, and the primary
section gains the same unknown-name guard the ignored section has. Only
ixvm remains in the ignored Aiur set.

CI

• aiur-cross previously never ran in CI (primary suites were
  filtered to tc-unit); it now runs in the "Aiur tests" step together
  with the promoted quick suites.
• Separate "IxVM kernel tests" step keeps --ignored ixvm.

Validation

• Full default lake test (all primary suites + runners): ~11.5s wall,
  green.
• aiur-cross: 1000+ checks including 20 rejection checks and the two
  new aggregates; aiur-prove: 29 proofs; aiur-hashes, rbtree-map,
  multi-stark, recursive-verifier, ixvm (pins, codegen parity,
  arena, exploits, shard): all green.
• cargo fmt clean, cargo clippy --release --workspace --all-targets --all-features zero warnings.