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 8 commits into
base: spec/main
Choose a base branch
from
+218 −148
Open

spec: Typecheck padding #670

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 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
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
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

@erik-3milabs erik-3milabs Jun 16, 2026

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.

I agree that the padding is invalid.
The proposed solution works.
A cleaner solution might be to have div_by_zero = 0.

@RobinJadoul RobinJadoul Jun 16, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

Encoding 0/1 = 0 then?

@RobinJadoul RobinJadoul Jun 16, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

Aha, the downside is that it makes the NEG workaround no longer work, because then we have NEG<1, signed>

Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ pad = 0
name = "q"
type = "DWordHL"
desc = "The quotient; $#`n` / #`d`$ rounded towards zero."
pad = 0
pad = ["arr", 65535, 65535, 65535, 65535]

[[variables.output]]
name = "r"
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