Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion prover-ray/backend/core.go
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import (
"os"

zkc_r5 "github.com/LFDT-Lineth/lineth-monorepo/prover-ray/backend/zkc-r5"
"github.com/LFDT-Lineth/lineth-monorepo/prover-ray/maths/koalabear/field"
"github.com/LFDT-Lineth/lineth-monorepo/prover-ray/wiop"
"github.com/LFDT-Lineth/lineth-monorepo/prover-ray/zkcdriver"
)
Expand Down Expand Up @@ -133,7 +134,7 @@ func (c *Core) runProve(
_ = ctx // cancellation not yet propagated into the prover internals

proof, pub := c.sys.Prove(func(rt *wiop.Runtime) {
c.driver.AssignWithPreRead(rt, preRead)
c.driver.AssignWithPreRead(rt, preRead, field.Octuplet{})
})

if err := c.sys.Verify(proof, pub); err != nil {
Expand Down
51 changes: 25 additions & 26 deletions prover-ray/crypto/koalabear/multiset_hashing/msethash.go
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
// Package multiset_hashing implements a LtHash-style multiset hash over the
// Koalabear field, and exposes a [Hasher] that satisfies the
// [preflight.AdditiveHasher] interface so it can drive the cross-shard
// shared-randomness protocol.
// Koalabear field. On top of the [MSetHash] accumulator it exposes an additive
// group API ([Hash], [Combine], [Identity], [ToSeed]) that drives the
// cross-shard shared-randomness protocol in
// [github.com/LFDT-Lineth/lineth-monorepo/prover-ray/preflight].
//
// The accumulator [MSetHash] is an array of [MSetHashSize] field elements
// The accumulator [MSetHash] is an array of [MSetHashSizeNumFieldElement] field elements
// initialised to zero (the empty-set digest). Inserting a message M maps M
// through Poseidon2 in 41 independent 8-element chunks and adds each chunk
// componentwise to the accumulator; removing subtracts instead. Because the
Expand All @@ -29,13 +30,13 @@ const (
// constant; the actual hashing still uses poseidon2.NewMDHasher.
blockSize = poseidon2.BlockSize

// MSetHashSize is the number of field elements in the accumulator.
MSetHashSize = chunkSize * blockSize
// MSetHashSizeNumFieldElement is the number of field elements in the accumulator.
MSetHashSizeNumFieldElement = chunkSize * blockSize
)

// MSetHash is a multiset hash accumulator over the Koalabear field. The zero
// value represents the empty set and is ready to use without initialisation.
type MSetHash [MSetHashSize]field.Element
type MSetHash [MSetHashSizeNumFieldElement]field.Element

// Insert adds msg to the accumulator. Panics on an empty msg.
func (m *MSetHash) Insert(msg ...field.Element) {
Expand Down Expand Up @@ -91,37 +92,35 @@ func (m *MSetHash) update(rem bool, msg ...field.Element) {
}
}

// Hasher implements [preflight.AdditiveHasher][MSetHash]. The zero value is
// ready to use.
//
// Hash maps a Merkle root (8 field elements) into an MSetHash accumulator by
// inserting the root elements. Combine adds two accumulators componentwise.
// ToSeed compresses the 328-element accumulator to a single [field.Octuplet]
// by hashing all elements through Poseidon2; the result seeds SetFSState.
type Hasher struct{}

// Hash implements [preflight.AdditiveHasher].
func (Hasher) Hash(root field.Octuplet) MSetHash {
// The functions below present the multiset hash as an additive group over
// [MSetHash]: [Hash] maps a value in, [Combine] is the group operation,
// [Identity] is the neutral element, and [ToSeed] compresses a group element
// back to a single octuplet.

// Hash maps a Merkle root (8 field elements) into a fresh accumulator by
// inserting the root elements.
func Hash(root field.Octuplet) MSetHash {
var m MSetHash
m.Insert(root[:]...)
return m
}

// Combine implements [preflight.AdditiveHasher].
func (Hasher) Combine(a, b MSetHash) MSetHash {

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Combine is never used, yet it is this feature that guarantees that the randomness is the same between the shards; what are the shared randomness tests actually testing ?

// Combine is the group operation: componentwise field addition, hence
// commutative and associative.
func Combine(a, b MSetHash) MSetHash {
a.Add(b)
return a
}

// Identity implements [preflight.AdditiveHasher].
func (Hasher) Identity() MSetHash {
// Identity returns the neutral element of the group, i.e. the empty-set digest.
func Identity() MSetHash {
return MSetHash{}
}

// ToSeed implements [preflight.AdditiveHasher]. It hashes all MSetHashSize
// elements of the accumulator through Poseidon2 and returns the resulting
// octuplet, which is suitable for use as a Fiat-Shamir FS state seed.
func (Hasher) ToSeed(p MSetHash) field.Octuplet {
// ToSeed hashes all MSetHashSize elements of the accumulator through Poseidon2
// and returns the resulting octuplet, which is suitable for use as a
// Fiat-Shamir FS state seed.
func ToSeed(p MSetHash) field.Octuplet {
hsh := poseidon2.NewMDHasher()
hsh.WriteElements(p[:]...)
return hsh.SumDigest()
Expand Down
32 changes: 0 additions & 32 deletions prover-ray/preflight/additive_hasher.go

This file was deleted.

52 changes: 26 additions & 26 deletions prover-ray/preflight/preflight.go
Original file line number Diff line number Diff line change
@@ -1,22 +1,24 @@
// Package preflight implements the pre-phase that establishes a shared

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this package is never used

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but it will eventually be used once we wire it with the arithmetization to concretely compute the shared randomness.

// Fiat-Shamir seed across shards without a coordinator.
// Package preflight implements the pre-phase that establishes γ, the shared
// Fiat-Shamir seed the message bus binds every shard against.
//
// Each shard receives the full collection of cross-shard column sets S_1 …
// S_n. It commits to each set with FRI (obtaining Merkle roots R_1 … R_n),
// maps each root through an [AdditiveHasher] (landing in a commutative group),
// accumulates the sum A = Σ AdditiveHash(R_i), and converts A to a
// [field.Octuplet] via [AdditiveHasher.ToSeed]. Every shard that holds the
// same S_i data produces the same octuplet regardless of processing order,
// because the group operation is commutative.
// [Run] takes the full collection of bus input sets S_1 … S_n — one per shard —
// commits to each with FRI (obtaining Merkle roots R_1 … R_n), maps each root
// into the multiset-hash group, sums them, and compresses the sum to a
// [field.Octuplet]. Because the group operation is commutative, the result does
// not depend on the order the sets are processed in, so no coordinator has to
// impose one.
//
// The octuplet is used as the Fiat-Shamir seed: each shard's prover and
// verifier call [wiop.Runtime.SetFSState] with it inside a
// [wiop.Round.RegisterPreSamplingHook] so the shared challenges α and β are
// derived from an identical state on every participating shard.
// This runs in the orchestrator, once, before any shard proof is produced — not
// inside a proof. It cannot run inside one: it consumes every shard's data,
// while a shard's prover holds only its own, and a verifier holds none at all.
// The resulting γ is handed to each shard as a public input; see
// [github.com/LFDT-Lineth/lineth-monorepo/prover-ray/zkcdriver/risc5.RegisterSharedRandomness]
// for how it enters a shard proof, and why a shard leaves it unconstrained.
package preflight

import (
"github.com/LFDT-Lineth/lineth-monorepo/prover-ray/crypto/koalabear/fri"
multisethashing "github.com/LFDT-Lineth/lineth-monorepo/prover-ray/crypto/koalabear/multiset_hashing"
"github.com/LFDT-Lineth/lineth-monorepo/prover-ray/maths/koalabear/field"
)

Expand All @@ -32,23 +34,21 @@ type BusInputSet struct {
Encoders []*fri.RSEncoder
}

// Run computes the shared Fiat-Shamir seed from a collection of cross-shard
// column sets.
// Run computes γ, the shared Fiat-Shamir seed, from the bus input sets of every
// participating shard.
//
// For each set s it commits to s.Table using s.Encoders (obtaining a Merkle
// root), maps the root through hasher.Hash, and accumulates the results with
// hasher.Combine. The final accumulated value is converted to a [field.Octuplet]
// via hasher.ToSeed.
// root) and accumulates the root; the final accumulated value is compressed
// into the returned octuplet.
//
// The result is deterministic and order-independent as long as hasher.Combine
// is commutative and associative, ensuring every shard computes the same seed.
func Run[P any](sets []BusInputSet, hasher AdditiveHasher[P]) field.Octuplet {
acc := hasher.Identity()
// The result is deterministic and order-independent. Callers must pass the sets
// of *all* shards: a γ computed from a subset binds only that subset, and the
// shards left out would be proving against a seed unrelated to their own data.
func Run(sets []BusInputSet) field.Octuplet {
acc := multisethashing.Identity()
for _, s := range sets {
cs := fri.Commit(s.Encoders, s.Table)
root := cs.Tree.Nodes[0]
a := hasher.Hash(root)
acc = hasher.Combine(acc, a)
acc = multisethashing.Combine(acc, multisethashing.Hash(cs.Tree.Root()))
}
return hasher.ToSeed(acc)
return multisethashing.ToSeed(acc)
}
81 changes: 55 additions & 26 deletions prover-ray/wiop/compilers/messagebus/messagebus.go
Original file line number Diff line number Diff line change
Expand Up @@ -60,12 +60,40 @@ import (
// [Compile] is single-invocation per system.
const PublicInputTag wiop.PublicInputTag = "MessageBus"

// CompileOptions are options for [Compile].
type CompileOptions struct {
// SharedRandomness makes the shard derive α and β from a γ handed to it from
// outside the proof instead of from its own Fiat-Shamir transcript, which is
// what lets several shards agree on those challenges. It declares γ and the
// shard's contribution to it as public inputs and wires the pre-sampling hook
// that seeds the transcript; see [registerSharedRandomness].
//
// Off by default: an unsharded protocol has no one to agree with and derives
// α and β from its own transcript. Turning it on obliges the prover to supply
// γ through [AssignSharedRandomnessSeed] — there is deliberately no default
// value, since a γ known in advance would hand the prover α and β before it
// commits to its bus columns.
//
// Setting it on a system with no message-bus entry does nothing: there is no
// coin round to seed. Nothing is registered, so [HasSharedRandomness] stays
// false and the prover has no γ to supply. A pipeline can therefore turn it on
// ahead of the entries it expects and have it engage the moment they arrive.
SharedRandomness bool
}

// Compile reduces every unreduced [wiop.MessageBus] entry in sys to a
// collection of [wiop.GrandProduct] queries (one per handle) plus one
// [wiop.VerifierAction] per handle that asserts the shard's product equals
// the expected value (one in the unsharded case). See the package
// documentation for the full reduction.
//
// Set [CompileOptions.SharedRandomness] to make α and β derive from a
// cross-shard γ rather than from this shard's transcript. Compile owns that
// wiring because it is the same call that fixes the coin round: registering the
// pre-sampling hook separately would leave the hook and the coins free to land
// on different rounds, which silently desynchronizes the shards rather than
// failing.
//
// The pass appends up to two fresh interactive rounds to sys.Rounds: a
// coin round where the shared α and β are declared, and a result round
// where the [wiop.GrandProduct] result cells and the per-handle verifier
Expand All @@ -87,7 +115,12 @@ const PublicInputTag wiop.PublicInputTag = "MessageBus"
// [wiop.MessageBus.OriginShard] — Compile is a per-shard operation and
// mixing shards in one call is a misuse — or if it is called a second time with
// new entries.
func Compile(sys *wiop.System) {
func Compile(sys *wiop.System, opts ...CompileOptions) {
opt := CompileOptions{}
if len(opts) > 0 {
opt = opts[0]
}

// Collect every unreduced MessageBus entry in declaration order, indexed by
// handle. Sort the handles for deterministic round/coin/cell ordering
// across runs.
Expand All @@ -112,9 +145,16 @@ func Compile(sys *wiop.System) {
}
byHandle[mb.Handle] = append(byHandle[mb.Handle], mb)
}

if len(byHandle) == 0 {
// Nothing left to reduce. A repeat call with no new entries is a
// harmless no-op, whether or not a previous call already ran.
//
// This includes a call that asked for shared randomness: with no entry
// there is no coin round, hence no α or β to seed and no cross-shard
// check to keep consistent, so the request is vacuous rather than a
// misuse. A pipeline may therefore set the option before the bus entries
// it anticipates exist, and have it take effect once they do.
return
}

Expand Down Expand Up @@ -149,19 +189,26 @@ func Compile(sys *wiop.System) {
// ensureRoundAfter reuses any tail round already at this position
// rather than appending a duplicate.

// Find the highest-ID round any participant column touches.
maxParticipantRound := latestParticipantRound(byHandle)
// Pick the slot directly after the participants — allocate a fresh round
// if empty, reuse any round already sitting there. The reuse path is what
// lands α/β on the *same* round a sharded caller pre-allocated for a
// Pick the slot directly after the participants — allocate a fresh round if
// empty, reuse any round already sitting there. The reuse path is what lands
// α/β on the *same* round a sharded caller pre-allocated for a
// PreSamplingHook, so the hook's SetFSState fires immediately before this
// round's coin sampling.
coinRound := ensureRoundAfter(sys, maxParticipantRound)
// round's coin sampling. Going through ensureCoinRound rather than
// open-coding the lookup is what guarantees the caller's pre-allocation and
// this one agree: both are the same call.
coinRound := ensureCoinRound(sys)
// Declare α on that round — sampled by AdvanceRound, after any pre-sampling hook fires.
alpha := coinRound.NewCoinField(compCtx.Childf("alpha"))
// Declare β on the same round, drawn from the same Fiat–Shamir state as α.
beta := coinRound.NewCoinField(compCtx.Childf("beta"))

// Seed that Fiat-Shamir state from a cross-shard γ, if asked. This has to
// happen here rather than in a separate call by the caller: the hook must land
// on the round that carries α and β, and this is where that round is decided.
if opt.SharedRandomness {
registerSharedRandomness(sys, coinRound)
}

// The result round (where GrandProduct cells and the verifier action live)
// sits strictly after the coin round so the GrandProduct prover action sees
// α and β already sampled.
Expand Down Expand Up @@ -227,24 +274,6 @@ func Compile(sys *wiop.System) {
}
}

// latestParticipantRound returns the [wiop.Round] with the highest ID among
// the participant columns of every unreduced MessageBus entry, or nil if no
// entry references a round-bearing leaf.
func latestParticipantRound(byHandle map[string][]*wiop.MessageBus) *wiop.Round {
var best *wiop.Round
update := func(r *wiop.Round) {
if r != nil && (best == nil || r.ID > best.ID) {
best = r
}
}
for _, entries := range byHandle {
for _, mb := range entries {
update(mb.Round())
}
}
return best
}

// ensureRoundAfter returns a round with ID > after.ID, reusing the existing
// tail round when one already sits in that slot; otherwise appending a fresh
// round via sys.NewRound. after may be nil, in which case the returned round
Expand Down
45 changes: 45 additions & 0 deletions prover-ray/wiop/compilers/messagebus/messagebus_coinround.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
package messagebus

import "github.com/LFDT-Lineth/lineth-monorepo/prover-ray/wiop"

// ensureCoinRound returns the round on which [Compile] declares the shared α
// and β coins, allocating it if it does not exist yet.
//
// A sharded protocol needs this round *before* [Compile] runs, so it can
// register a [wiop.Round.RegisterPreSamplingHook] that seeds the Fiat-Shamir
// state with the shared randomness every shard agrees on. [Compile] calls this
// same function rather than repeating the lookup, so the round a caller
// pre-allocated and the round α and β land on are the same by construction.
//
// The result is one past the last bus-impacting round. In the sharded RISC-V
// layout that means: round 0 commits the program verification data, round 1
// commits the columns the message bus reads, and the coins therefore land on
// round 2 — after everything the bus binds, and before the shard-specific data
// that must not influence the shared challenges.
//
// Call it after every [wiop.MessageBus] entry has been declared and before
// [Compile]. The round is derived from the participant columns, so an entry
// declared afterwards can move Compile's choice and leave the hook stranded on
// a round that no longer carries the coins — a divergence that produces
// mismatched challenges across shards rather than an error.
func ensureCoinRound(sys *wiop.System) *wiop.Round {
return ensureRoundAfter(sys, latestUnreducedParticipantRound(sys))
}

// latestUnreducedParticipantRound returns the highest-ID round touched by any
// unreduced [wiop.MessageBus] entry in sys, or nil if no such entry exists.
// It mirrors the logic of [latestParticipantRound] but operates directly on
// sys.MessageBuses rather than on a pre-built by-handle map, so it can be
// called before [Compile] has grouped entries.
func latestUnreducedParticipantRound(sys *wiop.System) *wiop.Round {
var best *wiop.Round
for _, mb := range sys.MessageBuses {
if mb.IsReduced() {
continue
}
if r := mb.Round(); r != nil && (best == nil || r.ID > best.ID) {
best = r
}
}
return best
}
Loading
Loading