Vibe ECSDA in SimplicityHL

vibe_ecdsa.simf

fn not(bit: bool) -> bool {
    <u1>::into(jet::complement_1(<bool>::into(bit)))
}

// ECDSA verify over secp256k1.
// Returns by asserting validity (panics on failure).
fn ecdsa_verify_raw(msg32: u256, pk_x: u256, pk_y_is_odd: u1, r: u256, s: u256) {
    // 1) Range checks: r,s in [1, n-1]
    let r_s: Scalar = r;
    let s_s: Scalar = s;

    assert!(not(jet::scalar_is_zero(r_s)));  // reject r == 0
    assert!(not(jet::scalar_is_zero(s_s)));  // reject s == 0

    let r_can: u256 = <u256>::into(jet::scalar_normalize(r_s));
    let s_can: u256 = <u256>::into(jet::scalar_normalize(s_s));
    assert!(jet::eq_256(r_can, r));                          // reject r >= n
    assert!(jet::eq_256(s_can, s));                          // reject s >= n

    // 2) w = s^{-1} mod n
    let w: Scalar = jet::scalar_invert(s_s);

    // 3) u1 = msg * w mod n, u2 = r * w mod n
    let z_s: Scalar = msg32;
    let u1: Scalar = jet::scalar_multiply(z_s, w);
    let u2: Scalar = jet::scalar_multiply(r_s, w);

    // 4) Lift pubkey: P from (parity, x)
    let x_fe: Fe = jet::fe_normalize(<Fe>::into(pk_x));
    let p_ge: Ge = match jet::decompress((pk_y_is_odd, x_fe)) { Some(g: Ge) => g, None => panic!(), };

    // Put P into Jacobian using infinity + P
    let p_gej: Gej = jet::gej_ge_add(jet::gej_infinity(), p_ge);

    // 5) R = u2 * P + u1 * G
    let R: Gej = jet::linear_combination_1((u2, p_gej), u1);
    assert!(not(jet::gej_is_infinity(R)));   // reject R at infinity

    // 6) Check r == x(R) mod n
    let R_aff: Ge = match jet::gej_normalize(R) { Some(v: Ge) => v, None => panic!(), };
    let (xR_fe, yR_fe): (Fe, Fe) = R_aff;
    let xR_u256: u256 = <u256>::into(jet::fe_normalize(xR_fe));
    let xR_s: Scalar = xR_u256;                   // this reduces x mod n
    let xR_can: u256 = <u256>::into(jet::scalar_normalize(xR_s));
    assert!(jet::eq_256(xR_can, r));
}