spec: Typecheck padding

[RobinJadoul]

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]

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]

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]

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

[RobinJadoul]

Encoding 0/1 = 0 then?

[RobinJadoul]

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

[erik-3milabs]

Not a fan of the walrus here.

Suggested change

	chips.append(chip := Chip.from_file(config, file))
	chip = Chip.from_file(config, file)
	chips.append(chip)

[erik-3milabs]

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.

[RobinJadoul]

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

[erik-3milabs]

Given that var_name is passed in to be solely passed on to reporter, consider passing it in through reporter.context to give this function a cleaner signature.

[erik-3milabs]

Can we do something about the names typecheck, type_match and Type?
To me, typecheck suggests a function with boolean output (fail/pass), but instead it returns an object of type Type (another stumbling block), which is actually an evaluation of sorts.
I also never know what the difference between typecheck and type_match are supposed to be.

[RobinJadoul]

This is using type checking as the act of assigning types to expressions. While technically the correct term for this may actually be typing, that feels more confusing to me.
Type being a type is kinda inherent to the reification of types that you need in a context like this.

type_match is more of a local thing for individual kinds of expression, that may have a different name possible. Where it is used, it's doing essentially some combination of type coercion to make operands compatible and computing the type for the combination of the result. The reason it's separate from the typecheck method in those places is because there's a variadic number of operands in those expressions, and we collapse them with a fold. Maybe typecheck_binary is a replacement name?