sigma-compiler/tests/claim_narrowing.rs

#![allow(non_snake_case)]
//! Term-free (public) equations are lowered one of two ways, and these
//! tests pin down which: conjoined, they are evaluated by `compile()`
//! and cost nothing on the wire; under a disjunction, they become claim
//! leaves whose constant shape lets a false branch be simulated.
use curve25519_dalek::ristretto::RistrettoPoint as G;
use group::Group;
use sha2::Sha512;
use sigma_compiler::*;

type Scalar = <G as Group>::Scalar;

/// A conjoined term-free equation leaves no trace: `compile()` strips
/// it, so the statement is the one written without it, down to the
/// transcript.  A proof of the stripped statement therefore verifies
/// here -- which it cannot if the equation became a claim leaf, since
/// that leaf is part of the composition the transcript binds.
#[test]
fn conjoined_claim_leaves_no_trace() -> Result<(), Box<dyn std::error::Error>> {
    sigma_compiler! { plain,
        (x),
        (C, const cind A),
        C = x*A,
    }
    sigma_compiler! { claimed,
        (x),
        (C, D, E, const cind A),
        C = x*A,
        D = E,
    }

    let mut rng = rand::thread_rng();
    let A = G::hash_from_bytes::<Sha512>(b"Generator A");
    let D = G::hash_from_bytes::<Sha512>(b"Element D");
    let x = Scalar::random(&mut rng);
    let C = x * A;

    let plain_proof = plain::prove(
        &plain::Instance { C, A },
        &plain::Witness { x },
        b"claim_narrowing",
        &mut rng,
    )?;

    // `D = E` holds, so the statement is exactly the one above.
    let instance = claimed::Instance { C, D, E: D, A };
    let claimed_proof = claimed::prove(
        &instance,
        &claimed::Witness { x },
        b"claim_narrowing",
        &mut rng,
    )?;
    claimed::verify(&instance, &claimed_proof, b"claim_narrowing")?;

    assert_eq!(claimed_proof.len(), plain_proof.len());
    Ok(claimed::verify(
        &instance,
        &plain_proof,
        b"claim_narrowing",
    )?)
}

/// A conjoined term-free equation that does not hold makes the instance
/// invalid, for the prover and the verifier alike -- an error, not a
/// panic and not a proof that fails to verify later.
#[test]
fn false_conjoined_claim_is_an_error() {
    sigma_compiler! { claimed,
        (x),
        (C, D, E, const cind A),
        C = x*A,
        D = E,
    }

    let mut rng = rand::thread_rng();
    let A = G::hash_from_bytes::<Sha512>(b"Generator A");
    let D = G::hash_from_bytes::<Sha512>(b"Element D");
    let E = G::hash_from_bytes::<Sha512>(b"Element E");
    let x = Scalar::random(&mut rng);
    let C = x * A;

    let instance = claimed::Instance { C, D, E, A };
    claimed::prove(
        &instance,
        &claimed::Witness { x },
        b"claim_narrowing",
        &mut rng,
    )
    .unwrap_err();
    claimed::verify(&instance, &[], b"claim_narrowing").unwrap_err();
}

/// Under a disjunction the claim leaf stays: the branch has to be
/// simulatable when its claim is false, and the proof must look the
/// same either way.
#[test]
fn disjunctive_claim_keeps_constant_shape() -> Result<(), Box<dyn std::error::Error>> {
    sigma_compiler! { proof,
        (x),
        (C, D, E, const cind A),
        OR (
            D = E,
            C = x*A,
        )
    }

    let mut rng = rand::thread_rng();
    let A = G::hash_from_bytes::<Sha512>(b"Generator A");
    let D = G::hash_from_bytes::<Sha512>(b"Element D");
    let E = G::hash_from_bytes::<Sha512>(b"Element E");
    let x = Scalar::random(&mut rng);
    let C = x * A;

    // The second disjunct is the real one in both runs; only the truth
    // of the first disjunct's claim differs.
    let mut sizes = Vec::new();
    for E in [D, E] {
        let instance = proof::Instance { C, D, E, A };
        let proof = proof::prove(
            &instance,
            &proof::Witness { x },
            b"claim_narrowing",
            &mut rng,
        )?;
        proof::verify(&instance, &proof, b"claim_narrowing")?;
        sizes.push(proof.len());
    }
    assert_eq!(sizes[0], sizes[1]);
    Ok(())
}