docs: add akita lattice specs#1606
Conversation
moodlezoup
force-pushed
the
prover-stack/10-jolt-prover
branch
from
068b024 to
240e724
Compare
- impl_inline_instruction: accept cfg attrs from for_each_instruction_kind - jolt-riscv: restore trace_row module/exports, from_bits, thiserror dep (accidentally dropped while rebasing onto JoltTraceRow foundation) - jolt-riscv: drop dead test-utils feature and unused rand dep (machete) - jolt-sdk/macros: restore committed-bytecode preprocessing from main, re-apply field-inline hook additively - tracer/cpu: restore interrupt_enabled match from main - guests: declare field-inline feature (silences unexpected_cfgs) - jolt-lookup-tables prefixes: lint-clean ported prefix_mle code (unwrap_or defaults, let-else, redundant else, unreachable!) - taplo fmt
Remove prefix_mle and update_prefix_checkpoint from SparseDensePrefix,
the Prefixes dispatch, and all 40 prefix implementations, along with the
Option-based PrefixCheckpoint alias. Prefixes are now computed solely via
per-phase materialization: evaluate() at binary points builds a dense
table at phase start, the table is bound during the phase's sumcheck
rounds, and the fully bound value becomes the next phase's checkpoint.
Rewrite prefix_suffix_test to exercise that flow end-to-end: materialize,
bind HighToLow with random challenges, check combine(prefixes, suffixes)
against the table MLE every round at c in {0,2}, chain checkpoints from
bound values, and compare the final claim against evaluate_mle over the
full 128-variable point, for both RPP=16 and RPP=8 prover configs.
- Decode FIELD_ASSERT_EQ with rd:None to match the tracer shape and avoid the rd=x0 virtual-register rewrite (bytecode/trace operand divergence). - Add FIELD_STORE_TO_X to field_inline_handles_rd_zero so store-to-x0 stays a legal no-op instead of producing an out-of-range x-register. - Reject out-of-range field-register indices in the emulator (was silently clamping, hiding fr16-31 misuse until proving). - Deduplicate the operand-shape match: expose field_inline_operand_shape_for_op in jolt-riscv; jolt-program and the tracer x_register_role delegate to it. - Replace the duplicated &TraceRow JoltCycle impl with a blanket impl for &T. - Delete the orphaned tracer inline_helpers.rs (undeclared, dead InstrAssembler). - Drop the unused centralized LookupTables::required_prefixes table. - Document the inv(0) and store-to-x truncation trace contracts. - Enforce the FieldRegister bound on deserialize via a real Valid::check and re-run FieldInlineBytecodeMetadata::validate() on the deserialize path. - Fix OwnedTrace::next_row so the field-inline feature actually compiles (TraceRow is not Copy under field-inline).
The field-inline feature is not part of host/zk/default, so no existing CI job compiled or tested it — the feature could regress while CI stayed green. Add an explicit clippy invocation and a nextest run over the crates that define it (tracer, jolt-program, jolt-riscv, jolt-lookup-tables).
0xAndoroid
force-pushed
the
prover-stack/10-jolt-prover
branch
from
2fa6989 to
eaa8020
Compare
0xAndoroid
force-pushed
the
prover-stack/11-akita-specs
branch
from
f28e02b to
ea30d97
Compare
|
Stack maintenance — rebased onto #1605 ( 📚 Stack A: #1596 → #1597 → #1598 → #1599 → #1600 → #1601 → #1602 → #1603 #1596 and #1597 are shared by both stacks; each PR targets the one before it. Conflict resolution
Local validation
|
|
Claude code review session started: https://claude.ai/code/session_01MvcVGF1XTpcLKwLNQFxwAE |
moodlezoup
left a comment
moodlezoup
left a comment
There was a problem hiding this comment.
Docs-only PR adding the AKITA lattice PCS spec stack (specs/akita/00–07). Read all eight specs end to end. The design is internally consistent — the cell-count/dimension math agrees across 00, 03, and 05 (23 byte facts → 5888 cells/row → n+13; fused increments 7938 → n+13; split 9988 → n+14), the masked-view soundness distinction (RamInc(r) != StoreFlag(r)·SignedInc(r), requiring a row-summed translation relation) is correctly identified and carried through 04/05, and the Store·RdPresent = 0 disjointness for AMO/RMW is explicitly flagged for audit rather than assumed. No soundness or correctness blockers at the spec level. Two small clarifications inline (identifier naming, claim-field injectivity); the rest is appropriately deferred to the Questions sections.
Generated by Claude Code
|
|
||
| ```text | ||
| 1. collect enabled fact families from verifier config. | ||
| 2. sort by stable PackedFamilyId. |
There was a problem hiding this comment.
Two names are used for the family identifier: PackedFamilyId here (and in the jolt-claims implementation plan at line 284) versus FactId in the FactFamily struct (line 313), the planner (sort families by FactId, line 346), and the streaming source (line 402). 04 and the invariants then refer to "fact family ordering." Pick one name so the sort key and the struct field are unambiguous for whoever implements the layout — the ordering invariant is load-bearing (it drives offsets and the digest), so the identity of the key shouldn't be guessable.
Generated by Claude Code
| to_akita_claim(F_jolt) -> F_akita | ||
|
|
||
| Required: | ||
| injective over all values that appear in claims. |
There was a problem hiding this comment.
The "injective over all values that appear in claims" contract is only meaningful once the claim field is pinned down. Sumcheck opening claims range over the full Jolt scalar field (BN254 Fr, ~254 bits), so injectivity forces |F_akita| >= |Fr|. That's automatic in base-field mode (identity), but it rules out any "claim field" smaller than Fr — which is the usual reason a lattice PCS wants a small base ring. Worth stating explicitly as an invariant here (claim field must embed all of Fr) so the extension-field mode in 02-Q1 doesn't accidentally pick a lossy conversion. Otherwise it reduces to the "implicit modular reduction" case this section already rejects.
Generated by Claude Code
Introduce the jolt-witness crate: the witness-generation layer producing committed and virtual polynomials for the Jolt VM, dory-assist, wrapper, and blindfold protocols. Consolidates follow-up refactors: - Split the jolt_vm witness module by stage and polynomial family (spartan_outer, stage2/3/6, registers, ra, ram, trace, streams, provider). - Share require_unique_ids / power_of_two_log_rows helpers across the wrapper and dory_assist providers via protocols/util.rs. - Tighten the core witness data-access API: log_rows-only WitnessDimensions, ViewRequirement-based oracle_view, and removal of dead encodings, policies, and builder indirection. - Document the core witness vocabulary types. - Restore the 1604 workspace build.
Mechanical adaptation to the prover-stack/09-jolt-witness API tightening: - WitnessDimensions::new takes only log_rows; .dimensions.rows is now the derived rows() method. - OracleViewRequest was folded into ViewRequirement: oracle_view / try_evaluate_oracle_view take the requirement directly. - try_collect_ra_family_cycle_indices moved to the RaFamilyCycleIndexSource capability trait: bound added on collect_ra_cycle_indices, the materialize_sumcheck_ra_pushforward / stage7_hamming_state trait methods and their cpu impls, plus an empty impl for the RaPushforwardTestWitness mock. - WitnessBuilder was removed: the e2e harnesses construct TraceBackedJoltVmWitness::new(config, inputs) directly. Verified: jolt-backends + jolt-witness compile clean and pass 114/114 tests. jolt-prover's adaptation is compile-blocked by pre-existing tracer and jolt-blindfold breakage on this branch (unrelated to these changes). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
crates/jolt-riscv/src/trace_row.rs existed in the tree but was never declared in lib.rs, leaving tracer's trace_row consumer with unresolvable imports. Declare and re-export the module, add the from_bits flag-set constructors it needs, and add the missing thiserror dependencies to jolt-riscv and tracer (ported from prover-stack/01-field-inline-tracing, identical to main). Update jolt-sdk's provable macro to the current preprocessing API (also from prover-stack/01). Adapt jolt-blindfold's protocol.rs, which called build_with_sources as a method while this crate defines the identical function as a free function in r1cs.rs. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Finishes the adaptation to the jolt-witness RA fast-path capability trait: the bound is threaded through stage 7's hamming-state preparation and the prover/api entry-point witness bound chains. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
These paths compile (and therefore lint) for the first time now that the stack builds end to end: discard the unit results of rayon::join in the cpu RA table scaling, collapse nine interrupt-mask match arms into pattern guards in the emulator, and drop a clone of the now-Copy ViewRequirement in stage 6 batching. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
0xAndoroid
force-pushed
the
prover-stack/10-jolt-prover
branch
from
3b9558f to
41d0bfb
Compare
0xAndoroid
force-pushed
the
prover-stack/11-akita-specs
branch
from
ea30d97 to
c77d7d5
Compare
moodlezoup
force-pushed
the
prover-stack/10-jolt-prover
branch
3 times, most recently
from
27d7e7f to
ca8b46e
Compare
3 participants
Part of the draft Jolt prover stack.
Base:
prover-stack/10-jolt-proverHead:
prover-stack/11-akita-specsAdds the AKITA lattice specification stack under
specs/akita/.Validation before submission:
cargo fmt -q -- --checkcargo metadata --no-deps --format-version 1gh stack pushsimulation against a temporary bare remotehandoffs/, oldSTACK.md,stack/, and old stack workflow