Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs

DOI10.1007/978-3-031-37709-9_8MaRDI QIDQ6535685zbMATH OpenFDO

Authors Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark Barrett

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

Cryptography (94A60) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Stacked garbling for disjunctive zero-knowledge proofs
• Automatic generation of \(\Sigma\)-protocols
• Scalable zero knowledge via cycles of elliptic curves
• Scalable zero knowledge via cycles of elliptic curves
• An efficient ZK compiler from SIMD circuits to general circuits

Cites work

• A formally verified compiler back-end
• A mathematical introduction to logic.
• Automated soundness proofs for dataflow analyses and transformations via local rules
• CakeML
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Marlin: preprocessing zkSNARKs with universal and updatable SRS
• Scalable zero knowledge with no trusted setup
• The knowledge complexity of interactive proof-systems
• The verified CakeML compiler backend
• Towards bit-width-independent proofs in SMT solvers
• Towards satisfiability modulo parametric bit-vectors

This page was built for publication: Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535685)