Light Client Circuit

Before reading this section, make sure that you are familiar with Gnark. In this chapter, we will analyze a light client circuit, verifying a modified Tendermint consensus (CometBLS).

At the heart of our light client is a data structure representing validators and their signatures:

type Validator struct {
	HashableX    frontend.Variable
	HashableXMSB frontend.Variable
	HashableY    frontend.Variable
	HashableYMSB frontend.Variable
	Power        frontend.Variable
}

type TendermintLightClientInput struct {
	Sig           gadget.G2Affine
	Validators    [MaxVal]Validator
	NbOfVal       frontend.Variable
	NbOfSignature frontend.Variable
	Bitmap        frontend.Variable
}

Each validator is represented by its public key coordinates (stored in a special format to work within field size limitations) and voting power. The TendermintLightClientInput combines these validators with signature data and metadata such as the number of validators and a bitmap indicating which validators have signed. This is the equivalent of our LightClientHeader as seen in the light client chapter.

The circuit uses several helper functions to efficiently manipulate large field elements:

// Given a variable of size N and limbs of size M, split the variable in N/M limbs.
func Unpack(api frontend.API, packed frontend.Variable, sizeOfInput int, sizeOfElem int) []frontend.Variable {
	nbOfElems := sizeOfInput / sizeOfElem
	if sizeOfElem == 1 {
		return api.ToBinary(packed, nbOfElems)
	} else {
		unpacked := api.ToBinary(packed, sizeOfInput)
		elems := make([]frontend.Variable, nbOfElems)
		for i := 0; i < nbOfElems; i++ {
			elems[i] = api.FromBinary(unpacked[i*sizeOfElem : (i+1)*sizeOfElem]...)
		}
		return elems
	}
}

// Reconstruct a value from it's limbs.
func Repack(api frontend.API, unpacked []frontend.Variable, sizeOfInput int, sizeOfElem int) []frontend.Variable {
	nbOfElems := sizeOfInput / sizeOfElem
	elems := make([]frontend.Variable, nbOfElems)
	for i := 0; i < nbOfElems; i++ {
		elems[i] = api.FromBinary(unpacked[i*sizeOfElem : (i+1)*sizeOfElem]...)
	}
	return elems
}

The Unpack function splits a variable into smaller components, while Repack does the opposite. These functions are needed when working with cryptographic values that exceed the size of the prime field.

The core logic of the light client is in the Verify method:

// Union whitepaper: Algorithm 2. procedure V
func (lc *TendermintLightClientAPI) Verify(message *gadget.G2Affine, expectedValRoot frontend.Variable, powerNumerator frontend.Variable, powerDenominator frontend.Variable) error {

This function verifies that:

The validator set matches a known root hash
A sufficient number of validators (by voting power) have signed
The signature is cryptographically valid

Let's break down the steps in the verification process:

lc.api.AssertIsLessOrEqual(lc.input.NbOfVal, MaxVal)
lc.api.AssertIsLessOrEqual(lc.input.NbOfSignature, lc.input.NbOfVal)
// Ensure that at least one validator/signature are provided
lc.api.AssertIsLessOrEqual(1, lc.input.NbOfSignature)

These constraints ensure basic properties: the number of validators doesn't exceed the maximum, the number of signatures doesn't exceed the number of validators, and there's at least one signature. Next the circuit defines a helper closure with logic to be executed for each validator.

// Facility to iterate over the validators in the lc, this function will
// do the necessary decoding/marshalling for the caller.
//
// This function will reconstruct each validator from the secret inputs by:
// - re-composing the public key from its shifted/msb values
forEachVal := func(f func(i int, signed frontend.Variable, cannotSign frontend.Variable, publicKey *gadget.G1Affine, power frontend.Variable, leaf frontend.Variable) error) error {
...

Note that the function accepts another closure, which it will call after reconstructing some values and adding constraints.

Inside this function, for each validator, we:

Compute a hash of the validator's data (similar to a Merkle leaf)

validator := lc.input.Validators[i]
h, err := mimc.NewMiMC(lc.api)
if err != nil {
	return fmt.Errorf("new mimc: %w", err)
}
// Union whitepaper: (11) H_pre
//
h.Write(validator.HashableX, validator.HashableY, validator.HashableXMSB, validator.HashableYMSB, validator.Power)
leaf := h.Sum()

Reconstruct the full public key by combining its components

// Reconstruct the public key from the merkle leaf
/*
   pk = (val.pk.X | (val.pk.XMSB << 253), val.pk.Y | (val.pk.YMSB << 253))
*/
shiftedX := Unpack(lc.api, validator.HashableX, 256, 1)
shiftedX[253] = validator.HashableXMSB
unshiftedX := Repack(lc.api, shiftedX, 256, 64)

shiftedY := Unpack(lc.api, validator.HashableY, 256, 1)
shiftedY[253] = validator.HashableYMSB
unshiftedY := Repack(lc.api, shiftedY, 256, 64)

var rebuiltPublicKey gadget.G1Affine
rebuiltPublicKey.X.Limbs = unshiftedX
rebuiltPublicKey.Y.Limbs = unshiftedY

Determine if this validator has signed by checking the bitmap

cannotSign := lc.api.IsZero(bitmapMask)

Apply the provided function to process this validator. This is where we pass an additional closure to calculate aggregated values over the entire validator set. This is a pattern often used in functional programming.

aggregatedPublicKey, nbOfKeys, err := bls.WithAggregation(
	func(aggregate func(selector frontend.Variable, publicKey *sw_emulated.AffinePoint[emulated.BN254Fp])) error {
		if err := forEachVal(func(i int, signed frontend.Variable, cannotSign frontend.Variable, publicKey *gadget.G1Affine, power frontend.Variable, leaf frontend.Variable) error {
			actuallySigned := lc.api.Select(cannotSign, 0, signed)
			// totalVotingPower = totalVotingPower + power
			totalVotingPower = lc.api.Add(totalVotingPower, lc.api.Select(cannotSign, 0, power))
			// currentVotingPower = currentVotingPower + if signed then power else 0
			currentVotingPower = lc.api.Add(currentVotingPower, lc.api.Select(actuallySigned, power, 0))
			// Optionally aggregated public key if validator at index signed
			aggregate(actuallySigned, publicKey)
			leafHashes[i] = lc.api.Select(cannotSign, 0, merkle.LeafHash([]frontend.Variable{leaf}))
			return nil
		}); err != nil {
			return err
		}
		return nil
	})
if err != nil {
	return err
}

The aggregated values of interest are:

totalVotingPower := frontend.Variable(0)
currentVotingPower := frontend.Variable(0)

We sum the voting power, since we do not want to verify that 2/3 validators attested the block, but that 2/3 of the voting power attested to it. In Tendermint based chains, validators can have a variable amount of stake, as opposed to Ethereum, where it is always 32 ETH.

Finally we verify the aggregated values.

// Ensure that we actually aggregated the correct number of signatures
lc.api.AssertIsEqual(nbOfKeys, lc.input.NbOfSignature)

// Ensure that the current sum of voting power exceed the expected threshold
votingPowerNeeded := lc.api.Mul(totalVotingPower, powerNumerator)
currentVotingPowerScaled := lc.api.Mul(currentVotingPower, powerDenominator)
lc.api.AssertIsLessOrEqual(votingPowerNeeded, currentVotingPowerScaled)

// Verify that the merkle root is equal to the given root (public input)
rootHash := merkle.RootHash(leafHashes, lc.input.NbOfVal)
lc.api.AssertIsEqual(expectedValRoot, rootHash)

return bls.VerifySignature(aggregatedPublicKey, message, &lc.input.Sig)

These verify that:

The claimed number of signatures matches the actual count.
The voting power of signers exceeds the required threshold (expressed as a fraction).
The validator set matches a known Merkle root.

Much like our Sudoku example, this circuit defines a relationship between public inputs (the expected validator root, message, and signature) and private witness data (the validator set details). When we generate a proof, we're demonstrating knowledge of a valid validator set that signed the message, without revealing the validator details.

This chapter does not cover some of the cryptographic primitives that had to be implemented to perform hashing or BLS aggregation and verification. Those can be found here.

Next we will explore the trusted setup ceremony, an alternative to doing an unsafe setup. All custom circuits that produce SNARKs require one.

Interop: Principles, Techniques, and Tools

Light Client Circuit