-
Notifications
You must be signed in to change notification settings - Fork 132
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #1259 from o1-labs/feature/gadgets-uint
add gadgets to API surface, UInt32, UInt64, implement rot32
- Loading branch information
Showing
14 changed files
with
923 additions
and
106 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,48 @@ | ||
import { provableTuple } from '../circuit_value.js'; | ||
import { Field } from '../core.js'; | ||
import { assert } from '../errors.js'; | ||
import { Provable } from '../provable.js'; | ||
import { rangeCheck32 } from './range-check.js'; | ||
|
||
export { divMod32, addMod32 }; | ||
|
||
function divMod32(n: Field) { | ||
if (n.isConstant()) { | ||
assert( | ||
n.toBigInt() < 1n << 64n, | ||
`n needs to fit into 64 bit, but got ${n.toBigInt()}` | ||
); | ||
|
||
let nBigInt = n.toBigInt(); | ||
let q = nBigInt >> 32n; | ||
let r = nBigInt - (q << 32n); | ||
return { | ||
remainder: new Field(r), | ||
quotient: new Field(q), | ||
}; | ||
} | ||
|
||
let [quotient, remainder] = Provable.witness( | ||
provableTuple([Field, Field]), | ||
() => { | ||
let nBigInt = n.toBigInt(); | ||
let q = nBigInt >> 32n; | ||
let r = nBigInt - (q << 32n); | ||
return [new Field(q), new Field(r)]; | ||
} | ||
); | ||
|
||
rangeCheck32(quotient); | ||
rangeCheck32(remainder); | ||
|
||
n.assertEquals(quotient.mul(1n << 32n).add(remainder)); | ||
|
||
return { | ||
remainder, | ||
quotient, | ||
}; | ||
} | ||
|
||
function addMod32(x: Field, y: Field) { | ||
return divMod32(x.add(y)).remainder; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,59 @@ | ||
import { ZkProgram } from '../proof_system.js'; | ||
import { | ||
equivalentProvable as equivalent, | ||
equivalentAsync, | ||
field, | ||
record, | ||
} from '../testing/equivalent.js'; | ||
import { Field } from '../core.js'; | ||
import { Gadgets } from './gadgets.js'; | ||
import { provable } from '../circuit_value.js'; | ||
import { assert } from './common.js'; | ||
|
||
let Arithmetic = ZkProgram({ | ||
name: 'arithmetic', | ||
publicOutput: provable({ | ||
remainder: Field, | ||
quotient: Field, | ||
}), | ||
methods: { | ||
divMod32: { | ||
privateInputs: [Field], | ||
method(a: Field) { | ||
return Gadgets.divMod32(a); | ||
}, | ||
}, | ||
}, | ||
}); | ||
|
||
await Arithmetic.compile(); | ||
|
||
const divMod32Helper = (x: bigint) => { | ||
let quotient = x >> 32n; | ||
let remainder = x - (quotient << 32n); | ||
return { remainder, quotient }; | ||
}; | ||
const divMod32Output = record({ remainder: field, quotient: field }); | ||
|
||
equivalent({ | ||
from: [field], | ||
to: divMod32Output, | ||
})( | ||
(x) => { | ||
assert(x < 1n << 64n, `x needs to fit in 64bit, but got ${x}`); | ||
return divMod32Helper(x); | ||
}, | ||
(x) => { | ||
return Gadgets.divMod32(x); | ||
} | ||
); | ||
|
||
await equivalentAsync({ from: [field], to: divMod32Output }, { runs: 3 })( | ||
(x) => { | ||
assert(x < 1n << 64n, `x needs to fit in 64bit, but got ${x}`); | ||
return divMod32Helper(x); | ||
}, | ||
async (x) => { | ||
return (await Arithmetic.divMod32(x)).publicOutput; | ||
} | ||
); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.