* spec: initial spec commit * spec: Basic chip data format and layout 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 <erik.takke@3milabs.tech> * spec: Fix some chip rendering pain points (#83) 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 <159244975+erik-3milabs@users.noreply.github.com> * spec: support array-like types (#85) Support array-like variable types. Typed as: ```toml [[variables.auxiliary]] name = "var" type = ["Bit", 5] desc = "five bits" ``` --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: Fixup wrong type sanity check for array types (#86) * Make precedence a lookup table instead of hardcoding it * Render type cast expressions * spec: Allow desc field on non-arith constraints as clarification * spec: Modify cast operator precedence * spec: improve definitions (#91) 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 table rendering (#93) * spec: update `description` printing * spec: update `polynomial constraint` printing * spec: introduce "condition" column type * spec: is_bit template * spec: CPU chip for RV64IMC (#88) * spec: Initial CPU version to handle RV64IMC * Address review comments * Add word_instr as input to SHIFT --------- Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: improve multi-poly definition rendering (#98) * spec: BRANCH chip (#92) * spec: init BRANCH chip * Small cleanup * Clean up variable naming and generally address review comments * outdated comment --------- Co-authored-by: Erik Takke <erik.takke@3milabs.tech> * spec: conditionally render constraint table headers (#94) * spec: conditionally render constraint table headers * spec: simplify `selected_constraints` expression * spec: repurpose `selected_constraints` * spec: do not print index in assumption/constraint ref (#96) * spec: Make constraint numbering restart when displaying multiple chips in one document (#108) * spec: Introduce LT chip (#90) Co-authored-by: Erik Takke <erik.takke@3milabs.tech> * spec: Fix constraint group lookup (#105) * spec: `SHIFT` chip (#84) * 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 <robin.jadoul@3milabs.tech> * 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 <robin.jadoul@3milabs.tech> * 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 <robin.jadoul@3milabs.tech> --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: `ADD` template (#97) * 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 <robin.jadoul@3milabs.tech> * Fix typos Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: have column table subheaders repeat on page wrap (#121) * spec: drop `dot` when multiplying constant with one-letter variable. (#120) * spec: `MUL` chip (#122) * 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 <robin.jadoul@3milabs.tech> * 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 <robin.jadoul@3milabs.tech> * spec: MUL: define padding --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: Add support for specifying padding values of columns (#133) Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: update range specifications to iters concept (#130) Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: `BITWISE` chip (#138) * spec: introduce BITWISE * spec: BITWISE: outline optimizations * spec: BITWISE: fix SLL naming mismatch * spec: BITWISE: fix length computation mistake * spec: drop `dot` in `expr_to_code` when multiplying constant with single-letter variable * spec: Initial inefficient MEMW chip (#104) Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: LOAD chip (#144) * fix CPU-CA41 typo (#189) * spec: `DECODE` (#143) * spec: DECODE: decode basics * spec: DECODE: update table + add *W instructions * spec: fix padding table for chips that don't have all types of variables * spec: introduce B49 * spec: DECODE: split-off decode uncompressed * spec: DECODE: overhaul decode * Apply suggestions from code review Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * Apply suggestion from @RobinJadoul Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * Fix `ADDI` flag mistakes * spec: DECODE: make `packed_encode` a `BaseField`; remove superfluous `B49` * spec: DECODE: set `mem_xB` when reading/writing _exactly_ `x` bytes * spec: DECODE: update `mp_selector` description. * Apply suggestions from code review * spec: DECODE: merge uncompressed page into decode.typ --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: placeholder chapters for chips to come (#190) * fix(spec): Use a better precedence value for "idx" (#197) * fix(spec): Missing `write_register` multiplicity. (#196) * spec: Initial version of memory argument (#164) Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * fix(spec): Correct typo in spec README and align style (#210) * spec: CPU padding (#195) * spec: CPU fast path for x0 reads * Do not write/read pc when in a padding row * specify padding for the CPU * Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: DECODE: update padding row * spec: DECODE: explain 'one more instruction' * spec: CPU: fix c_type_instruction typo * Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: align `packed_decode` in `DECODE` and `CPU` * spec: DECODE: add `read_registerX` to `packed_decode` * spec: DECODE: specify `read_register1` and `2` * spec: DECODE: update pc padding value * spec: DECODE: several small fixes * spec: DECODE: fix ECALL's rs2 value Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: DECODE: minor rewording Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: DECODE: minor fix --------- Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> Co-authored-by: Erik Takke <erik.takke@3milabs.tech> * spec: update `ECALL` signature (#244) * spec: update `ECALL` signature * spec: CPU/ECALL: cast rv1 to DWordWL * spec: Allow for cross referencing between different chapters, both in pdf and web mode (#225) * spec: Allow for cross referencing between different chapters, both in pdf and web mode * Improve PDF organization The PDF now no longer depends on shiroa trickery to compile, so errors are more clearly visible instead of being hidden behind layour iterations. Additionally, we can now have nice chapter headings and references to them. * Allow xref by specifying only the label * document strip-all * It does work, after all; with only ~7GB of RAM usage for the entire thing * small cleanup * Update spec/book.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * Address some review comments * less repetition for file names --------- Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: Update LT interaction signature so that it can be used properly for timestamps (#246) * spec: Update LT interaction signature so that it can be used properly for timestamps * fix(spec): add missing signed argument to LT from MEMW * Update spec/src/lt.toml Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * Update spec/src/lt.toml Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --------- Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: `HALT` chip (#235) * spec: HALT: first draft * spec: HALT: add link to sys call number * spec: HALT: update ECALL signature * spec: HALT: minor update * spec: HALT: document cleanup verification alternative * adapt to new chapter format * spec: HALT: fix MEMW register indexing * spec: HALT: move halt.typ into ecall.typ --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: minor `MUL` fixes (#223) * spec: MUL: fix missing iters * spec: MUL: fix res slice in lookup contribution * spec: MU: split `res` into `lo` and `hi` * spec: MUL: replace `range` by `iter` * spec: MUL: update `lo` and `hi` types + introduce `res` as virtual * spec: MUL: add note on future optimization * spec: `SIGN` (#279) * spec: introduce SIGN template * Update spec/src/sign.toml Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> --------- Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> * spec: drop `IsZero` template (#278) * spec: fix header levels (#264) * spec: offset headers in PDF * spec: decrement header levels for chip descriptions * spec: move heading offset to ebook.typ * spec: LOAD: fix LOAD-C9 signature (#284) * spec: `NEG` template (#270) * spec: tweak code-rendering "not" * spec: introduce NEG template * Update spec/book.typ Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> * spec: update NEG * spec: NEG: refactor * spec: NEG: fix range-assumption on x * spec: NEG: update cond * spec: tweak math-rendering "not" Analogous to 801f5ee * spec: NEG: add non-zero x case distinction --------- Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> * spec: Introduce DVRM chip spec: DVRM: introduce `μ_sum` spec: DVRM: apply SIGN template spec: DVRM: fix `n_sub_r_is_negative` spec: DVRM: range check `n_sub_r` spec: DVRM: add missing LT constraint spec: DVRM: add missing abs_* range checks required by SUB calls. spec: DVRM: fix LT lookup spec: support variable labelling spec: DVRM: completely refactor DVRM chip spec: DVRM: make multiplicities binary spec: DVRM: spec padding spec: DVRM: remove superfluous TODOs spec: DVRM: drop msb lookup for `sign_r` spec: DVRM: replace `range=` by `iter=` spec: DVRM: replace range assumptions for q and r by constraints Apply suggestions from code review Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> spec: DVRM: drop bit checks for multiplicities spec:DVRM: complete refactor spec: DVRM: update padding spec: DVRM: fix minor discrepancy spec: DVRM: drop superfluous `q_if_overflow` spec: DVRM: fix typos spec: DVRM: fix casting spec: ZERO: expand lookup to B20 spec: DVRM: abandon `IsZero` and `IsEqual` templates spec: DVRM: fix typo spec: expr: update constant rendering in expr_to_math Update spec/bitwise.typ Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> spec: DVRM: replace [Half, x] by xHL spec: DVRM: use QuadHL-sub to constrain `extended_n_sub_r` spec: drop support variable labelling This reverts commit c8d6896 (and removes a bit more). spec: DVRM: fix dvrm:c:div_by_zero Update spec/dvrm.typ Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: signatures (#280) * spec: list all interaction signatures * Update spec/signatures.typ Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> * spec: signatures: fix LOAD signature * spec: signatures: make IS_BIT's cond a BaseField * spec: signatures: make ECALL's syscallnr a DWordWL * spec: signatures: preemptively introduce NEG signature (see #270) * spec: signatures: fix DWordDL typo Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> --------- Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: Leverage `NEG` in `DVRM` (#287) * spec: DVRM: use NEG template for abs_r and abs_d This saves 4 columns. * Apply suggestions from @RobinJadoul Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: Add initial tooling to check data formats, prepare for more elaborate type checking (#271) * spec: Add initial tooling to check data formats, prepare for more elaborate type checking * Initial type checking * ruff format * Update some more typing mismatches * Move to range-based type checks * Avoid casting to more limbs by leveraging scalar-array mult and literal casts * toml fixes to pass type checks * Type check virtual definitions properly now * ruff format * Make typst compile by turning big range values to string * Switch some isinstance checks around to make both mypy and ty work * Fix issues after rebasing on spec/main * Address review comments * Review comments * lit -> const * spec: Introduce array expressions (#295) Closes #135 * spec: separate ALU path for STORE to enable byte representation of rv2 to exist in arg2 (#308) * spec: separate ALU path for STORE to enable byte representation of rv2 to exist in arg2 * Apply review suggestion Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * Update spec/src/cpu.toml Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --------- Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: `COMMIT` chip (#283) * spec: update footnote numbering * spec: COMMIT: specify commit chip * spec: COMMIT: fix typos * Move footnote numbering to a more general spot and allow easy future updates * Update common-formatting location * spec: COMMIT: update citation links * spec: COMMIT: deal with committing 0 bytes * spec: COMMIT: list future improvement * Fix typos Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: COMMIT: rearrange CNB multiplicity * spec: COMMIT: update padding strategy permitting ADD and SUB constraints of lower degree * spec: COMMIT: list two possible optimizations --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: Typecheck signatures and make all chips pass (#312) * spec: Typecheck signatures and make all chips pass * Apply suggestion from @RobinJadoul * Apply suggestion from @RobinJadoul * Apply suggestion from @RobinJadoul * s/IS_HALFWORD/IS_HALF * Ensure constants being casted fit into the first limb * spec: Variable category for constants (#327) Closes #303 * spec: Fix interaction signatures for COMMIT (#328) * spec: Cleanup, uniformize chapters, make colors work better on web. (#336) * spec: Cleanup, uniformize chapters, make colors work better on web. * Fix double scroll bar * Improve decode table * Remove `style` state and make aside box grey. Having multiple web themes makes the style approach almost always wrong, since we cannot rely on the scheme being dark or light, in contrast to a regular PDF. * Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * Update spec/cpu.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --------- Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> * spec: LogUp: Vanilla protocol description (#243) --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: Add a version and title/front pages (#367) * spec: Losing some MEMW weight (#398) * spec: Some fixes and improvements for SHIFT (#400) * spec: Some fixes for SHIFT Closes: #389 * spec: Merge HWSL with HWSLC, to simplify SHIFT Closes: #119 * typo Co-authored-by: Cyprien de Saint Guilhem <c.desaintguilhem@gmail.com> --------- Co-authored-by: Cyprien de Saint Guilhem <c.desaintguilhem@gmail.com> * Fix type checking for MEMW_A (#423) * Spec/memw update (#434) * spec/memw: read/write from/to -> read from/write to * spec/memw: rename add_limb_overflow as carry * spec/memw: minor var desc updates * spec/memw: remove superfluous minus symbol * spec/memw: update description * spec/memw_a: minor optimization * Apply suggestions from code review Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com> * spec/MEMW: fix interaction typing * spec/MEMW: drop superfluous notes * spec/MEMW: update alignment requirement * spec/MEMW: intentionally separate carry's prose and .toml descriptions --------- Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com> * spec/MEMW(_A): minor update (#459) * spec/memw: read/write from/to -> read from/write to * spec/memw: rename add_limb_overflow as carry * spec/memw: minor var desc updates * spec/memw: remove superfluous minus symbol * spec/memw: update description * spec/memw_a: minor optimization * Apply suggestions from code review Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com> * spec/MEMW: fix interaction typing * spec/MEMW: drop superfluous notes * spec/MEMW: update alignment requirement * spec/MEMW: intentionally separate carry's prose and .toml descriptions * spec/MEMW: fix multiplicities * spec/MEMW_A: padding * spec/MEMW: padding * spec/MEMW: bit check multiplicities * spec/MEMW: simplify padding --------- Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com> * spec/MEMW_R: register access fast path (#457) --------- Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com> * spec: Fix CPU sign bit constraints for `word_instr` (#435) * spec: interaction counter (#469) * spec: recursively compute chip interaction count * spec: print interaction count per chip * spec: cleanup * spec/interaction-counter: add multi-dimensional iter support * spec/interaction-counter: count SUB interactions * spec/interaction-counter: drop silent lookup fails * spec/interaction-counter: remove superfluous code * spec/interaction_count: merge getter and setter * spec/interaction_counter: clean up * spec: run spec-tooling in CI (#440) * spec: have tooling exit(1) on error * spec: run spec tooling in CI * spec/tooling: verbosely state when no issues are found * spec/CI: ignore benchmarks for spec stuff * spec: update TOC (#478) * spec: add chapters * spec: clean up toc * spec: separate ecalls * Fixes for shiroa * Reformat ebook.typ a bit --------- Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech> * spec: cleanup before v0.2 (#479) * spec: add backticks to section titles * spec: replace "columns" headers with "variables" * spec: auto count nr_variables * spec: standardize "optimizations"-section headers * spec/config: add missing spaces * spec/chip: rename *_column_table as *_variable_table * spec: drop table captions * spec/v0.2: turn note into aside * spec: place correctness arguments in separate section * spec/tooling: add default case in `build_signature` * spec/tooling: fix hidden global variable * spec/tooling: fix silent side effect * spec/tooling: context manage file reads * spec: fix precedence Swap precedence of ADD and SUB and treat the first subexpression of a SUB differently --------- Co-authored-by: Erik Takke <erik.takke@3milabs.tech> Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> Co-authored-by: Joaquin Carletti <56092489+ColoCarletti@users.noreply.github.com> Co-authored-by: Cyprien de Saint Guilhem <c.desaintguilhem@gmail.com> Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> Co-authored-by: Diego K <43053772+diegokingston@users.noreply.github.com>

spec: Padding specifications for array types #135

Description

Activity

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions