Does anybody have some hints where I can use Z3 to prove rules in multiple nested firewall layers?
I found the article about Azure using Z3 to manage the combination of firewall rules fascinating, and I wonder if there is similar stuff out there.
Idea is that a product team can self service their firewall rules after they successfully validated them against the “firewall oracle” implemented in Z3.
I'm not super informed about this but never thought of Z3 and Coq as even being related.
As far as I know, Z3 is a platform that allows one to run a variety of proving algorithms, from SAT solvers to whatever. Basically, it's function is "doing things for you".
Coq is called an "automated theorem prover" but really it's a platform to allow broad mathematical theories to be stated and their proofs verified. It's function isn't doing things for you, it's function is "showing you did things".
But I guess, it seems, Coq has facilities like Z3. So you can translate a Z3 tutorial into Coq.
Coq is usually called an interactive theorem prover, not an automated prover. Interactive provers tend to accumulate varying degrees of automation.
Coq is a project at the scale of other niche programming languages. It is more of a platform than Z3 is. Z3 is more of a solver than a platform.
Coq has many, many moving parts. At it's core it has a dependently typed functional programming language and specification language called Gallina. But around that is built something called the tactic system, which slightly or signifcantly automates proof steps. On top of that there are scripting system like Ltac or plugins for specialized solvers. Coq also basically requires IDE support of sorts, as the proving process is a kind of REPL converation with the system.
Coq is vastly more expressive than Z3, so it makes sense that anything expressible in Z3 is expressible in Coq. What may be more surprising to people who have taken introductory tutorials is that there is significant automation in Coq, it just takes more effort and expertise than Z3's. In principle Coq could use Z3 as a plugin https://smtcoq.github.io/ but the other direction would make no sense at the moment. Z3 is the better choice for large scale but conceptually simple queries or proofs, such as a theorem just involving linear inequalities, arrays, Ands, and Ors, or for solving constraint problems. Coq is the better choice for almost anything more complex than that.
I do agree that they are usually not mentioned as competitors. Z3 does indeed basically find things, and Coq does mostly just verify things and not find them for you.
For everyone asking the difference, see that Coq, which is build on CIC, encompasses everything Z3 could do but also a much more. It's perfectly visualized with Lambda cube[1].
Coq can do everything Z3 does (with a few axioms mixed in)... except for the fast automation a SMT solver is all about :-). The decidable logic fragment Z3 was king on for more than a decade — uninterpreted functions, linear arithmetic, arrays, bitvectors, and more recently datatypes, is quite restricted but for formulas that fit in it (possibly after encoding) Z3 will steamroll Coq's automation.
That is, unless you use CoqHammer which just calls Z3 or cvc4 from Coq, of course.
This is a nice article. We use z3 at work (to solve client specific resource allocation problems with certain business constraints), and I personally have been interested in looking at Coq. Looking at the other comments it seems like there might be an expressive-ness vs compute time tradeoff, but worth exploring for some of the harder problems I guess.
What's the advantage of Coq over Z3? I've spent a fair amount of time working on logic solvers with the Python Z3 bindings, so I have some bias, but the Z3 syntax here is far more readable to me. Are there actual advantages to the Coq solver or syntax?
They actually have different enough use cases and abilities that it is rare to consider them as competitors.
The logic of Coq is vastly more expressive and it's proof process is vastly more controllable.
All of this comes at the cost of level of expertise required and ease and scale of automation.
I'm a big fan of Z3 clearly, but there are entire realms of human thought that can be clearly encoded into Coq that basically cannot in Z3.
You can in principle be fairly expressive in Z3Py if you use quantifiers freely and python as kind of a macro system but it is clunky and Z3 won't actually be able to solve convoluted quantifier usage, at which point you're sunk. You may at that point start to try to split up your theorem into pieces, but then you are building an ad hoc theorem prover that isn't quite just Z3.
In Coq, there is always the ability to appeal to the effort and ingenuity of the programmer/prover.
Coq has a much better ability to deal with the infinite, induction, and symbolic manipulation. It is also an entire programming language in its own right that you can run or extract to OCaml.
Another difference is the de Bruijn criterion. Proofs from a prover are only as trusted as the code of the prover itself. The "trusted core" of Coq is small, a few thousand lines of code. Whereas Z3 is not designed with this in mind, and there is no trusted core of Z3. You have to trust basically all of it. This point does not personally bother me that much, but other people find it important
One of the Coq downsides is the speed. Partially because of the higher level computations, but also partially because of the OCaml. I hope, OCaml Multicore will help the cause significantly.
Is/Are there projects like Coq but with a similar aim to Z3? (I.e. being embedded into other things, with an API). I'm not exactly sure what I'm looking for since I'm not an expert in theorem proving.
It's a question I hadn't really considered before. On first pass, as far as I know, I'd say the answer is no. It isn't clear to me what the objective of embedding Coq with a C api for example would be. The very core of Coq is about verifying proofs and not producing them and I'm not sure what the benefit of embedding it is.
Having said that there are a few projects that may be something like what you're asking. First off, Coq has the SerAPI project https://github.com/ejgallego/coq-serapi through which external programs can talk to coq. This has been used for example to make a python OpenAi gym like interface https://github.com/princeton-vl/CoqGym.
A different direction might be something like MetaMath Zero https://arxiv.org/abs/1910.10703 which is intended to be a small and fast verifier for it's language, perhaps maybe someday for embedding in applications. There is this notion of "Proof Carrying Code" which I don't really know what the current state of the art is. https://en.wikipedia.org/wiki/Proof-carrying_code One might want an easily embeddable trusted verifier for that purpose. I don't know.
You should check out sasyLF. It has a eclipse plugin as well. If you are interested in learning about proof checkers it's a good starting point. My PhD advisor is it's maintainer.
To formally verify simple things where a simple SMT solver does the job, why do you need a 40-year old beast like Coq? Even the very title of the article doesn't make much sense: why would you _want_ to translate Z3 to Coq? Coq is useful, not just for formally verifying things that are far more complicated, but also for formalising (simple) pure mathematical constructs (ref: the HoTT effort). Coq was used to formally verify an entire C compiler (ref: CompCert), which was a landmark achievement.
If you're looking for a middle-ground between SMT automation and proving things that automation fails at, see efforts like F*. There are several proof assistants that use Z3 as a backend.
Coq is the oldest and most mature proof assistant. There are simpler alternatives like Agda, Isabelle, and Lean, each with their own downsides for the simplicity that they offer. For instance, cubical type theory has been formalised in Agda, but I'm currently working on a project to formalise semi-cubical sets in Coq, a project that has been running for a year, and might not be completed.
Coq has a very advanced dependently-typed system, but as a result, the Coq unifier is heuristic-based, and fails at certain points without good diagnostics. That's where the Coq tactic system Ltac2 steps in: there is no other proof assistant that has such such an advanced tactic language.
TL;DR: Coq is a 40-year old ageing beast, and there is nothing quite as powerful. However, even it is immature when it comes to formalising higher categories or other similar graduate-level mathematics. It's painful to work with, because of the number of warts it has accumulated, but there is simply no alternative.
> Even the very title of the article doesn't make much sense: why would you _want_ to translate Z3 to Coq?
You misread both the title and the article itself. It's not about some sort of general translation from Z3 to Coq. It's about translating examples from a tutorial to compare certain introductory proofs and (for the SEND+MORE=MONEY) problem solving strategies.
Idea is that a product team can self service their firewall rules after they successfully validated them against the “firewall oracle” implemented in Z3.
Somehow a mix of Z3 and OpenPolicyAgent.
Link to Azure/Z3 https://medium.com/@ahelwer/checking-firewall-equivalence-wi...