-
Notifications
You must be signed in to change notification settings - Fork 39
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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 commutative diagram. C ───── degree-lowering ────> C || k ╷ ╷ subtract │ subtract │ fixed │ fixed │ output │ output │ │ │ v v C* ─── degree-lowering ────> C* || k The point of this elaboration is that in this particular case, testing completeness and soundness require the same code path. If `input` and `input || some_expr(input)` work for circuits before and after degree lowering, this fact establishes both completeness and soundness simultaneously.
- Loading branch information
Showing
10 changed files
with
777 additions
and
61 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
# Triton VM AIR | ||
|
||
This crate is part of the [Triton VM](https://triton-vm.org) ecosystem. It contains the definition | ||
of the AIR constraints, which are part of the STARK proving system. | ||
of the AIR constraints, which are part of the STARK proving system, before degree lowering. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,91 @@ | ||
use constraint_circuit::ConstraintCircuitMonad; | ||
use divan::black_box; | ||
use triton_constraint_builder::Constraints; | ||
|
||
fn main() { | ||
divan::main(); | ||
} | ||
|
||
#[divan::bench(sample_count = 10)] | ||
fn assemble_constraints() { | ||
black_box(Constraints::all()); | ||
} | ||
|
||
#[divan::bench(sample_count = 10)] | ||
fn initial_constraints(bencher: divan::Bencher) { | ||
bencher | ||
.with_inputs(|| { | ||
let degree_lowering_info = Constraints::default_degree_lowering_info(); | ||
let constraints = Constraints::initial_constraints(); | ||
(degree_lowering_info, constraints) | ||
}) | ||
.bench_values(|(degree_lowering_info, mut constraints)| { | ||
black_box(ConstraintCircuitMonad::lower_to_degree( | ||
&mut constraints, | ||
degree_lowering_info, | ||
)); | ||
}); | ||
} | ||
|
||
#[divan::bench(sample_count = 10)] | ||
fn consistency_constraints(bencher: divan::Bencher) { | ||
bencher | ||
.with_inputs(|| { | ||
let degree_lowering_info = Constraints::default_degree_lowering_info(); | ||
let constraints = Constraints::consistency_constraints(); | ||
(degree_lowering_info, constraints) | ||
}) | ||
.bench_values(|(degree_lowering_info, mut constraints)| { | ||
black_box(ConstraintCircuitMonad::lower_to_degree( | ||
&mut constraints, | ||
degree_lowering_info, | ||
)); | ||
}); | ||
} | ||
|
||
#[divan::bench(sample_count = 1)] | ||
fn transition_constraints(bencher: divan::Bencher) { | ||
bencher | ||
.with_inputs(|| { | ||
let degree_lowering_info = Constraints::default_degree_lowering_info(); | ||
let constraints = Constraints::transition_constraints(); | ||
(degree_lowering_info, constraints) | ||
}) | ||
.bench_values(|(degree_lowering_info, mut constraints)| { | ||
black_box(ConstraintCircuitMonad::lower_to_degree( | ||
&mut constraints, | ||
degree_lowering_info, | ||
)); | ||
}); | ||
} | ||
|
||
#[divan::bench(sample_count = 10)] | ||
fn terminal_constraints(bencher: divan::Bencher) { | ||
bencher | ||
.with_inputs(|| { | ||
let degree_lowering_info = Constraints::default_degree_lowering_info(); | ||
let constraints = Constraints::terminal_constraints(); | ||
(degree_lowering_info, constraints) | ||
}) | ||
.bench_values(|(degree_lowering_info, mut constraints)| { | ||
black_box(ConstraintCircuitMonad::lower_to_degree( | ||
&mut constraints, | ||
degree_lowering_info, | ||
)); | ||
}); | ||
} | ||
|
||
#[divan::bench(sample_count = 1)] | ||
fn degree_lower_all(bencher: divan::Bencher) { | ||
bencher | ||
.with_inputs(|| { | ||
let constraints = Constraints::all(); | ||
let degree_lowering_info = Constraints::default_degree_lowering_info(); | ||
(degree_lowering_info, constraints) | ||
}) | ||
.bench_values(|(degree_lowering_info, mut constraints)| { | ||
black_box( | ||
constraints.lower_to_target_degree_through_substitutions(degree_lowering_info), | ||
); | ||
}); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.