Sharding: per-shard check / prove / verify on the IxVM kernel

[arthurpaulino]

Wire the .ixes manifest into the proving path: a sharded environment can now be checked, proven, and verified as independent per-shard CheckEnv claims that compose off-circuit into a whole-environment "well-typed" verdict. No kernel changes -- a shard is the existing Claim.CheckEnv(env_root, asm): run_check_env ingresses the shard's reference closure and check_all_skipping checks exactly the owned constants, trusting (skipping) the frontier.

CLI: check, prove, and verify all gain the same shape -- --ixe <env> --ixes <manifest> [--shard K]:

ix check  --ixe E --ixes M --shard K      check shard K (Aiur bytecode)
ix check  --ixe E --ixes M                check every shard concurrently after a
                                          coverage check (--jobs N caps RAM)
ix prove  --ixe E --ixes M --shard K      STARK-prove shard K
ix prove  --ixe E --ixes M                prove every shard (sequential)
ix verify --ixe E --ixes M                coverage verdict (disjoint cover)
ix verify --ixe E --ixes M --shard K [P]  shard K's claim digest, or bind+verify P
ix verify --ixe E --ixes M P0 P1 ...      composed verdict: every proof bound to a
                                          shard, every shard covered, + coverage
ix verify P0 P1 ...                       plain proof verification

Shard -> claim. A shard's owned set is every env constant whose check-schedule block is owned by that shard, where a projection collapses to its SCC/Muts wrapper and everything else is its own block (mirrors check_schedule_block_addr). The CheckEnv claim is reconstructed deterministically from (env, owned) -- canonical trees sort addresses -- so the digest a prove --shard K commits is reproducible, and verify binds a proof to its shard by digest equality.

Soundness is off-circuit: every constant's block must be owned by exactly one shard (disjoint cover) -- then each constant is checked once and every shard's frontier is owned (checked) by another shard. Full ingress pins types via the per-constant blake3, so no cross-shard type matching is needed; coverage alone suffices for check, coverage + per-shard proof verification for verify.

check parallelizes across shards (independent read-only bytecode runs, one dedicated task each); --jobs N caps the number in flight, since each shard re-ingests its closure into its own IO buffer. prove stays sequential (each STARK proof is RAM-heavy).

Other:

• .ixes parser is a bounds-checked StateT cursor: a truncated/malformed manifest yields a clean error, never an index-out-of-bounds panic.
• ClaimHarness: shardCheckEnvClaim (claim + closure + assumption trees, no IO buffer -- cheap reconstruction for binding) and buildShardCheckEnvWitness (the witness, IO buffer restricted to the shard closure).
• lake exe arena-exclude --out <file> writes the exclude list to a file instead of stdout, so callers don't need a shell redirect.

Validated end-to-end on a small kernel-arena env (profile -> shard 4 -> prove all -> composed verify), including the negative cases (wrong-shard binding and coverage gaps rejected).