diff --git a/Cargo.lock b/Cargo.lock index da80823..4809964 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -188,6 +188,9 @@ dependencies = [ [[package]] name = "brainfuck_prover" version = "0.1.0" +dependencies = [ + "stwo-prover", +] [[package]] name = "brainfuck_vm" diff --git a/crates/brainfuck_prover/Cargo.toml b/crates/brainfuck_prover/Cargo.toml index 2a2f634..ce63d6a 100644 --- a/crates/brainfuck_prover/Cargo.toml +++ b/crates/brainfuck_prover/Cargo.toml @@ -9,3 +9,4 @@ description.workspace = true workspace = true [dependencies] +stwo-prover.workspace = true diff --git a/crates/brainfuck_prover/src/main.rs b/crates/brainfuck_prover/src/bin/brainfuck_prover.rs similarity index 100% rename from crates/brainfuck_prover/src/main.rs rename to crates/brainfuck_prover/src/bin/brainfuck_prover.rs diff --git a/crates/brainfuck_prover/src/brainfuck_air/mod.rs b/crates/brainfuck_prover/src/brainfuck_air/mod.rs new file mode 100644 index 0000000..5ab3fcb --- /dev/null +++ b/crates/brainfuck_prover/src/brainfuck_air/mod.rs @@ -0,0 +1,207 @@ +use stwo_prover::core::{ + air::{Component, ComponentProver}, + backend::simd::SimdBackend, + channel::{Blake2sChannel, Channel}, + pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig, TreeVec}, + poly::circle::{CanonicCoset, PolyOps}, + prover::{self, verify, ProvingError, StarkProof, VerificationError}, + vcs::{ + blake2_merkle::{Blake2sMerkleChannel, Blake2sMerkleHasher}, + ops::MerkleHasher, + }, +}; + +/// The STARK proof of the execution of a given Brainfuck program. +/// +/// It includes the proof as well as the claims during the various phases of the proof generation. +pub struct BrainfuckProof { + pub claim: BrainfuckClaim, + pub interaction_claim: BrainfuckInteractionClaim, + pub proof: StarkProof, +} + +/// All the claims from the first phase (interaction phase 0). +/// +/// It includes the common claim values such as the initial and final states +/// and the claim of each component. +pub struct BrainfuckClaim; + +impl BrainfuckClaim { + pub fn mix_into(&self, _channel: &mut impl Channel) { + todo!(); + } + + pub fn log_sizes(&self) -> TreeVec> { + todo!(); + } +} + +/// All the interaction elements (drawn from the channel) +/// required by the various components during the interaction phase. +pub struct BrainfuckInteractionElements; + +impl BrainfuckInteractionElements { + pub fn draw(_channel: &mut impl Channel) -> Self { + todo!(); + } +} + +/// All the claims from the second phase (interaction phase 1). +/// +/// Mainly the claims on global relations (lookup, permutation, evaluation). +pub struct BrainfuckInteractionClaim; + +impl BrainfuckInteractionClaim { + pub fn mix_into(&self, _channel: &mut impl Channel) { + todo!(); + } +} + +/// Verify that the claims (i.e. Statement) are valid. +pub fn lookup_sum_valid( + _claim: &BrainfuckClaim, + _interaction_elements: &BrainfuckInteractionElements, + _interaction_claim: &BrainfuckInteractionClaim, +) -> bool { + todo!(); +} + +/// All the components that constitute the Brainfuck ZK-VM. +/// +/// Components are used by the prover as a `ComponentProver`, +/// and by the verifier as a `Component`. +pub struct BrainfuckComponents; + +impl BrainfuckComponents { + /// Initializes all the Brainfuck components from the claims generated from the trace. + pub fn new( + _claim: &BrainfuckClaim, + _interaction_elements: &BrainfuckInteractionElements, + _interaction_claim: &BrainfuckInteractionClaim, + ) -> Self { + todo!(); + } + + /// Returns the `ComponentProver` of each components, used by the prover. + pub fn provers(&self) -> Vec<&dyn ComponentProver> { + todo!(); + } + + /// Returns the `Component` of each components, used by the verifier. + pub fn components(&self) -> Vec<&dyn Component> { + todo!(); + } +} + +/// `LOG_MAX_ROWS = log2(MAX_ROWS)` ? +/// +/// Means that the ZK-VM does not accept programs with more than 2^20 steps (1M steps). +const LOG_MAX_ROWS: u32 = 20; + +pub fn prove_brainfuck() -> Result, ProvingError> { + // ┌──────────────────────────┐ + // │ Protocol Setup │ + // └──────────────────────────┘ + + let config = PcsConfig::default(); + let twiddles = SimdBackend::precompute_twiddles( + CanonicCoset::new(LOG_MAX_ROWS + config.fri_config.log_blowup_factor + 2) + .circle_domain() + .half_coset, + ); + let channel = &mut Blake2sChannel::default(); + let commitment_scheme = + &mut CommitmentSchemeProver::<_, Blake2sMerkleChannel>::new(config, &twiddles); + let tree_builder = commitment_scheme.tree_builder(); + + // ┌──────────────────────────┐ + // │ Interaction Phase 0 │ + // └──────────────────────────┘ + + // Generate BrainfuckClaim (from the execution trace provided by brainfuck_vm) + + // Commit to the claim and the trace. + let claim = BrainfuckClaim {}; + claim.mix_into(channel); + tree_builder.commit(channel); + + // ┌──────────────────────────┐ + // │ Interaction Phase 1 │ + // └──────────────────────────┘ + + // Draw interaction elements + let interaction_elements = BrainfuckInteractionElements::draw(channel); + + // Generate the interaction trace and the BrainfuckInteractionClaim + let tree_builder = commitment_scheme.tree_builder(); + + let interaction_claim = BrainfuckInteractionClaim {}; + interaction_claim.mix_into(channel); + tree_builder.commit(channel); + + // ┌──────────────────────────┐ + // │ Interaction Phase 2 │ + // └──────────────────────────┘ + + // Generate constant columns (e.g. is_first) + let tree_builder = commitment_scheme.tree_builder(); + tree_builder.commit(channel); + + // ┌──────────────────────────┐ + // │ Proof Generation │ + // └──────────────────────────┘ + let component_builder = + BrainfuckComponents::new(&claim, &interaction_elements, &interaction_claim); + let components = component_builder.provers(); + let _proof = prover::prove::(&components, channel, commitment_scheme)?; + + // Ok(BrainfuckProof { claim, interaction_claim, proof }) + todo!(); +} + +/// Verify a given STARK proof of a Brainfuck program execution with corresponding claim. +pub fn verify_brainfuck( + BrainfuckProof { claim, interaction_claim, proof }: BrainfuckProof, +) -> Result<(), VerificationError> { + // ┌──────────────────────────┐ + // │ Protocol Setup │ + // └──────────────────────────┘ + let config = PcsConfig::default(); + let channel = &mut Blake2sChannel::default(); + let commitment_scheme_verifier = + &mut CommitmentSchemeVerifier::::new(config); + let sizes = &claim.log_sizes(); + + // ┌──────────────────────────┐ + // │ Interaction Phase 0 │ + // └──────────────────────────┘ + claim.mix_into(channel); + commitment_scheme_verifier.commit(proof.commitments[0], &sizes[0], channel); + + // ┌──────────────────────────┐ + // │ Interaction Phase 1 │ + // └──────────────────────────┘ + let interaction_elements = BrainfuckInteractionElements::draw(channel); + // Check that the lookup sum is valid, otherwise throw + // TODO: panic! should be replaced by custom error + if !lookup_sum_valid(&claim, &interaction_elements, &interaction_claim) { + return Err(VerificationError::InvalidLookup("Invalid logup sum".to_string())); + }; + interaction_claim.mix_into(channel); + commitment_scheme_verifier.commit(proof.commitments[1], &sizes[1], channel); + + // ┌──────────────────────────┐ + // │ Interaction Phase 2 │ + // └──────────────────────────┘ + commitment_scheme_verifier.commit(proof.commitments[2], &sizes[2], channel); + + // ┌──────────────────────────┐ + // │ Proof Verification │ + // └──────────────────────────┘ + + let component_builder = + BrainfuckComponents::new(&claim, &interaction_elements, &interaction_claim); + let components = component_builder.components(); + + verify(&components, channel, commitment_scheme_verifier, proof) +} diff --git a/crates/brainfuck_prover/src/components/mod.rs b/crates/brainfuck_prover/src/components/mod.rs new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/crates/brainfuck_prover/src/components/mod.rs @@ -0,0 +1 @@ + diff --git a/crates/brainfuck_prover/src/lib.rs b/crates/brainfuck_prover/src/lib.rs new file mode 100644 index 0000000..8913003 --- /dev/null +++ b/crates/brainfuck_prover/src/lib.rs @@ -0,0 +1,2 @@ +pub mod brainfuck_air; +pub mod components;