MCSat Approaches for Solving Non-linear Modular Arithmetic

on YouTube ↗47m

" summary

Presents two concrete MCSat-based solvers: PolySAT in Z3, a word-level bitvector solver that keeps variable domains as symbolic intervals, extracts forbidden intervals from linear occurrences, and already handles some 256-bit smart-contract patterns though many shapes still fall back to bit-blasting; and FFSAT prototype, a finite-field engine that builds explanations by eliminating the top variable using subresultant regular subchains (SRS) computed via Sage, compares against Gröbner-basis runs, and shows promise on random q benchmarks but currently struggles to scale to larger field sizes.

AI-written summary · about

" chapters (14)

1. 0:00Start
2. 2:30Solving polynomial equations
3. 5:27MCSAT based approaches for non-linear modular arithmetic
4. 8:20MCSat - Idea
5. 15:37Variable Elimination
6. 16:43Single incompatibility
7. 18:05Coefficient based explanation generation
8. 21:46Example: SRS
9. 32:28Bitvector Pitfalls
10. 34:04Solving Approaches
11. 34:52Bitvector Constraints in PolySAT
12. 36:51How to choose values?
13. 39:00Forbidden Interval Lemma
14. 40:57Conflict Resolution Strategy

" related talks

• 40mPost-QuantumJames Howe, Thomas Prest, Thijs Laarhoven, Corentin Jeudy · RSAC 2021
• 32mSymmetric Cryptanalysis IJunjie Cheng, Juan Grados · RSA Conference 2023
• 01h 08mTutorial on Proof SystemsAbhishek Jain · Minimal Complexity Assumptions for Cryptography 2023
• 01h 04mExplicit SoS Lower Bounds from (Small-Set) High Dimensional ExpandersMax Hopkins · Beyond the Boolean Cube 2023
• 01h 02mObfuscation IIAmit Sahai · Cryptography Boot Camp 2015
• 01h 16mMultilinear Maps Over the Integers: From Design to SecurityTancrède Lepoint · The Mathematics of Modern Cryptography
• 01h 32mThe Short Integer Solutions Problem and Cryptographic ApplicationsDaniele Micciancio · Lattices: Algorithms, Complexity, and Cryptography Boot Camp 2020
• 01h 08mSecure Computation 1Peter Scholl · Cryptography 10 Years Later: Obfuscation, Proof Systems, and Secure Computation Boot Camp 2025