spec: Field VM by RobinJadoul · Pull Request #971 · yetanotherco/lambda_vm

RobinJadoul · 2026-09-08T15:18:29Z

No description provided.

github-actions · 2026-09-08T15:18:43Z

Kimi Code Review

⚠️ Review failed: Kimi API request failed with status 401

Automated review by Kimi (Moonshot AI)

github-actions · 2026-09-08T15:19:48Z

Codex Code Review

Found five issues in the changed specification/tooling:

High — Register preservation is missing (field_vm.toml:174). The polynomial constrains pc' - (pc + 1) instead of registers'[i] - registers[i]. When hint_output = 1, unrelated registers can change freely; ordinary jumps are also forced to fall through. Use the register difference shown in the accompanying constraint.
High — FMA polynomial implements multiplication of three operands (field_vm.toml:156). It enforces o = a * b * c, rather than o = a * b + c. Move args[3] outside the multiplication. For example, the documented MUL expansion has c = 0, so this polynomial forces its result to zero.
Medium — New type breaks specification validation (config.toml:11). ExtField references itself before being registered. Running the checker fails immediately with Couldn't lookup type by name: 'ExtField'. Add explicit extension-field support or a supported representation.
Medium — Register multiplexing has invalid references (field_vm.toml:85). The power wrapper uses arg_reg_pows_computed[j][j-1] instead of [i][j-1], sharing argument 1’s power across all operands. Additionally, MUX has six entries but is indexed through six inclusive, and the power constraint references undefined arg_registers. Correct these to preserve register selection.
Medium — PC transition polynomial contains an unbound index (field_vm.toml:187). This constraint uses i without an iterator and incorrectly includes hint_input[i]. Remove that factor and use MUX[1], matching the stated PC-selector constraint.

RobinJadoul · 2026-09-08T15:26:54Z

Getting the typechecker to be happy with ExtField elements is one of the next steps ;)

erik-3milabs

Summary:

instruction and constraints are similar, but not the same. Sketching the right mental model is informative.
an instruction spans multiple states, which is a new concept in this spec. The reader is not helped to understand this. Sketching the right mental model is informative.
the concepts of input hinting, output hinting and register hinting and their relation is unclear.
have another look at the lower and upper bounds of sum. There seem to be some issues with that.
minor notes/rephrase proposals

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

erik-3milabs · 2026-09-18T12:14:06Z

+[[variables.input]]
+name = "hint_input"
+type = ["Bit", 5] # PARAM: ["Bit", N]
+desc = "Whether each input register is hinted this cycle"


Suggested change

desc = "Whether each input register is hinted this cycle"

desc = "Whether each general purpose register is input hinted this cycle"

?

erik-3milabs · 2026-09-18T12:15:06Z

consider adding

#show math.equation.where(block: false): box

as I find equations line breaking, which is rather annoying imo.

erik-3milabs · 2026-09-18T12:15:37Z

+The `ZERO` register indicates whether the previous instruction had a zero result,
+i.e. $next("ZERO") <=> #`d` = 0$.
+The `PC` register stores the program counter: the address of the current instruction,
+and --- except when branches are taken, through register hinting --- is incremented by one


Suggested change

and --- except when branches are taken, through register hinting --- is incremented by one

and --- except when branches are taken, through register hinting --- is incremented by $1$

?

erik-3milabs · 2026-09-18T12:17:22Z

+== Register hinting
+
+Each general-purpose register in the current state can be marked as _hinted_ by the acting instruction.
+This means that from the current state onwards, the register can take a value


why are you choosing "onwards" here? It suggests that if for one instruction you set a register to hintable, and it remains that way for the rest of the execution trace. Perhaps worth clarifying that this is a way for the transition constraint not to hold for that particular instruction.

erik-3milabs · 2026-09-18T12:17:35Z

+
+In contrast, input hinting does not look like any traditional model of execution,
+instead allowing to update one or more values in the state, as long as the resulting state still satisfies
+the FMA constraint.


Suggested change

the FMA constraint.

the `FMA` constraint.

erik-3milabs · 2026-09-18T12:37:52Z

+and used through the `MUX` constant columns.
+In this way, $f_(i, 0)$ can have degree at most $d - 2$, as it gets multiplied with $#`imm`_0$ and the register value,
+and the other $f_(i, k)$ can have degree at most $d - 3$, as they also get multiplied with the appropriate power of $x$.
+This leads to a total degree of $op("deg") f_(i) = d - 1 + t dot (d - 2) - 1$ for a maximal number of registers $N + 2 <= op("deg") f_(i) + 1$.


is there a reason you're not simplifying this to (t+1)(d-2)?

erik-3milabs · 2026-09-18T12:58:30Z

+For `argument_registers` however, which should be in the range $[0, N + 1]$,
+which upon first attempt cannot be checked with a constraint of degree $<= d$.


this double "which" is confusing

erik-3milabs · 2026-09-18T12:58:30Z

+the decoding table to reduce its number of columns.
+Doing so would require the elements being combined into one column to be range checked on this side
+of the interaction, ideally without needing any extra interactions or committed columns.
+For `Bit` variables, this is no problem with the `IS_BIT` template from @isbit.


Does 1 not have different square roots in the extension field other than itself?

erik-3milabs · 2026-09-18T12:59:39Z

+the decoding table to reduce its number of columns.
+Doing so would require the elements being combined into one column to be range checked on this side
+of the interaction, ideally without needing any extra interactions or committed columns.
+For `Bit` variables, this is no problem with the `IS_BIT` template from @isbit.


does 1 not have another square root in the extension field?

erik-3milabs · 2026-09-18T13:08:07Z

+
+Besides enforcing the FMA constraints and the correct transitions between states, we also need to ensure that execution
+starts at the correct instruction and ends with a halting instruction.
+This means that the verifier must check that the first row of the table corresponds to a state at `PC = 1` and all other variables set to $0$;


Shouldn't we introduce a "first-row" indicator row to make this a constraints? Otherwise, how is the verifier going to do this? The prover can only open elements in the codeword, but that is blown-up + shifted compared to the original table.

Field VM, first edition

03131e5

RobinJadoul requested a review from erik-3milabs September 8, 2026 15:18

RobinJadoul self-assigned this Sep 8, 2026

Silly oversights

c4b58ab

RobinJadoul added 4 commits September 8, 2026 18:24

Typechecker working for opaque types (as generalization of ExtField)

d5644dd

Make ruff happier

8339204

Various fixes

29f0a57

Fix input hinting constraints to take hint_input from the next row

cba7504

erik-3milabs reviewed Sep 10, 2026

View reviewed changes

RobinJadoul and others added 15 commits September 10, 2026 12:03

Apply batched suggestions from code review

49d4cf8

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>

Improve expression rendering

47a2a04

Field is not a code-term in the titles, imo

72c7c70

Rename o register to d

14ea6b6

More elaborate VM architecture to intro

186a681

Instructions vs states

c447faa

Registers and hinting

09e64be

pseudoinstructions as a table

0ed78ce

Clarify negative offsets into frame

c49f796

clarify syntactic degree being too high for mux

f014a2e

typo

fae3ab7

Switch everything to next(...) notation

1fbfdd8

Compression in the decode lookup

f3f282f

padding

b9f4134

Decode table

3b942fe

RobinJadoul requested a review from erik-3milabs September 17, 2026 12:12

Minor

38faf79

erik-3milabs reviewed Sep 18, 2026

View reviewed changes

	desc = "Whether each input register is hinted this cycle"
	desc = "Whether each general purpose register is input hinted this cycle"

	and --- except when branches are taken, through register hinting --- is incremented by one
	and --- except when branches are taken, through register hinting --- is incremented by $1$

		For `argument_registers` however, which should be in the range $[0, N + 1]$,
		which upon first attempt cannot be checked with a constraint of degree $<= d$.

Conversation

RobinJadoul commented Sep 8, 2026

Uh oh!

github-actions Bot commented Sep 8, 2026

Kimi Code Review

Uh oh!

github-actions Bot commented Sep 8, 2026

Codex Code Review

Uh oh!

RobinJadoul commented Sep 8, 2026

Uh oh!

erik-3milabs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

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