TritonVM / triton-vm / 11037850665

98%

Build Type

push

github

Committed by jan-ferdinand

Commit Message

test: Correctness & soundness of degree lowering

Test the completeness and soundness of the `apply_substitution`
function, which substitutes a single node during degree lowering.

In this context, completeness means: “given a satisfying assignment to
the circuit before degree lowering, one can derive a satisfying
assignment to the circuit after degree lowering.” Soundness means the
converse.

These features are tested using random input vectors. Naturally, the
output is not the zero vector (with high probability) and so the given
input is *not* a satisfying assignment (with high probability).
However, the circuit can be extended by way of thought experiment into
one that subtracts a fixed constant from the original output. For the
right choice of subtrahend, the random input now *is* a satisfying
assignment to the circuit.

Specifically, let `input` denote the original (before degree lowering)
input, and `C` the circuit. Then `input` is a satisfying input for the
new circuit `C'(X) = C(X) - C(input)`.

After applying a substitution to obtain circuit `C || k` from `C`, where
`k = Z - some_expr(X)` and `Z` is the introduced variable, the length
of the input and output increases by 1. Moreover, if `input` is a
satisfying input to `C'` then `input || some_expr(input)` is* a
satisfying input to `C' || k`.

(*: If the transformation is complete.)

To establish the converse, we want to start from a satisfying input to
`C" || k` and reduce it to a satisfying input to `C"`. The requirement,
implied by "satisfying input", that `k(X || Z) == 0` implies `Z ==
some_expr(X)`. Therefore, in order to sample a random satisfying input
to `C" || k`, it suffices to select `input` at random, define `C"(X) =
C(X) - C(input)`, and evaluate `some_expr(input)`. Then `input ||
some_expr(input)` is a random satisfying input to `C" || k`. It
follows** that `input` is a satisfying input to `C"`.

(**: If the transformation is sound.)

This description makes use of the following ... (continued)

Run Details

335 of 349 new or added lines in 3 files covered. (95.99%)

12 existing lines in 2 files now uncovered.

23974 of 24359 relevant lines covered (98.42%)

6164037.92 hits per line