Unclear UnSat Error: 'RecursiveSNARK::verify: Err(UnSat)'

[fraVlaca]

Following examples found in NovaScotia and I get error UnSat, that following Nova docs means: returned if the supplied witness is not a satisfying witness to a given shape and instance.

The circuit is proved correctly but when it comes to verify it, this problems comes out with the witness verification. I have literally no idea on where the problem is as the circuit is proved correctly and should be verified correctly too, is there as step that I am missing with the primary or secondary curves inputs, for the secondary I am just passing 0 as I have no idea what it does (but can see that if I pass any other number I get ProofVerifyError, which tells me that the 0 might be on the right road)

I am using NovaScotia to compile a recursiveSnark from my Circom circuit and then using Nova to verify and compress the proof.

This is my script code:

use std::{
    collections::HashMap,
    env::current_dir,
    io::Write,
    time::{Duration, Instant},
};
use babyjubjub_rs::Point;
use pasta_curves::group::ff::PrimeField;

use nova_scotia::{
    circom::reader::load_r1cs, create_public_params, create_recursive_circuit, FileLocation, F
};
use nova_snark::{
    traits::{circuit::TrivialTestCircuit, Group},
    CompressedSNARK, PublicParams, RecursiveSNARK,
};
use serde::{Deserialize, Serialize};
use serde_json::json;
use poseidon_rs::{Fr, Poseidon};

#[derive(Serialize, Deserialize)]
#[allow(non_snake_case)]
struct ProofInput {
    step_in: Vec<String>,
    newData: Vec<String>,
    nextUserBehavioralProfileCommitments: Vec<String>,
    r8x: String,
    r8y: String,
    s: String,
}

fn bench() -> (Duration, Duration) {
    type G1 = pasta_curves::pallas::Point;
    type G2 = pasta_curves::vesta::Point;
    let root = current_dir().unwrap();

    let circuit_file = root.join("../build/recursiveLogin.r1cs");

    let r1cs = load_r1cs::<G1, G2>(&FileLocation::PathBuf(circuit_file));
    let witness_generator_file =
        root.join("../build/recursiveLogin_js/recursiveLogin.wasm");


    // load serde json
    let users_data: Vec<ProofInput> =
        serde_json::from_str(include_str!("fetcher/loginsInputs.json")).unwrap();
    let iteration_count: usize = users_data.len();

    let start_public_input = [
        F::<G1>::from_str_vartime(&users_data[0].step_in[0]).unwrap(),
        F::<G1>::from_str_vartime(&users_data[0].step_in[1]).unwrap(),
        F::<G1>::from_str_vartime(&users_data[0].step_in[2]).unwrap(),
        F::<G1>::from_str_vartime(&users_data[0].step_in[3]).unwrap()
    ];

    let mut private_inputs = Vec::new();

    for i in 0..users_data.len() {
        let mut private_input = HashMap::new();
        private_input.insert(
            "newData".to_string(),
            json!(
                users_data[i].newData
            ),
            //(0..lengthNewData).map(|j| F1::from_raw(&usersData[i].newData[j]).unwrap()).collect();
        );
        private_input.insert(
            "S".to_string(),
            json!(users_data[i].s)
        );
        private_input.insert(
            "R8x".to_string(),
            json!(users_data[i].r8x)
        );
        private_input.insert(
            "R8y".to_string(),
            json!(users_data[i].r8y)
        );
        let mut nextUserBehavioralProfileCommitments = Vec::new();

        nextUserBehavioralProfileCommitments.extend_from_slice(&users_data[i].nextUserBehavioralProfileCommitments);

        private_input.insert(
            "nextUserBehavioralProfileCommitments".to_string(),
            json!(
                nextUserBehavioralProfileCommitments
            ),
        );
        private_inputs.push(private_input);
    }

     println!("{:?} {:?}", start_public_input, private_inputs);

    let pp = create_public_params(r1cs.clone());

    println!(
        "Number of constraints per step (primary circuit): {}",
        pp.num_constraints().0
    );
    println!(
        "Number of constraints per step (secondary circuit): {}",
        pp.num_constraints().1
    );

    println!(
        "Number of variables per step (primary circuit): {}",
        pp.num_variables().0
    );
    println!(
        "Number of variables per step (secondary circuit): {}",
        pp.num_variables().1
    );

    println!("witness_generator_file {:?}", witness_generator_file);

    println!("Creating a RecursiveSNARK...");
    let start = Instant::now();
    let recursive_snark = create_recursive_circuit(
        FileLocation::PathBuf(witness_generator_file),
        r1cs,
        private_inputs,
        start_public_input.to_vec(),
        &pp,
    )
    .unwrap();
    let prover_time = start.elapsed();
    println!("RecursiveSNARK creation took {:?}", start.elapsed());

    let z0_secondary = [<G2 as Group>::Scalar::zero()];

    // verify the recursive SNARK
    println!("Verifying a RecursiveSNARK...");
    let start = Instant::now();
    let res = recursive_snark.verify(
        &pp,
        iteration_count,
        &start_public_input,
        &z0_secondary,
    );
    println!(
        "RecursiveSNARK::verify: {:?}, took {:?}",
        res,
        start.elapsed()
    );
    let verifier_time = start.elapsed();
    assert!(res.is_ok());

    // produce a compressed SNARK
    println!("Generating a CompressedSNARK using Spartan with IPA-PC...");
    let (pk, vk) = CompressedSNARK::<_, _, _, _, S1, S2>::setup(&pp).unwrap();

    // produce a compressed SNARK
    println!("Generating a CompressedSNARK using Spartan with IPA-PC...");
    let start = Instant::now();
    type EE1 = nova_snark::provider::ipa_pc::EvaluationEngine<G1>;
    type EE2 = nova_snark::provider::ipa_pc::EvaluationEngine<G2>;
    type S1 = nova_snark::spartan::snark::RelaxedR1CSSNARK<G1, EE1>;
    type S2 = nova_snark::spartan::snark::RelaxedR1CSSNARK<G2, EE2>;
    let res = CompressedSNARK::<_, _, _, _, S1, S2>::prove(&pp, &pk, &recursive_snark);
    println!(
        "CompressedSNARK::prove: {:?}, took {:?}",
        res.is_ok(),
        start.elapsed()
    );
    assert!(res.is_ok());
    let compressed_snark = res.unwrap();

    // verify the compressed SNARK
    println!("Verifying a CompressedSNARK...");
    let start = Instant::now();
    let res = compressed_snark.verify(
        &vk,
        iteration_count,
        start_public_input.clone().to_vec(),
        z0_secondary.to_vec(),
    );
    println!(
        "CompressedSNARK::verify: {:?}, took {:?}",
        res.is_ok(),
        start.elapsed()
    );
    assert!(res.is_ok());
    let serialized_compressed_snark = serde_json::to_string(&compressed_snark).unwrap();

    (prover_time, verifier_time)
}

fn main() {
    // create benchmark file
    let mut file = std::fs::File::create("src/benchmark.csv").unwrap();
    file.write_all(b"iteration_count,prover_time,verifier_time\n")
        .unwrap();
    let iteration_count = 100;

        // run bash script
        /* std::process::Command::new("bash")
            .arg("../scripts/circom/compile.sh")
            .arg(i.to_string())
            .output()
            .expect("failed to execute process"); */

    let (prover_time, verifier_time) = bench();
    file.write_all(format!("{},{:?},{:?}\n", iteration_count, prover_time, verifier_time).as_bytes())
        .unwrap();
}

I get

Number of constraints per step (primary circuit): 15892
Number of constraints per step (secondary circuit): 10347
Number of variables per step (primary circuit): 16659
Number of variables per step (secondary circuit): 10329
witness_generator_file "/Users/vlaca/Documents/work/innerworks/zero-knowledge/zk/nova/../build/recursiveLogin_js/recursiveLogin.wasm"
Creating a RecursiveSNARK...
RecursiveSNARK creation took 1.677693459s
Verifying a RecursiveSNARK...
RecursiveSNARK::verify: Err(UnSat), took 104.866ms
thread 'main' panicked at 'assertion failed: res.is_ok()', src/main.rs:165:5

The UnSat error really does not tell me much and I am stuck

[fraVlaca]

Solved, I was compiling with the wrong curve using circom