Skip to content

spec: Typecheck padding #670

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

Open
RobinJadoul wants to merge 9 commits into
base: spec/main
Choose a base branch
from
+219 −149
Open

spec: Typecheck padding #670

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
6b9e38d
Check padding for structure/type. Closes #351 and #634
RobinJadoul Jun 15, 2026
f027614
Check padding satisfies as many constraints as we can reasonably check
RobinJadoul Jun 16, 2026
6f500eb
Avoid crashing on runs that don't check all chips
RobinJadoul Jun 16, 2026
f089adf
Turn push_context into a context manager
RobinJadoul Jun 16, 2026
ae425a0
Check that no template cond is given when it isn't possible
RobinJadoul Jun 16, 2026
6566701
rename type_match to typecheck_binop
RobinJadoul Jun 16, 2026
dc81fbc
Cleanup some signatures
RobinJadoul Jun 16, 2026
c537134
Rework template_checkers recursion
RobinJadoul Jun 16, 2026
955febd
Simpler DVRM padding
RobinJadoul Jun 19, 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
2 changes: 1 addition & 1 deletion spec/dvrm.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,5 +144,5 @@ Lastly, this chip contributes the following to the lookup:
#render_constraint_table(chip, config, groups:("output", ))

= Padding
To pad the #dvrm table, we use the following data, representing the unsigned division $frac(0, 0, style: "horizontal")$:
To pad the #dvrm table, we use the following data:
#render_chip_padding_table(chip, config)
6 changes: 3 additions & 3 deletions spec/src/commit.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,19 +18,19 @@ pad = 0
name = "address"
type = "DWordWL"
desc = "Address of first byte to commit."
pad = ["arr", 0, 0, 0, 0]
pad = 0

[[variables.auxiliary]]
name = "address_incr"
type = "DWordHL"
desc = "$#`address` + 1$"
pad = ["arr", 1, 0, 0, 0]
pad = 1

[[variables.auxiliary]]
name = "count"
type = "DWordWL"
desc = "number of bytes to commit"
pad = ["arr", 1, 0, 0, 0]
pad = 1

[[variables.auxiliary]]
name = "count_decr"
Expand Down
2 changes: 1 addition & 1 deletion spec/src/cpu.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ pad = 0
name = "half_instruction_length"
type = "Byte"
desc = "Half the number of bytes consumed by this instruction, commonly used to indicate whether the instruction is of C type, i.e., whether it is 2 bytes long (= 1) instead of 4 (= 2)"
pad = 2
pad = 0

[[variables.input]]
name = "word_instr"
Expand Down
2 changes: 1 addition & 1 deletion spec/src/dvrm.toml
View file
Open in desktop
Comment thread
erik-3milabs marked this conversation as resolved.
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ pad = 0
name = "div_by_zero"
type = "Bit"
desc = "Whether $#`d`=0$."
pad = 1
pad = 0

[[variables.auxiliary]]
name = "overflow"
Expand Down
24 changes: 12 additions & 12 deletions spec/src/sha256round.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,18 +126,6 @@ type = "Word"
desc = "`w[index]`"
pad = 0

[[variables.virtual]]
name = "carry_a"
type = "Byte"
desc = "The carry from `out_a`"
def = ["*", ["^", 2, -32], ["-", ["+", "temp1", "temp2"], ["cast", "out_a", "Word"]]]

[[variables.virtual]]
name = "carry_e"
type = "Byte"
desc = "The carry from `out_e`"
def = ["*", ["^", 2, -32], ["-", ["+", "d", "temp1"], ["cast", "out_e", "Word"]]]

[[variables.virtual]]
name = "ch"
type = "Word"
Expand All @@ -162,6 +150,18 @@ type = "BaseField"
desc = "`temp2` value"
def = ["+", "S0", "maj"]

[[variables.virtual]]
name = "carry_a"
type = "Byte"
desc = "The carry from `out_a`"
def = ["*", ["^", 2, -32], ["-", ["+", "temp1", "temp2"], ["cast", "out_a", "Word"]]]

[[variables.virtual]]
name = "carry_e"
type = "Byte"
desc = "The carry from `out_e`"
def = ["*", ["^", 2, -32], ["-", ["+", "d", "temp1"], ["cast", "out_e", "Word"]]]

[[variables.multiplicity]]
name = "μ"
type = "Bit"
Expand Down
Loading
Loading