fix: clippy in vk_codec, document Zisk sharding, scope CI execute

- vk_codec: drop the always-Ok `Result` wrapper from `to_bytes`
  (clippy `unnecessary_wraps`); callers updated.
- README: document the Zisk shard-proving path — profile → shard →
  prove via `--shard-plan`, and the resumable proof store
  (`--store-dir`/`--no-reuse`/`--require-closed`).
- ci: scope the riscv-zkvm-execute job to `--only-const myReflEq` so
  it certifies one constant (Init deps become Claim assumptions)
  instead of typechecking all of Init, which never finished.

Author: samuelburnham

.github/workflows/ci.yml

@@ -119,20 +119,20 @@ jobs:
           echo "$HOME/.zisk/bin" >> "$GITHUB_PATH"
       # `download-artifact` drops minimal.ixe in the repo root; both hosts run
       # from their workspace dir, so the env is `../minimal.ixe`. Debug builds
-      # (no `--release`) keep host compile time down; the fixture is tiny so
-      # execution is fast regardless.
+      # (no `--release`) keep host compile time down. minimal.ixe carries the
+      # full Init closure (the three MinimalDefs constants plus everything the
+      # implicit prelude import pulls in), so we scope execution with
+      # `--only-const myReflEq`: that typechecks just the one constant and
+      # leaves its Init dependencies as Claim assumptions, instead of
+      # typechecking all of Init (which never finishes in the emulator).
       - name: SP1 — execute minimal.ixe (assert failures == 0)
         run: |
           cd sp1
-          cargo run --bin sp1-host -- --execute --ixe ../minimal.ixe | tee whole.txt
-          grep -qE "failures: 0\b" whole.txt
           cargo run --bin sp1-host -- --execute --ixe ../minimal.ixe --only-const myReflEq | tee only.txt
           grep -qE "failures: 0\b" only.txt
       - name: Zisk — execute minimal.ixe (assert failures == 0)
         run: |
           cd zisk
           ulimit -l unlimited 2>/dev/null || true
-          cargo run --bin zisk-host -- --execute --ixe ../minimal.ixe | tee whole.txt
-          grep -qE "failures: 0\b" whole.txt
           cargo run --bin zisk-host -- --execute --ixe ../minimal.ixe --only-const myReflEq | tee only.txt
           grep -qE "failures: 0\b" only.txt

README.md

@@ -401,9 +401,10 @@ Non-Nix users: install Zisk manually per the
    cached on disk (`CUDA_CACHE_MAXSIZE` above), so even a *fresh* process stays
    warm — the ~12 s figure above is a separate process from the cold run. So a
    single small one-off proof looks slow (it eats the cold-start); amortize by
-   batching, or just disregard it. Proving is stateful with no checkpointing —
-   if a run is killed it loses in-flight shard proofs and restarts from the
-   first shard.
+   batching, or just disregard it. By default proving is stateful with no
+   checkpointing — if a run is killed it loses in-flight shard proofs and
+   restarts from the first shard; use a proof store (`--store-dir`, see
+   *Sharding large environments* below) to make a sharded run resumable.
 
    ```
    RUST_LOG=info cargo run --release -- --gpu \
@@ -464,7 +465,9 @@ Non-Nix users: install Zisk manually per the
    or scope to a single constant with `--only-const <name>` (both backends),
    which resolves the name to its work item and ships only that constant's
    closure sub-env to the guest — so individual constants of a large env still
-   fit the cap.
+   fit the cap. To prove a large env in full under Zisk, shard it (see
+   *Sharding large environments* below): each shard ships only its own closure
+   sub-env, so the pieces fit the cap even when the whole env does not.
 
    **Host RAM cap (`--max-witness-stored`).** Distinct from the in-guest
    heap cap above, the prover side (Zisk's `proofman`) holds in-flight
@@ -494,6 +497,99 @@ Non-Nix users: install Zisk manually per the
    `CALCULATING_CONTRIBUTIONS`. Not relevant for `--execute` or
    `--verify-constraints` modes.
 
+3. **Sharding large environments.** A whole large env (e.g. all of
+   `Init`) does not fit a single Zisk proof: it overruns both the 512 MB
+   guest heap and, more bindingly, the prover's minimal-trace shared-memory
+   ceiling (64 GB per job on the assembly path). Sharding splits the env's
+   type-checking work into pieces that are proven independently — each
+   shipped with only its own dependency closure — and then folded into one
+   aggregate proof. This is a two-part workflow: produce a shard manifest
+   (a `.ixes` file), then prove it with `--shard-plan`.
+
+   **(a) Produce a shard manifest.** A manifest partitions the env's
+   per-constant work, balancing shards by real type-checking cost and
+   cutting where cross-shard dependencies are fewest. Two ways today:
+
+   - *Fixed shard count*, via the `ix` CLI. Profiling runs the kernel over
+     the env (slow) and writes a `.ixesp` cost map; sharding is instant
+     graph work on that map, so the shard count is cheap to re-tune without
+     re-profiling:
+
+     ```
+     # Profile once (slow): writes the .ixesp cost map.
+     lake exe ix profile init.ixe --out init.ixesp
+     # Cut into N shards (instant): writes the .ixes manifest. Re-run with a
+     # different N to re-tune — no re-profiling needed.
+     lake exe ix shard init.ixesp --shards 16 --out init.ixes
+     ```
+
+   - *Sized by a cycle or peak-RAM budget* (so you pick a resource limit
+     instead of a shard count). This currently lives in a kernel example
+     binary rather than the `ix` CLI; it profiles and shards in one step
+     (re-profiling on each run). With no flags it auto-sizes the shard count
+     from this machine's RAM (peak prover RAM ≈ `45 + 32 × cycles_billions`
+     GB, targeting ~78 % of total):
+
+     ```
+     # Auto-size N from this box's RAM; writes init.ixe.ixes.
+     cargo run -p ix-kernel --release --example shard_plan -- init.ixe
+     # Or force a per-shard guest-cycle budget / a RAM figure / a fixed count:
+     #   --max-cycles 4500000000   --ram-gb 256   --shards 16
+     ```
+
+   **(b) Prove the manifest.** Pass the `.ixes` to the host with
+   `--shard-plan` alongside the same `--ixe` it was built for. Each shard
+   becomes one leaf proof (built over only that shard's closure sub-env),
+   and the leaves fold up the manifest's bisection tree into a single root
+   proof:
+
+   ```
+   cd zisk
+   RUST_LOG=info cargo run --release -- --gpu \
+     --ixe ../init.ixe --shard-plan ../init.ixes
+   ```
+
+   **Resumable proving (`--store-dir`).** A proof store makes a sharded run
+   restartable and lets proofs be reused across runs and envs:
+
+   ```
+   RUST_LOG=info cargo run --release -- --gpu \
+     --ixe ../init.ixe --shard-plan ../init.ixes \
+     --store-dir ../init-store --require-closed
+   ```
+
+   - `--store-dir DIR`: each completed shard proof is banked to
+     `DIR/proofs/<n>.{proof,cover,asm}` as it finishes. **Re-run the same
+     command to resume** — shards already covered by the store are skipped
+     (not re-proven) and folded into the aggregate instead. Reuse is
+     trustless: a stored proof is re-verified in-circuit at aggregation,
+     never trusted by the host. Proofs are content-addressed, so a constant
+     proven in one env is reused in any other env that contains it.
+   - `--no-reuse`: ignore the store for this run (the "no sharing" baseline);
+     the existing store is neither read nor overwritten.
+   - `--require-closed`: error *before* proving unless every typing
+     dependency of every certified constant is either proven in this run or
+     already in the store — axioms are the only permitted residual. Turns
+     "result modulo axioms" from a printed hope into an enforced
+     precondition. Pairs with `--plan` for a no-prove check.
+
+   **Other shard modes and tuning flags.**
+
+   - *Static partitioning without a manifest:* `--shard-consts N` (N work
+     items per shard) or `--shard-bytes B` (pack contiguous items until
+     serialized bytes exceed `B`). Simpler, but not balanced by real
+     type-checking cost — `--shard-plan` is the performant path.
+   - `--plan`: print the planned partition and exit, no proving.
+   - `--execute`: run the shards in the VM only and print per-shard cycle
+     counts — use it to measure a shard's true cycle cost (e.g. to pick or
+     recalibrate a cycle budget) without proving.
+   - `--only-shard K`: prove just the 1-indexed shard `K` (skips
+     aggregation) for smoke-testing a single shard.
+   - `--dump-input FILE`: write one shard's guest stdin to `FILE` for
+     standalone profiling with `ziskemu` or `cargo-zisk`.
+   - `--agg-arity A` (default 16): how many child proofs each aggregation
+     step folds at once.
+
 ### Nix
 
 #### Prerequisites

crates/aiur/src/vk_codec.rs

@@ -192,9 +192,7 @@ impl W {
 
 /// Serialize the verifying key `System<AiurCircuit>` (preprocessed traces are
 /// skipped — see the module docs).
-pub(crate) fn to_bytes(
-  system: &System<AiurCircuit>,
-) -> Result<Vec<u8>, String> {
+pub(crate) fn to_bytes(system: &System<AiurCircuit>) -> Vec<u8> {
   let mut w = W { buf: Vec::new() };
   w.usize(system.commitment_parameters.log_blowup);
   w.usize(system.commitment_parameters.cap_height);
@@ -203,12 +201,12 @@ pub(crate) fn to_bytes(
   w.vec(&system.preprocessed_indices, |w, idx| {
     w.option(idx, |w, &i| w.usize(i))
   });
-  Ok(w.buf)
+  w.buf
 }
 
 /// Convenience: serialize the verifying key of a built [`AiurSystem`].
 pub fn aiur_system_to_bytes(sys: &AiurSystem) -> Result<Vec<u8>, String> {
-  to_bytes(&sys.system)
+  Ok(to_bytes(&sys.system))
 }
 
 // ════════════════════════════════════════════════════════════════════════════
@@ -395,9 +393,9 @@ mod tests {
         LookupAir::new(AiurCircuit::Bytes2, Bytes2.lookups()),
       ],
     );
-    let bytes = to_bytes(&system).expect("encode");
+    let bytes = to_bytes(&system);
     let back = from_bytes(&bytes).expect("decode");
-    let reencoded = to_bytes(&back).expect("re-encode");
+    let reencoded = to_bytes(&back);
     assert_eq!(bytes, reencoded, "verifying-key codec round-trip mismatch");
   }
 
@@ -406,7 +404,7 @@ mod tests {
     let cp = CommitmentParameters { log_blowup: 1, cap_height: 0 };
     let (system, _key) =
       System::new(cp, [LookupAir::new(AiurCircuit::Bytes1, Bytes1.lookups())]);
-    let mut bytes = to_bytes(&system).expect("encode");
+    let mut bytes = to_bytes(&system);
     bytes.push(0);
     assert!(from_bytes(&bytes).is_err(), "should reject trailing data");
   }