Skip to content

Commit

Permalink
Merge pull request #1216 from o1-labs/feature/multi-range-check
Browse files Browse the repository at this point in the history
Foreign fields 1: Multi-range-check gadgets
  • Loading branch information
mitschabaude authored Nov 3, 2023
2 parents a891c4b + 9a594c9 commit 222fe49
Show file tree
Hide file tree
Showing 8 changed files with 345 additions and 29 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm

- `Gadgets.leftShift() / Gadgets.rightShift()`, new provable method to support bitwise shifting for native field elements. https://github.com/o1-labs/o1js/pull/1194
- `Gadgets.and()`, new provable method to support bitwise and for native field elements. https://github.com/o1-labs/o1js/pull/1193
- `Gadgets.multiRangeCheck()` and `Gadgets.compactMultiRangeCheck()`, two building blocks for non-native arithmetic with bigints of size up to 264 bits. https://github.com/o1-labs/o1js/pull/1216

## [0.14.0](https://github.com/o1-labs/o1js/compare/045faa7...e8e7510e1)

Expand Down
2 changes: 1 addition & 1 deletion src/bindings
52 changes: 51 additions & 1 deletion src/lib/gadgets/gadgets.ts
Original file line number Diff line number Diff line change
@@ -1,7 +1,11 @@
/**
* Wrapper file for various gadgets, with a namespace and doccomments.
*/
import { rangeCheck64 } from './range-check.js';
import {
compactMultiRangeCheck,
multiRangeCheck,
rangeCheck64,
} from './range-check.js';
import { rotate, xor, and, leftShift, rightShift } from './bitwise.js';
import { Field } from '../core.js';

Expand Down Expand Up @@ -206,4 +210,50 @@ const Gadgets = {
and(a: Field, b: Field, length: number) {
return and(a, b, length);
},

/**
* Multi-range check.
*
* Proves that x, y, z are all in the range [0, 2^88).
*
* This takes 4 rows, so it checks 88*3/4 = 66 bits per row. This is slightly more efficient
* than 64-bit range checks, which can do 64 bits in 1 row.
*
* In particular, the 3x88-bit range check supports bigints up to 264 bits, which in turn is enough
* to support foreign field multiplication with moduli up to 2^259.
*
* @example
* ```ts
* Gadgets.multiRangeCheck([x, y, z]);
* ```
*
* @throws Throws an error if one of the input values exceeds 88 bits.
*/
multiRangeCheck(limbs: [Field, Field, Field]) {
multiRangeCheck(limbs);
},

/**
* Compact multi-range check
*
* This is a variant of {@link multiRangeCheck} where the first two variables are passed in
* combined form xy = x + 2^88*y.
*
* The gadget
* - splits up xy into x and y
* - proves that xy = x + 2^88*y
* - proves that x, y, z are all in the range [0, 2^88).
*
* The split form [x, y, z] is returned.
*
* @example
* ```ts
* let [x, y] = Gadgets.compactMultiRangeCheck([xy, z]);
* ```
*
* @throws Throws an error if `xy` exceeds 2*88 = 176 bits, or if z exceeds 88 bits.
*/
compactMultiRangeCheck(xy: Field, z: Field) {
return compactMultiRangeCheck(xy, z);
},
};
155 changes: 153 additions & 2 deletions src/lib/gadgets/range-check.ts
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,10 @@ import { Field } from '../field.js';
import * as Gates from '../gates.js';
import { bitSlice, exists } from './common.js';

export { rangeCheck64 };
export { rangeCheck64, multiRangeCheck, compactMultiRangeCheck, L };

/**
* Asserts that x is in the range [0, 2^64), handles constant case
* Asserts that x is in the range [0, 2^64)
*/
function rangeCheck64(x: Field) {
if (x.isConstant()) {
Expand Down Expand Up @@ -48,3 +48,154 @@ function rangeCheck64(x: Field) {
false // not using compact mode
);
}

// default bigint limb size
const L = 88n;
const twoL = 2n * L;
const lMask = (1n << L) - 1n;

/**
* Asserts that x, y, z \in [0, 2^88)
*/
function multiRangeCheck([x, y, z]: [Field, Field, Field]) {
if (x.isConstant() && y.isConstant() && z.isConstant()) {
if (x.toBigInt() >> L || y.toBigInt() >> L || z.toBigInt() >> L) {
throw Error(`Expected fields to fit in ${L} bits, got ${x}, ${y}, ${z}`);
}
return;
}

let [x64, x76] = rangeCheck0Helper(x);
let [y64, y76] = rangeCheck0Helper(y);
rangeCheck1Helper({ x64, x76, y64, y76, z, yz: new Field(0) });
}

/**
* Compact multi-range-check - checks
* - xy = x + 2^88*y
* - x, y, z \in [0, 2^88)
*
* Returns the full limbs x, y, z
*/
function compactMultiRangeCheck(xy: Field, z: Field): [Field, Field, Field] {
// constant case
if (xy.isConstant() && z.isConstant()) {
if (xy.toBigInt() >> twoL || z.toBigInt() >> L) {
throw Error(
`Expected fields to fit in ${twoL} and ${L} bits respectively, got ${xy}, ${z}`
);
}
let [x, y] = splitCompactLimb(xy.toBigInt());
return [new Field(x), new Field(y), z];
}

let [x, y] = exists(2, () => splitCompactLimb(xy.toBigInt()));

let [z64, z76] = rangeCheck0Helper(z, false);
let [x64, x76] = rangeCheck0Helper(x, true);
rangeCheck1Helper({ x64: z64, x76: z76, y64: x64, y76: x76, z: y, yz: xy });

return [x, y, z];
}

function splitCompactLimb(x01: bigint): [bigint, bigint] {
return [x01 & lMask, x01 >> L];
}

function rangeCheck0Helper(x: Field, isCompact = false): [Field, Field] {
// crumbs (2-bit limbs)
let [x0, x2, x4, x6, x8, x10, x12, x14] = exists(8, () => {
let xx = x.toBigInt();
return [
bitSlice(xx, 0, 2),
bitSlice(xx, 2, 2),
bitSlice(xx, 4, 2),
bitSlice(xx, 6, 2),
bitSlice(xx, 8, 2),
bitSlice(xx, 10, 2),
bitSlice(xx, 12, 2),
bitSlice(xx, 14, 2),
];
});

// 12-bit limbs
let [x16, x28, x40, x52, x64, x76] = exists(6, () => {
let xx = x.toBigInt();
return [
bitSlice(xx, 16, 12),
bitSlice(xx, 28, 12),
bitSlice(xx, 40, 12),
bitSlice(xx, 52, 12),
bitSlice(xx, 64, 12),
bitSlice(xx, 76, 12),
];
});

Gates.rangeCheck0(
x,
[x76, x64, x52, x40, x28, x16],
[x14, x12, x10, x8, x6, x4, x2, x0],
isCompact
);

// the two highest 12-bit limbs are returned because another gate
// is needed to add lookups for them
return [x64, x76];
}

function rangeCheck1Helper(inputs: {
x64: Field;
x76: Field;
y64: Field;
y76: Field;
z: Field;
yz: Field;
}) {
let { x64, x76, y64, y76, z, yz } = inputs;

// create limbs for current row
let [z22, z24, z26, z28, z30, z32, z34, z36, z38, z50, z62, z74, z86] =
exists(13, () => {
let zz = z.toBigInt();
return [
bitSlice(zz, 22, 2),
bitSlice(zz, 24, 2),
bitSlice(zz, 26, 2),
bitSlice(zz, 28, 2),
bitSlice(zz, 30, 2),
bitSlice(zz, 32, 2),
bitSlice(zz, 34, 2),
bitSlice(zz, 36, 2),
bitSlice(zz, 38, 12),
bitSlice(zz, 50, 12),
bitSlice(zz, 62, 12),
bitSlice(zz, 74, 12),
bitSlice(zz, 86, 2),
];
});

// create limbs for next row
let [z0, z2, z4, z6, z8, z10, z12, z14, z16, z18, z20] = exists(11, () => {
let zz = z.toBigInt();
return [
bitSlice(zz, 0, 2),
bitSlice(zz, 2, 2),
bitSlice(zz, 4, 2),
bitSlice(zz, 6, 2),
bitSlice(zz, 8, 2),
bitSlice(zz, 10, 2),
bitSlice(zz, 12, 2),
bitSlice(zz, 14, 2),
bitSlice(zz, 16, 2),
bitSlice(zz, 18, 2),
bitSlice(zz, 20, 2),
];
});

Gates.rangeCheck1(
z,
yz,
[z86, z74, z62, z50, z38, z36, z34, z32, z30, z28, z26, z24, z22],
[z20, z18, z16, x76, x64, y76, y64, z14, z12, z10, z8, z6, z4, z2, z0]
);
}
106 changes: 92 additions & 14 deletions src/lib/gadgets/range-check.unit-test.ts
Original file line number Diff line number Diff line change
@@ -1,49 +1,127 @@
import type { Gate } from '../../snarky.js';
import { mod } from '../../bindings/crypto/finite_field.js';
import { Field } from '../../lib/core.js';
import { ZkProgram } from '../proof_system.js';
import { Provable } from '../provable.js';
import {
Spec,
boolean,
equivalentAsync,
field,
fieldWithRng,
} from '../testing/equivalent.js';
import { Random } from '../testing/property.js';
import { assert, exists } from './common.js';
import { Gadgets } from './gadgets.js';
import { L } from './range-check.js';
import { expect } from 'expect';

let maybeUint64: Spec<bigint, Field> = {
...field,
rng: Random.map(Random.oneOf(Random.uint64, Random.uint64.invalid), (x) =>
mod(x, Field.ORDER)
),
let uint = (n: number | bigint): Spec<bigint, Field> => {
let uint = Random.bignat((1n << BigInt(n)) - 1n);
return fieldWithRng(uint);
};

let maybeUint = (n: number | bigint): Spec<bigint, Field> => {
let uint = Random.bignat((1n << BigInt(n)) - 1n);
return fieldWithRng(
Random.map(Random.oneOf(uint, uint.invalid), (x) => mod(x, Field.ORDER))
);
};

// constraint system sanity check

function csWithoutGenerics(gates: Gate[]) {
return gates.map((g) => g.type).filter((type) => type !== 'Generic');
}

let check64 = Provable.constraintSystem(() => {
let [x] = exists(1, () => [0n]);
Gadgets.rangeCheck64(x);
});
let multi = Provable.constraintSystem(() => {
let x = exists(3, () => [0n, 0n, 0n]);
Gadgets.multiRangeCheck(x);
});
let compact = Provable.constraintSystem(() => {
let [xy, z] = exists(2, () => [0n, 0n]);
Gadgets.compactMultiRangeCheck(xy, z);
});

let expectedLayout64 = ['RangeCheck0'];
let expectedLayoutMulti = ['RangeCheck0', 'RangeCheck0', 'RangeCheck1', 'Zero'];

expect(csWithoutGenerics(check64.gates)).toEqual(expectedLayout64);
expect(csWithoutGenerics(multi.gates)).toEqual(expectedLayoutMulti);
expect(csWithoutGenerics(compact.gates)).toEqual(expectedLayoutMulti);

// TODO: make a ZkFunction or something that doesn't go through Pickles
// --------------------------
// RangeCheck64 Gate
// --------------------------

let RangeCheck64 = ZkProgram({
name: 'range-check-64',
let RangeCheck = ZkProgram({
name: 'range-check',
methods: {
run: {
check64: {
privateInputs: [Field],
method(x) {
Gadgets.rangeCheck64(x);
},
},
checkMulti: {
privateInputs: [Field, Field, Field],
method(x, y, z) {
Gadgets.multiRangeCheck([x, y, z]);
},
},
checkCompact: {
privateInputs: [Field, Field],
method(xy, z) {
let [x, y] = Gadgets.compactMultiRangeCheck(xy, z);
x.add(y.mul(1n << L)).assertEquals(xy);
},
},
},
});

await RangeCheck64.compile();
await RangeCheck.compile();

// TODO: we use this as a test because there's no way to check custom gates quickly :(
await equivalentAsync({ from: [maybeUint64], to: boolean }, { runs: 3 })(

await equivalentAsync({ from: [maybeUint(64)], to: boolean }, { runs: 3 })(
(x) => {
if (x >= 1n << 64n) throw Error('expected 64 bits');
assert(x < 1n << 64n);
return true;
},
async (x) => {
let proof = await RangeCheck64.run(x);
return await RangeCheck64.verify(proof);
let proof = await RangeCheck.check64(x);
return await RangeCheck.verify(proof);
}
);

await equivalentAsync(
{ from: [maybeUint(L), uint(L), uint(L)], to: boolean },
{ runs: 3 }
)(
(x, y, z) => {
assert(!(x >> L) && !(y >> L) && !(z >> L), 'multi: not out of range');
return true;
},
async (x, y, z) => {
let proof = await RangeCheck.checkMulti(x, y, z);
return await RangeCheck.verify(proof);
}
);

await equivalentAsync(
{ from: [maybeUint(2n * L), uint(L)], to: boolean },
{ runs: 3 }
)(
(xy, z) => {
assert(!(xy >> (2n * L)) && !(z >> L), 'compact: not out of range');
return true;
},
async (xy, z) => {
let proof = await RangeCheck.checkCompact(xy, z);
return await RangeCheck.verify(proof);
}
);
Loading

0 comments on commit 222fe49

Please sign in to comment.