R1CS circuit for Falcon signature verification.

Overview

Falcon R1CS

This crate generates the R1CS circuit for Falcon signature verifications.

Performance

The total #constraints for a single Falcon-512 signature verification is listed below. The table can be obtained via

cargo run --release --example constraint_counts
# instance variables # witness #constraints
ntt conversion 0 14848 15360
verify with ntt 1025 78386 81460
verify with schoolbook 1025 312882 315956

In comparison, an ECC scalar multiplication over Jubjub curve (~256 bits) takes a little over 3k constraints (example here). So this will be something like 10 times more costly than proving, say, Schnorr over Jubjub curve.

Pseudocode for NTT based verification

// signature; requires 1 ntt conversion circuit
u := sig
u_var = u.into_circuit()
u_ntt_var = ntt_circuit(u)

// public key; no ntt conversion circuit is required
h := pk              
h_ntt = ntt(h)                    
h_ntt_var = h_ntt.into_circuit()

// hash of the message; no ntt conversion circuit is required
hm = hash_message(msg, nonce) 
hm_ntt = ntt(hm)
hn_ntt_var = hm_ntt.into_circuit()

// compute v = hm + u * h in the clear
v =  hm + u * h

// compute v = hm + u * h with circuit
v_ntt_var = hm_ntt_var + u_ntt_var * h_ntt_var

// enforce v_ntt_var is indeed v, requires 1 ntt conversion
v_var = v.into_circuit()
v_ntt_var.is_equal( ntt_circuit(v_var) )

// enforce the l2 norm constraints
l2_norm_var = compute_l2_norm(v_var, u_var)
l2_nrom_var.is_smaller( L2_NORM_BOUND )

Pseudocode for NTT conversion

The following code implements NTT circuit with just 15K constraints. The component is

  • n log(n) number of native field arithmetics
  • n number of non-native field arithmetics In comparison, a previous version here takes n log(n) number of non-native field arithmetics. Since a non-native operation is around 30 times more costly than a native one, we can fairly claim that this code achieves almost linear cost for NTT circuit; and improves upon the previous version by a factor of ~log(n).

The core idea is to handle the first while loop with native field arithmetic. A subtly is how to compute a negation of an integer without modulo arithmetics. For an integer v, and for a given round l, we need to proper bound the max value of the current loop, i.e., bound := 2^l * q^{l+1}, and use this bound, which is also a multiple of q to subtract v, i.e., neg_v = bound - v. Know the bound for u, v and neg_v gives us a bound for output for the current round, which recursively gives the bound for next round.

// the  constant wires are [q, 2*q^2, 4 * q^3, ..., 2^9 * q^10]
let mut output = input.to_vec();
let mut t = 512;
for l in 0..9 {
    let m = 1 << l;
    let ht = t / 2;
    let mut i = 0;
    let mut j1 = 0;
    while i < m {
        let s = param[m + i].clone();
        let j2 = j1 + ht;
        let mut j = j1;
        while j < j2 {
            // for the l-th loop, we know that all the output's
            // coefficients are less than q^{l+1}
            // therefore we have
            //  u < 2^l * q^{l+1}
            //  v < 2^l * q^{l+2}
            // and we have
            //  neg_v = q^{l+2} - v
            // note that this works when q^10 < F::Modulus
            // so all operations here becomes native field operations
            let u = output[j].clone();
            let v = &output[j + ht] * &s;
            let neg_v = &const_vars[l + 1] - &v;

            // output[j] and output[j+ht]
            // are between 0 and 2^{l+1} * q^{l+2}
            output[j] = &u + &v;
            output[j + ht] = &u + &neg_v;
            j += 1;
        }
        i += 1;
        j1 += t
    }
    t = ht;
}

// perform a final mod reduction to make the
// output into the right range
// this is the only place that we need non-native circuits
for e in output.iter_mut() {
    *e = mod_q(cs.clone(), e, &const_vars[0])?;
}
You might also like...
Rust implementation of {t,n}-threshold ECDSA (elliptic curve digital signature algorithm).
Rust implementation of {t,n}-threshold ECDSA (elliptic curve digital signature algorithm).

Multi-party ECDSA This project is a Rust implementation of {t,n}-threshold ECDSA (elliptic curve digital signature algorithm). Threshold ECDSA include

Cryptographic signature algorithms: ECDSA, Ed25519

RustCrypto: signatures Support for digital signatures, which provide authentication of data using public-key cryptography. All algorithms reside in th

ECDSA Signature Server

Simple REST API used for serving ECDSA signatures to prevent automation software from minting NFTs in bulk.

An ECDSA threshold signature algorithm implemented in Rust.
An ECDSA threshold signature algorithm implemented in Rust.

Open TSS This project is a Rust implementation of multi-party {t,n}-threshold signature scheme(TSS). The current version of this library supports ECDS

Fast and efficient ed25519 signing and verification in Rust.
Fast and efficient ed25519 signing and verification in Rust.

ed25519-dalek Fast and efficient Rust implementation of ed25519 key generation, signing, and verification in Rust. Documentation Documentation is avai

deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!
deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!

Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889 About Creusot is a tool for deductive verification of Rust code. I

Cover is an open internet service for canister code verification on the Internet Computer
Cover is an open internet service for canister code verification on the Internet Computer

Cover Cover (short for Code Verification) is an open internet service that helps verify the code of canisters on the Internet Computer. Visit our webs

An implementation of NZ COVID Pass verification written in Rust

NZCP Rust   An implementation of NZ COVID Pass verification, New Zealand's proof of COVID-19 vaccination solution, written in Rust 🦀 We also have a J

Independent verification of binary packages - reproducible builds
Independent verification of binary packages - reproducible builds

rebuilderd(1) Independent verification system of binary packages. Accessing a rebuilderd instance in your browser Scripting access to a rebuilderd ins

Simple verification of Rust programs via functional purification in Lean 2(!)
Simple verification of Rust programs via functional purification in Lean 2(!)

electrolysis About A tool for formally verifying Rust programs by transpiling them into definitions in the Lean theorem prover. Masters thesis: Simple

sg = Steam Guard, access sg verification code locally.

Steam Guard CLI Access your Steam Guard token locally. Credit https://github.com/steevp/UpdogFarmer/blob/master/app/src/main/java/com/steevsapps/idled

Shellfirm - Intercept any risky patterns (default or defined by you) and prompt you a small challenge for double verification
Shellfirm - Intercept any risky patterns (default or defined by you) and prompt you a small challenge for double verification

shellfirm Opppppsss you did it again? 😱 😱 😰 Protect yourself from yourself! rm -rf * git reset --hard before saving? kubectl delete ns which going

A certificate verification library for rustls that uses the operating system's verifier

rustls-platform-verifier A Rust library to verify the validity of TLS certificates based on the operating system's certificate facilities. On operatin

A certificate verification library for rustls that uses the operating system's verifier

rustls-platform-verifier A Rust library to verify the validity of TLS certificates based on the operating system's certificate facilities. On operatin

RSA dependency for rust, with cert verification

About Project End to End encryption (RSA) for multiple languages (cross-platform) with double encryption and double decryption methods Icon Item 🥳 Up

Owner
zhenfei
cryptographer, blockchain engineer, rustacean.
zhenfei
Rust-verification-tools - RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.

Rust verification tools This is a collection of tools/libraries to support both static and dynamic verification of Rust programs. We see static verifi

null 249 Nov 6, 2022
Arkworks bindings to Circom's R1CS, for Groth16 Proof and Witness generation in Rust.

ark-circom Arkworks bindings to Circom's R1CS, for Groth16 Proof and Witness generation in Rust.

Georgios Konstantopoulos 123 Nov 14, 2022
R1cs-tutorial - Tutorial for writing constraints in the `arkworks` framework

Introduction to SNARK Development with `arkworks` In this tutorial, we will learn how to write applications for use with state-of-the-art zkSNARKs usi

arkworks 104 Nov 28, 2022
zkSnark circuit compiler

Quickstart ==> Get started here ℹ Important deprecation note The old circom compiler written in Javascript will be frozen, but it can still be downloa

iden3 633 Dec 5, 2022
Logimu: Circuit & logic gate simulator

Logimu: Circuit & logic gate simulator The main goal of Logimu is to simulate large circuits at a high speed. Features Live simulation Embed other cir

David Hoppenbrouwers 4 Nov 20, 2022
Damavand is a quantum circuit simulator. It can run on laptops or High Performance Computing architectures, such CPU distributed architectures or multi GPU distributed architectures.

Damavand is a quantum circuit simulator. It can run on laptops or High Performance Computing architectures, such CPU distributed architectures or multi GPU distributed architectures.

MichelNowak 0 Mar 29, 2022
Damavand is a quantum circuit simulator. It can run on laptops or High Performance Computing architectures, such CPU distributed architectures or multi GPU distributed architectures.

Damavand is a code that simulates quantum circuits. In order to learn more about damavand, refer to the documentation. Development status Core feature

prevision.io 6 Mar 29, 2022
Pure Rust implementation of the Leighton Micali Signature scheme.

Leighton-Micali Hash-Based Signatures LMS implementation in Rust according to the IETF RFC 8554. This implementation is binary compatible with the ref

Fraunhofer AISEC 6 Jun 2, 2022
`decaf377-rdsa` is a randomizable signature scheme using the `decaf377` group.

decaf377-rdsa is a variant of RedDSA, instantiated using the decaf377 group. Signatures are parameterized by domain (for instance, Binding and SpendAu

Penumbra 8 Oct 25, 2022
Finds matching solidity function signatures for a given 4 byte signature hash and arguments.

Finds matching solidity function signatures for a given 4 byte signature hash and arguments. Useful for finding collisions or 0x00000000 gas saving methods (though there are better techniques for saving gas on calldata)

null 71 Dec 4, 2022