Md spec#239
Draft
MauroToscano wants to merge 128 commits into
Draft
Conversation
See the original yetanotherco/lambda_vm_spec #1 for more details, if it still exists. * Introduce `config` and "variables" * chip column-to-table rendering * restructuring * some basic interactions idea * Sample lt chip design * Update formatting * Interpret variable indexing * BRANCH draft * Fix indexing + render template * Render labels for references to constraints * Rendering chip assumptions * Add an editorconfig for consistency in indentation and trailing newlines * The constraint range index found its way back home * Finish (?) LT chip * Improve lisp rendering * support constraint group rendering * Support "^" type setting * dvrm * add dvrm assumptions * Rendering virtual column definitions and polynomials for arith constraints * ignore ebook.pdf * Split LT and BRANCH into groups * Nicer mutual recursion in expression formatting * Use negation instead of mult by -1 in lt * Format expr.typ * Simplify subtraction expression * Remove parentheses using precedence rules * fmt * improve dvrm readability * fix lt parentheses * move `extended_n_sub_r` def from constraint to var * Set div chip word types to HL * divrem fixes * more dvrm tweaks * Specify grammar * add docs * Drop chip files * Improve `chip` readability * minor fixes --------- Co-authored-by: Erik Takke <[email protected]>
This fixes the following pain points: - Assumptions and constraints requiring a `ref` for rendering to succeed - The `desc` field of `arith` constraints not being rendered - The `constraint` field of an `arith` constraint using eval in code mode - Long tables (columns and constraints) didn't break across pages - Template constraints did not have conditions rendered - Constraint groups didn't get the proper prefix if specified - The default branch of expression rendering has missing arguments It also introduces a nice visual todo macro --------- Co-authored-by: Erik <[email protected]>
Support array-like variable types. Typed as: ```toml [[variables.auxiliary]] name = "var" type = ["Bit", 5] desc = "five bits" ``` --------- Co-authored-by: Robin Jadoul <[email protected]>
Updated definition rendering: * definitions are only allowed for virtual variables * definitions are now labelled with `def` rather than `poly` or `polys` * more flexible definitions possible for array-type virtuals.
* spec: update `description` printing * spec: update `polynomial constraint` printing
* spec: Initial CPU version to handle RV64IMC * Address review comments * Add word_instr as input to SHIFT --------- Co-authored-by: Erik <[email protected]>
* spec: init BRANCH chip * Small cleanup * Clean up variable naming and generally address review comments * outdated comment --------- Co-authored-by: Erik Takke <[email protected]>
* spec: conditionally render constraint table headers * spec: simplify `selected_constraints` expression * spec: repurpose `selected_constraints`
…s in one document (#108)
Co-authored-by: Erik Takke <[email protected]>
* spec: rough draft SHIFT chip * various minor fixes * implement right-limb shifting * Update rendering "polynomial constriant" in table * fix degree 4 issues * Further update to SHIFT chip * Clean up SHIFT * spec/shift: add assumption * spec/shift: Add lookup constraint * spec/shift: make extension virtual Kudos to Robin for uncovering this! * spec/shift: Simplify limb-situation Kudos to Robin for pointing this out! * spec/SHIFT: fix typo * Turn `limb_shift_x` into array * spec: support "sum" expression in math * Simplify limb-shifting constraint * spec: attempt at refactoring `shift` * spec: overhaul SHIFT * spec: SHIFT: rename `extensions` as `extension` Co-authored-by: Robin Jadoul <[email protected]> * spec: SHIFT: make `shift` of type Byte * spec: SHIFT: replace variable '0x' with constant 0x * spec: SHIFT: remove "cheaper" remark * spec: SHIFT: fix `shifted` description * spec: SHIFT: make output a DWordWL * spec: SHIFT * spec: SHIFT: introduce explanation; update some constraint elaborations * Apply suggestions from the code review Co-authored-by: Robin Jadoul <[email protected]> * spec: SHIFT: update `bits_shift` desc * spec: SHIFT: update `limb_shift` desc * spec: SHIFT: add missing IS_BIT constraint for limb_shift * spec: SHIFT: update description * spec: SHIFT: fix sum's expr-to-math * Minor language pass Co-authored-by: Robin Jadoul <[email protected]> --------- Co-authored-by: Robin Jadoul <[email protected]>
* spec: ADD draft * spec: ADD: fix `carry` size * spec: ADD: clarify sum is mod 2^64 * spec: introduce `SUB` template notation. * Fix assumption indices Co-authored-by: Robin Jadoul <[email protected]> * Fix typos Co-authored-by: Robin Jadoul <[email protected]> --------- Co-authored-by: Robin Jadoul <[email protected]>
* spec: support "sum" expression * spec: introduce "QuadHL" type * spec: introduce MUL chip * spec: Introduce QuadWL * spec: introduce B20[4] * spec: simplify MUL to 26 columns * spec: Fix expr-sum bug * spec: simplify MUL to 22 columns * spec: improve MUL readability * spec: MUL: fix indexing * spec: MUL: refactor * spec: drop B20 * spec: MUL: fix raw_product relation * spec: MUL: fix IS_B19 check range Co-authored-by: Robin Jadoul <[email protected]> * spec: MUL: add missing res range check assumption * spec: MUL: remove superfluous/invalid constraints * spec: MUL: leverage SIGN template * spec: MUL: fix index mistake * spec: MUL: update description * spec: permit non-constant exponents * spec: MUL: drop `limb_product` * spec: MUL: minor tweaks * spec: MUL: bump headers * spec: MUL: update description * spec: MUL: update to IS_B20 * spec: MUL: remove 'eloquent' * Apply suggestions from code review Thanks Robin! Co-authored-by: Robin Jadoul <[email protected]> * spec: MUL: define padding --------- Co-authored-by: Robin Jadoul <[email protected]>
Co-authored-by: Erik <[email protected]>
Co-authored-by: Erik <[email protected]>
--------- Co-authored-by: Robin Jadoul <[email protected]>
* spec: First sha256 accelerator draft * Types checked * Update typst description * HWSLC -> HWSL * Apply suggestions from code review Co-authored-by: Erik <[email protected]> Co-authored-by: Robin Jadoul <[email protected]> * preliminary changes after review * fix out_e carry check * rotxor with 2 fewer columns * Correct count of bytes for out range checks * Explicit tables for SHA256_K * whoops * cosmetic + explanation * Apply suggestions from code review Co-authored-by: Erik <[email protected]> * Update spec/sha256.typ * Replace base_addr by entry in addr * review comments * structure * Apply suggestions from code review Co-authored-by: Erik <[email protected]> * Update spec/sha256.typ Co-authored-by: Erik <[email protected]> * spec/sha256: rebase fixes --------- Co-authored-by: Erik <[email protected]> Co-authored-by: Erik Takke <[email protected]>
* spec: math/code render mod expr * spec/type_check: add ModExpr * spec: add multi-dimensional array support * spec/KECCAK: introduce v0 * spec/keccak: define padding * spec: support multidimensional array in signatures * spec/keccak: add signatures * spec/keccak: update core chip * spec/keccak: update keccak_rnd description * spec/keccak: define round constant lookup * Apply suggestions from code review Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com> * spec/keccak: clarify "optimizations" header * spec/keccak: list `state_ptr` simplification optimization * spec/keccak: fix C3 * spec/keccak: fix missing EOF * spec/keccak: list interaction counts * spec/keccak: list three-way XOR optimization idea * spec/tooling: fix mod_expr default * spec: add spaces round `%` rendering * spec: reuse `type_to_code` in `signatures.typ` * Apply suggestions from code review Co-authored-by: Robin Jadoul <[email protected]> * spec/keccak: update three-way XOR optimization benefits * spec/ecall: reintroduce ecall-number overview * spec/keccak: ref to sections in FIPS202 on state endianness * spec/keccak: fix typo --------- Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com> Co-authored-by: Robin Jadoul <[email protected]>
* spec: Inline PC memory access into CPU * Apply suggestions from code review Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com> Co-authored-by: Robin Jadoul <[email protected]> * Apply review suggestion Co-authored-by: Erik <[email protected]> * Remove `pc_double_read` constraints and clarify why in cpu.typ * Potential optimization -> subsubsection * Address review comments * Clarifying remark on register initialization --------- Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com> Co-authored-by: Erik <[email protected]>
* Fix shiroa build - Strip raw blocks from chapter titles for `project` argument - Add an explicit description (based on chapter title) to chapters to avoid compilation issues when context appears early in the chapter - Export interaction counts from the pdf version to use in shiroa, since otherwise we run into convergence issues that are hard to debug * cd into script directory and harden against stale interaction counts * Update spec/book.typ Co-authored-by: Erik <[email protected]> * Fall back to single-threaded shiroa when insufficient memory --------- Co-authored-by: Erik <[email protected]>
* spec: Enable heading numbering for section references in shiroa * Remove explicit heading numbering from logup chapter
* spec/ARE_BYTES: introduce ARE_BYTES signature * spec/ARE_BYTES: introduce ARE_BYTES lookup * spec/ARE_BYTES: introduce IS_BYTE template * spec/ARE_BYTES: switch IS_BYTE lookup to IS_BYTE template * spec/ARE_BYTES: drop IS_BYTE interaction * spec/ARE_BYTES: drop IS_BYTE lookup signature * spec/ARE_BYTES: turn multiplicity into cond * spec/ARE_BYTES: remove as potential optimization * spec/ARE_BYTES: update assumptions using IS_BYTE
* spec/keccak: fix cyclic-shift indexing mistakes * spec/ecall: fix negative ECALL numbering * spec/keccak: optimize Cxz_right from Byte to Bit * spec/KECCAK: add potential optimization rot_left and rot_right contain 96 constant zero-columns, which can be dropped. Additionally, those zeroes do not have to be byte-checked. * spec/KECCAK: fix typo * spec/KECCAK: list another potential optimization * spec/keccak: fix index division problems * spec/keccak: remove condition from IS_BIT
* spec: Draft CPU rework, still missing updates for all ALU chips, DECODE and CPU32 * Decoding for the new CPU * Bitwise using BYTE_ALU * Update old chips for the new CPU * Fix decode for MEMORY signed flag * Add input range check to SHIFTs typ * MEMORY signature HL -> WL * Clarify SHIFTW decoding * Further updates and new chips for the new CPU * Fix arg2 muxes * Link instruction length to CPU32 * Apply easy changes from code review Co-authored-by: Erik <[email protected]> * Address more review comments * Fix CPU32 register interactions * Fix CPUs PC write multiplicity * Fix HALT's interaction with the CPU padding * Add some optional extra arith constraints to enforce the "easy" assumptions * Combine assumptions constraints * Remove todo comments that got a tracking issue * word_instr gate for read_registerX out of caution * Fix JAL(R) decoding and ALU * Placate the type checker * Represent instruction length as half * Update spec/src/cpu.toml Co-authored-by: Erik <[email protected]> * fixes --------- Co-authored-by: Erik <[email protected]>
…ng rows (#646) * Add extra constraints to prevent register side effects in CPU32 padding rows * fixes * Patch 'signed' soundness hole and small cleanups * More explicit constraint
- Sync CHAPTERS with book.typ: add is_byte, cpu32, eq, bytewise, store, keccak - Support new expr ops: arr, opsel, mod (spec/expr.typ grammar) - Padding tables now read per-variable 'pad' attrs (mirrors chip.typ) - Drop stale ecall.md (ecall.typ is not a book chapter on spec/main)
…ng rows (#646) * Add extra constraints to prevent register side effects in CPU32 padding rows * fixes * Patch 'signed' soundness hole and small cleanups * More explicit constraint
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.