Skip to content

spec/MEMW(_A): minor update #459

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
erik-3milabs merged 17 commits into from
Mar 23, 2026
Merged

spec/MEMW(_A): minor update #459

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
f38c1c7
spec/memw: read/write from/to -> read from/write to
erik-3milabs Mar 17, 2026
677b166
spec/memw: rename add_limb_overflow as carry
erik-3milabs Mar 17, 2026
ad3f093
spec/memw: minor var desc updates
erik-3milabs Mar 17, 2026
109489b
spec/memw: remove superfluous minus symbol
erik-3milabs Mar 17, 2026
03a2338
spec/memw: update description
erik-3milabs Mar 17, 2026
b8fc0b7
spec/memw_a: minor optimization
erik-3milabs Mar 17, 2026
b6b00c6
Apply suggestions from code review
erik-3milabs Mar 18, 2026
a099bbd
spec/MEMW: fix interaction typing
erik-3milabs Mar 18, 2026
448555d
spec/MEMW: drop superfluous notes
erik-3milabs Mar 18, 2026
4936d8c
spec/MEMW: update alignment requirement
erik-3milabs Mar 18, 2026
0e3d0f8
spec/MEMW: intentionally separate carry's prose and .toml descriptions
erik-3milabs Mar 18, 2026
75199d5
spec/MEMW: fix multiplicities
erik-3milabs Mar 23, 2026
55ed2e6
spec/MEMW_A: padding
erik-3milabs Mar 23, 2026
0b99118
spec/MEMW: padding
erik-3milabs Mar 23, 2026
c7203e5
spec/MEMW: bit check multiplicities
erik-3milabs Mar 23, 2026
a9a5bd2
Merge branch 'spec/main' into spec/memw_update2
erik-3milabs Mar 23, 2026
e7d9e01
spec/MEMW: simplify padding
erik-3milabs Mar 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions spec/memw.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
total_nr_variables,
total_nr_instantiated_columns,
render_constraint_table,
render_chip_padding_table,
)

#let config = load_config()
Expand Down Expand Up @@ -64,6 +65,10 @@ to effectuate that part of the memory argument.
This chip contributes the following to the lookup argument:
#render_constraint_table(chip, config, groups: "output")

= Padding
The table can be padded to the next power of two with the following value assignments:
#render_chip_padding_table(chip, config)

= Read-size aligned fast path

#let alignedchip = load_chip("src/memw_aligned.toml", config)
Expand All @@ -87,6 +92,9 @@ The #aligned chip only needs #nr_variables variables, expressed through #nr_colu
#render_chip_assumptions(alignedchip, config)
#render_constraint_table(alignedchip, config)

== Padding
The table can be padded to the next power of two with the following value assignments:
#render_chip_padding_table(alignedchip, config)

= Future optimization ideas

Expand Down
27 changes: 24 additions & 3 deletions spec/src/memw.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,36 +6,43 @@ name = "MEMW"
name = "is_register"
type = "Bit"
desc = "Whether the address represents a register index"
pad = 0

[[variables.input]]
name = "base_address"
type = "DWordWL"
desc = "The base address to read from/write to. Gets offset by $[0, 7]$ depending on the size of the access"
pad = 0

[[variables.input]]
name = "value"
type = ["BaseField", 8]
desc = "The values to store in memory. For RAM, these should be (up to) 8 range-checked `Byte`s; registers are stored as two range-checked `Word`s"
pad = 0

[[variables.input]]
name = "timestamp"
type = "DWordWL"
desc = "The timestamp at which this memory access occurs"
pad = 0

[[variables.input]]
name = "write2"
type = "Bit"
desc = "Whether to write exactly 2 values"
pad = 0

[[variables.input]]
name = "write4"
type = "Bit"
desc = "Whether to write exactly 4 values"
pad = 0

[[variables.input]]
name = "write8"
type = "Bit"
desc = "Whether to write exactly 8 values"
pad = 0

# Output

Expand All @@ -44,18 +51,21 @@ name = "old"
type = ["BaseField", 8]
desc = """The old value written at `base_address`. See `value` for information about representation.
Only the elements corresponding to the `writeN` bits are guaranteed"""
pad = 0

# Auxiliary

[[variables.auxiliary]]
name = "carry"
type = ["Bit", 7]
desc = "Whether `base_address[0] + i + 1` $>= 2^32$"
pad = 0

[[variables.auxiliary]]
name = "old_timestamp"
type = ["DWordWL", 8]
desc = "The timestamp at which address `base_address + i` was last accessed"
pad = 0

# Virtual

Expand Down Expand Up @@ -92,12 +102,13 @@ def = ["+", "μ_read", "μ_write"]
name = "μ_read"
type = "Bit"
desc = "Whether we are performing a read (and hence return `out`)"
pad = 0

[[variables.multiplicity]]
name = "μ_write"
type = "Bit"
desc = "Whether we are performing a write (and hence not return `out`)"

pad = 0

[[assumptions]]
desc = "`IS_WORD[base_address[i]]`"
Expand All @@ -123,6 +134,16 @@ iter = ["i", 0, 1]
[[constraint_groups]]
name = "consistency"

[[constraints.consistency]]
kind = "template"
tag = "IS_BIT"
input = ["μ_read"]

[[constraints.consistency]]
kind = "template"
tag = "IS_BIT"
input = ["μ_write"]

[[constraints.consistency]]
kind = "template"
tag = "IS_BIT"
Expand Down Expand Up @@ -235,10 +256,10 @@ kind = "interaction"
tag = "MEMW"
input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"]
output = "old"
multiplicity = "μ_read"
multiplicity = ["-", "μ_read"]

[[constraints.output]]
kind = "interaction"
tag = "MEMW"
input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"]
multiplicity = "μ_write"
multiplicity = ["-", "μ_write"]
25 changes: 23 additions & 2 deletions spec/src/memw_aligned.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,36 +6,43 @@ name = "MEMW_A"
name = "is_register"
type = "Bit"
desc = "Whether the address represents a register index"
pad = 0

[[variables.input]]
name = "base_address"
type = "DWordWHH"
desc = "The base address to read from/write to. Gets offset by $[0, 7]$ depending on the size of the access"
pad = 0

[[variables.input]]
name = "value"
type = ["BaseField", 8]
desc = "The values to store in memory. For regular memory, these should be (up to) 8 range-checked `Byte`s; registers are stored as two range-checked `Word`s"
pad = 0

[[variables.input]]
name = "timestamp"
type = "DWordWL"
desc = "The timestamp at which this memory access is said to occur"
pad = 0

[[variables.input]]
name = "write2"
type = "Bit"
desc = "Whether to write exactly 2 values"
pad = 0

[[variables.input]]
name = "write4"
type = "Bit"
desc = "Whether to write exactly 4 values"
pad = 0

[[variables.input]]
name = "write8"
type = "Bit"
desc = "Whether to write exactly 8 values"
pad = 0

# Output

Expand All @@ -44,13 +51,15 @@ name = "old"
type = ["BaseField", 8]
desc = """The old value written at `base_address + i`. See `value` for information about representation.
Only the elements corresponding to the `writeN` bits are guaranteed"""
pad = 0
Copy link
Copy Markdown

@claude claude Bot Mar 23, 2026

Choose a reason for hiding this comment

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

Low – Inconsistent padding format for array variable

old has type ["BaseField", 8] but uses scalar pad = 0, while the equivalent variable in memw.toml uses pad = ["arr", 0,0,0,0,0,0,0,0].

Functionally both produce the same zero padding since the tooling doesn't type-check pad against the variable type, but the rendered spec table will show 0 instead of (0,0,0,0,0,0,0,0), which is misleading for readers.

Suggested change
pad = 0
pad = ["arr", 0,0,0,0,0,0,0,0]

Same applies to value (type ["BaseField", 8], line 21) — it also uses scalar 0. Both should use the explicit array form to match the pattern used in memw.toml for array-typed variables.

Copy link
Copy Markdown
Collaborator

@RobinJadoul RobinJadoul Mar 23, 2026

Choose a reason for hiding this comment

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

Constant zero should cast to array form just fine, and is probably easier on the eyes


# Auxiliary

[[variables.auxiliary]]
name = "old_timestamp"
type = "DWordWL"
desc = "The timestamp at which the address was last accessed"
pad = 0

# Virtual

Expand Down Expand Up @@ -78,11 +87,13 @@ def = ["+", "μ_read", "μ_write"]
name = "μ_read"
type = "Bit"
desc = "Whether we are performing a read (and hence return `out`)"
pad = 0

[[variables.multiplicity]]
name = "μ_write"
type = "Bit"
desc = "Whether we are performing a write (and hence not return `out`)"
pad = 0

[[assumptions]]
desc = "`IS_HALF[base_address[i]]`"
Expand Down Expand Up @@ -117,6 +128,16 @@ tag = "IS_HALF"
input = [["+", ["idx", "base_address", 0], "write2", ["*", 3, "write4"], ["*", 7, "write8"]]]
multiplicity = "μ_sum"

[[constraints.consistency]]
kind = "template"
tag = "IS_BIT"
input = ["μ_read"]

[[constraints.consistency]]
kind = "template"
tag = "IS_BIT"
input = ["μ_write"]

[[constraints.consistency]]
kind = "template"
tag = "IS_BIT"
Expand Down Expand Up @@ -200,10 +221,10 @@ kind = "interaction"
tag = "MEMW"
input = ["is_register", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"]
output = "old"
multiplicity = "μ_read"
multiplicity = ["-", "μ_read"]

[[constraints.output]]
kind = "interaction"
tag = "MEMW"
input = ["is_register", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"]
multiplicity = "μ_write"
multiplicity = ["-", "μ_write"]
Loading