Spec/memw update by erik-3milabs · Pull Request #434 · yetanotherco/lambda_vm

erik-3milabs · 2026-03-17T09:21:06Z

Changes:

Remove one column from MEMW_A
Expand base_address increment-trick explanation
Variable renames & description updates

github-actions · 2026-03-17T09:23:21Z

Codex Code Review

Findings

High – VM correctness/security regression (alignment check removed)

In spec/src/memw_aligned.toml, the old alignment constraint (AND_BYTE with mask 1/3/7) was replaced with IS_HALFWORD(base_address[0] + offset).
This no longer enforces read/write alignment (addr % 2/4/8 == 0). Example: base_address[0]=1, write2=1 passes IS_HALFWORD(2) but is misaligned.
For VM memory semantics, this is a real behavior/soundness risk.

High – Type/signature mismatch in MEMW interaction

spec/src/memw_aligned.toml:198 and spec/src/memw_aligned.toml:205 now pass base_address of type DWordWHH directly to tag MEMW.
MEMW signature expects DWordWL in spec/src/signatures.toml:63 and spec/src/signatures.toml:70.
Memory constraints in the same file already added explicit casts, but output constraints did not. This can break constraint typing or wire the wrong representation.

Medium – Input assumptions are weakened/incorrect for DWordWHH

spec/src/memw_aligned.toml:88 now assumes IS_WORD[base_address[i]] for i=0..1.
DWordWHH is ["Half","Half","Word"] (config.toml:86); this assumption skips one limb and does not enforce halfword bounds on the first two limbs.
This underconstrains address well-formedness compared to the previous explicit checks.

claude · 2026-03-17T09:26:20Z

+Still, these properties are necessary for the consistency of the system as a whole, and therefore
 we document it here, keeping the type information as a reading help.

 = Constraints


Low – Off-by-one in carry description

The prose says the carry bit indicates whether base_address_0 + i >= 2^32, but the polynomial definition in memw.toml computes address_add[i] = base_address + (i + 1), so the carry is used to absorb overflow of base_address[0] + i + 1. The .toml description correctly says base_address[0] + i + 1 >= 2^32.

Suggested change

= Constraints

+Rather than computing these in full (which would require the later addresses to be instantiated),

+it suffices to know the `carry`: the bit indicating whether $#`base_address`_0 + i + 1 >= 2^32$, i.e., whether adding $i + 1$ to `base_address` requires a carry from the lower to the upper limb.

The i in the prose does not match the one in the toml. I've updated the prose to better illustrate the difference.

github-actions · 2026-03-17T09:26:38Z

Benchmark Results for unmodified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base binary_search`	75.2 ± 11.6	62.7	88.9	1.15 ± 0.18
`head binary_search`	65.6 ± 2.9	62.2	68.8	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base bitwise_ops`	65.9 ± 3.5	62.4	70.2	1.03 ± 0.07
`head bitwise_ops`	64.0 ± 2.8	62.2	69.3	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base fibonacci_26`	67.8 ± 2.0	65.7	71.4	1.00 ± 0.05
`head fibonacci_26`	67.8 ± 2.4	65.8	71.4	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base hashmap`	135.1 ± 3.3	131.4	142.7	1.00
`head hashmap`	136.3 ± 6.1	130.8	152.4	1.01 ± 0.05

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base keccak`	133.7 ± 4.7	126.7	138.9	1.02 ± 0.05
`head keccak`	130.9 ± 4.4	126.2	138.8	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base matrix_multiply`	70.5 ± 5.9	66.0	83.2	1.04 ± 0.09
`head matrix_multiply`	67.5 ± 1.6	65.5	70.8	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base modular_exp`	62.3 ± 0.6	61.6	63.5	1.00
`head modular_exp`	66.4 ± 3.6	61.8	69.4	1.06 ± 0.06

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base quicksort`	74.2 ± 20.1	65.3	131.0	1.11 ± 0.30
`head quicksort`	66.6 ± 2.1	65.0	70.8	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base sieve`	70.5 ± 2.9	67.2	73.7	1.00
`head sieve`	70.8 ± 3.1	67.3	75.2	1.00 ± 0.06

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base sum_array`	79.6 ± 2.1	76.9	82.3	1.00
`head sum_array`	80.1 ± 1.7	78.3	81.9	1.01 ± 0.03

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`base syscall_commit`	100.3 ± 3.8	96.7	106.9	1.02 ± 0.05
`head syscall_commit`	98.0 ± 3.1	95.8	106.5	1.00

claude · 2026-03-17T09:27:00Z

Review: spec/memw update

The simplification of MEMW_A (replacing three decomposed inputs with a single DWordWHH) is a reasonable improvement, but the PR introduces a few correctness issues.

[Medium] IS_HALFWORD undefined and alignment semantics changed (memw_aligned.toml:113)

IS_HALFWORD does not appear in signatures.toml. More critically, the old AND_BYTE[byte, mask] = 0 was a true alignment constraint (forcing the lowest N bits of the address to zero for 2/4/8-byte accesses). If IS_HALFWORD is just a range check for [0, 2^16), alignment is no longer enforced in the aligned fast-path. If it is a new alignment-aware lookup, it needs to be added to signatures.toml.

[Medium] Missing range-check assumption for base_address[2] (memw_aligned.toml:87-89)

DWordWHH has subtypes [Half, Half, Word] — three components. The new assumption iterates i in [0, 1], leaving base_address[2] (the high Word) without a range-check assumption. The old spec had IS_WORD[base_address_high] explicitly. Additionally, IS_WORD on Half subtypes is weaker than IS_HALF; base_address[0] and base_address[1] should use IS_HALF, and base_address[2] should use IS_WORD.

[Medium] Type mismatch in constraints.output MEMW interactions (memw_aligned.toml, output section — not in diff)

All constraints.memory interactions correctly cast base_address to DWordWL. However the two constraints.output MEMW interactions still pass base_address (type DWordWHH) directly, but the MEMW signature expects DWordWL. These should also use cast base_address DWordWL, as was implicitly correct before (when base_address was a virtual DWordWL).

[Low] Off-by-one in carry description in prose (memw.typ:39)

The .typ says carry indicates base_address_0 + i >= 2^32, but the polynomial computes base_address[0] + i + 1 - 2^32 * carry[i]. So carry captures overflow of base_address[0] + i + 1, not base_address[0] + i. The .toml description is already correct (>= 2^32 for i+1); the .typ should match.

RobinJadoul

Neat trick!
This makes the fast chip even more applicable (though hard to say how much of the extra applicability will ever actually be used).

RobinJadoul · 2026-03-17T10:18:00Z

I would update this description a bit to reflect the update

Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

erik-3milabs · 2026-03-18T10:05:41Z

Addressing the automated reviews:

High – VM correctness/security regression (alignment check removed)

While correctly assessed that there is a change, here, this does not lead to a regression.
In fact, it allows the aligned access chip to be used more often (although both @RobinJadoul and I are unsure whether the increase will be significant)

High – Type/signature mismatch in MEMW interaction

Correctly assessed. This was changed accordingly.

Medium – Input assumptions are weakened/incorrect for DWordWHH

Correctly assessed. This was changed accordingly.

[Medium] IS_HALFWORD undefined and alignment semantics changed (memw_aligned.toml:113)

Correctly assessed. This was changed accordingly.

[Medium] Missing range-check assumption for base_address[2] (memw_aligned.toml:87-89)

Duplicate

[Medium] Type mismatch in constraints.output MEMW interactions (memw_aligned.toml, output section — not in diff)

Duplicate

[Low] Off-by-one in carry description in prose (memw.typ:39)

The prose and .toml were not supposed to align in the first place. I've updated the prose to further illustrate them being disjoint descriptions.

* Add MEMW_A aligned-memory fast path table * fix deviation from spec: is_half and is_byte assumptions * add comment * Add a prove_elf test * add prove_elf test using both MEMW and MEMW_A chips * fix comment: bus numbering * Use Multiplicity::Sum3 for w2 in MEMW_A to avoid heap allocation on hot path * change max_rows per chunk to 2^19 insted of 2^20 * Update MEMW and MEMW_A tables to match spec after PRs #434 and #459 * fix u16 overflow * Update comment * fix numbering in comments --------- Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>

@RobinJadoul

* 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>

erik-3milabs added 6 commits March 17, 2026 09:26

spec/memw: read/write from/to -> read from/write to

f38c1c7

spec/memw: rename add_limb_overflow as carry

677b166

spec/memw: minor var desc updates

ad3f093

spec/memw: remove superfluous minus symbol

109489b

spec/memw: update description

03a2338

spec/memw_a: minor optimization

b8fc0b7

erik-3milabs requested a review from RobinJadoul March 17, 2026 09:21

erik-3milabs self-assigned this Mar 17, 2026

erik-3milabs added the spec Updates and improvements to the spec document label Mar 17, 2026

claude Bot reviewed Mar 17, 2026

View reviewed changes

Comment thread spec/src/memw_aligned.toml Outdated

claude Bot reviewed Mar 17, 2026

View reviewed changes

Comment thread spec/src/memw_aligned.toml

claude Bot reviewed Mar 17, 2026

View reviewed changes

RobinJadoul reviewed Mar 17, 2026

View reviewed changes

erik-3milabs and others added 5 commits March 18, 2026 10:45

Apply suggestions from code review

b6b00c6

Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

spec/MEMW: fix interaction typing

a099bbd

spec/MEMW: drop superfluous notes

448555d

spec/MEMW: update alignment requirement

4936d8c

spec/MEMW: intentionally separate carry's prose and .toml descriptions

0e3d0f8

erik-3milabs requested a review from RobinJadoul March 18, 2026 10:21

RobinJadoul approved these changes Mar 18, 2026

View reviewed changes

erik-3milabs merged commit 8f7ddea into spec/main Mar 23, 2026
6 checks passed

erik-3milabs deleted the spec/memw_update branch March 23, 2026 16:23

nicole-graus added a commit that referenced this pull request Mar 25, 2026

Update MEMW and MEMW_A tables to match spec after PRs #434 and #459

c5c69f4

nicole-graus mentioned this pull request Mar 31, 2026

Update MEMW and MEMW_A to match spec #472

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Spec/memw update#434

Spec/memw update#434
erik-3milabs merged 11 commits into
spec/mainfrom
spec/memw_update

erik-3milabs commented Mar 17, 2026

Uh oh!

github-actions Bot commented Mar 17, 2026

Uh oh!

Uh oh!

Uh oh!

claude Bot Mar 17, 2026

Uh oh!

erik-3milabs Mar 18, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Mar 17, 2026 •

edited

Loading

Uh oh!

claude Bot commented Mar 17, 2026

Uh oh!

RobinJadoul left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

RobinJadoul Mar 17, 2026

Uh oh!

erik-3milabs commented Mar 18, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	= Constraints
	+Rather than computing these in full (which would require the later addresses to be instantiated),
	+it suffices to know the `carry`: the bit indicating whether $#`base_address`_0 + i + 1 >= 2^32$, i.e., whether adding $i + 1$ to `base_address` requires a carry from the lower to the upper limb.

Conversation

erik-3milabs commented Mar 17, 2026

Uh oh!

github-actions Bot commented Mar 17, 2026

Codex Code Review

Uh oh!

Uh oh!

Uh oh!

claude Bot Mar 17, 2026

Choose a reason for hiding this comment

Uh oh!

erik-3milabs Mar 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Mar 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

claude Bot commented Mar 17, 2026

Review: spec/memw update

Uh oh!

RobinJadoul left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

RobinJadoul Mar 17, 2026

Choose a reason for hiding this comment

Uh oh!

erik-3milabs commented Mar 18, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

erik-3milabs Mar 18, 2026 •

edited

Loading

github-actions Bot commented Mar 17, 2026 •

edited

Loading