spec: Recursion

[erik-3milabs]

No description provided.

[github-actions]

Kimi Code Review

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

---

Automated review by Kimi (Moonshot AI)

[github-actions]

Codex Code Review

• Medium — Recursive verification omits the required commitment (spec/recursion.typ:105). verify accepts a commitmentSpace, but the recursive branch treats commitment_1 as a function; lines 116–118 similarly pass verifier functions directly. Use an explicitly defined specialization operation producing comm(verify'(commitment_0, commitment_1, ·)). As written, the equations are ill-typed and do not establish the claimed recursive chain.

[cdesaintguilhem]

Mostly minor comments!

[RobinJadoul]

I'm wondering whether we should choose for the $f$ function in the proof system to be the ELF proof, or if it should purely be the VM itself, and moving the ELF into public inputs.

[RobinJadoul]

Not paying attention to all possible typography yet, trying to get the last high-level stuff out of the way
I'll try to do another pass later this week, but this is a first go at it

[RobinJadoul]

A couple minor things, but looking better and better.
Probably good to have another review pass by @cdesaintguilhem around this point, too.

[RobinJadoul]

This would need to define $d_{v^*}$, presumably in terms of $d_v$, as part of the definition of the split, I think.

[erik-3milabs]

done.

[RobinJadoul]

We might even make the definition of a split into a triple (v_0, v_1, d_v).
This gets rid of the existential quantifier, and makes it explicit where everything comes from when we get to here

[RobinJadoul]

As discussed, there's indeed a subtlety about non-generator records.
We probably need to split up the arrows so that we get

• completeness: $v(x) = 1 \implies v_0(x, d(x)) = 1 \wedge v_1(x, d(x)) = 1$
• soundness: $\forall r. v_0(x, r) = 1 \wedge v_1(x, r) = 1 \implies v(x) = 1$

[erik-3milabs]

fixed

[cdesaintguilhem]

I've read until, but not including, "34.4 Split-recursion". See typos and aesthetic remark in comments, otherwise everything reads very nicely up until then!

[cdesaintguilhem]

Some more nits and notation comments, but otherwise looks good to me.

[github-actions]

Kimi Code Review

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

---

Automated review by Kimi (Moonshot AI)