Merge pull request #4 from okwme/break-up-vector-simple

trifle-labs · Oct 21, 2023 · 0c34657 · 0c34657
2 parents 33d95a0 + 5eb58cf
commit 0c34657
Show file tree

Hide file tree

Showing 22 changed files with 414 additions and 325 deletions.
diff --git a/README.md b/README.md
@@ -172,35 +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() | 842 |
-| detectCollision(3) | 1,548 |
-| forceAccumulator(3) | 4,518 |
-| 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) | 6,157 |
-| stepState(3, 10) | 61,570 |
-| stepState(3, 100) | 615,700 |
-| stepState(4, 1) | 9,863 |
-| stepState(4, 10) | 98,630 |
-| stepState(4, 100) | 986,300 |
+| 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/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
@@ -1,6 +1,7 @@
 pragma circom 2.1.6;
 
 include "approxMath.circom";
+include "helpers.circom";
 
 template CalculateForce() {
 /* 
@@ -28,42 +29,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 = 3; // maxBits: 2
+  var scalingFactor = 10**scalingFactorFactor; // maxBits: 10 (maxNum: 1_000)
+
+  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: 20 (maxNum: 1_000_000)
 
+  var GScaled =  Gravity * scalingFactor; // maxBits: 17 (maxNum: 100_000)
+  // log("GScaled", GScaled);
 
   signal input in_bodies[2][5];
-  signal output out_forces[2];
+  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
 
-  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: 36 (maxNum: 40_000_000_000)
+  // NOTE: minDistanceScaled is maximum of 
   // log("minDistanceScaled", minDistanceScaled);
-  var body1_position_x = in_bodies[0][0];
+  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 = in_bodies[0][1];
+  var body1_position_y = getY(in_bodies[0]); // maxBits: 20 (maxNum: 1_000_000) = 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 = getMass(in_bodies[0]); // maxBits: 14 = numBits(13 * scalingFactor) (maxNum: 13_000)
+
+  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 = in_bodies[1][1];
+  var body2_position_y = getY(in_bodies[1]); // maxBits: 20 (maxNum: 1_000_000) = windowWidthScaled
   // log("body2_position_y", body2_position_y);
-  var body2_radius = in_bodies[1][4];
+
+  // NOTE: maximum radius currently 13
+  var body2_radius = getMass(in_bodies[1]); // maxBits: 14 = numBits(13 * scalingFactor) (maxNum: 13_000)
 
-  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
-  absoluteValueSubtraction.in[0] <== body1_position_x;
-  absoluteValueSubtraction.in[1] <== body2_position_x;
-  signal dxAbs <== absoluteValueSubtraction.out;
+  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;
-  component absoluteValueSubtraction2 = AbsoluteValueSubtraction(60); // TODO: test limit
-  absoluteValueSubtraction2.in[0] <== body1_position_y;
-  absoluteValueSubtraction2.in[1] <== body2_position_y;
-  signal dyAbs <== absoluteValueSubtraction2.out;
+  signal dy <== body2_position_y - body1_position_y; // maxBits: 254 because it can be negative
+  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);
@@ -72,121 +90,110 @@ template CalculateForce() {
   // log("dxAbs", dxAbs);
   // log("dyAbs", dyAbs);
 
-  signal dxs <== dxAbs * dxAbs;
+  signal dxs <== dxAbs * dxAbs; // maxBits: 40 = 20 * 2 (maxNum: 1_000_000_000_000)
   // log("dxs", dxs);
-  signal dys <== dyAbs * dyAbs;
+  signal dys <== dyAbs * dyAbs; // maxBits: 40 = 20 * 2 (maxNum: 1_000_000_000_000)
   // log("dys", dys);
-  signal unboundDistanceSquared <== dxs + dys;
+  signal unboundDistanceSquared <== dxs + dys; // maxBits: 41 = 40 + 1 (maxNum: 2_000_000_000_000)
   // log("unboundDistanceSquared", unboundDistanceSquared);
 
-  component lessThan = LessThan(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;
+  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;
-  myMux.c[1] <== minDistanceScaled;
+  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;
+  signal distanceSquared <== myMux.out; // maxBits: 41 (maxNum: 2_000_000_000_000)
 
   // 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: 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(60);  // TODO: test the limits of this. 
-  acceptableMarginOfError.expected <== distance ** 2;
-  acceptableMarginOfError.actual <== distanceSquared;
+  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;
 
 
-  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: 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;
-  myMux2.c[1] <== 0;
+  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;
+  isZero2.in <== body2_radius; // maxBits: 14
 
   component myMux3 = Mux1();
-  myMux3.c[0] <== myMux2.out;
-  myMux3.c[1] <== 0;
+  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;
+  signal bodies_sum <== myMux3.out; // maxBits: 17 (maxNum: 104_000)
 
   // 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: 42 (maxNum: 4_000_000_000_000)
   // 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: 44 (maxNum: 10_400_000_000_000)
   // log("forceMag_numerator", forceMag_numerator);
 
-  signal forceDenom <== distanceSquared_with_avg_denom * distance;
+  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;
+  signal forceXnum <== dxAbs * forceMag_numerator; // maxBits: 64 (maxNum: 10_400_000_000_000_000_000)
   // log("forceXnum", forceXnum);
-  signal forceXunsigned <-- approxDiv(forceXnum, forceDenom);
+  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;
-  component acceptableErrorOfMarginDiv1 = AcceptableMarginOfError(divisionBits);  // TODO: test the limits of this. 
-  acceptableErrorOfMarginDiv1.expected <== forceXnum;
-  acceptableErrorOfMarginDiv1.actual <== approxNumerator1;
-  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();
-  isZero3.in <== dxAbs + dx;
+  // NOTE: isZero handles overflow bit values correctly
+  isZero3.in <== dxAbs + dx; // maxBits:  maxBits: 21 (maxNum: 2_000_000)
   // log("isZero3", dxAbs + dx, isZero3.out);
-  component myMux4 = Mux1();
-  myMux4.c[0] <== forceXunsigned;
-  myMux4.c[1] <== forceXunsigned * -1;
-  myMux4.s <== isZero3.out;
-  signal forceX <== myMux4.out;
-  // log("forceX", forceX);
-
-  signal forceYnum <== dyAbs * forceMag_numerator;
+  out_forces[0][0] <== isZero3.out; // isZero is 1 when dx is negative
+  out_forces[0][1] <== forceXunsigned; // maxBits 64 (maxNum: 10_400_000_000_000_000_000)
+
+  signal forceYnum <== dyAbs * forceMag_numerator; // maxBits:64 (maxNum: 10_400_000_000_000_000_000)
   // log("forceYnum", forceYnum);
-  signal forceYunsigned <-- approxDiv(forceYnum, forceDenom);
+  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;
-  component acceptableErrorOfMarginDiv2 = AcceptableMarginOfError(divisionBits);  // TODO: test the limits of this. 
-  acceptableErrorOfMarginDiv2.expected <== forceYnum;
-  acceptableErrorOfMarginDiv2.actual <== approxNumerator2;
-  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();
-  isZero4.in <== dyAbs + dy;
-  component myMux5 = Mux1();
-  myMux5.c[0] <== forceYunsigned;
-  myMux5.c[1] <== forceYunsigned * -1;
-  myMux5.s <== isZero4.out;
-  signal forceY <== myMux5.out;
-  // log("forceY", forceY);
-
-  out_forces[0] <== forceX;
-  out_forces[1] <== forceY;
-}
+    // NOTE: isZero handles overflow bit values correctly
+  isZero4.in <== dyAbs + dy; // maxBits: 255 = max(37, 254) + 1
 
-
-/* INPUT = {
-    "in_bodies": [ ["82600000000", "4200000000", "-133000000", "-629000000", "10000000000"], ["36300000000", "65800000000", "-332000000", "374000000", "7500000000"] ]
-} */
+  // log("forceY", forceY);
+  out_forces[1][0] <== isZero4.out;
+  out_forces[1][1] <== forceYunsigned; // maxBits 64 (maxNum: 10_400_000_000_000_000_000)
+}