Previously, we added them during a constraint optimization pass as
a part of the AST traversal. This is not ideal for many reasons.
First, we only want to include the definitons once,
but the AST traversal opens an opportunity to accidentally include them
more than once (e.g. if we happen to have a rcmds as a subnode of another node).
Second, it meant that we needed the pdef? parameter so that
on alternative constraints, the prime definitions are omitted.
The refactoring simply put the definition inclusion at the top-level,
simplifying the optimization pass.
Prior this commit, yvec will reuse input variables from xvec
which is sound because we assume that they are equal anyway.
However, this reusing adds complexity to Picus.
This commit removes the reusing, simplifying the codebase.
The removal should also not affect performance,
since SMT solvers are very good at dealing with equalities.
This also allows modular verification to be programmed more
straightforwardly.
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 fixes the problem where an interrupt will not kill a
solver spawn by Picus, causing many solvers to be run concurrently in
the background. Since the fix needs to be applied to three files
that communicate with cvc5, Z3, and cvc4, I also took an opportunity to
refactor them and unify them into one common file.
We should avoid building the resulting query string with `format`
repeatedly, because `format` creates an entirely new string in
each invocation. When the query is big, the cost is
prohibitively expensive.
This commit instead builds the query string by writing to a
string port directly (similar to the StringBuilder idiom in languages
like Java). As the fix needs to be done on Z3, cvc4, and cvc5, I also
take an opportunity to refactor them to reduce code redundancy.
Instead of using `rcmds-ref` in a loop, which takes quadratic time,
directly iterate over three consecutive elements simultaneously,
making it linear time traversal.
This change makes the large benchmark not stuck at aboz lemma.
Previously, we use `(list->set (set->list ks))` to copy the set `ks`,
but this is in fact not needed at all. `ks`, which is an immutable set,
can't be structurally mutated (although its binding can be mutated).
The copying is especially harmful when it's done in a hot loop
(the `update` function in particular), since known and unknown set could
be very large.
This change makes the large benchmark not stuck at basis2-lemma
Prior this commit, linear lemma depends on the CDMAP and RCDMAP
procedures.
Let's say that constraint i involves variables Xi and Yi, where Xi variables
are the linear part, and Yi variables are the non-linear parts.
That is to say, the input follows this format:
Constraint 1: X11 X12 ... Y11 Y12 ...
Constraint 2: X21 X22 ... Y21 Y22 ...
...
Constraint n: Xn1 Xn2 ... Yn1 Yn2 ...
which is of size O(sum |Xi| + sum |Yi|).
The CDMAP procedure produces a map from a variable to a list of list of
variables. Meaning: a key can be uniquely determined if one of the list
of variables are all uniquely determined.
Thus, CDMAP produces a data of size O(sum { |Xi| (|Xi| + |Yi|) }) as the
output (where values of the same key are grouped together)
X11: X12 X13 ... Y11 Y12 ...
X12: X11 X13 ... Y11 Y12 ...
...
X1k: X11 X12 ... Y11 Y12 ...
X21: X22 X23 ... Y21 Y22 ...
X22: X21 X23 ... Y21 Y22 ...
...
.....
Xn1: Xn2 Xn3 ... Yn1 Yn2 ...
Xn2: Xn1 Xn3 ... Yn1 Yn2 ...
...
Xnk: Xn1 Xn2 ... Yn1 Yn2 ...
Often, some clauses might have O(n) variables, making the size
O(n^3) if the table is dense, or O(n^2) if the table is sparse.
The RCDMAP procedure essentially consumes a map that CDMAP procedure
outputs, and produces the inverse of that map, with duplicate keys of
the input map grouped together. The size is thus the same.
RCDMAP is also used in the counter selector. E.g., given:
1 2 3 | 4 6
1 3 5 | 4 6
Then CDMAP produces:
1: [2 3 4 6, 3 5 4 6]
2: [1 3 4 6]
3: [1 2 4 6, 1 5 4 6]
5: [1 3 4 6]
And RCDMAP produces:
1 3 4 6: [2, 5]
2 3 4 6: [1]
3 5 4 6: [1]
1 2 4 6: [3]
1 5 4 6: [3]
The counter selector counts that 5 occurs 2 times in the keys,
so it is weighted 2. 6, by contrast, occurs 5 times, so it is weighted 5.
-------------------------------------------------------------------
This commit aims to improve the performance by avoiding blowing up the
data size beyond linear. It also aims to preserve the existing behavior
as much as possible.
This is done by removing the CDMAP and RCDMAP procedures,
and instead employing the straightforward encoding:
X11 X12 ... | Y11 Y12 ...
X21 X22 ... | Y21 Y22 ...
...
Xn1 Xn2 ... | Yn1 Yn2 ...
which has the linear size.
When a variable is uniquely determined, we simply cross it off from the
above table. A variable becomes propagable when it's the only one left
in the linear part, and the non-linear part is empty.
For counter selector, we produce the counter without expanding the
encoding beyond linear size. This can be done by simple multiplication:
in (Xi, Yi), each variable in Xi contributes to other variables in Xi
exactly |Xi|-1 times (not counting itself) and each variable in Yi
contributes to other variables in Xi exactly |Xi| times.
The results are not the same, however. Consider the earlier concrete example:
Our encoding:
1 2 3 | 4 6
1 3 5 | 4 6
RCDMAP:
1 3 4 6: [2, 5]
2 3 4 6: [1]
3 5 4 6: [1]
1 2 4 6: [3]
1 5 4 6: [3]
The weights of 5 in both our encoding and RCDMAP agree: 2.
However, the weights of 6 do not agree.
Our encoding produces weight 6.
RCDMAP produces weight 5.
Arguably, our weight is more "correct", because it takes the value
part into account. I.e., in "1 3 4 6: [2, 5]", 6 contributes twice
(2 once and 5 once), so it should be counted twice.
Separately, I also believe that the counter selector is not ideal,
and plan to revamp the strategy soon, so the discrepancies will not
matter anyway.
In basis2 lemma, set-remove (which removes a single element) is used
instead of set-subtract (which removes a set of elements).
Previously, Picus gets away with this incorrect result because linear
lemma will "clean up" afterward by syncing known set and unknown set.
However, in the PR #18, we no longer do this syncing,
thus uncovering this issue. This commit fixes the problem.
Instead of using list-ref in a loop (which takes quadratic time)
and list membership in a loop (which also takes quadratic time),
switch to direct element iteration and set membership query.
This reduces the running time from >10mins (I haven't fully measured it.
Terminated it early because I don't want to wait) to 0.6s.
This commit renames the existing --verbose to --cex-verbose,
and makes --verbose control the non-counterexample output,
which could be overwhelming on a very large circuit.
Similar to --cex-verbose, there are three levels for --verbose.
- 0: hides "large" outputs entirely.
- 1: shows the output, but display ... when the output is too large
- 2: shows the full output.
This commit adds a flag `--verbose` for verbose level,
which supplants the flag `--raw-output` (or, previously, `--map`).
- When the verbose level is 0 (not verbose),
the output is in the circom variable format.
- When the verbose level is 1, the output is a mixed between the circom
variable format and the r1cs signal format, where we prefer the circom
variable format whenever possible.
- When the verbose level is 2, the output is always in
the r1cs signal format.
For `--verbose 0`, the output now has three sections: inputs, first
possible outputs, and second possible outputs.
For other verbosity level, there could be four sections. The extra
section is "other bindings".
Entries that are different in the first possible outputs and
second possible outputs are further highlighted with ANSI escape sequence.
Examples:
With `--verbose 0`:
```
# inputs:
# m1.main.inp: 0
# first possible outputs:
# m1.main.out[0]: 0
# m1.main.out[1]: 0
# m1.main.success: 0
# second possible outputs:
# m2.main.out[0]: 1
# m2.main.out[1]: 0
# m2.main.success: 1
```
With `--verbose 1`:
```
# inputs:
# m1.main.inp: 0
# first possible outputs:
# m1.main.out[0]: 0
# m1.main.out[1]: 0
# m1.main.success: 0
# second possible outputs:
# m2.main.out[0]: 1
# m2.main.out[1]: 0
# m2.main.success: 1
# other bindings:
# one: 1
# p: 21888242871839275222246405745257275088548364400416034343698204186575808495617
# ps1: 21888242871839275222246405745257275088548364400416034343698204186575808495616
# ps2: 21888242871839275222246405745257275088548364400416034343698204186575808495615
# ps3: 21888242871839275222246405745257275088548364400416034343698204186575808495614
# ps4: 21888242871839275222246405745257275088548364400416034343698204186575808495613
# ps5: 21888242871839275222246405745257275088548364400416034343698204186575808495612
# zero: 0
```
With `--verbose 2`
```
# inputs:
# x4: 0
# first possible outputs:
# x1: 0
# x2: 0
# x3: 0
# second possible outputs:
# y1: 1
# y2: 0
# y3: 1
# other bindings:
# one: 1
# p: 21888242871839275222246405745257275088548364400416034343698204186575808495617
# ps1: 21888242871839275222246405745257275088548364400416034343698204186575808495616
# ps2: 21888242871839275222246405745257275088548364400416034343698204186575808495615
# ps3: 21888242871839275222246405745257275088548364400416034343698204186575808495614
# ps4: 21888242871839275222246405745257275088548364400416034343698204186575808495613
# ps5: 21888242871839275222246405745257275088548364400416034343698204186575808495612
# zero: 0
```
