diff --git a/spec/book.typ b/spec/book.typ new file mode 100644 index 000000000..847730933 --- /dev/null +++ b/spec/book.typ @@ -0,0 +1,236 @@ +#import "@preview/shiroa:0.3.1": * +#import "/templates/page.typ": project +#import "@preview/equate:0.3.2": equate + +#show: book + +#let meta = ( + title: "Lambda VM specification", + authors: ("3MI Labs", "Aligned"), + version: "0.2", + summary: ( + ("PROOF SYSTEM", ( + ("logup.typ", [`LogUp` argument], ), + ("memory.typ", [Memory argument], ), + ("streaming.typ", [Streaming prover], ), + ("verifier.typ", [Verification], ) + )), + ("OVERVIEW", ( + ("variables.typ", [Variables], ), + ("signatures.typ", [Signatures], ), + )), + ("TEMPLATES", ( + ("is_bit.typ", [`IS_BIT` template], ), + ("is_byte.typ", [`IS_BYTE` template], ), + ("sign.typ", [`SIGN` template], ), + ("add.typ", [`ADD`/`SUB` template], ), + ("neg.typ", [`NEG` template], ), + ("reg.typ", [`REG`/`REGW` template], ), + )), + ("CPU", ( + ("decode.typ", [`DECODE` table], ), + ("cpu.typ", [`CPU` chip], ), + ("cpu32.typ", [`CPU32` chip], ), + )), + ("ALU", ( + ("shift.typ", [`SHIFT` chip], ), + ("branch.typ", [`BRANCH` chip], ), + ("lt.typ", [`LT` chip], ), + ("eq.typ", [`EQ` chip], ), + ("mul.typ", [`MUL` chip], ), + ("dvrm.typ", [`DVRM` chip], ), + ("bitwise.typ", [`BITWISE` chips], ), + ("bytewise.typ", [`BYTEWISE` chip], ) + )), + ("MEMORY", ( + ("memw.typ", [`MEMW` chip], ), + ("load.typ", [`LOAD` chip], ), + ("store.typ", [`STORE` chip], ), + )), + ("ECALLS", ( + ("about_ecalls.typ", [About `ECALL`], ), + ("halt.typ", [`HALT` chip], ), + ("commit.typ", [`COMMIT` chip], ), + ("sha256.typ", [`SHA256` accelerator], ), + ("keccak.typ", [`KECCAK` accelerator], ), + ("ecsm.typ", [`ECSM` accelerator], ), + ("fext.typ", [Extension field accelerator], ), + )), + ("RECURSION", ( + ("recursion.typ", [Recursive verification], ), + ("field.typ", [`Field` VM], ), + ("field_decode.typ", [`Field` `DECODE` table], ), + )), + ("MATHEMATICS", ( + ("limbs_and_carries.typ", [On limb decomposition and carries], ), + )) + ) +) +#let meta_sections = meta.summary.map(m => m.at(1)).sum() +#book-meta( + title: meta.title, + authors: meta.authors, + summary: prefix-chapter("front.typ", meta.title) + + meta.summary.map( + ((title, sections)) => { + heading(depth: 1, title) + sections.map(((ch, title, _ref)) => chapter(ch, title)).join() + } + ).join() +) + +#let highlights = ( + "aside": ("Aside", rgb("55aaff")), + "attention": ("Attention", rgb("ff2600")), +) + +#let highlight(title, body, ref: none, kind: "aside") = [ + #figure( + caption: title, + supplement: highlights.at(kind).at(0), + kind: kind, + body + )#ref +] + +#let aside = highlight.with(kind: "aside") +#let attention = highlight.with(kind: "attention") + +#let common-formatting(body) = { + set footnote(numbering: "[1]") + show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt) + show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label") + show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => { + set figure.caption(position: top) + show figure.caption: cap => block( + inset: (left: 1em, right: 1em, top: .75em, bottom: .75em), + outset: (left: 1em), + width: 100% + 1em, + fill: highlights.at(it.kind).at(1), + stroke: luma(50%), + align(center, strong(text(fill: black, cap))) + ) + block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false, align(left, it)) + } + body +} + + +#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: 20%, stroke: black)[ + #set text(fill: foreground) + *TODO #if name != none { [(#name)] }*: #body +] +#let rj = todo.with(background: teal, name: "Robin") +#let et = todo.with(background: rgb("d4aa3a"), name: "Erik") +#let cdsg = todo.with(background: olive, name: "Cyprien") + + +#let is-shiroa = "x-target" in sys.inputs + +// Strip styling to keep only "pure" content. +// This is useful to avoid errors on the `set document(...)` in `project` +// when invisibly including other chapters to resolve xrefs. +#let strip-all(content) = { + if repr(content.func()) == "sequence" { + for c in content.children { + strip-all(c) + } + } else if repr(content.func()) == "styled" { + strip-all(content.child) + } else { + content + } +} + +#let _toplevel = state("_toplevel", none) +#let _xref-included = state("_xref-included", (:)) + +// Invisibly include another chapter, so that its labels can be resolved +#let xref-include(f) = { + show ref: none + context { + place(hide(box(width: auto, height: 0%, strip-all(include "/" + f)))) + } +} + +// Generate a cross-link for references to other chapters. +// Leaves the ref untouched if it can't be resolved or points to the current chapter. +#let xref(rf) = { + assert(is-shiroa, message: "xref should only be used when compiling for shiroa") + let lbl = rf.target + let found = meta_sections.find(((_, _, tag)) => str(lbl).starts-with(str(tag))) + context if found != none and found.at(0) != _toplevel.final() { + let (ch, title, ref) = found + if ref == lbl { + cross-link("/" + ch, [Chapter #(meta_sections.position(x => x == found) + 1)]) + } else { + // Because shiroa does weird url escaping + let shiroa-label = label(str(lbl).replace(":", "%3A")) + context _xref-included.update(x => x + ((ch): true)) + // The ideal would be to use `rf` directly as content argument to `cross-link`, + // as that would inherit any/all formatting of the ref we want or need. + // Unfortunately the ref link seems to take precedence over the cross-link hyperlink + // when clicking. + // There may still be some way around it by messing with some html output + let link-content = context { + let fig = query(lbl).first() + let counter = if fig.has("counter") { + fig.counter + } else { + counter(fig.func()) + } + + let supplement = if rf.supplement == auto { + fig.fields().at("supplement", default: none) + } else { + rf.supplement + } + [#supplement #numbering(fig.numbering, ..counter.at(lbl))] + } + cross-link("/" + ch, reference: shiroa-label, link-content) + } + } else { + rf + } +} + +#let book-page(file, ..args) = { + if not file.ends-with(".typ") { + file = lower(file) + ".typ" + } + + assert(meta_sections.find(s => s.at(0) == file) != none, message: "Couldn't resolve typst source file " + file) + + if is-shiroa { + (body) => { + show: common-formatting + context _toplevel.update(s => { + if s == none { + file + } else { + s + } + }) + let cond() = _toplevel.final() == file + show ref: it => context if cond() { xref(it) } + let title = context { + // Strip raw, because shiroa already makes the title raw + show raw: it => it.text + meta_sections.find(x => x.at(0) == _toplevel.final()).at(1) + } + project.with(..args, title: title, description: plain-text(meta_sections.find(x => x.at(0) == file).at(1)), cond: cond)([ + #context _xref-included.final().pairs().map(((key, value)) => context if value and cond() { + xref-include(key) + }).join() + #metadata(json("interaction_count.json").sum(default: (:))) + + #let chapter-index = meta_sections.position(x => x.at(0) == file) + 1 + #set heading(numbering: (..args) => [#chapter-index.#numbering("1.1", ..args)]) + #counter(heading).update(0) + + #body + ]) + } + } else { + body => body + } +} diff --git a/spec/chapters/field.typ b/spec/chapters/field.typ new file mode 100644 index 000000000..1333ed77b --- /dev/null +++ b/spec/chapters/field.typ @@ -0,0 +1 @@ +TODO diff --git a/spec/chapters/field_decode.typ b/spec/chapters/field_decode.typ new file mode 100644 index 000000000..6921ceac3 --- /dev/null +++ b/spec/chapters/field_decode.typ @@ -0,0 +1,2 @@ + +TODO diff --git a/spec/chapters/recursion.typ b/spec/chapters/recursion.typ new file mode 100644 index 000000000..6b86cacaf --- /dev/null +++ b/spec/chapters/recursion.typ @@ -0,0 +1,258 @@ +#import "/meta.typ": et, aside + +// Spaces and instances +#let (programSpace, program) = ($cal(F)$, $f$) +#let (inputSpace, input) = ($II$, $bb(i)$) +#let (instanceSpace, instance) = ($XX$, $bb(x)$) +#let (witnessSpace, witness) = ($WW$, $bb(w)$) +#let (proofSpace, proof) = ($bb(Pi)$, $pi$) + +#let (commitmentSpace, commitment) = ($cal(C)$, $bb(c)$) +#let commit(x) = $overline(#x)$ +#let comm(x) = $commit(#x)$ + +#let relation = $cal(R)$ +#let language = $cal(L)$ + +#let verifierSpace = $cal(V)$ +#let (prove, verify) = ($italic("p")$, $italic("v")$) + +// Mathematical symbols +#let (zero, one) = ($0$, $1$) +#let iff = $arrow.double.l.r$ +#let implies = $arrow.double.r$ +#let prob = $PP$ +#let to = math.arrow.r + +#show math.equation.where(block: false): box + += Notation +Let $BB := { zero, one }$ denote the boolean set and let +$programSpace := {program: inputSpace times witnessSpace to BB}$ denote +the set of functions mapping the (public) input space $inputSpace$ and (private) +witness space $witnessSpace$ to this set. +We define instance space $instanceSpace := programSpace times inputSpace = {program: witnessSpace to BB}$; +program-input pairs $(program, input) in instanceSpace$ +are henceforth referred to as _function instances_, or simply _instances_. +Where the individual components of the pair are irrelevant, an instance is +denoted as $instance in instanceSpace$. + +We define relation $relation subset instanceSpace times witnessSpace$ where $((program, input), witness) in relation$ if $program(input, witness) = 1$. +This relation induces the language $language subset instanceSpace$ of _solvable instances_, +where $instance in language$ if there exists a witness $witness$ for which $(instance, witness)in relation$. + +Lastly, we introduce the instance commitment function $c: instanceSpace to commitmentSpace$. +Note that this commitment scheme does not involve randomness; it is a _determistic_ scheme. +Randomness is typically required to make a commitment _hiding_. +For the purposes of this discussion, we are not concerned with this property, +as the function will only be used for committing to public information. +To simplify notation, we henceforth use $commit(instance)$ to represent the commitment $c(instance)$ of $instance$. + +We now assume the existence of _proof system_ $(prove, verify)$ with +prover $prove: instanceSpace times witnessSpace to proofSpace$ and +verifier $verify: commitmentSpace times proofSpace to BB$ that is both +_complete_ --- i.e., $verify$ accepts all valid proofs generated by $prove$ --- +and _sound_ --- i.e., one cannot create an acceptable proof for an unsolvable instance. + +Translating this to the purposes of this VM, a prover wishes to convince the verifier +that for some agreed upon program ($program in programSpace$) and specified public input ($input in inputSpace$), +they know a private input ($witness in witnessSpace$) such that the program terminates successfully +(i.e., $(program, input) in language$). +To this end, the prover uses $prove(program(input; dot); witness)$ +to construct some proof $proof in proofSpace$ and sends this to the verifier. +They then use $verify(comm(program(input; dot)), proof)$ to check that the proof is valid, +convincing them of the prover's claim. + += Proof recursion +Now observe that the verifier $verify$ is itself a function in +$verifierSpace := {hat(f): commitmentSpace times proofSpace to BB} subset.eq programSpace$. +This means that we can use $prove$ to prove that the verification of a proof $proof$ +for a given instance $instance$ succeeds: +$ + &prove(verify(comm(instance), dot); proof) = proof', text("and") + &verify(comm(verify(comm(instance), dot)), proof') = one. +$ +This new proof $proof'$ thus attests to _the existence of a proof $proof$ that +satisfies the verifier on the given instance $instance$_. + +This concept, colloquially known as _proof recursion_, can be applied repeatedly. +The technique is specifically beneficial for _succinct_ proving systems where proof size +typically shrinks (and verification time reduces) as the level of recursion increases. +The technique is mostly useful in settings where the extra time spent by the prover +is outweighed by the time saved by the verifier(s), +e.g., a computationally constrained verifier, or multiple verifiers. + += Resolving growing instance complexity +While recursive proving leads to a decrease in proof size, this is naively traded off +against an increase in instance complexity. +Looking at a depth-two recursive proof, +$ + prove(verify(comm(verify(comm(instance), dot)), dot); proof') = proof'', text("and") + verify(comm(verify(comm(verify(comm(instance), dot)), dot)), proof'') = one +$ +we see that the verifier first has to derive the commitment +$comm(verify(comm(verify(comm(instance), dot)), dot))$ +from the given base instance $instance$ before verifying the proof. +This increase in verifier computation is undesirable and should be avoided. + +A solution to this, is to leverage the following variation to the verification algorithm: +$ + verify': commitmentSpace^2 times {0, 1} times proofSpace: (overline(r), overline(s), b, proof) mapsto + cases( + verify(overline(r), proof) &text("if") b=0, + verify(overline(s(overline(r), overline(s); dot)), proof) &text("if") b=1, + ) +$ +where it is assumed that $overline(s(overline(r), overline(s); dot)) in commitmentSpace$ can efficiently be constructed from $(overline(r), overline(s)) in commitmentSpace^2$. +Now observe that +$ + verify'(comm(instance), comm(verify'), 0, proof) &= verify(comm(instance), proof), text("and")\ + verify'(comm(instance), comm(verify'), 1, proof) &= verify(comm(verify'((comm(instance), comm(verify')); dot)), proof). +$ + +In other words, by setting $(commitment_0, commitment_1) = (commit(instance), commit(verify'))$, +this algorithm can verify a base proof by choosing $b=0$ or a recursive proof when selecting $b=1$. +Importantly, the verification of some proof $proof$ using $verify'(comm(instance), comm(verify'), 1, dot)$ +succeeds only if the prover has used $verify'$ at every step in the proof recursion. +This fact is illustrated by the following expansion: +$ + verify'(commit(instance), commit(verify'), 1, proof^((n))) + &= verify(comm(verify'(commit(instance), commit(verify'), dot)), proof^((n)))\ + &= verify(comm(verify(comm(verify'(comm(instance), comm(verify'), dot)), dot)), proof^((n)))\ + &= verify(comm(verify(comm(verify(comm(verify'(comm(instance), comm(verify'), dot)), dot)), dot)), proof^((n)))\ + &= verify(comm(verify(comm(verify(comm(dots.c (comm(verify(comm(instance), dot) dots.c))), dot)), dot)), proof^((n)))\ +$ +Hence, a recursive proof based on $verify'$ attests that $verify'$ was the +only algorithm used throughout the entire recursion stack. + +Lastly, note that the verification of a recursive proof $proof^((n))$ only +depends on $comm(instance)$, since $comm(verify')$ can be precomputed. +We have thus established a recursive proving system that only requires the base +instance as input to the verification of a recursive proof. + +#aside([$comm(verify')$ absorption])[ +Note that $commit(verify')$ must be provided to $verify'$ as a _parameter_; +absorbing it into $verify'$ would imply an object containing a cryptographic commitment of itself, +which is theoretically impossible. +] + +#et("illustrate that there comes a termination point, i.e., a proof cannot prove itself.") +#et("note shakiness of recursion") + += Split processing +#let record = $bb(r)$ +In practice, we find that the set of operations utilized for verification differs vastly from +those typically performed by guest programs. +Specifically, verification primarily involves hashing and (extension) field arithmetic, +where especially the second is absent in typical guest programs. + +Emulating field arithmetic on a binary arithmetic-oriented VM, typically +incurs significant computational overhead. +With the aim of avoiding this performance penalty, we introduce a field +arithmetic-oriented mini-VM (henceforth referred to as the _field-VM_), +which will act as a _co-processor_ to the established _binary-VM_. +Since both VMs are proven using the same proof system, a unified proof can be +produced for the parallel execution of both VMs. + +The introduction of this split allows the verification algorithm to be split in two halves, +with each VM performing the computations it is fastest at. +The two halves cannot work independently, however. +In the process of verifying proofs of the current proof system (`DEEP-FRI` + `LogUp`), +results of binary arithmetic are used to verify field arithmetical constraints +--- e.g., field challenges extracted from binary hash outputs --- +and vice-versa --- e.g., hashing merkle leafs containing field elements during FRI-query proof verification. +This implies that some form of communication between both VMs is required. + +Our architecture enables the required communications by introducing a +prover-hinted _communication record_ $record$ accessible to both VMs. +In practice, this record will primarily contain values being reinterpreted +--- from $FF$ to $ZZ_(2^64)$ and vice-versa --- during verification. +The two halves of the split verification algorithm are adapted to leverage +the record: for each value on the record, one of the VMs _verifies_ the value to be correct, +while the other _assumes_ its correctness and resumes verification under this assumption. + +To ensure correct verification, both verification-algorithm halves must align +on the interpretation of each value on the proof-record pair. +To this end, the dimensions of the record must be determined at _verification algorithm design-time_ +and parametrized in terms of the proof only. +Then, both verification algorithm halves can be given the same logic to interpret the record, +effectively synchronizing their interpretation. + +#aside("Coupling")[ + As observed, both verification halves must be synchronized to correctly verify a proof. + This implies that some coupling between both halves must exist. + This design utilizes little coupling in the VM design, instead forcing + the guest programs to solve synchronization, as a result introducing the coupling there. + + This no-coupling VM design permits one of the two halves to transition to a + different proof system (e.g., moving to Flock + #footnote(link( + "https://eprint.iacr.org/2026/1329", + "Flock: Fast Proving for Batch Boolean Computations. src: https://eprint.iacr.org/2026/1329" + )) + to accelerate hash-verification) while incurring as little design overhead as possible. +] + +In theory, any division of tasks between the two VMs would work. +Moreover, it is unclear what division will lead to optimal performance. +Yet, it is expected that divisions adhering to these high-level guidelines will +be a good first step towards a performant verifier: ++ have the field-VM perform all verification steps involving field arithmetic, ++ include all verifier-issued challenges required by these verification steps + in the communication record $record$ as field-elements, so that the field-VM does not have to derive them, ++ use the binary-VM to verify the challenges hinted by the communication record are indeed correct. + += Recursive proving and split processing +We lastly provide some notes on applying the recursive proving and split processing to +the verification of a proof in the context of this VM. + +First, we note that in any scenario, the prover has to commit to the program $program$ +being exeucted and the public input $input$ that is provided. +In a non-recursive proof, this is trivially done by committing to the `DECODE` table +representing $program$, and the `PAGE` tables storing the public $input$. +Since these commitments are deterministic, the verifier can locally reconstruct +the commitments and verify any opening proofs against its own version of the commitment. +Note that in this case, the prover may exclude the opened value from any proof strings +pertaining to the `DECODE` and `PAGE` tables, as these are already known to the verifier. + +When recursing on this process, the prover provides the verifier with this commitment. +We thus have to demonstrate the commitments the prover provides are as expected. +This is achieved by having the verificationan algorithm `COMMIT` (see @commit) +to the public input it is provided. +This act produces an imbalance in the LogUp-component of the proof-of-verification, +which must be balanced during verification in the _next_ recursion layer. +In later recursions, the verifier must consistently `COMMIT` to its public input +and use the _same_ public input to balance out the LogUp-component of the proof +it is provided. +This solution effectively kicks the can down the road; the final verifier has to +provide the initial input to the program as input to verify the recursive proof. + +Denoted as pseudo-algorithms, we find: + +#set list(marker: [---]) +*Communication record overview:* +- the data required according to the chosen verification split, +- if $b=1$, reconstructed commitment $comm(verify'(comm(instance), comm(verify'); dot))$ + +*$verify'_b\(comm(instance), (comm(verify'_b), comm(verify'_f)), b, proof, record)$:* +- `COMMIT` to $comm(instance)$, $comm(verify'_b),$ and $comm(verify'_f)$ +- assert that $b in {0, 1}$, +- verify proof: + - if $b=0$: execute $verify_b (comm(instance), proof)$ + - if $b=1$: + + construct $comm(verify'(comm(instance), comm(verify'); dot))$ from $(comm(instance), (comm(verify'_b), comm(verify'_f)))$ + + execute $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$ + +*$verify'_f\(comm(instance), (comm(verify'_b), comm(verify'_f)), b, proof, record)$:* +- verify proof: $verify_b (comm(verify'(comm(instance), comm(verify'); dot)), proof)$ + - if $b=1$, use $comm(instance), comm(verify'_b), comm(verify'_f)$ to complete the `COMMIT` LogUp-balance. + +*Prover:* +$ + proof &arrow.l prove(instance, witness)\ + proof' &arrow.l prove(verify'_b || verify'_f, (commit(instance), (commit(verify'_b), commit(verify'_f)), 0, proof, record))\ + proof^((i)) &arrow.l prove(verify'_b || verify'_f, (commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((i-1)), record)) +$ + +*Final verification.* +$verify'(commit(instance), (commit(verify'_b), commit(verify'_f)), 1, proof^((n))) =^? one$ diff --git a/spec/chapters/verifier.typ b/spec/chapters/verifier.typ new file mode 100644 index 000000000..e85903478 --- /dev/null +++ b/spec/chapters/verifier.typ @@ -0,0 +1,4 @@ +// TODO: +// - sigma protocol, layout the various steps +// - Fiat Shamir transformation into non-interactive protocol. +// diff --git a/spec/meta.typ b/spec/meta.typ index fc6bc783b..eea8f6e4a 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -10,6 +10,7 @@ ("logup", [`LogUp` argument], ), ("memory", [Memory argument], ), ("streaming", [Streaming prover], ), + ("verifier", [Verification], ), )), ("OVERVIEW", ( ("variables", [Variables], ), @@ -52,6 +53,11 @@ ("ecsm", [`ECSM` accelerator], ), ("fext", [Extension field accelerator], ), )), + ("RECURSION", ( + ("recursion", [Recursive verification], ), + ("field", [`Field` VM], ), + ("field_decode", [`Field` `DECODE` table], ), + )), ("MATHEMATICS", ( ("limbs_and_carries", [On limb decomposition and carries], ), ))