Skip to content

speedrunpapi 0.7.1

Latest

Choose a tag to compare

@lmtlssss lmtlssss released this 11 Nov 02:55
e7300e4

speedrunpapi 0.7.1

This release replaces the analyzer.

There is no 0.7.0 package. A v0.7.0 tag was pushed to the wrong commit by mistake, the publish workflow's version guard refused it, and release tags in this repository are immutable, so the tag stays and the release is 0.7.1.

What was wrong

Versions before 0.7.1 classified Circom, Verilog and INT8 sources by template name and keyword. They did not analyse the constraint system. A circuit whose output was assigned with <-- and never constrained was reported Certified if its main template had a recognised name such as BigAdd, or if the file mentioned BinSum. The hosted service signed those verdicts, and also signed verdicts that a client merely reported.

Those results were not proofs. If you relied on a Certified result from an earlier version, scan again with this one. Every certificate issued before 0.7.1 has been revoked; the revocation feed is at https://api.colony.technology/v1/revocations.

What 0.7.1 does

scan compiles Circom with the real circom compiler and analyses the R1CS it emits for output determinism: do two satisfying witnesses with the same inputs always have the same outputs?

  • Certified: a derivation shows they do. An independent checker replays it before the verdict is reported.
  • Broken: two witnesses that share every input and differ on an output. Both are re-evaluated against every constraint.
  • Unknown: neither was established. The open signals are listed with the condition under which a constraint would fix them.

The report (--report) carries the derivation or the witnesses and can be checked without the scanner: speedrunpapi verify, or the standard-library Python checker in verifiers/determinism/.

New options: --main "Template(args)" for library files, -l/--include, --assume-binary for inputs a template expects to be bits (the assumption becomes part of the claim), --strict for witness uniqueness, --report, --opt.

Measured

circomlib templates, circom 2.2.3 --O0, Apple M1, Node.js 26, single runs:

Circuit Verdict Constraints Prove Replay
Sha256compression() Certified 202,784 228 ms 155 ms
Poseidon(5) Certified 1,347 1.9 ms 1.1 ms
LessThan(252) Certified 256 0.8 ms 0.6 ms
Num2Bits(254) Broken 255
Decoder(4) Broken 6
MontgomeryAdd() Broken 3

The Broken rows hold for those templates taken alone with unrestricted inputs; circomlib uses them where the caller excludes the degenerate cases. The 71-case corpus has 46 Certified, 15 Broken and 10 Unknown, and no verdict contradicts the known answer. A fuzzer that compares the engine with brute-force enumeration over small fields ran 150,000 random systems without a wrong Certified or Broken.

What still returns Unknown

Elliptic-curve arithmetic whose uniqueness rests on a number-theoretic fact (Baby Jubjub addition), big-integer arithmetic that depends on range bounds across limbs, alias checks such as Num2Bits_strict, circuits with no outputs, and R1CS with custom gates.

Breaking changes

  • Verilog, INT8, ONNX-text and carry-graph inputs return Unknown. Those classifiers are removed.
  • Bitcoin Script and RV32IM trace inputs return Unknown. An audit found that the Script adapter executed nothing (it reported Certified for scripts that can never complete) and that the trace adapter only replayed a trace against instruction words the trace itself supplied.
  • Result JSON has a new shape (schema: colony.determinism/1). Results from earlier versions cannot be verified.
  • The hosted API signs only Certified or Broken results that it re-verified from a submitted R1CS (up to 8 MiB). It no longer signs client-reported verdicts or Unknown.
  • The GitHub Action no longer requires an API key. It scans locally and fails on Broken; a key adds a signed certificate.

The hosted-job client (run, solve, optimize, check, ...) and the ONNX checker are unchanged.