From 6ced47593781f5714570f8511aad010bfa2a0eb2 Mon Sep 17 00:00:00 2001 From: Gregor Mitscha-Baude Date: Wed, 6 Mar 2024 23:47:14 +0100 Subject: [PATCH 01/41] assertBoolean --- src/lib/bool.ts | 3 ++- src/lib/field.ts | 3 ++- src/lib/gadgets/basic.ts | 6 +++--- src/snarky.d.ts | 4 ---- 4 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/lib/bool.ts b/src/lib/bool.ts index 8957e89d53..6645165d2e 100644 --- a/src/lib/bool.ts +++ b/src/lib/bool.ts @@ -10,6 +10,7 @@ import { Bool as B } from '../provable/field-bigint.js'; import { defineBinable } from '../bindings/lib/binable.js'; import { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver } from './provable-context.js'; +import { assertBoolean } from './gadgets/basic.js'; export { BoolVar, Bool }; @@ -321,7 +322,7 @@ class Bool { static sizeInBytes = 1; static check(x: Bool): void { - Snarky.field.assertBoolean(x.value); + assertBoolean(x.toField()); } static Unsafe = { diff --git a/src/lib/field.ts b/src/lib/field.ts index 0e643cb2a5..261d8b9651 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,6 +5,7 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; +import { assertBoolean } from './gadgets/basic.js'; // external API export { Field }; @@ -898,7 +899,7 @@ class Field { } return; } - Snarky.field.assertBoolean(this.value); + assertBoolean(this); } catch (err) { throw withMessage(err, message); } diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index 4db98792bc..8595b4a242 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -6,15 +6,15 @@ import type { Field, VarField } from '../field.js'; import { existsOne, toVar } from './common.js'; import { Gates } from '../gates.js'; import { TupleN } from '../util/types.js'; -import { Snarky } from '../../snarky.js'; export { assertBoolean, arrayGet, assertOneOf }; /** * Assert that x is either 0 or 1. */ -function assertBoolean(x: VarField) { - Snarky.field.assertBoolean(x.value); +function assertBoolean(x_: Field) { + let x = toVar(x_); + assertBilinear(x, x, [1n, -1n, 0n, 0n]); } // TODO: create constant versions of these and expose on Gadgets diff --git a/src/snarky.d.ts b/src/snarky.d.ts index e11a2ccf63..8d38ed3bf5 100644 --- a/src/snarky.d.ts +++ b/src/snarky.d.ts @@ -249,10 +249,6 @@ declare const Snarky: { * x*x === y without handling of constants */ assertSquare(x: FieldVar, y: FieldVar): void; - /** - * x*x === x without handling of constants - */ - assertBoolean(x: FieldVar): void; /** * check x < y and x <= y */ From 6f80c5c835c1dc5a34075f9d14136ca97e9fa4fd Mon Sep 17 00:00:00 2001 From: Gregor Mitscha-Baude Date: Wed, 6 Mar 2024 23:57:41 +0100 Subject: [PATCH 02/41] ofField -> fromField and some cleanup --- src/lib/bool.ts | 9 ++++----- src/lib/field.ts | 6 ++---- src/lib/gadgets/arithmetic.ts | 3 +-- src/lib/gadgets/bit-slices.ts | 4 ++-- src/lib/gadgets/elliptic-curve.ts | 12 ++++++------ 5 files changed, 15 insertions(+), 19 deletions(-) diff --git a/src/lib/bool.ts b/src/lib/bool.ts index 6645165d2e..5f6ae05dbe 100644 --- a/src/lib/bool.ts +++ b/src/lib/bool.ts @@ -10,7 +10,6 @@ import { Bool as B } from '../provable/field-bigint.js'; import { defineBinable } from '../bindings/lib/binable.js'; import { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver } from './provable-context.js'; -import { assertBoolean } from './gadgets/basic.js'; export { BoolVar, Bool }; @@ -322,19 +321,19 @@ class Bool { static sizeInBytes = 1; static check(x: Bool): void { - assertBoolean(x.toField()); + x.toField().assertBool(); } static Unsafe = { /** - * Converts a {@link Field} into a {@link Bool}. This is a **dangerous** operation + * Converts a {@link Field} into a {@link Bool}. This is an **unsafe** operation * as it assumes that the field element is either 0 or 1 (which might not be true). * - * Only use this with constants or if you have already constrained the Field element to be 0 or 1. + * Only use this if you have already constrained the Field element to be 0 or 1. * * @param x a {@link Field} */ - ofField(x: Field) { + fromField(x: Field) { asProver(() => { let x0 = x.toBigInt(); if (x0 !== 0n && x0 !== 1n) diff --git a/src/lib/field.ts b/src/lib/field.ts index 261d8b9651..84002145e2 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -882,12 +882,10 @@ class Field { } /** - * Assert that this {@link Field} is equal to 1 or 0 as a "field-like" value. - * Calling this function is equivalent to `Bool.or(Field(...).equals(1), Field(...).equals(0)).assertEquals(Bool(true))`. + * Prove that this {@link Field} is equal to 0 or 1. * - * **Important**: If an assertion fails, the code throws an error. + * If the assertion fails, the code throws an error. * - * @param value - the "field-like" value to compare & assert with this {@link Field}. * @param message? - a string error message to print if the assertion fails, optional. */ assertBool(message?: string) { diff --git a/src/lib/gadgets/arithmetic.ts b/src/lib/gadgets/arithmetic.ts index e5c07e6b76..9d7cac4f6c 100644 --- a/src/lib/gadgets/arithmetic.ts +++ b/src/lib/gadgets/arithmetic.ts @@ -1,4 +1,3 @@ -import { Bool } from '../bool.js'; import { provableTuple } from '../circuit-value.js'; import { Field } from '../core.js'; import { assert } from '../errors.js'; @@ -34,7 +33,7 @@ function divMod32(n: Field, quotientBits = 32) { ); if (quotientBits === 1) { - Bool.check(Bool.Unsafe.ofField(quotient)); + quotient.assertBool(); } else { rangeCheckN(quotientBits, quotient); } diff --git a/src/lib/gadgets/bit-slices.ts b/src/lib/gadgets/bit-slices.ts index 0672e1aeb5..a83882e040 100644 --- a/src/lib/gadgets/bit-slices.ts +++ b/src/lib/gadgets/bit-slices.ts @@ -123,7 +123,7 @@ function sliceField( let remainingChunk = Field.from(0n); for (let i = 0; i < size; i++) { let bit = bits[i]; - Bool.check(Bool.Unsafe.ofField(bit)); + bit.assertBool(); remainingChunk = remainingChunk.add(bit.mul(1n << BigInt(i))); } sum = remainingChunk = remainingChunk.seal(); @@ -141,7 +141,7 @@ function sliceField( let size = Math.min(maxBits - i, chunkSize); // last chunk might be smaller for (let j = 0; j < size; j++) { let bit = bits[i + j]; - Bool.check(Bool.Unsafe.ofField(bit)); + bit.assertBool(); chunk = chunk.add(bit.mul(1n << BigInt(j))); } chunk = chunk.seal(); diff --git a/src/lib/gadgets/elliptic-curve.ts b/src/lib/gadgets/elliptic-curve.ts index ab37aa5fcb..3db54dcc11 100644 --- a/src/lib/gadgets/elliptic-curve.ts +++ b/src/lib/gadgets/elliptic-curve.ts @@ -17,7 +17,7 @@ import { import { Bool } from '../bool.js'; import { provable } from '../circuit-value.js'; import { assertPositiveInteger } from '../../bindings/crypto/non-negative.js'; -import { arrayGet, assertBoolean } from './basic.js'; +import { arrayGet } from './basic.js'; import { sliceField3 } from './bit-slices.js'; import { Hashed } from '../provable-types/packed.js'; @@ -475,7 +475,7 @@ function multiScalarMul( function negateIf(condition: Field, P: Point, f: bigint) { let y = Provable.if( - Bool.Unsafe.ofField(condition), + Bool.Unsafe.fromField(condition), Field3.provable, ForeignField.negate(P.y, f), P.y @@ -515,18 +515,18 @@ function decomposeNoRangeCheck(Curve: CurveAffine, s: Field3) { // (in theory this would allow us to hard-code the high quotient limb to zero in the ffmul below, and save 2 RCs.. but not worth it) let s0: Field3 = [s00, s01, Field.from(0n)]; let s1: Field3 = [s10, s11, Field.from(0n)]; - assertBoolean(s0Negative); - assertBoolean(s1Negative); + s0Negative.assertBool(); + s1Negative.assertBool(); // prove that s1*lambda = s - s0 let lambda = Provable.if( - Bool.Unsafe.ofField(s1Negative), + Bool.Unsafe.fromField(s1Negative), Field3.provable, Field3.from(Curve.Scalar.negate(Curve.Endo.scalar)), Field3.from(Curve.Endo.scalar) ); let rhs = Provable.if( - Bool.Unsafe.ofField(s0Negative), + Bool.Unsafe.fromField(s0Negative), Field3.provable, ForeignField.Sum(s).add(s0).finish(Curve.order), ForeignField.Sum(s).sub(s0).finish(Curve.order) From 69e214b7a85c1e271929151658f3a6776070fccb Mon Sep 17 00:00:00 2001 From: Gregor Mitscha-Baude Date: Thu, 7 Mar 2024 00:47:52 +0100 Subject: [PATCH 03/41] boolean gadgets --- src/lib/bool.ts | 30 +++++++++++++++++++++++++----- src/snarky.d.ts | 12 ------------ 2 files changed, 25 insertions(+), 17 deletions(-) diff --git a/src/lib/bool.ts b/src/lib/bool.ts index 5f6ae05dbe..3849165147 100644 --- a/src/lib/bool.ts +++ b/src/lib/bool.ts @@ -10,6 +10,7 @@ import { Bool as B } from '../provable/field-bigint.js'; import { defineBinable } from '../bindings/lib/binable.js'; import { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver } from './provable-context.js'; +import { existsOne } from './gadgets/common.js'; export { BoolVar, Bool }; @@ -63,7 +64,9 @@ class Bool { if (this.isConstant()) { return new Bool(!this.toBoolean()); } - return new Bool(Snarky.bool.not(this.value)); + // 1 - x + let not = new Field(1).sub(this.toField()); + return new Bool(not.value); } /** @@ -75,7 +78,8 @@ class Bool { if (this.isConstant() && isConstant(y)) { return new Bool(this.toBoolean() && toBoolean(y)); } - return new Bool(Snarky.bool.and(this.value, toFieldVar(y))); + // x * y + return new Bool(this.toField().mul(Bool.toField(y)).value); } /** @@ -87,7 +91,8 @@ class Bool { if (this.isConstant() && isConstant(y)) { return new Bool(this.toBoolean() || toBoolean(y)); } - return new Bool(Snarky.bool.or(this.value, toFieldVar(y))); + // 1 - (1 - x)(1 - y) = x + y - xy + return this.not().and(new Bool(y).not()).not(); } /** @@ -102,7 +107,7 @@ class Bool { } return; } - Snarky.bool.assertEqual(this.value, toFieldVar(y)); + this.toField().assertEquals(Bool.toField(y)); } catch (err) { throw withMessage(err, message); } @@ -144,7 +149,22 @@ class Bool { if (this.isConstant() && isConstant(y)) { return new Bool(this.toBoolean() === toBoolean(y)); } - return new Bool(Snarky.bool.equals(this.value, toFieldVar(y))); + if (isConstant(y)) { + if (toBoolean(y)) return this; + else return this.not(); + } + if (this.isConstant()) { + return new Bool(y).equals(this); + } + // 1 - (x - y)^2 = 2xy - x - y + 1 + // match snarky logic: + // 2x * y === x + y - z + // return 1 - z + let z = existsOne(() => BigInt(this.toBoolean() === toBoolean(y))); + let x = this.toField(); + let y_ = Bool.toField(y); + Snarky.field.assertMul(x.add(x).value, y_.value, x.add(y_).sub(z).value); + return new Bool(z.value).not(); } /** diff --git a/src/snarky.d.ts b/src/snarky.d.ts index 8d38ed3bf5..17c4ca9b2d 100644 --- a/src/snarky.d.ts +++ b/src/snarky.d.ts @@ -467,18 +467,6 @@ declare const Snarky: { ): void; }; - bool: { - not(x: BoolVar): BoolVar; - - and(x: BoolVar, y: BoolVar): BoolVar; - - or(x: BoolVar, y: BoolVar): BoolVar; - - equals(x: BoolVar, y: BoolVar): BoolVar; - - assertEqual(x: BoolVar, y: BoolVar): void; - }; - group: { scale(p: MlGroup, s: MlArray): MlGroup; }; From 83f2634b7868a624566017680f000a16f0f32f8c Mon Sep 17 00:00:00 2001 From: Gregor Mitscha-Baude Date: Thu, 7 Mar 2024 01:21:12 +0100 Subject: [PATCH 04/41] assert square --- src/lib/field.ts | 16 +++++++++------- src/lib/gadgets/basic.ts | 11 ++++++++++- src/snarky.d.ts | 4 ---- 3 files changed, 19 insertions(+), 12 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 84002145e2..fe690e275a 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,7 +5,7 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; -import { assertBoolean } from './gadgets/basic.js'; +import { assertBoolean, assertSquare } from './gadgets/basic.js'; // external API export { Field }; @@ -547,12 +547,13 @@ class Field { return new Field(Fp.square(this.toBigInt())); } // create a new witness for z = x^2 - let z = Snarky.existsVar(() => + let z_ = Snarky.existsVar(() => FieldConst.fromBigint(Fp.square(this.toBigInt())) ); + let z = new Field(z_); // add a squaring constraint - Snarky.field.assertSquare(this.value, z); - return new Field(z); + assertSquare(this, z); + return z; } /** @@ -582,13 +583,14 @@ class Field { return new Field(z); } // create a witness for sqrt(x) - let z = Snarky.existsVar(() => { + let z_ = Snarky.existsVar(() => { let z = Fp.sqrt(this.toBigInt()) ?? 0n; return FieldConst.fromBigint(z); }); + let z = new Field(z_); // constrain z * z === x - Snarky.field.assertSquare(z, this.value); - return new Field(z); + assertSquare(z, this); + return z; } /** diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index 8595b4a242..cee67b4b20 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -7,7 +7,7 @@ import { existsOne, toVar } from './common.js'; import { Gates } from '../gates.js'; import { TupleN } from '../util/types.js'; -export { assertBoolean, arrayGet, assertOneOf }; +export { assertBoolean, assertSquare, arrayGet, assertOneOf }; /** * Assert that x is either 0 or 1. @@ -17,6 +17,15 @@ function assertBoolean(x_: Field) { assertBilinear(x, x, [1n, -1n, 0n, 0n]); } +/** + * Assert square, x^2 === z + */ +function assertSquare(x_: Field, z_: Field) { + let x = toVar(x_); + let z = toVar(z_); + assertBilinear(x, x, [1n, 0n, 0n, 0n], z); +} + // TODO: create constant versions of these and expose on Gadgets /** diff --git a/src/snarky.d.ts b/src/snarky.d.ts index 17c4ca9b2d..fd95ec5b3c 100644 --- a/src/snarky.d.ts +++ b/src/snarky.d.ts @@ -245,10 +245,6 @@ declare const Snarky: { * x*y === z without handling of constants */ assertMul(x: FieldVar, y: FieldVar, z: FieldVar): void; - /** - * x*x === y without handling of constants - */ - assertSquare(x: FieldVar, y: FieldVar): void; /** * check x < y and x <= y */ From 98b0b8bced96e2485f5ce418d862f112c1313681 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 7 Mar 2024 15:31:10 +0100 Subject: [PATCH 05/41] add ts assertmul --- src/lib/gadgets/basic.ts | 179 +++++++++++++++++++++++++++++++++++--- src/lib/gadgets/common.ts | 20 +++-- src/lib/gates.ts | 46 ++++++---- 3 files changed, 213 insertions(+), 32 deletions(-) diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index cee67b4b20..525c284eb3 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -2,23 +2,125 @@ * Basic gadgets that only use generic gates */ import { Fp } from '../../bindings/crypto/finite-field.js'; -import type { Field, VarField } from '../field.js'; -import { existsOne, toVar } from './common.js'; -import { Gates } from '../gates.js'; +import { + Field, + FieldConst, + FieldType, + FieldVar, + VarField, + VarFieldVar, +} from '../field.js'; +import { assert, existsOne, toVar } from './common.js'; +import { Gates, fieldVar } from '../gates.js'; import { TupleN } from '../util/types.js'; -export { assertBoolean, assertSquare, arrayGet, assertOneOf }; +export { assertMul, assertSquare, assertBoolean, arrayGet, assertOneOf }; /** - * Assert that x is either 0 or 1. + * Assert multiplication constraint, `x * y === z` */ -function assertBoolean(x_: Field) { - let x = toVar(x_); - assertBilinear(x, x, [1n, -1n, 0n, 0n]); +function assertMul( + x: Field | FieldVar, + y: Field | FieldVar, + z: Field | FieldVar +) { + // this faithfully implements snarky's `assert_r1cs`, + // see `R1CS_constraint_system.add_constraint` -> `Snarky_backendless.Constraint.R1CS` + + let xv = toScaledVar(x); + let yv = toScaledVar(y); + let zv = toScaledVar(z); + + // three variables + + if (isVar(xv) && isVar(yv) && isVar(zv)) { + let [[sx, x], [sy, y], [sz, z]] = [getVar(xv), getVar(yv), getVar(zv)]; + + // -sx sy * x y + sz z = 0 + return Gates.generic( + { left: 0n, right: 0n, out: sz, mul: -sx * sy, const: 0n }, + { left: x, right: y, out: z } + ); + } + + // two variables, one constant + + if (isVar(xv) && isVar(yv) && isConst(zv)) { + let [[sx, x], [sy, y], sz] = [getVar(xv), getVar(yv), getConst(zv)]; + + // sx sy * x y - sz = 0 + return Gates.generic( + { left: 0n, right: 0n, out: 0n, mul: sx * sy, const: -sz }, + { left: x, right: y, out: emptyCell() } + ); + } + + if (isVar(xv) && isConst(yv) && isVar(zv)) { + let [[sx, x], sy, [sz, z]] = [getVar(xv), getConst(yv), getVar(zv)]; + + // sx sy * x - sz z = 0 + return Gates.generic( + { left: sx * sy, right: 0n, out: -sz, mul: 0n, const: 0n }, + { left: x, right: emptyCell(), out: z } + ); + } + + if (isConst(xv) && isVar(yv) && isVar(zv)) { + let [sx, [sy, y], [sz, z]] = [getConst(xv), getVar(yv), getVar(zv)]; + + // sx sy * y - sz z = 0 + return Gates.generic( + { left: 0n, right: sx * sy, out: -sz, mul: 0n, const: 0n }, + { left: emptyCell(), right: y, out: z } + ); + } + + // two constants, one variable + + if (isVar(xv) && isConst(yv) && isConst(zv)) { + let [[sx, x], sy, sz] = [getVar(xv), getConst(yv), getConst(zv)]; + + // sx sy * x - sz = 0 + return Gates.generic( + { left: sx * sy, right: 0n, out: 0n, mul: 0n, const: -sz }, + { left: x, right: emptyCell(), out: emptyCell() } + ); + } + + if (isConst(xv) && isVar(yv) && isConst(zv)) { + let [sx, [sy, y], sz] = [getConst(xv), getVar(yv), getConst(zv)]; + + // sx sy * y - sz = 0 + return Gates.generic( + { left: 0n, right: sx * sy, out: 0n, mul: 0n, const: -sz }, + { left: emptyCell(), right: y, out: emptyCell() } + ); + } + + if (isConst(xv) && isConst(yv) && isVar(zv)) { + let [sx, sy, [sz, z]] = [getConst(xv), getConst(yv), getVar(zv)]; + + // sz z - sx sy = 0 + return Gates.generic( + { left: 0n, right: 0n, out: sz, mul: 0n, const: -sx * sy }, + { left: emptyCell(), right: emptyCell(), out: z } + ); + } + + // three constants + + if (isConst(xv) && isConst(yv) && isConst(zv)) { + let [sx, sy, sz] = [getConst(xv), getConst(yv), getConst(zv)]; + + assert(sx * sy === sz, `assertMul(): ${sx} * ${sy} !== ${sz}`); + } + + // sadly TS doesn't know that this was exhaustive + assert(false, `assertMul(): unreachable`); } /** - * Assert square, x^2 === z + * Assert square, `x^2 === z` */ function assertSquare(x_: Field, z_: Field) { let x = toVar(x_); @@ -26,6 +128,14 @@ function assertSquare(x_: Field, z_: Field) { assertBilinear(x, x, [1n, 0n, 0n, 0n], z); } +/** + * Assert that x is either 0 or 1, `x^2 === x` + */ +function assertBoolean(x_: Field) { + let x = toVar(x_); + assertBilinear(x, x, [1n, -1n, 0n, 0n]); +} + // TODO: create constant versions of these and expose on Gadgets /** @@ -126,10 +236,10 @@ function bilinear(x: VarField, y: VarField, [a, b, c, d]: TupleN) { * The default for z is 0. */ function assertBilinear( - x: VarField, - y: VarField, + x: VarField | VarFieldVar, + y: VarField | VarFieldVar, [a, b, c, d]: TupleN, - z?: VarField + z?: VarField | VarFieldVar ) { // b*x + c*y - z? + a*x*y + d === 0 Gates.generic( @@ -141,3 +251,48 @@ function assertBilinear( function emptyCell() { return existsOne(() => 0n); } + +/** + * reduce a general `FieldVar` to a `Scale(c, Var) | Constant` + * + * this is an optimization over `toVar(x): Var`. + * it allows callers to handle the scaling factor separately, to avoid + * wastefully adding constraints of the form `c * x === y` before using `c * x`. + */ +function toScaledVar(x: Field | FieldVar): Scaled | Constant { + x = fieldVar(x); + + // return constants as is + if (FieldVar.isConstant(x)) return x; + + // return vars with a scaling factor of 1 + if (FieldVar.isVar(x)) return [FieldType.Scale, FieldConst[1], x]; + + // return scaled vars as is + if (x[0] === FieldType.Scale && x[2][0] === FieldType.Var) { + return x as Scaled; + } + + // reduce anything else (normally, Add) to a var + let xVar = toVar(x); + return [FieldType.Scale, FieldConst[1], xVar.value]; +} + +// helpers for dealing with scaled vars and constants + +type Scaled = [FieldType.Scale, FieldConst, VarFieldVar]; +type Constant = [FieldType.Constant, FieldConst]; + +function isVar(x: Scaled | Constant): x is Scaled { + return x[0] === FieldType.Scale; +} +function isConst(x: Scaled | Constant): x is Constant { + return x[0] === FieldType.Constant; +} + +function getVar(x: Scaled): [bigint, VarFieldVar] { + return [x[1][1], x[2]]; +} +function getConst(x: Constant): bigint { + return x[1][1]; +} diff --git a/src/lib/gadgets/common.ts b/src/lib/gadgets/common.ts index 3a1a36b5a5..a32c8b6c5f 100644 --- a/src/lib/gadgets/common.ts +++ b/src/lib/gadgets/common.ts @@ -1,8 +1,15 @@ -import { Field, FieldConst, FieldVar, VarField } from '../field.js'; +import { + Field, + FieldConst, + FieldVar, + VarField, + VarFieldVar, +} from '../field.js'; import { Tuple, TupleN } from '../util/types.js'; import { Snarky } from '../../snarky.js'; import { MlArray } from '../ml/base.js'; import { Bool } from '../bool.js'; +import { fieldVar } from '../gates.js'; const MAX_BITS = 64 as const; @@ -42,16 +49,19 @@ function exists TupleN>( * * Same as `Field.seal()` with the difference that `seal()` leaves constants as is. */ -function toVar(x: Field | bigint): VarField { +function toVar(x_: Field | FieldVar | bigint): VarField { + let x = new Field(x_); // don't change existing vars if (isVar(x)) return x; - let xVar = existsOne(() => Field.from(x).toBigInt()); + let xVar = existsOne(() => x.toBigInt()); xVar.assertEquals(x); return xVar; } -function isVar(x: Field | bigint): x is VarField { - return x instanceof Field && FieldVar.isVar(x.value); +function isVar(x: FieldVar | bigint): x is VarFieldVar; +function isVar(x: Field | bigint): x is VarField; +function isVar(x: Field | FieldVar | bigint) { + return FieldVar.isVar(fieldVar(x)); } /** diff --git a/src/lib/gates.ts b/src/lib/gates.ts index a8900cfe49..b34ce670e0 100644 --- a/src/lib/gates.ts +++ b/src/lib/gates.ts @@ -1,5 +1,5 @@ import { Snarky } from '../snarky.js'; -import { FieldConst, type Field } from './field.js'; +import { FieldConst, type Field, FieldVar } from './field.js'; import { exists } from './gadgets/common.js'; import { MlArray, MlTuple } from './ml/base.js'; import { TupleN } from './util/types.js'; @@ -17,6 +17,8 @@ export { KimchiGateType, }; +export { fieldVar }; + const Gates = { rangeCheck0, rangeCheck1, @@ -131,23 +133,27 @@ function xor( */ function generic( coefficients: { - left: bigint; - right: bigint; - out: bigint; - mul: bigint; - const: bigint; + left: bigint | FieldConst; + right: bigint | FieldConst; + out: bigint | FieldConst; + mul: bigint | FieldConst; + const: bigint | FieldConst; }, - inputs: { left: Field; right: Field; out: Field } + inputs: { + left: Field | FieldVar; + right: Field | FieldVar; + out: Field | FieldVar; + } ) { Snarky.gates.generic( - FieldConst.fromBigint(coefficients.left), - inputs.left.value, - FieldConst.fromBigint(coefficients.right), - inputs.right.value, - FieldConst.fromBigint(coefficients.out), - inputs.out.value, - FieldConst.fromBigint(coefficients.mul), - FieldConst.fromBigint(coefficients.const) + fieldConst(coefficients.left), + fieldVar(inputs.left), + fieldConst(coefficients.right), + fieldVar(inputs.right), + fieldConst(coefficients.out), + fieldVar(inputs.out), + fieldConst(coefficients.mul), + fieldConst(coefficients.const) ); } @@ -265,3 +271,13 @@ enum KimchiGateType { Xor16, Rot64, } + +// helper + +function fieldVar(x: Field | FieldVar | bigint): FieldVar { + if (typeof x === 'bigint') return FieldVar.constant(x); + return Array.isArray(x) ? x : x.value; +} +function fieldConst(x: bigint | FieldConst): FieldConst { + return typeof x === 'bigint' ? FieldConst.fromBigint(x) : x; +} From c48de8b1d796152c42e7094c31e06d40333869e5 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 7 Mar 2024 15:31:22 +0100 Subject: [PATCH 06/41] use ts assertmul --- src/lib/bool.ts | 3 ++- src/lib/field.ts | 12 ++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/lib/bool.ts b/src/lib/bool.ts index 3849165147..bea955ca2f 100644 --- a/src/lib/bool.ts +++ b/src/lib/bool.ts @@ -11,6 +11,7 @@ import { defineBinable } from '../bindings/lib/binable.js'; import { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver } from './provable-context.js'; import { existsOne } from './gadgets/common.js'; +import { assertMul } from './gadgets/basic.js'; export { BoolVar, Bool }; @@ -163,7 +164,7 @@ class Bool { let z = existsOne(() => BigInt(this.toBoolean() === toBoolean(y))); let x = this.toField(); let y_ = Bool.toField(y); - Snarky.field.assertMul(x.add(x).value, y_.value, x.add(y_).sub(z).value); + assertMul(x.add(x), y_, x.add(y_).sub(z)); return new Bool(z.value).not(); } diff --git a/src/lib/field.ts b/src/lib/field.ts index fe690e275a..7848151dfd 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,7 +5,7 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; -import { assertBoolean, assertSquare } from './gadgets/basic.js'; +import { assertBoolean, assertMul, assertSquare } from './gadgets/basic.js'; // external API export { Field }; @@ -452,7 +452,7 @@ class Field { FieldConst.fromBigint(Fp.mul(this.toBigInt(), toFp(y))) ); // add a multiplication constraint - Snarky.field.assertMul(this.value, y.value, z); + assertMul(this, y, z); return new Field(z); } @@ -485,7 +485,7 @@ class Field { return FieldConst.fromBigint(z); }); // constrain x * z === 1 - Snarky.field.assertMul(this.value, z, FieldVar[1]); + assertMul(this, z, FieldVar[1]); return new Field(z); } @@ -610,11 +610,11 @@ class Field { }); // add constraints // b * x === 0 - Snarky.field.assertMul(b, this.value, FieldVar[0]); + assertMul(b, this, FieldVar[0]); // z * x === 1 - b - Snarky.field.assertMul( + assertMul( z, - this.value, + this, Snarky.field.add(FieldVar[1], Snarky.field.scale(FieldConst[-1], b)) ); // ^^^ these prove that b = Bool(x === 0): From b1832e55742770776dba085693e868dd37cd2a9e Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 7 Mar 2024 18:10:52 +0100 Subject: [PATCH 07/41] start adding logic to reduce linear combinations --- src/lib/gadgets/basic.ts | 82 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 76 insertions(+), 6 deletions(-) diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index 525c284eb3..3070baf428 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -259,7 +259,7 @@ function emptyCell() { * it allows callers to handle the scaling factor separately, to avoid * wastefully adding constraints of the form `c * x === y` before using `c * x`. */ -function toScaledVar(x: Field | FieldVar): Scaled | Constant { +function toScaledVar(x: Field | FieldVar): ScaledVar | Constant { x = fieldVar(x); // return constants as is @@ -270,7 +270,7 @@ function toScaledVar(x: Field | FieldVar): Scaled | Constant { // return scaled vars as is if (x[0] === FieldType.Scale && x[2][0] === FieldType.Var) { - return x as Scaled; + return x as ScaledVar; } // reduce anything else (normally, Add) to a var @@ -278,19 +278,89 @@ function toScaledVar(x: Field | FieldVar): Scaled | Constant { return [FieldType.Scale, FieldConst[1], xVar.value]; } +/** + * Converts a `FieldVar` into a set of constraints, returns the remainder as a ScaledVar | Constant + */ +function reduceLinearCombination(x: FieldVar): { + constant: bigint; + terms: [bigint, VarFieldVar][]; +} { + return toLinearCombination(x); +} + +/** + * Flatten the AST of a `FieldVar` to a linear combination of the form + * + * `c + s1*x1 + s2*x2 + ... + sn*xn` + * + * where no vars are duplicated. + */ +function toLinearCombination( + x: FieldVar, + sx = 1n, + lincom: { constant: bigint; terms: [bigint, VarFieldVar][] } = { + constant: 0n, + terms: [], + } +): { constant: bigint; terms: [bigint, VarFieldVar][] } { + let { constant, terms } = lincom; + // the recursive logic here adds a new term sx*x to an existing linear combination + // but x might have to be expanded first to a linear combination itself + + switch (x[0]) { + case FieldType.Constant: { + // a constant is just added to the constant term + let [, [, c]] = x; + return { constant: Fp.add(constant, Fp.mul(sx, c)), terms }; + } + case FieldType.Var: { + let [, i] = x; + + // we search for an existing term with the same var + let y = terms.find((t) => t[1][1] === i); + + // if there is none, we just add a new term + if (y === undefined) return { constant, terms: [[sx, x], ...terms] }; + + // if there is one, we add the scales + let [sy] = y; + y[0] = Fp.add(sy, sx); + + if (y[0] === 0n) { + // if the sum is 0, we remove the term + terms = terms.filter((t) => t[1][1] !== i); + } + + return { constant, terms }; + } + case FieldType.Scale: { + // sx * (s * x) + ... = (sx * s) * x + ... + let [, [, s], v] = x; + return toLinearCombination(v, Fp.mul(sx, s), lincom); + } + case FieldType.Add: { + // sx * (x1 + x2) + ... = sx * x2 + (sx * x1 + ...) + let [, x1, x2] = x; + lincom = toLinearCombination(x1, sx, lincom); + return toLinearCombination(x2, sx, lincom); + } + } +} + // helpers for dealing with scaled vars and constants -type Scaled = [FieldType.Scale, FieldConst, VarFieldVar]; +// type Scaled = [FieldType.Scale, FieldConst, FieldVar]; +type ScaledVar = [FieldType.Scale, FieldConst, VarFieldVar]; type Constant = [FieldType.Constant, FieldConst]; -function isVar(x: Scaled | Constant): x is Scaled { +function isVar(x: ScaledVar | Constant): x is ScaledVar { return x[0] === FieldType.Scale; } -function isConst(x: Scaled | Constant): x is Constant { +function isConst(x: ScaledVar | Constant): x is Constant { return x[0] === FieldType.Constant; } -function getVar(x: Scaled): [bigint, VarFieldVar] { +function getVar(x: ScaledVar): [bigint, VarFieldVar] { return [x[1][1], x[2]]; } function getConst(x: Constant): bigint { From 87bc3411ad06cd02446523efc4ef9d991f9c1456 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 7 Mar 2024 21:16:23 +0100 Subject: [PATCH 08/41] implement proper reducing --- src/lib/gadgets/basic.ts | 96 ++++++++++++++++++++++++++-------------- 1 file changed, 62 insertions(+), 34 deletions(-) diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index 3070baf428..edcc9e9b1f 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -27,9 +27,9 @@ function assertMul( // this faithfully implements snarky's `assert_r1cs`, // see `R1CS_constraint_system.add_constraint` -> `Snarky_backendless.Constraint.R1CS` - let xv = toScaledVar(x); - let yv = toScaledVar(y); - let zv = toScaledVar(z); + let xv = reduceLinearCombination(x); + let yv = reduceLinearCombination(y); + let zv = reduceLinearCombination(z); // three variables @@ -211,14 +211,35 @@ function assertOneOf(x: Field, allowed: [bigint, bigint, ...bigint[]]) { // low-level helpers to create generic gates +/** + * Compute linear function of x: + * `z = a*x + b` + */ +function linear(x: VarField | VarFieldVar, [a, b]: TupleN) { + let z = existsOne(() => { + let x0 = new Field(x).toBigInt(); + return a * x0 + b; + }); + // a*x - z + b === 0 + Gates.generic( + { left: a, right: 0n, out: -1n, mul: 0n, const: b }, + { left: x, right: emptyCell(), out: z } + ); + return z; +} + /** * Compute bilinear function of x and y: * `z = a*x*y + b*x + c*y + d` */ -function bilinear(x: VarField, y: VarField, [a, b, c, d]: TupleN) { +function bilinear( + x: VarField | VarFieldVar, + y: VarField | VarFieldVar, + [a, b, c, d]: TupleN +) { let z = existsOne(() => { - let x0 = x.toBigInt(); - let y0 = y.toBigInt(); + let x0 = new Field(x).toBigInt(); + let y0 = new Field(y).toBigInt(); return a * x0 * y0 + b * x0 + c * y0 + d; }); // b*x + c*y - z + a*x*y + d === 0 @@ -253,39 +274,45 @@ function emptyCell() { } /** - * reduce a general `FieldVar` to a `Scale(c, Var) | Constant` + * Converts a `FieldVar` into a set of constraints, returns the remainder as a ScaledVar | Constant + * + * Handles duplicated variables optimally. * - * this is an optimization over `toVar(x): Var`. - * it allows callers to handle the scaling factor separately, to avoid - * wastefully adding constraints of the form `c * x === y` before using `c * x`. + * This is better than fully reducing to a Var, because it allows callers to fold the scaling factor into the next operation, + * instead of wasting a constraint on `c * x === y` before using `c * x`. */ -function toScaledVar(x: Field | FieldVar): ScaledVar | Constant { - x = fieldVar(x); - - // return constants as is - if (FieldVar.isConstant(x)) return x; +function reduceLinearCombination(x: Field | FieldVar): ScaledVar | Constant { + let { constant: c, terms } = toLinearCombination(fieldVar(x)); - // return vars with a scaling factor of 1 - if (FieldVar.isVar(x)) return [FieldType.Scale, FieldConst[1], x]; + if (terms.length === 0) { + // constant + return [FieldType.Constant, FieldConst.fromBigint(c)]; + } - // return scaled vars as is - if (x[0] === FieldType.Scale && x[2][0] === FieldType.Var) { - return x as ScaledVar; + if (terms.length === 1) { + let [s, v] = terms[0]; + if (c === 0n) { + // s*c + return [FieldType.Scale, FieldConst.fromBigint(s), v]; + } else { + // res = s*x + c + let res = linear(v, [s, c]); + return [FieldType.Scale, FieldConst[1], res.value]; + } } - // reduce anything else (normally, Add) to a var - let xVar = toVar(x); - return [FieldType.Scale, FieldConst[1], xVar.value]; -} + // res = s0*x0 + s1*x1 + ... + sn*xn + c + let [[s0, x0], [s1, x1], ...rest] = terms; -/** - * Converts a `FieldVar` into a set of constraints, returns the remainder as a ScaledVar | Constant - */ -function reduceLinearCombination(x: FieldVar): { - constant: bigint; - terms: [bigint, VarFieldVar][]; -} { - return toLinearCombination(x); + for (let [si, xi] of rest) { + // x1 = s1*x1 + si*xi + x1 = bilinear(x1, xi, [0n, s1, si, 0n]).value; + s1 = 1n; + } + + // res = s0*x0 + 1*x1 + c + let res = bilinear(x0, x1, [0n, s0, 1n, c]); + return [FieldType.Scale, FieldConst[1], res.value]; } /** @@ -305,15 +332,16 @@ function toLinearCombination( ): { constant: bigint; terms: [bigint, VarFieldVar][] } { let { constant, terms } = lincom; // the recursive logic here adds a new term sx*x to an existing linear combination - // but x might have to be expanded first to a linear combination itself + // but x itself is an AST switch (x[0]) { case FieldType.Constant: { - // a constant is just added to the constant term + // a constant is added to the constant term let [, [, c]] = x; return { constant: Fp.add(constant, Fp.mul(sx, c)), terms }; } case FieldType.Var: { + // a variable as added to the terms or included in an existing one let [, i] = x; // we search for an existing term with the same var From f35329aab1cae252561b151a2be8338b3e2b4973 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 09:19:50 +0100 Subject: [PATCH 09/41] start separate assert mul with the goal of compatibility, to swap out later --- src/lib/bool.ts | 2 +- src/lib/field.ts | 3 +- src/lib/gadgets/basic.ts | 4 + src/lib/gadgets/compatible.ts | 231 ++++++++++++++++++++++++++++++++++ 4 files changed, 238 insertions(+), 2 deletions(-) create mode 100644 src/lib/gadgets/compatible.ts diff --git a/src/lib/bool.ts b/src/lib/bool.ts index bea955ca2f..65e4e56ebd 100644 --- a/src/lib/bool.ts +++ b/src/lib/bool.ts @@ -11,7 +11,7 @@ import { defineBinable } from '../bindings/lib/binable.js'; import { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver } from './provable-context.js'; import { existsOne } from './gadgets/common.js'; -import { assertMul } from './gadgets/basic.js'; +import { assertMul } from './gadgets/compatible.js'; export { BoolVar, Bool }; diff --git a/src/lib/field.ts b/src/lib/field.ts index 7848151dfd..60b6bb2aab 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,7 +5,8 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; -import { assertBoolean, assertMul, assertSquare } from './gadgets/basic.js'; +import { assertBoolean, assertSquare } from './gadgets/basic.js'; +import { assertMul } from './gadgets/compatible.js'; // external API export { Field }; diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index edcc9e9b1f..fd37c63283 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -16,6 +16,8 @@ import { TupleN } from '../util/types.js'; export { assertMul, assertSquare, assertBoolean, arrayGet, assertOneOf }; +export { emptyCell, linear, bilinear, ScaledVar, Constant }; + /** * Assert multiplication constraint, `x * y === z` */ @@ -394,3 +396,5 @@ function getVar(x: ScaledVar): [bigint, VarFieldVar] { function getConst(x: Constant): bigint { return x[1][1]; } + +const ScaledVar = { isVar, getVar, isConst, getConst }; diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts new file mode 100644 index 0000000000..a363d9604e --- /dev/null +++ b/src/lib/gadgets/compatible.ts @@ -0,0 +1,231 @@ +/** + * Basic gadgets that only use generic gates, and are compatible with (create the same constraints as) + * `plonk_constraint_system.ml` / R!CS_constraint_system. + */ +import { Fp } from '../../bindings/crypto/finite-field.js'; +import { + Field, + FieldConst, + FieldType, + FieldVar, + VarFieldVar, +} from '../field.js'; +import { assert } from './common.js'; +import { Gates, fieldVar } from '../gates.js'; +import { + Constant, + ScaledVar, + bilinear, + emptyCell, + linear, + assertMul, +} from './basic.js'; + +export { assertMulCompatible as assertMul }; + +let { isVar, getVar, isConst, getConst } = ScaledVar; + +/** + * Assert multiplication constraint, `x * y === z` + */ +function assertMulCompatible( + x: Field | FieldVar, + y: Field | FieldVar, + z: Field | FieldVar +) { + // this faithfully implements snarky's `assert_r1cs`, + // see `R1CS_constraint_system.add_constraint` -> `Snarky_backendless.Constraint.R1CS` + + let xv = reduceLinearCombination(x); + let yv = reduceLinearCombination(y); + let zv = reduceLinearCombination(z); + + // three variables + + if (isVar(xv) && isVar(yv) && isVar(zv)) { + let [[sx, x], [sy, y], [sz, z]] = [getVar(xv), getVar(yv), getVar(zv)]; + + // -sx sy * x y + sz z = 0 + return Gates.generic( + { left: 0n, right: 0n, out: sz, mul: -sx * sy, const: 0n }, + { left: x, right: y, out: z } + ); + } + + // two variables, one constant + + if (isVar(xv) && isVar(yv) && isConst(zv)) { + let [[sx, x], [sy, y], sz] = [getVar(xv), getVar(yv), getConst(zv)]; + + // sx sy * x y - sz = 0 + return Gates.generic( + { left: 0n, right: 0n, out: 0n, mul: sx * sy, const: -sz }, + { left: x, right: y, out: emptyCell() } + ); + } + + if (isVar(xv) && isConst(yv) && isVar(zv)) { + let [[sx, x], sy, [sz, z]] = [getVar(xv), getConst(yv), getVar(zv)]; + + // sx sy * x - sz z = 0 + return Gates.generic( + { left: sx * sy, right: 0n, out: -sz, mul: 0n, const: 0n }, + { left: x, right: emptyCell(), out: z } + ); + } + + if (isConst(xv) && isVar(yv) && isVar(zv)) { + let [sx, [sy, y], [sz, z]] = [getConst(xv), getVar(yv), getVar(zv)]; + + // sx sy * y - sz z = 0 + return Gates.generic( + { left: 0n, right: sx * sy, out: -sz, mul: 0n, const: 0n }, + { left: emptyCell(), right: y, out: z } + ); + } + + // two constants, one variable + + if (isVar(xv) && isConst(yv) && isConst(zv)) { + let [[sx, x], sy, sz] = [getVar(xv), getConst(yv), getConst(zv)]; + + // sx sy * x - sz = 0 + return Gates.generic( + { left: sx * sy, right: 0n, out: 0n, mul: 0n, const: -sz }, + { left: x, right: emptyCell(), out: emptyCell() } + ); + } + + if (isConst(xv) && isVar(yv) && isConst(zv)) { + let [sx, [sy, y], sz] = [getConst(xv), getVar(yv), getConst(zv)]; + + // sx sy * y - sz = 0 + return Gates.generic( + { left: 0n, right: sx * sy, out: 0n, mul: 0n, const: -sz }, + { left: emptyCell(), right: y, out: emptyCell() } + ); + } + + if (isConst(xv) && isConst(yv) && isVar(zv)) { + let [sx, sy, [sz, z]] = [getConst(xv), getConst(yv), getVar(zv)]; + + // sz z - sx sy = 0 + return Gates.generic( + { left: 0n, right: 0n, out: sz, mul: 0n, const: -sx * sy }, + { left: emptyCell(), right: emptyCell(), out: z } + ); + } + + // three constants + + if (isConst(xv) && isConst(yv) && isConst(zv)) { + let [sx, sy, sz] = [getConst(xv), getConst(yv), getConst(zv)]; + + assert(sx * sy === sz, `assertMul(): ${sx} * ${sy} !== ${sz}`); + } + + // sadly TS doesn't know that this was exhaustive + assert(false, `assertMul(): unreachable`); +} + +/** + * Converts a `FieldVar` into a set of constraints, returns the remainder as a ScaledVar | Constant + * + * Handles duplicated variables optimally. + * + * This is better than fully reducing to a Var, because it allows callers to fold the scaling factor into the next operation, + * instead of wasting a constraint on `c * x === y` before using `c * x`. + */ +function reduceLinearCombination(x: Field | FieldVar): ScaledVar | Constant { + let { constant: c, terms } = toLinearCombination(fieldVar(x)); + + if (terms.length === 0) { + // constant + return [FieldType.Constant, FieldConst.fromBigint(c)]; + } + + if (terms.length === 1) { + let [s, v] = terms[0]; + if (c === 0n) { + // s*c + return [FieldType.Scale, FieldConst.fromBigint(s), v]; + } else { + // res = s*x + c + let res = linear(v, [s, c]); + return [FieldType.Scale, FieldConst[1], res.value]; + } + } + + // res = s0*x0 + s1*x1 + ... + sn*xn + c + let [[s0, x0], [s1, x1], ...rest] = terms; + + for (let [si, xi] of rest) { + // x1 = s1*x1 + si*xi + x1 = bilinear(x1, xi, [0n, s1, si, 0n]).value; + s1 = 1n; + } + + // res = s0*x0 + 1*x1 + c + let res = bilinear(x0, x1, [0n, s0, 1n, c]); + return [FieldType.Scale, FieldConst[1], res.value]; +} + +/** + * Flatten the AST of a `FieldVar` to a linear combination of the form + * + * `c + s1*x1 + s2*x2 + ... + sn*xn` + * + * where no vars are duplicated. + */ +function toLinearCombination( + x: FieldVar, + sx = 1n, + lincom: { constant: bigint; terms: [bigint, VarFieldVar][] } = { + constant: 0n, + terms: [], + } +): { constant: bigint; terms: [bigint, VarFieldVar][] } { + let { constant, terms } = lincom; + // the recursive logic here adds a new term sx*x to an existing linear combination + // but x itself is an AST + + switch (x[0]) { + case FieldType.Constant: { + // a constant is added to the constant term + let [, [, c]] = x; + return { constant: Fp.add(constant, Fp.mul(sx, c)), terms }; + } + case FieldType.Var: { + // a variable as added to the terms or included in an existing one + let [, i] = x; + + // we search for an existing term with the same var + let y = terms.find((t) => t[1][1] === i); + + // if there is none, we just add a new term + if (y === undefined) return { constant, terms: [[sx, x], ...terms] }; + + // if there is one, we add the scales + let [sy] = y; + y[0] = Fp.add(sy, sx); + + if (y[0] === 0n) { + // if the sum is 0, we remove the term + terms = terms.filter((t) => t[1][1] !== i); + } + + return { constant, terms }; + } + case FieldType.Scale: { + // sx * (s * x) + ... = (sx * s) * x + ... + let [, [, s], v] = x; + return toLinearCombination(v, Fp.mul(sx, s), lincom); + } + case FieldType.Add: { + // sx * (x1 + x2) + ... = sx * x2 + (sx * x1 + ...) + let [, x1, x2] = x; + lincom = toLinearCombination(x1, sx, lincom); + return toLinearCombination(x2, sx, lincom); + } + } +} From d71bf6dcdc9ad604e31ef56b9cfd040afab47744 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 10:44:21 +0100 Subject: [PATCH 10/41] compatibility fixes --- src/lib/gadgets/compatible.ts | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index a363d9604e..aef6023fdf 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -138,6 +138,7 @@ function assertMulCompatible( */ function reduceLinearCombination(x: Field | FieldVar): ScaledVar | Constant { let { constant: c, terms } = toLinearCombination(fieldVar(x)); + terms.reverse(); if (terms.length === 0) { // constant @@ -145,28 +146,30 @@ function reduceLinearCombination(x: Field | FieldVar): ScaledVar | Constant { } if (terms.length === 1) { - let [s, v] = terms[0]; + let [s, x] = terms[0]; if (c === 0n) { - // s*c - return [FieldType.Scale, FieldConst.fromBigint(s), v]; + // s*x + return [FieldType.Scale, FieldConst.fromBigint(s), x]; } else { // res = s*x + c - let res = linear(v, [s, c]); + let res = linear(x, [s, c]); return [FieldType.Scale, FieldConst[1], res.value]; } } // res = s0*x0 + s1*x1 + ... + sn*xn + c - let [[s0, x0], [s1, x1], ...rest] = terms; + let [[s0, x0], ...rest] = terms; - for (let [si, xi] of rest) { + let [s1, x1] = rest.pop()!; + + for (let [si, xi] of rest.reverse()) { // x1 = s1*x1 + si*xi - x1 = bilinear(x1, xi, [0n, s1, si, 0n]).value; + x1 = bilinear(xi, x1, [0n, si, s1, 0n]).value; s1 = 1n; } - // res = s0*x0 + 1*x1 + c - let res = bilinear(x0, x1, [0n, s0, 1n, c]); + // res = s0*x0 + s1*x1 + c + let res = bilinear(x0, x1, [0n, s0, s1, c]); return [FieldType.Scale, FieldConst[1], res.value]; } From aedd45cca1e8ef413d818a09332e29ee43142e57 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 11:21:12 +0100 Subject: [PATCH 11/41] figure out the secret code --- src/lib/gadgets/compatible.ts | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index aef6023fdf..1c1a581aa4 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -138,7 +138,9 @@ function assertMulCompatible( */ function reduceLinearCombination(x: Field | FieldVar): ScaledVar | Constant { let { constant: c, terms } = toLinearCombination(fieldVar(x)); - terms.reverse(); + + // sort terms alphabetically by variable index + terms.sort(([, [, i]], [, [, j]]) => i - j); if (terms.length === 0) { // constant From 04c16249bc8faf1a5210bf917757e7a592542fd4 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 11:54:16 +0100 Subject: [PATCH 12/41] merge back duplicated code --- src/lib/gadgets/basic.ts | 34 ++++++--- src/lib/gadgets/compatible.ts | 127 +--------------------------------- 2 files changed, 27 insertions(+), 134 deletions(-) diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index fd37c63283..e453c449dc 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -16,7 +16,15 @@ import { TupleN } from '../util/types.js'; export { assertMul, assertSquare, assertBoolean, arrayGet, assertOneOf }; -export { emptyCell, linear, bilinear, ScaledVar, Constant }; +// internal +export { + reduceLinearCombination, + emptyCell, + linear, + bilinear, + ScaledVar, + Constant, +}; /** * Assert multiplication constraint, `x * y === z` @@ -286,34 +294,40 @@ function emptyCell() { function reduceLinearCombination(x: Field | FieldVar): ScaledVar | Constant { let { constant: c, terms } = toLinearCombination(fieldVar(x)); + // sort terms alphabetically by variable index + // (to match snarky implementation) + terms.sort(([, [, i]], [, [, j]]) => i - j); + if (terms.length === 0) { // constant return [FieldType.Constant, FieldConst.fromBigint(c)]; } if (terms.length === 1) { - let [s, v] = terms[0]; + let [s, x] = terms[0]; if (c === 0n) { - // s*c - return [FieldType.Scale, FieldConst.fromBigint(s), v]; + // s*x + return [FieldType.Scale, FieldConst.fromBigint(s), x]; } else { // res = s*x + c - let res = linear(v, [s, c]); + let res = linear(x, [s, c]); return [FieldType.Scale, FieldConst[1], res.value]; } } // res = s0*x0 + s1*x1 + ... + sn*xn + c - let [[s0, x0], [s1, x1], ...rest] = terms; + let [[s0, x0], ...rest] = terms; + + let [s1, x1] = rest.pop()!; - for (let [si, xi] of rest) { + for (let [si, xi] of rest.reverse()) { // x1 = s1*x1 + si*xi - x1 = bilinear(x1, xi, [0n, s1, si, 0n]).value; + x1 = bilinear(xi, x1, [0n, si, s1, 0n]).value; s1 = 1n; } - // res = s0*x0 + 1*x1 + c - let res = bilinear(x0, x1, [0n, s0, 1n, c]); + // res = s0*x0 + s1*x1 + c + let res = bilinear(x0, x1, [0n, s0, s1, c]); return [FieldType.Scale, FieldConst[1], res.value]; } diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index 1c1a581aa4..19f508237d 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -2,24 +2,10 @@ * Basic gadgets that only use generic gates, and are compatible with (create the same constraints as) * `plonk_constraint_system.ml` / R!CS_constraint_system. */ -import { Fp } from '../../bindings/crypto/finite-field.js'; -import { - Field, - FieldConst, - FieldType, - FieldVar, - VarFieldVar, -} from '../field.js'; +import { Field, FieldVar } from '../field.js'; import { assert } from './common.js'; -import { Gates, fieldVar } from '../gates.js'; -import { - Constant, - ScaledVar, - bilinear, - emptyCell, - linear, - assertMul, -} from './basic.js'; +import { Gates } from '../gates.js'; +import { ScaledVar, emptyCell, reduceLinearCombination } from './basic.js'; export { assertMulCompatible as assertMul }; @@ -127,110 +113,3 @@ function assertMulCompatible( // sadly TS doesn't know that this was exhaustive assert(false, `assertMul(): unreachable`); } - -/** - * Converts a `FieldVar` into a set of constraints, returns the remainder as a ScaledVar | Constant - * - * Handles duplicated variables optimally. - * - * This is better than fully reducing to a Var, because it allows callers to fold the scaling factor into the next operation, - * instead of wasting a constraint on `c * x === y` before using `c * x`. - */ -function reduceLinearCombination(x: Field | FieldVar): ScaledVar | Constant { - let { constant: c, terms } = toLinearCombination(fieldVar(x)); - - // sort terms alphabetically by variable index - terms.sort(([, [, i]], [, [, j]]) => i - j); - - if (terms.length === 0) { - // constant - return [FieldType.Constant, FieldConst.fromBigint(c)]; - } - - if (terms.length === 1) { - let [s, x] = terms[0]; - if (c === 0n) { - // s*x - return [FieldType.Scale, FieldConst.fromBigint(s), x]; - } else { - // res = s*x + c - let res = linear(x, [s, c]); - return [FieldType.Scale, FieldConst[1], res.value]; - } - } - - // res = s0*x0 + s1*x1 + ... + sn*xn + c - let [[s0, x0], ...rest] = terms; - - let [s1, x1] = rest.pop()!; - - for (let [si, xi] of rest.reverse()) { - // x1 = s1*x1 + si*xi - x1 = bilinear(xi, x1, [0n, si, s1, 0n]).value; - s1 = 1n; - } - - // res = s0*x0 + s1*x1 + c - let res = bilinear(x0, x1, [0n, s0, s1, c]); - return [FieldType.Scale, FieldConst[1], res.value]; -} - -/** - * Flatten the AST of a `FieldVar` to a linear combination of the form - * - * `c + s1*x1 + s2*x2 + ... + sn*xn` - * - * where no vars are duplicated. - */ -function toLinearCombination( - x: FieldVar, - sx = 1n, - lincom: { constant: bigint; terms: [bigint, VarFieldVar][] } = { - constant: 0n, - terms: [], - } -): { constant: bigint; terms: [bigint, VarFieldVar][] } { - let { constant, terms } = lincom; - // the recursive logic here adds a new term sx*x to an existing linear combination - // but x itself is an AST - - switch (x[0]) { - case FieldType.Constant: { - // a constant is added to the constant term - let [, [, c]] = x; - return { constant: Fp.add(constant, Fp.mul(sx, c)), terms }; - } - case FieldType.Var: { - // a variable as added to the terms or included in an existing one - let [, i] = x; - - // we search for an existing term with the same var - let y = terms.find((t) => t[1][1] === i); - - // if there is none, we just add a new term - if (y === undefined) return { constant, terms: [[sx, x], ...terms] }; - - // if there is one, we add the scales - let [sy] = y; - y[0] = Fp.add(sy, sx); - - if (y[0] === 0n) { - // if the sum is 0, we remove the term - terms = terms.filter((t) => t[1][1] !== i); - } - - return { constant, terms }; - } - case FieldType.Scale: { - // sx * (s * x) + ... = (sx * s) * x + ... - let [, [, s], v] = x; - return toLinearCombination(v, Fp.mul(sx, s), lincom); - } - case FieldType.Add: { - // sx * (x1 + x2) + ... = sx * x2 + (sx * x1 + ...) - let [, x1, x2] = x; - lincom = toLinearCombination(x1, sx, lincom); - return toLinearCombination(x2, sx, lincom); - } - } -} From 9f4268663681acf6a963a3336e699335f40d5877 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 12:01:56 +0100 Subject: [PATCH 13/41] add simpler assertMul --- src/lib/gadgets/basic.ts | 128 +++++++--------------------------- src/lib/gadgets/compatible.ts | 8 +-- 2 files changed, 31 insertions(+), 105 deletions(-) diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index e453c449dc..62f14d020e 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -10,21 +10,14 @@ import { VarField, VarFieldVar, } from '../field.js'; -import { assert, existsOne, toVar } from './common.js'; +import { existsOne, toVar } from './common.js'; import { Gates, fieldVar } from '../gates.js'; import { TupleN } from '../util/types.js'; export { assertMul, assertSquare, assertBoolean, arrayGet, assertOneOf }; // internal -export { - reduceLinearCombination, - emptyCell, - linear, - bilinear, - ScaledVar, - Constant, -}; +export { reduceToScaledVar, emptyCell, linear, bilinear, ScaledVar, Constant }; /** * Assert multiplication constraint, `x * y === z` @@ -34,99 +27,27 @@ function assertMul( y: Field | FieldVar, z: Field | FieldVar ) { - // this faithfully implements snarky's `assert_r1cs`, - // see `R1CS_constraint_system.add_constraint` -> `Snarky_backendless.Constraint.R1CS` + // simpler version of assertMulCompatible that currently uses the same amount of constraints but is not compatible - let xv = reduceLinearCombination(x); - let yv = reduceLinearCombination(y); - let zv = reduceLinearCombination(z); + // TODO: if we replace `reduceToScaledVar()` with a function that leaves `a*x + b` unreduced, we can save constraints here + // for example: (x - 1)*(x - 2) === 0 would become 1 constraint instead of 3 + let [[sx, vx], cx] = getLinear(reduceToScaledVar(x)); + let [[sy, vy], cy] = getLinear(reduceToScaledVar(y)); + let [[sz, vz], cz] = getLinear(reduceToScaledVar(z)); - // three variables + // (sx * vx + cx) * (sy * vy + cy) = (sz * vz + cz) + // sx*cy*vx + sy*cx*vy - sz*vz + sx*sy*x*vy + (cx*cy - cz) = 0 - if (isVar(xv) && isVar(yv) && isVar(zv)) { - let [[sx, x], [sy, y], [sz, z]] = [getVar(xv), getVar(yv), getVar(zv)]; - - // -sx sy * x y + sz z = 0 - return Gates.generic( - { left: 0n, right: 0n, out: sz, mul: -sx * sy, const: 0n }, - { left: x, right: y, out: z } - ); - } - - // two variables, one constant - - if (isVar(xv) && isVar(yv) && isConst(zv)) { - let [[sx, x], [sy, y], sz] = [getVar(xv), getVar(yv), getConst(zv)]; - - // sx sy * x y - sz = 0 - return Gates.generic( - { left: 0n, right: 0n, out: 0n, mul: sx * sy, const: -sz }, - { left: x, right: y, out: emptyCell() } - ); - } - - if (isVar(xv) && isConst(yv) && isVar(zv)) { - let [[sx, x], sy, [sz, z]] = [getVar(xv), getConst(yv), getVar(zv)]; - - // sx sy * x - sz z = 0 - return Gates.generic( - { left: sx * sy, right: 0n, out: -sz, mul: 0n, const: 0n }, - { left: x, right: emptyCell(), out: z } - ); - } - - if (isConst(xv) && isVar(yv) && isVar(zv)) { - let [sx, [sy, y], [sz, z]] = [getConst(xv), getVar(yv), getVar(zv)]; - - // sx sy * y - sz z = 0 - return Gates.generic( - { left: 0n, right: sx * sy, out: -sz, mul: 0n, const: 0n }, - { left: emptyCell(), right: y, out: z } - ); - } - - // two constants, one variable - - if (isVar(xv) && isConst(yv) && isConst(zv)) { - let [[sx, x], sy, sz] = [getVar(xv), getConst(yv), getConst(zv)]; - - // sx sy * x - sz = 0 - return Gates.generic( - { left: sx * sy, right: 0n, out: 0n, mul: 0n, const: -sz }, - { left: x, right: emptyCell(), out: emptyCell() } - ); - } - - if (isConst(xv) && isVar(yv) && isConst(zv)) { - let [sx, [sy, y], sz] = [getConst(xv), getVar(yv), getConst(zv)]; - - // sx sy * y - sz = 0 - return Gates.generic( - { left: 0n, right: sx * sy, out: 0n, mul: 0n, const: -sz }, - { left: emptyCell(), right: y, out: emptyCell() } - ); - } - - if (isConst(xv) && isConst(yv) && isVar(zv)) { - let [sx, sy, [sz, z]] = [getConst(xv), getConst(yv), getVar(zv)]; - - // sz z - sx sy = 0 - return Gates.generic( - { left: 0n, right: 0n, out: sz, mul: 0n, const: -sx * sy }, - { left: emptyCell(), right: emptyCell(), out: z } - ); - } - - // three constants - - if (isConst(xv) && isConst(yv) && isConst(zv)) { - let [sx, sy, sz] = [getConst(xv), getConst(yv), getConst(zv)]; - - assert(sx * sy === sz, `assertMul(): ${sx} * ${sy} !== ${sz}`); - } - - // sadly TS doesn't know that this was exhaustive - assert(false, `assertMul(): unreachable`); + Gates.generic( + { + left: sx * cy, + right: sy * cx, + out: -sz, + mul: sx * sy, + const: cx * cy - cz, + }, + { left: vx, right: vy, out: vz } + ); } /** @@ -286,12 +207,12 @@ function emptyCell() { /** * Converts a `FieldVar` into a set of constraints, returns the remainder as a ScaledVar | Constant * - * Handles duplicated variables optimally. + * Collapses duplicated variables, so e.g. x - x just becomes the 0 constant. * * This is better than fully reducing to a Var, because it allows callers to fold the scaling factor into the next operation, * instead of wasting a constraint on `c * x === y` before using `c * x`. */ -function reduceLinearCombination(x: Field | FieldVar): ScaledVar | Constant { +function reduceToScaledVar(x: Field | FieldVar): ScaledVar | Constant { let { constant: c, terms } = toLinearCombination(fieldVar(x)); // sort terms alphabetically by variable index @@ -411,4 +332,9 @@ function getConst(x: Constant): bigint { return x[1][1]; } +function getLinear(x: ScaledVar | Constant): [[bigint, VarFieldVar], bigint] { + if (isVar(x)) return [getVar(x), 0n]; + return [[0n, emptyCell().value], getConst(x)]; +} + const ScaledVar = { isVar, getVar, isConst, getConst }; diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index 19f508237d..5e8803ec15 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -5,7 +5,7 @@ import { Field, FieldVar } from '../field.js'; import { assert } from './common.js'; import { Gates } from '../gates.js'; -import { ScaledVar, emptyCell, reduceLinearCombination } from './basic.js'; +import { ScaledVar, emptyCell, reduceToScaledVar } from './basic.js'; export { assertMulCompatible as assertMul }; @@ -22,9 +22,9 @@ function assertMulCompatible( // this faithfully implements snarky's `assert_r1cs`, // see `R1CS_constraint_system.add_constraint` -> `Snarky_backendless.Constraint.R1CS` - let xv = reduceLinearCombination(x); - let yv = reduceLinearCombination(y); - let zv = reduceLinearCombination(z); + let xv = reduceToScaledVar(x); + let yv = reduceToScaledVar(y); + let zv = reduceToScaledVar(z); // three variables From 6b8eb3af53095088905a432b74bcdbc6cf59ad8d Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 12:13:52 +0100 Subject: [PATCH 14/41] remove unused bindings --- src/snarky.d.ts | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/src/snarky.d.ts b/src/snarky.d.ts index fd95ec5b3c..59b8ed1e80 100644 --- a/src/snarky.d.ts +++ b/src/snarky.d.ts @@ -229,10 +229,6 @@ declare const Snarky: { * scale x by a constant to get a new AST node Scale(c, x); handles if x is a constant */ scale(c: FieldConst, x: FieldVar): FieldVar; - /** - * witnesses z = x*y and constrains it with [assert_r1cs]; handles constants - */ - mul(x: FieldVar, y: FieldVar): FieldVar; /** * evaluates a CVar by walking the AST and reading Vars from a list of public input + aux values */ @@ -244,10 +240,6 @@ declare const Snarky: { /** * x*y === z without handling of constants */ - assertMul(x: FieldVar, y: FieldVar, z: FieldVar): void; - /** - * check x < y and x <= y - */ compare( bitLength: number, x: FieldVar, @@ -274,18 +266,6 @@ declare const Snarky: { * (implemented with toConstantAndTerms) */ seal(x: FieldVar): VarFieldVar; - /** - * Unfolds AST to get `x = c + c0*Var(i0) + ... + cn*Var(in)`, - * returns `(c, [(c0, i0), ..., (cn, in)])`; - * c is optional - */ - toConstantAndTerms( - x: FieldVar - ): [ - _: 0, - constant: MlOption, - terms: MlList> - ]; }; gates: { From f45731898acbd75159e7e19a9174b5f1f3921d57 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 12:34:42 +0100 Subject: [PATCH 15/41] compatible assert square --- src/lib/field.ts | 4 +-- src/lib/gadgets/basic.ts | 12 ++------ src/lib/gadgets/compatible.ts | 52 ++++++++++++++++++++++++++++++++++- 3 files changed, 55 insertions(+), 13 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 60b6bb2aab..1df605d01c 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,8 +5,8 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; -import { assertBoolean, assertSquare } from './gadgets/basic.js'; -import { assertMul } from './gadgets/compatible.js'; +import { assertBoolean } from './gadgets/basic.js'; +import { assertMul, assertSquare } from './gadgets/compatible.js'; // external API export { Field }; diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index 62f14d020e..04d1d62a0b 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -14,7 +14,7 @@ import { existsOne, toVar } from './common.js'; import { Gates, fieldVar } from '../gates.js'; import { TupleN } from '../util/types.js'; -export { assertMul, assertSquare, assertBoolean, arrayGet, assertOneOf }; +export { assertMul, assertBoolean, arrayGet, assertOneOf }; // internal export { reduceToScaledVar, emptyCell, linear, bilinear, ScaledVar, Constant }; @@ -28,6 +28,7 @@ function assertMul( z: Field | FieldVar ) { // simpler version of assertMulCompatible that currently uses the same amount of constraints but is not compatible + // also, doesn't handle all-constant case (handled by calling gadgets already) // TODO: if we replace `reduceToScaledVar()` with a function that leaves `a*x + b` unreduced, we can save constraints here // for example: (x - 1)*(x - 2) === 0 would become 1 constraint instead of 3 @@ -50,15 +51,6 @@ function assertMul( ); } -/** - * Assert square, `x^2 === z` - */ -function assertSquare(x_: Field, z_: Field) { - let x = toVar(x_); - let z = toVar(z_); - assertBilinear(x, x, [1n, 0n, 0n, 0n], z); -} - /** * Assert that x is either 0 or 1, `x^2 === x` */ diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index 5e8803ec15..7dd7b1bea9 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -7,7 +7,10 @@ import { assert } from './common.js'; import { Gates } from '../gates.js'; import { ScaledVar, emptyCell, reduceToScaledVar } from './basic.js'; -export { assertMulCompatible as assertMul }; +export { + assertMulCompatible as assertMul, + assertSquareCompatible as assertSquare, +}; let { isVar, getVar, isConst, getConst } = ScaledVar; @@ -113,3 +116,50 @@ function assertMulCompatible( // sadly TS doesn't know that this was exhaustive assert(false, `assertMul(): unreachable`); } + +/** + * Assert square, `x^2 === z` + */ +function assertSquareCompatible(x: Field, z: Field) { + let xv = reduceToScaledVar(x); + let zv = reduceToScaledVar(z); + + if (isVar(xv) && isVar(zv)) { + let [[sx, x], [sz, z]] = [getVar(xv), getVar(zv)]; + + // -sz * z + (sx)^2 * x*x = 0 + return Gates.generic( + { left: 0n, right: 0n, out: -sz, mul: sx ** 2n, const: 0n }, + { left: x, right: x, out: z } + ); + } + + if (isVar(xv) && isConst(zv)) { + let [[sx, x], sz] = [getVar(xv), getConst(zv)]; + + // (sx)^2 * x*x - sz = 0 + return Gates.generic( + { left: 0n, right: 0n, out: 0n, mul: sx ** 2n, const: -sz }, + { left: x, right: x, out: emptyCell() } + ); + } + + if (isConst(xv) && isVar(zv)) { + let [sx, [sz, z]] = [getConst(xv), getVar(zv)]; + + // sz * z - (sx)^2 = 0 + return Gates.generic( + { left: 0n, right: 0n, out: sz, mul: 0n, const: -(sx ** 2n) }, + { left: emptyCell(), right: emptyCell(), out: z } + ); + } + + if (isConst(xv) && isConst(zv)) { + let [sx, sz] = [getConst(xv), getConst(zv)]; + + assert(sx ** 2n === sz, `assertSquare(): ${sx}^2 !== ${sz}`); + } + + // sadly TS doesn't know that this was exhaustive + assert(false, `assertSquare(): unreachable`); +} From 502ee85e074fac3773f9b31be1c586dc536f3060 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 12:45:52 +0100 Subject: [PATCH 16/41] compatible assert boolean --- src/lib/field.ts | 7 +++++-- src/lib/gadgets/basic.ts | 10 +--------- src/lib/gadgets/compatible.ts | 31 +++++++++++++++++++++++++++++-- 3 files changed, 35 insertions(+), 13 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 1df605d01c..e53980b98b 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,8 +5,11 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; -import { assertBoolean } from './gadgets/basic.js'; -import { assertMul, assertSquare } from './gadgets/compatible.js'; +import { + assertMul, + assertSquare, + assertBoolean, +} from './gadgets/compatible.js'; // external API export { Field }; diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index 04d1d62a0b..f6c7931a3a 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -14,7 +14,7 @@ import { existsOne, toVar } from './common.js'; import { Gates, fieldVar } from '../gates.js'; import { TupleN } from '../util/types.js'; -export { assertMul, assertBoolean, arrayGet, assertOneOf }; +export { assertMul, arrayGet, assertOneOf }; // internal export { reduceToScaledVar, emptyCell, linear, bilinear, ScaledVar, Constant }; @@ -51,14 +51,6 @@ function assertMul( ); } -/** - * Assert that x is either 0 or 1, `x^2 === x` - */ -function assertBoolean(x_: Field) { - let x = toVar(x_); - assertBilinear(x, x, [1n, -1n, 0n, 0n]); -} - // TODO: create constant versions of these and expose on Gadgets /** diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index 7dd7b1bea9..2ccc320e0d 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -2,6 +2,7 @@ * Basic gadgets that only use generic gates, and are compatible with (create the same constraints as) * `plonk_constraint_system.ml` / R!CS_constraint_system. */ +import { Fp } from '../../bindings/crypto/finite-field.js'; import { Field, FieldVar } from '../field.js'; import { assert } from './common.js'; import { Gates } from '../gates.js'; @@ -10,6 +11,7 @@ import { ScaledVar, emptyCell, reduceToScaledVar } from './basic.js'; export { assertMulCompatible as assertMul, assertSquareCompatible as assertSquare, + assertBooleanCompatible as assertBoolean, }; let { isVar, getVar, isConst, getConst } = ScaledVar; @@ -110,7 +112,10 @@ function assertMulCompatible( if (isConst(xv) && isConst(yv) && isConst(zv)) { let [sx, sy, sz] = [getConst(xv), getConst(yv), getConst(zv)]; - assert(sx * sy === sz, `assertMul(): ${sx} * ${sy} !== ${sz}`); + assert( + Fp.equal(Fp.mul(sx, sy), sz), + `assertMul(): ${sx} * ${sy} !== ${sz}` + ); } // sadly TS doesn't know that this was exhaustive @@ -157,9 +162,31 @@ function assertSquareCompatible(x: Field, z: Field) { if (isConst(xv) && isConst(zv)) { let [sx, sz] = [getConst(xv), getConst(zv)]; - assert(sx ** 2n === sz, `assertSquare(): ${sx}^2 !== ${sz}`); + assert(Fp.equal(Fp.square(sx), sz), `assertSquare(): ${sx}^2 !== ${sz}`); } // sadly TS doesn't know that this was exhaustive assert(false, `assertSquare(): unreachable`); } + +/** + * Assert that x is either 0 or 1, `x^2 === x` + */ +function assertBooleanCompatible(x: Field) { + let xv = reduceToScaledVar(x); + + if (isVar(xv)) { + let [_sx, x] = getVar(xv); + + // FIXME: it's wrong that the scaling factor is ignored here, means it can't be different than 1 + // this needs to be compatible, so need to change `plonk_constraint_system.ml` + // x^2 - x = 0 + return Gates.generic( + { left: -1n, right: 0n, out: 0n, mul: 1n, const: 0n }, + { left: x, right: x, out: emptyCell() } + ); + } + + let x0 = getConst(xv); + assert(Fp.equal(Fp.square(x0), x0), `assertBoolean(): ${x} is not 0 or 1`); +} From 1ad22e2bbf2ecc3621474038eef5de680d286a59 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 13:01:20 +0100 Subject: [PATCH 17/41] document failing test, add fixed version --- src/lib/field.unit-test.ts | 8 ++++++++ src/lib/gadgets/compatible.ts | 24 ++++++++++++++++++++++-- 2 files changed, 30 insertions(+), 2 deletions(-) diff --git a/src/lib/field.unit-test.ts b/src/lib/field.unit-test.ts index 2b955dca85..121fadef7e 100644 --- a/src/lib/field.unit-test.ts +++ b/src/lib/field.unit-test.ts @@ -131,6 +131,14 @@ equivalent({ from: [field], to: unit })( (x) => x === 0n || x === 1n || throwError('not boolean'), (x) => x.assertBool() ); +// FIXME: failing test +// equivalent({ from: [field], to: unit })( +// (x) => x === 0n || x === 1n || throwError('not boolean'), +// (x) => { +// let y = Provable.witness(Field, () => x.div(2)); +// y.mul(2).assertBool(); +// } +// ); equivalent({ from: [smallField], to: bool })( (x) => (x & 1n) === 0n, (x) => x.isEven() diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index 2ccc320e0d..9b6d15d321 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -176,11 +176,11 @@ function assertBooleanCompatible(x: Field) { let xv = reduceToScaledVar(x); if (isVar(xv)) { - let [_sx, x] = getVar(xv); + let [_s, x] = getVar(xv); // FIXME: it's wrong that the scaling factor is ignored here, means it can't be different than 1 // this needs to be compatible, so need to change `plonk_constraint_system.ml` - // x^2 - x = 0 + // -x + x^2 = 0 return Gates.generic( { left: -1n, right: 0n, out: 0n, mul: 1n, const: 0n }, { left: x, right: x, out: emptyCell() } @@ -190,3 +190,23 @@ function assertBooleanCompatible(x: Field) { let x0 = getConst(xv); assert(Fp.equal(Fp.square(x0), x0), `assertBoolean(): ${x} is not 0 or 1`); } + +/** + * Assert that x is either 0 or 1, `x^2 === x` + */ +function assertBooleanFixed(x: Field) { + let xv = reduceToScaledVar(x); + + if (isVar(xv)) { + let [s, x] = getVar(xv); + + // -s*x + s^2 * x^2 = 0 + return Gates.generic( + { left: -s, right: 0n, out: 0n, mul: s ** 2n, const: 0n }, + { left: x, right: x, out: emptyCell() } + ); + } + + let x0 = getConst(xv); + assert(Fp.equal(Fp.square(x0), x0), `assertBoolean(): ${x} is not 0 or 1`); +} From 1987e784de6ea6004ec0ab1ca55046982d49f9ce Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 13:03:40 +0100 Subject: [PATCH 18/41] fixup bool --- src/lib/bool.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/bool.ts b/src/lib/bool.ts index 65e4e56ebd..b63a6ee663 100644 --- a/src/lib/bool.ts +++ b/src/lib/bool.ts @@ -161,7 +161,7 @@ class Bool { // match snarky logic: // 2x * y === x + y - z // return 1 - z - let z = existsOne(() => BigInt(this.toBoolean() === toBoolean(y))); + let z = existsOne(() => BigInt(this.toBoolean() !== toBoolean(y))); let x = this.toField(); let y_ = Bool.toField(y); assertMul(x.add(x), y_, x.add(y_).sub(z)); From c9874b24e4f1cc24910c968185ef5aa0f8fa9b85 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 13:28:01 +0100 Subject: [PATCH 19/41] add back some bindings --- src/snarky.d.ts | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/snarky.d.ts b/src/snarky.d.ts index 59b8ed1e80..c5a32933ed 100644 --- a/src/snarky.d.ts +++ b/src/snarky.d.ts @@ -240,6 +240,18 @@ declare const Snarky: { /** * x*y === z without handling of constants */ + assertMul(x: FieldVar, y: FieldVar, z: FieldVar): void; + /** + * x*x === y without handling of constants + */ + assertSquare(x: FieldVar, y: FieldVar): void; + /** + * x*x === x without handling of constants + */ + assertBoolean(x: FieldVar): void; + /** + * check x < y and x <= y + */ compare( bitLength: number, x: FieldVar, From e37074f60696677af4a912e2dfff30ab354621a7 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 13:34:54 +0100 Subject: [PATCH 20/41] switch back to snarky assert bool --- src/lib/field.ts | 8 ++------ src/lib/gadgets/compatible.ts | 2 +- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index e53980b98b..0f6551b065 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,11 +5,7 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; -import { - assertMul, - assertSquare, - assertBoolean, -} from './gadgets/compatible.js'; +import { assertMul, assertSquare } from './gadgets/compatible.js'; // external API export { Field }; @@ -903,7 +899,7 @@ class Field { } return; } - assertBoolean(this); + Snarky.field.assertBoolean(this.value); } catch (err) { throw withMessage(err, message); } diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index 9b6d15d321..dda85c2661 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -1,6 +1,6 @@ /** * Basic gadgets that only use generic gates, and are compatible with (create the same constraints as) - * `plonk_constraint_system.ml` / R!CS_constraint_system. + * `plonk_constraint_system.ml` / R1CS_constraint_system. */ import { Fp } from '../../bindings/crypto/finite-field.js'; import { Field, FieldVar } from '../field.js'; From 3729694822bd734cc533d785df02609046e35b61 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 16:53:35 +0100 Subject: [PATCH 21/41] add assert equal, not compatible yet --- src/lib/gadgets/basic.ts | 6 ++-- src/lib/gadgets/compatible.ts | 58 +++++++++++++++++++++++++++++++++++ 2 files changed, 62 insertions(+), 2 deletions(-) diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index f6c7931a3a..e4f8b564e8 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -241,7 +241,7 @@ function reduceToScaledVar(x: Field | FieldVar): ScaledVar | Constant { * * `c + s1*x1 + s2*x2 + ... + sn*xn` * - * where no vars are duplicated. + * where none of the vars xi are duplicated. */ function toLinearCombination( x: FieldVar, @@ -255,6 +255,8 @@ function toLinearCombination( // the recursive logic here adds a new term sx*x to an existing linear combination // but x itself is an AST + if (sx === 0n) return lincom; + switch (x[0]) { case FieldType.Constant: { // a constant is added to the constant term @@ -262,7 +264,7 @@ function toLinearCombination( return { constant: Fp.add(constant, Fp.mul(sx, c)), terms }; } case FieldType.Var: { - // a variable as added to the terms or included in an existing one + // a variable is added to the terms or included in an existing one let [, i] = x; // we search for an existing term with the same var diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index dda85c2661..3320d32f90 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -7,11 +7,13 @@ import { Field, FieldVar } from '../field.js'; import { assert } from './common.js'; import { Gates } from '../gates.js'; import { ScaledVar, emptyCell, reduceToScaledVar } from './basic.js'; +import { Snarky } from '../../snarky.js'; export { assertMulCompatible as assertMul, assertSquareCompatible as assertSquare, assertBooleanCompatible as assertBoolean, + assertEqualCompatible as assertEqual, }; let { isVar, getVar, isConst, getConst } = ScaledVar; @@ -116,6 +118,7 @@ function assertMulCompatible( Fp.equal(Fp.mul(sx, sy), sz), `assertMul(): ${sx} * ${sy} !== ${sz}` ); + return; } // sadly TS doesn't know that this was exhaustive @@ -163,6 +166,7 @@ function assertSquareCompatible(x: Field, z: Field) { let [sx, sz] = [getConst(xv), getConst(zv)]; assert(Fp.equal(Fp.square(sx), sz), `assertSquare(): ${sx}^2 !== ${sz}`); + return; } // sadly TS doesn't know that this was exhaustive @@ -210,3 +214,57 @@ function assertBooleanFixed(x: Field) { let x0 = getConst(xv); assert(Fp.equal(Fp.square(x0), x0), `assertBoolean(): ${x} is not 0 or 1`); } + +/** + * Assert equality, `x === y` + */ +function assertEqualCompatible(x: Field | FieldVar, y: Field | FieldVar) { + // TODO this isn't compatible with snarky's `assert_equal` yet + let xv = reduceToScaledVar(x); + let yv = reduceToScaledVar(y); + + if (isVar(xv) && isVar(yv)) { + let [[sx, x], [sy, y]] = [getVar(xv), getVar(yv)]; + + if (sx === sy) { + // x === y, so use a wire + return Snarky.field.assertEqual(x, y); + } + + // sx * x - sy * y = 0 + return Gates.generic( + { left: sx, right: -sy, out: 0n, mul: 0n, const: 0n }, + { left: x, right: y, out: emptyCell() } + ); + } + + if (isVar(xv) && isConst(yv)) { + let [[sx, x], sy] = [getVar(xv), getConst(yv)]; + + // x === sy / sx, call into snarky to use its constants table + return Snarky.field.assertEqual( + FieldVar.scale(sx, x), + FieldVar.constant(sy) + ); + } + + if (isConst(xv) && isVar(yv)) { + let [sx, [sy, y]] = [getConst(xv), getVar(yv)]; + + // sx / sy === y, call into snarky to use its constants table + return Snarky.field.assertEqual( + FieldVar.constant(sx), + FieldVar.scale(sy, y) + ); + } + + if (isConst(xv) && isConst(yv)) { + let [sx, sy] = [getConst(xv), getConst(yv)]; + + assert(Fp.equal(sx, sy), `assertEqual(): ${sx} !== ${sy}`); + return; + } + + // sadly TS doesn't know that this was exhaustive + assert(false, `assertEqual(): unreachable`); +} From 558ea3355132eefd99932ece57c4d903d22ea67e Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 8 Mar 2024 16:55:27 +0100 Subject: [PATCH 22/41] use assert equals (but not compatible yet) --- src/lib/field.ts | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 0f6551b065..73cc025602 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,7 +5,7 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; -import { assertMul, assertSquare } from './gadgets/compatible.js'; +import { assertEqual, assertMul, assertSquare } from './gadgets/compatible.js'; // external API export { Field }; @@ -274,7 +274,7 @@ class Field { } return; } - Snarky.field.assertEqual(this.value, toFieldVar(y)); + assertEqual(this, toFieldVar(y)); } catch (err) { throw withMessage(err, message); } @@ -646,8 +646,9 @@ class Field { let xMinusY = Snarky.existsVar(() => FieldConst.fromBigint(Fp.sub(this.toBigInt(), toFp(y))) ); - Snarky.field.assertEqual(this.sub(y).value, xMinusY); - return new Field(xMinusY).isZero(); + let z = new Field(xMinusY); + this.sub(y).assertEquals(z); + return z.isZero(); } /** From 13a0838dcd4806e5381a35fa352109ab61008638 Mon Sep 17 00:00:00 2001 From: Gregor Date: Wed, 13 Mar 2024 16:48:29 +0100 Subject: [PATCH 23/41] fix compatibility --- src/lib/gadgets/compatible.ts | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index 3320d32f90..cc33cc6fba 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -219,9 +219,10 @@ function assertBooleanFixed(x: Field) { * Assert equality, `x === y` */ function assertEqualCompatible(x: Field | FieldVar, y: Field | FieldVar) { - // TODO this isn't compatible with snarky's `assert_equal` yet - let xv = reduceToScaledVar(x); + // TODO not optimal for a case like `x + y === c*z`, + // where this reduces x + y and then is still not able to just use a wire let yv = reduceToScaledVar(y); + let xv = reduceToScaledVar(x); if (isVar(xv) && isVar(yv)) { let [[sx, x], [sy, y]] = [getVar(xv), getVar(yv)]; From ca25adfe64304490d68a048adeccc50c34a80bd1 Mon Sep 17 00:00:00 2001 From: Gregor Date: Wed, 13 Mar 2024 16:58:30 +0100 Subject: [PATCH 24/41] add test which works now --- src/lib/field.unit-test.ts | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/lib/field.unit-test.ts b/src/lib/field.unit-test.ts index c7bc866554..0390828f45 100644 --- a/src/lib/field.unit-test.ts +++ b/src/lib/field.unit-test.ts @@ -132,14 +132,13 @@ equivalent({ from: [field], to: unit })( (x) => x === 0n || x === 1n || throwError('not boolean'), (x) => x.assertBool() ); -// FIXME: failing test -// equivalent({ from: [field], to: unit })( -// (x) => x === 0n || x === 1n || throwError('not boolean'), -// (x) => { -// let y = Provable.witness(Field, () => x.div(2)); -// y.mul(2).assertBool(); -// } -// ); +equivalent({ from: [field], to: unit })( + (x) => x === 0n || x === 1n || throwError('not boolean'), + (x) => { + let y = Provable.witness(Field, () => x.div(2)); + y.mul(2).assertBool(); + } +); equivalent({ from: [smallField], to: bool })( (x) => (x & 1n) === 0n, (x) => x.isEven() From be94648272a5b0e03159b1852fd301117d32d6f8 Mon Sep 17 00:00:00 2001 From: Gregor Date: Wed, 13 Mar 2024 17:24:02 +0100 Subject: [PATCH 25/41] change to fixed assert bool --- src/lib/field.ts | 9 +++++++-- src/lib/gadgets/compatible.ts | 22 ---------------------- 2 files changed, 7 insertions(+), 24 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 73cc025602..d9f13cee2d 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -5,7 +5,12 @@ import type { NonNegativeInteger } from '../bindings/crypto/non-negative.js'; import { asProver, inCheckedComputation } from './provable-context.js'; import { Bool } from './bool.js'; import { assert } from './errors.js'; -import { assertEqual, assertMul, assertSquare } from './gadgets/compatible.js'; +import { + assertEqual, + assertMul, + assertSquare, + assertBoolean, +} from './gadgets/compatible.js'; // external API export { Field }; @@ -900,7 +905,7 @@ class Field { } return; } - Snarky.field.assertBoolean(this.value); + assertBoolean(this); } catch (err) { throw withMessage(err, message); } diff --git a/src/lib/gadgets/compatible.ts b/src/lib/gadgets/compatible.ts index cc33cc6fba..262dbb3585 100644 --- a/src/lib/gadgets/compatible.ts +++ b/src/lib/gadgets/compatible.ts @@ -179,28 +179,6 @@ function assertSquareCompatible(x: Field, z: Field) { function assertBooleanCompatible(x: Field) { let xv = reduceToScaledVar(x); - if (isVar(xv)) { - let [_s, x] = getVar(xv); - - // FIXME: it's wrong that the scaling factor is ignored here, means it can't be different than 1 - // this needs to be compatible, so need to change `plonk_constraint_system.ml` - // -x + x^2 = 0 - return Gates.generic( - { left: -1n, right: 0n, out: 0n, mul: 1n, const: 0n }, - { left: x, right: x, out: emptyCell() } - ); - } - - let x0 = getConst(xv); - assert(Fp.equal(Fp.square(x0), x0), `assertBoolean(): ${x} is not 0 or 1`); -} - -/** - * Assert that x is either 0 or 1, `x^2 === x` - */ -function assertBooleanFixed(x: Field) { - let xv = reduceToScaledVar(x); - if (isVar(xv)) { let [s, x] = getVar(xv); From 9f243f45816e39ae2e35193337026a5a3f7dea7d Mon Sep 17 00:00:00 2001 From: Gregor Date: Wed, 13 Mar 2024 17:24:15 +0100 Subject: [PATCH 26/41] submodules --- src/bindings | 2 +- src/mina | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/bindings b/src/bindings index 10fc60a86e..0b03d328d0 160000 --- a/src/bindings +++ b/src/bindings @@ -1 +1 @@ -Subproject commit 10fc60a86e87d2f19e4b49cce06ac86af63cbeb6 +Subproject commit 0b03d328d0ec6c59c6d5eb90e3e1174787fb4eac diff --git a/src/mina b/src/mina index 0ddc4b90f5..e818ecbe7c 160000 --- a/src/mina +++ b/src/mina @@ -1 +1 @@ -Subproject commit 0ddc4b90f54b73bb5279db690e74b4b7a0bd8495 +Subproject commit e818ecbe7c45ac3bd45c08f36220aa7e7d4e03d8 From 702eb1e8322d2c3f3722fd79d0f6582dd2c0e85a Mon Sep 17 00:00:00 2001 From: Gregor Date: Wed, 13 Mar 2024 21:16:01 +0100 Subject: [PATCH 27/41] compatible scale --- src/lib/field.ts | 42 ++++++++++++++++++++++++++++++++++++------ 1 file changed, 36 insertions(+), 6 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index f744c18c63..9088dbe80c 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -81,16 +81,24 @@ type ConstantFieldVar = [FieldType.Constant, FieldConst]; type VarFieldVar = [FieldType.Var, number]; const FieldVar = { + // constructors + Constant(x: FieldConst): ConstantFieldVar { + return [FieldType.Constant, x]; + }, + Var(x: number): VarFieldVar { + return [FieldType.Var, x]; + }, + Add(x: FieldVar, y: FieldVar): [FieldType.Add, FieldVar, FieldVar] { + return [FieldType.Add, x, y]; + }, + Scale(c: FieldConst, x: FieldVar): [FieldType.Scale, FieldConst, FieldVar] { + return [FieldType.Scale, c, x]; + }, + constant(x: bigint | FieldConst): ConstantFieldVar { let x0 = typeof x === 'bigint' ? FieldConst.fromBigint(x) : x; return [FieldType.Constant, x0]; }, - isConstant(x: FieldVar): x is ConstantFieldVar { - return x[0] === FieldType.Constant; - }, - isVar(x: FieldVar): x is VarFieldVar { - return x[0] === FieldType.Var; - }, add(x: FieldVar, y: FieldVar): FieldVar { if (FieldVar.isConstant(x) && x[1][1] === 0n) return y; if (FieldVar.isConstant(y) && y[1][1] === 0n) return x; @@ -106,8 +114,30 @@ const FieldVar = { if (FieldVar.isConstant(x)) { return FieldVar.constant(Fp.mul(c0[1], x[1][1])); } + if (FieldVar.isScale(x)) { + return [ + FieldType.Scale, + FieldConst.fromBigint(Fp.mul(c0[1], x[1][1])), + x[2], + ]; + } return [FieldType.Scale, c0, x]; }, + + // type guards + isConstant(x: FieldVar): x is ConstantFieldVar { + return x[0] === FieldType.Constant; + }, + isVar(x: FieldVar): x is VarFieldVar { + return x[0] === FieldType.Var; + }, + isAdd(x: FieldVar): x is [FieldType.Add, FieldVar, FieldVar] { + return x[0] === FieldType.Add; + }, + isScale(x: FieldVar): x is [FieldType.Scale, FieldConst, FieldVar] { + return x[0] === FieldType.Scale; + }, + [0]: [FieldType.Constant, FieldConst[0]] satisfies ConstantFieldVar, [1]: [FieldType.Constant, FieldConst[1]] satisfies ConstantFieldVar, [-1]: [FieldType.Constant, FieldConst[-1]] satisfies ConstantFieldVar, From 2f73b398cbea59b437b47993e3b2d1f6c8838306 Mon Sep 17 00:00:00 2001 From: Gregor Mitscha-Baude Date: Wed, 13 Mar 2024 22:00:53 +0100 Subject: [PATCH 28/41] use fieldvar combinators --- src/lib/field.ts | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 9088dbe80c..6f14fdbe0f 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -349,7 +349,7 @@ class Field { return new Field(Fp.add(this.toBigInt(), toFp(y))); } // return new AST node Add(x, y) - let z = Snarky.field.add(this.value, toFieldVar(y)); + let z = FieldVar.add(this.value, toFieldVar(y)); return new Field(z); } @@ -377,7 +377,7 @@ class Field { return new Field(Fp.negate(this.toBigInt())); } // return new AST node Scale(-1, x) - let z = Snarky.field.scale(FieldConst[-1], this.value); + let z = FieldVar.scale(FieldConst[-1], this.value); return new Field(z); } @@ -476,11 +476,11 @@ class Field { } // if one of the factors is constant, return Scale AST node if (isConstant(y)) { - let z = Snarky.field.scale(toFieldConst(y), this.value); + let z = FieldVar.scale(toFieldConst(y), this.value); return new Field(z); } if (this.isConstant()) { - let z = Snarky.field.scale(this.value[1], y.value); + let z = FieldVar.scale(this.value[1], y.value); return new Field(z); } // create a new witness for z = x*y @@ -651,7 +651,7 @@ class Field { assertMul( z, this, - Snarky.field.add(FieldVar[1], Snarky.field.scale(FieldConst[-1], b)) + FieldVar.add(FieldVar[1], FieldVar.scale(FieldConst[-1], b)) ); // ^^^ these prove that b = Bool(x === 0): // if x = 0, the 2nd equation implies b = 1 From 4c3d82a27699ac7d7287838fa268f18d82527f53 Mon Sep 17 00:00:00 2001 From: Gregor Mitscha-Baude Date: Wed, 13 Mar 2024 22:34:02 +0100 Subject: [PATCH 29/41] seal --- src/lib/field.ts | 11 +++++++++-- src/lib/gadgets/basic.ts | 10 +++++++++- src/snarky.d.ts | 5 ----- 3 files changed, 18 insertions(+), 8 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 6f14fdbe0f..4f4dac90d4 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -12,6 +12,7 @@ import { assertSquare, assertBoolean, } from './gadgets/compatible.js'; +import { toLinearCombination } from './gadgets/basic.js'; // external API export { Field }; @@ -1047,8 +1048,14 @@ class Field { * @return A {@link Field} element that is equal to the result of AST that was previously on this {@link Field} element. */ seal() { - if (this.isConstant()) return this; - let x = Snarky.field.seal(this.value); + let { constant, terms } = toLinearCombination(this.value); + if (terms.length === 0) return new Field(constant); + if (terms.length === 1 && constant === 0n) { + let [c, x] = terms[0]; + if (c === 1n) return new Field(x); + } + let x = Snarky.existsVar(() => Snarky.field.readVar(this.value)); + this.assertEquals(new Field(x)); return VarField(x); } diff --git a/src/lib/gadgets/basic.ts b/src/lib/gadgets/basic.ts index e4f8b564e8..ac07907300 100644 --- a/src/lib/gadgets/basic.ts +++ b/src/lib/gadgets/basic.ts @@ -17,7 +17,15 @@ import { TupleN } from '../util/types.js'; export { assertMul, arrayGet, assertOneOf }; // internal -export { reduceToScaledVar, emptyCell, linear, bilinear, ScaledVar, Constant }; +export { + reduceToScaledVar, + toLinearCombination, + emptyCell, + linear, + bilinear, + ScaledVar, + Constant, +}; /** * Assert multiplication constraint, `x * y === z` diff --git a/src/snarky.d.ts b/src/snarky.d.ts index 523708b73c..e484ee1aeb 100644 --- a/src/snarky.d.ts +++ b/src/snarky.d.ts @@ -316,11 +316,6 @@ declare const Snarky: { * does 16 bits per row (vs 1 bits per row that you can do with generic gates). */ truncateToBits16(lengthDiv16: number, x: FieldVar): FieldVar; - /** - * returns a new witness from an AST - * (implemented with toConstantAndTerms) - */ - seal(x: FieldVar): VarFieldVar; }; gates: { From 11191f03e6546290f3cf1bb9a2c06279cab8ade3 Mon Sep 17 00:00:00 2001 From: Gregor Mitscha-Baude Date: Wed, 13 Mar 2024 22:36:54 +0100 Subject: [PATCH 30/41] remove unused --- src/snarky.d.ts | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/snarky.d.ts b/src/snarky.d.ts index e484ee1aeb..4c8b0a711a 100644 --- a/src/snarky.d.ts +++ b/src/snarky.d.ts @@ -264,14 +264,6 @@ declare const Snarky: { * APIs to add constraints on field variables */ field: { - /** - * add x, y to get a new AST node Add(x, y); handles if x, y are constants - */ - add(x: FieldVar, y: FieldVar): FieldVar; - /** - * scale x by a constant to get a new AST node Scale(c, x); handles if x is a constant - */ - scale(c: FieldConst, x: FieldVar): FieldVar; /** * evaluates a CVar by walking the AST and reading Vars from a list of public input + aux values */ @@ -300,14 +292,6 @@ declare const Snarky: { x: FieldVar, y: FieldVar ): [_: 0, less: BoolVar, lessOrEqual: BoolVar]; - /** - * - */ - toBits(length: number, x: FieldVar): MlArray; - /** - * - */ - fromBits(bits: MlArray): FieldVar; /** * returns x truncated to the lowest `16 * lengthDiv16` bits * => can be used to assert that x fits in `16 * lengthDiv16` bits. From 5396c390cc1bdfe4b57a824b43a5cc886d486588 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:10:37 +0100 Subject: [PATCH 31/41] move exists, existsVar -> existsOne --- src/lib/field.ts | 16 ++++++++-------- src/lib/gadgets/common.ts | 4 ++-- src/lib/provable.ts | 2 +- src/snarky.d.ts | 31 +++++++++++++++---------------- 4 files changed, 26 insertions(+), 27 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 4f4dac90d4..284d5dc761 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -430,7 +430,7 @@ class Field { isEven() { if (this.isConstant()) return new Bool(this.toBigInt() % 2n === 0n); - let [, isOddVar, xDiv2Var] = Snarky.exists(2, () => { + let [, isOddVar, xDiv2Var] = Snarky.run.exists(2, () => { let bits = Fp.toBits(this.toBigInt()); let isOdd = bits.shift()! ? 1n : 0n; @@ -485,7 +485,7 @@ class Field { return new Field(z); } // create a new witness for z = x*y - let z = Snarky.existsVar(() => + let z = Snarky.run.existsOne(() => FieldConst.fromBigint(Fp.mul(this.toBigInt(), toFp(y))) ); // add a multiplication constraint @@ -517,7 +517,7 @@ class Field { return new Field(z); } // create a witness for z = x^(-1) - let z = Snarky.existsVar(() => { + let z = Snarky.run.existsOne(() => { let z = Fp.inverse(this.toBigInt()) ?? 0n; return FieldConst.fromBigint(z); }); @@ -584,7 +584,7 @@ class Field { return new Field(Fp.square(this.toBigInt())); } // create a new witness for z = x^2 - let z_ = Snarky.existsVar(() => + let z_ = Snarky.run.existsOne(() => FieldConst.fromBigint(Fp.square(this.toBigInt())) ); let z = new Field(z_); @@ -620,7 +620,7 @@ class Field { return new Field(z); } // create a witness for sqrt(x) - let z_ = Snarky.existsVar(() => { + let z_ = Snarky.run.existsOne(() => { let z = Fp.sqrt(this.toBigInt()) ?? 0n; return FieldConst.fromBigint(z); }); @@ -639,7 +639,7 @@ class Field { } // create witnesses z = 1/x, or z=0 if x=0, // and b = 1 - zx - let [, b, z] = Snarky.exists(2, () => { + let [, b, z] = Snarky.run.exists(2, () => { let x = this.toBigInt(); let z = Fp.inverse(x) ?? 0n; let b = Fp.sub(1n, Fp.mul(z, x)); @@ -680,7 +680,7 @@ class Field { return this.sub(y).isZero(); } // if both are variables, we create one new variable for x-y so that `isZero` doesn't create two - let xMinusY = Snarky.existsVar(() => + let xMinusY = Snarky.run.existsOne(() => FieldConst.fromBigint(Fp.sub(this.toBigInt(), toFp(y))) ); let z = new Field(xMinusY); @@ -1054,7 +1054,7 @@ class Field { let [c, x] = terms[0]; if (c === 1n) return new Field(x); } - let x = Snarky.existsVar(() => Snarky.field.readVar(this.value)); + let x = Snarky.run.existsOne(() => Snarky.field.readVar(this.value)); this.assertEquals(new Field(x)); return VarField(x); } diff --git a/src/lib/gadgets/common.ts b/src/lib/gadgets/common.ts index a32c8b6c5f..0d1ba58963 100644 --- a/src/lib/gadgets/common.ts +++ b/src/lib/gadgets/common.ts @@ -26,7 +26,7 @@ export { }; function existsOne(compute: () => bigint) { - let varMl = Snarky.existsVar(() => FieldConst.fromBigint(compute())); + let varMl = Snarky.run.existsOne(() => FieldConst.fromBigint(compute())); return VarField(varMl); } @@ -34,7 +34,7 @@ function exists TupleN>( n: N, compute: C ) { - let varsMl = Snarky.exists(n, () => + let varsMl = Snarky.run.exists(n, () => MlArray.mapTo(compute(), FieldConst.fromBigint) ); let vars = MlArray.mapFrom(varsMl, VarField); diff --git a/src/lib/provable.ts b/src/lib/provable.ts index ceff63ba68..57151d9483 100644 --- a/src/lib/provable.ts +++ b/src/lib/provable.ts @@ -239,7 +239,7 @@ function witness = FlexibleProvable>( let id = snarkContext.enter({ ...ctx, inWitnessBlock: true }); try { - let [, ...fieldVars] = Snarky.exists(type.sizeInFields(), () => { + let [, ...fieldVars] = Snarky.run.exists(type.sizeInFields(), () => { proverValue = compute(); let fields = type.toFields(proverValue); let fieldConstants = fields.map((x) => x.toConstant().value[1]); diff --git a/src/snarky.d.ts b/src/snarky.d.ts index 4c8b0a711a..105128214f 100644 --- a/src/snarky.d.ts +++ b/src/snarky.d.ts @@ -174,25 +174,24 @@ declare namespace Snarky { * Note for devs: This module is intended to closely mirror snarky-ml's core, low-level APIs. */ declare const Snarky: { - /** - * witness `sizeInFields` field element variables - * - * Note: this is called "exists" because in a proof, you use it like this: - * > "I prove that there exists x, such that (some statement)" - */ - exists( - sizeInFields: number, - compute: () => MlArray - ): MlArray; - /** - * witness a single field element variable - */ - existsVar(compute: () => FieldConst): VarFieldVar; - /** * APIs that have to do with running provable code */ run: { + /** + * witness `sizeInFields` field element variables + * + * Note: this is called "exists" because in a proof, you use it like this: + * > "I prove that there exists x, such that (some statement)" + */ + exists( + sizeInFields: number, + compute: () => MlArray + ): MlArray; + /** + * witness a single field element variable + */ + existsOne(compute: () => FieldConst): VarFieldVar; /** * Checks whether Snarky runs in "prover mode", that is, with witnesses */ @@ -229,7 +228,7 @@ declare const Snarky: { ): (fields: MlOption>) => MlArray; /** - * Snarky's internal state + * Operations on snarky's internal state */ state: { allocVar(state: SnarkyState): FieldVar; From 3f588b9edd6ca165997c5c07f32c713d1b3e18d1 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:14:06 +0100 Subject: [PATCH 32/41] remove dependence of gadgets common on Bool --- src/lib/gadgets/common.ts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/lib/gadgets/common.ts b/src/lib/gadgets/common.ts index 0d1ba58963..55d5f574c6 100644 --- a/src/lib/gadgets/common.ts +++ b/src/lib/gadgets/common.ts @@ -8,7 +8,7 @@ import { import { Tuple, TupleN } from '../util/types.js'; import { Snarky } from '../../snarky.js'; import { MlArray } from '../ml/base.js'; -import { Bool } from '../bool.js'; +import type { Bool } from '../bool.js'; import { fieldVar } from '../gates.js'; const MAX_BITS = 64 as const; @@ -78,10 +78,10 @@ function toVars>( * Can be used in provable code. */ function assert(stmt: boolean | Bool, message?: string): asserts stmt { - if (stmt instanceof Bool) { + if (typeof stmt === 'boolean') { + if (!stmt) throw Error(message ?? 'Assertion failed'); + } else { stmt.assertTrue(message ?? 'Assertion failed'); - } else if (!stmt) { - throw Error(message ?? 'Assertion failed'); } } From f999d33ef6bd72d779e3bb181c01c6ef34b25afe Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:16:38 +0100 Subject: [PATCH 33/41] bindings --- src/bindings | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bindings b/src/bindings index 0b03d328d0..7306b452d5 160000 --- a/src/bindings +++ b/src/bindings @@ -1 +1 @@ -Subproject commit 0b03d328d0ec6c59c6d5eb90e3e1174787fb4eac +Subproject commit 7306b452d5d26e2e588e92bc2d41c50f5097949f From e8ec39abc0f0dda107a9813c899558b84511b2f4 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:21:24 +0100 Subject: [PATCH 34/41] remove misguided max_bits constant --- src/lib/gadgets/bitwise.ts | 19 +++++++++---------- src/lib/gadgets/common.ts | 3 --- 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/src/lib/gadgets/bitwise.ts b/src/lib/gadgets/bitwise.ts index 7b34a3e85e..d0c741fbb1 100644 --- a/src/lib/gadgets/bitwise.ts +++ b/src/lib/gadgets/bitwise.ts @@ -3,7 +3,6 @@ import { Field as Fp } from '../../provable/field-bigint.js'; import { Field } from '../field.js'; import { Gates } from '../gates.js'; import { - MAX_BITS, assert, divideWithRemainder, toVar, @@ -204,13 +203,13 @@ function rotate64( ) { // Check that the rotation bits are in range assert( - bits >= 0 && bits <= MAX_BITS, + bits >= 0 && bits <= 64, `rotation: expected bits to be between 0 and 64, got ${bits}` ); if (field.isConstant()) { assert( - field.toBigInt() < 1n << BigInt(MAX_BITS), + field.toBigInt() < 1n << 64n, `rotation: expected field to be at most 64 bits, got ${field.toBigInt()}` ); return new Field(Fp.rot(field.toBigInt(), BigInt(bits), direction)); @@ -250,9 +249,9 @@ function rot64( bits: number, direction: 'left' | 'right' = 'left' ): [Field, Field, Field] { - const rotationBits = direction === 'right' ? MAX_BITS - bits : bits; - const big2Power64 = 2n ** BigInt(MAX_BITS); - const big2PowerRot = 2n ** BigInt(rotationBits); + const rotationBits = direction === 'right' ? 64 - bits : bits; + const big2Power64 = 1n << 64n; + const big2PowerRot = 1n << BigInt(rotationBits); const [rotated, excess, shifted, bound] = Provable.witness( Provable.Array(Field, 4), @@ -319,13 +318,13 @@ function rot64( function rightShift64(field: Field, bits: number) { assert( - bits >= 0 && bits <= MAX_BITS, + bits >= 0 && bits <= 64, `rightShift: expected bits to be between 0 and 64, got ${bits}` ); if (field.isConstant()) { assert( - field.toBigInt() < 2n ** BigInt(MAX_BITS), + field.toBigInt() < 1n << 64n, `rightShift: expected field to be at most 64 bits, got ${field.toBigInt()}` ); return new Field(Fp.rightShift(field.toBigInt(), bits)); @@ -336,13 +335,13 @@ function rightShift64(field: Field, bits: number) { function leftShift64(field: Field, bits: number) { assert( - bits >= 0 && bits <= MAX_BITS, + bits >= 0 && bits <= 64, `rightShift: expected bits to be between 0 and 64, got ${bits}` ); if (field.isConstant()) { assert( - field.toBigInt() < 2n ** BigInt(MAX_BITS), + field.toBigInt() < 1n << 64n, `rightShift: expected field to be at most 64 bits, got ${field.toBigInt()}` ); return new Field(Fp.leftShift(field.toBigInt(), bits)); diff --git a/src/lib/gadgets/common.ts b/src/lib/gadgets/common.ts index 55d5f574c6..72084a08e5 100644 --- a/src/lib/gadgets/common.ts +++ b/src/lib/gadgets/common.ts @@ -11,10 +11,7 @@ import { MlArray } from '../ml/base.js'; import type { Bool } from '../bool.js'; import { fieldVar } from '../gates.js'; -const MAX_BITS = 64 as const; - export { - MAX_BITS, exists, existsOne, toVars, From c59b0617aa4f435fcbd8869ad8233a559f70f77c Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:29:46 +0100 Subject: [PATCH 35/41] do a todo --- src/lib/bool.ts | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/lib/bool.ts b/src/lib/bool.ts index b63a6ee663..22cf60d4f7 100644 --- a/src/lib/bool.ts +++ b/src/lib/bool.ts @@ -5,6 +5,7 @@ import { FieldType, FieldVar, readVarMessage, + withMessage, } from './field.js'; import { Bool as B } from '../provable/field-bigint.js'; import { defineBinable } from '../bindings/lib/binable.js'; @@ -395,10 +396,3 @@ function toFieldVar(x: boolean | Bool): BoolVar { if (x instanceof Bool) return x.value; return FieldVar.constant(B(x)); } - -// TODO: This is duplicated -function withMessage(error: unknown, message?: string) { - if (message === undefined || !(error instanceof Error)) return error; - error.message = `${message}\n${error.message}`; - return error; -} From 7ba854c53a3cb7b5489f3650a2b850cc0406b0a6 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:30:10 +0100 Subject: [PATCH 36/41] improve unreachable error message --- src/lib/proof-system/prover-keys.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/proof-system/prover-keys.ts b/src/lib/proof-system/prover-keys.ts index c76db0ec71..02c79e8722 100644 --- a/src/lib/proof-system/prover-keys.ts +++ b/src/lib/proof-system/prover-keys.ts @@ -125,7 +125,7 @@ function encodeProverKey(value: SnarkKey): Uint8Array { } default: value satisfies never; - throw Error('todo'); + throw Error('unreachable'); } } @@ -165,7 +165,7 @@ function decodeProverKey(header: SnarkKeyHeader, bytes: Uint8Array): SnarkKey { } default: header satisfies never; - throw Error('todo'); + throw Error('unreachable'); } } From bbc4a9900f252c641eb4b503a4db3b601b4fe5b6 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:38:46 +0100 Subject: [PATCH 37/41] remove the misleading "range check helper" API --- src/lib/field.ts | 29 ----------------------------- src/lib/gadgets/range-check.ts | 7 ++++++- 2 files changed, 6 insertions(+), 30 deletions(-) diff --git a/src/lib/field.ts b/src/lib/field.ts index 284d5dc761..e5767a89b0 100644 --- a/src/lib/field.ts +++ b/src/lib/field.ts @@ -1007,35 +1007,6 @@ class Field { .seal(); } - /** - * Create a new {@link Field} element from the first `length` bits of this {@link Field} element. - * - * The `length` has to be a multiple of 16, and has to be between 0 and 255, otherwise the method throws. - * - * As {@link Field} elements are represented using [little endian binary representation](https://en.wikipedia.org/wiki/Endianness), - * the resulting {@link Field} element will equal the original one if it fits in `length` bits. - * - * @param length - The number of bits to take from this {@link Field} element. - * - * @return A {@link Field} element that is equal to the `length` of this {@link Field} element. - */ - rangeCheckHelper(length: number) { - checkBitLength('Field.rangeCheckHelper()', length); - if (length % 16 !== 0) - throw Error( - 'Field.rangeCheckHelper(): `length` has to be a multiple of 16.' - ); - let lengthDiv16 = length / 16; - if (this.isConstant()) { - let bits = Fp.toBits(this.toBigInt()) - .slice(0, length) - .concat(Array(Fp.sizeInBits - length).fill(false)); - return new Field(Fp.fromBits(bits)); - } - let x = Snarky.field.truncateToBits16(lengthDiv16, this.value); - return new Field(x); - } - /** * **Warning**: This function is mainly for internal use. Normally it is not intended to be used by a zkApp developer. * diff --git a/src/lib/gadgets/range-check.ts b/src/lib/gadgets/range-check.ts index a4b6161d92..ae51e53196 100644 --- a/src/lib/gadgets/range-check.ts +++ b/src/lib/gadgets/range-check.ts @@ -11,7 +11,6 @@ export { rangeCheck32, multiRangeCheck, compactMultiRangeCheck, - rangeCheckHelper, rangeCheckN, isInRangeN, rangeCheck8, @@ -239,6 +238,12 @@ function rangeCheck1Helper(inputs: { /** * Helper function that creates a new {@link Field} element from the first `length` bits of this {@link Field} element. + * + * This returns the `x` truncated to `length` bits. However, it does **not** prove this truncation or any + * other relation of the output with `x`. + * + * This only proves that the output value is in the range [0, 2^length), and so can be combined + * with the initial value to prove a range check. */ function rangeCheckHelper(length: number, x: Field) { assert( From 2a2debc775d22cb998cda7aa45b2be6d3870704b Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:39:47 +0100 Subject: [PATCH 38/41] fixup --- src/lib/gadgets/range-check.ts | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/lib/gadgets/range-check.ts b/src/lib/gadgets/range-check.ts index ae51e53196..f55a5d3fab 100644 --- a/src/lib/gadgets/range-check.ts +++ b/src/lib/gadgets/range-check.ts @@ -316,7 +316,7 @@ function rangeCheck16(x: Field) { return; } // check that x fits in 16 bits - x.rangeCheckHelper(16).assertEquals(x); + rangeCheckHelper(16, x).assertEquals(x); } function rangeCheck8(x: Field) { @@ -329,8 +329,8 @@ function rangeCheck8(x: Field) { } // check that x fits in 16 bits - x.rangeCheckHelper(16).assertEquals(x); + rangeCheckHelper(16, x).assertEquals(x); // check that 2^8 x fits in 16 bits let x256 = x.mul(1 << 8).seal(); - x256.rangeCheckHelper(16).assertEquals(x256); + rangeCheckHelper(16, x256).assertEquals(x256); } From 0021fb1671f7cdf54b66471b86607c92ef3eb57b Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:50:48 +0100 Subject: [PATCH 39/41] clarify and rename misleading "is in range" gadget --- src/lib/gadgets/gadgets.ts | 20 +++++++++-------- src/lib/gadgets/range-check.ts | 12 +++++++--- src/lib/int.ts | 40 +++++++++++++++++++++++++++------- 3 files changed, 52 insertions(+), 20 deletions(-) diff --git a/src/lib/gadgets/gadgets.ts b/src/lib/gadgets/gadgets.ts index fedbc8b89b..95489d8370 100644 --- a/src/lib/gadgets/gadgets.ts +++ b/src/lib/gadgets/gadgets.ts @@ -8,7 +8,7 @@ import { rangeCheck64, rangeCheck32, rangeCheckN, - isInRangeN, + isDefinitelyInRangeN, rangeCheck8, } from './range-check.js'; import { @@ -109,24 +109,26 @@ const Gadgets = { }, /** - * Checks whether the input value is in the range [0, 2^n). `n` must be a multiple of 16. + * Returns a boolean which being true proves that x is in the range [0, 2^n). * - * This function proves that the provided field element can be represented with `n` bits. - * If the field element exceeds `n` bits, `Bool(false)` is returned and `Bool(true)` otherwise. + * **Beware**: The output being false does **not** prove that x is not in the range [0, 2^n). + * This should not be viewed as a standalone provable method but as an advanced helper function + * for gadgets which need a weakened form of range check. * - * @param x - The value to be range-checked. + * @param x - The value to be weakly range-checked. * @param n - The number of bits to be considered for the range check. * - * @returns a Bool indicating whether the input value is in the range [0, 2^n). + * @returns a Bool that is definitely only true if the input is in the range [0, 2^n), + * but could also be false _even if_ the input is in the range [0, 2^n). * * @example * ```ts * const x = Provable.witness(Field, () => Field(12345678n)); - * let inRange = Gadgets.isInRangeN(32, x); // return Bool(true) + * let definitelyInRange = Gadgets.isDefinitelyInRangeN(32, x); // could be true or false * ``` */ - isInRangeN(n: number, x: Field) { - return isInRangeN(n, x); + isDefinitelyInRangeN(n: number, x: Field) { + return isDefinitelyInRangeN(n, x); }, /* * Asserts that the input value is in the range [0, 2^16). diff --git a/src/lib/gadgets/range-check.ts b/src/lib/gadgets/range-check.ts index f55a5d3fab..d110a6349b 100644 --- a/src/lib/gadgets/range-check.ts +++ b/src/lib/gadgets/range-check.ts @@ -12,7 +12,7 @@ export { multiRangeCheck, compactMultiRangeCheck, rangeCheckN, - isInRangeN, + isDefinitelyInRangeN, rangeCheck8, rangeCheck16, }; @@ -289,9 +289,15 @@ function rangeCheckN(n: number, x: Field, message: string = '') { } /** - * Checks that x is in the range [0, 2^n) and returns a Boolean indicating whether the check passed. + * Returns a boolean which, being true, proves that x is in the range [0, 2^n). + * + * **Beware**: The output being false does **not** prove that x is not in the range [0, 2^n). + * In other words, it can happen that this returns false even if x is in the range [0, 2^n). + * + * This should not be viewed as a standalone provable method but as an advanced helper function + * for gadgets which need a weakened form of range check. */ -function isInRangeN(n: number, x: Field) { +function isDefinitelyInRangeN(n: number, x: Field) { assert( n <= Fp.sizeInBits, `bit length must be ${Fp.sizeInBits} or less, got ${n}` diff --git a/src/lib/int.ts b/src/lib/int.ts index 0a835246a0..e12a8aec53 100644 --- a/src/lib/int.ts +++ b/src/lib/int.ts @@ -405,9 +405,15 @@ class UInt64 extends CircuitValue { let xMinusY = this.value.sub(y.value).seal(); let yMinusX = xMinusY.neg(); - let xMinusYFits = RangeCheck.isInRangeN(UInt64.NUM_BITS, xMinusY); + let xMinusYFits = RangeCheck.isDefinitelyInRangeN( + UInt64.NUM_BITS, + xMinusY + ); - let yMinusXFits = RangeCheck.isInRangeN(UInt64.NUM_BITS, yMinusX); + let yMinusXFits = RangeCheck.isDefinitelyInRangeN( + UInt64.NUM_BITS, + yMinusX + ); xMinusYFits.or(yMinusXFits).assertEquals(true); // x <= y if y - x fits in 64 bits @@ -425,9 +431,15 @@ class UInt64 extends CircuitValue { let xMinusY = this.value.sub(y.value).seal(); let yMinusX = xMinusY.neg(); - let xMinusYFits = RangeCheck.isInRangeN(UInt64.NUM_BITS, xMinusY); + let xMinusYFits = RangeCheck.isDefinitelyInRangeN( + UInt64.NUM_BITS, + xMinusY + ); - let yMinusXFits = RangeCheck.isInRangeN(UInt64.NUM_BITS, yMinusX); + let yMinusXFits = RangeCheck.isDefinitelyInRangeN( + UInt64.NUM_BITS, + yMinusX + ); xMinusYFits.or(yMinusXFits).assertEquals(true); // x <= y if y - x fits in 64 bits @@ -935,8 +947,14 @@ class UInt32 extends CircuitValue { } else { let xMinusY = this.value.sub(y.value).seal(); let yMinusX = xMinusY.neg(); - let xMinusYFits = RangeCheck.isInRangeN(UInt32.NUM_BITS, xMinusY); - let yMinusXFits = RangeCheck.isInRangeN(UInt32.NUM_BITS, yMinusX); + let xMinusYFits = RangeCheck.isDefinitelyInRangeN( + UInt32.NUM_BITS, + xMinusY + ); + let yMinusXFits = RangeCheck.isDefinitelyInRangeN( + UInt32.NUM_BITS, + yMinusX + ); xMinusYFits.or(yMinusXFits).assertEquals(true); // x <= y if y - x fits in 64 bits return yMinusXFits; @@ -952,8 +970,14 @@ class UInt32 extends CircuitValue { } else { let xMinusY = this.value.sub(y.value).seal(); let yMinusX = xMinusY.neg(); - let xMinusYFits = RangeCheck.isInRangeN(UInt32.NUM_BITS, xMinusY); - let yMinusXFits = RangeCheck.isInRangeN(UInt32.NUM_BITS, yMinusX); + let xMinusYFits = RangeCheck.isDefinitelyInRangeN( + UInt32.NUM_BITS, + xMinusY + ); + let yMinusXFits = RangeCheck.isDefinitelyInRangeN( + UInt32.NUM_BITS, + yMinusX + ); xMinusYFits.or(yMinusXFits).assertEquals(true); // x <= y if y - x fits in 64 bits return yMinusXFits; From f4da5d3bc497c018994a9c94e831ca88e0005cd4 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 15:54:44 +0100 Subject: [PATCH 40/41] changelog --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3b77842dbf..b7f1460b80 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -38,6 +38,9 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm - This prevents you from accidentally creating a `UInt64` without proving that it fits in 64 bits - Equivalent changes were made to `UInt32` - Fixed vulnerability in `Field.to/fromBits()` outlined in [#1023](https://github.com/o1-labs/o1js/issues/1023) by imposing a limit of 254 bits https://github.com/o1-labs/o1js/pull/1461 +- Remove `Field.rangeCheckHelper()` which was too low-level and easy to misuse https://github.com/o1-labs/o1js/pull/1485 + - Also, rename the misleadingly named `Gadgets.isInRangeN()` to `Gadgets.isDefinitelyInRangeN()` +- Rename `Bool.Unsafe.ofField()` to `Bool.Unsafe.fromField()` https://github.com/o1-labs/o1js/pull/1485 ### Added From 83d51a48b40c2c82d079a47a755e58179966721f Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 14 Mar 2024 16:02:28 +0100 Subject: [PATCH 41/41] remove Gadgets namespace export which confused TS to no end --- CHANGELOG.md | 2 ++ src/lib/gadgets/foreign-field.ts | 3 +++ src/lib/gadgets/foreign-field.unit-test.ts | 12 +++------ src/lib/gadgets/gadgets.ts | 30 +++++++++------------- src/lib/gadgets/test-utils.ts | 12 +++------ 5 files changed, 25 insertions(+), 34 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b7f1460b80..2686d8e543 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -41,6 +41,8 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm - Remove `Field.rangeCheckHelper()` which was too low-level and easy to misuse https://github.com/o1-labs/o1js/pull/1485 - Also, rename the misleadingly named `Gadgets.isInRangeN()` to `Gadgets.isDefinitelyInRangeN()` - Rename `Bool.Unsafe.ofField()` to `Bool.Unsafe.fromField()` https://github.com/o1-labs/o1js/pull/1485 +- Replace the namespaced type exports `Gadgets.Field3` and `Gadgets.ForeignField.Sum` with `Field3` and `ForeignFieldSum` + - Unfortunately, the namespace didn't play well with auto-imports in TypeScript ### Added diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts index c4fe120e6c..8990a2667b 100644 --- a/src/lib/gadgets/foreign-field.ts +++ b/src/lib/gadgets/foreign-field.ts @@ -556,6 +556,9 @@ function assertMul( assertMulInternal(x0, y0, xy0, f, message); } +/** + * Lazy sum of {@link Field3} elements, which can be used as input to `Gadgets.ForeignField.assertMul()`. + */ class Sum { #result?: Field3; #summands: Field3[]; diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts index 7a7831b565..7147a9a478 100644 --- a/src/lib/gadgets/foreign-field.unit-test.ts +++ b/src/lib/gadgets/foreign-field.unit-test.ts @@ -10,7 +10,7 @@ import { unit, } from '../testing/equivalent.js'; import { Random } from '../testing/random.js'; -import { Gadgets } from './gadgets.js'; +import { Field3, Gadgets } from './gadgets.js'; import { ZkProgram } from '../proof-system.js'; import { Provable } from '../provable.js'; import { assert } from './common.js'; @@ -35,7 +35,7 @@ import { } from './test-utils.js'; import { l2 } from './range-check.js'; -const { ForeignField, Field3 } = Gadgets; +const { ForeignField } = Gadgets; let sign = fromRandom(Random.oneOf(1n as const, -1n as const)); @@ -277,7 +277,7 @@ await equivalentAsync({ from: [f, f], to: f }, { runs })( // assert mul example // (x - y) * (x + y) = x^2 - y^2 -function assertMulExample(x: Gadgets.Field3, y: Gadgets.Field3, f: bigint) { +function assertMulExample(x: Field3, y: Field3, f: bigint) { // witness x^2, y^2 let x2 = Provable.witness(Field3.provable, () => ForeignField.mul(x, x, f)); let y2 = Provable.witness(Field3.provable, () => ForeignField.mul(y, y, f)); @@ -289,11 +289,7 @@ function assertMulExample(x: Gadgets.Field3, y: Gadgets.Field3, f: bigint) { ForeignField.assertMul(xMinusY, xPlusY, x2MinusY2, f); } -function assertMulExampleNaive( - x: Gadgets.Field3, - y: Gadgets.Field3, - f: bigint -) { +function assertMulExampleNaive(x: Field3, y: Field3, f: bigint) { // witness x^2, y^2 let x2 = Provable.witness(Field3.provable, () => ForeignField.mul(x, x, f)); let y2 = Provable.witness(Field3.provable, () => ForeignField.mul(y, y, f)); diff --git a/src/lib/gadgets/gadgets.ts b/src/lib/gadgets/gadgets.ts index 95489d8370..4da3b4d68f 100644 --- a/src/lib/gadgets/gadgets.ts +++ b/src/lib/gadgets/gadgets.ts @@ -22,11 +22,15 @@ import { leftShift32, } from './bitwise.js'; import { Field } from '../core.js'; -import { ForeignField, Field3, Sum } from './foreign-field.js'; +import { + ForeignField, + Field3, + Sum as ForeignFieldSum, +} from './foreign-field.js'; import { divMod32, addMod32 } from './arithmetic.js'; import { SHA256 } from './sha256.js'; -export { Gadgets }; +export { Gadgets, Field3, ForeignFieldSum }; const Gadgets = { /** @@ -688,7 +692,12 @@ const Gadgets = { * ForeignField.assertMul(xMinusY, z, aPlusBPlusC, f); * ``` */ - assertMul(x: Field3 | Sum, y: Field3 | Sum, z: Field3 | Sum, f: bigint) { + assertMul( + x: Field3 | ForeignFieldSum, + y: Field3 | ForeignFieldSum, + z: Field3 | ForeignFieldSum, + f: bigint + ) { return ForeignField.assertMul(x, y, z, f); }, @@ -820,18 +829,3 @@ const Gadgets = { */ SHA256: SHA256, }; - -export namespace Gadgets { - /** - * A 3-tuple of Fields, representing a 3-limb bigint. - */ - export type Field3 = [Field, Field, Field]; - - export namespace ForeignField { - /** - * Lazy sum of {@link Field3} elements, which can be used as input to {@link Gadgets.ForeignField.assertMul}. - */ - export type Sum = Sum_; - } -} -type Sum_ = Sum; diff --git a/src/lib/gadgets/test-utils.ts b/src/lib/gadgets/test-utils.ts index 6db27b513c..cc15759e6b 100644 --- a/src/lib/gadgets/test-utils.ts +++ b/src/lib/gadgets/test-utils.ts @@ -1,7 +1,7 @@ import type { FiniteField } from '../../bindings/crypto/finite-field.js'; import { ProvableSpec, spec } from '../testing/equivalent.js'; import { Random } from '../testing/random.js'; -import { Gadgets } from './gadgets.js'; +import { Field3 } from './gadgets.js'; import { assert } from './common.js'; import { Bytes } from '../provable-types/provable-types.js'; @@ -13,11 +13,9 @@ export { throwError, }; -const { Field3 } = Gadgets; - // test input specs -function foreignField(F: FiniteField): ProvableSpec { +function foreignField(F: FiniteField): ProvableSpec { return { rng: Random.otherField(F), there: Field3.from, @@ -30,7 +28,7 @@ function foreignField(F: FiniteField): ProvableSpec { function unreducedForeignField( maxBits: number, F: FiniteField -): ProvableSpec { +): ProvableSpec { return { rng: Random.bignat(1n << BigInt(maxBits)), there: Field3.from, @@ -45,9 +43,7 @@ function unreducedForeignField( } // for fields that must follow an unbiased distribution, like private keys -function uniformForeignField( - F: FiniteField -): ProvableSpec { +function uniformForeignField(F: FiniteField): ProvableSpec { return { rng: Random(F.random), there: Field3.from,