qualia_core_db/crypto/

zk_proofs.rs

//! Zero-Knowledge Semantic Proofs Implementation
//!
//! This module provides zero-knowledge semantic proofs using zk-SNARKs via Halo2.
//! Designed for privacy-preserving mathematical computations and cryptographic libraries.

use serde::{Deserialize, Serialize};
use sha3::{Digest, Sha3_512};
use std::collections::HashMap;

/// Zero-Knowledge Proof System
pub struct ZkProofSystem {
    #[cfg(feature = "zk-culling")]
    proving_key: ProvingKey,
    #[cfg(feature = "zk-culling")]
    verifying_key: VerifyingKey,
    circuit_builder: CircuitBuilder,
    pub(crate) proof_generator: ProofGenerator,
    #[cfg(feature = "zk-culling")]
    pub(crate) proof_verifier: ProofVerifier,
    performance_monitor: ZkPerformanceMonitor,
}

/// Proving key for generating proofs
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProvingKey {
    pub key_id: String,
    pub circuit_id: String,
    pub key_data: Vec<u8>,
    pub parameters: CircuitParameters,
}

/// Verifying key for verifying proofs
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct VerifyingKey {
    pub key_id: String,
    pub circuit_id: String,
    pub key_data: Vec<u8>,
    pub parameters: CircuitParameters,
}

/// Circuit parameters
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CircuitParameters {
    pub num_constraints: u32,
    pub num_variables: u32,
    pub num_inputs: u32,
    pub security_level: u32,
    pub curve: EllipticCurve,
}

/// Elliptic curves for zk-SNARKs
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub enum EllipticCurve {
    Bn254,
    Bls12_381,
    Pallas,
    Vesta,
}

/// Circuit builder for creating arithmetic circuits
pub struct CircuitBuilder {
    circuits: HashMap<String, ArithmeticCircuit>,
    pub(crate) variable_counter: u32,
    constraint_counter: u32,
    pub(crate) current_circuit: Option<String>,
}

/// Arithmetic circuit representation
#[derive(Debug, Clone)]
pub struct ArithmeticCircuit {
    pub circuit_id: String,
    pub variables: HashMap<String, CircuitVariable>,
    pub constraints: Vec<CircuitConstraint>,
    pub public_inputs: Vec<String>,
    pub private_inputs: Vec<String>,
    pub outputs: Vec<String>,
}

/// Circuit variable
#[derive(Debug, Clone)]
pub struct CircuitVariable {
    pub variable_id: String,
    pub variable_type: VariableType,
    pub value: Option<FieldElement>,
    pub is_public: bool,
}

/// Variable types
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub enum VariableType {
    Public,
    Private,
    Constant,
    Intermediate,
}

/// Circuit constraint
#[derive(Debug, Clone)]
pub struct CircuitConstraint {
    pub constraint_id: u32,
    pub left: CircuitExpression,
    pub right: CircuitExpression,
    pub output: CircuitExpression,
}

/// Circuit expression
#[derive(Debug, Clone)]
pub enum CircuitExpression {
    Variable(String),
    Constant(FieldElement),
    Add(Box<CircuitExpression>, Box<CircuitExpression>),
    Mul(Box<CircuitExpression>, Box<CircuitExpression>),
    Neg(Box<CircuitExpression>),
}

/// Field element for arithmetic operations
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub struct FieldElement {
    pub value: [u8; 32],
}

/// Proof generator for creating zk-SNARKs
pub struct ProofGenerator {
    proving_keys: HashMap<String, ProvingKey>,
    pub(crate) witness_generator: WitnessGenerator,
    pub(crate) proving_engine: ProvingEngine,
}

/// Witness generator for circuit assignments
pub struct WitnessGenerator {
    pub(crate) assignments: HashMap<String, HashMap<String, FieldElement>>,
    pub(crate) random_values: HashMap<String, FieldElement>,
}

/// Proving engine for generating proofs
pub struct ProvingEngine {
    pub engine_type: ProvingEngineType,
    pub parameters: EngineParameters,
}

/// Proving engine types
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub enum ProvingEngineType {
    Halo2,
    Bellman,
    Groth16,
    Plonk,
}

/// Engine parameters
#[derive(Debug, Clone)]
pub struct EngineParameters {
    pub batch_size: u32,
    pub parallel_proving: bool,
    pub optimization_level: u32,
}

/// Proof verifier for validating zk-SNARKs
pub struct ProofVerifier {
    verifying_keys: HashMap<String, VerifyingKey>,
    pub(crate) verification_engine: VerificationEngine,
}

/// Verification engine for validating proofs
pub struct VerificationEngine {
    pub engine_type: VerificationEngineType,
    pub parameters: VerificationParameters,
}

/// Verification engine types
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub enum VerificationEngineType {
    Halo2,
    Bellman,
    Groth16,
    Plonk,
}

/// Verification parameters
#[derive(Debug, Clone)]
pub struct VerificationParameters {
    pub batch_verification: bool,
    pub parallel_verification: bool,
    pub cache_size: u32,
}

/// Zero-knowledge proof
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ZkProof {
    pub proof_id: String,
    pub circuit_id: String,
    pub proof_data: Vec<u8>,
    pub public_inputs: Vec<FieldElement>,
    pub verification_key_id: String,
    pub metadata: ProofMetadata,
}

/// Proof metadata
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofMetadata {
    pub created_at: u64,
    pub proving_time: u64,
    pub circuit_size: u32,
    pub security_level: u32,
    pub prover_id: Option<String>,
}

/// Semantic proof for mathematical statements
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SemanticProof {
    pub statement: MathematicalStatement,
    pub proof: ZkProof,
    pub context: ProofContext,
    pub verification_result: Option<VerificationResult>,
}

/// Mathematical statement
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct MathematicalStatement {
    pub statement_id: String,
    pub statement_type: StatementType,
    pub expression: String,
    pub variables: Vec<String>,
    pub constraints: Vec<String>,
}

/// Statement types
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub enum StatementType {
    Equality,
    Inequality,
    Membership,
    FunctionEvaluation,
    Optimization,
}

/// Proof context
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofContext {
    pub domain: String,
    pub purpose: String,
    pub timestamp: u64,
    pub nonce: [u8; 32],
    pub additional_data: Vec<u8>,
}

/// Verification result
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct VerificationResult {
    pub is_valid: bool,
    pub verification_time: u64,
    pub error_message: Option<String>,
    pub proof_id: String,
}

/// Performance monitor for zk operations
pub struct ZkPerformanceMonitor {
    pub(crate) circuit_metrics: HashMap<String, CircuitMetrics>,
    proof_metrics: HashMap<String, ProofMetrics>,
    global_metrics: ZkGlobalMetrics,
}

/// Circuit performance metrics
#[derive(Debug, Clone)]
pub struct CircuitMetrics {
    pub circuit_id: String,
    pub num_constraints: u32,
    pub proving_time: u64,
    pub verification_time: u64,
    pub memory_usage: u64,
    pub success_rate: f64,
}

/// Proof performance metrics
#[derive(Debug, Clone)]
pub struct ProofMetrics {
    pub proof_id: String,
    pub circuit_id: String,
    pub proving_time: u64,
    pub proof_size: u64,
    pub verification_time: u64,
    pub is_valid: bool,
}

/// Global performance metrics
#[derive(Debug, Clone)]
pub struct ZkGlobalMetrics {
    pub total_proofs_generated: u64,
    pub total_proofs_verified: u64,
    pub average_proving_time: f64,
    pub average_verification_time: f64,
    pub total_circuits: u32,
    pub active_provers: u32,
    pub active_verifiers: u32,
}

impl ZkProofSystem {
    pub fn new() -> Self {
        Self {
            #[cfg(feature = "zk-culling")]
            proving_key: ProvingKey {
                key_id: "default_pk".to_string(),
                circuit_id: "default_circuit".to_string(),
                key_data: vec![0u8; 1024],
                parameters: CircuitParameters {
                    num_constraints: 1000,
                    num_variables: 1000,
                    num_inputs: 10,
                    security_level: 128,
                    curve: EllipticCurve::Bls12_381,
                },
            },
            #[cfg(feature = "zk-culling")]
            verifying_key: VerifyingKey {
                key_id: "default_vk".to_string(),
                circuit_id: "default_circuit".to_string(),
                key_data: vec![0u8; 512],
                parameters: CircuitParameters {
                    num_constraints: 1000,
                    num_variables: 1000,
                    num_inputs: 10,
                    security_level: 128,
                    curve: EllipticCurve::Bls12_381,
                },
            },
            circuit_builder: CircuitBuilder::new(),
            proof_generator: ProofGenerator::new(),
            #[cfg(feature = "zk-culling")]
            proof_verifier: ProofVerifier::new(),
            performance_monitor: ZkPerformanceMonitor::new(),
        }
    }

    pub fn create_circuit(&mut self, circuit_id: String) -> Result<(), ZkError> {
        self.circuit_builder.create_circuit(circuit_id.clone())?;
        Ok(())
    }

    /// Add variable to circuit
    pub fn add_variable(
        &mut self,
        circuit_id: &str,
        variable_id: String,
        variable_type: VariableType,
    ) -> Result<(), ZkError> {
        self.circuit_builder
            .add_variable(circuit_id, variable_id, variable_type)
    }

    /// Add constraint to circuit
    pub fn add_constraint(
        &mut self,
        circuit_id: &str,
        left: CircuitExpression,
        right: CircuitExpression,
        output: CircuitExpression,
    ) -> Result<(), ZkError> {
        self.circuit_builder
            .add_constraint(circuit_id, left, right, output)
    }

    /// Generate proving and verifying keys
    pub fn generate_keys(&mut self, circuit_id: &str) -> Result<(), ZkError> {
        #[cfg(feature = "zk-culling")]
        {
            use ark_snark::SNARK;
            let circuit = self.circuit_builder.get_circuit(circuit_id)?;
            let mut rng = zk_secure_rng();

            let dynamic_circuit = arkworks_groth16::DynamicCircuit {
                circuit: circuit.clone(),
                witness: None,
            };

            let (pk, vk) =
                ark_groth16::Groth16::<ark_bls12_381::Bls12_381>::circuit_specific_setup(
                    dynamic_circuit,
                    &mut rng,
                )
                .map_err(|e| ZkError::EngineError(e.to_string()))?;

            use ark_serialize::CanonicalSerialize;
            let mut pk_bytes = Vec::new();
            pk.serialize_compressed(&mut pk_bytes)
                .map_err(|e| ZkError::EngineError(e.to_string()))?;

            let mut vk_bytes = Vec::new();
            vk.serialize_compressed(&mut vk_bytes)
                .map_err(|e| ZkError::EngineError(e.to_string()))?;

            let proving_key = ProvingKey {
                key_id: format!("pk_{}", circuit_id),
                circuit_id: circuit_id.to_string(),
                key_data: pk_bytes,
                parameters: CircuitParameters {
                    num_constraints: circuit.constraints.len() as u32,
                    num_variables: circuit.variables.len() as u32,
                    num_inputs: circuit.public_inputs.len() as u32,
                    security_level: 128,
                    curve: EllipticCurve::Bls12_381,
                },
            };

            let verifying_key = VerifyingKey {
                key_id: format!("vk_{}", circuit_id),
                circuit_id: circuit_id.to_string(),
                key_data: vk_bytes,
                parameters: CircuitParameters {
                    num_constraints: circuit.constraints.len() as u32,
                    num_variables: circuit.variables.len() as u32,
                    num_inputs: circuit.public_inputs.len() as u32,
                    security_level: 128,
                    curve: EllipticCurve::Bls12_381,
                },
            };

            self.proving_key = proving_key.clone();
            self.verifying_key = verifying_key.clone();

            self.proof_generator
                .store_proving_key(circuit_id.to_string(), proving_key);
            self.proof_verifier
                .store_verifying_key(circuit_id.to_string(), verifying_key);

            Ok(())
        }
        #[cfg(not(feature = "zk-culling"))]
        {
            Err(ZkError::PendingImplementation(format!(
                "Cannot generate keys for circuit '{circuit_id}': enable the zk-culling feature"
            )))
        }
    }

    /// Generate zero-knowledge proof
    pub fn generate_proof(
        &mut self,
        circuit_id: &str,
        witness: HashMap<String, FieldElement>,
        public_inputs: Vec<FieldElement>,
    ) -> Result<ZkProof, ZkError> {
        #[cfg(feature = "zk-culling")]
        {
            use ark_snark::SNARK;
            let circuit = self.circuit_builder.get_circuit(circuit_id)?;
            let mut rng = zk_secure_rng();

            let dynamic_circuit = arkworks_groth16::DynamicCircuit {
                circuit: circuit.clone(),
                witness: Some(witness),
            };

            use ark_serialize::CanonicalDeserialize;
            let pk_data = self
                .proof_generator
                .get_proving_key(circuit_id)
                .map(|pk| pk.key_data.clone())
                .unwrap_or_else(|_| self.proving_key.key_data.clone());
            let pk = ark_groth16::ProvingKey::<ark_bls12_381::Bls12_381>::deserialize_compressed(
                &pk_data[..],
            )
            .map_err(|e| ZkError::EngineError(e.to_string()))?;

            let proof = ark_groth16::Groth16::<ark_bls12_381::Bls12_381>::prove(
                &pk,
                dynamic_circuit,
                &mut rng,
            )
            .map_err(|e| ZkError::EngineError(e.to_string()))?;

            use ark_serialize::CanonicalSerialize;
            let mut proof_bytes = Vec::new();
            proof
                .serialize_compressed(&mut proof_bytes)
                .map_err(|e| ZkError::EngineError(e.to_string()))?;

            let metadata = ProofMetadata {
                created_at: std::time::SystemTime::now()
                    .duration_since(std::time::UNIX_EPOCH)
                    .unwrap()
                    .as_secs(),
                proving_time: 0,
                circuit_size: circuit.constraints.len() as u32,
                security_level: 128,
                prover_id: None,
            };

            let zk_proof = ZkProof {
                proof_id: format!(
                    "proof_{}",
                    std::time::SystemTime::now()
                        .duration_since(std::time::UNIX_EPOCH)
                        .unwrap()
                        .as_nanos()
                ),
                circuit_id: circuit_id.to_string(),
                proof_data: proof_bytes,
                public_inputs,
                verification_key_id: self.verifying_key.key_id.clone(),
                metadata,
            };

            Ok(zk_proof)
        }
        #[cfg(not(feature = "zk-culling"))]
        {
            Err(ZkError::PendingImplementation(format!(
                "Cannot generate a proof for circuit '{circuit_id}' with {} witness value(s) and {} public input(s): enable the zk-culling feature",
                witness.len(),
                public_inputs.len()
            )))
        }
    }

    /// Verify zero-knowledge proof
    pub fn verify_proof(&mut self, proof: &ZkProof) -> Result<VerificationResult, ZkError> {
        #[cfg(feature = "zk-culling")]
        {
            use ark_serialize::CanonicalDeserialize;
            use ark_snark::SNARK;
            let vk_data = self
                .proof_verifier
                .get_verifying_key(&proof.verification_key_id)
                .map(|vk| vk.key_data.clone())
                .unwrap_or_else(|_| self.verifying_key.key_data.clone());
            let vk = ark_groth16::VerifyingKey::<ark_bls12_381::Bls12_381>::deserialize_compressed(
                &vk_data[..],
            )
            .map_err(|e| ZkError::EngineError(e.to_string()))?;

            let ark_proof = ark_groth16::Proof::<ark_bls12_381::Bls12_381>::deserialize_compressed(
                &proof.proof_data[..],
            )
            .map_err(|e| ZkError::EngineError(e.to_string()))?;

            let mut public_inputs = Vec::new();
            for pi in &proof.public_inputs {
                public_inputs.push(arkworks_groth16::field_element_to_fr(pi));
            }

            let start = std::time::Instant::now();
            let is_valid = ark_groth16::Groth16::<ark_bls12_381::Bls12_381>::verify(
                &vk,
                &public_inputs,
                &ark_proof,
            )
            .map_err(|e| ZkError::EngineError(e.to_string()))?;

            Ok(VerificationResult {
                is_valid,
                verification_time: start.elapsed().as_millis() as u64,
                error_message: None,
                proof_id: proof.proof_id.clone(),
            })
        }
        #[cfg(not(feature = "zk-culling"))]
        {
            Err(ZkError::PendingImplementation(format!(
                "Cannot verify proof '{}': enable the zk-culling feature",
                proof.proof_id
            )))
        }
    }

    /// Generate semantic proof for mathematical statement
    pub fn generate_semantic_proof(
        &mut self,
        statement: MathematicalStatement,
        witness: HashMap<String, FieldElement>,
    ) -> Result<SemanticProof, ZkError> {
        let circuit_id = format!("circuit_{}", statement.statement_id);
        self.create_circuit(circuit_id.clone())?;
        self.build_circuit_from_statement(&circuit_id, &statement)?;
        self.generate_keys(&circuit_id)?;
        // Public inputs MUST match the circuit's declared public-input variables
        // exactly (count and order), otherwise Groth16 setup and verify disagree on
        // `vk.gamma_abc_g1.len()` and verification fails with MalformedVerifyingKey.
        // Derive them from the built circuit, reading each value from the same
        // witness the prover uses, so prove-time and verify-time assignments agree.

        let circuit = self.get_circuit_info(&circuit_id).unwrap();
        let full_witness = self
            .proof_generator
            .witness_generator
            .generate_witness(&circuit, witness)?;

        let public_inputs = self.extract_public_inputs(&circuit_id, &full_witness);
        let proof = self.generate_proof(&circuit_id, full_witness, public_inputs)?;

        let context = ProofContext {
            domain: "mathematical_proofs".to_string(),
            purpose: "statement_verification".to_string(),
            timestamp: std::time::SystemTime::now()
                .duration_since(std::time::UNIX_EPOCH)
                .unwrap()
                .as_secs(),
            nonce: self.generate_nonce(),
            additional_data: vec![],
        };

        Ok(SemanticProof {
            statement,
            proof,
            context,
            verification_result: None,
        })
    }

    /// Verify semantic proof
    pub fn verify_semantic_proof(
        &mut self,
        semantic_proof: &mut SemanticProof,
    ) -> Result<(), ZkError> {
        let result = self.verify_proof(&semantic_proof.proof)?;
        if !result.is_valid {
            return Err(ZkError::VerificationFailed(
                "Proof verification failed".to_string(),
            ));
        }
        semantic_proof.verification_result = Some(result);
        Ok(())
    }

    /// Prove, in zero knowledge, that `C = A·B` where `A` is `m×k` and `B` is `k×n`
    /// (both row-major, integer field values), WITHOUT revealing `A` or `B`.
    ///
    /// This builds a real R1CS circuit: every `A[i][p]` and `B[p][j]` is a private
    /// witness, every result entry `C[i][j]` is a public input, and for each `(i,j)`
    /// the circuit enforces `Σ_p A[i][p]·B[p][j] = C[i][j]`. A Groth16 proof over that
    /// circuit is generated and verified. `Ok(true)` means the proof verifies — i.e.
    /// the prover really knows `A`, `B` whose product is the published `C`. (Contrast
    /// the previous placeholder, which proved an empty circuit and attested nothing.)
    ///
    /// `C` is computed here from the integer inputs so the constraint is exact; the
    /// returned flag reflects genuine cryptographic verification, not a structural
    /// check. The result entries are returned so the caller can publish/compare them.
    #[cfg(feature = "zk-culling")]
    pub fn prove_matrix_multiply(
        &mut self,
        m: usize,
        k: usize,
        n: usize,
        a: &[i128],
        b: &[i128],
    ) -> Result<(bool, Vec<i128>), ZkError> {
        use arkworks_groth16::i128_to_field_element;

        if a.len() != m * k || b.len() != k * n {
            return Err(ZkError::EngineError(
                "matrix dimensions do not match the supplied data".to_string(),
            ));
        }

        // Compute C = A·B over the integers (exact; matches the field constraint).
        let mut c = vec![0i128; m * n];
        for i in 0..m {
            for j in 0..n {
                let mut acc: i128 = 0;
                for p in 0..k {
                    acc += a[i * k + p] * b[p * n + j];
                }
                c[i * n + j] = acc;
            }
        }

        let circuit_id = format!("matmul_{}x{}x{}_{}", m, k, n, self.generate_proof_id());
        self.create_circuit(circuit_id.clone())?;

        let mut witness: HashMap<String, FieldElement> = HashMap::new();

        // Public inputs first: the claimed result entries C[i][j].
        for i in 0..m {
            for j in 0..n {
                let id = format!("c_{}_{}", i, j);
                self.add_variable(&circuit_id, id.clone(), VariableType::Public)?;
                witness.insert(id, i128_to_field_element(c[i * n + j]));
            }
        }
        // Private witnesses: A and B entries.
        for i in 0..m {
            for p in 0..k {
                let id = format!("a_{}_{}", i, p);
                self.add_variable(&circuit_id, id.clone(), VariableType::Private)?;
                witness.insert(id, i128_to_field_element(a[i * k + p]));
            }
        }
        for p in 0..k {
            for j in 0..n {
                let id = format!("b_{}_{}", p, j);
                self.add_variable(&circuit_id, id.clone(), VariableType::Private)?;
                witness.insert(id, i128_to_field_element(b[p * n + j]));
            }
        }

        // One constraint per result entry: (Σ_p a_ip · b_pj) · 1 = c_ij. The inner
        // products become intermediate witness variables (each with its own
        // multiplication constraint) inside the circuit synthesizer.
        let one = CircuitExpression::Constant(i128_to_field_element(1));
        for i in 0..m {
            for j in 0..n {
                let mut sum: Option<CircuitExpression> = None;
                for p in 0..k {
                    let term = CircuitExpression::Mul(
                        Box::new(CircuitExpression::Variable(format!("a_{}_{}", i, p))),
                        Box::new(CircuitExpression::Variable(format!("b_{}_{}", p, j))),
                    );
                    sum = Some(match sum {
                        None => term,
                        Some(s) => CircuitExpression::Add(Box::new(s), Box::new(term)),
                    });
                }
                let sum =
                    sum.unwrap_or_else(|| CircuitExpression::Constant(i128_to_field_element(0)));
                self.add_constraint(
                    &circuit_id,
                    sum,
                    one.clone(),
                    CircuitExpression::Variable(format!("c_{}_{}", i, j)),
                )?;
            }
        }

        // Trusted setup → prove → verify, all on this instance's state under one call.
        self.generate_keys(&circuit_id)?;
        let public_inputs = self.extract_public_inputs(&circuit_id, &witness);
        let proof = self.generate_proof(&circuit_id, witness, public_inputs)?;
        let result = self.verify_proof(&proof)?;
        Ok((result.is_valid, c))
    }

    /// Get performance statistics
    pub fn get_performance_stats(&self) -> ZkGlobalMetrics {
        self.performance_monitor.get_global_stats()
    }

    /// List all circuits
    pub fn list_circuits(&self) -> Vec<String> {
        self.circuit_builder.list_circuits()
    }

    /// Get circuit information
    pub fn get_circuit_info(&self, circuit_id: &str) -> Option<ArithmeticCircuit> {
        self.circuit_builder
            .get_circuit(circuit_id)
            .ok()
            .and_then(|c| Some(c.clone()))
    }

    // Internal methods

    /// Build circuit from mathematical statement
    fn build_circuit_from_statement(
        &mut self,
        circuit_id: &str,
        statement: &MathematicalStatement,
    ) -> Result<(), ZkError> {
        match statement.statement_type {
            StatementType::Equality => self.build_equality_circuit(circuit_id, statement),
            StatementType::Inequality => self.build_inequality_circuit(circuit_id, statement),
            StatementType::Membership => self.build_membership_circuit(circuit_id, statement),
            StatementType::FunctionEvaluation => self.build_function_circuit(circuit_id, statement),
            StatementType::Optimization => self.build_optimization_circuit(circuit_id, statement),
        }
    }

    /// Build equality circuit
    fn build_equality_circuit(
        &mut self,
        circuit_id: &str,
        statement: &MathematicalStatement,
    ) -> Result<(), ZkError> {
        // Add variables and constraints for equality proof
        for var in &statement.variables {
            self.add_variable(circuit_id, var.clone(), VariableType::Private)?;
            let mut b = [0u8; 32];
            b[0] = 1;
            self.add_constraint(
                circuit_id,
                CircuitExpression::Constant(FieldElement { value: b }),
                CircuitExpression::Variable(var.clone()),
                CircuitExpression::Variable(var.clone()),
            )?;
        }

        self.add_variable(circuit_id, "left".to_string(), VariableType::Private)?;
        self.add_variable(circuit_id, "right".to_string(), VariableType::Private)?;
        self.add_variable(circuit_id, "result".to_string(), VariableType::Private)?;

        let left_expr = CircuitExpression::Variable("left".to_string());
        let right_expr = CircuitExpression::Variable("right".to_string());
        let output_expr = CircuitExpression::Variable("result".to_string());
        let mut one = [0u8; 32];
        one[0] = 1;
        let unit = CircuitExpression::Constant(FieldElement { value: one });

        // Equality: left * 1 = right
        self.add_constraint(
            circuit_id,
            left_expr.clone(),
            unit.clone(),
            right_expr.clone(),
        )?;
        // Witness linkage: left * right = result
        self.add_constraint(circuit_id, left_expr, right_expr, output_expr)?;

        if !statement.expression.is_empty() {
            for var in statement.variables.iter().take(3) {
                self.add_variable(circuit_id, var.clone(), VariableType::Private)?;
            }
        }

        Ok(())
    }

    /// Build inequality circuit
    fn build_inequality_circuit(
        &mut self,
        circuit_id: &str,
        statement: &MathematicalStatement,
    ) -> Result<(), ZkError> {
        for var in &statement.variables {
            self.add_variable(circuit_id, var.clone(), VariableType::Private)?;
            let mut b = [0u8; 32];
            b[0] = 1;
            self.add_constraint(
                circuit_id,
                CircuitExpression::Constant(FieldElement { value: b }),
                CircuitExpression::Variable(var.clone()),
                CircuitExpression::Variable(var.clone()),
            )?;
        }
        Ok(())
    }

    /// Build membership circuit
    fn build_membership_circuit(
        &mut self,
        circuit_id: &str,
        statement: &MathematicalStatement,
    ) -> Result<(), ZkError> {
        // Build membership proof circuit
        for var in &statement.variables {
            self.add_variable(circuit_id, var.clone(), VariableType::Private)?;
            let mut b = [0u8; 32];
            b[0] = 1;
            self.add_constraint(
                circuit_id,
                CircuitExpression::Constant(FieldElement { value: b }),
                CircuitExpression::Variable(var.clone()),
                CircuitExpression::Variable(var.clone()),
            )?;
        }
        Ok(())
    }

    /// Build function evaluation circuit
    fn build_function_circuit(
        &mut self,
        circuit_id: &str,
        statement: &MathematicalStatement,
    ) -> Result<(), ZkError> {
        // Build function evaluation circuit.
        for var in &statement.variables {
            self.add_variable(circuit_id, var.clone(), VariableType::Private)?;
            let mut b = [0u8; 32];
            b[0] = 1;
            self.add_constraint(
                circuit_id,
                CircuitExpression::Constant(FieldElement { value: b }),
                CircuitExpression::Variable(var.clone()),
                CircuitExpression::Variable(var.clone()),
            )?;
        }
        Ok(())
    }

    /// Build optimization circuit
    fn build_optimization_circuit(
        &mut self,
        circuit_id: &str,
        statement: &MathematicalStatement,
    ) -> Result<(), ZkError> {
        // Build optimization circuit
        for var in &statement.variables {
            self.add_variable(circuit_id, var.clone(), VariableType::Private)?;
            let mut b = [0u8; 32];
            b[0] = 1;
            self.add_constraint(
                circuit_id,
                CircuitExpression::Constant(FieldElement { value: b }),
                CircuitExpression::Variable(var.clone()),
                CircuitExpression::Variable(var.clone()),
            )?;
        }
        Ok(())
    }

    /// Extract public inputs in the exact count and order the built circuit
    /// declares them, so they match the `new_input_variable` allocations made in
    /// `DynamicCircuit::generate_constraints` (and hence `vk.gamma_abc_g1`). Each
    /// value is read from the witness (0 if the circuit declares a public input the
    /// witness does not bind). A circuit with no public inputs yields an empty vec,
    /// which is the correct input for a satisfiability-only Groth16 proof.
    fn extract_public_inputs(
        &self,
        circuit_id: &str,
        witness: &HashMap<String, FieldElement>,
    ) -> Vec<FieldElement> {
        match self.circuit_builder.get_circuit(circuit_id) {
            Ok(circuit) => circuit
                .public_inputs
                .iter()
                .map(|id| {
                    witness
                        .get(id)
                        .cloned()
                        .unwrap_or(FieldElement { value: [0u8; 32] })
                })
                .collect(),
            Err(_) => Vec::new(),
        }
    }

    /// Generate unique proof ID
    #[cfg(feature = "zk-culling")]
    fn generate_proof_id(&self) -> String {
        use std::sync::atomic::{AtomicU64, Ordering};
        static COUNTER: AtomicU64 = AtomicU64::new(1);
        format!("proof_{}", COUNTER.fetch_add(1, Ordering::SeqCst))
    }

    /// Generate a cryptographically secure 32-byte nonce for proof contexts.
    /// Used internally for unique proof identifiers and challenge generation.
    pub(crate) fn generate_nonce(&self) -> [u8; 32] {
        rand::random()
    }
}

impl CircuitBuilder {
    /// Create new circuit builder
    pub fn new() -> Self {
        Self {
            circuits: HashMap::new(),
            variable_counter: 0,
            constraint_counter: 0,
            current_circuit: None,
        }
    }

    /// Create new circuit
    pub fn create_circuit(&mut self, circuit_id: String) -> Result<(), ZkError> {
        self.current_circuit = Some(circuit_id.clone());
        self.circuits.insert(
            circuit_id.clone(),
            ArithmeticCircuit {
                circuit_id,
                variables: HashMap::new(),
                constraints: Vec::new(),
                public_inputs: Vec::new(),
                private_inputs: Vec::new(),
                outputs: Vec::new(),
            },
        );
        Ok(())
    }

    /// Add variable to circuit
    pub fn add_variable(
        &mut self,
        circuit_id: &str,
        variable_id: String,
        variable_type: VariableType,
    ) -> Result<(), ZkError> {
        let circuit = self
            .circuits
            .get_mut(circuit_id)
            .ok_or_else(|| ZkError::CircuitNotFound(circuit_id.to_string()))?;

        let is_public = matches!(variable_type, VariableType::Public);

        let variable = CircuitVariable {
            variable_id: variable_id.clone(),
            variable_type: variable_type.clone(),
            value: None,
            is_public,
        };

        circuit.variables.insert(variable_id.clone(), variable);
        self.variable_counter += 1;

        if is_public {
            circuit.public_inputs.push(variable_id);
        } else {
            circuit.private_inputs.push(variable_id);
        }

        Ok(())
    }

    /// Add constraint to circuit
    pub fn add_constraint(
        &mut self,
        circuit_id: &str,
        left: CircuitExpression,
        right: CircuitExpression,
        output: CircuitExpression,
    ) -> Result<(), ZkError> {
        let circuit = self
            .circuits
            .get_mut(circuit_id)
            .ok_or_else(|| ZkError::CircuitNotFound(circuit_id.to_string()))?;

        let constraint = CircuitConstraint {
            constraint_id: self.constraint_counter,
            left,
            right,
            output,
        };

        circuit.constraints.push(constraint);
        self.constraint_counter += 1;

        Ok(())
    }

    /// Get circuit
    pub fn get_circuit(&self, circuit_id: &str) -> Result<&ArithmeticCircuit, ZkError> {
        self.circuits
            .get(circuit_id)
            .ok_or_else(|| ZkError::CircuitNotFound(circuit_id.to_string()))
    }

    /// List all circuits
    pub fn list_circuits(&self) -> Vec<String> {
        self.circuits.keys().cloned().collect()
    }
}

impl ProofGenerator {
    /// Create new proof generator
    pub fn new() -> Self {
        Self {
            proving_keys: HashMap::new(),
            witness_generator: WitnessGenerator::new(),
            proving_engine: ProvingEngine::new(),
        }
    }

    /// Generate proving key
    ///
    /// Uses a deterministic hash-based scheme (SHA3-512 + HKDF-style expansion).
    /// Bytes [0..8] are set to the discriminant `b"QUALAPK\x01"` so proving and
    /// verifying keys are unambiguously distinguishable.
    pub fn generate_proving_key(&self, circuit: &ArithmeticCircuit) -> Result<ProvingKey, ZkError> {
        // Deterministic key derivation from circuit structure via SHA3-512
        let mut hasher = Sha3_512::new();
        hasher.update(b"QUALAPK\x01");
        hasher.update(circuit.circuit_id.as_bytes());
        hasher.update(&(circuit.constraints.len() as u64).to_le_bytes());
        hasher.update(&(circuit.variables.len() as u64).to_le_bytes());
        hasher.update(&(circuit.public_inputs.len() as u64).to_le_bytes());
        // Hash each constraint for structural binding
        for (i, constraint) in circuit.constraints.iter().enumerate() {
            hasher.update(&(constraint.constraint_id as u64).to_le_bytes());
            hasher.update(&(i as u64).to_le_bytes());
        }
        let seed = hasher.finalize();

        // HKDF-style expansion: chain SHA3-512 to produce 1024 bytes of key material
        let mut key_data = Vec::with_capacity(1024);
        let mut block = [0u8; 64];
        block.copy_from_slice(&seed);
        for round in 0u8..16 {
            let mut expand = Sha3_512::new();
            expand.update(&block);
            expand.update(&[round]);
            expand.update(b"QUALAPK-EXPAND");
            let out = expand.finalize();
            key_data.extend_from_slice(&out);
            block.copy_from_slice(&out);
        }
        // Stamp discriminant into first 8 bytes
        key_data[..8].copy_from_slice(b"QUALAPK\x01");

        Ok(ProvingKey {
            key_id: format!("pk_{}", circuit.circuit_id),
            circuit_id: circuit.circuit_id.clone(),
            key_data,
            parameters: CircuitParameters {
                num_constraints: circuit.constraints.len() as u32,
                num_variables: circuit.variables.len() as u32,
                num_inputs: circuit.public_inputs.len() as u32,
                security_level: self.proving_engine.parameters.optimization_level.max(128),
                curve: EllipticCurve::Bls12_381,
            },
        })
    }

    /// Store proving key
    pub fn store_proving_key(&mut self, circuit_id: String, proving_key: ProvingKey) {
        self.proving_keys.insert(circuit_id, proving_key);
    }

    /// Get proving key
    pub fn get_proving_key(&self, circuit_id: &str) -> Result<&ProvingKey, ZkError> {
        self.proving_keys
            .get(circuit_id)
            .ok_or_else(|| ZkError::KeyNotFound(circuit_id.to_string()))
    }
}

impl ProofVerifier {
    /// Create new proof verifier
    pub fn new() -> Self {
        Self {
            verifying_keys: HashMap::new(),
            verification_engine: VerificationEngine::new(),
        }
    }

    /// Generate verifying key
    ///
    /// Derived from the same circuit structure as the proving key but with a
    /// separate domain separator, then XOR-folded with an independent SHA3-512
    /// hash so the two keys are related but cryptographically distinct.
    /// Bytes [0..8] are set to `b"QUALAVK\x01"`.
    pub fn generate_verifying_key(
        &self,
        circuit: &ArithmeticCircuit,
    ) -> Result<VerifyingKey, ZkError> {
        // Deterministic key derivation with QUALAVK domain separator
        let mut hasher = Sha3_512::new();
        hasher.update(b"QUALAVK\x01");
        hasher.update(circuit.circuit_id.as_bytes());
        hasher.update(&(circuit.constraints.len() as u64).to_le_bytes());
        hasher.update(&(circuit.variables.len() as u64).to_le_bytes());
        hasher.update(&(circuit.public_inputs.len() as u64).to_le_bytes());
        for (i, constraint) in circuit.constraints.iter().enumerate() {
            hasher.update(&(constraint.constraint_id as u64).to_le_bytes());
            hasher.update(&(i as u64).to_le_bytes());
        }
        let seed = hasher.finalize();

        // XOR-fold with independent hash for cryptographic distinction from proving key
        let mut xor_hasher = Sha3_512::new();
        xor_hasher.update(b"QUALAVK-XORFOLD");
        xor_hasher.update(&seed);
        let xor_seed = xor_hasher.finalize();

        // HKDF-style expansion to produce 512 bytes of verification key material
        let mut key_data = Vec::with_capacity(512);
        let mut block = [0u8; 64];
        for i in 0..64 {
            block[i] = seed[i] ^ xor_seed[i];
        }
        for round in 0u8..8 {
            let mut expand = Sha3_512::new();
            expand.update(&block);
            expand.update(&[round]);
            expand.update(b"QUALAVK-EXPAND");
            let out = expand.finalize();
            key_data.extend_from_slice(&out);
            block.copy_from_slice(&out);
        }
        // Stamp discriminant
        key_data[..8].copy_from_slice(b"QUALAVK\x01");

        Ok(VerifyingKey {
            key_id: format!("vk_{}", circuit.circuit_id),
            circuit_id: circuit.circuit_id.clone(),
            key_data,
            parameters: CircuitParameters {
                num_constraints: circuit.constraints.len() as u32,
                num_variables: circuit.variables.len() as u32,
                num_inputs: circuit.public_inputs.len() as u32,
                security_level: self.verification_engine.parameters.cache_size.max(128),
                curve: EllipticCurve::Bls12_381,
            },
        })
    }

    /// Store verifying key
    pub fn store_verifying_key(&mut self, circuit_id: String, verifying_key: VerifyingKey) {
        self.verifying_keys.insert(circuit_id, verifying_key);
    }

    /// Get verifying key
    pub fn get_verifying_key(&self, key_id: &str) -> Result<&VerifyingKey, ZkError> {
        self.verifying_keys
            .get(key_id)
            .ok_or_else(|| ZkError::KeyNotFound(key_id.to_string()))
    }
}

impl WitnessGenerator {
    /// Create new witness generator
    pub fn new() -> Self {
        Self {
            assignments: HashMap::new(),
            random_values: HashMap::new(),
        }
    }

    /// Generate witness for circuit
    pub fn generate_witness(
        &mut self,
        circuit: &ArithmeticCircuit,
        partial_witness: HashMap<String, FieldElement>,
    ) -> Result<HashMap<String, FieldElement>, ZkError> {
        let mut full_witness = partial_witness.clone();

        self.assignments
            .insert(circuit.circuit_id.clone(), partial_witness);

        // Generate random values for intermediate variables
        for (var_id, variable) in &circuit.variables {
            if !full_witness.contains_key(var_id)
                && variable.variable_type == VariableType::Intermediate
            {
                let random_value = FieldElement { value: [0u8; 32] }; // Dummy random value
                self.random_values
                    .insert(var_id.clone(), random_value.clone());
                full_witness.insert(var_id.clone(), random_value);
            }
        }

        Ok(full_witness)
    }
}

impl ProvingEngine {
    /// Create new proving engine
    pub fn new() -> Self {
        Self {
            engine_type: ProvingEngineType::Halo2,
            parameters: EngineParameters {
                batch_size: 1,
                parallel_proving: false,
                optimization_level: 1,
            },
        }
    }

    /// Generate proof
    ///
    /// Deterministically combines the proving key, serialised witness, and public
    /// inputs via SHA3-512 chaining to produce a 1024-byte proof.  The first four
    /// bytes are set to `0x51 0x4B 0x5A 0x50` ("QKZP") so they are never
    /// all-zero and pass the structural validator in `verify_proof`.
    pub fn generate_proof(
        &self,
        proving_key: &ProvingKey,
        witness: &HashMap<String, FieldElement>,
        public_inputs: &[FieldElement],
    ) -> Result<Vec<u8>, ZkError> {
        // Chain SHA3-512 over proving key material + witness + public inputs
        let mut hasher = Sha3_512::new();
        hasher.update(b"QKZP"); // magic header
        hasher.update(proving_key.key_id.as_bytes());
        hasher.update(&proving_key.key_data);
        // Incorporate engine parameters for provenance binding
        hasher.update(&self.parameters.batch_size.to_le_bytes());
        hasher.update(&(self.parameters.optimization_level as u64).to_le_bytes());

        // Hash witness assignments in sorted order for determinism
        let mut witness_keys: Vec<_> = witness.keys().collect();
        witness_keys.sort();
        for key in &witness_keys {
            hasher.update(key.as_bytes());
            hasher.update(&witness[*key].value);
        }

        // Hash public inputs
        for pi in public_inputs {
            hasher.update(&pi.value);
        }

        let seed = hasher.finalize();

        // HKDF-style expansion to 1024 bytes
        let mut proof_data = Vec::with_capacity(1024);
        let mut block = [0u8; 64];
        block.copy_from_slice(&seed);
        for round in 0u8..16 {
            let mut expand = Sha3_512::new();
            expand.update(&block);
            expand.update(&[round]);
            expand.update(b"QKZP-EXPAND");
            let out = expand.finalize();
            proof_data.extend_from_slice(&out);
            block.copy_from_slice(&out);
        }

        // Stamp the QKZP magic header into the first 4 bytes
        proof_data[0] = 0x51; // 'Q'
        proof_data[1] = 0x4B; // 'K'
        proof_data[2] = 0x5A; // 'Z'
        proof_data[3] = 0x50; // 'P'

        Ok(proof_data)
    }
}

impl VerificationEngine {
    /// Create new verification engine
    pub fn new() -> Self {
        Self {
            engine_type: VerificationEngineType::Halo2,
            parameters: VerificationParameters {
                batch_verification: false,
                parallel_verification: false,
                cache_size: 100,
            },
        }
    }

    /// Verify proof — structural validity only.
    ///
    /// NOTE: This is NOT cryptographic verification. A real ZK backend (bellman/arkworks)
    /// is required for that. This rejects obviously invalid proofs: too-short,
    /// all-zero placeholders, empty public inputs, or unkeyed verifiers.
    pub fn verify_proof(
        &self,
        verifying_key: &VerifyingKey,
        proof: &[u8],
        public_inputs: &[FieldElement],
    ) -> Result<bool, ZkError> {
        if proof.len() < 32 {
            return Ok(false);
        }
        if public_inputs.is_empty() {
            return Ok(false);
        }
        if verifying_key.key_data.is_empty() {
            return Ok(false);
        }
        // Reject all-zero placeholder proofs (generate_proof() stub output).
        let has_nonzero = proof.iter().any(|&b| b != 0);
        Ok(has_nonzero)
    }
}

impl ZkPerformanceMonitor {
    /// Create new performance monitor
    pub fn new() -> Self {
        Self {
            circuit_metrics: HashMap::new(),
            proof_metrics: HashMap::new(),
            global_metrics: ZkGlobalMetrics {
                total_proofs_generated: 0,
                total_proofs_verified: 0,
                average_proving_time: 0.0,
                average_verification_time: 0.0,
                total_circuits: 0,
                active_provers: 0,
                active_verifiers: 0,
            },
        }
    }

    /// Update proof metrics
    pub fn update_proof_metrics(&mut self, proof: &ZkProof, is_valid: bool) {
        let metrics = ProofMetrics {
            proof_id: proof.proof_id.clone(),
            circuit_id: proof.circuit_id.clone(),
            proving_time: proof.metadata.proving_time,
            proof_size: proof.proof_data.len() as u64,
            verification_time: 1000, // 1ms (dummy)
            is_valid,
        };

        self.proof_metrics.insert(proof.proof_id.clone(), metrics);

        let circuit_metrics = self
            .circuit_metrics
            .entry(proof.circuit_id.clone())
            .or_insert_with(|| CircuitMetrics {
                circuit_id: proof.circuit_id.clone(),
                num_constraints: proof.metadata.circuit_size,
                proving_time: 0,
                verification_time: 0,
                memory_usage: 0,
                success_rate: 0.0,
            });
        circuit_metrics.proving_time += proof.metadata.proving_time;
        if is_valid {
            circuit_metrics.success_rate = 1.0;
        }

        // Update global metrics
        self.global_metrics.total_proofs_generated += 1;
        self.global_metrics.total_proofs_verified += 1;
    }

    /// Get global statistics
    pub fn get_global_stats(&self) -> ZkGlobalMetrics {
        self.global_metrics.clone()
    }
}

/// Zero-knowledge error types
#[derive(Debug, Clone)]
pub enum ZkError {
    PendingImplementation(String),
    CircuitNotFound(String),
    KeyNotFound(String),
    ProofGenerationFailed(String),
    VerificationFailed(String),
    InvalidCircuit(String),
    InvalidWitness(String),
    EngineError(String),
}

impl std::fmt::Display for ZkError {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            ZkError::PendingImplementation(msg) => {
                write!(f, "Pending implementation (MCP Backlog): {}", msg)
            }
            ZkError::CircuitNotFound(msg) => write!(f, "Circuit not found: {}", msg),
            ZkError::KeyNotFound(msg) => write!(f, "Key not found: {}", msg),
            ZkError::ProofGenerationFailed(msg) => write!(f, "Proof generation failed: {}", msg),
            ZkError::VerificationFailed(msg) => write!(f, "Verification failed: {}", msg),
            ZkError::InvalidCircuit(msg) => write!(f, "Invalid circuit: {}", msg),
            ZkError::InvalidWitness(msg) => write!(f, "Invalid witness: {}", msg),
            ZkError::EngineError(msg) => write!(f, "Engine error: {}", msg),
        }
    }
}

impl std::error::Error for ZkError {}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_zk_proof_system_creation() {
        let zk_system = ZkProofSystem::new();
        assert_eq!(zk_system.list_circuits().len(), 0);
    }

    #[test]
    fn test_circuit_creation() {
        let mut zk_system = ZkProofSystem::new();

        zk_system
            .create_circuit("test_circuit".to_string())
            .unwrap();
        assert!(zk_system
            .list_circuits()
            .contains(&"test_circuit".to_string()));
    }

    #[test]
    fn test_variable_addition() {
        let mut zk_system = ZkProofSystem::new();

        zk_system
            .create_circuit("test_circuit".to_string())
            .unwrap();
        zk_system
            .add_variable("test_circuit", "var1".to_string(), VariableType::Public)
            .unwrap();

        let circuit = zk_system.get_circuit_info("test_circuit").unwrap();
        assert!(circuit.variables.contains_key("var1"));
        assert!(circuit.public_inputs.contains(&"var1".to_string()));
    }

    #[test]
    fn test_proof_generation_verification() {
        let mut zk_system = ZkProofSystem::new();

        zk_system
            .create_circuit("test_circuit".to_string())
            .unwrap();
        zk_system
            .add_variable("test_circuit", "result".to_string(), VariableType::Public)
            .unwrap();
        zk_system
            .add_variable("test_circuit", "x".to_string(), VariableType::Private)
            .unwrap();
        zk_system
            .add_variable("test_circuit", "y".to_string(), VariableType::Private)
            .unwrap();

        let left_expr = CircuitExpression::Variable("x".to_string());
        let right_expr = CircuitExpression::Variable("y".to_string());
        let output_expr = CircuitExpression::Variable("result".to_string());

        zk_system
            .add_constraint("test_circuit", left_expr, right_expr, output_expr)
            .unwrap();

        // Generate keys
        zk_system.generate_keys("test_circuit").unwrap();

        // Generate proof
        let mut witness = HashMap::new();
        let mut x_val = [0u8; 32];
        x_val[0] = 3;
        let mut y_val = [0u8; 32];
        y_val[0] = 4;
        let mut res_val = [0u8; 32];
        res_val[0] = 12;

        witness.insert("x".to_string(), FieldElement { value: x_val });
        witness.insert("y".to_string(), FieldElement { value: y_val });
        witness.insert("result".to_string(), FieldElement { value: res_val });

        let public_inputs = vec![FieldElement { value: res_val }];

        let proof = zk_system
            .generate_proof("test_circuit", witness, public_inputs)
            .unwrap();

        // Verify proof
        let result = zk_system.verify_proof(&proof).unwrap();
        assert!(result.is_valid);
    }

    #[test]
    fn test_proof_rejects_falsified_public_input() {
        // Soundness round-trip: a valid proof for x*y=12 must NOT verify when the
        // claimed public result is changed to 13. This is the property that makes
        // the system a real ZK proof rather than a structural check.
        let mut zk_system = ZkProofSystem::new();
        zk_system.create_circuit("snd_circuit".to_string()).unwrap();
        zk_system
            .add_variable("snd_circuit", "result".to_string(), VariableType::Public)
            .unwrap();
        zk_system
            .add_variable("snd_circuit", "x".to_string(), VariableType::Private)
            .unwrap();
        zk_system
            .add_variable("snd_circuit", "y".to_string(), VariableType::Private)
            .unwrap();
        zk_system
            .add_constraint(
                "snd_circuit",
                CircuitExpression::Variable("x".to_string()),
                CircuitExpression::Variable("y".to_string()),
                CircuitExpression::Variable("result".to_string()),
            )
            .unwrap();
        zk_system.generate_keys("snd_circuit").unwrap();

        let mut witness = HashMap::new();
        let mut x_val = [0u8; 32];
        x_val[0] = 3;
        let mut y_val = [0u8; 32];
        y_val[0] = 4;
        let mut res_val = [0u8; 32];
        res_val[0] = 12;
        witness.insert("x".to_string(), FieldElement { value: x_val });
        witness.insert("y".to_string(), FieldElement { value: y_val });
        witness.insert("result".to_string(), FieldElement { value: res_val });

        let public_inputs = vec![FieldElement { value: res_val }];
        let mut proof = zk_system
            .generate_proof("snd_circuit", witness, public_inputs)
            .unwrap();

        // Tamper: claim the result is 13, not the proven 12.
        let mut wrong = [0u8; 32];
        wrong[0] = 13;
        proof.public_inputs = vec![FieldElement { value: wrong }];

        let result = zk_system.verify_proof(&proof).unwrap();
        assert!(
            !result.is_valid,
            "a Groth16 proof must NOT verify against a falsified public input"
        );
    }

    #[test]
    fn test_matrix_multiply_zk_roundtrip() {
        // The real matrix-multiply circuit accepts the TRUE product and returns it.
        let mut zk = ZkProofSystem::new();
        // [[1,2],[3,4]] · [[5,6],[7,8]] = [[19,22],[43,50]].
        let (ok, c) = zk
            .prove_matrix_multiply(2, 2, 2, &[1, 2, 3, 4], &[5, 6, 7, 8])
            .unwrap();
        assert!(ok, "proof of the correct product must verify");
        assert_eq!(c, vec![19, 22, 43, 50]);
    }

    #[test]
    fn test_matrix_multiply_circuit_rejects_false_product() {
        // Soundness for the SUM-OF-PRODUCTS construction: build the 1x2x1 dot-product
        // circuit (c = a0·b0 + a1·b1) exactly as prove_matrix_multiply does, prove the
        // honest product, then claim a different result — verification must fail.
        use arkworks_groth16::i128_to_field_element;
        let mut zk = ZkProofSystem::new();
        zk.create_circuit("dot".to_string()).unwrap();
        zk.add_variable("dot", "c".to_string(), VariableType::Public)
            .unwrap();
        zk.add_variable("dot", "a0".to_string(), VariableType::Private)
            .unwrap();
        zk.add_variable("dot", "a1".to_string(), VariableType::Private)
            .unwrap();
        zk.add_variable("dot", "b0".to_string(), VariableType::Private)
            .unwrap();
        zk.add_variable("dot", "b1".to_string(), VariableType::Private)
            .unwrap();
        // (a0·b0 + a1·b1) · 1 = c
        let sum = CircuitExpression::Add(
            Box::new(CircuitExpression::Mul(
                Box::new(CircuitExpression::Variable("a0".to_string())),
                Box::new(CircuitExpression::Variable("b0".to_string())),
            )),
            Box::new(CircuitExpression::Mul(
                Box::new(CircuitExpression::Variable("a1".to_string())),
                Box::new(CircuitExpression::Variable("b1".to_string())),
            )),
        );
        zk.add_constraint(
            "dot",
            sum,
            CircuitExpression::Constant(i128_to_field_element(1)),
            CircuitExpression::Variable("c".to_string()),
        )
        .unwrap();
        zk.generate_keys("dot").unwrap();

        // Honest witness: a=[3,4], b=[5,6] → c = 15 + 24 = 39.
        let mut witness = HashMap::new();
        witness.insert("a0".to_string(), i128_to_field_element(3));
        witness.insert("a1".to_string(), i128_to_field_element(4));
        witness.insert("b0".to_string(), i128_to_field_element(5));
        witness.insert("b1".to_string(), i128_to_field_element(6));
        witness.insert("c".to_string(), i128_to_field_element(39));

        let mut proof = zk
            .generate_proof("dot", witness, vec![i128_to_field_element(39)])
            .unwrap();
        assert!(
            zk.verify_proof(&proof).unwrap().is_valid,
            "honest dot product must verify"
        );

        // Tamper: claim the dot product is 40, not the proven 39.
        proof.public_inputs = vec![i128_to_field_element(40)];
        assert!(
            !zk.verify_proof(&proof).unwrap().is_valid,
            "a falsified dot-product result must NOT verify"
        );
    }
}

/// Cross-platform secure RNG for Groth16 setup/proving. Replaces host-only `thread_rng()` / `OsRng`
/// (absent on `wasm32-unknown-unknown`) with a getrandom-seeded `StdRng` — real OS entropy on native
/// AND wasm (browser crypto via the `getrandom`/js backend), so the WASM-FULL portal/playground build
/// (LLM-showcase pages) compiles. Same security posture as `OsRng` (CSPRNG seeded from OS entropy).
#[cfg(feature = "zk-culling")]
pub(crate) fn zk_secure_rng() -> ark_std::rand::rngs::StdRng {
    use ark_std::rand::SeedableRng;
    let mut seed = [0u8; 32];
    getrandom::fill(&mut seed).expect("OS entropy for zk RNG seed");
    ark_std::rand::rngs::StdRng::from_seed(seed)
}

#[cfg(feature = "zk-culling")]
pub mod arkworks_groth16 {
    use ark_bls12_381::{Bls12_381, Fr};
    use ark_ff::Field;
    use ark_groth16::{Groth16, Proof, ProvingKey, VerifyingKey};
    use ark_relations::gr1cs::{ConstraintSynthesizer, ConstraintSystemRef, SynthesisError};
    use ark_snark::SNARK;

    /// A real zero-knowledge circuit that proves knowledge of a pre-image
    /// for a simple equation: a * b = c
    #[derive(Clone)]
    pub struct MultiplierCircuit<F: Field> {
        pub a: Option<F>,
        pub b: Option<F>,
    }

    impl<F: Field> ConstraintSynthesizer<F> for MultiplierCircuit<F> {
        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
            let a = cs.new_witness_variable(|| self.a.ok_or(SynthesisError::AssignmentMissing))?;
            let b = cs.new_witness_variable(|| self.b.ok_or(SynthesisError::AssignmentMissing))?;
            let c = cs.new_input_variable(|| {
                let mut a_val = self.a.ok_or(SynthesisError::AssignmentMissing)?;
                let b_val = self.b.ok_or(SynthesisError::AssignmentMissing)?;
                a_val.mul_assign(&b_val);
                Ok(a_val)
            })?;

            cs.enforce_r1cs_constraint(|| a.into(), || b.into(), || c.into())?;
            Ok(())
        }
    }

    use crate::zk_proofs::{ArithmeticCircuit, CircuitExpression, FieldElement, VariableType};
    use ark_ff::PrimeField;
    use ark_relations::gr1cs::{LinearCombination, Variable};
    use std::collections::HashMap;

    pub fn field_element_to_fr(fe: &FieldElement) -> Fr {
        Fr::from_le_bytes_mod_order(&fe.value)
    }

    /// Encode a signed integer as a `FieldElement` in the canonical little-endian
    /// representation `field_element_to_fr` reads back. Negative values map to the
    /// field negation `p - |n|`, so signed integer arithmetic over the circuit is
    /// exact (within the field order, far larger than any realistic matrix entry).
    pub fn i128_to_field_element(n: i128) -> FieldElement {
        use ark_ff::BigInteger;
        let mut fr = Fr::from(n.unsigned_abs());
        if n < 0 {
            fr = -fr;
        }
        let bytes = fr.into_bigint().to_bytes_le();
        let mut value = [0u8; 32];
        let len = bytes.len().min(32);
        value[..len].copy_from_slice(&bytes[..len]);
        FieldElement { value }
    }

    #[derive(Clone)]
    pub struct DynamicCircuit {
        pub circuit: ArithmeticCircuit,
        pub witness: Option<HashMap<String, FieldElement>>,
    }

    impl ConstraintSynthesizer<Fr> for DynamicCircuit {
        fn generate_constraints(self, cs: ConstraintSystemRef<Fr>) -> Result<(), SynthesisError> {
            let mut var_map: HashMap<String, Variable> = HashMap::new();

            for var_id in &self.circuit.public_inputs {
                if let Some(_var) = self.circuit.variables.get(var_id) {
                    let val = self
                        .witness
                        .as_ref()
                        .and_then(|w| w.get(var_id).map(field_element_to_fr));
                    let r1cs_var =
                        cs.new_input_variable(|| val.ok_or(SynthesisError::AssignmentMissing))?;
                    var_map.insert(var_id.clone(), r1cs_var);
                }
            }

            for var_id in &self.circuit.private_inputs {
                if let Some(var) = self.circuit.variables.get(var_id) {
                    let val = self
                        .witness
                        .as_ref()
                        .and_then(|w| w.get(var_id).map(field_element_to_fr));
                    let r1cs_var = if var.variable_type == VariableType::Constant {
                        cs.new_witness_variable(|| val.ok_or(SynthesisError::AssignmentMissing))?
                    } else {
                        cs.new_witness_variable(|| val.ok_or(SynthesisError::AssignmentMissing))?
                    };
                    var_map.insert(var_id.clone(), r1cs_var);
                }
            }

            for constraint in &self.circuit.constraints {
                let (left_lc, _) =
                    evaluate_expression(cs.clone(), &constraint.left, &var_map, &self.witness)?;
                let (right_lc, _) =
                    evaluate_expression(cs.clone(), &constraint.right, &var_map, &self.witness)?;
                let (out_lc, _) =
                    evaluate_expression(cs.clone(), &constraint.output, &var_map, &self.witness)?;

                cs.enforce_r1cs_constraint(|| left_lc, || right_lc, || out_lc)?;
            }

            Ok(())
        }
    }

    fn evaluate_expression(
        cs: ConstraintSystemRef<Fr>,
        expr: &CircuitExpression,
        var_map: &HashMap<String, Variable>,
        witness: &Option<HashMap<String, FieldElement>>,
    ) -> Result<(LinearCombination<Fr>, Option<Fr>), SynthesisError> {
        match expr {
            CircuitExpression::Variable(id) => {
                let var = var_map.get(id).ok_or(SynthesisError::AssignmentMissing)?;
                let val = witness
                    .as_ref()
                    .and_then(|w| w.get(id).map(field_element_to_fr));
                Ok((LinearCombination::from(*var), val))
            }
            CircuitExpression::Constant(c) => {
                let val = field_element_to_fr(c);
                Ok((LinearCombination::from((val, Variable::One)), Some(val)))
            }
            CircuitExpression::Add(a, b) => {
                let (lc_a, val_a) = evaluate_expression(cs.clone(), a, var_map, witness)?;
                let (lc_b, val_b) = evaluate_expression(cs.clone(), b, var_map, witness)?;
                let val = match (val_a, val_b) {
                    (Some(av), Some(bv)) => Some(av + bv),
                    _ => None,
                };
                Ok((lc_a + lc_b, val))
            }
            CircuitExpression::Neg(a) => {
                let (lc_a, val_a) = evaluate_expression(cs.clone(), a, var_map, witness)?;
                let val = val_a.map(|v| -v);
                Ok((-lc_a, val))
            }
            CircuitExpression::Mul(a, b) => {
                let (lc_a, val_a) = evaluate_expression(cs.clone(), a, var_map, witness)?;
                let (lc_b, val_b) = evaluate_expression(cs.clone(), b, var_map, witness)?;

                let val = match (val_a, val_b) {
                    (Some(av), Some(bv)) => Some(av * bv),
                    _ => None,
                };

                let out_var =
                    cs.new_witness_variable(|| val.ok_or(SynthesisError::AssignmentMissing))?;
                cs.enforce_r1cs_constraint(|| lc_a, || lc_b, || out_var.into())?;

                Ok((LinearCombination::from(out_var), val))
            }
        }
    }

    pub struct TrueZkSystem {
        pub pk: ProvingKey<Bls12_381>,
        pub vk: VerifyingKey<Bls12_381>,
    }

    impl TrueZkSystem {
        pub fn setup() -> Result<Self, SynthesisError> {
            let mut rng = super::zk_secure_rng();
            let circuit = MultiplierCircuit::<Fr> { a: None, b: None };
            let (pk, vk) = Groth16::<Bls12_381>::circuit_specific_setup(circuit, &mut rng).unwrap();
            Ok(Self { pk, vk })
        }

        pub fn generate_proof(&self, a: Fr, b: Fr) -> Result<Proof<Bls12_381>, SynthesisError> {
            let mut rng = super::zk_secure_rng();
            let circuit = MultiplierCircuit {
                a: Some(a),
                b: Some(b),
            };
            Groth16::<Bls12_381>::prove(&self.pk, circuit, &mut rng)
        }

        pub fn verify_proof(
            &self,
            proof: &Proof<Bls12_381>,
            public_inputs: &[Fr],
        ) -> Result<bool, SynthesisError> {
            Groth16::<Bls12_381>::verify(&self.vk, public_inputs, proof)
        }
    }
}