Pith. sign in

REVIEW 3 major objections 6 minor 87 references

Integer Reasoning Modulo Different Constants in SMT

T0 review · 3 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper establishes a sound and terminating refutation calculus for systems of integer polynomial equalities and disequalities modulo different constants, and shows experimentally that its implementation outperforms existing solvers on…

desk verdict A genuinely new lifting/lowering refutation calculus for multimodular integer systems, with a sound core, but the reported implementation leans on an unproven ILP approximation and unexamined Singular assumptions over composite moduli. read the letter →

arxiv 2505.14998 v1 pith:AYXYFUVO submitted 2025-05-21 cs.LO

Elizaveta Pertseva , Alex Ozdemir , Shankara Pailoor , Alp Bassa , Sorawee Porncharoenwase , Işil Dillig , Clark Barrett This is my paper · ORCID
classification cs.LO MSC 03B7013P1068Q60
keywords SMTsolvingmultimodulararithmeticGröbnerbasesliftingandloweringrefutationcalculuscryptographicverificationintegerunsatisfiability
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Systems that mix constraints modulo different constants, such as arithmetic modulo a power of two in an implementation and modulo a large prime in a specification, are hard for existing SMT solvers. This paper proposes a refutation procedure that splits such a system into one subsystem per modulus, uses algebraic ideal-membership tests inside each subsystem, and shares lemmas across subsystems by lifting constraints to integer arithmetic and lowering them back into other moduli. The paper proves the calculus sound and terminating and gives a partial completeness theorem for its weighted Gröbner basis method of finding liftable equalities. On unsatisfiable benchmarks from Montgomery arithmetic and zero-knowledge proof implementations, the procedure solves more instances than existing QF_NIA, QF_BV, and QF_FF solvers, including 76 instances that no other tested solver solves.

What carries the argument

The object that carries the argument is the refutation calculus over configurations (B, R≈∞, R≠∞, R≈n1, R≠n1, . . .), where each R≈n holds expressions representing equalities modulo n and R≠n holds disequalities. The central mechanism is the lifting/lowering pair: Lemma 1 lifts e mod n ≈ 0 to an integer equality e ≈ 0 when the polynomial e lies in the modulus-n ideal and the interval-arithmetic bound CalcBds(B, e) lies in [1 − n, n − 1]; Lemma 3 lowers any entailed integer equality into every modulus; Lemma 4 lowers disequalities under the same range condition. To find polynomials worth lifting, the paper uses a weighted reverse-lexicographic monomial order with weights log(max(|B(xi)1|, |B(xi)2|) + ε), which makes monomials with small ranges small in the order, biasing Gröbner basis generators toward near-zero, liftable polynomials. A complementary method encodes the search for a liftable linear combination of existing expressions as an integer linear constraint system. The lowering rules use the signed-remainder rewrite simpn(e), which replaces every integer constant in e by its remainder modulo n and thereby simplifies equations inside each modulus-n subsystem.

What would settle it

Force the algebra engine to time out on a known-satisfiable system with composite modulus 6, where the relevant equation follows only after a polynomial combination that the timeout misses, and check whether the procedure ever reports unsat; a wrong result would show the fallback set-inclusion test is unsound in practice.

Watch

Extended reading notes

Core claim

The central claim is that multimodular unsatisfiability can be refuted by per-modulus algebra plus lemma exchange rather than by monolithic nonlinear integer reasoning. The calculus keeps, for each modulus n and for the integers themselves, a set of equalities, a set of disequalities, and a variable bound map; it refutes when a modulus-n ideal contains 1, when an active disequality lies in that ideal, or when bounds clash; and it grows the subsystems by lifting, adding e = 0 to the integer subsystem when e mod n = 0 is entailed and the range of e lies within [1 − n, n − 1], and by lowering, adding the simplified remainder of e to a modulus-n subsystem when e = 0 is entailed. The paper proves local soundness of every rule and hence Theorem 1: a closed derivation tree with root C certifies that C is unsatisfiable in integer arithmetic. It also proves termination on finite configurations with bounded variables, and Theorem 3, a partial completeness result: with a weighted reverse-lexicographic Gröbner basis, if every generator whose leading monomial has small range corresponds to a liftable equality, then all liftable equalities in the ideal are found. On the released benchmarks, the weighted-Gröbner configuration solves 255 of 336 unsatisfiable instances, ahead of the next-best solver's 190, and wins 5 of the 7 benchmark categories.

Load-bearing premise

The load-bearing premise is that the algebra engine is always correct about which polynomial equations follow from the others, for every modulus, prime or composite; if the engine times out and falls back to a weaker check, the refutation may be wrong.

Editorial extensions

If this is right

  • A closed derivation tree in this calculus is a checkable certificate of unsatisfiability in integer arithmetic, independent of the engine that found it.
  • Weighted Gröbner lifting is complete whenever every generator with a small-range leading monomial lifts; in that case the method provably discovers all liftable equalities hidden in the modulus-n ideal.
  • The integer-linear-constraint encoding for liftable linear combinations is exact in theory, so the search for liftable equalities of that form is a finite integer programming problem.
  • The reported experiments support using this procedure as a dedicated theory solver for the multimodular fragment rather than encoding modular constraints with auxiliary variables into general nonlinear integer arithmetic.
  • On the f/f(s), f/f(m), f/b(s), and b/f(m) families, the procedure solves substantially more instances than the best QF_NIA, QF_BV, and QF_FF baselines, including all determinism benchmarks in f/f(s) and b/f(m).

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper, the same lifting calculus should transfer to satisfiability-oriented search: since lifting adds integer equations only when equisatisfiability is preserved, a model-building version could use the lifted integer system to restrict the search space, a direction the paper explicitly leaves open.
  • The failure profile on f/b(m), which accounts for 34 of the 81 unsolved instances, suggests a concrete experiment: add the unweighted Gröbner basis to the weighted candidate pool for that family, since the paper's own ablation shows the unweighted method lifts more equalities there.
  • The bound-dependent weight scheme is a general recipe for any ideal-membership procedure with interval information: it biases basis computation toward low-range witnesses and could be reused outside modular reasoning, for instance in polynomial reasoning over the reals.
  • A practical engineering consequence, not drawn by the paper, is that the 30-second Gröbner-basis timeout is the most likely place for the practical procedure to lose either completeness or soundness; replacing the black-box engine with an incremental basis computation could remove that fallback entirely.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper introduces QF_MIA, a fragment of non-linear integer arithmetic with explicit modular equalities and disequalities, and presents a refutation procedure for multimodular systems. The procedure partitions constraints by modulus, maintains variable bounds, and exchanges information across subsystems through lifting and lowering lemmas (Lemmas 1–4). The resulting calculus is proved sound (Theorem 1) and terminating (Theorem 2). Two lemma-generation strategies are described: a weighted Gröbner basis method (Section 5.4, Theorem 3) and an integer linear programming method (Section 5.5, Theorem 4). The procedure is implemented in cvc5 using Singular for Gröbner bases and GLPK for the integer linear constraints, and is evaluated on cryptographic benchmarks from Montgomery arithmetic and zero-knowledge proof implementations. The best configuration reports 255 total unsat solves, compared with 190 for z3 and 166 for cvc5 on the same benchmarks, with 76 unique solves.

Significance. If the empirical claims hold, the paper delivers a genuinely useful new solver architecture for a class of constraints that is important in cryptographic verification and that existing SMT solvers handle poorly. The theoretical core is attractive: the lifting/lowering lemmas are simple yet effective, the calculus is locally sound, the termination measure is natural, and the paper is honest about the incompleteness of its lifting strategies. The use of external benchmark families and a fixed formula for the monomial-order weights avoids circularity in the experimental evaluation. The main reasons for not recommending acceptance now are not in the calculus itself but in the soundness evidence for the implemented system: the reliance on composite-modulus Gröbner bases from Singular and the use of an approximate ILP encoding whose soundness is not established.

major comments (3)
  1. [Section 6 and Table 2] The main empirical result depends on Singular computing strong Gröbner bases in Z_n[X] for composite n. The f/b(s) and f/b(m) families use moduli of the form 2^b and account for 67 of the 255 solves in Table 2. The rules UnsatOne, UnsatDiseq, and LiftEq all require exact ideal-membership or ideal-generation checks, so a false positive in Singular's Gröbner basis computation would make the solver return unsat for a satisfiable instance. The paper gives no independent evidence that Singular computes correct strong reduced Gröbner bases over Z_n[X] for composite n, nor any validation strategy. Please add a concrete validation, for example by checking the implementation on composite-modulus instances with independently known satisfiability status, or by restricting the empirical claims to prime moduli, or by providing an independent verification of the ideal-membership results.
  2. [Section 6 / Appendix E / Table 3] The ILP-based lifting used in the experiments is an approximate version in which constants are scaled by slog2, and Appendix E states that all experimental results use this relaxation. Theorem 4 proves the soundness of the exact encoding only. The paper does not state whether the candidate coefficient vectors produced by the approximate encoding are subsequently checked against the exact LiftEq premises before being added to R_∞. If they are not checked, the Lin. Constraints and hybrid rows of Table 3 may include unsound solves. Please specify the filtering mechanism, or prove that the approximation preserves the soundness condition, or remove the unsound configuration from the experimental claims. This does not affect Table 2, whose best configuration uses the weighted Gröbner basis only, but it affects the secondary claim that the ILP method is a viable supplementary lifting strategy.
  3. [Section 5.4, Eq. (2)] The weighted monomial order uses weights log(max(|B(x_i)_1|, |B(x_i)_2|) + ε/4). If any variable has both bounds equal to 0, and ε is chosen in the usual small range (0 < ε < 4), the assigned weight is negative. A monomial order is required to satisfy 1 ≤ m for every monomial, and negative weights can violate this condition, so the object computed with Eq. (2) may not be a Gröbner basis in the sense used by the calculus. Since Theorem 3 and the weighted-GB configuration depend on Eq. (2) defining a monomial order, please state the permitted range of ε and prove that the resulting weights are nonnegative, or modify the formula to guarantee that property.
minor comments (6)
  1. [Figure 4, ConstrBds] The ConstrBds rule divides by a but does not state a ≠ 0; the premise should include this condition, and the written premise contains the typo B(x_i)_w instead of a defined bound component.
  2. [Section 3.2 / Section 5.1] The paper says CalcBds returns the maximum and minimum possible values of an expression, but the rules only require an over-approximation from interval arithmetic; the wording should make clear that CalcBds is an interval-arithmetic over-approximation, since the soundness arguments rely on this over-approximation property.
  3. [Appendix B, termination proof] The termination proof calls the lexicographic order on ideals 'total', but the ideal-order component is defined by strict inclusion and is only a partial order; this does not affect the well-foundedness argument, but the text should say 'well-founded partial order' rather than 'total well-founded order'.
  4. [Section 5.5] The indices in the definition of Φ are inconsistent: the sum over monomials is written with index i while i already indexes the expressions e_i; the summation over monomials should use a distinct index, and the number of monomials is t, not k.
  5. [Appendix C, Lemma 5 proof] The proof of Lemma 5 has several transcription errors, including a stray '5' after a displayed equation and an omitted closing parenthesis in the definition of w(JmK); these should be corrected for readability.
  6. [Section 5.4] The text says the weighted Gröbner basis method is 'complete' under the condition in Theorem 3, but the condition is essentially that every generator passing the leading-monomial bound test is liftable; stating this as a 'completeness guarantee' is potentially misleading and should be phrased as a conditional completeness result.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: the calculus is proven locally, the monomial-order weights are a closed-form function of bounds, and the benchmarks are external; the few self-citations are background only.

full rationale

The paper's central theoretical claim (Theorem 1, soundness) is established by a local-soundness argument for each derivation rule, relying on standard ideal and interval-arithmetic facts rather than on the experimental results or on a self-citation. The termination proof (Theorem 2) uses a well-founded lexicographic measure. The lifting and lowering lemmas (Lemmas 1-4) are proved directly from equisatisfiability and bound reasoning, not by assuming what they conclude. The weighted Gröbner-basis order in Equation (2) is computed deterministically from variable bounds via a fixed logarithmic formula; it is not fitted to benchmark outcomes. Theorem 3 is a conditional completeness statement whose proof constructs a reduction sequence using properties of the weighted order; it is a genuine mathematical reduction, even if its premise is strong, and the paper openly states that the method lacks general completeness. Theorem 4 is an exact encoding of the linear-combination lifting condition, not a fit. The benchmarks come from external cryptographic sources (Montgomery arithmetic, Succinct Labs, o1-labs, xjSnark), and comparisons are made against independent solvers such as z3, Yices, and bitwuzla. Self-citations to prior finite-field work ([65], [66]) provide background and a comparison baseline; they are not load-bearing for the new calculus. The reliance on Singular for strong Gröbner bases over composite moduli is a legitimate implementation-soundness and correctness risk, but it is not circularity: the empirical claim could fail for tooling reasons without the derivation reducing to its own inputs.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The procedure introduces new algorithmic techniques (lifting, lowering, weighted monomial orders) but no new mathematical entities like particles or forces. The free parameter epsilon is a numerical stabilization constant. The main axioms are standard algebra and the assumption that external tools and benchmarks are correct.

free parameters (1)
  • epsilon in weighted monomial order weights = Unspecified in the paper; a small additive constant used to avoid log(0).
    Equation 2 uses log(max(|B(xi)1|, |B(xi)2|) + epsilon); epsilon is chosen by hand for numerical stability and is not fitted to any benchmark result.
assumptions (4)
  • domain assumption Strong Groebner bases exist and can be computed over principal ideal rings such as Z_n[X]
    Section 3.2 cites Norton and Salagean for strong Groebner bases; the implementation uses Singular to compute these bases over composite moduli.
  • standard math Interval arithmetic (CalcBds) returns sound bounds for polynomial expressions over integer variable bounds
    Section 5.1 defines CalcBds via standard interval arithmetic [45]; soundness is assumed for the lifting and lowering conditions.
  • domain assumption The benchmark formulas from Montgomery arithmetic and ZKP libraries are faithful encodings of real verification tasks
    Section 7.1 describes benchmark generation from published implementations; if the encodings are wrong, the comparison is not meaningful.
  • domain assumption All variables in benchmark instances are bounded, so the termination theorem applies
    Section 7.1 benchmarks use finite ranges; Appendix B proves termination only for configurations where every variable is bounded.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Integer Reasoning Modulo Different Constants in SMT." pith.science (2026). https://pith.science/paper/AYXYFUVO

@misc{pith2026250514998,
  author       = {Pith},
  title        = {Pith review of: Integer Reasoning Modulo Different Constants in SMT},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AYXYFUVO}},
  note         = {Machine review of arXiv:2505.14998}
}
read the original abstract

This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported by algebraic tools like weighted Gr\"obner bases. Our experiments show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related to Montgomery arithmetic and zero-knowledge proofs.

Figures

Figures reproduced from arXiv: 2505.14998 by the authors.

Figure 1
Figure 1. Overview of our refutation procedure. Integer-reasoning interacts with [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The signature and grammar for QF_MIA, a fragment of QF_NIA. 4 A Multimodular Logic Previous work on verifying arithmetic modulo large primes [65, 66] encodes con￾straints using TFF. However, the signature of TFF does not support non-prime moduli or constraints that share variables and use different moduli, limiting the range of problems that can be encoded. Instead, we encode multimodular con￾straints directly in TI… view at source ↗
Figure 3
Figure 3. Encoding rules for a multimodular system [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Derivation rules. e, s are expressions, a ∈ Z, and n ∈ Z + ∞. We present the calculus as rules that modify configurations, as is common in SMT procedures [50, 73]. Here, a configuration is the representation of the system of constraints C as the tuple (B, R≈ ∞, R̸≈ ∞, …
Figure 5
Figure 5. Figure 5: Benchmarks solved over time for top 5 solvers: ours ( [PITH_FULL_IMAGE:figures/full_fig_p018_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

87 extracted references · 79 canonical work pages

  1. [1]

    Abbott and A

    J. Abbott and A. M. Bigatti. CoCoALib: A C++ library for computations in commutative algebra... and beyond. InInternational Congress on Mathematical Software, 2010

    2010

  2. [2]

    Ábrahám, J

    E. Ábrahám, J. H. Davenport, M. England, and G. Kremer. Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings.Journal of Logical and Algebraic Methods in Programming, 119, 2021

    2021

  3. [3]

    Barbosa, C

    H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, and Y. Zohar. cvc5: A versatile and industrial-strength SMT solver. InTACAS, 2022

    2022

  4. [4]

    P. S. Barreto, B. Lynn, and M. Scott. Constructing elliptic curves with prescribed embedding degrees. InSCN, 2003

    2003

  5. [5]

    Barrett, P

    C. Barrett, P. Fontaine, and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016

    2016

  6. [6]

    Barrett and C

    C. Barrett and C. Tinelli. Satisfiability modulo theories. In E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, editors,Handbook of Model Checking, pages 305–343. Springer International Publishing, 2018

    2018

  7. [7]

    P. Barrett. Implementing the rivest shamir and adleman public key encryption algorithm on a standard digital signal processor. InCRYPTO, 1986

    1986

  8. [8]

    Bjørner and L

    N. Bjørner and L. Nachmanson. Arithmetic solving in z3. InCAV, 2024

    work page 2024

Show all 87 references
  1. [9]

    Bosma, J

    W. Bosma, J. Cannon, and C. Playoust. The Magma algebra system I: The user language. Journal of Symbolic Computation, 24(3-4):235–265, 1997

    1997

  2. [10]

    S. Bowe. BLS12-381: New zk-snark elliptic curve construction, Mar. 2017. https://electriccoin.co/blog/new-snark-curve/

    2017

  3. [11]

    Brummayer and A

    R. Brummayer and A. Biere. Boolector: An efficient SMT solver for bit-vectors and arrays. InTACAS, 2009

    2009

  4. [12]

    Buchberger

    B. Buchberger. Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, University of Innsbruck, 1965

    1965

  5. [13]

    Buchberger

    B. Buchberger. A theoretical basis for the reduction of polynomials to canonical forms. SIGSAM Bulletin, 1976

    1976

  6. [14]

    B. F. Caviness and J. R. Johnson.Quantifier elimination and cylindrical algebraic decomposition. Springer Science & Business Media, 2012

    2012

  7. [15]

    Chaliasos, J

    S. Chaliasos, J. Ernstberger, D. Theodore, D. Wong, M. Jahanara, and B. Livshits. SoK: What don’t we know? understanding security vulnerabilities in SNARKs. In USENIX Security, 2024

    2024

  8. [16]

    C. Chin, H. Wu, R. Chu, A. Coglio, E. McCarthy, and E. Smith. Leo: A programming language for formally verified, zero-knowledge applications, 2021. Preprint at https://ia.cr/2021/651

    2021

  9. [17]

    Cimatti, A

    A. Cimatti, A. Griggio, A. Irfan, M. Roveri, and R. Sebastiani. Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM TOCL, 19(3), 2018

    2018

  10. [18]

    Coglio, E

    A. Coglio, E. McCarthy, E. Smith, C. Chin, P. Gaddamadugu, and M. Dellepere. Compositional formal verification of zero-knowledge circuits, 2023. https://ia.cr/2023/1278. Integer Reasoning Modulo Different Constants in SMT 21

    2023

  11. [19]

    Corzilius, G

    F. Corzilius, G. Kremer, S. Junges, S. Schupp, and E. Ábrahám. SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. InSAT, 2015

    2015

  12. [20]

    Dahlgren

    F. Dahlgren. It pays to be Circomspect. https://blog.trailofbits.com/2022/09/15/it-pays-to-be-circomspect/ ,

    2022

  13. [21]

    Davenport

    J. Davenport. The axiom system, 1992

    1992

  14. [22]

    C. David. Ideals, Varieties, and Algorithms-An Introduction to Computational Algebraic Geometry and Commutative Algebra.Undergraduate Texts in Mathematics, 1991

    1991

  15. [23]

    Decker, G.-M

    W. Decker, G.-M. Greuel, G. Pfister, and H. Schönemann.Singular 4-4-0 — A computer algebra system for polynomial computations. http://www.singular.uni-kl.de, 2024

    2024

  16. [24]

    Diffie and M

    W. Diffie and M. E. Hellman. New directions in cryptography.IEEE Transactions on Information Theory, 22(6), 1976

    1976

  17. [25]

    D. S. Dummit and R. M. Foote.Abstract algebra, volume 3. Wiley Hoboken, 2004

    2004

  18. [26]

    Dutertre

    B. Dutertre. Yices 2.2. InCAV, 2014

    2014

  19. [27]

    Eder and T

    C. Eder and T. Hofmann. Efficient Gröbner bases computation over principal ideal rings. Journal of Symbolic Computation, 103:1–13, 2021

    2021

  20. [28]

    Eisenbud, D

    D. Eisenbud, D. R. Grayson, M. Stillman, and B. Sturmfels.Computations in algebraic geometry with Macaulay 2, volume 8. Springer Science & Business Media, 2001

    2001

  21. [29]

    H. B. Enderton.A mathematical introduction to logic. Elsevier, 2001

    2001

  22. [30]

    Erbsen, J

    A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala. Systematic generation of fast elliptic curve cryptography implementations. Technical report, MIT, 2018

    2018

  23. [31]

    Erbsen, J

    A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala. Simple high-level code for cryptographic arithmetic: With proofs, without compromises.ACM SIGOPS Operating Systems Review, 54(1), 2020

    2020

  24. [32]

    J. C. Faugére. A new efficient algorithm for computing Gröbner bases (f4). Journal of Pure and Applied Algebra, 139(1):61–88, 1999

    1999

  25. [33]

    J. C. Faugére. A new efficient algorithm for computing Gröbner bases without reduction to zero (f5). InISSAC. ACM, 2002

    2002

  26. [34]

    Fournet, C

    C. Fournet, C. Keller, and V. Laporte. A certified compiler for verifiable computing. In CSF, 2016

    2016

  27. [35]

    Fränzle, C

    M. Fränzle, C. Herde, T. Teige, S. Ratschan, and T. Schubert. Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation, 1(3-4), 2006

    2006

  28. [36]

    https://www.gap-system.org, this year

    GAP – Groups, Algorithms, and Programming, Version 4.13dev. https://www.gap-system.org, this year

  29. [37]

    C. Gentry. Fully homomorphic encryption using ideal lattices. InSTOC, 2009

    2009

  30. [38]

    Goldwasser, S

    S. Goldwasser, S. Micali, and C. Rackoff. The knowledge complexity of interactive proof systems.SIAM Journal of Computation, 18(1):186–208, 1989

    1989

  31. [39]

    Graham-Lengrand, D

    S. Graham-Lengrand, D. Jovanović, and B. Dutertre. Solving bitvectors with MCSAT: explanations from bits and pieces. InIJCAR, 2020

    2020

  32. [40]

    T. Hader. Non-linear SMT-reasoning over finite fields, 2022. MS Thesis (TU Wein)

    2022

  33. [41]

    Hader, D

    T. Hader, D. Kaufmann, and L. Kovács. SMT solving over finite field arithmetic. In LPAR, 2023

    2023

  34. [42]

    Hader and L

    T. Hader and L. Kovács. Non-linear SMT-reasoning over finite fields. InSMT,

  35. [43]

    M. Hamburg. Ed448-goldilocks, a new elliptic curve, 2015. https://ia.cr/2015/625

    2015

  36. [44]

    Extended Abstract. 22 E. Pertseva et al

  37. [45]

    Hickey, Q

    T. Hickey, Q. Ju, and M. H. Van Emden. Interval arithmetic: From principles to implementation. ACM, 48(5):1038–1068, Sept. 2001

    2001

  38. [46]

    Heck and W

    A. Heck and W. Koepf.Introduction to MAPLE, volume 1993. 1993

    1993

  39. [47]

    Jovanović and L

    D. Jovanović and L. De Moura. Solving non-linear arithmetic.ACM Communications in Computer Algebra, 46(3/4), 2013

    2013

  40. [48]

    Jovanović

    D. Jovanović. Solving nonlinear integer arithmetic with MCSAT. InVMCAI, 2017

    2017

  41. [49]

    Kosba, C

    A. Kosba, C. Papamanthou, and E. Shi. xJsnark: A framework for efficient verifiable computation. InIEEE S&P, 2018

    2018

  42. [50]

    Jovanović and L

    D. Jovanović and L. d. Moura. Cutting to the chase solving linear integer arithmetic. In CADE, 2011

    2011

  43. [51]

    J. Liu, I. Kretz, H. Liu, B. Tan, J. Wang, Y. Sun, L. Pearson, A. Miltner, I. Dillig, and Y. Feng. Certifying zero-knowledge circuits with refinement types,

  44. [52]

    Liang, A

    T. Liang, A. Reynolds, C. Tinelli, C. Barrett, and M. Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. InCAV. Springer

  45. [53]

    Maréchal, A

    A. Maréchal, A. Fouilhé, T. King, D. Monniaux, and M. Périn. Polyhedral approximation of multivariate polynomials using handelman’s theorem. In VMCAI, 2016

    2016

  46. [54]

    N. H. McCoy.Rings and ideals, volume 8. American Mathematical Soc., 1948

    1948

  47. [55]

    Makhorin

    A. Makhorin. GNU linear programming kit version 4.6.0. http://www.gnu.org/software/glpk/glpk.html, 2024

    2024

  48. [56]

    P. L. Montgomery. Modular multiplication without trial division.Mathematics of computation, 44(170):519–521, 1985

    1985

  49. [57]

    L. d. Moura and N. Bjørner. Z3: An efficient SMT solver. InTACAS, 2008

    2008

  50. [58]

    Meurer, C

    A. Meurer, C. P. Smith, M. Paprocki, O. Čertík, S. B. Kirpichev, M. Rocklin, A. Kumar, S. Ivanov, J. K. Moore, S. Singh, et al. Sympy: symbolic computing in python. PeerJ Computer Science, 3:e103, 2017

    2017

  51. [59]

    Niemetz and M

    A. Niemetz and M. Preiner. Ternary propagation-based local search for more bit-precise reasoning. InFMCAD, 2020

    2020

  52. [60]

    Niemetz and M

    A. Niemetz and M. Preiner. Bitwuzla. InCAV, 2023

    2023

  53. [61]

    L. d. Moura and D. Jovanović. A model-constructing satisfiability calculus. In VMCAI, 2013

    2013

  54. [62]

    Niemetz, M

    A. Niemetz, M. Preiner, and Y. Zohar. Scalable bit-blasting with abstractions. In CAV, 2024

    2024

  55. [63]

    G. H. Norton and A. Sˇ alˇ agean. Strong Gröbner bases for polynomials over a principal ideal ring.Bulletin of the Australian Mathematical Society, 64(3):505–528, 2001

    2001

  56. [64]

    Niemetz, M

    A. Niemetz, M. Preiner, A. Reynolds, Y. Zohar, C. Barrett, and C. Tinelli. Towards bit-width-independent proofs in SMT solvers. InCADE, 2019

    2019

  57. [65]

    Ozdemir, G

    A. Ozdemir, G. Kremer, C. Tinelli, and C. Barrett. Satisfiability modulo finite fields. In CAV, 2023

    2023

  58. [66]

    Ozdemir, S

    A. Ozdemir, S. Pailoor, A. Bassa, K. Ferles, C. Barrett, and I. Dillig. Split Gröbner Bases for satisfiability modulo finite fields. InCAV, 2024

    2024

  59. [67]

    Foreign field multiplication gate, 2024

    o1-labs. Foreign field multiplication gate, 2024. https://github.com/o1-labs/rfcs/blob/ eeb8070c9901c611c9a557464022bbf9237900b9/0006-ffmul-revised.md

    2024

  60. [68]

    Pailoor, Y

    S. Pailoor, Y. Chen, F. Wang, C. Rodríguez, J. Van Geffen, J. Morton, M. Chu, B. Gu, Y. Feng, and I. Dillig. Automated detection of under-constrained circuits in zero-knowledge proofs. InPLDI, 2023

    2023

  61. [69]

    Philipoom

    J. Philipoom. Correct-by-construction finite field arithmetic in Coq. PhD thesis, Massachusetts Institute of Technology, 2018

    2018

  62. [70]

    Ozdemir, R

    A. Ozdemir, R. S. Wahby, F. Brown, and C. Barrett. Bounded verification for finite-field-blasting. InCAV, 2023. Integer Reasoning Modulo Different Constants in SMT 23

    2023

  63. [71]

    R. L. Rivest, A. Shamir, and L. Adleman. A method for obtaining digital signatures and public-key cryptosystems.Communications of the ACM, 21(2):120–126, 1978

    1978

  64. [72]

    Schwabe, B

    P. Schwabe, B. Viguier, T. Weerwag, and F. Wiedijk. A Coq proof of the correctness of X25519 in TweetNaCl. InCSF, 2021

    2021

  65. [73]

    W. Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. InSC, 1991

    1991

  66. [74]

    Gnark Plonky2 recursive verifier: The goldilocks field implementation, 2024

    Succinct Labs. Gnark Plonky2 recursive verifier: The goldilocks field implementation, 2024. https://github.com/succinctlabs/gnark-plonky2-verifier/tree/ 7025b2efd67b5ed30bd85f93c694774106d21b3d/goldilocks

    2024

  67. [75]

    C. Tsay, J. Kronqvist, A. Thebelt, and R. Misener. Partition-based formulations for mixed-integer optimization of trained relu neural networks.NeurIPS, 2021

    2021

  68. [76]

    Sheng, A

    Y. Sheng, A. Nötzli, A. Reynolds, Y. Zohar, D. Dill, W. Grieskamp, J. Park, S. Qadeer, C. Barrett, and C. Tinelli. Reasoning about vectors using an SMT theory of sequences. InIJCAR, 2022

    2022

  69. [77]

    Walfish and A

    M. Walfish and A. J. Blumberg. Verifying computations without reexecuting them. Communications of the ACM, 58(2):74–84, 2015

    2015

  70. [78]

    F. Wang. Ecne: Automated verification of ZK circuits, 2022. https://0xparc.org/blog/ecne

    2022

  71. [79]

    V. X. Tung, T. V. Khanh, and M. Ogawa. raSAT: An SMT solver for polynomial constraints. InIJCAR, 2016

    2016

  72. [80]

    H. Wen, J. Stephens, Y. Chen, K. Ferles, S. Pailoor, K. Charbonnet, I. Dillig, and Y. Feng. Practical security analysis of zero-knowledge proof circuits, 2023. https://ia.cr/2023/190

    2023

  73. [81]

    Wolfram.Mathematica: a system for doing mathematics by computer

    S. Wolfram.Mathematica: a system for doing mathematics by computer. Addison Wesley Longman Publishing Co., Inc., 1991

    1991

  74. [82]

    Weispfenning

    V. Weispfenning. Quantifier elimination for real algebra—the quadratic case and beyond. Applicable Algebra in Engineering, Communication and Computing, 8(2), 1997

    1997

  75. [83]

    Zimmermann, A

    P. Zimmermann, A. Casamayou, N. Cohen, G. Connan, T. Dumont, L. Fousse, F. Maltey, M. Meulien, M. Mezzarobba, C. Pernet, et al.Computational mathematics with SageMath. SIAM, 2018. A Proofs of lifting and lowering lemmas. Lemma 1. Let C be a multimodular system with boundsB and...

    2018

  76. [85]

    A. C. Yao. Protocols for secure computations. InFOCS, 1982

    1982

  77. [87]

    ⇐ Assume there exists a linear combination of the forme′ = Pl i=1 aiei, ai ∈ Z and ei ∈ R≈ n s.t e′ is liftable inC and e′ ̸= 0

    By set up ofΦ and properties ofReLU there must exist at least one monomial JmiK ∈ Je′K with a nonzero coefficient and thusJe′K ̸= 0and e′ ̸= 0. ⇐ Assume there exists a linear combination of the forme′ = Pl i=1 aiei, ai ∈ Z and ei ∈ R≈ n s.t e′ is liftable inC and e′ ̸= 0. Sinc...

  78. [2022]

    Accessed: 15 October 2023

    2023

  79. [2023]

    https://ia.cr/2023/547

    2023

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.