IOBuffer channels

[arthurpaulino]

Adds a per-channel dimension to Aiur's IOBuffer and uses it to clean
up IxVM's key-suffix workaround for distinguishing constants, blobs,
and reducibility hints.

Motivation

Today IOBuffer is a single keyed store: any two pieces of
non-deterministic data that happen to share a key collide. IxVM works
around this by appending a discriminator byte to keys (addr ++ [0]
for blobs, addr ++ [1] for hints). The workaround scales poorly,
clutters every reader, and forces all subsystems into one global
namespace.

A channel : G argument on every IO op gives each subsystem its own
key space and its own data arena, with no semantic cost — IOBuffer
is unconstrained, so channels are pure prover-side namespacing.

What changed

Aiur core

IOBuffer is now two-axis:

structure IOBuffer where
  data : Std.HashMap G (Array G)            -- per-channel arenas
  map  : Std.HashMap (G × Array G) IOKeyInfo -- channel-keyed info map

Each of the four ops takes a leading channel : G:

io_get_info(channel, key)
io_set_info(channel, key, idx, len); cont
io_read(channel, idx, len)
io_write(channel, data); cont

Idx in IOKeyInfo is an offset into the channel's arena, not a
global one — two channels can both io_set_info(ch, key, idx=5, len=3)
without aliasing each other's bytes.

The channel threads through every IR stage
(Source/Typed/Simple/Concrete/Bytecode), every compiler pass
(Check/Match/Simple/Concretize/Lower/Layout), every evaluator
(BytecodeEval/SourceEval/Interpret), the parser (Meta.lean), and the
Rust executor + FFI wire format.

IxVM cleanup

Existing IxVM code is migrated off the suffix-byte hack onto dedicated
channels:

channel	content
0	constants
1	blobs
2	reducibility hints

Keys are now always the bare 32-G blake3 hash — no addr ++ [0] /
addr ++ [1] suffixes anywhere.

read_byte_stream gains a leading channel argument so callers can
read from the arena they previously queried with io_get_info.

Also drops the dead len == 0 fallback in load_constant_hint:
io_get_info aborts on missing keys, so the harness must seed channel
2 for every defn — there is no absence-handling path to take, and the
previous match len { 0 => 1, _ => ... } was unreachable.

Tests

The existing read_write_io test (in both Tests/Aiur/Aiur.lean and
Tests/Aiur/Cross.lean) is enhanced to exercise channel
disambiguation directly: reads identical key [0] from two channels
backed by distinct arenas, then writes the concatenation to a third
channel.

Test plan

• lake build
• lake test -- aiur-cross
• lake test -- aiur
• lake test -- --ignored ixvm
• cargo clippy --all-targets

Commits

1. Add channel arg to IOBuffer ops for key disambiguation —
   pipeline-wide plumbing for the new channel dimension. Existing
   IxVM Aiur sources are migrated to pass channel 0 so nothing
   changes semantically yet.
2. Use channels to separate consts/blobs/hints in IxVM — drops
   the suffix-byte hack in favour of channels 0/1/2; tightens
   load_constant_hint to remove the dead absence-handling branch.