feat: (halo2) SNARK verifier

[MonkeyKing-1]

Guest library for verifying halo2 proofs.

Integration test currently failing because:

• snark-verifier requires std library and in particular uses std::collections::HashMap. We need to implement sys_rand with a phantom instruction passing to host randomness (INT-2955) Change snark-verifier to use BTreeMap. chore: use BTreeMap instead of HashMap for evaluations axiom-crypto/snark-verifier#68

[lispc]

With the following modifications, i can use this branch to build/run/prove a plonk verification program.

Things i fixed:

1. i find the halo2curves-axiom and snark-verifier::halo2curves-axiom is a version management nightmare, so in my local env, i unify to use same version.
2. snark-verifier/src/verifier/plonk/proof.rs uses HashMap, which is not support inside zkvm. So i switched to BTreeMap.
3. i added several review comments, some endianness are not correct.
4. this PR lacks this trait, i added.

impl<const LIMBS: usize, const BITS: usize> AccumulatorEncoding<G1Affine, OpenVmLoader>
for LimbsEncoding<LIMBS, BITS>
{
type Accumulator = KzgAccumulator<G1Affine, OpenVmLoader>;

fn from_repr(limbs: &[&OpenVmScalar<Halo2Fr, Fr>]) -> Result<Self::Accumulator, Error> {
    assert_eq!(limbs.len(), 4 * LIMBS);

            let loader = &*LOADER;

            let [lhs_x, lhs_y, rhs_x, rhs_y]: [_; 4] = limbs
                .chunks(LIMBS)
                .map(|limbs| {
                    let v: [Halo2Fr; LIMBS] = limbs.iter().map(|limb| {
                      let mut buf = limb.0.to_be_bytes();
                      buf.reverse();
                      Halo2Fr::from_bytes(&buf).expect("Halo2Fr::from_bytes")
                }).collect_vec().try_into().unwrap();
                    fe_from_limbs::<_, Halo2Fp, LIMBS, BITS>(
                        v
                    )
                }
                )
                .collect_vec()
                .try_into()
                .unwrap();

                let accumulator = KzgAccumulator::new(
                    OpenVmEcPoint(EcPoint {
                        x: Fp::from_le_bytes(&lhs_x.to_bytes()),
                        y: Fp::from_le_bytes(&lhs_y.to_bytes()),
                    }, PhantomData),
                    OpenVmEcPoint(EcPoint {
                        x: Fp::from_le_bytes(&rhs_x.to_bytes()),
                        y: Fp::from_le_bytes(&rhs_y.to_bytes()),
                    }, PhantomData)
                );
                Ok(accumulator)
}
}

Other thoughts:

1. i feel the current API, Fp::from_bytes() will not panic for overflowed inputs. It will pass along the wrong data a long way till err. Not easy to debug. Add another API from_bytes_strict for debugging?

My program

#[derive(Serialize, Deserialize)]
struct FullProof {
    pub proof: Vec<u8>,
    pub instances: Vec<Vec<Fr>>, 
    pub dk: KzgDecidingKey<Bn256>, // const
    pub protocol: PlonkProtocol<G1Affine>, // const
}

fn verify_guest() {
    use snark_verifier_sdk::{PlonkSuccinctVerifier, PlonkVerifier, SHPLONK};

    let full_proof_bytes = include_bytes!("../full_proof.json");
    let full_proof = serde_json::from_slice::<FullProof>(full_proof_bytes).unwrap();

    println!("serde done");

    let mut transcript = OpenVmTranscript::<G1Affine, _, _>::new(full_proof.proof.as_slice());

    let instances: Vec<
        Vec<OpenVmScalar<halo2curves_axiom::bn256::Fr, openvm_pairing_guest::bn254::Scalar>>,
    > = full_proof
        .instances
        .into_iter()
        .map(|x| {
            x.into_iter()
                .map(|x| {
                    use openvm_ecc_guest::algebra::IntMod;
                    let value = openvm_pairing_guest::bn254::Scalar::from_le_bytes(&x.to_bytes());
                    OpenVmScalar(value, PhantomData)
                })
                .collect()
        })
        .collect::<Vec<_>>();
    println!("transcript done");

    let loader = &LOADER;
    let protocol: PlonkProtocol<G1Affine, OpenVmLoader> = full_proof.protocol.loaded(loader);
    println!("protocol loaded");
    let loaded_proof: snark_verifier_sdk::snark_verifier::verifier::plonk::PlonkProof<
        G1Affine,
        OpenVmLoader,
        SHPLONK,
    > = PlonkVerifier::<SHPLONK>::read_proof(
        &full_proof.dk,
        &protocol,
        &instances[..],
        &mut transcript,
    )
    .unwrap();

    println!("loaded_proof done");
    let accumulators = PlonkSuccinctVerifier::<SHPLONK>::verify(
        full_proof.dk.as_ref(),
        &protocol,
        &instances[..],
        &loaded_proof,
    )
    .unwrap();
    println!("before pairing, pairing num {}", accumulators.len());

    SHPLONK::decide_all(&full_proof.dk, accumulators).unwrap();

    println!("plonk verify done");
    // TODO: assert some parts of instances to be predefined consts (like program commitment)
}

[jonathanpwang]

I think there was some nightmare with halo2curves-axiom, but in current main I tried to make everything use the same crates.io version (I hope). I'll look into the other issues, thanks!

[lispc]

some high level thoughts:

the plonk verification can be generally split into 2 parts: (1) msm and pairing, heavy computation, may >90% of all "cycles" needed (2) light weight computation, like fr ops and other control flow glue codes. Maybe just "patch" msm and pairing, we can get most of the speedup.

Though the PR works well, i feel there are a lot of "wrapper" codes in trait.rs, also in other files, the codes are quite similar to NativeLoader. I don't have an alternative good solution now, just feel this design may not be easy to maintain long term, it has to be changed with snark-verfier::EvmTranscript every time, like endianness and how squeeze_challenge is computated.

[jonathanpwang]

@lispc previous tests were only on host, not targeting zkvm. I added integration test targeting zkvm and discovered that snark-verifier uses std library HashMap somewhere. This hashmap thing is annoying enough I will try to add the sys_rand support tomorrow

[lispc]

@lispc previous tests were only on host, not targeting zkvm. I added integration test targeting zkvm and discovered that snark-verifier uses std library HashMap somewhere. This hashmap thing is annoying enough I will try to add the sys_rand support tomorrow

oh actually I tested in guest. （and even proved it "recursively") I changed hashmap to btree map locally. I remember it is a "evaluation.rs"?

[jonathanpwang]

@lispc previous tests were only on host, not targeting zkvm. I added integration test targeting zkvm and discovered that snark-verifier uses std library HashMap somewhere. This hashmap thing is annoying enough I will try to add the sys_rand support tomorrow

oh actually I tested in guest. （and even proved it "recursively") I changed hashmap to btree map locally. I remember it is a "evaluation.rs"?

Ah, maybe it's easier if I just update in snark-verifier then... thanks