spec: Typecheck padding by RobinJadoul · Pull Request #670 · yetanotherco/lambda_vm

RobinJadoul · 2026-06-16T11:20:40Z

This manages to catch both the observed issue with the CPUs padding for half_instruction_length and an previously unknown issue in the padding for DVRM.

github-actions · 2026-06-16T11:23:14Z

Codex Code Review

No issues found in the PR diff.

I reviewed the changed TOML padding values and the new recursive padding/template checker in spec/tooling/chip.py. I also ran:

python spec/tooling/chip.py spec/src/config.toml spec/src/signatures.toml spec/src/*.toml

It completed with No issues were found.

claude · 2026-06-16T11:24:33Z

Review: spec/typecheck-padding

Summary

This PR introduces type-checking for padding values in chip specs, fixing two concrete bugs:

half_instruction_length had pad 2 (incorrect) → now 0
q in DVRM had pad 0 (incorrect for a 4-element array type) → now ["arr", 65535, 65535, 65535, 65535]

It also reorders carry_a/carry_e in sha256round so they appear after temp1/temp2 (which they depend on), required by the new populate_env ordering contract.

The overall approach is sound. Two issues worth addressing:

Issues

Medium – Signature.matches ignores the new condition field (see inline)
The field is populated via build_signature and InteractionLike.typecheck, but matches never compares it. If condition types are intentionally excluded from structural matching, a comment explaining why would prevent future confusion.

Medium – Unhandled KeyError in check_assignment (see inline)
check_template[sig.tag] will crash with a Python traceback for any unknown template tag. Since tags come from TOML files, a typo would produce an unguarded exception instead of a reporter.error. It also leaves the context stack dirty (push without pop) which corrupts subsequent error locations.

Minor notes

The push_context/pop_context pattern appears in several places without try/finally. This is fine as long as reporter.error never raises — but the KeyError above shows a case where it can. Worth keeping in mind as the checker grows.
The workaround comment in CastExpr.typecheck ("This may become cleaner if we eventually get to the cast rework from spec: Tighter range checks #326") is a good breadcrumb; no action needed now.

erik-3milabs · 2026-06-16T12:11:47Z

            continue
-        chips.append(Chip.from_file(config, file))
+        chips.append(chip := Chip.from_file(config, file))
+        template_checkers[chip.name] = template_checker(template_checkers, chip)


this recursion is trippy: to set template_checkers[some chip]: Callable, it passes in all of template_checkers, which gets bound (?) into a function which is then returned?

This, I believe, requires proper documentation, either directly here, or by wrapping this in a well-named function and documenting that function. I cannot make heads or tails of what is happening here, nor what template_checkers even means / is supposed to do.

template_checkers is a collection of functions, indexed by template name/tag, that checks whether a given assignment satisfies the template.

Passing in template_checkers could be delayed to the invocations of these checkers as well, we're just tying the knot a bit earlier here.
We need to pass template_checkers to an individual checker somewhere to be able to deal with templates inside of a template definition (such as IS_BIT inside of ADD).
The downside of delaying the access to all templates to later is that the typing of template_checkers itself needs to become recursive, since now the Callable needs an argument of the type dict[str, Callable[dict[...], Optional[Type], ...]. Which could in itself work out

Hmmm.

Having reviewed again, I'm not convinced the recursion is the best way to go. Why not introduce a check_assignment for templates and have a (global?) tag_to_chip map?
Then the last part on check_assignment on chips would look something like this:

Suggested change

template_checkers[chip.name] = template_checker(template_checkers, chip)

for c in self.constraints:

with reporter.context(repr(c)):

all_signatures = c.typecheck(env)

templates = filter(lambda s: isinstance(s, TemplateSignature))

for sig in templates:

tag_to_chip[sig.tag].check_assignment(sig)

which I find a lot easier to read.

I don't see a big difference, besides now getting a global variable that I don't love having to setup if we ever do end up using this as a "library" for potential other tooling.

The one other difference is that now check_assignment takes a Signature, which I find to not as cleanly represents what an assignment should be. Perhaps there's a way to decompose it into something that maps sig into an assignment given only the chip and then chaining a check_assignment — which is currently encoded in the template checker.

Aha, and after a quick attempt at implementation, another downside appears: we can't easily have this mapping for SUB, which needs to rearrange some things before passing it on to the logic for ADD.
So the replacement would end up being a map from tag to (chip, extractor) where extractor needs to give you the assignment for a signature, which is comparable to the current approach, but now implemented as a suggestion.

Now simplified after stacking the PR on top of #695

erik-3milabs · 2026-06-22T10:32:07Z

+    def check_assignment(
+        self,
+        template_checkers: dict[str, "TemplateChecker"],
+        values: Optional[dict[str, Type]] = None,
+    ):


Rather than having check_assignment default to checking the padding when no values are provided, I'd instead propose introducing check_padding which calls check_assignment on the padding.

Also: should we additionally verify that self.variables INSECTION values.keys() = self.variables? That way we can strain out assignments that propose setting non-existent variables.

erik-3milabs · 2026-06-22T12:02:18Z

+        for c in self.constraints:
+            for sig in c.typecheck(env):
+                # Recurse on templates
+                if isinstance(sig, TemplateSignature) and sig.tag in template_checkers:


what if sig.tag not in template_checkers? Wouldn't that indicate a bug?

Not really, we could be checking a chip in isolation and not invoking chip.py with all templates present

Should we at least have the reporter mention this? Not as an issue, but at least as an heads up.

Perhaps, yeah. Added

erik-3milabs · 2026-06-22T12:12:19Z

+type TemplateChecker = Callable[[dict[str, TemplateChecker], Optional[Type], list[Type], Optional[Type]], None]
+
+def build_template_checker(chip: Chip) -> TemplateChecker:
+    def check(template_checkers: dict[str, TemplateChecker], cond: Optional[Type], input: list[Type], output: Optional[Type]) -> None:


Consider passing in sig: TemplateSignature rather than decomposing it into cond, input and output.

erik-3milabs · 2026-06-22T12:42:14Z

            continue
-        chips.append(Chip.from_file(config, file))
+        chips.append(chip := Chip.from_file(config, file))
+        template_checkers[chip.name] = template_checker(template_checkers, chip)


Hmmm.

Having reviewed again, I'm not convinced the recursion is the best way to go. Why not introduce a check_assignment for templates and have a (global?) tag_to_chip map?
Then the last part on check_assignment on chips would look something like this:

Suggested change

template_checkers[chip.name] = template_checker(template_checkers, chip)

for c in self.constraints:

with reporter.context(repr(c)):

all_signatures = c.typecheck(env)

templates = filter(lambda s: isinstance(s, TemplateSignature))

for sig in templates:

tag_to_chip[sig.tag].check_assignment(sig)

which I find a lot easier to read.

RobinJadoul added 2 commits June 15, 2026 15:27

Check padding for structure/type. Closes #351 and #634

6b9e38d

Check padding satisfies as many constraints as we can reasonably check

f027614

RobinJadoul requested a review from erik-3milabs June 16, 2026 11:20

RobinJadoul self-assigned this Jun 16, 2026

RobinJadoul added the spec Updates and improvements to the spec document label Jun 16, 2026

Avoid crashing on runs that don't check all chips

6f500eb

claude Bot reviewed Jun 16, 2026

View reviewed changes

Comment thread spec/tooling/chip.py

claude Bot reviewed Jun 16, 2026

View reviewed changes

Comment thread spec/tooling/chip.py Outdated

RobinJadoul added 2 commits June 16, 2026 13:33

Turn push_context into a context manager

f089adf

Check that no template cond is given when it isn't possible

ae425a0

erik-3milabs reviewed Jun 16, 2026

View reviewed changes

RobinJadoul added 3 commits June 16, 2026 15:41

rename type_match to typecheck_binop

6566701

Cleanup some signatures

dc81fbc

Rework template_checkers recursion

c537134

RobinJadoul requested a review from erik-3milabs June 16, 2026 15:16

Simpler DVRM padding

955febd

erik-3milabs reviewed Jun 22, 2026

View reviewed changes

Different separation of concerns attempt

8d73916

RobinJadoul requested a review from erik-3milabs June 22, 2026 13:36

RobinJadoul added 3 commits June 22, 2026 16:52

Warn about unavailable templates

c0cad81

Merge branch 'spec/explicit-sub' into spec/typecheck-padding

357756f

Simplify having SUB as a full template

859d5af

RobinJadoul changed the base branch from spec/main to spec/explicit-sub June 22, 2026 15:42

-        template_checkers[chip.name] = template_checker(template_checkers, chip)
+        for c in self.constraints:
+            with reporter.context(repr(c)):
+                all_signatures = c.typecheck(env)
+                templates = filter(lambda s: isinstance(s, TemplateSignature))
+                for sig in templates:
+                    tag_to_chip[sig.tag].check_assignment(sig)

Conversation

RobinJadoul commented Jun 16, 2026

Uh oh!

github-actions Bot commented Jun 16, 2026

Codex Code Review

Uh oh!

Uh oh!

Uh oh!

claude Bot commented Jun 16, 2026

Review: spec/typecheck-padding

Summary

Issues

Minor notes

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!

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants