The commit adds --wtns, which indicates the output directory for the
witness files. If not given, no witness file is generated.
The witness files are called `first-witness.wtns` and
`second-witness.wtns`.
This commit adds a framework for logging and exiting in a way that
conforms to the SaaS requirement. Logging in particular could be
done in either the JSON mode or the text mode.
The main entry point to the framework is the `with-framework` function.
This commit does not yet switch Picus to use the framework.
That will be done in a separate commit.
See `framework-test.rkt` for tests of the framework.
This commit adds a flag `--parallel <id> <num>` to the test script.
This divides the tests into <num> parts, and the script will
only run the <id>-th part.
We almost always only want the weak safety (checking that output signals
of the main component are deterministic), not strong safety
(checking that all signals are deterministic). However, currently the
strong safety mode is the default. This makes it cumbersome to invoke
Picus, since we need to indicate that we want the weak safety explicitly.
This commit inverts the behavior by removing the flag `--weak` and
adds the flag `--strong` (for strong safety), which is defaulted to false.
This commit adds a capability to process circom files directly
via the `--circom` flag. This is done by creating a
temporary directory to store the compiled r1cs file.
The temporary directory is cleaned up on exit when Picus exits normally.
However, when Picus crashes or when it is interrupted,
the temporary directory will not be cleaned, giving the user an
opportunity to inspect files.
Prior this commit, we cannot write tests expecting a timeout.
This commit adds the ability to do so.
Another major change is to support tests with optimization flag.
When Circom is given -O2, Circom files without public inputs
(which are all of our benchmarks) will fail to be compiled correctly.
This commit adds a heustistic to detect such situation,
and then "patch" the Circom file to add public inputs.
This is done by doing Circom compilation twice.
The first compilation allows us to read information from R1CS file,
which is then used for patching. The second compilation compiles
the patched file.
Prior this commit, `read-r1cs` copied bytes in the file over and over
again in a hot loop, causing the time complexity to be quadratic.
This commit switches to use index-based access in the hot loop instead,
resulting in a large performance improvement.
The benchmark file that accompanies this fix took 30 minutes to
successfully parse (according to @shankarapailoor).
This commit reduces the parsing time to 2 seconds.
It should be noted that not all bytes copying is avoided,
since bytes copying outside the hot loop, although not ideal,
does not really impact the performance.
- Prior this commit, every job depends on `publish-docker`, which is only
run on push. Therefore, all jobs are skipped. This commit fixes the
issue by removing the dependency.
- `publish-docker` is now also run as the last step, only when all tests passed.
- All subsequent jobs are now run on veridise/picus:git-latest,
so that we do not need to push first.
- The tests are slightly more sophisticated. Previously, it only ensures
that there's no error. Now, we also check against expected
output (underconstrained or not).
- Switch to use Racket and Rosette that are already installed in the
image. It turns out that we need to set the environment variable
`PLTADDONDIR` for this to work, because $HOME is overriden in containers
in GHA (https://github.com/actions/runner/issues/863).
- Remove a job that only compiles circomlib.
There's no point to do that.
