Sharing noir-rlwe-gadgets, a Noir/UltraHonk library that proves a BFV ciphertext is a well-formed public-key encryption of a bounded message — the “is this submitted input a valid encryption?” proof an fhEVM-style user needs without holding the FHE secret key.
It proves c0 = [pk0·u + e0 + Δ·m]_q, c1 = [pk1·u + e1]_q with u ternary, ‖e‖∞ ≤ B, m ∈ [0,t), all enforced by in-circuit range checks, using Schwartz-Zippel polynomial-product checks (no in-circuit NTT). At n=1024 it’s ~80k gates / ~0.9 s prove / ~2.5M gas on-chain, with theciphertext as a single hashed public input.
Context vs Zama’s existing tooling: TFHE-rs ships a production ZKPoK for TFHE/compact-PK ciphertexts (Libert-based). This is a different point in the design space — RLWE/BFV, SNARK-based, with a standard on-chain Solidity verifier — and is unaudited research (though the soundness lemmas are written out and the parameters are lattice-estimator-validated). I’d appreciate feedback from anyone thinking about input-validity proofs for FHE coprocessors: which scheme/parameters (BFV vs BGV vs CKKS) and which exact well-formedness statement would be most useful to standardize on.
Repo can be found in my GitHub @AryaEthN.