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-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.

The onwards is there to avoid making it seem like it's only for this state, i.e. that the transition constraints do carry it forward and it's not a temporary exception.

Added a footnote to hopefully clarify a bit. We don't really have "transition constraints" yet at this point of the expose.

We don't really have "transition constraints" yet at this point of the expose. [...] The onwards is there to avoid making it seem like it's only for this state, i.e. that the transition constraints do carry it forward and it's not a temporary exception.

Should we then not start this section with outlining that, in principal, register values of contiguous states are the same (referring to the state machine description at the start of 35.1.1).
That furthermore allows us to explain why hinting should be included in the first place: to permit exceptions to this rule. And then clarify that indicating a "hint" just means severing this "continuity requirement" for one state transition.

wdyt?

erik-3milabs · 2026-09-22T07:40:09Z

+  `MUL d, a, b`][`FMA d == a * b + (0 * X), hint out`][Multiplication][
+  `INV d, a`][`FMA d == (a + 1) * d - 1, hint <register of d>`][Extension field inversion. Note: `d` and `a` cannot use the same register here, and `d` should not be input-hinted in the next instruction.][
+  `J a`][`FMA PC == a, hint out`][Jump. Can be to a register, memory content, or absolute address, depending on the addressing mode of `a`, even relative to PC][
+  `JZA imm`][`FMA PC == (ZERO)*(-1*PC+(imm-1))+(1*PC+1), hint out`][Jump if ZERO, absolute target address][


A) I'm not exactly sure what you mean here, the notation is meant to imply that in the translation of JZA, the immediate used is modified and not copied as-is.

Let me rephrase.

Denoting -1*PC+(imm-1) in JZA suggests that this argument has the form imm_0 * X + imm_1 - imm_2, where imm_0 = -1, X = PC and imm_2 = 1; it does not cleanly fit the imm_0 * X + imm_1 format

Same holds for JNZA, whose notation suggests that the b-argument has either the form

imm_0 * X + imm_1 - imm_2, with imm_1 = 0, or

imm_0 * X + imm_1 * imm_2, with imm_1 = -1.

B) Ok, I see. Why do you prefer this way of writing over, say,

#table( columns: (auto, auto, auto) [a][b][c] [d][e][f] )

?

erik-3milabs · 2026-09-22T07:53:38Z

+
+Since the VM makes use of read-only memory, traditional usage of a program stack does not work.
+We assume that each function invocation (unless other optimizations apply) will have an associated _frame_,
+pointed to by a _frame pointer_ `fp`, one of the general purpose registers.


What do you think of rephrasing

"... pointed to by a frame pointer ..." to "... pointed to by the frame pointer ...", and

"we assume here that fp is one of the general purpose registers" to "we assume one of the general purpose registers to assume the role of fp"
?

(github doesn't support suggestions on outdated comments :grumble:)

erik-3milabs · 2026-09-22T07:55:24Z

 we perform a _"degree split"_:
-$ f_(i)(x) = f_(i, 0)(x) + x^(d - 1) (f_(i, 1)(x) + x^(d - 2) (f_(i, 2) + x^(d - 2) (f_(i, 3) + ...))), $
+$ f_(i)(x) &= f_(i, 0)(x) + x^(d - 1) (f_(i, 1)(x) + x^(d - 2) (f_(i, 2) + x^(d - 2) (f_(i, 3) + ...)))\
+           &= 1 dot f_(i,0)(x) + x^(d - 1) f_(i,1)(x) + ... + x^(d - 1 + (t - 1) dot (d - 2)) f(i, t)(x), $


Suggested change

&= 1 dot f_(i,0)(x) + x^(d - 1) f_(i,1)(x) + ... + x^(d - 1 + (t - 1) dot (d - 2)) f(i, t)(x), $

&= 1 dot f_(i,0)(x) + x^(d - 1) f_(i,1)(x) + ... + x^(d - 1 + (t - 1) dot (d - 2)) f_(i, t)(x), $

erik-3milabs · 2026-09-22T08:19:49Z

+== 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


We don't really have "transition constraints" yet at this point of the expose. [...] The onwards is there to avoid making it seem like it's only for this state, i.e. that the transition constraints do carry it forward and it's not a temporary exception.

Should we then not start this section with outlining that, in principal, register values of contiguous states are the same (referring to the state machine description at the start of 35.1.1).
That furthermore allows us to explain why hinting should be included in the first place: to permit exceptions to this rule. And then clarify that indicating a "hint" just means severing this "continuity requirement" for one state transition.

wdyt?

erik-3milabs · 2026-09-28T08:25:40Z

+```
+FMA [1 * X + 2] == [3 * Y + 4] * (5 * Z) + [W + 6], hint out + Z
+```


Is this overview supposed to be complete, or just an example? I.e., does Z have an additional sum imm and W a product imm?

Comparing this overview to the below table suggests some of the operations cannot actually be mapped onto this overview.

It's an example where I wanted to highlight some options to simplify notation for the common case of imm_0 ∈ {0,1} or imm_1 = 0

erik-3milabs · 2026-09-28T08:32:16Z

+A state is then the tuple of all values the registers have at a given point in time during the execution.#footnote[
+  If we consider states across different executions, the contents of `MEM` should also be considered part of the state.
+]
+Each instruction acts upon _current state_ to produce the _future state_.#footnote[


Suggested change

Each instruction acts upon _current state_ to produce the _future state_.#footnote[

Each instruction acts upon the _current state_ to produce the _future state_.#footnote[

erik-3milabs · 2026-09-28T08:52:44Z

+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 $1$
+for every consecutive state.


I don't follow the "..., and --- [...] --- is incremented ..."-segment all that well,

I find the comma in the em-dashed sentence hard to read.

what about

Suggested change

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 $1$

for every consecutive state.

The `PC` register stores the program counter: the address of the current instruction.

Almost every instruction increments this value by $1$, except those taking a branch.

or a variation on this?

erik-3milabs · 2026-09-28T09:00:11Z

+By default, a general-purpose register will have the same value the future state
+as it does in the current state.
+To change register values, each general-purpose register in the current state
+can be marked as _hinted_ by the acting instruction.


At the very least:

Suggested change

By default, a general-purpose register will have the same value the future state

as it does in the current state.

To change register values, each general-purpose register in the current state

can be marked as _hinted_ by the acting instruction.

By default, a general-purpose register will have the same value in the future state

The concepts of current and future state only exist in the context of an instruction. I recommend that we either:
i. mention the instruction as context in the first sentence, or
ii. start more generic by using "consecutive states" or "contiguous states".

I don't fully agree on the existence of the states being dependent on an instruction, but I also agree that something like "across consecutive states" probably reads better for the first sentence.

erik-3milabs · 2026-09-29T08:31:53Z

+Here all of `d`, `a`, `b` and `c` are arguments following the addressing scheme described below.
+
+This constraint-based view generally goes well with a read-only memory.
+The memory system gives us that guarantee that whenever we access `MEM` at the same index,


Suggested change

The memory system gives us that guarantee that whenever we access `MEM` at the same index,

The memory system gives us the guarantee that whenever we access `MEM` at the same index,

erik-3milabs · 2026-09-29T08:59:33Z

+the register can take a value that is independent from the previous value,
+except as constrained by the instruction.
+Additionally, the _output_ can be marked as hinted, meaning that the register used in the `d` argument
+will change from the future state onwards, and as such in the `d` argument too.


will change from the future state onwards, and as such in the d argument too.

The use of "as such ... too" suggests that the d argument will change in the future state onwards? Idk, sounds weird.
What about

Suggested change

will change from the future state onwards, and as such in the `d` argument too.

will change from the future state onwards, thus impacting the `d` argument of the current transition.

?

erik-3milabs · 2026-09-29T09:02:27Z

+on the result.
+There may even be situations where hinting multiple values can be chosen simultaneously, such as a decomposition
+$a = b + c$ in a divide-and-conquer algorithm.
+Even hinting registers that are not used in the current instruction may provide useful in limited situations.


Suggested change

Even hinting registers that are not used in the current instruction may provide useful in limited situations.

Even hinting registers that are not used in the current instruction may prove useful in limited situations.

erik-3milabs · 2026-09-29T09:17:51Z

+implementers and practitioners are encouraged to discover and use their own,
+as experience may point out further useful abstractions.
+
+#table(columns: (auto, 2fr, 1fr),


omitting my comments on this table, as those are being discussed in our chat.

erik-3milabs · 2026-09-29T09:33:28Z

+We again make use of the multiplexing machinery from before.
+The constraints we want to enforce on a register index $r$ are as follows:
+- $!next("hint_input")_r and !#`hint_output` => next("registers")_r = #`registers`_r$,\ `r` could not have been hinted,
+  since it was not input-hinted in the next row, and there was no output hint, so the next `r` should remain the same.


Suggested change

since it was not input-hinted in the next row, and there was no output hint, so the next `r` should remain the same.

since it was not input-hinted in the next row, and there was no output hint, so `r'` should remain the same.

erik-3milabs · 2026-09-29T09:37:54Z

+# PARAM: $limits(sum)_(j = 0)^T #`arg_register_powers`_(i,j) dot limits(sum)_(k = 0)^(d - 1) #`argument_registers`_i^k dot #`RANGE`_(j,k)$
+constraint = "$limits(sum)_(j = 0)^1 #`arg_register_powers`_(i,j) dot limits(sum)_(k = 0)^4 #`argument_registers`_i^k dot #`RANGE`_(j,k)$"


Missing = 0?

erik-3milabs

my remaining remarks are so minor, that I think this is ready to be merged!

erik-3milabs · 2026-09-30T06:47:53Z

+  ([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [], [@decode:note:word_instr, <note_signed>]),
+  ([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [@decode:note:word_instr, <note_signed>]),


Suggested change

([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [], [@decode:note:word_instr, <note_signed>]),

([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [@decode:note:word_instr, <note_signed>]),

([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [], [@decode:note:word_instr@decode:note:signed]),

([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [@decode:note:word_instr@decode:note:signed]),

erik-3milabs · 2026-09-30T06:56:56Z


+#let notelist(prefix, body) = {
+  show figure.where(kind: "note"): it => {
+    super(it.counter.display(it.numbering)) + box(it)


this box(it) doesn't seem to do much here

erik-3milabs · 2026-09-30T07:13:37Z

on the pdf, address overflows to the next line. Maybe break here and put // address on the next line?

erik-3milabs · 2026-09-30T07:15:00Z

  show math.equation.where(block: false): box // Don't line-break inline equations by default
  show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label")
+  show ref: it => if it.element != none and it.element.func() == figure and it.element.kind == "note" {
+    super[[#it]]


indeed curious that it does not include the brackets from the numbering here...

github-actions · 2026-09-30T08:10:32Z

Kimi Code Review

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

Automated review by Kimi (Moonshot AI)

github-actions · 2026-09-30T08:11:33Z

Codex Code Review

No actionable issues found in the PR diff. The specification validator passes. Changes are limited to specification documents and tooling; no Rust runtime code changed.

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

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

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

RobinJadoul self-assigned this Sep 8, 2026

erik-3milabs reviewed Sep 10, 2026

View reviewed changes

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

erik-3milabs reviewed Sep 18, 2026

View reviewed changes

erik-3milabs added the spec Updates and improvements to the spec document label Sep 21, 2026

RobinJadoul force-pushed the spec/recursion.vm branch from 38faf79 to a06c369 Compare September 21, 2026 09:17

RobinJadoul requested a review from erik-3milabs September 21, 2026 09:59

erik-3milabs reviewed Sep 22, 2026

View reviewed changes

RobinJadoul requested a review from erik-3milabs September 25, 2026 14:09

RobinJadoul force-pushed the spec/recursion.vm branch from f43e542 to d9af179 Compare September 25, 2026 14:12

erik-3milabs reviewed Sep 29, 2026

View reviewed changes

erik-3milabs approved these changes Sep 30, 2026

View reviewed changes

RobinJadoul marked this pull request as ready for review September 30, 2026 08:10

Base automatically changed from spec/recursion to spec/main October 2, 2026 12:14

RobinJadoul and others added 9 commits October 2, 2026 14:27

Field VM, first edition

e0eaf91

Silly oversights

2b82d95

Typechecker working for opaque types (as generalization of ExtField)

423772e

Make ruff happier

3a8cafc

Various fixes

08bf6d5

Fix input hinting constraints to take hint_input from the next row

188524b

Apply batched suggestions from code review

843a96e

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

Improve expression rendering

a6cbfb3

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

8458648

RobinJadoul and others added 24 commits October 2, 2026 14:27

Rename o register to d

6ca44a0

More elaborate VM architecture to intro

1230403

Instructions vs states

cf1da6b

Registers and hinting

82c4035

pseudoinstructions as a table

8b41451

Clarify negative offsets into frame

8615d8e

clarify syntactic degree being too high for mux

8b477de

typo

9c0230c

Switch everything to next(...) notation

0ac326e

Compression in the decode lookup

ab4e1a4

padding

3662069

Decode table

b1b2119

Minor

d5f771b

Don't line-break inline equations by default

ba642a9

deg notation

dea79f8

Apply batched suggestions from code review

abbd403

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>

Clarify some writing

8713c60

Comments on CALL/RET

580040c

Expand degree split differently

0e200e7

review

e93fc96

review

511b79d

Notelist

09f66f9

HTML support for notelist

dcc4707

Cleanup from review

e5e4cd8

RobinJadoul force-pushed the spec/recursion.vm branch from ce9be50 to e5e4cd8 Compare October 2, 2026 12:27

RobinJadoul merged commit 41c3af9 into spec/main Oct 2, 2026
2 checks passed

RobinJadoul deleted the spec/recursion.vm branch October 2, 2026 12:28

erik-3milabs mentioned this pull request Oct 14, 2026

Discussion: split proving implementation #1019

Draft

	&= 1 dot f_(i,0)(x) + x^(d - 1) f_(i,1)(x) + ... + x^(d - 1 + (t - 1) dot (d - 2)) f(i, t)(x), $
	&= 1 dot f_(i,0)(x) + x^(d - 1) f_(i,1)(x) + ... + x^(d - 1 + (t - 1) dot (d - 2)) f_(i, t)(x), $

	Each instruction acts upon _current state_ to produce the _future state_.#footnote[
	Each instruction acts upon the _current state_ to produce the _future state_.#footnote[

	The memory system gives us that guarantee that whenever we access `MEM` at the same index,
	The memory system gives us the guarantee that whenever we access `MEM` at the same index,

	Even hinting registers that are not used in the current instruction may provide useful in limited situations.
	Even hinting registers that are not used in the current instruction may prove useful in limited situations.

	since it was not input-hinted in the next row, and there was no output hint, so the next `r` should remain the same.
	since it was not input-hinted in the next row, and there was no output hint, so `r'` should remain the same.

		# PARAM: $limits(sum)_(j = 0)^T #`arg_register_powers`_(i,j) dot limits(sum)_(k = 0)^(d - 1) #`argument_registers`_i^k dot #`RANGE`_(j,k)$
		constraint = "$limits(sum)_(j = 0)^1 #`arg_register_powers`_(i,j) dot limits(sum)_(k = 0)^4 #`argument_registers`_i^k dot #`RANGE`_(j,k)$"

		([`DIV[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [], [@decode:note:word_instr, <note_signed>]),
		([`REM[U][W] rd, rs1, rs2`], [`DIVREM`], [`[W]`], [#sym.not`[U]`], [`muldiv_selector`], [@decode:note:word_instr, <note_signed>]),

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!

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!

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!

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!

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!