From 732ff6d7c2329596b383ea0e7d58da8740dd4f50 Mon Sep 17 00:00:00 2001 From: Billy Rennekamp Date: Wed, 18 Oct 2023 11:20:34 +0200 Subject: [PATCH 1/4] unfortunate results --- README.md | 6 +- circuits/approxMath.circom | 38 ++++---- circuits/calculateForce.circom | 150 ++++++++++++++++++------------- circuits/calculateMissile.circom | 54 ++++++----- circuits/forceAccumulator.circom | 72 ++++++++------- circuits/getDistance.circom | 6 +- 6 files changed, 184 insertions(+), 142 deletions(-) diff --git a/README.md b/README.md index 8418b19c..b02b9683 100644 --- a/README.md +++ b/README.md @@ -195,9 +195,9 @@ Currently the project is targeting [powersOfTau28_hez_final_20.ptau](https://git | stepState(2, 1) | 3,293 | | stepState(2, 10) | 32,930 | | stepState(2, 100) | 329,300 | -| stepState(3, 1) | 6,157 | -| stepState(3, 10) | 61,570 | -| stepState(3, 100) | 615,700 | +| stepState(3, 1) | 7,653 | +| stepState(3, 10) | 76,530 | +| stepState(3, 100) | 765,300 | | stepState(4, 1) | 9,863 | | stepState(4, 10) | 98,630 | | stepState(4, 100) | 986,300 | diff --git a/circuits/approxMath.circom b/circuits/approxMath.circom index c88e46af..ee38503f 100644 --- a/circuits/approxMath.circom +++ b/circuits/approxMath.circom @@ -103,23 +103,23 @@ template AbsoluteValueSubtraction (n) { out <== greaterValue - lesserValue; } -// TODO: Confirm this doesn't work because most_positive_number is too large for LessThan circuit -template AbsoluteValue() { - signal input in; - signal output out; - signal most_positive_number <== 10944121435919637611123202872628637544274182200208017171849102093287904247808; - // p = 21888242871839275222246405745257275088548364400416034343698204186575808495617; - // p_minus_one = 21888242871839275222246405745257275088548364400416034343698204186575808495616; - - component lessThan = LessThan(252); // TODO: confirm this is necessary for most_positive_number - lessThan.in[0] <== in; - lessThan.in[1] <== most_positive_number; - - component myMux = Mux1(); - myMux.c[0] <== in * -1; - myMux.c[1] <== in; // TODO: confirm whether cheaper to do p - in using p as signal - myMux.s <== lessThan.out; - - out <== myMux.out; -} +// NOTE: This isn't an efficient system because LessThan has max 252 bits, which could be overridden but still not ideal +// template AbsoluteValue() { +// signal input in; +// signal output out; +// signal most_positive_number <== 10944121435919637611123202872628637544274182200208017171849102093287904247808; +// // p = 21888242871839275222246405745257275088548364400416034343698204186575808495617; +// // p_minus_one = 21888242871839275222246405745257275088548364400416034343698204186575808495616; + +// component lessThan = LessThan(252); // TODO: confirm this is necessary for most_positive_number +// lessThan.in[0] <== in; +// lessThan.in[1] <== most_positive_number; + +// component myMux = Mux1(); +// myMux.c[0] <== in * -1; +// myMux.c[1] <== in; // TODO: confirm whether cheaper to do p - in using p as signal +// myMux.s <== lessThan.out; + +// out <== myMux.out; +// } diff --git a/circuits/calculateForce.circom b/circuits/calculateForce.circom index f148c5e5..985e2702 100644 --- a/circuits/calculateForce.circom +++ b/circuits/calculateForce.circom @@ -28,42 +28,59 @@ template CalculateForce() { return createVector(forceX, forceY); */ - var scalingFactor = 10**8; - var GScaled = 100 * scalingFactor; // TODO: these could be constrained, do they need to be? - // log("GScaled", GScaled); - var divisionBits = 120; // TODO: test the limits of this. + // NOTE: scalingFactorFactor appears in calculateMissile, forceAccumulator as well + var scalingFactorFactor = 8; // maxBits: 4 + var scalingFactor = 10**scalingFactorFactor; // maxBits: 27 + + var Gravity = 100; // maxBits: 7 + var minDistance = 200; // maxBits: 8 + + // NOTE: windowWidth appears in calculateMissile, forceAccumulator as well and needs to match + var windowWidth = 1000; // maxBits: 10 + var windowWidthScaled = windowWidth * scalingFactor; // maxBits: 37 + + + // TODO: these could be constrained, do they need to be? + var GScaled = Gravity * scalingFactor; // maxBits: 34 + // log("GScaled", GScaled); signal input in_bodies[2][5]; signal output out_forces[2]; - signal minDistanceScaled <== 200 * 200 * scalingFactor * scalingFactor; // NOTE: this is 200**2 so we have to square the scaling factor too + // NOTE: this is 200**2 so we have to square the scaling factor too + signal minDistanceScaled <== (minDistance ** 2) * (scalingFactor ** 2); // maxBits: 69 + // NOTE: minDistanceScaled is maximum of // log("minDistanceScaled", minDistanceScaled); - var body1_position_x = in_bodies[0][0]; + var body1_position_x = in_bodies[0][0]; // maxBits: 37 = windowWidthScaled // log("body1_position_x", body1_position_x); - var body1_position_y = in_bodies[0][1]; + var body1_position_y = in_bodies[0][1]; // maxBits: 37 = windowWidthScaled // log("body1_position_y", body1_position_y); - var body1_radius = in_bodies[0][4]; - var body2_position_x = in_bodies[1][0]; + // NOTE: maximum radius currently 13 + var body1_radius = in_bodies[0][4]; // maxBits: 31 = numBits(13 * scalingFactor) + + var body2_position_x = in_bodies[1][0]; // maxBits: 37 = windowWidthScaled // log("body2_position_x", body2_position_x); - var body2_position_y = in_bodies[1][1]; + var body2_position_y = in_bodies[1][1]; // maxBits: 37 = windowWidthScaled // log("body2_position_y", body2_position_y); - var body2_radius = in_bodies[1][4]; + + // NOTE: maximum radius currently 13 + var body2_radius = in_bodies[1][4]; // maxBits: 31 = numBits(13 * scalingFactor) - signal dx <== body2_position_x - body1_position_x; + signal dx <== body2_position_x - body1_position_x; // maxBits: 254 because it can be negative - component absoluteValueSubtraction = AbsoluteValueSubtraction(60); // TODO: test limit + component absoluteValueSubtraction = AbsoluteValueSubtraction(37); absoluteValueSubtraction.in[0] <== body1_position_x; absoluteValueSubtraction.in[1] <== body2_position_x; - signal dxAbs <== absoluteValueSubtraction.out; + signal dxAbs <== absoluteValueSubtraction.out; // maxBits: 37 - signal dy <== body2_position_y - body1_position_y; - component absoluteValueSubtraction2 = AbsoluteValueSubtraction(60); // TODO: test limit + signal dy <== body2_position_y - body1_position_y; // maxBits: 254 because it can be negative + component absoluteValueSubtraction2 = AbsoluteValueSubtraction(37); absoluteValueSubtraction2.in[0] <== body1_position_y; absoluteValueSubtraction2.in[1] <== body2_position_y; - signal dyAbs <== absoluteValueSubtraction2.out; + signal dyAbs <== absoluteValueSubtraction2.out; // maxBits: 37 // log("dx", dx); // log("dy", dy); @@ -72,118 +89,127 @@ template CalculateForce() { // log("dxAbs", dxAbs); // log("dyAbs", dyAbs); - signal dxs <== dxAbs * dxAbs; + signal dxs <== dxAbs * dxAbs; // maxBits: 74 = 37 * 2 // log("dxs", dxs); - signal dys <== dyAbs * dyAbs; + signal dys <== dyAbs * dyAbs; // maxBits: 74 = 37 * 2 // log("dys", dys); - signal unboundDistanceSquared <== dxs + dys; + signal unboundDistanceSquared <== dxs + dys; // maxBits: 75 = 74 + 1 // log("unboundDistanceSquared", unboundDistanceSquared); - component lessThan = LessThan(75); // NOTE: max distance should be corner to corner of max grid size + component lessThan = LessThan(75); // NOTE: also because unboundDistanceSquared is 75 + // NOTE: max distance should be corner to corner of max grid size // max grid is 1000_00000000 which means 1000_00000000 * sqrt(2) = 1414_21356237 // 1414_21356237**2 is 19,999,999,999,912,458,800,169 // 19,999,999,999,912,460,800,000 in bits is 76 // max number using 75 bits is 2**75 - 1 = 75,557,863,725,914,323,419,135 - lessThan.in[0] <== unboundDistanceSquared; - lessThan.in[1] <== minDistanceScaled; + lessThan.in[0] <== unboundDistanceSquared; // maxBits: 75 + lessThan.in[1] <== minDistanceScaled; // maxBits: 69 // distanceSquared <== is_below_minimum ? minDistanceScaled : unboundDistanceSquared; component myMux = Mux1(); - myMux.c[0] <== unboundDistanceSquared; - myMux.c[1] <== minDistanceScaled; + myMux.c[0] <== unboundDistanceSquared; // maxBits: 75 + myMux.c[1] <== minDistanceScaled; // maxBits: 69 myMux.s <== lessThan.out; - signal distanceSquared <== myMux.out; + signal distanceSquared <== myMux.out; // maxBits: 75 // NOTE: confirm this is correct - signal distance <-- approxSqrt(distanceSquared); + // NOTE: squre root should require half as many bits as the input + // TODO: confirm that 2 bit more is enough for the margin of error of distance * 2 + signal distance <-- approxSqrt(distanceSquared); // maxBits: 39 = 75 / 2 + 2 // log("distance", distance); // log("distanceSquared", distanceSquared); // bits should be maximum of the vectorLimiter which would be (10 * 10 ** 8) * (10 * 10 ** 8) which is under 60 bits - component acceptableMarginOfError = AcceptableMarginOfError(60); // TODO: test the limits of this. - acceptableMarginOfError.expected <== distance ** 2; - acceptableMarginOfError.actual <== distanceSquared; + component acceptableMarginOfError = AcceptableMarginOfError(78); // TODO: test the limits of this. + acceptableMarginOfError.expected <== distance ** 2; // maxBits: 78 = 39 * 2 + acceptableMarginOfError.actual <== distanceSquared; // maxBits: 75 // margin of error should be midpoint between squares acceptableMarginOfError.marginOfError <== distance * 2; // TODO: confrim if (distance * 2) +1 is needed acceptableMarginOfError.out === 1; - signal bodies_sum_tmp <== (body1_radius + body2_radius) * 4; // NOTE: this could be tweaked as a variable for "liveliness" of bodies + // NOTE: this could be tweaked as a variable for "liveliness" of bodies + signal bodies_sum_tmp <== (body1_radius + body2_radius) * 4; // maxBits: 34 = 31 + 1 + 2 // bodies_sum is 0 if either body1_radius or body2_radius is 0 component isZero = IsZero(); isZero.in <== body1_radius; component myMux2 = Mux1(); - myMux2.c[0] <== bodies_sum_tmp; - myMux2.c[1] <== 0; + myMux2.c[0] <== bodies_sum_tmp; // maxBits: 34 + myMux2.c[1] <== 0; // maxBits: 0 myMux2.s <== isZero.out; component isZero2 = IsZero(); - isZero2.in <== body2_radius; + isZero2.in <== body2_radius; // maxBits: 31 component myMux3 = Mux1(); - myMux3.c[0] <== myMux2.out; - myMux3.c[1] <== 0; + myMux3.c[0] <== myMux2.out; // maxBits: 34 + myMux3.c[1] <== 0; // maxBits: 0 myMux3.s <== isZero2.out; - signal bodies_sum <== myMux3.out; + signal bodies_sum <== myMux3.out; // maxBits: 34 // log("bodies_sum", bodies_sum); - signal distanceSquared_with_avg_denom <== distanceSquared * 2; // NOTE: this is a result of moving division to end of calculation to preserve precision + // NOTE: this is a result of moving division to end of calculation to preserve precision + signal distanceSquared_with_avg_denom <== distanceSquared * 2; // maxBits: 76 = 75 + 1 // log("distanceSquared_with_avg_denom", distanceSquared_with_avg_denom); - signal forceMag_numerator <== GScaled * bodies_sum * scalingFactor; // NOTE: distance should be divided by scaling factor, but we can multiply GScaled by scaling factor instead to prevent division rounding errors + + // NOTE: distance should be divided by scaling factor, but we can multiply GScaled by scaling factor instead to prevent division rounding errors + signal forceMag_numerator <== GScaled * bodies_sum * scalingFactor; // maxBits: 95 = 34 + 34 + 27 // log("forceMag_numerator", forceMag_numerator); - signal forceDenom <== distanceSquared_with_avg_denom * distance; + signal forceDenom <== distanceSquared_with_avg_denom * distance; // maxBits: 115 = 76 + 39 // log("forceDenom", forceDenom); - signal forceXnum <== dxAbs * forceMag_numerator; + signal forceXnum <== dxAbs * forceMag_numerator; // maxBits: 132 = 37 + 95 // log("forceXnum", forceXnum); - signal forceXunsigned <-- approxDiv(forceXnum, forceDenom); + signal forceXunsigned <-- approxDiv(forceXnum, forceDenom); // maxBits: 132 = forceXnum // log("forceXunsigned", forceXunsigned); // NOTE: the following constraints the approxDiv to ensure it's within the acceptable error of margin - signal approxNumerator1 <== forceXunsigned * forceDenom; - component acceptableErrorOfMarginDiv1 = AcceptableMarginOfError(divisionBits); // TODO: test the limits of this. - acceptableErrorOfMarginDiv1.expected <== forceXnum; - acceptableErrorOfMarginDiv1.actual <== approxNumerator1; + signal approxNumerator1 <== forceXunsigned * forceDenom; // maxBits: 247 = 132 + 115 + component acceptableErrorOfMarginDiv1 = AcceptableMarginOfError(247); + acceptableErrorOfMarginDiv1.expected <== forceXnum; // maxBits: 132 + acceptableErrorOfMarginDiv1.actual <== approxNumerator1; // maxBits: 247 acceptableErrorOfMarginDiv1.marginOfError <== forceDenom; // TODO: actually could be further reduced to (realDenom / 2) + 1 but then we're using division again acceptableErrorOfMarginDiv1.out === 1; // if dxAbs + dx is 0, then forceX should be negative component isZero3 = IsZero(); - isZero3.in <== dxAbs + dx; + // NOTE: isZero handles overflow bit values correctly + isZero3.in <== dxAbs + dx; // maxBits: 255 = max(37, 254) + 1 // log("isZero3", dxAbs + dx, isZero3.out); component myMux4 = Mux1(); - myMux4.c[0] <== forceXunsigned; - myMux4.c[1] <== forceXunsigned * -1; + myMux4.c[0] <== forceXunsigned; // maxBits: 132 + myMux4.c[1] <== forceXunsigned * -1; // maxBits: 254 myMux4.s <== isZero3.out; - signal forceX <== myMux4.out; + signal forceX <== myMux4.out; // maxBits: 254 // log("forceX", forceX); - signal forceYnum <== dyAbs * forceMag_numerator; + signal forceYnum <== dyAbs * forceMag_numerator; // maxBits: 132 = 37 + 95 // log("forceYnum", forceYnum); - signal forceYunsigned <-- approxDiv(forceYnum, forceDenom); + signal forceYunsigned <-- approxDiv(forceYnum, forceDenom); // maxBits: 132 = forceYnum // log("forceYunsigned", forceYunsigned); // NOTE: the following constraints the approxDiv to ensure it's within the acceptable error of margin - signal approxNumerator2 <== forceYunsigned * forceDenom; - component acceptableErrorOfMarginDiv2 = AcceptableMarginOfError(divisionBits); // TODO: test the limits of this. - acceptableErrorOfMarginDiv2.expected <== forceYnum; - acceptableErrorOfMarginDiv2.actual <== approxNumerator2; + signal approxNumerator2 <== forceYunsigned * forceDenom; // maxBits: 247 = 132 + 115 + component acceptableErrorOfMarginDiv2 = AcceptableMarginOfError(247); + acceptableErrorOfMarginDiv2.expected <== forceYnum; // maxBits: 132 + acceptableErrorOfMarginDiv2.actual <== approxNumerator2; // maxBits: 247 acceptableErrorOfMarginDiv2.marginOfError <== forceDenom; // TODO: actually could be further reduced to (realDenom / 2) + 1 but then we're using division again acceptableErrorOfMarginDiv2.out === 1; // if dyAbs + dy is 0, then forceY should be negative component isZero4 = IsZero(); - isZero4.in <== dyAbs + dy; + // NOTE: isZero handles overflow bit values correctly + isZero4.in <== dyAbs + dy; // maxBits: 255 = max(37, 254) + 1 component myMux5 = Mux1(); - myMux5.c[0] <== forceYunsigned; - myMux5.c[1] <== forceYunsigned * -1; + myMux5.c[0] <== forceYunsigned; // maxBits: 132 + myMux5.c[1] <== forceYunsigned * -1; // maxBits: 254 myMux5.s <== isZero4.out; - signal forceY <== myMux5.out; + signal forceY <== myMux5.out; // maxBits: 254 // log("forceY", forceY); - out_forces[0] <== forceX; - out_forces[1] <== forceY; + out_forces[0] <== forceX; // maxBits: 254 + out_forces[1] <== forceY; // maxBits: 254 } diff --git a/circuits/calculateMissile.circom b/circuits/calculateMissile.circom index dd9a7c92..77a587ec 100644 --- a/circuits/calculateMissile.circom +++ b/circuits/calculateMissile.circom @@ -14,9 +14,9 @@ This function calculates the movement of one missile using the following inputs: The calculation is a simple addition of the x vector with the x position and the y vector with the y position. -The missile is shot from position (0, windowWidth) and x vector is always positive +The missile is shot from position (0, windowWidthScaled) and x vector is always positive and y vector is always negative. If the missile reaches the edge of the screen it -will either be in the X direction at windowWidth or in the Y direction at 0. +will either be in the X direction at windowWidthScaled or in the Y direction at 0. If the missile reaches the edge of the screen in either direction it will be removed and the radius is reduced to 0. @@ -25,25 +25,35 @@ and the radius is reduced to 0. template CalculateMissile() { signal input in_missile[5]; - signal output out_missile[5]; + + // NOTE: scalingFactorFactor appears in calculateForce, forceAccumulator as well + var scalingFactorFactor = 8; // maxBits: 4 + var scalingFactor = 10**scalingFactorFactor; // maxBits: 27 + + + // NOTE: windowWidthScaled appears in forceAccumulator, calculateForce as well and needs to match + var windowWidth = 1000; // maxBits: 10 + var windowWidthScaled = windowWidth * scalingFactor; // maxBits: 37 + // TODO: confirm the max vector of missiles (may change frequently) - var maxVector = 1000000000; // using 10^8 decimals - // log("maxVector", maxVector); - // NOTE: windowWidth appears in forceAccumulator as well and needs to match - var windowWidth = 100000000000; // using 10^8 decimals + var maxVector = 10; // maxBits: 4 + var maxVectorScaled = maxVector * scalingFactor; // maxBits: 27 + // log("maxVectorScaled", maxVectorScaled); signal new_pos[2]; - new_pos[0] <== in_missile[0] + in_missile[2]; // position_x + vector_x - new_pos[1] <== in_missile[1] + in_missile[3]; // position_y + vector_y + // position_x + vector_x + new_pos[0] <== in_missile[0] + in_missile[2]; // maxBits: 38 = 37 + 1 = windowWidthScaled + 1 + // position_y + vector_y + new_pos[1] <== in_missile[1] + in_missile[3]; // maxBits: 38 = 37 + 1 = windowWidthScaled + 1 - // position X is only going to increase from 0 to windowWidth - // it needs to be kept less than windowWidth + // position X is only going to increase from 0 to windowWidthScaled + // it needs to be kept less than windowWidthScaled // can return 0 if it exceeds and use this information to remove the missile component positionLimiterX = Limiter(37); // TODO: confirm type matches bit limit - positionLimiterX.in <== new_pos[0] + maxVector; - positionLimiterX.limit <== windowWidth + maxVector; + positionLimiterX.in <== new_pos[0] + maxVectorScaled; // maxBits: 39 = max(38, 27) + 1 + positionLimiterX.limit <== windowWidthScaled + maxVectorScaled; // maxBits: 38 = max(37, 27) + 1 positionLimiterX.rather <== 0; // This is for the radius of the missile @@ -57,16 +67,16 @@ template CalculateMissile() { muxX.c[1] <== 0; muxX.s <== isZeroX.out; - // Since the plane goes from 0 to windowWidth on the y axis from top to bottom - // the missile will approach 0 after starting at windowWidth - // check whether it goes below 0 by using the maxVector as a buffer - // return 0 if it is below maxVector to remove the missile + // Since the plane goes from 0 to windowWidthScaled on the y axis from top to bottom + // the missile will approach 0 after starting at windowWidthScaled + // check whether it goes below 0 by using the maxVectorScaled as a buffer + // return 0 if it is below maxVectorScaled to remove the missile // TODO: this assumes a missile removal at less than or equal to 0 // make sure the JS also is <= 0 and not just < 0 for the missile removal // also check the general overboard logic. Would be an edge case but possible. - component positionLowerLimiterY = LowerLimiter(37); // TODO: confirm type matches bit limit - positionLowerLimiterY.in <== new_pos[1] + maxVector; - positionLowerLimiterY.limit <== maxVector; + component positionLowerLimiterY = LowerLimiter(39); // TODO: confirm type matches bit limit + positionLowerLimiterY.in <== new_pos[1] + maxVectorScaled; // maxBits: 39 = max(38, 27) + 1 + positionLowerLimiterY.limit <== maxVectorScaled; // maxBits: 27 positionLowerLimiterY.rather <== 0; component isZeroY = IsZero(); @@ -76,8 +86,8 @@ template CalculateMissile() { muxY.c[1] <== 0; muxY.s <== isZeroY.out; - out_missile[0] <== new_pos[0]; // position_x + vector_x - out_missile[1] <== new_pos[1]; // position_y + vector_y + out_missile[0] <== new_pos[0]; // maxBits: 38 + out_missile[1] <== new_pos[1]; // maxBits: 38 out_missile[2] <== in_missile[2]; out_missile[3] <== in_missile[3]; out_missile[4] <== muxY.out; // will have the update radius diff --git a/circuits/forceAccumulator.circom b/circuits/forceAccumulator.circom index 5a7a8fc4..fe61b034 100644 --- a/circuits/forceAccumulator.circom +++ b/circuits/forceAccumulator.circom @@ -19,23 +19,29 @@ include "calculateForce.circom"; // This will help us restrict bits needed for each type // maybe can streamline the square root and division -template ForceAccumulator(totalBodies) { +template ForceAccumulator(totalBodies) { // max 10 = maxBits: 4 signal input bodies[totalBodies][5]; signal output out_bodies[totalBodies][5]; - // [0] = position_x using 10^8 decimals - // [1] = position_y using 10^8 decimals - // [2] = vector_x using 10^8 decimals - // [3] = vector_y using 10^8 decimals - // [4] = radius using 10^8 decimals + // [0] = position_x | maxBits: 37 = windowWidthScaled + // [1] = position_y | maxBits: 37 = windowWidthScaled + // [2] = vector_x | maxBits: 254 = negative values are possible + // [3] = vector_y | maxBits: 254 = negative values are possible + // [4] = radius | maxBits: 31 = numBits(13 * scalingFactor) + // NOTE: scalingFactorFactor appears in calculateMissile, calculateForce as well + var scalingFactorFactor = 8; // maxBits: 4 + var scalingFactor = 10**scalingFactorFactor; // maxBits: 27 - var maxVector = 1000000000; // using 10^8 decimals - // NOTE: windowWidth appears in calculateMissile as well and needs to match - var windowWidth = 100000000000; // using 10^8 decimals + var maxVector = 10; // maxBits: 4 + var maxVectorScaled = 10 * scalingFactor; // maxBits: 31 + + // NOTE: windowWidth appears in calculateMissile, calculateForce, forceAccumulator as well and needs to match + var windowWidth = 1000; // maxBits: 10 + var windowWidthScaled = windowWidth * scalingFactor; // maxBits: 37 var accumulated_body_forces[totalBodies][2]; - var totalIterations = totalBodies * (totalBodies - 1) / 2; + var totalIterations = totalBodies * (totalBodies - 1) / 2; // maxBits: 7 component calculateForceComponent[totalIterations]; signal force_x[totalIterations]; signal force_y[totalIterations]; @@ -81,38 +87,38 @@ template ForceAccumulator(totalBodies) { // limit the magnitude of the vector vectorLimiterX[i] = Limiter(252); // TODO: confirm bits limit vectorLimiterX[i].in <== new_vector_x[i]; - vectorLimiterX[i].limit <== maxVector; // speedLimit - vectorLimiterX[i].rather <== maxVector; + vectorLimiterX[i].limit <== maxVectorScaled; // speedLimit + vectorLimiterX[i].rather <== maxVectorScaled; out_bodies[i][2] <== vectorLimiterX[i].out; vectorLimiterY[i] = Limiter(252); // TODO: confirm bits limit vectorLimiterY[i].in <== new_vector_y[i]; - vectorLimiterY[i].limit <== maxVector; // speedLimit - vectorLimiterY[i].rather <== maxVector; + vectorLimiterY[i].limit <== maxVectorScaled; // speedLimit + vectorLimiterY[i].rather <== maxVectorScaled; out_bodies[i][3] <== vectorLimiterY[i].out; // need to limit position so plane loops off edges - positionLimiterX[i] = Limiter(37); // NOTE: position is limited to maxWidth + (2*maxVector) which should be under 37 bits + positionLimiterX[i] = Limiter(37); // NOTE: position is limited to maxWidth + (2*maxVectorScaled) which should be under 37 bits // positionLimiter.x <== bodies[0][0] + vectorLimiter.limitedX; - positionLimiterX[i].in <== bodies[i][0] + vectorLimiterX[i].out + maxVector; // NOTE: adding maxVector ensures it is never negative - positionLimiterX[i].limit <== windowWidth + maxVector; // windowWidth - positionLimiterX[i].rather <== maxVector; - // NOTE: maxVector is still included, needs to be removed at end of calculation - positionLowerLimiterX[i] = LowerLimiter(37); // NOTE: position is limited to maxWidth + (2*maxVector) which should be under 37 bits + positionLimiterX[i].in <== bodies[i][0] + vectorLimiterX[i].out + maxVectorScaled; // NOTE: adding maxVectorScaled ensures it is never negative + positionLimiterX[i].limit <== windowWidthScaled + maxVectorScaled; // windowWidthScaled + positionLimiterX[i].rather <== maxVectorScaled; + // NOTE: maxVectorScaled is still included, needs to be removed at end of calculation + positionLowerLimiterX[i] = LowerLimiter(37); // NOTE: position is limited to maxWidth + (2*maxVectorScaled) which should be under 37 bits positionLowerLimiterX[i].in <== positionLimiterX[i].out; - positionLowerLimiterX[i].limit <== maxVector; - positionLowerLimiterX[i].rather <== windowWidth + maxVector; - out_bodies[i][0] <== positionLowerLimiterX[i].out - maxVector; - - positionLimiterY[i] = Limiter(37); // NOTE: position is limited to maxWidth + (2*maxVector) which should be under 37 bits - positionLimiterY[i].in <== bodies[i][1] + vectorLimiterY[i].out + maxVector; // NOTE: adding maxVector ensures it is never negative - positionLimiterY[i].limit <== windowWidth + maxVector; // windowWidth - positionLimiterY[i].rather <== maxVector; - // NOTE: maxVector is still included, needs to be removed at end of calculation - positionLowerLimiterY[i] = LowerLimiter(37); // NOTE: position is limited to maxWidth + (2*maxVector) which should be under 37 bits + positionLowerLimiterX[i].limit <== maxVectorScaled; + positionLowerLimiterX[i].rather <== windowWidthScaled + maxVectorScaled; + out_bodies[i][0] <== positionLowerLimiterX[i].out - maxVectorScaled; + + positionLimiterY[i] = Limiter(37); // NOTE: position is limited to maxWidth + (2*maxVectorScaled) which should be under 37 bits + positionLimiterY[i].in <== bodies[i][1] + vectorLimiterY[i].out + maxVectorScaled; // NOTE: adding maxVectorScaled ensures it is never negative + positionLimiterY[i].limit <== windowWidthScaled + maxVectorScaled; // windowWidthScaled + positionLimiterY[i].rather <== maxVectorScaled; + // NOTE: maxVectorScaled is still included, needs to be removed at end of calculation + positionLowerLimiterY[i] = LowerLimiter(37); // NOTE: position is limited to maxWidth + (2*maxVectorScaled) which should be under 37 bits positionLowerLimiterY[i].in <== positionLimiterY[i].out; - positionLowerLimiterY[i].limit <== maxVector; - positionLowerLimiterY[i].rather <== windowWidth + maxVector; - out_bodies[i][1] <== positionLowerLimiterY[i].out - maxVector; + positionLowerLimiterY[i].limit <== maxVectorScaled; + positionLowerLimiterY[i].rather <== windowWidthScaled + maxVectorScaled; + out_bodies[i][1] <== positionLowerLimiterY[i].out - maxVectorScaled; // log(i, "out_bodies[i][2]", out_bodies[i][2]); } // log("out_bodies[0][0]", out_bodies[0][0]); diff --git a/circuits/getDistance.circom b/circuits/getDistance.circom index 8d977b9e..4c260f0c 100644 --- a/circuits/getDistance.circom +++ b/circuits/getDistance.circom @@ -10,13 +10,13 @@ template GetDistance(n) { signal output distance; // signal dx <== x2 - x1; - component absoluteValueSubtraction = AbsoluteValueSubtraction(n); // TODO: test limit + component absoluteValueSubtraction = AbsoluteValueSubtraction(n); absoluteValueSubtraction.in[0] <== x1; absoluteValueSubtraction.in[1] <== x2; signal dxAbs <== absoluteValueSubtraction.out; // signal dy <== y2 - y1; - component absoluteValueSubtraction2 = AbsoluteValueSubtraction(n); // TODO: test limit + component absoluteValueSubtraction2 = AbsoluteValueSubtraction(n); absoluteValueSubtraction2.in[0] <== y1; absoluteValueSubtraction2.in[1] <== y2; signal dyAbs <== absoluteValueSubtraction2.out; @@ -28,7 +28,7 @@ template GetDistance(n) { // NOTE: confirm this is correct distance <-- approxSqrt(distanceSquared); // bits should be maximum of the vectorLimiter which would be (10 * 10 ** 8) * (10 * 10 ** 8) which is under 60 bits - component acceptableMarginOfError = AcceptableMarginOfError(n); // TODO: test the limits of this. + component acceptableMarginOfError = AcceptableMarginOfError(n); acceptableMarginOfError.expected <== distanceSquared; acceptableMarginOfError.actual <== distance ** 2; // margin of error should be midpoint between squares From 84d5ddf730d4debeb59e055adb1868dce42cd61b Mon Sep 17 00:00:00 2001 From: Billy Rennekamp Date: Wed, 18 Oct 2023 11:22:35 +0200 Subject: [PATCH 2/4] readme results --- README.md | 25 +++---------------------- 1 file changed, 3 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index b02b9683..b68abbe2 100644 --- a/README.md +++ b/README.md @@ -174,33 +174,14 @@ Currently the project is targeting [powersOfTau28_hez_final_20.ptau](https://git |---------|-------------| | absoluteValueSubtraction(252) | 257 | | acceptableMarginOfError(60) | 126 | -| calculateForce() | 842 | +| calculateForce() | 1,340 | | detectCollision(3) | 1,548 | -| forceAccumulator(3) | 4,518 | +| forceAccumulator(3) | 6,012 | | getDistance(252) | 1,026 | | limiter(252) | 254 | | lowerLimiter(252) | 254 | -| nft(2, 1) | 2,170 | -| nft(2, 10) | 21,700 | -| nft(2, 100) | 217,000 | -| nft(3, 1) | 4,518 | -| nft(3, 10) | 45,180 | -| nft(3, 100) | 451,800 | -| nft(4, 1) | 7708 | -| nft(4, 10) | 77,080 | -| nft(4, 100) | 770,800 | -| nft(5, 1) | 11,740 | -| nft(5, 10) | 117,400 | -| nft(5, 100) | 1,174,000 | -| stepState(2, 1) | 3,293 | -| stepState(2, 10) | 32,930 | -| stepState(2, 100) | 329,300 | -| stepState(3, 1) | 7,653 | +| nft(3, 10) | 60,120 | | stepState(3, 10) | 76,530 | -| stepState(3, 100) | 765,300 | -| stepState(4, 1) | 9,863 | -| stepState(4, 10) | 98,630 | -| stepState(4, 100) | 986,300 | # built using circom-starter From 2c47bd2d9f9a6cc8628d7123d29960749aad3155 Mon Sep 17 00:00:00 2001 From: Billy Rennekamp Date: Thu, 19 Oct 2023 12:25:58 +0200 Subject: [PATCH 3/4] pause for help --- circuits/calculateForce.circom | 47 ++++++++++++++++------------- circuits/forceAccumulator.circom | 51 +++++++++++++++++++++----------- circuits/helpers.circom | 17 +++++++++++ 3 files changed, 78 insertions(+), 37 deletions(-) create mode 100644 circuits/helpers.circom diff --git a/circuits/calculateForce.circom b/circuits/calculateForce.circom index 985e2702..f3b31663 100644 --- a/circuits/calculateForce.circom +++ b/circuits/calculateForce.circom @@ -1,6 +1,7 @@ pragma circom 2.1.6; include "approxMath.circom"; +include "helpers.circom"; template CalculateForce() { /* @@ -46,28 +47,30 @@ template CalculateForce() { var GScaled = Gravity * scalingFactor; // maxBits: 34 // log("GScaled", GScaled); - signal input in_bodies[2][5]; - signal output out_forces[2]; + signal input in_bodies[2][7]; + signal output out_forces[2][2]; // type is an array where [n][v] such that n is whether + // the vector is negative or not (0 not negative, 1 is negative) and v is the absolute + // value of the vector, with maxBit: xxx // NOTE: this is 200**2 so we have to square the scaling factor too signal minDistanceScaled <== (minDistance ** 2) * (scalingFactor ** 2); // maxBits: 69 // NOTE: minDistanceScaled is maximum of // log("minDistanceScaled", minDistanceScaled); - var body1_position_x = in_bodies[0][0]; // maxBits: 37 = windowWidthScaled + var body1_position_x = getX(in_bodies[0]); // maxBits: 37 = windowWidthScaled // log("body1_position_x", body1_position_x); - var body1_position_y = in_bodies[0][1]; // maxBits: 37 = windowWidthScaled + var body1_position_y = getY(in_bodies[0]); // maxBits: 37 = windowWidthScaled // log("body1_position_y", body1_position_y); // NOTE: maximum radius currently 13 - var body1_radius = in_bodies[0][4]; // maxBits: 31 = numBits(13 * scalingFactor) + var body1_radius = getMass(in_bodies[0]); // maxBits: 31 = numBits(13 * scalingFactor) - var body2_position_x = in_bodies[1][0]; // maxBits: 37 = windowWidthScaled + var body2_position_x = getX(in_bodies[1]); // maxBits: 37 = windowWidthScaled // log("body2_position_x", body2_position_x); - var body2_position_y = in_bodies[1][1]; // maxBits: 37 = windowWidthScaled + var body2_position_y = getY(in_bodies[1]); // maxBits: 37 = windowWidthScaled // log("body2_position_y", body2_position_y); // NOTE: maximum radius currently 13 - var body2_radius = in_bodies[1][4]; // maxBits: 31 = numBits(13 * scalingFactor) + var body2_radius = getMass(in_bodies[1]); // maxBits: 31 = numBits(13 * scalingFactor) signal dx <== body2_position_x - body1_position_x; // maxBits: 254 because it can be negative @@ -178,12 +181,14 @@ template CalculateForce() { // NOTE: isZero handles overflow bit values correctly isZero3.in <== dxAbs + dx; // maxBits: 255 = max(37, 254) + 1 // log("isZero3", dxAbs + dx, isZero3.out); - component myMux4 = Mux1(); - myMux4.c[0] <== forceXunsigned; // maxBits: 132 - myMux4.c[1] <== forceXunsigned * -1; // maxBits: 254 - myMux4.s <== isZero3.out; - signal forceX <== myMux4.out; // maxBits: 254 + // component myMux4 = Mux1(); + // myMux4.c[0] <== forceXunsigned; // maxBits: 132 + // myMux4.c[1] <== forceXunsigned * -1; // maxBits: 254 + // myMux4.s <== isZero3.out; + // signal forceX <== myMux4.out; // maxBits: 254 // log("forceX", forceX); + out_forces[0][0] <== isZero3.out; // isZero is 1 when dx is negative + out_forces[0][1] <== forceXunsigned; // maxBits 132 signal forceYnum <== dyAbs * forceMag_numerator; // maxBits: 132 = 37 + 95 // log("forceYnum", forceYnum); @@ -201,15 +206,17 @@ template CalculateForce() { component isZero4 = IsZero(); // NOTE: isZero handles overflow bit values correctly isZero4.in <== dyAbs + dy; // maxBits: 255 = max(37, 254) + 1 - component myMux5 = Mux1(); - myMux5.c[0] <== forceYunsigned; // maxBits: 132 - myMux5.c[1] <== forceYunsigned * -1; // maxBits: 254 - myMux5.s <== isZero4.out; - signal forceY <== myMux5.out; // maxBits: 254 + // component myMux5 = Mux1(); + // myMux5.c[0] <== forceYunsigned; // maxBits: 132 + // myMux5.c[1] <== forceYunsigned * -1; // maxBits: 254 + // myMux5.s <== isZero4.out; + // signal forceY <== myMux5.out; // maxBits: 254 // log("forceY", forceY); + out_forces[1][0] <== isZero4.out; + out_forces[1][1] <== forceYunsigned; // maxBits 132 - out_forces[0] <== forceX; // maxBits: 254 - out_forces[1] <== forceY; // maxBits: 254 + // out_forces[0] <== forceX; // maxBits: 254 + // out_forces[1] <== forceY; // maxBits: 254 } diff --git a/circuits/forceAccumulator.circom b/circuits/forceAccumulator.circom index fe61b034..3303c67c 100644 --- a/circuits/forceAccumulator.circom +++ b/circuits/forceAccumulator.circom @@ -2,6 +2,7 @@ pragma circom 2.1.6; include "limiter.circom"; include "calculateForce.circom"; +include "helpers.circom"; // TODO: // √ confirm why circom interprets negative input differently than p-n (https://github.com/0xPARC/zkrepl/issues/11) @@ -20,13 +21,13 @@ include "calculateForce.circom"; // maybe can streamline the square root and division template ForceAccumulator(totalBodies) { // max 10 = maxBits: 4 - signal input bodies[totalBodies][5]; - signal output out_bodies[totalBodies][5]; - // [0] = position_x | maxBits: 37 = windowWidthScaled - // [1] = position_y | maxBits: 37 = windowWidthScaled - // [2] = vector_x | maxBits: 254 = negative values are possible - // [3] = vector_y | maxBits: 254 = negative values are possible - // [4] = radius | maxBits: 31 = numBits(13 * scalingFactor) + signal input bodies[totalBodies][7]; + signal output out_bodies[totalBodies][7]; + // [0] = position_x | maxBits: 37 = windowWidthScaled + // [1] = position_y | maxBits: 37 = windowWidthScaled + // [[2],[3]] = vector_x | maxBits: 133= 2 * maxVectorScaled = 1 + 132 + // [[4],[5]] = vector_y | maxBits: 133 = 2 * maxVectorScaled = 1 + 132 + // [6] = radius | maxBits: 31 = numBits(13 * scalingFactor) // NOTE: scalingFactorFactor appears in calculateMissile, calculateForce as well var scalingFactorFactor = 8; // maxBits: 4 @@ -39,31 +40,47 @@ template ForceAccumulator(totalBodies) { // max 10 = maxBits: 4 var windowWidth = 1000; // maxBits: 10 var windowWidthScaled = windowWidth * scalingFactor; // maxBits: 37 - var accumulated_body_forces[totalBodies][2]; var totalIterations = totalBodies * (totalBodies - 1) / 2; // maxBits: 7 component calculateForceComponent[totalIterations]; - signal force_x[totalIterations]; - signal force_y[totalIterations]; + signal force_x[totalIterations][2]; // maxBits: 132 + signal force_y[totalIterations][2]; // maxBits: 132 + signal accumulated_body_forces[totalIterations + 1][totalBodies][2]; + component mux[totalIterations * 2]; var ii = 0; for (var i = 0; i < totalBodies; i++) { // radius of body doesn't change - out_bodies[i][4] <== bodies[i][4]; + out_bodies[i][6] <== getMass(bodies[i]); for (var j = i+1; j < totalBodies; j++) { // var ii = i + j - 1; // calculate the force between i and j calculateForceComponent[ii] = CalculateForce(); calculateForceComponent[ii].in_bodies[0] <== bodies[i]; calculateForceComponent[ii].in_bodies[1] <== bodies[j]; - force_x[ii] <== calculateForceComponent[ii].out_forces[0]; - force_y[ii] <== calculateForceComponent[ii].out_forces[1]; + force_x[ii] <== calculateForceComponent[ii].out_forces[0]; // maxBits: 132 + force_y[ii] <== calculateForceComponent[ii].out_forces[1]; // maxBits: 132 // accumulate the value of the force on body i and body j // log("j", j, "force_x[ii]", force_x[ii]); - accumulated_body_forces[i][0] = accumulated_body_forces[i][0] + force_x[ii]; - accumulated_body_forces[i][1] = accumulated_body_forces[i][1] + force_y[ii]; - accumulated_body_forces[j][0] = accumulated_body_forces[j][0] - force_x[ii]; - accumulated_body_forces[j][1] = accumulated_body_forces[j][1] - force_y[ii]; + + mux[ii] = MultiMux1(2); + mux[ii].c[0][0] <== accumulated_body_forces[ii][i][0] + force_x[ii][1]; + mux[ii].c[0][1] <== accumulated_body_forces[ii][i][0] - force_x[ii][1]; + mux[ii].c[1][0] <== accumulated_body_forces[ii][j][0] - force_x[ii][1]; + mux[ii].c[1][1] <== accumulated_body_forces[ii][j][0] + force_x[ii][1]; + mux[ii].s <== force_x[ii][0]; + accumulated_body_forces[ii + 1][i][0] <== mux[ii].out[0]; + accumulated_body_forces[ii + 1][j][0] <== mux[ii].out[1]; + + mux[totalIterations + ii] = MultiMux1(2); + mux[ii].c[0][0] <== accumulated_body_forces[ii][i][1] + force_y[ii][1]; + mux[ii].c[0][1] <== accumulated_body_forces[ii][i][1] - force_y[ii][1]; + mux[ii].c[1][0] <== accumulated_body_forces[ii][j][1] - force_y[ii][1]; + mux[ii].c[1][1] <== accumulated_body_forces[ii][j][1] + force_y[ii][1]; + mux[ii].s <== force_y[ii][0]; + accumulated_body_forces[ii + 1][i][1] <== mux[ii].out[0]; + accumulated_body_forces[ii + 1][j][1] <== mux[ii].out[1]; + ii = ii + 1; } } diff --git a/circuits/helpers.circom b/circuits/helpers.circom new file mode 100644 index 00000000..509cb441 --- /dev/null +++ b/circuits/helpers.circom @@ -0,0 +1,17 @@ +pragma circom 2.1.6; + +function getX(body) { + return body[0]; +} +function getY(body) { + return body[1]; +} +function getVx(body) { + return [body[2], body[3]]; +} +function getVy(body) { + return [body[4], body[5]]; +} +function getMass(body) { + return body[6]; +} \ No newline at end of file From 5eb58cfedf0ef277d8db4eeda19148732d5d82f3 Mon Sep 17 00:00:00 2001 From: Billy Rennekamp Date: Sat, 21 Oct 2023 17:08:51 +0200 Subject: [PATCH 4/4] break up vector and reduce scaling factor --- README.md | 20 +-- circuits/calculateForce.circom | 160 ++++++++++------------- circuits/detectCollision.circom | 28 ++--- circuits/forceAccumulator.circom | 175 ++++++++++++++++---------- circuits/getDistance.circom | 37 +++--- circuits/getDistanceMain.circom | 2 +- circuits/helpers.circom | 6 +- circuits/nft.json | 6 +- circuits/stepStateMain.json | 6 +- docs/index.js | 32 ++--- test/absoluteValueSubtraction.test.js | 1 + test/acceptableMarginOfError.test.js | 1 + test/calculateForceMain.test.js | 52 +++++--- test/detectCollisionMain.test.js | 9 +- test/forceAccumulator.test.js | 10 +- test/getDistanceMain.test.js | 11 +- test/limiterMain.test.js | 1 + test/lowerLimiterMain.test.js | 1 + test/nft.test.js | 9 +- test/stepStateMain.test.js | 10 +- 20 files changed, 301 insertions(+), 276 deletions(-) diff --git a/README.md b/README.md index b68abbe2..f3bd175a 100644 --- a/README.md +++ b/README.md @@ -172,16 +172,16 @@ Currently the project is targeting [powersOfTau28_hez_final_20.ptau](https://git | Circuit | Non-Linear Constraints | |---------|-------------| -| absoluteValueSubtraction(252) | 257 | -| acceptableMarginOfError(60) | 126 | -| calculateForce() | 1,340 | -| detectCollision(3) | 1,548 | -| forceAccumulator(3) | 6,012 | -| getDistance(252) | 1,026 | -| limiter(252) | 254 | -| lowerLimiter(252) | 254 | -| nft(3, 10) | 60,120 | -| stepState(3, 10) | 76,530 | +| absoluteValueSubtraction(252) | 259 | +| acceptableMarginOfError(60) | 128 | +| calculateForce() | 717 | +| detectCollision(3) | 526 | +| forceAccumulator(3) | 2821 | +| getDistance(20) | 142 | +| limiter(252) | 257 | +| lowerLimiter(252) | 257 | +| nft(3, 10) | 28039 | +| stepState(3, 10) | 33891 | # built using circom-starter diff --git a/circuits/calculateForce.circom b/circuits/calculateForce.circom index f3b31663..a298ccf3 100644 --- a/circuits/calculateForce.circom +++ b/circuits/calculateForce.circom @@ -31,8 +31,8 @@ template CalculateForce() { // NOTE: scalingFactorFactor appears in calculateMissile, forceAccumulator as well - var scalingFactorFactor = 8; // maxBits: 4 - var scalingFactor = 10**scalingFactorFactor; // maxBits: 27 + var scalingFactorFactor = 3; // maxBits: 2 + var scalingFactor = 10**scalingFactorFactor; // maxBits: 10 (maxNum: 1_000) var Gravity = 100; // maxBits: 7 var minDistance = 200; // maxBits: 8 @@ -40,50 +40,48 @@ template CalculateForce() { // NOTE: windowWidth appears in calculateMissile, forceAccumulator as well and needs to match var windowWidth = 1000; // maxBits: 10 - var windowWidthScaled = windowWidth * scalingFactor; // maxBits: 37 + var windowWidthScaled = windowWidth * scalingFactor; // maxBits: 20 (maxNum: 1_000_000) - - // TODO: these could be constrained, do they need to be? - var GScaled = Gravity * scalingFactor; // maxBits: 34 + var GScaled = Gravity * scalingFactor; // maxBits: 17 (maxNum: 100_000) // log("GScaled", GScaled); - signal input in_bodies[2][7]; - signal output out_forces[2][2]; // type is an array where [n][v] such that n is whether - // the vector is negative or not (0 not negative, 1 is negative) and v is the absolute - // value of the vector, with maxBit: xxx + signal input in_bodies[2][5]; + signal output out_forces[2][2]; // maxBit: 64 (maxNum: 10_400_000_000_000_000_000) + // type is an array where [n][v] such that n is whether the vector is negative or not + // (0 not negative, 1 is negative) and v is the absolute value of the vector // NOTE: this is 200**2 so we have to square the scaling factor too - signal minDistanceScaled <== (minDistance ** 2) * (scalingFactor ** 2); // maxBits: 69 + signal minDistanceScaled <== (minDistance ** 2) * (scalingFactor ** 2); // maxBits: 36 (maxNum: 40_000_000_000) // NOTE: minDistanceScaled is maximum of // log("minDistanceScaled", minDistanceScaled); - var body1_position_x = getX(in_bodies[0]); // maxBits: 37 = windowWidthScaled + var body1_position_x = getX(in_bodies[0]); // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled // log("body1_position_x", body1_position_x); - var body1_position_y = getY(in_bodies[0]); // maxBits: 37 = windowWidthScaled + var body1_position_y = getY(in_bodies[0]); // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled // log("body1_position_y", body1_position_y); // NOTE: maximum radius currently 13 - var body1_radius = getMass(in_bodies[0]); // maxBits: 31 = numBits(13 * scalingFactor) + var body1_radius = getMass(in_bodies[0]); // maxBits: 14 = numBits(13 * scalingFactor) (maxNum: 13_000) - var body2_position_x = getX(in_bodies[1]); // maxBits: 37 = windowWidthScaled + var body2_position_x = getX(in_bodies[1]); // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled // log("body2_position_x", body2_position_x); - var body2_position_y = getY(in_bodies[1]); // maxBits: 37 = windowWidthScaled + var body2_position_y = getY(in_bodies[1]); // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled // log("body2_position_y", body2_position_y); // NOTE: maximum radius currently 13 - var body2_radius = getMass(in_bodies[1]); // maxBits: 31 = numBits(13 * scalingFactor) + var body2_radius = getMass(in_bodies[1]); // maxBits: 14 = numBits(13 * scalingFactor) (maxNum: 13_000) signal dx <== body2_position_x - body1_position_x; // maxBits: 254 because it can be negative - component absoluteValueSubtraction = AbsoluteValueSubtraction(37); - absoluteValueSubtraction.in[0] <== body1_position_x; - absoluteValueSubtraction.in[1] <== body2_position_x; - signal dxAbs <== absoluteValueSubtraction.out; // maxBits: 37 + component absoluteValueSubtraction = AbsoluteValueSubtraction(20); + absoluteValueSubtraction.in[0] <== body1_position_x; // maxBits: 20 (maxNum: 1_000_000) + absoluteValueSubtraction.in[1] <== body2_position_x; // maxBits: 20 (maxNum: 1_000_000) + signal dxAbs <== absoluteValueSubtraction.out; // maxBits: 20 (maxNum: 1_000_000) signal dy <== body2_position_y - body1_position_y; // maxBits: 254 because it can be negative - component absoluteValueSubtraction2 = AbsoluteValueSubtraction(37); - absoluteValueSubtraction2.in[0] <== body1_position_y; - absoluteValueSubtraction2.in[1] <== body2_position_y; - signal dyAbs <== absoluteValueSubtraction2.out; // maxBits: 37 + component absoluteValueSubtraction2 = AbsoluteValueSubtraction(20); + absoluteValueSubtraction2.in[0] <== body1_position_y; // maxBits: 20 (maxNum: 1_000_000) + absoluteValueSubtraction2.in[1] <== body2_position_y; // maxBits: 20 (maxNum: 1_000_000) + signal dyAbs <== absoluteValueSubtraction2.out; // maxBits: 20 (maxNum: 1_000_000) // log("dx", dx); // log("dy", dy); @@ -92,134 +90,110 @@ template CalculateForce() { // log("dxAbs", dxAbs); // log("dyAbs", dyAbs); - signal dxs <== dxAbs * dxAbs; // maxBits: 74 = 37 * 2 + signal dxs <== dxAbs * dxAbs; // maxBits: 40 = 20 * 2 (maxNum: 1_000_000_000_000) // log("dxs", dxs); - signal dys <== dyAbs * dyAbs; // maxBits: 74 = 37 * 2 + signal dys <== dyAbs * dyAbs; // maxBits: 40 = 20 * 2 (maxNum: 1_000_000_000_000) // log("dys", dys); - signal unboundDistanceSquared <== dxs + dys; // maxBits: 75 = 74 + 1 + signal unboundDistanceSquared <== dxs + dys; // maxBits: 41 = 40 + 1 (maxNum: 2_000_000_000_000) // log("unboundDistanceSquared", unboundDistanceSquared); - component lessThan = LessThan(75); // NOTE: also because unboundDistanceSquared is 75 - // NOTE: max distance should be corner to corner of max grid size - // max grid is 1000_00000000 which means 1000_00000000 * sqrt(2) = 1414_21356237 - // 1414_21356237**2 is 19,999,999,999,912,458,800,169 - // 19,999,999,999,912,460,800,000 in bits is 76 - // max number using 75 bits is 2**75 - 1 = 75,557,863,725,914,323,419,135 - lessThan.in[0] <== unboundDistanceSquared; // maxBits: 75 - lessThan.in[1] <== minDistanceScaled; // maxBits: 69 + component lessThan = LessThan(41); + lessThan.in[0] <== unboundDistanceSquared; // maxBits: 41: (maxNum: 2_000_000_000_000) + lessThan.in[1] <== minDistanceScaled; // maxBits: 36 (maxNum: 40_000_000_000) - // distanceSquared <== is_below_minimum ? minDistanceScaled : unboundDistanceSquared; component myMux = Mux1(); - myMux.c[0] <== unboundDistanceSquared; // maxBits: 75 - myMux.c[1] <== minDistanceScaled; // maxBits: 69 + myMux.c[0] <== unboundDistanceSquared; // maxBits: 41 (maxNum: 2_000_000_000_000) + myMux.c[1] <== minDistanceScaled; // maxBits: 36 (maxNum: 40_000_000_000) myMux.s <== lessThan.out; - signal distanceSquared <== myMux.out; // maxBits: 75 + signal distanceSquared <== myMux.out; // maxBits: 41 (maxNum: 2_000_000_000_000) // NOTE: confirm this is correct // NOTE: squre root should require half as many bits as the input // TODO: confirm that 2 bit more is enough for the margin of error of distance * 2 - signal distance <-- approxSqrt(distanceSquared); // maxBits: 39 = 75 / 2 + 2 + signal distance <-- approxSqrt(distanceSquared); // maxBits: 21 (maxNum: 1_414_214) ~= 41 / 2 + 2 // log("distance", distance); // log("distanceSquared", distanceSquared); // bits should be maximum of the vectorLimiter which would be (10 * 10 ** 8) * (10 * 10 ** 8) which is under 60 bits - component acceptableMarginOfError = AcceptableMarginOfError(78); // TODO: test the limits of this. - acceptableMarginOfError.expected <== distance ** 2; // maxBits: 78 = 39 * 2 - acceptableMarginOfError.actual <== distanceSquared; // maxBits: 75 + component acceptableMarginOfError = AcceptableMarginOfError(41); + acceptableMarginOfError.expected <== distance ** 2; // maxBits: 41 (maxNum: 2_000_001_237_796) ~= 21 * 2 + acceptableMarginOfError.actual <== distanceSquared; // maxBits: 41 // margin of error should be midpoint between squares - acceptableMarginOfError.marginOfError <== distance * 2; // TODO: confrim if (distance * 2) +1 is needed + acceptableMarginOfError.marginOfError <== distance * 2; // maxBits: 22 (maxNum: 2_828_428) acceptableMarginOfError.out === 1; // NOTE: this could be tweaked as a variable for "liveliness" of bodies - signal bodies_sum_tmp <== (body1_radius + body2_radius) * 4; // maxBits: 34 = 31 + 1 + 2 + signal bodies_sum_tmp <== (body1_radius + body2_radius) * 4; // maxBits: 17 (maxNum: 104_000) // bodies_sum is 0 if either body1_radius or body2_radius is 0 component isZero = IsZero(); - isZero.in <== body1_radius; + isZero.in <== body1_radius; // maxBits: 14 component myMux2 = Mux1(); - myMux2.c[0] <== bodies_sum_tmp; // maxBits: 34 + myMux2.c[0] <== bodies_sum_tmp; // maxBits: 17 (maxNum: 104_000) myMux2.c[1] <== 0; // maxBits: 0 myMux2.s <== isZero.out; component isZero2 = IsZero(); - isZero2.in <== body2_radius; // maxBits: 31 + isZero2.in <== body2_radius; // maxBits: 14 component myMux3 = Mux1(); - myMux3.c[0] <== myMux2.out; // maxBits: 34 + myMux3.c[0] <== myMux2.out; // maxBits: 17 (maxNum: 104_000) myMux3.c[1] <== 0; // maxBits: 0 myMux3.s <== isZero2.out; - signal bodies_sum <== myMux3.out; // maxBits: 34 + signal bodies_sum <== myMux3.out; // maxBits: 17 (maxNum: 104_000) // log("bodies_sum", bodies_sum); // NOTE: this is a result of moving division to end of calculation to preserve precision - signal distanceSquared_with_avg_denom <== distanceSquared * 2; // maxBits: 76 = 75 + 1 + signal distanceSquared_with_avg_denom <== distanceSquared * 2; // maxBits: 42 (maxNum: 4_000_000_000_000) // log("distanceSquared_with_avg_denom", distanceSquared_with_avg_denom); // NOTE: distance should be divided by scaling factor, but we can multiply GScaled by scaling factor instead to prevent division rounding errors - signal forceMag_numerator <== GScaled * bodies_sum * scalingFactor; // maxBits: 95 = 34 + 34 + 27 + signal forceMag_numerator <== GScaled * bodies_sum * scalingFactor; // maxBits: 44 (maxNum: 10_400_000_000_000) // log("forceMag_numerator", forceMag_numerator); - signal forceDenom <== distanceSquared_with_avg_denom * distance; // maxBits: 115 = 76 + 39 + signal forceDenom <== distanceSquared_with_avg_denom * distance; // maxBits: 63 (maxNum: 5_656_856_000_000_000_000) // log("forceDenom", forceDenom); - signal forceXnum <== dxAbs * forceMag_numerator; // maxBits: 132 = 37 + 95 + signal forceXnum <== dxAbs * forceMag_numerator; // maxBits: 64 (maxNum: 10_400_000_000_000_000_000) // log("forceXnum", forceXnum); - signal forceXunsigned <-- approxDiv(forceXnum, forceDenom); // maxBits: 132 = forceXnum + signal forceXunsigned <-- approxDiv(forceXnum, forceDenom); // maxBits: 64 (maxNum: 10_400_000_000_000_000_000) // log("forceXunsigned", forceXunsigned); // NOTE: the following constraints the approxDiv to ensure it's within the acceptable error of margin - signal approxNumerator1 <== forceXunsigned * forceDenom; // maxBits: 247 = 132 + 115 - component acceptableErrorOfMarginDiv1 = AcceptableMarginOfError(247); - acceptableErrorOfMarginDiv1.expected <== forceXnum; // maxBits: 132 - acceptableErrorOfMarginDiv1.actual <== approxNumerator1; // maxBits: 247 - acceptableErrorOfMarginDiv1.marginOfError <== forceDenom; // TODO: actually could be further reduced to (realDenom / 2) + 1 but then we're using division again - acceptableErrorOfMarginDiv1.out === 1; + signal approxNumerator1 <== forceXunsigned * forceDenom; // maxBits: 126 (maxNum: 58_831_302_400_000_000_000_000_000_000_000_000_000) + component acceptableMarginOfErrorDiv1 = AcceptableMarginOfError(126); + acceptableMarginOfErrorDiv1.expected <== forceXnum; // maxBits: 64 + acceptableMarginOfErrorDiv1.actual <== approxNumerator1; // maxBits: 126 + acceptableMarginOfErrorDiv1.marginOfError <== forceDenom; // TODO: actually could be further reduced to (realDenom / 2) + 1 but then we're using division again + acceptableMarginOfErrorDiv1.out === 1; // if dxAbs + dx is 0, then forceX should be negative component isZero3 = IsZero(); // NOTE: isZero handles overflow bit values correctly - isZero3.in <== dxAbs + dx; // maxBits: 255 = max(37, 254) + 1 + isZero3.in <== dxAbs + dx; // maxBits: maxBits: 21 (maxNum: 2_000_000) // log("isZero3", dxAbs + dx, isZero3.out); - // component myMux4 = Mux1(); - // myMux4.c[0] <== forceXunsigned; // maxBits: 132 - // myMux4.c[1] <== forceXunsigned * -1; // maxBits: 254 - // myMux4.s <== isZero3.out; - // signal forceX <== myMux4.out; // maxBits: 254 - // log("forceX", forceX); out_forces[0][0] <== isZero3.out; // isZero is 1 when dx is negative - out_forces[0][1] <== forceXunsigned; // maxBits 132 + out_forces[0][1] <== forceXunsigned; // maxBits 64 (maxNum: 10_400_000_000_000_000_000) - signal forceYnum <== dyAbs * forceMag_numerator; // maxBits: 132 = 37 + 95 + signal forceYnum <== dyAbs * forceMag_numerator; // maxBits:64 (maxNum: 10_400_000_000_000_000_000) // log("forceYnum", forceYnum); - signal forceYunsigned <-- approxDiv(forceYnum, forceDenom); // maxBits: 132 = forceYnum + signal forceYunsigned <-- approxDiv(forceYnum, forceDenom); // maxBits: 64 (maxNum: 10_400_000_000_000_000_000) // log("forceYunsigned", forceYunsigned); // NOTE: the following constraints the approxDiv to ensure it's within the acceptable error of margin - signal approxNumerator2 <== forceYunsigned * forceDenom; // maxBits: 247 = 132 + 115 - component acceptableErrorOfMarginDiv2 = AcceptableMarginOfError(247); - acceptableErrorOfMarginDiv2.expected <== forceYnum; // maxBits: 132 - acceptableErrorOfMarginDiv2.actual <== approxNumerator2; // maxBits: 247 - acceptableErrorOfMarginDiv2.marginOfError <== forceDenom; // TODO: actually could be further reduced to (realDenom / 2) + 1 but then we're using division again - acceptableErrorOfMarginDiv2.out === 1; + signal approxNumerator2 <== forceYunsigned * forceDenom; // maxBits: 126 (maxNum: 58_831_302_400_000_000_000_000_000_000_000_000_000) + component acceptableMarginOfErrorDiv2 = AcceptableMarginOfError(126); + acceptableMarginOfErrorDiv2.expected <== forceYnum; // maxBits: 64 + acceptableMarginOfErrorDiv2.actual <== approxNumerator2; // maxBits: 126 + acceptableMarginOfErrorDiv2.marginOfError <== forceDenom; // TODO: actually could be further reduced to (realDenom / 2) + 1 but then we're using division again + acceptableMarginOfErrorDiv2.out === 1; // if dyAbs + dy is 0, then forceY should be negative component isZero4 = IsZero(); // NOTE: isZero handles overflow bit values correctly isZero4.in <== dyAbs + dy; // maxBits: 255 = max(37, 254) + 1 - // component myMux5 = Mux1(); - // myMux5.c[0] <== forceYunsigned; // maxBits: 132 - // myMux5.c[1] <== forceYunsigned * -1; // maxBits: 254 - // myMux5.s <== isZero4.out; - // signal forceY <== myMux5.out; // maxBits: 254 + // log("forceY", forceY); out_forces[1][0] <== isZero4.out; - out_forces[1][1] <== forceYunsigned; // maxBits 132 - - // out_forces[0] <== forceX; // maxBits: 254 - // out_forces[1] <== forceY; // maxBits: 254 -} - - -/* INPUT = { - "in_bodies": [ ["82600000000", "4200000000", "-133000000", "-629000000", "10000000000"], ["36300000000", "65800000000", "-332000000", "374000000", "7500000000"] ] -} */ \ No newline at end of file + out_forces[1][1] <== forceYunsigned; // maxBits 64 (maxNum: 10_400_000_000_000_000_000) +} \ No newline at end of file diff --git a/circuits/detectCollision.circom b/circuits/detectCollision.circom index 609a071d..9c6ca934 100644 --- a/circuits/detectCollision.circom +++ b/circuits/detectCollision.circom @@ -5,18 +5,10 @@ include "../node_modules/circomlib/circuits/mux1.circom"; template DetectCollision(totalBodies) { signal input bodies[totalBodies][5]; - // log("bodies[0][0]", bodies[0][0]); - // log("bodies[0][1]", bodies[0][1]); - // log("-133000000 ", -133000000); - // log("-1 (p-1) ", -1); - // log("bodies[0][2]", bodies[0][2]); - // log("bodies[0][3]", bodies[0][3]); - // log("bodies[0][4]", bodies[0][4]); signal input missile[5]; signal output out_bodies[totalBodies][5]; signal output out_missile[5]; - signal tmp_missiles[totalBodies + 1][3]; // only storing x, y and radius as 0, 1, 2 tmp_missiles[0][0] <== missile[0]; tmp_missiles[0][1] <== missile[1]; @@ -32,11 +24,11 @@ template DetectCollision(totalBodies) { // loop through all bodies and get distance between missile and body for (var i = 0; i < totalBodies; i++) { - getDistance[i] = GetDistance(60); // TODO: check bit limit size - getDistance[i].x1 <== bodies[i][0]; - getDistance[i].y1 <== bodies[i][1]; - getDistance[i].x2 <== tmp_missiles[i][0]; - getDistance[i].y2 <== tmp_missiles[i][1]; + getDistance[i] = GetDistance(20); // n = 20 but inside GetDistance n = 2 * n + 1 and returns maxBits 21 + getDistance[i].x1 <== bodies[i][0]; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + getDistance[i].y1 <== bodies[i][1]; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + getDistance[i].x2 <== tmp_missiles[i][0]; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + getDistance[i].y2 <== tmp_missiles[i][1]; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled // check whether the radius of the missile is 0, this means there is currently no missile isZero[i] = IsZero(); @@ -44,16 +36,16 @@ template DetectCollision(totalBodies) { // if there is no missile (isZeroOut == 1), then set distanceMin to 0. Even if they are exact same coordinates the distance will be 0 and 0 < 0 is false distanceMinMux[i] = Mux1(); - distanceMinMux[i].c[0] <== bodies[i][4] * 2; + distanceMinMux[i].c[0] <== bodies[i][4] * 2; // maxBits: 15 = numBits(2 * 13 * scalingFactor) (maxNum: 26_000) distanceMinMux[i].c[1] <== 0; distanceMinMux[i].s <== isZero[i].out; - lessThan[i] = LessThan(252); // TODO: check bit limit size - lessThan[i].in[0] <== getDistance[i].distance; - lessThan[i].in[1] <== distanceMinMux[i].out; + lessThan[i] = LessThan(21); + lessThan[i].in[0] <== getDistance[i].distance; // maxBits: 21 (maxNum: 1_414_214) = approxSqrt(distanceSquared) = approxSqrt(2_000_000_000_000) + lessThan[i].in[1] <== distanceMinMux[i].out; // maxBits: 15 (maxNum: 26_000) mux[i] = Mux1(); - mux[i].c[0] <== bodies[i][4]; + mux[i].c[0] <== bodies[i][4]; // maxBits: 14 = numBits(13 * scalingFactor) (maxNum: 13_000) mux[i].c[1] <== 0; mux[i].s <== lessThan[i].out; out_bodies[i][0] <== bodies[i][0]; diff --git a/circuits/forceAccumulator.circom b/circuits/forceAccumulator.circom index 3303c67c..03f4bf55 100644 --- a/circuits/forceAccumulator.circom +++ b/circuits/forceAccumulator.circom @@ -21,65 +21,73 @@ include "helpers.circom"; // maybe can streamline the square root and division template ForceAccumulator(totalBodies) { // max 10 = maxBits: 4 - signal input bodies[totalBodies][7]; - signal output out_bodies[totalBodies][7]; - // [0] = position_x | maxBits: 37 = windowWidthScaled - // [1] = position_y | maxBits: 37 = windowWidthScaled - // [[2],[3]] = vector_x | maxBits: 133= 2 * maxVectorScaled = 1 + 132 - // [[4],[5]] = vector_y | maxBits: 133 = 2 * maxVectorScaled = 1 + 132 - // [6] = radius | maxBits: 31 = numBits(13 * scalingFactor) + signal input bodies[totalBodies][5]; + signal output out_bodies[totalBodies][5]; + // [0] = position_x | maxBits: 20 = windowWidthScaled (maxNum: 1_000_000) + // [1] = position_y | maxBits: 20 = windowWidthScaled (maxNum: 1_000_000) + // [2] = vector_x | maxBits: 15 (maxNum: 20_000) = 2 * maxVector (maxVector offset by +maxVector so num is never negative) + // [3] = vector_y | maxBits: 15 (maxNum: 20_000) = 2 * maxVector (maxVector offset by +maxVector so num is never negative) + // [4] = radius | maxBits: 14 = numBits(13 * scalingFactor) (maxNum: 13_000) // NOTE: scalingFactorFactor appears in calculateMissile, calculateForce as well - var scalingFactorFactor = 8; // maxBits: 4 - var scalingFactor = 10**scalingFactorFactor; // maxBits: 27 + var scalingFactorFactor = 3; // maxBits: 2 + var scalingFactor = 10**scalingFactorFactor; // maxBits: 10 (maxNum: 1_000) var maxVector = 10; // maxBits: 4 - var maxVectorScaled = 10 * scalingFactor; // maxBits: 31 + var maxVectorScaled = 10 * scalingFactor; // maxBits: 14 (maxNum: 10_000) // NOTE: windowWidth appears in calculateMissile, calculateForce, forceAccumulator as well and needs to match var windowWidth = 1000; // maxBits: 10 - var windowWidthScaled = windowWidth * scalingFactor; // maxBits: 37 + var windowWidthScaled = windowWidth * scalingFactor; // maxBits: 20 (maxNum: 1_000_000) - - var totalIterations = totalBodies * (totalBodies - 1) / 2; // maxBits: 7 + var accumulated_body_forces[totalBodies][2]; + var totalIterations = totalBodies * (totalBodies - 1) / 2; // maxBits: 6 (maxNum: 45) component calculateForceComponent[totalIterations]; - signal force_x[totalIterations][2]; // maxBits: 132 - signal force_y[totalIterations][2]; // maxBits: 132 - signal accumulated_body_forces[totalIterations + 1][totalBodies][2]; + signal force_x[totalIterations][2]; // maxBits: 64 (maxNum: 10_400_000_000_000_000_000) + signal force_y[totalIterations][2]; // maxBits: 64 (maxNum: 10_400_000_000_000_000_000) component mux[totalIterations * 2]; - var ii = 0; + // NOTE: Below we're setting initial values for accumulate_body_forces to be the + // maximum accumulated value possible (maximum value for force multiplied by + // totalIterations). This is an offset to avoid going into negative numbers so that + // comparators later on will not need to cover the full range of the prime field. + // Maximum accumulated value must be removed before final value is returned. + var maximum_accumulated_possible = 468000000000000000000; // maxBits: 69 (maxNum: 468_000_000_000_000_000_000) = out_forces * totalIterations + for (var i = 0; i < totalBodies; i++) { + accumulated_body_forces[i][0] = maximum_accumulated_possible; // maxBits: 69 (maxNum: 468_000_000_000_000_000_000) = out_forces * totalIterations + accumulated_body_forces[i][1] = maximum_accumulated_possible; // maxBits: 69 (maxNum: 468_000_000_000_000_000_000) = out_forces * totalIterations + } for (var i = 0; i < totalBodies; i++) { // radius of body doesn't change - out_bodies[i][6] <== getMass(bodies[i]); + out_bodies[i][4] <== bodies[i][4]; // maxBits: 14 (maxNum: 13_000) for (var j = i+1; j < totalBodies; j++) { - // var ii = i + j - 1; // calculate the force between i and j calculateForceComponent[ii] = CalculateForce(); calculateForceComponent[ii].in_bodies[0] <== bodies[i]; calculateForceComponent[ii].in_bodies[1] <== bodies[j]; - force_x[ii] <== calculateForceComponent[ii].out_forces[0]; // maxBits: 132 - force_y[ii] <== calculateForceComponent[ii].out_forces[1]; // maxBits: 132 + force_x[ii] <== calculateForceComponent[ii].out_forces[0]; // maxBits: 64 (maxNum: 10_400_000_000_000_000_000) + force_y[ii] <== calculateForceComponent[ii].out_forces[1]; // maxBits: 64 (maxNum: 10_400_000_000_000_000_000) // accumulate the value of the force on body i and body j - // log("j", j, "force_x[ii]", force_x[ii]); + // accumulate the x forces mux[ii] = MultiMux1(2); - mux[ii].c[0][0] <== accumulated_body_forces[ii][i][0] + force_x[ii][1]; - mux[ii].c[0][1] <== accumulated_body_forces[ii][i][0] - force_x[ii][1]; - mux[ii].c[1][0] <== accumulated_body_forces[ii][j][0] - force_x[ii][1]; - mux[ii].c[1][1] <== accumulated_body_forces[ii][j][0] + force_x[ii][1]; + mux[ii].c[0][0] <== accumulated_body_forces[i][0] + force_x[ii][1]; // maxBits: 70 (maxNum: 936_000_000_000_000_000_000) = 2 * maximum_accumulated_possible + mux[ii].c[0][1] <== accumulated_body_forces[i][0] - force_x[ii][1]; // maxBits: 69 (maxNum: 468_000_000_000_000_000_000) + mux[ii].c[1][0] <== accumulated_body_forces[j][0] - force_x[ii][1]; // maxBits: 69 (maxNum: 468_000_000_000_000_000_000) + mux[ii].c[1][1] <== accumulated_body_forces[j][0] + force_x[ii][1]; // maxBits: 70 (maxNum: 936_000_000_000_000_000_000) = 2 * maximum_accumulated_possible mux[ii].s <== force_x[ii][0]; - accumulated_body_forces[ii + 1][i][0] <== mux[ii].out[0]; - accumulated_body_forces[ii + 1][j][0] <== mux[ii].out[1]; + accumulated_body_forces[i][0] = mux[ii].out[0]; // maxBits: 70 (maxNum: 936_000_000_000_000_000_000) + accumulated_body_forces[j][0] = mux[ii].out[1]; // maxBits: 70 (maxNum: 936_000_000_000_000_000_000) + // accumulate the y forces mux[totalIterations + ii] = MultiMux1(2); - mux[ii].c[0][0] <== accumulated_body_forces[ii][i][1] + force_y[ii][1]; - mux[ii].c[0][1] <== accumulated_body_forces[ii][i][1] - force_y[ii][1]; - mux[ii].c[1][0] <== accumulated_body_forces[ii][j][1] - force_y[ii][1]; - mux[ii].c[1][1] <== accumulated_body_forces[ii][j][1] + force_y[ii][1]; - mux[ii].s <== force_y[ii][0]; - accumulated_body_forces[ii + 1][i][1] <== mux[ii].out[0]; - accumulated_body_forces[ii + 1][j][1] <== mux[ii].out[1]; + mux[totalIterations + ii].c[0][0] <== accumulated_body_forces[i][1] + force_y[ii][1]; // maxBits: 70 (maxNum: 936_000_000_000_000_000_000) = 2 * maximum_accumulated_possible + mux[totalIterations + ii].c[0][1] <== accumulated_body_forces[i][1] - force_y[ii][1]; // maxBits: 69 (maxNum: 468_000_000_000_000_000_000) + mux[totalIterations + ii].c[1][0] <== accumulated_body_forces[j][1] - force_y[ii][1]; // maxBits: 69 (maxNum: 468_000_000_000_000_000_000) + mux[totalIterations + ii].c[1][1] <== accumulated_body_forces[j][1] + force_y[ii][1]; // maxBits: 70 (maxNum: 936_000_000_000_000_000_000) = 2 * maximum_accumulated_possible + mux[totalIterations + ii].s <== force_y[ii][0]; + accumulated_body_forces[i][1] = mux[totalIterations + ii].out[0]; // maxBits: 70 (maxNum: 936_000_000_000_000_000_000) + accumulated_body_forces[j][1] = mux[totalIterations + ii].out[1]; // maxBits: 70 (maxNum: 936_000_000_000_000_000_000) ii = ii + 1; } @@ -96,47 +104,78 @@ template ForceAccumulator(totalBodies) { // max 10 = maxBits: 4 for (var i = 0; i < totalBodies; i++) { // calculate the new vector for body i - new_vector_x[i] <== bodies[i][2] + accumulated_body_forces[i][0]; - new_vector_y[i] <== bodies[i][3] + accumulated_body_forces[i][1]; - // log(i, "accumulated_body_forces[i][0]", accumulated_body_forces[i][0]); - // log(i, "new_vector_x[i][2]", new_vector_x[i]); + /* + NOTE: + new_vector is a combination of the current vector which is offset by maxVectorScaled + and the accumulated_body_forces which is offset by maximum_accumulated_possible + */ + new_vector_x[i] <== bodies[i][2] + accumulated_body_forces[i][0]; // maxBits: 70 (maxNum: 936_000_000_000_000_020_000) = (2 * maximum_accumulated_possible) + (2 * maxVector) + new_vector_y[i] <== bodies[i][3] + accumulated_body_forces[i][1]; // maxBits: 70 (maxNum: 936_000_000_000_000_020_000) = (2 * maximum_accumulated_possible) + (2 * maxVector) // limit the magnitude of the vector - vectorLimiterX[i] = Limiter(252); // TODO: confirm bits limit - vectorLimiterX[i].in <== new_vector_x[i]; - vectorLimiterX[i].limit <== maxVectorScaled; // speedLimit - vectorLimiterX[i].rather <== maxVectorScaled; - out_bodies[i][2] <== vectorLimiterX[i].out; - vectorLimiterY[i] = Limiter(252); // TODO: confirm bits limit - vectorLimiterY[i].in <== new_vector_y[i]; - vectorLimiterY[i].limit <== maxVectorScaled; // speedLimit - vectorLimiterY[i].rather <== maxVectorScaled; - out_bodies[i][3] <== vectorLimiterY[i].out; + /* + NOTE: vectorLimitX needs to be limited by maxVectorScaled. However because new_vector_x + is already offset by maxVectorScaled and maximum_accumulated_possible, we need to add + both to the limit and remove maximum_accumulated_possible from the result. The final + result will still contain the maxVectorScaled offset that will prevent the vector from + becoming negative. + */ + vectorLimiterX[i] = Limiter(69); + vectorLimiterX[i].in <== new_vector_x[i]; // maxBits: 70 (maxNum: 936_000_000_000_000_020_000) + vectorLimiterX[i].limit <== maxVectorScaled + maxVectorScaled + maximum_accumulated_possible; // maxBits: 69 (maxNum: 468_000_000_000_000_020_000) + vectorLimiterX[i].rather <== maxVectorScaled + maxVectorScaled + maximum_accumulated_possible; // maxBits: 69 (maxNum: 468_000_000_000_000_020_000) + + out_bodies[i][2] <== vectorLimiterX[i].out - maximum_accumulated_possible; // maxBits: 15 (maxNum: 20_000) + + // NOTE: same as above + vectorLimiterY[i] = Limiter(69); + vectorLimiterY[i].in <== new_vector_y[i]; // maxBits: 70 (maxNum: 936_000_000_000_000_020_000) + vectorLimiterY[i].limit <== maxVectorScaled + maxVectorScaled + maximum_accumulated_possible; // maxBits: 69 (maxNum: 468_000_000_000_000_020_000) + vectorLimiterY[i].rather <== maxVectorScaled + maxVectorScaled + maximum_accumulated_possible; // maxBits: 69 (maxNum: 468_000_000_000_000_020_000) + out_bodies[i][3] <== vectorLimiterY[i].out - maximum_accumulated_possible; // maxBits: 15 (maxNum: 20_000) + // need to limit position so plane loops off edges - positionLimiterX[i] = Limiter(37); // NOTE: position is limited to maxWidth + (2*maxVectorScaled) which should be under 37 bits - // positionLimiter.x <== bodies[0][0] + vectorLimiter.limitedX; - positionLimiterX[i].in <== bodies[i][0] + vectorLimiterX[i].out + maxVectorScaled; // NOTE: adding maxVectorScaled ensures it is never negative - positionLimiterX[i].limit <== windowWidthScaled + maxVectorScaled; // windowWidthScaled - positionLimiterX[i].rather <== maxVectorScaled; - // NOTE: maxVectorScaled is still included, needs to be removed at end of calculation - positionLowerLimiterX[i] = LowerLimiter(37); // NOTE: position is limited to maxWidth + (2*maxVectorScaled) which should be under 37 bits - positionLowerLimiterX[i].in <== positionLimiterX[i].out; - positionLowerLimiterX[i].limit <== maxVectorScaled; - positionLowerLimiterX[i].rather <== windowWidthScaled + maxVectorScaled; + /* + NOTE: vectors are already offset with maxVectorScaled so that they are never negative. + When calculating the change in position, we need to subtract maxVectorScaled to ensure + that negative values are handled properly. However, we also want to prevent the position + from becoming a negative value and requiring 254 bits to represent. To do this, we add + maxVectorScaled to the position before limiting it. That is why we have the otherwise + nonsensical calculation below where we add then remove maxVectorScaled. + + +bodies[i][0] is the actual position of the body (maxNum: 1_000_000) + +out_bodies[i][2] is the x vector of the body with an additional maxVectorScaled offset (maxNum: 20_000) + -maxVectorScaled has to be removed to account for the vector offset (maxNum: 10_000) + +maxVectorScaled is added to ensure that the position is never negative (maxNum: 10_000) + + maxVectorScaled will need to be removed from the final position value + */ + positionLimiterX[i] = Limiter(20); + positionLimiterX[i].in <== bodies[i][0] + out_bodies[i][2] - maxVectorScaled + maxVectorScaled; // maxBits: 20 (maxNum: 1_020_000) + positionLimiterX[i].limit <== windowWidthScaled + maxVectorScaled; // maxBits: 20 (maxNum: 1_010_000) + positionLimiterX[i].rather <== maxVectorScaled; // maxBits: 14 (maxNum: 10_000) + + // NOTE: maxVectorScaled is still included, needs to be removed at end of lowerLimiter + positionLowerLimiterX[i] = LowerLimiter(20); + positionLowerLimiterX[i].in <== positionLimiterX[i].out; // maxBits: 20 (maxNum: 1_020_000) + positionLowerLimiterX[i].limit <== maxVectorScaled; // maxBits: 14 (maxNum: 10_000) + positionLowerLimiterX[i].rather <== windowWidthScaled + maxVectorScaled; // maxBits: 20 (maxNum: 1_010_000) out_bodies[i][0] <== positionLowerLimiterX[i].out - maxVectorScaled; - positionLimiterY[i] = Limiter(37); // NOTE: position is limited to maxWidth + (2*maxVectorScaled) which should be under 37 bits - positionLimiterY[i].in <== bodies[i][1] + vectorLimiterY[i].out + maxVectorScaled; // NOTE: adding maxVectorScaled ensures it is never negative - positionLimiterY[i].limit <== windowWidthScaled + maxVectorScaled; // windowWidthScaled - positionLimiterY[i].rather <== maxVectorScaled; + + // NOTE: same as above + positionLimiterY[i] = Limiter(20); + positionLimiterY[i].in <== bodies[i][1] + out_bodies[i][3] - maxVectorScaled + maxVectorScaled; // maxBits: 20 (maxNum: 1_020_000) + positionLimiterY[i].limit <== windowWidthScaled + maxVectorScaled; // maxBits: 20 (maxNum: 1_010_000) + positionLimiterY[i].rather <== maxVectorScaled; // maxBits: 14 (maxNum: 10_000) + // NOTE: maxVectorScaled is still included, needs to be removed at end of calculation - positionLowerLimiterY[i] = LowerLimiter(37); // NOTE: position is limited to maxWidth + (2*maxVectorScaled) which should be under 37 bits - positionLowerLimiterY[i].in <== positionLimiterY[i].out; - positionLowerLimiterY[i].limit <== maxVectorScaled; - positionLowerLimiterY[i].rather <== windowWidthScaled + maxVectorScaled; + positionLowerLimiterY[i] = LowerLimiter(20); + positionLowerLimiterY[i].in <== positionLimiterY[i].out; // maxBits: 20 (maxNum: 1_020_000) + positionLowerLimiterY[i].limit <== maxVectorScaled; // maxBits: 14 (maxNum: 10_000) + positionLowerLimiterY[i].rather <== windowWidthScaled + maxVectorScaled; // maxBits: 20 (maxNum: 1_010_000) out_bodies[i][1] <== positionLowerLimiterY[i].out - maxVectorScaled; - // log(i, "out_bodies[i][2]", out_bodies[i][2]); } // log("out_bodies[0][0]", out_bodies[0][0]); // log("out_bodies[0][1]", out_bodies[0][1]); diff --git a/circuits/getDistance.circom b/circuits/getDistance.circom index 4c260f0c..b508c990 100644 --- a/circuits/getDistance.circom +++ b/circuits/getDistance.circom @@ -3,35 +3,34 @@ pragma circom 2.1.6; include "approxMath.circom"; template GetDistance(n) { - signal input x1; - signal input y1; - signal input x2; - signal input y2; + signal input x1; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + signal input y1; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + signal input x2; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + signal input y2; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled signal output distance; // signal dx <== x2 - x1; component absoluteValueSubtraction = AbsoluteValueSubtraction(n); - absoluteValueSubtraction.in[0] <== x1; - absoluteValueSubtraction.in[1] <== x2; - signal dxAbs <== absoluteValueSubtraction.out; + absoluteValueSubtraction.in[0] <== x1; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + absoluteValueSubtraction.in[1] <== x2; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + signal dxAbs <== absoluteValueSubtraction.out; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled // signal dy <== y2 - y1; component absoluteValueSubtraction2 = AbsoluteValueSubtraction(n); - absoluteValueSubtraction2.in[0] <== y1; - absoluteValueSubtraction2.in[1] <== y2; - signal dyAbs <== absoluteValueSubtraction2.out; + absoluteValueSubtraction2.in[0] <== y1; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + absoluteValueSubtraction2.in[1] <== y2; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled + signal dyAbs <== absoluteValueSubtraction2.out; // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled - signal dxs <== dxAbs * dxAbs; - signal dys <== dyAbs * dyAbs; - signal distanceSquared <== dxs + dys; + signal dxs <== dxAbs * dxAbs; // maxBits: 40 = 20 * 2 (maxNum: 1_000_000_000_000) + signal dys <== dyAbs * dyAbs; // maxBits: 40 = 20 * 2 (maxNum: 1_000_000_000_000) + signal distanceSquared <== dxs + dys; // maxBits: 41 = 40 + 1 (maxNum: 2_000_000_000_000) // NOTE: confirm this is correct - distance <-- approxSqrt(distanceSquared); - // bits should be maximum of the vectorLimiter which would be (10 * 10 ** 8) * (10 * 10 ** 8) which is under 60 bits - component acceptableMarginOfError = AcceptableMarginOfError(n); - acceptableMarginOfError.expected <== distanceSquared; - acceptableMarginOfError.actual <== distance ** 2; + distance <-- approxSqrt(distanceSquared); // maxBits: 21 (maxNum: 1_414_214) ~= 41 / 2 + 2 + component acceptableMarginOfError = AcceptableMarginOfError((2 * n) + 1); + acceptableMarginOfError.expected <== distance ** 2; // maxBits: 41 (maxNum: 2_000_001_237_796) ~= 21 * 2 + acceptableMarginOfError.actual <== distanceSquared; // maxBits: 41 // margin of error should be midpoint between squares - acceptableMarginOfError.marginOfError <== distance * 2; // TODO: confrim if (distance * 2) +1 is needed + acceptableMarginOfError.marginOfError <== distance * 2; // maxBits: 22 (maxNum: 2_828_428) acceptableMarginOfError.out === 1; } \ No newline at end of file diff --git a/circuits/getDistanceMain.circom b/circuits/getDistanceMain.circom index 5fed926d..48e4275e 100644 --- a/circuits/getDistanceMain.circom +++ b/circuits/getDistanceMain.circom @@ -2,4 +2,4 @@ pragma circom 2.1.3; include "getDistance.circom"; -component main { public [x1, y1, x2, y2]} = GetDistance(252); \ No newline at end of file +component main { public [x1, y1, x2, y2]} = GetDistance(20); \ No newline at end of file diff --git a/circuits/helpers.circom b/circuits/helpers.circom index 509cb441..c0f978ab 100644 --- a/circuits/helpers.circom +++ b/circuits/helpers.circom @@ -7,11 +7,11 @@ function getY(body) { return body[1]; } function getVx(body) { - return [body[2], body[3]]; + return body[2]; } function getVy(body) { - return [body[4], body[5]]; + return body[3]; } function getMass(body) { - return body[6]; + return body[4]; } \ No newline at end of file diff --git a/circuits/nft.json b/circuits/nft.json index e487eeae..9a2f2722 100644 --- a/circuits/nft.json +++ b/circuits/nft.json @@ -1,7 +1,7 @@ { "bodies": [ - ["22600000000", "4200000000", "-133000000", "-629000000", "10000000000"], - ["36300000000", "65800000000", "-332000000", "374000000", "7500000000"], - ["67900000000", "50000000000", "229000000", "252000000", "5000000000"] + ["226000", "42000", "8670", "3710", "100000"], + ["363000", "658000", "6680", "13740", "75000"], + ["679000", "500000", "12290", "12520", "50000"] ] } \ No newline at end of file diff --git a/circuits/stepStateMain.json b/circuits/stepStateMain.json index 30fa512c..70fad3de 100644 --- a/circuits/stepStateMain.json +++ b/circuits/stepStateMain.json @@ -1,8 +1,8 @@ { "bodies": [ - ["22600000000", "4200000000", "-133000000", "-629000000", "10000000000"], - ["36300000000", "65800000000", "-332000000", "374000000", "7500000000"], - ["67900000000", "50000000000", "229000000", "252000000", "5000000000"] + ["22600000000", "4200000000", "1", "133000000", "1", "629000000", "10000000000"], + ["36300000000", "65800000000", "1", "332000000", "0", "374000000", "7500000000"], + ["67900000000", "50000000000", "0", "229000000", "0", "252000000", "5000000000"] ], "missile": [ ["0", "0", "0", "0", "0"], diff --git a/docs/index.js b/docs/index.js index 53bd324e..b44e841a 100644 --- a/docs/index.js +++ b/docs/index.js @@ -12,7 +12,7 @@ const rightEdge = windowWidth, topEdge = 0, leftEdge = 0, bottomEdge = windowWid const boundaryRadius = windowWidth / 2 let n = 0, img1 const fps = 300 -const preRun = 0 +const preRun = 10000 const prime = 21888242871839275222246405745257275088548364400416034343698204186575808495617n; const admin = false const minRadius = 50 @@ -300,7 +300,7 @@ function explosion(x, y, radius) { return bombs } -const scalingFactor = 10n ** 8n +const scalingFactor = 10n ** 3n function calculateForce(body1, body2) { const bodies = convertBodiesToBigInts([body1, body1]) @@ -734,40 +734,43 @@ function randomPosition() { } function convertScaledStringArrayToFloat(body) { + const maxVectorScaled = convertFloatToScaledBigInt(vectorLimit) return { position: { x: convertScaledBigIntToFloat(body[0]), y: convertScaledBigIntToFloat(body[1]) }, velocity: { - x: convertScaledBigIntToFloat(body[2]), - y: convertScaledBigIntToFloat(body[3]) + x: convertScaledBigIntToFloat(body[2]) - maxVectorScaled, + y: convertScaledBigIntToFloat(body[3]) - maxVectorScaled }, radius: convertScaledBigIntToFloat(body[4]) } } function convertScaledStringArrayToBody(body) { + const maxVectorScaled = convertFloatToScaledBigInt(vectorLimit) return { position: { x: BigInt(body[0]), y: BigInt(body[1]) }, velocity: { - x: BigInt(body[2]), - y: BigInt(body[3]) + x: BigInt(body[2]) - maxVectorScaled, + y: BigInt(body[3]) - maxVectorScaled }, radius: BigInt(body[4]) } } function convertScaledBigIntBodyToArray(b) { + const maxVectorScaled = convertFloatToScaledBigInt(vectorLimit) const bodyArray = [] bodyArray.push( convertBigIntToModP(b.position.x), convertBigIntToModP(b.position.y), - convertBigIntToModP(b.velocity.x), - convertBigIntToModP(b.velocity.y), + convertBigIntToModP(b.velocity.x + maxVectorScaled), + convertBigIntToModP(b.velocity.y + maxVectorScaled), convertBigIntToModP(b.radius) ) return bodyArray.map(b => b.toString()) @@ -784,19 +787,14 @@ function convertBigIntToModP(v) { function convertBodiesToBigInts(bodies) { const bigBodies = [] + const maxVectorScaled = convertFloatToScaledBigInt(vectorLimit) for (let i = 0; i < bodies.length; i++) { const body = bodies[i] const newBody = { position: {}, velocity: {}, radius: null } newBody.position.x = convertFloatToScaledBigInt(body.position.x) newBody.position.y = convertFloatToScaledBigInt(body.position.y) - newBody.velocity.x = convertFloatToScaledBigInt(body.velocity.x) - // while (newBody.velocity.x < 0n) { - // newBody.velocity.x += p - // } - newBody.velocity.y = convertFloatToScaledBigInt(body.velocity.y) - // while (newBody.velocity.y < 0n) { - // newBody.velocity.y += p - // } + newBody.velocity.x = convertFloatToScaledBigInt(body.velocity.x)// + maxVectorScaled + newBody.velocity.y = convertFloatToScaledBigInt(body.velocity.y)// + maxVectorScaled newBody.radius = convertFloatToScaledBigInt(body.radius) if (body.c) { newBody.c = body.c @@ -849,6 +847,8 @@ if (module) { convertScaledBigIntBodyToArray, calculateForce, sqrtApprox, + approxDiv, + vectorLimit, scalingFactor, runComputation, runComputationBigInt, diff --git a/test/absoluteValueSubtraction.test.js b/test/absoluteValueSubtraction.test.js index 8f4166f7..36dfc33b 100644 --- a/test/absoluteValueSubtraction.test.js +++ b/test/absoluteValueSubtraction.test.js @@ -22,6 +22,7 @@ describe("absoluteValueSubtraction circuit", () => { it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInput[0].in, sanityCheck); + console.log(`| absoluteValueSubtraction(252) | ${witness.length} |`) await circuit.checkConstraints(witness); }); diff --git a/test/acceptableMarginOfError.test.js b/test/acceptableMarginOfError.test.js index cd3990b3..2594c85e 100644 --- a/test/acceptableMarginOfError.test.js +++ b/test/acceptableMarginOfError.test.js @@ -18,6 +18,7 @@ describe("acceptableMarginOfError circuit", () => { it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInput, sanityCheck); + console.log(`| acceptableMarginOfError(60) | ${witness.length} |`) await circuit.checkConstraints(witness); }); diff --git a/test/calculateForceMain.test.js b/test/calculateForceMain.test.js index 49f49aad..7dd77a17 100644 --- a/test/calculateForceMain.test.js +++ b/test/calculateForceMain.test.js @@ -1,31 +1,37 @@ const hre = require("hardhat"); const { assert } = require("chai"); -const { calculateForceBigInt, sqrtApprox, scalingFactor, convertBigIntToModP, convertScaledStringArrayToBody, convertScaledBigIntBodyToArray } = require("../docs/index.js"); +const { calculateForceBigInt, convertFloatToScaledBigInt, vectorLimit, convertBigIntToModP, convertScaledStringArrayToBody } = require("../docs/index.js"); const p = 21888242871839275222246405745257275088548364400416034343698204186575808495617n; describe("calculateForceMain circuit", () => { let circuit; - + // NOTE: velocities are offset by 10_000 to avoid negative numbers // sample inputs can have 0 and 0 for velocities since calculateForce doesn't involve velocity const sampleInputs = [ - // { - // in_bodies: [ - // ["32600000000", "6200000000", "-133000000", "-629000000", "10000000000"], - // ["26300000000", "15800000000", "-332000000", "-374000000", "7500000000"] - // ] - // }, { in_bodies: [ - ["36300000000", "65800000000", "0", "0", "7500000000"], - ["67900000000", "50000000000", "0", "0", "5000000000"] + ["326000", "62000", "8670", "3710", "100000"], + ["263000", "158000", "6680", "6260", "75000"] + ] + }, + { + in_bodies: [ + ["363000", "658000", "10000", "10000", "75000"], + ["679000", "500000", "10000", "10000", "50000"] + ] + }, + { + in_bodies: [ + ["226000", "42000", "10000", "10000", "100000"], + ["363000", "658000", "10000", "10000", "75000"] ] }, - // { - // in_bodies: [ - // ["22600000000", "4200000000", "0", "0", "10000000000"], - // ["36300000000", "65800000000", "0", "0", "7500000000"] - // ] - // } + { + in_bodies: [ + ["226000", "42000", "8670", "3710", "100000"], + ["363000", "658000", "6680", "13740", "75000"] + ] + } ]; const sanityCheck = true; @@ -35,6 +41,7 @@ describe("calculateForceMain circuit", () => { it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInputs[0], sanityCheck); + console.log(`| calculateForce() | ${witness.length} |`) await circuit.checkConstraints(witness); }); @@ -52,12 +59,19 @@ describe("calculateForceMain circuit", () => { }); it("has the correct output", async () => { - for (let i = 0; i < sampleInputs.length; i++) { const sampleInput = sampleInputs[i] const bodies = sampleInput.in_bodies.map(convertScaledStringArrayToBody) - const out_forces = calculateForceBigInt(bodies[0], bodies[1]).map(convertBigIntToModP) - const expected = { out_forces: [out_forces[0].toString(), out_forces[1].toString()] }; + const out_forces = calculateForceBigInt(bodies[0], bodies[1]).map(v => { + if (v < 0n) { + return [1, convertBigIntToModP(v * -1n)].map(n => n.toString()) + } else { + return [0, convertBigIntToModP(v)].map(n => n.toString()) + } + }) + // console.log({ out_forces }) + const expected = { out_forces }; + // console.log({ expected }) const witness = await circuit.calculateWitness(sampleInput, sanityCheck); await circuit.assertOut(witness, expected); } diff --git a/test/detectCollisionMain.test.js b/test/detectCollisionMain.test.js index 785f3a25..b1ae6ad2 100644 --- a/test/detectCollisionMain.test.js +++ b/test/detectCollisionMain.test.js @@ -11,11 +11,11 @@ describe("detectCollisionMain circuit", () => { const sampleInput = { "bodies": [ - ["22600000000", "4200000000", "-1", "-629000000", "10000000000"], - ["36300000000", "65800000000", "-332000000", "374000000", "7500000000"], - ["67900000000", "50000000000", "229000000", "252000000", "5000000000"] + ["226000", "42000", "9999", "3710", "100000"], + ["363000", "658000", "6680", "13740", "75000"], + ["679000", "500000", "12290", "12520", "50000"] ], - "missile": ["22600000000", "4200000000", "0", "0", "10000000000"] + "missile": ["226000", "42000", "10000", "10000", "100000"] }; const sanityCheck = true; @@ -25,6 +25,7 @@ describe("detectCollisionMain circuit", () => { it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInput, sanityCheck); + console.log(`| detectCollision(3) | ${witness.length} |`) await circuit.checkConstraints(witness); }); diff --git a/test/forceAccumulator.test.js b/test/forceAccumulator.test.js index 8ef9e243..359a39a7 100644 --- a/test/forceAccumulator.test.js +++ b/test/forceAccumulator.test.js @@ -17,20 +17,20 @@ describe("forceAccumulatorMain circuit", () => { const sampleInput = { bodies: [ - ["22600000000", "4200000000", "-133000000", "-629000000", "10000000000"], - ["36300000000", "65800000000", "-332000000", "374000000", "7500000000"], - ["67900000000", "50000000000", "229000000", "252000000", "5000000000"] - ] + ["226000", "42000", "8670", "3710", "100000"], + ["363000", "658000", "6680", "13740", "75000"], + ["679000", "500000", "12290", "12520", "50000"] + ], }; const sanityCheck = true; before(async () => { circuit = await hre.circuitTest.setup("forceAccumulatorMain"); - }); it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInput, sanityCheck); + console.log(`| forceAccumulator(3) | ${witness.length} |`) await circuit.checkConstraints(witness); }); diff --git a/test/getDistanceMain.test.js b/test/getDistanceMain.test.js index 686e906e..9540b067 100644 --- a/test/getDistanceMain.test.js +++ b/test/getDistanceMain.test.js @@ -5,10 +5,10 @@ describe("getDistanceMain circuit", () => { let circuit; const sampleInput = { - x1: "1300000000", - y1: "700000000", - x2: "400000000", - y2: "200000000", + x1: "13000", + y1: "7000", + x2: "4000", + y2: "2000", }; const sanityCheck = true; @@ -18,6 +18,7 @@ describe("getDistanceMain circuit", () => { it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInput, sanityCheck); + console.log(`| getDistance(20) | ${witness.length} |`) await circuit.checkConstraints(witness); }); @@ -36,7 +37,7 @@ describe("getDistanceMain circuit", () => { }); it("has the correct output", async () => { - const expected = { distance: 1029563015 }; // should be 900000000 but 1029563015 is within margin of error + const expected = { distance: 10295 }; // should be 9000 but 10295 is within margin of error const witness = await circuit.calculateWitness(sampleInput, sanityCheck); await circuit.assertOut(witness, expected); }); diff --git a/test/limiterMain.test.js b/test/limiterMain.test.js index 37af7b8f..bdbf7dfe 100644 --- a/test/limiterMain.test.js +++ b/test/limiterMain.test.js @@ -38,6 +38,7 @@ describe("limiterMain circuit", () => { it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInputs[0].sampleInput, sanityCheck); + console.log(`| limiter(252) | ${witness.length} |`) await circuit.checkConstraints(witness); }); diff --git a/test/lowerLimiterMain.test.js b/test/lowerLimiterMain.test.js index f4f6e574..626dd703 100644 --- a/test/lowerLimiterMain.test.js +++ b/test/lowerLimiterMain.test.js @@ -38,6 +38,7 @@ describe("lowerLimiterMain circuit", () => { it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInputs[0].sampleInput, sanityCheck); + console.log(`| lowerLimiter(252) | ${witness.length} |`) await circuit.checkConstraints(witness); }); diff --git a/test/nft.test.js b/test/nft.test.js index 1fc57f6d..0993f6ea 100644 --- a/test/nft.test.js +++ b/test/nft.test.js @@ -14,12 +14,12 @@ const p = 2188824287183927522224640574525727508854836440041603434369820418657580 describe("nft circuit", () => { let circuit; - + // NOTE: velocities are offset by 10_000 to avoid negative numbers const sampleInput = { bodies: [ - ["22600000000", "4200000000", "-133000000", "-629000000", "10000000000"], - ["36300000000", "65800000000", "-332000000", "374000000", "7500000000"], - ["67900000000", "50000000000", "229000000", "252000000", "5000000000"] + ["226000", "42000", "8670", "3710", "100000"], + ["363000", "658000", "6680", "13740", "75000"], + ["679000", "500000", "12290", "12520", "50000"] ] }; const sanityCheck = true; @@ -31,6 +31,7 @@ describe("nft circuit", () => { it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInput, sanityCheck); + console.log(`| nft(3, 10) | ${witness.length} |`) await circuit.checkConstraints(witness); }); diff --git a/test/stepStateMain.test.js b/test/stepStateMain.test.js index f3b58363..59d15c04 100644 --- a/test/stepStateMain.test.js +++ b/test/stepStateMain.test.js @@ -14,14 +14,14 @@ describe("stepStateMain circuit", () => { const sampleInput = { bodies: [ - ["22600000000", "4200000000", "-133000000", "-629000000", "10000000000"], - ["36300000000", "65800000000", "-332000000", "374000000", "7500000000"], - ["67900000000", "50000000000", "229000000", "252000000", "5000000000"] + ["226000", "42000", "8670", "3710", "100000"], + ["363000", "658000", "6680", "13740", "75000"], + ["679000", "500000", "12290", "12520", "50000"] ], // NOTE: need to have array of 11 when step = 10 because missiles need to be n + 1 missiles: [ - ["22600000000", "4200000000", "0", "0", "10000000000"], + ["226000", "42000", "10000", "10000", "100000"], ["0", "0", "0", "0", "0"], ["0", "0", "0", "0", "0"], ["0", "0", "0", "0", "0"], @@ -38,11 +38,11 @@ describe("stepStateMain circuit", () => { before(async () => { circuit = await hre.circuitTest.setup("stepStateMain"); - }); it("produces a witness with valid constraints", async () => { const witness = await circuit.calculateWitness(sampleInput, sanityCheck); + console.log(`| stepState(3, 10) | ${witness.length} |`) await circuit.checkConstraints(witness); });