Skip to content

spec: Introduce array expressions#295

Merged
RobinJadoul merged 1 commit into
spec/mainfrom
spec/arr-expr
Feb 10, 2026
Merged

spec: Introduce array expressions#295
RobinJadoul merged 1 commit into
spec/mainfrom
spec/arr-expr

Conversation

@RobinJadoul
Copy link
Copy Markdown
Collaborator

@RobinJadoul RobinJadoul commented Feb 6, 2026

Closes #135

To be merged after #271

@RobinJadoul RobinJadoul self-assigned this Feb 6, 2026
@RobinJadoul RobinJadoul added enhancement New feature or request spec Updates and improvements to the spec document labels Feb 6, 2026
@greptile-apps
Copy link
Copy Markdown

greptile-apps Bot commented Feb 6, 2026

Greptile Overview

Greptile Summary

  • Adds a new expression form for arrays (["arr", ...]) and renders it in both code and math formatters.
  • Updates chip tooling parser/typechecker to recognize array expressions and updates some TOML specs to use array padding values.
  • Adjusts chip.typ preprocessed-variable detection to avoid treating unknown types as preprocessed.
  • Main issue: the new math formatter for arrays likely emits nested $...$ math blocks, which will break Typst compilation where expr_to_math is embedded in other math expressions.

Confidence Score: 3/5

  • This PR is close to mergeable but likely breaks Typst compilation due to the new array math formatter emitting nested math delimiters.
  • Core changes are small and scoped, but the expr_to_math implementation for arrays appears inconsistent with the existing formatter contract (math fragments), which is a concrete compile-time issue for the spec docs. Python tooling changes look structurally fine but weren’t executable in this environment.
  • spec/expr.typ (array math formatting); secondarily spec/tooling/chip.py for type semantics consistency

Important Files Changed

Filename Overview
spec/chip.typ Fixes preprocessed-variable detection to avoid .all() on empty type lookup; otherwise unchanged.
spec/expr.typ Adds array expression syntax and formatting in code/math renderers; introduces a likely formatting bug in expr_to_math for arrays due to nested math mode delimiters.
spec/src/branch.toml Updates padding for next_pc_high from scalar 0 to an explicit array expression ["arr", 0,0,0] matching type length.
spec/src/shift.toml Replaces scalar pad placeholders with explicit array padding expressions for X, Y, limb_shift to match their array types.
spec/tooling/chip.py Introduces ArrExpr and parsing for ["arr", ...] plus minor formatting; ArrExpr.typecheck returns a Python list but Type alias expects list[Type]

Sequence Diagram

sequenceDiagram
  participant TOML as spec/src/*.toml
  participant ChipPy as spec/tooling/chip.py
  participant ExprTyp as spec/expr.typ
  participant ChipTyp as spec/chip.typ

  TOML->>ChipPy: build_expr(["arr", ...]) from pad/defs
  ChipPy->>ChipPy: ArrExpr.typecheck(env)
  ChipPy-->>ChipTyp: Typed columns/padding used in tables

  TOML->>ExprTyp: expr_to_code/expr_to_math(pad expr)
  ExprTyp-->>ChipTyp: Render padding/defs in spec tables
  ChipTyp-->>ChipTyp: is_preprocessed(var) checks type metadata

Loading

Copy link
Copy Markdown

@greptile-apps greptile-apps Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

5 files reviewed, 1 comment

Edit Code Review Agent Settings | Greptile

@greptile-apps
Copy link
Copy Markdown

greptile-apps Bot commented Feb 6, 2026

Additional Comments (1)

spec/expr.typ
Array math formatter breaks

expr_to_math's new array case wraps the whole result in $...$ even though this formatter already returns math fragments. This will end up nesting math mode delimiters inside an existing math context (e.g. expr_to_math is used inside other $...$ expressions in spec/chip.typ), which causes Typst parse errors.

    "arr": (pp, rec, e) => $[#e.slice(1).map(rec.with(PREC.MAX)).join($, $)]$,

Consider returning a fragment without $...$, e.g. $[#... ] (or build the bracketed list via mwrap(...)), consistent with other cases like "+" and "*".

@RobinJadoul RobinJadoul linked an issue Feb 6, 2026 that may be closed by this pull request
@RobinJadoul RobinJadoul mentioned this pull request Feb 6, 2026
@RobinJadoul
Copy link
Copy Markdown
Collaborator Author

Everything compiles fine in typst, and mwrap isn't needed since arrays come with their own non-paren delimiters.
@greptileai

@greptile-apps
Copy link
Copy Markdown

greptile-apps Bot commented Feb 6, 2026

Greptile Overview

Greptile Summary

This PR introduces array expression support to the specification system, allowing array-typed variables to have proper array padding values instead of using scalar fallbacks. The changes add a new ArrExpr type to the Python type checker (spec/tooling/chip.py), update the Typst grammar and formatters (spec/expr.typ), and convert padding values in branch.toml and shift.toml from scalar 0 to proper array expressions like ["arr", 0, 0, 0].

Key changes:

  • Added ArrExpr dataclass with typechecking that returns a list of element types
  • Implemented array expression parsing in build_expr() matching ["arr", *elems]
  • Added formatters for array expressions in both code ([e1, e2, e3]) and math notation
  • Fixed bug in spec/chip.typ where .all() was called on potentially empty filtered arrays
  • Updated padding values for array-typed variables (next_pc_high, X, Y, limb_shift) to use array expressions

The implementation follows existing patterns in the codebase, properly integrates with the type system, and resolves TODO comments about array handling.

Confidence Score: 5/5

  • This PR is safe to merge with minimal risk
  • The implementation is clean, well-structured, and follows existing patterns throughout the codebase. The array expression feature adds proper type support for array padding values, replacing placeholder scalar values. The bug fix in spec/chip.typ prevents potential runtime errors from calling .all() on empty arrays. All changes are self-contained, the new ArrExpr class integrates seamlessly with the existing type system, and the TOML updates properly leverage the new functionality.
  • No files require special attention

Important Files Changed

Filename Overview
spec/tooling/chip.py Added ArrExpr dataclass and array expression parsing support - clean implementation following existing patterns
spec/expr.typ Added array expression syntax to grammar and formatters for both code and math rendering
spec/chip.typ Fixed bug where .all() was called on potentially empty array by checking length first
spec/src/branch.toml Updated next_pc_high padding from scalar 0 to array expression ["arr", 0, 0, 0]
spec/src/shift.toml Updated padding for X, Y, and limb_shift arrays from scalar 0 to proper array expressions

Sequence Diagram

sequenceDiagram
    participant TOML as TOML Files (branch.toml, shift.toml)
    participant Parser as build_expr()
    participant ArrExpr as ArrExpr Class
    participant Typecheck as typecheck()
    participant Formatter as Formatters (expr_to_code, expr_to_math)
    participant Renderer as Typst Renderer
    
    Note over TOML: pad = ["arr", 0, 0, 0]
    
    TOML->>Parser: Parse padding expression
    Parser->>Parser: Match ["arr", *elems]
    Parser->>ArrExpr: Create ArrExpr(elems)
    
    Note over ArrExpr: Stores list of child expressions
    
    ArrExpr->>Typecheck: typecheck(env)
    loop For each element
        Typecheck->>Typecheck: e.typecheck(env)
    end
    Typecheck-->>ArrExpr: Return list[Type]
    
    ArrExpr->>Formatter: Format for display
    alt Code Format
        Formatter->>Formatter: expr_to_code()
        Note over Formatter: [e1, e2, e3]
    else Math Format
        Formatter->>Formatter: expr_to_math()
        Note over Formatter: [e₁, e₂, e₃]
    end
    
    Formatter->>Renderer: Render in document
    Note over Renderer: Display padding values in tables
Loading

@RobinJadoul RobinJadoul force-pushed the spec/arr-expr branch 2 times, most recently from a25ff49 to 3242100 Compare February 9, 2026 10:47
Copy link
Copy Markdown
Collaborator

@erik-3milabs erik-3milabs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would move some of the code (e.g. 7ef1970) to PR271, that is all about type checking, to keep this PR clean & focused on just arrays.
Aside from that, LGTM

Comment thread spec/tooling/chip.py
elems: list[Expr]

def typecheck(self, env: Environment) -> Type:
return [e.typecheck(env) for e in self.elems]
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do we not wish to enforce that len(elems) > 0? (though perhaps already on __init__)

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

suddenly, this code was moved to #271?

Comment thread spec/tooling/chip.py Outdated
Comment thread spec/tooling/chip.py Outdated
Comment thread spec/chip.typ
Comment thread spec/tooling/chip.py
@RobinJadoul
Copy link
Copy Markdown
Collaborator Author

I must have messed up with the update-refs, because that was absolutely meant to move onto the typechecking only

@RobinJadoul
Copy link
Copy Markdown
Collaborator Author

Hmm, but 7ef1970 definitely appears as commit on typecheck, so I can only guess it's a problem in github's UI

@RobinJadoul RobinJadoul force-pushed the spec/arr-expr branch 2 times, most recently from 7e92332 to 482b273 Compare February 10, 2026 13:11
@RobinJadoul RobinJadoul force-pushed the spec/arr-expr branch 2 times, most recently from 756a17e to 40365b2 Compare February 10, 2026 14:51
Base automatically changed from spec/typecheck to spec/main February 10, 2026 14:58
gabrielbosio pushed a commit that referenced this pull request Apr 10, 2026
* 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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request spec Updates and improvements to the spec document

Projects

None yet

Development

Successfully merging this pull request may close these issues.

spec: Padding specifications for array types

2 participants