superVer: Verifying Probabilistic Independence of Systems of Expressions using(…)
summary
superVer implements a Rust tool built on the egg equality‑saturation library to decide when sets of algebraic probes have joint distributions independent of secrets, claiming completeness (no false negatives) by encoding the optimistic sampling rule and adding observation nodes that point to e‑classes instead of merging them. a realization analysis enumerates combinations of observation notes to catch global conflicts across multiple probes. current focus is correctness over speed; prototypes handle Boolean and converted arithmetic (b2a) circuits, outperforming some tools on expressiveness but running slower on larger benchmarks.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:42Probabilistic expressions in crypto
- 2:07Attacker model and probing
- 3:57Optimistic sampling rule
- 5:43Naive rewriting in E-graphs
- 8:14Semantic vs probabilistic rewrites
- 9:41Limitations of naive approach
- 11:12Fixing with observation classes
- 12:58Systems with observation nodes
- 14:24Global context analysis
- 18:09Evaluation and tool comparison
- 19:35Arithmetic circuits via B2A
- 20:39Next steps
- 22:04Q&A
related talks
30mProof Logging for Constraint Programming
01h 08mTutorial on Proof Systems
22mComputational-Bounded Robust Compilation and Universally Composable Security
01h 00mKeynote: Bringing Verified Cryptographic Protocols to Practice
23mSonic: Nearly Trustless SNARK Setups
01h 09mProofs - Practice 1
19mAutomated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs
01h 04mExplicit SoS Lower Bounds from (Small-Set) High Dimensional Expanders