Perspective aware lexicographic ordering arguments

[OlivierBBB]

@DavePearce I am about to start specifying perspective aware lexicographic ordering arguments, something I've been promising for a while (maybe a full year at this point ?). It should be a simple variation on already existing lexicographic ordering arguments for row-permutations.

The reason for this is that I'm about to merge the HUB consistency arguments for

• accounts
• context
• storage

This should bring the number of consistency arguments for the HUB down to 3 (from 5):

• execution environment consistency constraints
• account / context / storage
• stack consistency

Before I'm doing this I am finishing the specification of the individual consistency arguments. This way we will have something that is implementable even if we don't have this new feature. I therefore am curious:

Question: do you believe you can implement this variation on the lex. ordering argument ? We may need it both for rust-corset and go-corset.

Also I'm producing two versions of these constraints:

• one where the comparisons are done "in house"
• one where the comparisons are "outsourced" to the WCP module

Resources:

• PR: https://github.com/Consensys/linea-specification-internal/pull/547
• (incomplete) drawing https://github.com/Consensys/linea-specification-internal/issues/555

[OlivierBBB]

Corset generated column comparison

I've finished a first (pretty solid I believe) draft of perspective aware lexicographic ordering arguments. It's a little convoluted but nothing that a zoom discussion can't clarify in a few minutes. In terms of upsides of this approach (which I wish to apply to the HUB module) we have, for the case of the HUB module:

• we collapse the 3 permutation arguments of ACCOUNT / CONTEXT / STORAGE into 1
• we get rid of 48 (!!!) byte columns in the HUB which would mostly be 0's anyway
• we get rid of 8 binary columns
  • $(4 + 1) + (2 + 1) + (6 + 1) = 15$ corset generated binary columns with the old approach
  • $\max \{ 4, 2, 6 \} + 1 = 7$ corset generated binary columns with the new approach
• we add an extra lookup HUB $\hookrightarrow$ WCP

[OlivierBBB]

When applied to "environment consistency"

We can further use the new "outsourced" lex. ordering arguments to reduce the cost of the "environment consistency" argument, again shaving off 16 byte columns in the HUB and adding no extra binary columns but an extra HUB $\hookrightarrow$ WCP lookup

[OlivierBBB]

When applied to "stack consistency"

We can also use the same "outsourced" lex. ordering arguments to reduce the cost of the "stack consistency" argument, again shaving off 16 byte columns in the HUB (which each are 4 * as large as the HUB!) and adding no extra binary columns but an extra HUB $\hookrightarrow$ WCP lookup.

[OlivierBBB]

Note. For both the ENV and STACK consistency arguments we could reasonably get away with far fewer byte columns in the current setup, 4 ought to suffice for all applications. Still, I believe the gains are real.

[OlivierBBB]

WCP cost

The new lookups HUB $\hookrightarrow$ WCP will incur many new WCP instructions. I attempt to bound the number of them here

• ACCOUNT / CONTEXT / STORAGE merge:
  • for account stuff we compare 4 columns, 99,99% of the time distinct addresses will already differ at the ADDRESS_HI level i.e. on the 4 first bytes; when working with the same address we will have to defer to comparing DOM_STAMP's which will be at most a 4 byte integer (it's something like 8 * HUB_STAMP), so 99.99% of all comparisons will take at most 4 rows in the WCP
    
    • Effective cost: [1 to 2] * [# of account touching operations] many 4 row WCP instructions (and a minority of larger WCP operations)
  • for context stuff we only compare CONTEXT_NUMBER's and HUB_STAMP's, which both will be in the millions at most. So 1-3 Byte comparisons will suffice in the WCP
    
    • Effective cost: [# context rows] many 4 row WCP instructions
  • for storage stuff we will either compare different addresses, again 99.99% of the time the comparison will happen at the ADDRESS_HI level so generate at most 4 rows in the WCP module; when working within a given account we may modify a few storage keys; what is a reasonable number of affected storage keys in a block ? a few hundred ? I don't know, but comparisons will usually require 16 rows in the WCP module; and when working with the same key multiple times we will compare either DOM_STAMP or SUB_STAMP and again require up to 4 rows in the WCP
    
    • Effective cost: [1 to 2] * [# of accounts whose storage was touched] many 4 row WCP instructions + [1 to 2] * [# of distinct touched storage keys] many 16 row WCP instructions

Note

The [1 to 2] factors account for the possibility of operations being reverted (and producing 2 account / storage rows rather than 1.) This should be a minority of the cases so effectively that factor ought to be much closer to 1 than to 2 for most all conflations.

[OlivierBBB]

Interface

In order to specify such an argument we should supply corset with a list of the following form

(module MODULE_NAME)

(perspective-aware-lexicographic-ordering-constraints
    (
        (perspective-1-spec)
        (perspective-2-spec)
        ...
        (perspective-p-spec)
    )
)

where each (perspective-k-spec) of these is of the form

(
    PERSPECTIVE_FLAG               ;; relevant perspective flag, k^👁️ in the spec
    perspective-weight             ;; small integer, = k for the k-th perspective
    requires-lex-ordering          ;; boolean value, true <=> k ∈ L
    (sign-sequence)                ;; ordered list of m_k symbols +/-, ε^k_• in the spec
    (order-defining-columns)       ;; ordered list of m_k columns
    (order-following-columns)      ;; list of columns we wish to permute besides the order defining ones
)

and where, following conventions of the spec, (sign-sequence) would correspond to

(
    ε^k_1
    ε^k_2
    ...
    ε^k_{m_k}
)

and (order-defining-columns) would correspond to

(
    k-ORD<1>
    k-ORD<2>
    ...
    k-ORD<m_k>
)

and (order-following-columns) isn't mentioned in the spec, it's just an (unordered) list of other columns that we wish to permute along side the (order-defining-columns) and following their lead in defining the permutation.

Note. What the spec calls $L$ is the set of flags with requires-lex-ordering = true

[OlivierBBB]

Why apply lex. ordering constraints on only a subset $L$ of the perspectives ?

We want it for the HUB. In the HUB we will apply this argument to the following ordered list of perspectives:

[ACC👁️, TXN👁️, CON👁️, MISC👁️, STO👁️]

With $L = \{$ ACC👁️, CON👁️, STO👁️ $\}$. The presence of the other perspectives (TXN👁️ and MISC👁️) interspliced with the ones we actually care about ($L$) comes at no extra cost to the argument and provides us with guaranteed "rest" between the perspectives we actually care about. The upshot of that is that we will be able to use the common infrastructure to conduct the consistency constraints for the relevant reordered perspectives of $L$ because there will be some "breathing room" where we can reset the common infrastructure.