readygo67
commented
8 months ago @hussein-aitlahcen, I think current behavior is as expected. below is my understanding step by step.
- The secret is in the func FromBits, which will not check these bits overflow(e.g. >modulus), and it call newInternalElement(limbs, 0), 0 indicate there is no overflow, and it is misleading。
// FromBits returns a new Element given the bits is little-endian order. func (f *Field[T]) FromBits(bs ...frontend.Variable) *Element[T] { nbLimbs := (uint(len(bs)) + f.fParams.BitsPerLimb() - 1) / f.fParams.BitsPerLimb() limbs := make([]frontend.Variable, nbLimbs) for i := uint(0); i < nbLimbs-1; i++ { limbs[i] = bits.FromBinary(f.api, bs[i*f.fParams.BitsPerLimb():(i+1)*f.fParams.BitsPerLimb()]) } limbs[nbLimbs-1] = bits.FromBinary(f.api, bs[(nbLimbs-1)*f.fParams.BitsPerLimb():]) return f.newInternalElement(limbs, 0). //THE 0 is MISLEADING } - IsZero call Reduce to make sure no overflow happens, but in the Reduce, first take a glance at overflow, if it is 0, it think the input has been reduced, so nothing happens.
- IsZero will check the reduced value(e.g. ca) isInRange, because step2, Assert will happen here.
func (f *Field[T]) IsZero(a *Element[T]) frontend.Variable { ca := f.Reduce(a) //CALL Reduce f.AssertIsInRange(ca) res := f.api.IsZero(ca.Limbs[0]) for i := 1; i < len(ca.Limbs); i++ { res = f.api.Mul(res, f.api.IsZero(ca.Limbs[i])) } return res }
func (f Field[T]) Reduce(a Element[T]) *Element[T] { f.enforceWidthConditional(a). if a.overflow == 0 { // fast path - already reduced, omit reduction. //SKIP THE OVERFLOWCHECK return a } // sanity check if _, aConst := f.constantValue(a); aConst { panic("trying to reduce a constant, which happen to have an overflow flag set") } // slow path - use hint to reduce value return f.mulMod(a, f.One(), 0) }
4. *doubleImage = field.Add(image, image)* call *reduceAndOp*, which will check the overflow unconditionally, so the *doubleImage* is reduced before call *IsZero*。
```go
func (f *Field[T]) Add(a, b *Element[T]) *Element[T] {
return f.reduceAndOp(f.add, f.addPreCond, a, b)
}
func (f *Field[T]) reduceAndOp(op func(*Element[T], *Element[T], uint) *Element[T], preCond func(*Element[T], *Element[T]) (uint, error), a, b *Element[T]) *Element[T] {
f.enforceWidthConditional(a)
f.enforceWidthConditional(b)
var nextOverflow uint
var err error
var target overflowError
for nextOverflow, err = preCond(a, b); errors.As(err, &target); nextOverflow, err = preCond(a, b) {
if !target.reduceRight {
a = f.Reduce(a)
} else {
b = f.Reduce(b)
}
}
return op(a, b, nextOverflow)
}I think there are 3 methods to fix this problem,
- make sure the preimage is less or equal than modulus by caller.
- Modify the FromBits function with overflow assumption.
func (f *Field[T]) FromBits(bs ...frontend.Variable) *Element[T] { nbLimbs := (uint(len(bs)) + f.fParams.BitsPerLimb() - 1) / f.fParams.BitsPerLimb() limbs := make([]frontend.Variable, nbLimbs) for i := uint(0); i < nbLimbs-1; i++ { limbs[i] = bits.FromBinary(f.api, bs[i*f.fParams.BitsPerLimb():(i+1)*f.fParams.BitsPerLimb()]) } limbs[nbLimbs-1] = bits.FromBinary(f.api, bs[(nbLimbs-1)*f.fParams.BitsPerLimb():]) return f.newInternalElement(limbs, 1) //Assume overflow happens for safety } - call image = field.Add(image, zero) like below to invoke reduceAndOp to make sure in range.
type C struct {
Preimage [Bytes * 8]frontend.Variable
Image emulated.Element[emulated.BN254Fp]
DoubleImage emulated.Element[emulated.BN254Fp]
}
func (c *C) Define(api frontend.API) error {
field, err := emulated.NewField[emulated.BN254Fp](api)
if err != nil {
return err
}
image := field.FromBits(c.Preimage[:]...) //without overflow check
zero := field.NewElement(0)
image = field.Add(image, zero) //FORCE all
field.AssertIsEqual(image, &c.Image)
doubleImage := field.Add(image, image)
field.AssertIsEqual(doubleImage, &c.DoubleImage)
// Breaks, works with field.IsZero(doubleImage)
field.IsZero(image)
return nil
}
hussein-aitlahcen
Unsure if it's a bug or not but I hit issues when calling
IsZeroafterFromBitswith input bigger than the modulus. I figured thatFromBitscan generate emulated elements with a number of limbs > NbLimbs param of the curve, is it expected? If so,IsZeroshould be passing? Please let me know if I am missing something. On the other hand, addition and multiplication are working, here is a strange snippet whereIsZero(image)is failing andIsZero(doubleImage)is passing: