spec: Introduce LT chip by RobinJadoul · Pull Request #90 · yetanotherco/lambda_vm

RobinJadoul · 2025-12-31T12:27:16Z

This should be a decent first version of the chip, ready to merge until we get to writing a bunch more things in the typst file.

erik-3milabs

There are some points to look at before we can merge this.

erik-3milabs

Couple more details to iron out.

erik-3milabs

Well, I found a bug (= old mistake of mine) and a potential optimisation!

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

RobinJadoul · 2026-01-05T18:05:04Z

@erik-3milabs I've managed to get the cleanup in, along with the optimizations we discussed. Proving was a bit of a struggle, but I think it should be correct now 🤞

erik-3milabs

I believe the explanation would significantly benefit from introducing separate symbols for signed and unsigned ordering. In one of my comments, I propose to use < and ≺, but I'm open to using other symbols if you happen to find something even better.

erik-3milabs · 2026-01-07T09:55:20Z

+We can conclude that $a < b$ exactly when any of the following disjoint events happens.
+
+- $(a < 0) and (b >= 0)$
+- $(a < 0) and (b < 0) and (a < b)$
+- $(a >= 0) and (b >= 0) and (a < b)$


It is confusing to me that we're decomposing a < b into three events and then have a<b again show up in two of those events. It makes me ask wonder: how could it ever be easier to detect a < 0 AND b <0 AND a < b than just a<b? The remaining explanation does not answer this question (for me).

Actually, I think we don't check that a < b, but rather that (a as u64 < b as u64) (i.e., a < b in the unsigned case). This is a slightly different less-than operation, which makes the decomposition a lot more sense.

Perhaps we should treat the LT operator as defining an ordering on 32-bit strings (in one of two ways), and then have two distinct orderings (e.g. < (unsigned) and ≺ (signed)), such that we can they say

a ≺ b iff

a ≺ 0 AND b ≽ 0, or

a ≺ 0 AND b ≺ 0 AND a < b, or

a ≽ 0 AND b ≽ 0 AND a < b

It becomes a bit more abstract, perhaps, but I do think it would yield a much more robust explanation. Wdyt?

Also, regarding an earlier remark:

Actually, I think we don't check that a < b, but rather that (a as u64 < b as u64) (i.e., a < b in the unsigned case)

If we do decide on the "more robust" explanation I propose above, we should consider to define C := unsigned_lt.

Also, perhaps we should make this an enumeration, rather than itemization?

The decomposition doesn't use the u64 comparison here yet.
It may seem nonsensical on the surface to define and event A in terms of (A and B) or (A and not B), but it's a common trick to condition things and allow treating different cases differently.
In this case, we've implicitly discarded the case (a < b) and (a >= 0) and (b < 0) since it's always false.

The rest of the construction first deals with the first case by inspection of sign bits, and then deals with the other two cases by introducing C.
Looking towards another comment, indeed C is maybe slightly ill defined and should instead be (a < b) conditioned on A == B instead.

The decomposition doesn't use the u64 comparison here yet.

I'm not saying it is. I'm just saying we could, and thus express the signed lt in terms of unsigned lt.

It may seem nonsensical on the surface to define and event A in terms of (A and B) or (A and not B), but it's a common trick to condition things and allow treating different cases differently.

I understand the trick. I'm just saying that if a<b becomes easier to compute when you're conditioning on a and/or b, you're probably not computing a<b directly there, but instead taking a slightly different relation (which you can compute easily) to derive a<b. In our case: we're taking the unsigned-< to compute signed-<

I'm done discussing this point, however. I'm OK with how things are written now.

erik-3milabs · 2026-01-07T10:05:30Z

+- $(a < 0) and (b < 0) and (a < b)$
+- $(a >= 0) and (b >= 0) and (a < b)$
+
+We represent can the comparisons of inputs to zero as the MSB or sign bits,


Suggested change

We represent can the comparisons of inputs to zero as the MSB or sign bits,

We can represent the comparisons of inputs to zero as the MSB or sign bits,

We can represent the comparisons of inputs to zero as the MSB or sign bits,

The phrase "as the MSB or sign bits" leaves me wandering .... "of what? How does 'the MSB or sign bits' relate to the rest of the sentence?"
I don't think swapping the with their does the trick. The more expressive "that input's [MSB or sign bit]" would do the trick IMO

Suggested change

We represent can the comparisons of inputs to zero as the MSB or sign bits,

We represent can the comparisons of inputs to zero as that input's MSB or sign bit,

but I feel the sentence would still be lacking detail on how an input's MSB/sign bit can represent its comparison to zero (I know: 1 = negative, 0 is non-negative. But the text doesn't tell me that)

Suggested change

We represent can the comparisons of inputs to zero as the MSB or sign bits,

We can represent the comparison of an input to zero as the input's MSB or sign bit,

But I would assume that anyone reading this is expected to understand 2s complement and how a sign bit relates to the sign

suffice it to say that the phrase "not(A) and B and (a<b)" is trivially false, took me some time to understand, because I has true=positive/false=negative in my head.

erik-3milabs · 2026-01-07T10:06:31Z

+
+We represent can the comparisons of inputs to zero as the MSB or sign bits,
+which we shall denote as $A$ for `lhs` and $B$ for `rhs`.
+From this, we obtain the boolean formula $A dash(B) or A B C or dash(A) dash(B) C$,


"From this" refers to the decomposition, which we haven't talked about for a complete sentence. I feel that this is reaching back too far.

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

erik-3milabs · 2026-01-07T16:33:24Z

+We split $a < b$ into four disjoint cases, conditioned on the sign of $a$ and $b$.
+Recall that the sign of a number in two's complement can be read off from the MSB,
+being $1$ for a negative number and $0$ for a positive one.
+For this analysis, we denote the MSB of `lhs` as $A$ and the MSB of `rhs` as $B$.


The enumeration comes seemingly out of nowhere. Perhaps rearranging the sentences and adding a colon suffices:

Suggested change

We split $a < b$ into four disjoint cases, conditioned on the sign of $a$ and $b$.

Recall that the sign of a number in two's complement can be read off from the MSB,

being $1$ for a negative number and $0$ for a positive one.

For this analysis, we denote the MSB of `lhs` as $A$ and the MSB of `rhs` as $B$.

Let us first recall that the sign of a number in two's complement can be read off from the MSB,

being $1$ for a negative number and $0$ for a positive one.

For this analysis, we denote the MSB of `lhs` as $A$ and the MSB of `rhs` as $B$.

We split $a < b$ into four disjoint cases, conditioned on the sign of $a$ and $b$:

also, you're talking about

"the sign of a and b",

"MSB of lhs as A and the msb of rhs as B" and

C = unsigned_lt

Either stick to a/b for an abstract discussion, or replace them with lhs/rhs for a specific discussion.

erik-3milabs · 2026-01-07T16:41:15Z

+The polynomial $P$ can be simplified to a total degree of two.
+We claim that the polynomial $Q(A, B, C) = A (1 - B) + A C + (1 - B) C$
+is, for the purposes of this chip, equivalent to $P$.
+An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$, only for the triple $(A, B, C) = (1, 0, 1)$.


Suggested change

An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$, only for the triple $(A, B, C) = (1, 0, 1)$.

An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$ only for the triple $(A, B, C) = (1, 0, 1)$.

erik-3milabs · 2026-01-07T16:41:25Z

+We claim that the polynomial $Q(A, B, C) = A (1 - B) + A C + (1 - B) C$
+is, for the purposes of this chip, equivalent to $P$.
+An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$, only for the triple $(A, B, C) = (1, 0, 1)$.
+This is however impossible due to the correctness of `ADD`.


Suggested change

This is however impossible due to the correctness of `ADD`.

This is, however, impossible due to the correctness of `ADD`.

erik-3milabs · 2026-01-07T16:43:17Z

+This is however impossible due to the correctness of `ADD`.
+In more detail, if we let $s$ be the (range-checked) difference $a - b$
+(so the equivalent of the #`lhs_sub_rhs` column),
+and $x'$ be the most significant word of $x$,


"let x' be the ms-word of x" suggests that x is an instantiated variable.

Suggested change

and $x'$ be the most significant word of $x$,

and use $x'$ to denote the most significant word of variable $x$,

erik-3milabs · 2026-01-07T16:45:58Z

+(so the equivalent of the #`lhs_sub_rhs` column),
+and $x'$ be the most significant word of $x$,
+we need $c dot 2^32 + a' = b' + s' + #`carry[0]`$, by the definition of `carry`.
+However, the left hand side of this, is at least $3 dot 2^31$, as $(A, C) = (1, 1)$,


Suggested change

However, the left hand side of this, is at least $3 dot 2^31$, as $(A, C) = (1, 1)$,

However, the left hand side of this is at least $3 dot 2^31$, as $(A, C) = (1, 1)$,

erik-3milabs · 2026-01-07T16:50:38Z

+
+[[constraints.defs]]
+kind = "arith"
+constraint = "$#`lt` = #`signed` dot (A (1 - B) + A C + (1 - B) C) + (1 - #`signed`) dot #`unsigned_lt`$"


I'm just now noticing that signed_lt is equivalent to lhs_msb + (1-rhs_msb) + carry_1 >= 2.
I don't know what we can do with that, but it is a linear expression 🤔 Maybe there is a way to make lt virtual?

Hmm, interesting; the only trick I can see immediately to check >= 2 is to do and AND_BYTE[..., 2], but that still needs an instantiated lt column.

erik-3milabs · 2026-01-07T16:52:51Z

+[[variables.virtual]]
+name = "carry"
+type = ["Bit", 2]
+desc = "The carry of subtracting limbs of `rhs` from those of `lhs`"


Technically speaking, this is the carry from adding lhs - rhs to rhs.
Also, it couldn't be "the carry of subtracting ..." since subtracting only knows a borrow.

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

RobinJadoul requested a review from erik-3milabs December 31, 2025 12:27

RobinJadoul self-assigned this Dec 31, 2025

erik-3milabs requested changes Jan 2, 2026

View reviewed changes

erik-3milabs added the documentation Improvements or additions to documentation label Jan 2, 2026

RobinJadoul force-pushed the spec/LT branch 2 times, most recently from 1692351 to 21a4731 Compare January 2, 2026 10:52

RobinJadoul requested a review from erik-3milabs January 2, 2026 10:53

RobinJadoul force-pushed the spec/LT branch from 21a4731 to e4c1c34 Compare January 2, 2026 11:03

erik-3milabs requested changes Jan 2, 2026

View reviewed changes

Comment thread spec/src/lt.toml Outdated

Comment thread spec/src/lt.toml Outdated

Comment thread spec/src/lt.toml

Comment thread spec/src/lt.toml Outdated

RobinJadoul requested a review from erik-3milabs January 2, 2026 15:48

RobinJadoul added the spec Updates and improvements to the spec document label Jan 2, 2026

erik-3milabs reviewed Jan 3, 2026

View reviewed changes

Comment thread spec/src/lt.toml Outdated

Comment thread spec/src/lt.toml Outdated

Comment thread spec/src/lt.toml

erik-3milabs and others added 7 commits January 5, 2026 19:03

spec: Introduce LT chip

65b3840

Address review comments

b69ca49

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

Update LT virtual defs to new format

3560d63

Fix signed_lt constraint to actually constraint signed_lt

31e0c35

Thanks Erik :)

c87e890

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

Logic fix

54dc14f

Optimize away two columns of LT and do some proving that that works

5d8834f

RobinJadoul force-pushed the spec/LT branch from 0fa55af to 5d8834f Compare January 5, 2026 18:03

RobinJadoul requested a review from erik-3milabs January 5, 2026 18:04

RobinJadoul force-pushed the spec/main branch 2 times, most recently from 273bbd2 to 1b83850 Compare January 6, 2026 10:44

erik-3milabs reviewed Jan 7, 2026

View reviewed changes

RobinJadoul and others added 2 commits January 7, 2026 12:09

Apply suggestions from code review

f0ad43f

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

Proof rewrite for clarity

9b163c2

RobinJadoul requested a review from erik-3milabs January 7, 2026 12:07

erik-3milabs approved these changes Jan 7, 2026

View reviewed changes

More review comments

691e8e2

RobinJadoul merged commit 7e842e5 into spec/main Jan 8, 2026

RobinJadoul deleted the spec/LT branch January 8, 2026 10:17

RobinJadoul mentioned this pull request Feb 26, 2026

spec: Add a version and title/front page #367

Merged

	We represent can the comparisons of inputs to zero as the MSB or sign bits,
	We can represent the comparisons of inputs to zero as the MSB or sign bits,

	We represent can the comparisons of inputs to zero as the MSB or sign bits,
	We can represent the comparison of an input to zero as the input's MSB or sign bit,

	An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$, only for the triple $(A, B, C) = (1, 0, 1)$.
	An exhaustive check shows that $P(A, B, C) != Q(A, B, C)$ only for the triple $(A, B, C) = (1, 0, 1)$.

	This is however impossible due to the correctness of `ADD`.
	This is, however, impossible due to the correctness of `ADD`.

	and $x'$ be the most significant word of $x$,
	and use $x'$ to denote the most significant word of variable $x$,

	However, the left hand side of this, is at least $3 dot 2^31$, as $(A, C) = (1, 1)$,
	However, the left hand side of this is at least $3 dot 2^31$, as $(A, C) = (1, 1)$,

Conversation

RobinJadoul commented Dec 31, 2025

Uh oh!

erik-3milabs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

erik-3milabs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

erik-3milabs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

RobinJadoul commented Jan 5, 2026

Uh oh!

erik-3milabs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RobinJadoul Jan 7, 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RobinJadoul Jan 7, 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

RobinJadoul Jan 7, 2026 •

edited

Loading

RobinJadoul Jan 7, 2026 •

edited

Loading