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

erik-3milabs · 2026-09-09T11:58:29Z

+The central instruction of the ISA is a constraint for a fused multiply-add over the extension field:
+`FMA o == a * b + c`.
+Here all of `o`, `a`, `b` and `c` are arguments following the addressing scheme described below.


Reading this section, I've noticed that this o is easy to misinterpret. Also, o and just o are hardly distinguishable. Would it be an idea to rename this as d (for "destination")? I also considered r for "result", but that also overlaps with "register" so that might not be the greatest...

"The central instruction of the ISA is a constraint"

We could (and maybe should?) spend a full paragraph unpacking the meaning of this single phrase. Starting with the purpose of this VM: verifying a proof. In other words, this VM doesn't need to really produce anything (like traditional programs), but rather just needs to check that a string has an acceptable format, by performing loads of assertions. (We do have some typical instructions, but those are to writeable registers only, and meant to reduce proof size.)

erik-3milabs · 2026-09-09T12:16:57Z

+The central instruction of the ISA is a constraint for a fused multiply-add over the extension field:
+`FMA o == a * b + c`.
+Here all of `o`, `a`, `b` and `c` are arguments following the addressing scheme described below.
+The field VM uses only read-only memory, which is implemented as a committed table,


Suggested change

The field VM uses only read-only memory, which is implemented as a committed table,

The field VM only uses read-only memory, which is implemented as a committed table,

or

Suggested change

The field VM uses only read-only memory, which is implemented as a committed table,

The field VM uses read-only memory only, which is implemented as a committed table,

or something else that bypasses the double "only"

erik-3milabs · 2026-09-09T12:24:12Z

+The central instruction of the ISA is a constraint for a fused multiply-add over the extension field:
+`FMA o == a * b + c`.
+Here all of `o`, `a`, `b` and `c` are arguments following the addressing scheme described below.
+The field VM uses only read-only memory, which is implemented as a committed table,


this does not mention the existence of writeable registers.

erik-3milabs · 2026-09-09T15:27:07Z

+
+[[constraints.memory]]
+kind = "arith"
+constraint = "$!#`mem_flags[i]` => #`args[i]` = #`args_premem[i]`$"


general note: why do we use ! to indicate the not-gate in this spec, when there is ¬?

I'm not sure; I initially wrote not there, but we'd used ! in the past, so I went for consistency.

erik-3milabs · 2026-09-10T08:09:54Z

    },
+    "next": (pp, rec, e) =>  {
+      assert(e.len() == 2 and type(e.at(1)) == str, message: "Invalid transition variable: " + repr(e))
+      cwrap($#rec(PREC.next, e.at(1))'$, pp < PREC.next)


why cwrap instead of mwrap? (I see now that "cast" also uses cwrap here, which is also confusing)

Uhh, copy-paste problems, I'm assuming

erik-3milabs · 2026-09-10T08:15:26Z

-  "add": 10,  // +  
-  "eq": 11,   // = and :=
-  "MAX": 12, // <the void outside every expression>
+  "next": 3, // var'


I'm noticing that [idx, [next, var], i] is expressed as $(var')_i$, where I would expect that $var'_i$ would also be acceptable. In fact, the added parentheses make reading the formula look bloated.

do you agree that the added parentheses are undesirable?

should we perhaps move the idx code to 3 (after next)? I'm not expecting we'll be indexing on a pow or a neg any time soon.

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

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

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>

	The field VM uses only read-only memory, which is implemented as a committed table,
	The field VM only uses read-only memory, which is implemented as a committed table,

	The field VM uses only read-only memory, which is implemented as a committed table,
	The field VM uses read-only memory only, which is implemented as a committed table,

Uh oh!

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!

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!

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants