Skip to content

Commit

Permalink
fix: correct the sr1cs constraints
Browse files Browse the repository at this point in the history
  • Loading branch information
@sorawee
sorawee committed Jan 31, 2024
1 parent a053cd5 commit 18037f3
Show file tree
Hide file tree
Showing 7 changed files with 121 additions and 65 deletions.
1 change: 1 addition & 0 deletions benchmarks/gnark-plonky2-verifier/fixed-int/inverse.unknown.sr1cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
(out 2)
(num-wires 7)
(prime-number 21888242871839275222246405745257275088548364400416034343698204186575808495617)
(extra-constraint (< (var 1) (int 18446744069414584321)))
(extra-constraint (< (var 3) (int 18446744069414584321)))
(extra-constraint (< (var 4) (int 18446744069414584321)))
(extra-constraint (< (var 5) (int 18446744069414584321)))
Expand Down
1 change: 1 addition & 0 deletions benchmarks/gnark-plonky2-verifier/int/inverse.unsafe.sr1cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
(out 2)
(num-wires 7)
(prime-number 21888242871839275222246405745257275088548364400416034343698204186575808495617)
(extra-constraint (< (var 1) (int 18446744069414584321)))
(extra-constraint (< (var 4) (int 18446744069414584321)))
(extra-constraint (< (var 5) (int 18446744069414584321)))
(constraint [(1 3) ] [(1 1) ] [(1 6) ])
Expand Down
154 changes: 89 additions & 65 deletions benchmarks/gnark-plonky2-verifier/pure/inverse.timeout.sr1cs
View file
Original file line number Diff line number Diff line change
@@ -1,73 +1,97 @@
(in 1)
(out 2)
(num-wires 114)
(num-wires 151)
(prime-number 21888242871839275222246405745257275088548364400416034343698204186575808495617)
(constraint [(1 3) ] [(1 1) ] [(1 6) ])
(constraint [(1 0) ] [(1 6) ] [(18446744069414584321 4) (1 5) ])
(constraint [(1 0) ] [(4294967296 7) (1 8) ] [(1 4) ])
(constraint [(1 10) ] [(4294967295 0) (-1 7) ] [(-1 0) (1 9) ])
(constraint [(1 9) ] [(21888242871839275222246405745257275088548364400416034343698204186571513528322 0) (1 7) ] [(0 0) ])
(constraint [(1 9) ] [(1 0) (-1 9) ] [(0 0) ])
(constraint [(1 9) ] [(1 8) ] [(1 11) ])
(constraint [(1 0) ] [(1 11) ] [(0 0) ])
(constraint [(1 0) ] [(4294967296 12) (1 13) ] [(1 5) ])
(constraint [(1 0) ] [(4294967296 3) (1 4) ] [(1 1) ])
(constraint [(1 6) ] [(4294967295 0) (-1 3) ] [(-1 0) (1 5) ])
(constraint [(1 5) ] [(21888242871839275222246405745257275088548364400416034343698204186571513528322 0) (1 3) ] [(0 0) ])
(constraint [(1 5) ] [(1 0) (-1 5) ] [(0 0) ])
(constraint [(1 5) ] [(1 4) ] [(1 7) ])
(constraint [(1 0) ] [(1 7) ] [(0 0) ])
(constraint [(1 8) ] [(1 1) ] [(1 11) ])
(constraint [(1 0) ] [(1 11) ] [(18446744069414584321 9) (1 10) ])
(constraint [(1 0) ] [(4294967296 12) (1 13) ] [(1 9) ])
(constraint [(1 15) ] [(4294967295 0) (-1 12) ] [(-1 0) (1 14) ])
(constraint [(1 14) ] [(21888242871839275222246405745257275088548364400416034343698204186571513528322 0) (1 12) ] [(0 0) ])
(constraint [(1 14) ] [(1 0) (-1 14) ] [(0 0) ])
(constraint [(1 14) ] [(1 13) ] [(1 16) ])
(constraint [(1 0) ] [(1 16) ] [(0 0) ])
(constraint [(1 0) ] [(1 5) ] [(1 0) ])
(constraint [(1 0) ] [(1 3) ] [(1 2) ])
(constraint [(1 0) ] [(1 17) (16 18) (256 19) (4096 20) (65536 21) (1048576 22) (16777216 23) (268435456 24) ] [(1 7) ])
(constraint [(1 0) ] [(1 25) (16 26) (256 27) (4096 28) (65536 29) (1048576 30) (16777216 31) (268435456 32) ] [(1 8) ])
(constraint [(1 0) ] [(1 33) (16 34) (256 35) (4096 36) (65536 37) (1048576 38) (16777216 39) (268435456 40) ] [(1 12) ])
(constraint [(1 0) ] [(1 41) (16 42) (256 43) (4096 44) (65536 45) (1048576 46) (16777216 47) (268435456 48) ] [(1 13) ])
(constraint [(1 65) ] [(1 66) ] [(1 49) ])
(constraint [(1 67) ] [(-1 0) (1 65) ] [(1 50) ])
(constraint [(1 68) ] [(-2 0) (1 65) ] [(1 51) ])
(constraint [(1 69) ] [(-3 0) (1 65) ] [(1 52) ])
(constraint [(1 70) ] [(-4 0) (1 65) ] [(1 53) ])
(constraint [(1 71) ] [(-5 0) (1 65) ] [(1 54) ])
(constraint [(1 72) ] [(-6 0) (1 65) ] [(1 55) ])
(constraint [(1 73) ] [(-7 0) (1 65) ] [(1 56) ])
(constraint [(1 74) ] [(-8 0) (1 65) ] [(1 57) ])
(constraint [(1 75) ] [(-9 0) (1 65) ] [(1 58) ])
(constraint [(1 76) ] [(-10 0) (1 65) ] [(1 59) ])
(constraint [(1 77) ] [(-11 0) (1 65) ] [(1 60) ])
(constraint [(1 78) ] [(-12 0) (1 65) ] [(1 61) ])
(constraint [(1 79) ] [(-13 0) (1 65) ] [(1 62) ])
(constraint [(1 80) ] [(-14 0) (1 65) ] [(1 63) ])
(constraint [(1 81) ] [(-15 0) (1 65) ] [(1 64) ])
(constraint [(1 82) ] [(-1 17) (1 65) ] [(1 0) ])
(constraint [(1 83) ] [(-1 18) (1 65) ] [(1 0) ])
(constraint [(1 84) ] [(-1 19) (1 65) ] [(1 0) ])
(constraint [(1 85) ] [(-1 20) (1 65) ] [(1 0) ])
(constraint [(1 86) ] [(-1 21) (1 65) ] [(1 0) ])
(constraint [(1 87) ] [(-1 22) (1 65) ] [(1 0) ])
(constraint [(1 88) ] [(-1 23) (1 65) ] [(1 0) ])
(constraint [(1 89) ] [(-1 24) (1 65) ] [(1 0) ])
(constraint [(1 90) ] [(-1 25) (1 65) ] [(1 0) ])
(constraint [(1 91) ] [(-1 26) (1 65) ] [(1 0) ])
(constraint [(1 92) ] [(-1 27) (1 65) ] [(1 0) ])
(constraint [(1 93) ] [(-1 28) (1 65) ] [(1 0) ])
(constraint [(1 94) ] [(-1 29) (1 65) ] [(1 0) ])
(constraint [(1 95) ] [(-1 30) (1 65) ] [(1 0) ])
(constraint [(1 96) ] [(-1 31) (1 65) ] [(1 0) ])
(constraint [(1 97) ] [(-1 32) (1 65) ] [(1 0) ])
(constraint [(1 98) ] [(-1 33) (1 65) ] [(1 0) ])
(constraint [(1 99) ] [(-1 34) (1 65) ] [(1 0) ])
(constraint [(1 100) ] [(-1 35) (1 65) ] [(1 0) ])
(constraint [(1 101) ] [(-1 36) (1 65) ] [(1 0) ])
(constraint [(1 102) ] [(-1 37) (1 65) ] [(1 0) ])
(constraint [(1 103) ] [(-1 38) (1 65) ] [(1 0) ])
(constraint [(1 104) ] [(-1 39) (1 65) ] [(1 0) ])
(constraint [(1 105) ] [(-1 40) (1 65) ] [(1 0) ])
(constraint [(1 106) ] [(-1 41) (1 65) ] [(1 0) ])
(constraint [(1 107) ] [(-1 42) (1 65) ] [(1 0) ])
(constraint [(1 108) ] [(-1 43) (1 65) ] [(1 0) ])
(constraint [(1 109) ] [(-1 44) (1 65) ] [(1 0) ])
(constraint [(1 110) ] [(-1 45) (1 65) ] [(1 0) ])
(constraint [(1 111) ] [(-1 46) (1 65) ] [(1 0) ])
(constraint [(1 112) ] [(-1 47) (1 65) ] [(1 0) ])
(constraint [(1 113) ] [(-1 48) (1 65) ] [(1 0) ])
(constraint [(1 0) ] [(1 66) (1 67) (1 68) (1 69) (1 70) (1 71) (1 72) (1 73) (1 74) (1 75) (1 76) (1 77) (1 78) (1 79) (1 80) (1 81) ] [(1 82) (1 83) (1 84) (1 85) (1 86) (1 87) (1 88) (1 89) (1 90) (1 91) (1 92) (1 93) (1 94) (1 95) (1 96) (1 97) (1 98) (1 99) (1 100) (1 101) (1 102) (1 103) (1 104) (1 105) (1 106) (1 107) (1 108) (1 109) (1 110) (1 111) (1 112) (1 113) ])
(constraint [(1 0) ] [(4294967296 17) (1 18) ] [(1 10) ])
(constraint [(1 20) ] [(4294967295 0) (-1 17) ] [(-1 0) (1 19) ])
(constraint [(1 19) ] [(21888242871839275222246405745257275088548364400416034343698204186571513528322 0) (1 17) ] [(0 0) ])
(constraint [(1 19) ] [(1 0) (-1 19) ] [(0 0) ])
(constraint [(1 19) ] [(1 18) ] [(1 21) ])
(constraint [(1 0) ] [(1 21) ] [(0 0) ])
(constraint [(1 0) ] [(1 10) ] [(1 0) ])
(constraint [(1 0) ] [(1 8) ] [(1 2) ])
(constraint [(1 0) ] [(1 22) (16 23) (256 24) (4096 25) (65536 26) (1048576 27) (16777216 28) (268435456 29) ] [(1 3) ])
(constraint [(1 0) ] [(1 30) (16 31) (256 32) (4096 33) (65536 34) (1048576 35) (16777216 36) (268435456 37) ] [(1 4) ])
(constraint [(1 0) ] [(1 38) (16 39) (256 40) (4096 41) (65536 42) (1048576 43) (16777216 44) (268435456 45) ] [(1 12) ])
(constraint [(1 0) ] [(1 46) (16 47) (256 48) (4096 49) (65536 50) (1048576 51) (16777216 52) (268435456 53) ] [(1 13) ])
(constraint [(1 0) ] [(1 54) (16 55) (256 56) (4096 57) (65536 58) (1048576 59) (16777216 60) (268435456 61) ] [(1 17) ])
(constraint [(1 0) ] [(1 62) (16 63) (256 64) (4096 65) (65536 66) (1048576 67) (16777216 68) (268435456 69) ] [(1 18) ])
(constraint [(1 86) ] [(1 87) ] [(1 70) ])
(constraint [(1 88) ] [(-1 0) (1 86) ] [(1 71) ])
(constraint [(1 89) ] [(-2 0) (1 86) ] [(1 72) ])
(constraint [(1 90) ] [(-3 0) (1 86) ] [(1 73) ])
(constraint [(1 91) ] [(-4 0) (1 86) ] [(1 74) ])
(constraint [(1 92) ] [(-5 0) (1 86) ] [(1 75) ])
(constraint [(1 93) ] [(-6 0) (1 86) ] [(1 76) ])
(constraint [(1 94) ] [(-7 0) (1 86) ] [(1 77) ])
(constraint [(1 95) ] [(-8 0) (1 86) ] [(1 78) ])
(constraint [(1 96) ] [(-9 0) (1 86) ] [(1 79) ])
(constraint [(1 97) ] [(-10 0) (1 86) ] [(1 80) ])
(constraint [(1 98) ] [(-11 0) (1 86) ] [(1 81) ])
(constraint [(1 99) ] [(-12 0) (1 86) ] [(1 82) ])
(constraint [(1 100) ] [(-13 0) (1 86) ] [(1 83) ])
(constraint [(1 101) ] [(-14 0) (1 86) ] [(1 84) ])
(constraint [(1 102) ] [(-15 0) (1 86) ] [(1 85) ])
(constraint [(1 103) ] [(-1 22) (1 86) ] [(1 0) ])
(constraint [(1 104) ] [(-1 23) (1 86) ] [(1 0) ])
(constraint [(1 105) ] [(-1 24) (1 86) ] [(1 0) ])
(constraint [(1 106) ] [(-1 25) (1 86) ] [(1 0) ])
(constraint [(1 107) ] [(-1 26) (1 86) ] [(1 0) ])
(constraint [(1 108) ] [(-1 27) (1 86) ] [(1 0) ])
(constraint [(1 109) ] [(-1 28) (1 86) ] [(1 0) ])
(constraint [(1 110) ] [(-1 29) (1 86) ] [(1 0) ])
(constraint [(1 111) ] [(-1 30) (1 86) ] [(1 0) ])
(constraint [(1 112) ] [(-1 31) (1 86) ] [(1 0) ])
(constraint [(1 113) ] [(-1 32) (1 86) ] [(1 0) ])
(constraint [(1 114) ] [(-1 33) (1 86) ] [(1 0) ])
(constraint [(1 115) ] [(-1 34) (1 86) ] [(1 0) ])
(constraint [(1 116) ] [(-1 35) (1 86) ] [(1 0) ])
(constraint [(1 117) ] [(-1 36) (1 86) ] [(1 0) ])
(constraint [(1 118) ] [(-1 37) (1 86) ] [(1 0) ])
(constraint [(1 119) ] [(-1 38) (1 86) ] [(1 0) ])
(constraint [(1 120) ] [(-1 39) (1 86) ] [(1 0) ])
(constraint [(1 121) ] [(-1 40) (1 86) ] [(1 0) ])
(constraint [(1 122) ] [(-1 41) (1 86) ] [(1 0) ])
(constraint [(1 123) ] [(-1 42) (1 86) ] [(1 0) ])
(constraint [(1 124) ] [(-1 43) (1 86) ] [(1 0) ])
(constraint [(1 125) ] [(-1 44) (1 86) ] [(1 0) ])
(constraint [(1 126) ] [(-1 45) (1 86) ] [(1 0) ])
(constraint [(1 127) ] [(-1 46) (1 86) ] [(1 0) ])
(constraint [(1 128) ] [(-1 47) (1 86) ] [(1 0) ])
(constraint [(1 129) ] [(-1 48) (1 86) ] [(1 0) ])
(constraint [(1 130) ] [(-1 49) (1 86) ] [(1 0) ])
(constraint [(1 131) ] [(-1 50) (1 86) ] [(1 0) ])
(constraint [(1 132) ] [(-1 51) (1 86) ] [(1 0) ])
(constraint [(1 133) ] [(-1 52) (1 86) ] [(1 0) ])
(constraint [(1 134) ] [(-1 53) (1 86) ] [(1 0) ])
(constraint [(1 135) ] [(-1 54) (1 86) ] [(1 0) ])
(constraint [(1 136) ] [(-1 55) (1 86) ] [(1 0) ])
(constraint [(1 137) ] [(-1 56) (1 86) ] [(1 0) ])
(constraint [(1 138) ] [(-1 57) (1 86) ] [(1 0) ])
(constraint [(1 139) ] [(-1 58) (1 86) ] [(1 0) ])
(constraint [(1 140) ] [(-1 59) (1 86) ] [(1 0) ])
(constraint [(1 141) ] [(-1 60) (1 86) ] [(1 0) ])
(constraint [(1 142) ] [(-1 61) (1 86) ] [(1 0) ])
(constraint [(1 143) ] [(-1 62) (1 86) ] [(1 0) ])
(constraint [(1 144) ] [(-1 63) (1 86) ] [(1 0) ])
(constraint [(1 145) ] [(-1 64) (1 86) ] [(1 0) ])
(constraint [(1 146) ] [(-1 65) (1 86) ] [(1 0) ])
(constraint [(1 147) ] [(-1 66) (1 86) ] [(1 0) ])
(constraint [(1 148) ] [(-1 67) (1 86) ] [(1 0) ])
(constraint [(1 149) ] [(-1 68) (1 86) ] [(1 0) ])
(constraint [(1 150) ] [(-1 69) (1 86) ] [(1 0) ])
(constraint [(1 0) ] [(1 87) (1 88) (1 89) (1 90) (1 91) (1 92) (1 93) (1 94) (1 95) (1 96) (1 97) (1 98) (1 99) (1 100) (1 101) (1 102) ] [(1 103) (1 104) (1 105) (1 106) (1 107) (1 108) (1 109) (1 110) (1 111) (1 112) (1 113) (1 114) (1 115) (1 116) (1 117) (1 118) (1 119) (1 120) (1 121) (1 122) (1 123) (1 124) (1 125) (1 126) (1 127) (1 128) (1 129) (1 130) (1 131) (1 132) (1 133) (1 134) (1 135) (1 136) (1 137) (1 138) (1 139) (1 140) (1 141) (1 142) (1 143) (1 144) (1 145) (1 146) (1 147) (1 148) (1 149) (1 150) ])
9 changes: 9 additions & 0 deletions benchmarks/gnark-plonky2-verifier/src/exp.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,15 @@ func (c *TestGoldilocksExpCircuit) Define(api frontend.API) error {
glApi := goldilocks.New(api)
var e *big.Int
e = big.NewInt(32)

// technically, we should add an assumption that c.X is in the field
//
// glApi.RangeCheck(c.X)
// goldilocks.RangeCheck(c.X.Limb)
//
// but since it's already deemed safe even without the assumption,
// we will leave it at that.

glApi.AssertIsEqual(glApi.Exp(c.X, e), c.Y)
return nil
}
4 changes: 4 additions & 0 deletions benchmarks/gnark-plonky2-verifier/src/inverse.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,10 @@ func (c *TestGoldilocksInverseCircuit) Define(api frontend.API) error {
annotateGVarIn(c.X)
annotateGVarOut(c.Y)
glApi := goldilocks.New(api)

glApi.RangeCheck(c.X)
// goldilocks.RangeCheck(c.X.Limb)

glApi.AssertIsEqual(glApi.Inverse(c.X), c.Y)
return nil
}
15 changes: 15 additions & 0 deletions benchmarks/gnark-plonky2-verifier/src/mul-add.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,21 @@ func (c *TestGoldilocksMulAddCircuit) Define(api frontend.API) error {
annotateGVarIn(c.Z)
annotateGVarOut(c.ExpectedResult)
glApi := goldilocks.New(api)

// technically, we should add an assumption that c.X, c.Y, and c.Z
// are in the field
//
// glApi.RangeCheck(c.X)
// glApi.RangeCheck(c.Y)
// glApi.RangeCheck(c.Z)
//
// goldilocks.RangeCheck(c.X.Limb)
// goldilocks.RangeCheck(c.Y.Limb)
// goldilocks.RangeCheck(c.Z.Limb)
//
// but since it's already deemed safe even without the assumption,
// we will leave it at that.

glApi.AssertIsEqual(glApi.MulAdd(c.X, c.Y, c.Z), c.ExpectedResult)
return nil
}
2 changes: 2 additions & 0 deletions changelogs/unreleased/24-01-31-correct-sr1cs-cnsts.yaml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
fixed:
- Fixed sr1cs constraints in the benchmark not having proper assumptions

0 comments on commit 18037f3

Please sign in to comment.