[moodlezoup]

Stacked on #2132 (Tier 1). Implements Tier 2 of #2013, full Zicclsm, behind a zicclsm Cargo feature: with it, misaligned loads and stores prove at every offset, including those that cross a doubleword boundary. Without it, a build proves exactly what Tier 1 does.

The zicclsm feature

Tier 2 costs every program bytecode (see Measurements), while only guests that make misaligned accesses gain from it, so they opt in.

• Without zicclsm (default).
  • Loads and stores expand once, as in Tier 1, and a misaligned access aborts the trace.
  • WindowMaskD/FunnelHigh and their virtual instructions do not exist: 55 tables and 462 bytecode lanes (472 with field-inline).
• With zicclsm. Tier 2 as described below: 57 tables, 464 lanes (474 with field-inline).

Plumbing follows field-inline:

• Declared by every crate that expands the instruction-kind lists or matches on the gated kinds: jolt-riscv, jolt-lookup-tables, jolt-program, tracer, jolt-tracer-x86, jolt-witness and z3-verifier.
• Forwarded by jolt-claims, jolt-host, jolt-verifier, jolt-prover and jolt-sdk. A host opts in with jolt-sdk/zicclsm; guests need no change.
• Shared plumbing. Only the semantic pieces are gated. The dual-expansion plumbing (row flag, PcSlot run, SourceExpansion, tracer selection, x86 dispatch) is shared, and without the feature it never sees a misaligned sequence.

It is a separate protocol profile:

• Digest domains. zicclsm selects its own program-preprocessing digest domains (…/zicclsm/v3, …/zicclsm/v2).
• Committed lane count. CommittedProgramPreprocessing records bytecode_lanes, and the verifier rejects a committed artifact whose lane count differs from its own build's. Both layouts pad to 512 lanes, so without the check an artifact committed by the other build would be accepted and its lanes misread.

Design (with zicclsm)

A top-level LH/LHU/LW/LWU/LD/SH/SW/SD expands twice, and the committed bytecode holds both sequences at the instruction's address:

• Aligned sequence. These are Tier 1's rows unchanged: the native LD/SD row, 3-row loads and 6-row stores. Constraint 0 and RAM RAF evaluation still pin it to naturally aligned addresses. An aligned program runs exactly the rows it ran under Tier 1.
• Misaligned sequence. It reads the doublewords holding the first and the last accessed byte with byte-class floor rows. It is correct at every offset, so no table pins it.

The prover picks the entry PC. The honest tracer runs the misaligned sequence exactly when ea mod width ≠ 0, the rule DualAccess::is_misaligned owns; the x86 dispatch stub mirrors it. R1CS is unchanged. The only protocol change is two lookup tables, both built from existing prefix and suffix families:

Table	Value
WindowMaskD	2^64 − 2^(8·(ea mod 8))
FunnelHigh(x, M)	left-shift half of VirtualROTR: (x mod 2^s) << (64 − s) on M = !0 << s, 0 at s = 0

Rows per sequence:

	Aligned	Misaligned
LH/LHU	3	8
LW/LWU	3	7
LD	1	6
SH/SW	6	16
SD	1	12

A misaligned load adds Pext(lo, m) and FunnelHigh(hi, m). The halves are disjoint, so the ADD is carry-free. A misaligned store scales by 2^(8·(ea mod 8)) = −m with MUL/MULHU and writes the second doubleword first.

Where this departs from the #2013 sketch

Each departure removes a table family or a memory-layout change. The spec records all four under "Tier 2 as implemented".

1. The split is aligned/misaligned, not non-crossing/crossing. No non-crossing tables are needed: a misaligned access that stays within one doubleword also takes the misaligned sequence.
2. The misaligned sequence is universal and unpinned. So the reverse wrong-variant case, the misaligned sequence on an aligned access, is correct by construction rather than rejected.
3. No guard doubleword. The second doubleword is addressed at ea + width − 1, so the sequence only touches doublewords that hold accessed bytes. That is a single doubleword when the access does not cross.
4. Mask-based tables instead of rank-8/9 funnel and shifted-store tables.

Plumbing

• Rows and PCs. JoltInstructionRow::misaligned_variant is prover metadata, not a bytecode lane. It is stamped by stamp_sequence_metadata and stored in JoltTraceRow control bit 7. PcSlot gains misaligned_sequence_length and is still 8 bytes. PCs resolve by (address, vsr, misaligned_variant).
• Expansion API. expand_instruction returns SourceExpansion::{Single, Dual(DualExpansion)}. Only top-level instructions are dual. The LW/SW inside LR.W/SC.W and the LD/SD rows of the .D atomics keep their aligned rows, so a misaligned atomic stays unprovable and still aborts the trace.
• Tracer.
  • Each PC caches an InlineExpansion, and the sequence is chosen before any row runs.
  • Aligned LD/SD keep the native-row fast path.
  • Sequence rows run through a non-dispatching trace_row, so an LD/SD row of an atomic never takes a misaligned sequence.
  • force_aligned_sequences replaces allow_misaligned_floor_accesses.
• x86 AOT backend. Each dual group head gets a dispatch stub on ea & (width − 1). The misaligned rows are emitted out of line and jump back to the next instruction. The jump table, pause checks and observations are unchanged.
• Lean export. It renders only the aligned sequence, since that model raises the alignment fault.

Breaking changes

• The program-preprocessing digest domains move to dory-whole-bytecode/v3 and akita-whole-bytecode/v2, because the row and PcSlot layouts changed, and zicclsm builds use …/zicclsm/v3 and …/zicclsm/v2. CommittedProgramPreprocessing gains bytecode_lanes. All golden digests are updated.
• The verifier fuzz bundles are regenerated from the default build, and FIXTURE_MAGIC is now JVCF0010. zicclsm builds cache their verifier fixtures separately.
• With zicclsm, every program's bytecode gains the misaligned sequences (see Measurements).

Testing

All run locally on this branch, with and without zicclsm unless noted.

• z3. With zicclsm, each sequence of every dual load and store is proved at all eight doubleword offsets against a byte-level RISC-V model, and the aligned sequence's own address assumptions are shown to admit only the naturally aligned offsets. Planted recipe bugs are all caught. Without the feature, loads and stores are checked against the contained-lane semantics, as in Tier 1. The nightly builds with zicclsm, whose expansions contain every row a default build runs.

• Expansion. Without zicclsm, every load and store expands once. The golden fixture pins each case's single or aligned sequence in output_sha256 (identical in both builds) and, for the 84 dual cases, the misaligned sequence in misaligned_sha256 (checked with zicclsm).

• Tracer. A byte-model test covers all eight offsets × 11 kinds × {positive, negative immediate} × {plain, compressed, rd = x0}. With zicclsm it checks registers, memory, the sequence chosen and the RAM records. Without it, a misaligned access must abort. Misaligned atomics abort in both builds.

• x86.

  • A per-source difftest runs each kind's real bytecode against the interpreter: at every offset with zicclsm, at every aligned offset without it.
  • memory_ops passes the record-mode and fast-run equivalence tests in both builds.
  • misaligned_memory_ops also passes dense chunking with zicclsm, and a misaligned access past the memory plane faults on its second row.

• End to end. Without zicclsm, memory-ops' memory_ops proves every aligned offset of every width. With it, misaligned_memory_ops proves every in-bounds offset of every width, by immediate and from one PC per kind with a walking base. Both run in clear, ZK and Akita modes. The field-inline matrix passes in both builds.

• Soundness. misaligned_memory.rs forces the aligned sequence on misaligned LH/LHU/LW/LWU/SH/SW/LD/SD. In both builds each witness satisfies every R1CS row and is rejected by RAF evaluation. Tamper tests reject a committed artifact with a foreign bytecode_lanes (Dory clear and ZK, Akita).

• Suites.

  Suite	Default	zicclsm
  jolt-program	55	56
  jolt-riscv, jolt-lookup-tables	475	487
  tracer / jolt-witness	171 / 32	171 / 32
  jolt-tracer-x86	122	128
  jolt-prover, clear / ZK / Akita	37 / 30 / 39	38 / 31 / 40
  jolt-verifier fixtures, clear / ZK	142 / 119	142 / 119
  z3 load/store proofs	24	24

  Also passing:

  • the field-inline matrix (clear and Akita without zicclsm; clear, ZK and Akita with it);
  • the jolt-verifier Akita (84) and field-inline (136) fixture suites;
  • the digest goldens in all eight akita × field-inline × zicclsm combinations, and the Fiat-Shamir inventory;
  • the verifier fuzz replay over the regenerated bundles;
  • jolt-eval's expansion-parity invariant;
  • the CI clippy matrix (all 33 runs, -D warnings), fmt, taplo, the style-invariants check and the fuzz lockfile check.

• CI. New lanes cover:

  • zicclsm clippy;
  • crate, tracer and x86 tests;
  • a prover job running the full package in clear, ZK and Akita, plus the field-inline matrix;
  • a verifier-fixture job.

Measurements

Scale-20 profile inputs, Tier 1 → this PR with zicclsm. Prover times are means of three interleaved runs of the optimized backend. Builds without zicclsm expand exactly as Tier 1 does.

Workload	Trace rows	Bytecode rows	Padded bytecode	Prover time
btreemap	489,836 (=)	5,576 → 16,209	8192 → 16384	4.85 s → 4.98 s
sha2-chain	572,466 (=)	4,700 → 9,125	8192 → 16384	6.84 s → 6.88 s
sha3-chain	718,801 (=)	5,891 → 10,168	8192 → 16384	7.21 s → 7.29 s
fibonacci	787,317 (=)	2,722 → 6,657	4096 → 8192	7.04 s → 7.26 s

• Bytecode size. Aligned programs prove the same traces. The cost is bytecode size: 1.7–2.9× the rows, and one more padded power of two.
  • That adds a bytecode address round. The muldiv ZK fixture's BlindFold shape gains one coefficient row and one auxiliary row under zicclsm.
  • It also roughly doubles the full-mode verifier's O(K) fold and committed-mode program preprocessing.
• Prover time. It rises 0.6–3.2%, within run-to-run noise but consistently upward.

Notes

• ram_K sizing, existing and not fixed here. jolt-prover/src/config.rs sizes ram_K from the highest touched index with no +1. An access to the very top of memory can therefore fall outside the domain, whether or not it is misaligned. It surfaces as the jolt-witness "beyond ram_k" error.
• Arch tests not enabled. The ACT4 misaligned-ldst-01 test is not enabled (tests/arch-tests/jolt/sail.json still declares misaligned accesses unsupported). It would need a zicclsm build of the arch-test harness, so I left it for a follow-up.
• First instruction. With zicclsm, the entry PC is the aligned head. A program whose very first instruction is a misaligned dual access cannot prove that first execution. This affects liveness only.

🤖 Generated with Claude Code

[github-actions]

📏 PR diff

Note

Actual code changed: 1,571 lines

🟢 +1,386 added    🔴 −185 removed

Tests, docs, fixtures, and helper scripts excluded.

Category	🟢 Added	🔴 Removed
⌨️ Actual code	+1,386	−185
🧪 Tests	+1,304	−238
📚 Docs	+355	−50
📦 Fixtures	+101	−101
🔧 Helper scripts	+160	−11
Total diff	+3,306	−585

_{Every changed line is classified once.}