From 80a22a403f74683c5e40250da4f348d033dd6e2d Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Thu, 22 Jan 2026 16:57:59 -0800 Subject: [PATCH 01/10] spec: Edit todo spacing --- spec/book.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/book.typ b/spec/book.typ index 29e61350c..5fefe9f8c 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -27,7 +27,7 @@ #import "/templates/page.typ": project #let book-page = project -#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.5em, radius: 20%, stroke: black)[ +#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 ] From 9dae193de87762b51f53785041d878a0c203c772 Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Thu, 22 Jan 2026 16:58:34 -0800 Subject: [PATCH 02/10] spec: Add todo binding --- spec/book.typ | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/book.typ b/spec/book.typ index 5fefe9f8c..6c757178d 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -33,6 +33,7 @@ ] #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 style = state("style", ( foreground: white, From 24ea3bc1a57e99386bc0fb51ca94a3d7674eb7e1 Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Thu, 22 Jan 2026 09:00:02 -0800 Subject: [PATCH 03/10] spec: Add blank page for LogUp argument --- spec/book.typ | 1 + spec/logup.typ | 5 +++++ 2 files changed, 6 insertions(+) create mode 100644 spec/logup.typ diff --git a/spec/book.typ b/spec/book.typ index 6c757178d..628b18f4d 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -20,6 +20,7 @@ #chapter("load.typ")[LOAD chip] #chapter("ecall.typ")[ECALL chips] #chapter("bitwise.typ")[BITWISE] + #chapter("logup.typ")[LogUp argument] ] ) diff --git a/spec/logup.typ b/spec/logup.typ new file mode 100644 index 000000000..97c7fb5c3 --- /dev/null +++ b/spec/logup.typ @@ -0,0 +1,5 @@ +#import "/book.typ": book-page + +#show: book-page.with(title: "LogUp Argument") + += LogUp Argument From 3b6dad5957c4396f35f044009e86d60c4e64d3aa Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Mon, 26 Jan 2026 20:16:03 -0800 Subject: [PATCH 04/10] spec: LogUp: First draft of Vanilla LogUp description --- spec/logup.typ | 80 ++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 78 insertions(+), 2 deletions(-) diff --git a/spec/logup.typ b/spec/logup.typ index 97c7fb5c3..c87983a90 100644 --- a/spec/logup.typ +++ b/spec/logup.typ @@ -1,5 +1,81 @@ -#import "/book.typ": book-page +#import "/book.typ": book-page, cdsg #show: book-page.with(title: "LogUp Argument") -= LogUp Argument +The _LogUp_ proof system conducts a permutation check based on summing partial derivatives. This check ensures that whatever tuple is sent to be "looked-up" by a _source table_ is indeed received in the expected _destination table_. + += Notation + +#let BaseField = math.FF +#let ExtensionField = math.GG + +== VM Notation + +#let numTables = math.sans()[t] +#let Table = $T$ +#let TableSet = ${Table_i}_(i in [t])$ +#let numColumns = math.sans()[m] +#let numRows = math.sans()[N] + +- $numTables in NN$: number of tables $Table_i$ in the arithmetisation of the VM. +- $TableSet$: set of all tables $Table_i$ in the arithmetisation of the VM. +- $numColumns_i in NN$: number of _columns_ in table $Table_i$ (not the number of variables). +- $numRows_i in NN$: number of _rows_ in table $Table_i$. + +== Interaction Notation + +#let Interaction = $I$ +#let id = math.sans()[id] +#let numElements = $l$ +#let weightFunction = $w$ +#let multiplicity = $mu$ + +The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the following tuple: + +#table( + columns: (auto, auto), + inset: 6pt, + align: horizon, + table.header([Symbol], [Description]), + [$id in FF$], + [the _type identifier_ of the interaction, usually the identifier of the chip that is sending or receiving the interaction.], + [$numElements in NN$], + [the _length_ of the tuple of elements being looked-up.], + [$weightFunction : FF^(numColumns) arrow FF^(numElements)$], + [the _weight function_ that maps row elements of table $Table$ to the looked-up tuple.], + [$multiplicity in [numColumns] union {1_BaseField, dots}$], + [the _multiplicity_ of the interaction, as either a column index in table $Table$ or a constant value.] +) + + += Vanilla LogUp Protocol + +#let logupChallenge = math.alpha +#let fingerprintCoeff = math.beta + ++ Prover commits to all traces. + ++ Verifier samples a random _(global) LogUp challenge_ $logupChallenge in ExtensionField$ and a random _fingerprint coefficient_ $fingerprintCoeff in ExtensionField$ and sends them to the Prover. + ++ Prover commits to interaction contribution and table running sum columns and to each table's contribution: + + + For each table $Table_i$, populate the interaction contribution columns and compute the _table (LogUp) contribution_: + + + For each interaction $Interaction_j$ of table $Table_i$, initialize an empty _interaction contribution column_ of length $numRows_i$. + + + Initialise a _table running sum column_ of length $numRows_i$ with $Sigma_0 = 0 in ExtensionField$ in the first row. + + + For each $j$-th row $R_j in BaseField^(numColumns_i)$ of $Table_i$, for $j in [numRows_i]$: + + For each $k$-th interaction $Interaction_k$ of table $Table_i$: + + Compute the _interaction contribution numerator_ $ n_(j,k) = cases(R_j [multiplicity] quad & "if" multiplicity in [numColumns]",", multiplicity & "otherwise.") $ + + If $n eq.not 0$, compute the _interaction contribution denominator_ $ d_(j,k) = logupChallenge + fingerprintCoeff dot Interaction_k\.id + sum_(l = 0)^(numElements - 1) fingerprintCoeff^(l + 1) dot weightFunction(R_l)[j] $. + + Save the _interaction contribution_ as $n_(j,k)/d_(j,k) in ExtensionField$ in the corresponding interaction contribution column for this interaction. + + *Constrain* the interaction contribution column according to the definitions of $n$ and $d$. + + + Compute the _row contribution_ as the sum $sigma_j = sum_k n_(j,k) / d_(j,k)$ and compute the next row's table running sum value $Sigma_(j+1) = Sigma_j + sigma_j$. + + + *Constrain* the update of the next row's running sum value. + + + Batch-commit to every table's interaction contribution columns and running sum columns with the column commitment scheme and commit to the table's overall contribution $Sigma_(N_i)$ by sending it in the clear to the verifier. + + + Verifier checks that the sum of every table's overall contribution is equal to zero: $sum_i Sigma_i == 0 in ExtensionField$, and delegates the checks of the constraints to the STARK. From 2736abe4af5dbfbf279a82175a1e53d4c0cc6868 Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Wed, 28 Jan 2026 17:49:46 -0800 Subject: [PATCH 05/10] spec: LogUp: Fix editorial issues from first review --- spec/logup.typ | 43 +++++++++++++++++++++++++++++++------------ 1 file changed, 31 insertions(+), 12 deletions(-) diff --git a/spec/logup.typ b/spec/logup.typ index c87983a90..cc249906b 100644 --- a/spec/logup.typ +++ b/spec/logup.typ @@ -11,6 +11,15 @@ The _LogUp_ proof system conducts a permutation check based on summing partial d == VM Notation +=== Preliminary notation +- $NN$: the set of non-zero natural integers. +- $BaseField$: the base finite field used by the arithmetisation. +- $ExtensionField$: a finite extension of $BaseField$ of cryptographic size. +- $[n]$ for $n in NN$: the set of integers ${0, dots, n - 1}$. +- $X[i]$ for tuple $X$: the $i$-th element of $X$, starting at $0$. + +=== Arithmetisation notation + #let numTables = math.sans()[t] #let Table = $T$ #let TableSet = ${Table_i}_(i in [t])$ @@ -36,15 +45,19 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo columns: (auto, auto), inset: 6pt, align: horizon, + stroke: none, + table.header([*Symbol*], [*Description*]), + table.hline(stroke: 1pt), + table.vline(stroke: 1pt, x: 1), table.header([Symbol], [Description]), - [$id in FF$], - [the _type identifier_ of the interaction, usually the identifier of the chip that is sending or receiving the interaction.], - [$numElements in NN$], + [$id_(i,j) in FF$], + [the _type identifier_ of the interaction, usually the identifier of the chip that is constraining the relation expected to hold within the looked-up tuple.], + [$numElements_(i,j) in NN$], [the _length_ of the tuple of elements being looked-up.], - [$weightFunction : FF^(numColumns) arrow FF^(numElements)$], - [the _weight function_ that maps row elements of table $Table$ to the looked-up tuple.], - [$multiplicity in [numColumns] union {1_BaseField, dots}$], - [the _multiplicity_ of the interaction, as either a column index in table $Table$ or a constant value.] + [$weightFunction_(i,j) : FF^(numColumns_i) arrow FF^(numElements_j)$], + [the _weight function_ that maps row elements of table $Table_i$ to the looked-up tuple.], + [$multiplicity_(i,j) in [numColumns] union {1_BaseField, dots}$], + [the _multiplicity_ of the interaction, as either a column index in table $Table_i$ or a constant value.] ) @@ -59,23 +72,29 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo + Prover commits to interaction contribution and table running sum columns and to each table's contribution: + #set enum(numbering: "a.") + + For each table $Table_i$, populate the interaction contribution columns and compute the _table (LogUp) contribution_: + #set enum(numbering: "i.") + + For each interaction $Interaction_j$ of table $Table_i$, initialize an empty _interaction contribution column_ of length $numRows_i$. - + Initialise a _table running sum column_ of length $numRows_i$ with $Sigma_0 = 0 in ExtensionField$ in the first row. + + Initialise a _table running sum column_ $S_i in ExtensionField^(numRows_i)$ with $S_i [0] = 0_ExtensionField$ in the first row. + For each $j$-th row $R_j in BaseField^(numColumns_i)$ of $Table_i$, for $j in [numRows_i]$: + #set enum(numbering: "1.") + For each $k$-th interaction $Interaction_k$ of table $Table_i$: + #set enum(numbering: "a.") + Compute the _interaction contribution numerator_ $ n_(j,k) = cases(R_j [multiplicity] quad & "if" multiplicity in [numColumns]",", multiplicity & "otherwise.") $ - + If $n eq.not 0$, compute the _interaction contribution denominator_ $ d_(j,k) = logupChallenge + fingerprintCoeff dot Interaction_k\.id + sum_(l = 0)^(numElements - 1) fingerprintCoeff^(l + 1) dot weightFunction(R_l)[j] $. + + If $n eq.not 0$, compute the _interaction contribution denominator_ $ d_(j,k) = logupChallenge + fingerprintCoeff dot Interaction_k\.id + sum_(l = 0)^(numElements - 1) fingerprintCoeff^(l + 2) dot weightFunction(R_j)[l] $. + Save the _interaction contribution_ as $n_(j,k)/d_(j,k) in ExtensionField$ in the corresponding interaction contribution column for this interaction. + *Constrain* the interaction contribution column according to the definitions of $n$ and $d$. - + Compute the _row contribution_ as the sum $sigma_j = sum_k n_(j,k) / d_(j,k)$ and compute the next row's table running sum value $Sigma_(j+1) = Sigma_j + sigma_j$. + + Compute the _row contribution_ as the sum $s_(j) = sum_k n_(j,k) / d_(j,k)$ and compute the next row's table running sum value $S_i [j+1] = S_i [j] + s_(j)$. + *Constrain* the update of the next row's running sum value. - + Batch-commit to every table's interaction contribution columns and running sum columns with the column commitment scheme and commit to the table's overall contribution $Sigma_(N_i)$ by sending it in the clear to the verifier. + + Batch-commit to every table's interaction contribution columns and running sum columns with the column commitment scheme and commit to the table's overall contribution $S_i [N_i]$ by sending it in the clear to the verifier. - + Verifier checks that the sum of every table's overall contribution is equal to zero: $sum_i Sigma_i == 0 in ExtensionField$, and delegates the checks of the constraints to the STARK. ++ Verifier checks that the sum of every table's overall contribution is equal to zero: $sum_i S_i [N_i] = 0_ExtensionField$, and delegates the checks of the constraints to the STARK. From a600469dd35d2382ede656b0f1da8ea052c20b01 Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Thu, 29 Jan 2026 17:07:49 -0800 Subject: [PATCH 06/10] spec: Logup: Fix editorial issues from second reviews --- spec/logup.typ | 24 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) diff --git a/spec/logup.typ b/spec/logup.typ index cc249906b..dc1470b72 100644 --- a/spec/logup.typ +++ b/spec/logup.typ @@ -1,6 +1,6 @@ #import "/book.typ": book-page, cdsg -#show: book-page.with(title: "LogUp Argument") +#show: book-page("logup") The _LogUp_ proof system conducts a permutation check based on summing partial derivatives. This check ensures that whatever tuple is sent to be "looked-up" by a _source table_ is indeed received in the expected _destination table_. @@ -20,11 +20,11 @@ The _LogUp_ proof system conducts a permutation check based on summing partial d === Arithmetisation notation -#let numTables = math.sans()[t] +#let numTables = $sans(t)$ #let Table = $T$ #let TableSet = ${Table_i}_(i in [t])$ -#let numColumns = math.sans()[m] -#let numRows = math.sans()[N] +#let numColumns = $sans(m)$ +#let numRows = $sans(N)$ - $numTables in NN$: number of tables $Table_i$ in the arithmetisation of the VM. - $TableSet$: set of all tables $Table_i$ in the arithmetisation of the VM. @@ -34,8 +34,8 @@ The _LogUp_ proof system conducts a permutation check based on summing partial d == Interaction Notation #let Interaction = $I$ -#let id = math.sans()[id] -#let numElements = $l$ +#let id = $sans(id)$ +#let numElements = $ell$ #let weightFunction = $w$ #let multiplicity = $mu$ @@ -66,28 +66,24 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo #let logupChallenge = math.alpha #let fingerprintCoeff = math.beta +#set enum(numbering: "1.a.i.1.a.") + + Prover commits to all traces. + Verifier samples a random _(global) LogUp challenge_ $logupChallenge in ExtensionField$ and a random _fingerprint coefficient_ $fingerprintCoeff in ExtensionField$ and sends them to the Prover. -+ Prover commits to interaction contribution and table running sum columns and to each table's contribution: - - #set enum(numbering: "a.") ++ Prover commits to (i) interaction contribution, (ii) table running sum columns, and (iii) each table's contribution: + For each table $Table_i$, populate the interaction contribution columns and compute the _table (LogUp) contribution_: - #set enum(numbering: "i.") - + For each interaction $Interaction_j$ of table $Table_i$, initialize an empty _interaction contribution column_ of length $numRows_i$. + Initialise a _table running sum column_ $S_i in ExtensionField^(numRows_i)$ with $S_i [0] = 0_ExtensionField$ in the first row. + For each $j$-th row $R_j in BaseField^(numColumns_i)$ of $Table_i$, for $j in [numRows_i]$: - #set enum(numbering: "1.") + For each $k$-th interaction $Interaction_k$ of table $Table_i$: - #set enum(numbering: "a.") + Compute the _interaction contribution numerator_ $ n_(j,k) = cases(R_j [multiplicity] quad & "if" multiplicity in [numColumns]",", multiplicity & "otherwise.") $ - + If $n eq.not 0$, compute the _interaction contribution denominator_ $ d_(j,k) = logupChallenge + fingerprintCoeff dot Interaction_k\.id + sum_(l = 0)^(numElements - 1) fingerprintCoeff^(l + 2) dot weightFunction(R_j)[l] $. + + If $n eq.not 0$, compute the _interaction contribution denominator_ $ d_(j,k) = logupChallenge + fingerprintCoeff dot id_(i,k) + sum_(l = 0)^(numElements - 1) fingerprintCoeff^(l + 2) dot weightFunction_(i,k) (R_j)[l]. $ + Save the _interaction contribution_ as $n_(j,k)/d_(j,k) in ExtensionField$ in the corresponding interaction contribution column for this interaction. + *Constrain* the interaction contribution column according to the definitions of $n$ and $d$. From c4ece24db17ffe195bd550959f8697fad9fbde04 Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Wed, 18 Feb 2026 16:30:20 -0800 Subject: [PATCH 07/10] spec: LogUp: unify weight function and multiplicity and other fixes --- spec/logup.typ | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/spec/logup.typ b/spec/logup.typ index dc1470b72..511c46ece 100644 --- a/spec/logup.typ +++ b/spec/logup.typ @@ -54,10 +54,11 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo [the _type identifier_ of the interaction, usually the identifier of the chip that is constraining the relation expected to hold within the looked-up tuple.], [$numElements_(i,j) in NN$], [the _length_ of the tuple of elements being looked-up.], - [$weightFunction_(i,j) : FF^(numColumns_i) arrow FF^(numElements_j)$], - [the _weight function_ that maps row elements of table $Table_i$ to the looked-up tuple.], - [$multiplicity_(i,j) in [numColumns] union {1_BaseField, dots}$], - [the _multiplicity_ of the interaction, as either a column index in table $Table_i$ or a constant value.] + [ + $weightFunction_(i,j) : FF^(numColumns_i) & arrow FF^(numElements_(i,j) + 1) \ + R & mapsto arrow(t)_(i,j) || mu_(i,j)$ + ], + [the _weight function_ that maps a row $R$ of table $Table_i$ to the looked-up tuple $arrow(t)_(i,j)$ and its multiplicity $mu_(i,j) in BaseField$.], ) @@ -80,17 +81,19 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo + Initialise a _table running sum column_ $S_i in ExtensionField^(numRows_i)$ with $S_i [0] = 0_ExtensionField$ in the first row. - + For each $j$-th row $R_j in BaseField^(numColumns_i)$ of $Table_i$, for $j in [numRows_i]$: + + *Constrain* the table running sum column to begin at $0_ExtensionField$. + + + For each $j$-th row $R_j in BaseField^(numColumns_i)$ of $Table_i$, for $j in [numRows_i - 1]$: + For each $k$-th interaction $Interaction_k$ of table $Table_i$: - + Compute the _interaction contribution numerator_ $ n_(j,k) = cases(R_j [multiplicity] quad & "if" multiplicity in [numColumns]",", multiplicity & "otherwise.") $ - + If $n eq.not 0$, compute the _interaction contribution denominator_ $ d_(j,k) = logupChallenge + fingerprintCoeff dot id_(i,k) + sum_(l = 0)^(numElements - 1) fingerprintCoeff^(l + 2) dot weightFunction_(i,k) (R_j)[l]. $ + + Compute the _interaction contribution numerator_ $ n_(j,k) = mu_(i,k) = w_(i,k)(R_j)[numElements_(i,k)] $ + + If $n eq.not 0$, compute the _interaction contribution denominator_ $ d_(j,k) = logupChallenge + fingerprintCoeff dot id_(i,k) + sum_(l = 0)^(numElements_(i,k) - 1) fingerprintCoeff^(l + 2) dot weightFunction_(i,k) (R_j)[l]. $ + Save the _interaction contribution_ as $n_(j,k)/d_(j,k) in ExtensionField$ in the corresponding interaction contribution column for this interaction. - + *Constrain* the interaction contribution column according to the definitions of $n$ and $d$. + + *Constrain* the interaction contribution column according to the definitions of $n$ and~$d$. + Compute the _row contribution_ as the sum $s_(j) = sum_k n_(j,k) / d_(j,k)$ and compute the next row's table running sum value $S_i [j+1] = S_i [j] + s_(j)$. + *Constrain* the update of the next row's running sum value. - + Batch-commit to every table's interaction contribution columns and running sum columns with the column commitment scheme and commit to the table's overall contribution $S_i [N_i]$ by sending it in the clear to the verifier. + + Batch-commit to every table's interaction contribution columns and running sum columns with the column commitment scheme and commit to the table's overall contribution $S_i [N_i - 1]$ by sending it in the clear to the verifier. -+ Verifier checks that the sum of every table's overall contribution is equal to zero: $sum_i S_i [N_i] = 0_ExtensionField$, and delegates the checks of the constraints to the STARK. ++ Verifier checks that the sum of every table's overall contribution is equal to zero: $sum_i S_i [N_i - 1] = 0_ExtensionField$, and delegates the checks of the constraints to the STARK. From 9c7bfb475dffca85b2b30e80db0a6c6eed0d4697 Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Thu, 19 Feb 2026 14:00:58 -0800 Subject: [PATCH 08/10] spec: LogUp: Describe constraint choices for running sum --- spec/logup.typ | 42 +++++++++++++++++++++++++++++++++++++++--- 1 file changed, 39 insertions(+), 3 deletions(-) diff --git a/spec/logup.typ b/spec/logup.typ index 511c46ece..ff79bb1c0 100644 --- a/spec/logup.typ +++ b/spec/logup.typ @@ -1,6 +1,10 @@ #import "/book.typ": book-page, cdsg #show: book-page("logup") +#set heading(numbering: "1.") +#show link: underline + +#show "constraint choice": link()[constraint choice] The _LogUp_ proof system conducts a permutation check based on summing partial derivatives. This check ensures that whatever tuple is sent to be "looked-up" by a _source table_ is indeed received in the expected _destination table_. @@ -62,7 +66,9 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo ) -= Vanilla LogUp Protocol += Vanilla LogUp + +== Protocol Description #let logupChallenge = math.alpha #let fingerprintCoeff = math.beta @@ -81,7 +87,7 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo + Initialise a _table running sum column_ $S_i in ExtensionField^(numRows_i)$ with $S_i [0] = 0_ExtensionField$ in the first row. - + *Constrain* the table running sum column to begin at $0_ExtensionField$. + + *Constrain* the first row if required by selected constraint choice. + For each $j$-th row $R_j in BaseField^(numColumns_i)$ of $Table_i$, for $j in [numRows_i - 1]$: + For each $k$-th interaction $Interaction_k$ of table $Table_i$: @@ -92,8 +98,38 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo + Compute the _row contribution_ as the sum $s_(j) = sum_k n_(j,k) / d_(j,k)$ and compute the next row's table running sum value $S_i [j+1] = S_i [j] + s_(j)$. - + *Constrain* the update of the next row's running sum value. + + *Constrain* the transition of the running sum column as indicated by the constraint choice. + + + *Constrain* the last row if required by selected constraint choice. + Batch-commit to every table's interaction contribution columns and running sum columns with the column commitment scheme and commit to the table's overall contribution $S_i [N_i - 1]$ by sending it in the clear to the verifier. + Verifier checks that the sum of every table's overall contribution is equal to zero: $sum_i S_i [N_i - 1] = 0_ExtensionField$, and delegates the checks of the constraints to the STARK. + +== Running Sum Constraint Choices + +=== Choice 1: transitions looking back + +tl,dr: implicit $0_ExtensionField$ initial value, explicit final value. + ++ (*Boundary, first row*) Constrain first row of running sum column to equal the sum of the first row of every interaction contribution column. (This is analogous an implicit $-1$-th row initialised at $0_ExtensionField$.) ++ (*Transition, looking back, applied to rows $1, dots, numRows_i - 1$*) For each row _other than the first_, constrain the _current_ running sum value to equal the sum of every current interaction contribution column added to the _previous_ running sum value. ++ (*Boundary, last row*) Constrain last row of running sum column to equal the claimed table contribution. + +Total constraints: 2 boundary + 1 transition over $numRows_i - 1$ rows. + +=== Choice 2: transitions looking forward + +tl,dr: explicit $0_ExtensionField$ initial value, implicit final value. + ++ (*Boundary, first row*) Constrain first row of running sum column to equal $0_ExtensionField$. ++ (*Transition, looking forward, applied to rows $0, dots, numRows_i - 2$*) For each row _other than the last_, constrain the _next_ running sum value to equal the sum of every current interaction contribution column added to the _current_ running sum value. ++ (*Boundary, last row*) Constrain last row of running sum column added to sum of last row of every interaction column to equal the claimed table contribution. (That is, the claimed table contribution is implicit in the last row of the table, but not written to last value of running sum column.) + +Total constraints: 2 boundary + 1 transition over $numRows_i - 1$ rows. + +=== Choice 3: circular transitions looking back/forward + ++ For each row, constrain the _current/next_ (wrapping to first on last if next) running sum value to equal the sum of every current interaction contribution value added to the _previous/current_ (wrapping to last on first if previous) running sum value added to claimed table contribution divided by $numRows_i$. + +Total constraints: 1 _circular_ transition over $numRows_i$ rows. From 36a9fce321ca88ad7ec0d432ef8138451c458a2e Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 20 Feb 2026 14:26:13 +0100 Subject: [PATCH 09/10] ref to logup --- spec/memory.typ | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/spec/memory.typ b/spec/memory.typ index 778183dab..183bb95fa 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -95,9 +95,8 @@ we can see the necessity for a memory initialization procedure ---in addition to having to make sure the initial memory content lines up with what the binary dictates. So long as we can properly constrain temporal integrity (that is, no memory operation can consume future tokens), -this "balancing" act of tokens can be integrated (with sufficient domain separation) into the existing LogUp argument: +this "balancing" act of tokens can be integrated (with sufficient domain separation) into the existing LogUp argument (@logup): consuming a token corresponds to a "receive" and emitting a new token is a "send". -#rj[properly link/refer to the logup spec] = Temporal integrity From a342bac85f50302ee6ab15227e4194bb255facee Mon Sep 17 00:00:00 2001 From: Cyprien de Saint Guilhem Date: Mon, 23 Feb 2026 10:51:58 -0500 Subject: [PATCH 10/10] spec: LogUp: Justify circular constraint and minor edits Addresses 20/02/2026 comments from @RobinJadoul. --- spec/book.typ | 2 +- spec/logup.typ | 21 ++++++++++++++++----- 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index ad156c445..190e63f17 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -7,6 +7,7 @@ title: "Lambda VM specification", authors: ("3MI Labs", "Aligned"), summary: ( + ("logup.typ", [LogUp argument], ), ("memory.typ", [Memory argument], ), ("variables.typ", [Variables], ), ("signatures.typ", [Signatures], ), @@ -25,7 +26,6 @@ ("load.typ", [LOAD chip], ), ("ecall.typ", [ECALL chips], ), ("bitwise.typ", [BITWISE chips], ), - ("logup.typ", [LogUp argument], ) ) ) #book-meta( diff --git a/spec/logup.typ b/spec/logup.typ index ff79bb1c0..7bb9a085d 100644 --- a/spec/logup.typ +++ b/spec/logup.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, cdsg +#import "/book.typ": book-page, aside, cdsg #show: book-page("logup") #set heading(numbering: "1.") @@ -16,7 +16,7 @@ The _LogUp_ proof system conducts a permutation check based on summing partial d == VM Notation === Preliminary notation -- $NN$: the set of non-zero natural integers. +- $NN$: the set of non-negative natural integers. - $BaseField$: the base finite field used by the arithmetisation. - $ExtensionField$: a finite extension of $BaseField$ of cryptographic size. - $[n]$ for $n in NN$: the set of integers ${0, dots, n - 1}$. @@ -53,7 +53,6 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo table.header([*Symbol*], [*Description*]), table.hline(stroke: 1pt), table.vline(stroke: 1pt, x: 1), - table.header([Symbol], [Description]), [$id_(i,j) in FF$], [the _type identifier_ of the interaction, usually the identifier of the chip that is constraining the relation expected to hold within the looked-up tuple.], [$numElements_(i,j) in NN$], @@ -85,7 +84,7 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo + For each interaction $Interaction_j$ of table $Table_i$, initialize an empty _interaction contribution column_ of length $numRows_i$. - + Initialise a _table running sum column_ $S_i in ExtensionField^(numRows_i)$ with $S_i [0] = 0_ExtensionField$ in the first row. + + Initialise a _table running sum column_ $S_i in ExtensionField^(numRows_i)$ with the first value $S_i [0]$ populated according to the constraint choice. + *Constrain* the first row if required by selected constraint choice. @@ -108,6 +107,8 @@ The $j$-th _interaction_ $Interaction_j$ of table $Table_i$ is defined by the fo == Running Sum Constraint Choices +#cdsg[Write the constraints in this section more formally after STARK description has been written.] + === Choice 1: transitions looking back tl,dr: implicit $0_ExtensionField$ initial value, explicit final value. @@ -130,6 +131,16 @@ Total constraints: 2 boundary + 1 transition over $numRows_i - 1$ rows. === Choice 3: circular transitions looking back/forward -+ For each row, constrain the _current/next_ (wrapping to first on last if next) running sum value to equal the sum of every current interaction contribution value added to the _previous/current_ (wrapping to last on first if previous) running sum value added to claimed table contribution divided by $numRows_i$. ++ For each row, constrain the _current/next_ (wrapping to first on last if "next") running sum value to equal the sum of every current interaction contribution value added to the _previous/current_ (wrapping to last on first if "previous") running sum value added to claimed table contribution divided by $numRows_i$. Total constraints: 1 _circular_ transition over $numRows_i$ rows. + +#aside("Justification")[ + This single circular constraint checks that each row's contribution $s_(i,j)$ is added to the running sum column, either in the current row's cell or in the next row's. + In order to avoid boundary constraints, the look-back or peek-forward into the running sum column wraps around the beginning or end of the table. + + This alone implies that difference between first and last row's values will be the table's overall real contribution $sum_j s_(i,j)$, which will be incompatible with the circularity of the constraint. + Since boundary constraints are avoided, the way to check that $sum_j s_(i,j)$ equals the claimed contribution $L_i$ is to remove a fraction of $L_i$ at each row in such a way that $L_i$ is removed completely after summing all $numRows_i$ rows; i.e., the constraint subtracts the public term $L_i / numRows_i$ from the running sum at every row. + + If the expected equality $sum_j s_(i,j) = L_i$ holds, then the circularity of the constraint will also hold. +]