Commit the Miller value only when the degree needs it: −15% transaction weight

README.md

@@ -25,10 +25,10 @@ Simplicity has no pairing jets, so we applied a bunch of tricks to fit Groth16 v
 
 | | |
 |---|---|
-| program cost, one public signal | 81.7 M mWU |
-| transaction | 107.4 kWU, 26.9 kvB |
-| pruned program / witness | 61 kB / 45 kB |
-| fee at 0.115 sat/vB | ~ 3,100 sat |
+| program cost, one public signal | 68.5 M mWU |
+| transaction | 90.8 kWU, 22.7 kvB |
+| pruned program / witness | 60 kB / 30 kB |
+| fee at 0.115 sat/vB | ~ 2,600 sat |
 
 The program's bytes earn more budget than it costs, so it needs no padding. The transaction is about a quarter of the 400 kWU standard limit.
 

docs/benchmarks.md

@@ -4,30 +4,43 @@ All costs are Simplicity's static cost bound in milliweight units (mWU), as rust
 
 ## One spend
 
-The toy circuit's verifier (one public signal bound to the transaction), spent on an Elements 23.3.1 regtest node in `9f4c1cb0…`:
+The toy circuit's verifier (one public signal bound to the transaction), spent on an Elements 23.3.1 regtest node in `511a3da3…`:
 
 | | |
 |---|---|
-| program cost | 81,743,632 mWU |
-| budget: (witness stack bytes + 50) x 1000 | 106,812,000 mWU, no padding needed |
-| pruned program | 61,411 bytes |
-| witness (proof, Miller values, slopes, quotient, Merkle sibling) | 45,281 bytes |
-| transaction | 107,423 WU, 26,856 vB |
-| fee at 0.115 sat/vB, which Liquid testnet accepts | about 3,100 sat |
+| program cost | 68,491,902 mWU |
+| budget: (witness stack bytes + 50) x 1000 | 90,195,000 mWU, no padding needed |
+| pruned program | 60,346 bytes |
+| witness (proof, 35 Miller values, slopes, quotient, Merkle sibling) | 29,729 bytes |
+| transaction | 90,804 WU, 22,701 vB |
+| fee at 0.115 sat/vB, which Liquid testnet accepts | about 2,600 sat |
 
 ## Where the cost goes
 
 | part | mWU | share |
 |---|---:|---:|
-| the loop: 88 steps, each a few relations at z | 66,612,776 | 81.5% |
-| MSM of the public input: 51 windows of 5 bits | 8,645,785 | 10.6% |
-| setup: on-curve checks, powers of z, c(z), the Frobenius images, the transcript header | 3,166,661 | 3.9% |
-| reading the witness, passing it between the parts | 2,144,910 | 2.6% |
-| end: the last relations, Q(z), the two hashes | 1,147,204 | 1.4% |
+| the loop: 88 steps, each a few relations at z | 51,949,542 | 75.8% |
+| MSM of the public input: 51 windows of 5 bits | 8,645,785 | 12.6% |
+| end: the last relations, Q(z) (200 coefficients), the two hashes | 3,305,204 | 4.8% |
+| setup: on-curve checks, powers of z, c(z), the Frobenius images, the transcript header | 3,166,661 | 4.6% |
+| reading the witness, passing it between the parts | 1,398,414 | 2.0% |
 | transaction binding, range check | 26,296 | 0.0% |
-| total | 81,743,632 | |
+| total | 68,491,902 | |
 
-Of the loop, 55.6 M is in the steps and 11.0 M in folding the loop state over the witness: the state carries 33 per-run values (the powers of z, the points at z, r) to every step.
+Of the loop, 43.8 M is in the steps and 8.2 M in folding the loop state over the witness: the state carries 33 per-run values (the powers of z, the points at z, r) to every step.
+
+## Where the bytes go
+
+| | bytes |
+|---|---:|
+| line constants of γ and δ: 4 words per pair and step | 22,528 |
+| program code | about 26,000 |
+| MSM: selected table entries and pruned branches | about 11,400 |
+| 35 committed Miller values | 13,440 |
+| quotient Q, 200 coefficients | 6,400 |
+| B's slopes, 88 steps | 5,632 |
+| inverses proving xQ != x, 23 additions | 1,472 |
+| MSM slopes, c, c^-1, the proof, the challenges | about 2,900 |
 
 ## Building blocks
 
@@ -38,30 +51,31 @@ Of the loop, 55.6 M is in the steps and 11.0 M in folding the loop state over th
 | F_p product with a constant, or normalisation | 8,923 |
 | F_p addition | 2,579 |
 | 12-term dot product, one reduction | 116,744 |
-| loop step: doubling (65 of them) | 609,273 |
-| loop step: addition with c or c^-1 (21) | 698,901 |
-| loop step: Frobenius addition (2) | 683,092 |
+| loop step: doubling (51 of them) | 385,831 |
+| loop step: doubling with a committed Miller value (14) | 608,873 |
+| loop step: addition with c or c^-1, committed (21) | 698,901 |
+| loop step: Frobenius addition (2) | 455,950 |
+| Q(z): eight coefficients (25 calls) | 94,597 |
 | MSM window (select and add) | about 169,500 |
 
-A doubling step evaluates the committed Miller value at z (a 12-term dot product), B's slope, the three lines, and adds its two relations to the Horner sum. Computed in the tower, the same step cost 3,644,556.
+A doubling step evaluates B's slope and the three lines at z and adds its relations to the Horner sum; a committed one also evaluates the committed Miller value (a 12-term dot product). Computed in the tower, the same step cost 3,644,556.
 
 ## Before and after
 
-| | tower Miller loop | one polynomial identity |
+| | tower Miller loop (main) | one polynomial identity |
 |---|---:|---:|
-| program cost | 371.8 M mWU (with 414 padding blocks) | 81.7 M mWU |
-| pruned program | 161 kB | 61 kB |
-| witness | 220 kB (212 kB of it padding) | 45 kB |
-| transaction | 382.2 kWU, 95.6 kvB | 107.4 kWU, 26.9 kvB |
-| room under the 400 kWU limit | one more public input | about 20 more |
+| program cost | 371.8 M mWU (with 414 padding blocks) | 68.5 M mWU |
+| pruned program | 161 kB | 60 kB |
+| witness | 220 kB (212 kB of it padding) | 30 kB |
+| transaction | 382.2 kWU, 95.6 kvB | 90.8 kWU, 22.7 kvB |
 
 ## Time
 
 | | |
 |---|---|
 | generate the program from a key (Python) | 2 s |
 | generate the witness: Miller values, residue witness, quotient (Python) | 2 s |
-| `deploy compile`: parse the 1.1 MB program text, once per key | 2.6 min |
+| `deploy compile`: parse the 1.1 MB program text, once per key | 2.5 min |
 | `deploy spend`: prune, execute, build the transaction | 1 s |
 | snarkjs setup / proof of the toy circuit | 1.3 min / 1 s |
 | `tests/test_groth16.py` | 3 min |
@@ -82,7 +96,7 @@ python3 tests/test_groth16.py    # the whole verifier
 python3 tests/test_binding.py    # the verifier with the transaction binding
 ```
 
-`deploy spend` prints the cost, the sizes and the budget of a real transaction, and `tools/harness/target/release/costs <program.simpl>` the cost of every named definition of a program. The files in `examples/multiplier/` regenerate the program and the witness of the regtest spend `9f4c1cb0…` byte for byte:
+`deploy spend` prints the cost, the sizes and the budget of a real transaction, and `tools/harness/target/release/costs <program.simpl>` the cost of every named definition of a program. The files in `examples/multiplier/` regenerate the program and the witness of the regtest spend `511a3da3…` byte for byte:
 
 ```sh
 E=examples/multiplier
@@ -95,8 +109,8 @@ gunzip -c $E/verifier.simpl.gz | cmp - build/check.simpl && gunzip -c $E/verifie
 
 | network | transaction | what |
 |---|---|---|
-| Elements 23.3.1 regtest | `0da39ffd…` | the walkthrough (`tools/regtest.sh`): proof spend, 107,421 WU, vsize 26,856 |
-| Elements 23.3.1 regtest | `901f2f6a…` | the same kind of proof redirected to another address: rejected with `Assertion failed inside jet` |
-| Elements 23.3.1 regtest | `9f4c1cb0…` | proof spend, the files in `examples/multiplier/` |
-| Elements 23.3.1 regtest | `d8d87a6a…` | the key path of the same leaf, 721 WU |
+| Elements 23.3.1 regtest | `beba377d…` | the walkthrough (`tools/regtest.sh`): proof spend, 90,804 WU, vsize 22,701 |
+| Elements 23.3.1 regtest | `511a3da3…` | proof spend, the files in `examples/multiplier/` |
+| Elements 23.3.1 regtest | a redirected proof | rejected with `Assertion failed inside jet` |
+| Elements 23.3.1 regtest | `5b6b46f1…` | the key path of the same leaf, 721 WU |
 | Liquid testnet | [`f25a6e90…`](https://blockstream.info/liquidtestnet/tx/f25a6e90417c427f25c1d6883869825f30ec111a357b0e550bf24a20725d3cdb), block 2,659,534 | an earlier verifier (tower Miller loop, without the G2 check): 381,492 WU, fee 11,000 sat |

docs/design.md

@@ -117,12 +117,14 @@ The Groth16 equation e(A, B) = e(α, β) e(L, γ) e(C, δ) holds if and only if
 
 The Miller loop runs along the signed-binary (NAF) digits of 6x + 2, the loop length of BN254's optimal ate pairing, and ends with two additions by Frobenius images of each G2 point: 88 steps, 65 doublings and 23 additions. The three pairs (-A, B), (L, γ) and (C, δ) advance in lockstep, so the accumulator f is squared once per step for all of them. The fourth pair, (α, β), belongs to the verifying key; its Miller value is a constant of the program.
 
-Each step multiplies f (squared, for a doubling) by three lines, one per pair, each of the form `yP + c3 xP w + c4 w^3` with c3 = -λ and c4 = λ xT - yT, where T is the pair's running G2 point and λ the slope of the step. The prover writes the new value f' into the witness, and the step becomes a relation between polynomials:
+Each step multiplies f (squared, for a doubling) by three lines, one per pair, each of the form `yP + c3 xP w + c4 w^3` with c3 = -λ and c4 = λ xT - yT, where T is the pair's running G2 point and λ the slope of the step. When the prover writes the new value f' into the witness, the step becomes a relation between polynomials:
 
 ```
 f^2 l_B l_γ l_δ - f' = 0   (mod M)
 ```
 
+The prover does not commit after every step. Without a commitment, f' is the product itself, a polynomial of higher degree that the next relation carries along, and that next relation checks two steps at once. A committed value costs 12 witness words; a higher degree costs words of the quotient (below). The generator skips a commitment whenever the identity's degree stays within 211, the cap with the fewest words in total: 35 of the 88 Miller values are committed.
+
 γ and δ belong to the key, so their slopes and lines are computed when the program is generated: each step receives c3 and c4 for both, four words each. B comes from the proof. The prover writes only B's slopes; B's points are never written down. The new point of a doubling is x' = λ^2 - 2x, y' = λ (x - x') - y, a polynomial in the slopes, and the program checks each slope instead:
 
 ```
@@ -148,21 +150,21 @@ The loop also proves that B is in G2. Its last point is T = [6x+2]B + ψ(B) - ψ
 
 ### One identity, checked at one point
 
-That makes 203 relations R_k, each a polynomial in w of degree at most 61. The prover combines them with the powers of a challenge r into S = Σ r^k R_k, divides S by M, and writes the quotient Q (50 coefficients) into the witness. The program then picks a point z, evaluates every polynomial at z, and checks
+That makes 150 relations R_k, each a polynomial in w of degree at most 211. The prover combines them with the powers of a challenge r into S = Σ r^k R_k, divides S by M, and writes the quotient Q (200 coefficients) into the witness. The program then picks a point z, evaluates every polynomial at z, and checks
 
 ```
 S(z) = Q(z) M(z)
 ```
 
 This is randomized extension-field arithmetic: [Garaga](https://hackmd.io/@feltroidprime/B1eyHHXNT) checks each F_p12 product with its own quotient, and Novakovic and Eagen (section 6) combine all relations into one quotient, as here. Two things are specific to this verifier: the challenges come from SHA-256 inside the program, and B's F_p2 arithmetic is part of the same identity, so B's points never enter the witness.
 
-The program never multiplies in F_p12. A committed value f' becomes the number f'(z), a 12-term dot product with the powers of z; a line becomes a number; a step's relation becomes a few F_p products, added to a running Horner sum of S(z). A doubling step costs 0.61 M mWU, against 3.6 M for computing it in the tower.
+The program never multiplies in F_p12. A committed value f' becomes the number f'(z), a 12-term dot product with the powers of z; a line becomes a number; a step's relation becomes a few F_p products, added to a running Horner sum of S(z). A doubling step costs 0.39 M mWU, or 0.61 M with a commitment, against 3.6 M for computing it in the tower. Q(z) is evaluated eight coefficients at a time by one shared function, so its code is in the program once.
 
-r and z come from SHA-256 (Fiat-Shamir): r hashes the public inputs, the proof, c, c^(-1), s and everything the loop committed, and z hashes r and Q. The program gets r and z as witness words, uses them throughout, and at the end compares them with the two hashes it has computed along the way. If some relation does not hold, S is nonzero modulo M except for at most 203 values of r, and then S - Q M is a nonzero polynomial of degree at most 61, which vanishes at z with probability at most 61/p. A cheating prover must find a hash output in a set of relative size about 2^-246.
+r and z come from SHA-256 (Fiat-Shamir): r hashes the public inputs, the proof, c, c^(-1), s and everything the loop committed, and z hashes r and Q. The program gets r and z as witness words, uses them throughout, and at the end compares them with the two hashes it has computed along the way. If some relation does not hold, S is nonzero modulo M except for at most 150 values of r, and then S - Q M is a nonzero polynomial of degree at most 211, which vanishes at z with probability at most 211/p. A cheating prover must find a hash output in a set of relative size about 2^-245.
 
 The committed words are checked to be below 2^254 (their two top bits are zero), so that the 12-term dot products fit the bound of the field arithmetic; every canonical word passes. The program normalises the challenges, whose words are arbitrary 256-bit hashes.
 
-The witness grows to 45 kB, mostly the 88 committed Miller values, and the program shrinks to 61 kB, since the line data of γ and δ is now four words per pair and step instead of eighteen.
+The witness is 30 kB: the committed Miller values (13 kB), the quotient (6 kB), B's slopes (6 kB) and the rest of the proof. The program is 60 kB; the line data of γ and δ, four words per pair and step, is 22 kB of it.
 
 ## Public input and transaction binding (curve.py, merkle.py, groth16.py)
 
@@ -172,7 +174,7 @@ To need only one, a circuit for this verifier exposes a single public signal: th
 
 ## Budget and padding (groth16.py)
 
-The program costs 81.7 M mWU. Its budget is 1,000 mWU per byte of the input's witness stack, so the 61 kB program and the 45 kB witness already earn about 107 M mWU, and no padding is needed: the input weighs about 107 kWU.
+The program costs 68.5 M mWU. Its budget is 1,000 mWU per byte of the input's witness stack, so the 60 kB program and the 30 kB witness already earn about 90 M mWU, and no padding is needed: the transaction weighs about 91 kWU.
 
 Programs that cost more than their bytes earn can still be padded. Elements does not relay transactions with an annex, the field rust-simplicity would use for padding, so the blocks of 512 zero bytes go into the Simplicity witness. A witness value the program never reads would get the wrong type, so each block is hashed into a throwaway SHA-256 context, which costs 25.5 k mWU per block. `Groth16.padding` sizes the padding from the program's cost, and `deploy spend` reports whether the budget is covered.
 

examples/README.md

@@ -16,13 +16,13 @@ tools/harness/target/release/hand examples/fp_mul.simpl examples/fp_mul.w0.json
 
 ## multiplier/
 
-The verifier of `circuits/multiplier.circom` (a·b = c, bound to the spending transaction) and the files of one spend on an Elements regtest node, transaction `9f4c1cb0…`, which proves c = 21.
+The verifier of `circuits/multiplier.circom` (a·b = c, bound to the spending transaction) and the files of one spend on an Elements regtest node, transaction `511a3da3…`, which proves c = 21.
 
 | file | |
 |---|---|
 | `verification_key.json` | the snarkjs key |
 | `verifier.simpl.gz` | the generated program, 1.1 MB of text |
-| `verifier.uprog` | its consensus encoding before pruning (`deploy compile`), CMR `c910831b…26b0be62` |
+| `verifier.uprog` | its consensus encoding before pruning (`deploy compile`), CMR `e502d43b…47fb0d6b` |
 | `proof.json`, `public.json` | the snarkjs proof and its public signal |
 | `leaves.json` | the two leaves behind the public signal: the transaction's sighash and c |
 | `verifier.w0.json.gz` | the witness: proof, Miller values, slopes, quotient, Merkle sibling |

examples/multiplier/leaves.json

@@ -1 +1 @@
-{"sighash": "2430abe796bfee9e30559fe742228b1d36004de4a4b0c4cb945366aa31bb7321", "values": ["21"]}
+{"sighash": "cdac35b192915c6ebbc240dd8c4f8d22cf4e5e13087fb23e9978fbc6ce2cb05c", "values": ["21"]}

examples/multiplier/proof.json

@@ -1,26 +1,26 @@
 {
  "pi_a": [
-  "7614975239070624198332854401873649505470572626547896149741070312897843358930",
-  "4611774705360608746977331987834566924868049144042721246704404533437671643615",
+  "21566684453736135585297791733111880454710809102449812304555056051874966362175",
+  "20439253185853980828249216164238736927967952351267181741770936990431369438778",
   "1"
  ],
  "pi_b": [
   [
-   "5261944696180792681624872483670754604546279463032739224986573158204266522465",
-   "12317633613943012002930990405081707670179665685030284658975824394534056369377"
+   "2376322599524250606318122939551750522956957733513865503231378596442919457301",
+   "21315688201840938592689832640776347449862151534123330070129388622190619729110"
   ],
   [
-   "21154522702036096038089906596923283702887853601323724616219725041146024442675",
-   "17356759660496773857362515270681502939595449805612756466401971378462211378698"
+   "3943731764001132601666642157228626600487124330574975950047211703846244120826",
+   "9258774679406286764135352324685156081411875551338919970350745361914487123535"
   ],
   [
    "1",
    "0"
   ]
  ],
  "pi_c": [
-  "3199714410403655289905644902552955024418647404663178093197136563332313053728",
-  "11760199718826279720608869179394965276413967892246556778442807843086576418841",
+  "4638708091212589675127653121818387886945714069030086334439062558372181182618",
+  "8670616252775378861952872650202232831163409290031897847958971087012591991932",
   "1"
  ],
  "protocol": "groth16",

examples/multiplier/public.json

@@ -1,3 +1,3 @@
 [
- "11319441843641788037619681105067091827983231747872427158058865524502604764122"
+ "51333353947613502813995737443488039187621314919488324933339036886237847445"
 ]