Zee3 - Bindings to the Z3 theorem prover

That sounds intriguing; I use z3 in Cure ( Type System — Dependently-Typed BEAM Language ) and I might maybe benefit from using this library instead of shelling out.

I didn’t know anyone here was using Z3 for non-trivial tasks, it’s great to see that other people see the use of Z3 (and see the use of avoiding Python when possible).

If you are using Z3 as an interactive theorem prover (i.e. using (push) and (pop)) I think you can benefit. If you run a new instance of Z3 everytime you want to check something, I’m not sure what the real benefit is. I am currently adding an escape hatch to add literal SMT-LIB2 text to the running Z3 process (you can already do that using Port.command, but it’s not part of the public API). Feel free to contribute if you find this useful!

I have just added some new functionality. One can now define functions inside an elixir module, import them into Z3 inside the Zee3.program and use those functions inside the program. These are “real function calls” and not merely the result of expanding the function in Elixir. Here is an example from the test suite:

defmodule Zee3.ProgramTest do
  use ExUnit.Case, async: true
  require Zee3
  alias Zee3.Smt2

  # ... omitted setup stuff

  defmodule AltLib do
    # Hide the Kernel operators and import the Z3 builtins
    use Zee3.StdLib
    # Make the `defzee3` macro available, as well as performing
    # some behind the scenes magic which will allow the program
    # to use this module correctly
    use Zee3.Defzee3

    @doc """
    Defines a Z3 function, which can be invoked if the module
    is used inside a program.
    """
    defzee3 funky_addition(a :: Sort.int(), b :: Sort.int()) :: Sort.int() do
      # Note that this is using the builtin Z3 operators
      # instead of the default Kernel operators
      a * b - 1
    end
  end

  test "functions defined with defzee3 work", %{solver: solver} do
    {{:sat, _model}, func_call} =
      Zee3.program solver do
        # TODO: find a better API than using the module
        use Zee3.ProgramTest.AltLib, with_alias: AltLib

        x = declare_const("x", Sort.int())
        y = declare_const("y", Sort.int())

        # When is funky addition equal to normal addition?
        assert AltLib.funky_addition(x, y) == x + y

        # Now, let's make sure `AltLib.funky_addition/2`
        # returns a Z3 function call instead of expanding
        # the function body itself.
        # To do this, we will call the function and assign
        # the result to a variable and outside the `Zee3.program`
        # we will serialize the contents of the variable.
        func_call = AltLib.funky_addition(x, y)

        {check_sat_and_get_model!(), func_call}
      end

    # The function call returns the internal representation
    # of a function call instead of expanding the
    assert Smt2.serialize(func_call) == "(Zee3.ProgramTest.AltLib.funky_addition x y)"
  end
end

The syntax to import the module is use Full.Path.To.MyModule, with_alias: MyModule (the alias is not optional). Currently the use ... macro is processed in a special way inside the Zee3.program whenever it has a single with_alias: ... option. This means it is not a “real” use macro. If your use macros don’t take a single with_alias: ... option, they will be processed normally. Note that the name of the function defined inside Z3 is the fullly qualified function name to avoid clashes. This allows you to have two modules with functions with the same name.

Dumb naming question: the idiom use Full.Path.MyModule, with_alias: MyModule is not very explicit regarding the fact that some Zee3 magic is happening. What about use Full.Path.MyModule, zee3_alias: MyModule? now zee3 appears somewhere in the use macro arguments…

Alternatively, I could use the following syntax construction, which is cleaner:

use Zee3.UserLib, module: Full.Path.To.MyModule, alias: MyModule

Some updates on the implementation: I have added some major functionality which will probabbly make this package very useful for other applications.

Datalog implementation

I have added bindings to the Z3 datalog engine (called muZ), which despite not being very performant, it is much more performant than I can implement natively in Elixir, especially when one needs the extensions to standard datalog that Z3 provides.

    require Zee3

    test "simple program with string entities", %{solver: pid} do
      {:ok, {:sat, solutions}} =
        Zee3.program pid do
          # Make sure the relations between entities declare entities
          # with the right sort from the standard library.
          edge = declare_rel("edge", [Sort.entity_id(), Sort.entity_id()])
          path = declare_rel("path", [Sort.entity_id(), Sort.entity_id()])
          # Declare variables, which, again, will use the correct sort.
          a = declare_var("a", Sort.entity_id())
          b = declare_var("b", Sort.entity_id())
          c = declare_var("c", Sort.entity_id())

          # Transitive closure definition
          rule(path.(a, b) <- edge.(a, b))
          rule(path.(a, c) <- path.(a, b) and path.(b, c))

          rule(edge.(entity_id("alice"), entity_id("bob")))
          rule(edge.(entity_id("alice"), entity_id("charlie")))
          rule(edge.(entity_id("bob"), entity_id("dan")))

          query("path")
        end

      # Z3 may return the tuples in any order so we sort them
      assert Enum.sort(solutions) == [
        {"alice", "bob"},
        {"alice", "charlie"},
        {"alice", "dan"},
        {"bob", "dan"}
      ]
    end

Finite sets implemented on top of existing theories

Small finite sets are quite useful in general, and it is useful to see how one can implement the basic axioms and operators of finite set theory in a relatively performant way in Z3. A lot of the operations are quadratic, so this is actually not super efficient, but I’m not sure I can do much better.

An example from the tests:

    require Zee3
    alias Zee3.StdLib.FiniteSet

    test "declare a set of bit vectors", %{solver: solver} do
        {:sat, model} =
        Zee3.program solver do
            s = FiniteSet.declare("s", Sort.bit_vec(8), max_size: 10)
            assert FiniteSet.contains(s, "a")
            assert FiniteSet.contains(s, "b")
            assert FiniteSet.contains(s, "c")
            assert FiniteSet.contains(s, "d")

            assert s.cardinality == 4

            check_sat_and_get_model!()
        end

        {:ok, s} = FiniteSet.extract_from_model(model, "s")

        assert MapSet.equal?(s, MapSet.new(["a", "b", "c", "d"]))
    end

Next steps

Another very useful feature of Z3 is a performant implementation of the Simplex algorithm for linear programming (optimization of a linear function under linear inequality constraints) and a not so performanc implementation of general non-linear optimizations. The current system can already handle this if one sets the right options (e.g. rounding the advanced real values, which are often presented as rationals and as roots of polynomials, which are pretty much impossible to calculate in Elixir), but I might want to add some wrappers around it.

Note that if anyone needs “normal” linear programming I already have a much better and much more performant solution in the form of the Dantzig package.

This is not an update on the state of the Zee3 library but just a comment on the some advantages of Z3 compared to using a normal linear programming library.

For unsatisfiable sets of constraints, Z3 can give the user an unsat core, which is useful to give feedback to the users or even to relax the constraints in order to get something that’s actually satisfiable.

For those who might be interested, I have implemented a version of the MARCO algorithm to list all minimum unsat cores in a companion package: GitHub - tmbb/zee3_marco: MARCO algorithm for Zee3 · GitHub.

The algorithm is very simple, but has enough little details that it can take a bit longer to implement than one might natively expect from reading a high-level description.

Thats a security and maintenance nightmare of every person responsible for dependency management.

First of all, I think that any library must never

1. download executable binaries
2. access internet during compilation
3. download not hash-verified binaries

And the way this library does it is just very wrong.

First of all, it uses httpc without any authority verification on the host. So just changing the /etc/hosts file to something like github.com my.malicious.binary.website.com would still work if the website would just return 200 with a self-signed github cert over https. If attacker has can poison the DNS for the build machine, they can run an arbitrary binary in the production.

Second, it downloads the binary for the machine it is compiled on. Again, doesn’t work when you compile on x86-64 and run on x86 for some reason.

Third, no hash verification. If z3 repository gets hacked and some other binary is returned, you may never know, because you don’t compare the hash of the file you got to the hash of the file you expected.

Fourth, compilation will fail when internet or a github will be unavailable. Imagine that your build pipeline is failing 1% of the time, because that’s how often the github fails.

The solution is to remove the vulnerable code and everything regarding this download-during-compilation approach and leave the binary download instructions in the README.

You don’t need to implement the buggy and vulnerable package manager, there are lots of tested, efficient and secure ones in the wild. Like Nix, for example.

I second that.