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
9 changes: 9 additions & 0 deletions std/algebra/emulated/sw_bw6761/pairing.go
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,15 @@ func (pr *Pairing) AssertFinalExponentiationIsOne(x *GTEl) {
A5: *res[5],
}

// Constrain residueWitness to be invertible (non-zero). The check below,
// x == residueWitness^Λ, is homogeneous in the hint output, so for x == 0
// the all-zero residue witness would satisfy it: the exponentiation chain
// degenerates to 0 and DivUnchecked(0, 0) only enforces 0 = quotient·0,
// leaving the quotient free. But 0 is not in the multiplicative target
// group and its final exponentiation is not one. Inverse asserts
// residueWitness·residueWitness⁻¹ == 1, ruling that out.
pr.Ext6.Inverse(&residueWitness)

// Check that x == residueWitness^Λ
// where Λ = x₀+1+p(x₀³-x₀²-x₀) and residueWitness from the hint.

Expand Down
32 changes: 32 additions & 0 deletions std/algebra/emulated/sw_bw6761/pairing_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -126,6 +126,38 @@ func TestFinalExponentiationIsOneSoundness(t *testing.T) {
assert.Error(err)
}

// assertFinalExponentiationIsOneDirectCircuit asserts the final-exponentiation
// property of a witness-supplied accumulator, as in
// https://eprint.iacr.org/2024/640.pdf Section 4 where the Miller loop output
// is a prover input.
type assertFinalExponentiationIsOneDirectCircuit struct {
InGt GTEl
}

func (c *assertFinalExponentiationIsOneDirectCircuit) Define(api frontend.API) error {
pairing, err := NewPairing(api)
if err != nil {
return fmt.Errorf("new pairing: %w", err)
}
pairing.AssertFinalExponentiationIsOne(&c.InGt)
return nil
}

// TestFinalExponentiationIsOneRejectsZeroAccumulator is a regression for the
// zero-residue-witness underconstraint: the check x == residueWitness^Λ is
// homogeneous in the hint output, so for a zero accumulator (x = 0, which is
// not in the multiplicative target group — its final exponentiation is 0, not
// 1) the all-zero residue witness degenerated the exponentiation chain and the
// unchecked division to 0 == 0 and was accepted. The invertibility anchor
// (residueWitness·residueWitness⁻¹ == 1) now rejects it.
func TestFinalExponentiationIsOneRejectsZeroAccumulator(t *testing.T) {
assert := test.NewAssert(t)
var zero bw6761.GT // = 0
witness := assertFinalExponentiationIsOneDirectCircuit{InGt: NewGTEl(zero)}
err := test.IsSolved(&assertFinalExponentiationIsOneDirectCircuit{}, &witness, ecc.BN254.ScalarField())
assert.Error(err, "zero accumulator must be rejected: Inverse(0) anchor is unsatisfiable")
}

type FinalExponentiationCircuit struct {
InGt GTEl
Res GTEl
Expand Down
Loading