chore(aiur): Migrate Aiur to new pipeline

[arthurpaulino]

Replace old Aiur implementation with a new staged pipeline. The new pipeline has explicit IRs per stage (Source, Typed, Simple, Concrete, Bytecode) under Ix/Aiur/Stages/ and dedicated compiler passes under Ix/Aiur/Compiler/ (Check, Match, Simple, Concretize, Layout, Lower, Dedup).

Highlights:

• Ix/Aiur/Goldilocks.lean centralizes G arithmetic — Add/Sub/Mul instances, u8/u32 gadget semantics, eqZero, BitDecomposition, commutativity lemmas — removing duplicated gPrime/mkG/addG/ subG/mulG helpers from per-file evaluators.
• Ix/Aiur/Meta.lean is the DSL elaborator. The ⟦ ... ⟧ surface parses the same programs as before (including fold(i..j, init, |acc, @v| body), range slices trm[i..j], and indexed access/set via @v), with the fold construct unrolled at elaboration time.
• Polymorphic constructor patterns in nested matches now mangle correctly: the match compiler threads the per-switch scrutinee type through Decision.switch, so concretize's rewritePattern sees the right tArgs and rewrites List.Nil → List_G.Nil (etc.).
• Ix/Aiur/Interpret.lean is the partial debug interpreter — callCache, call-stack-trace errors, dbg_trace on .debug ops, plus two semantic refinements (ioSetInfo errors on existing key, ioRead errors on OOB).
• Ix/Aiur/Semantics/ keeps the reference evaluators needed by the cross-agreement tests: SourceEval (on Source.Term) and BytecodeEval (Lean-native bytecode evaluator), plus Flatten and BytecodeFfi. Proof-only evaluators (TypedEval, ConcreteEval) and the full proofs layer are excluded from this PR.
• Tests/Aiur/Cross.lean compares source-eval and bytecode-eval outputs on every surface-language program.
• Ix/Aiur/Statistics.lean ports the circuit-size reporter used by kernel.
• Ix/Lib.lean gathers generic List/Array/HashMap lemmas.
• lakefile.lean: precompileModules := true on the Ix lib to enable native_decide in G.one_ne_zero.

Consumers (IxVM, Kernel, Benchmarks, Tests/Aiur prover suite) migrated to the new API. lake test, lake test -- --ignored aiur ixvm, and lake exe kernel Nat.add_comm all pass with circuit widths/FFT cost identical to main.