Open Source Adventures: Episode 01: Crystal FFI and Z3

Welcome to my new series! Previously I did Electron Adventures and 100 Languages Speedrun.

Now it's time for something a bit less ambitious. I do a lot of small Open Source things anyway all the time, so in this series I'll just write about the kind of things I do anyway.

I plan it as a more or less daily series of 100 episodes. They'll mostly be much smaller than in my 100 Languages Speedrun series, and any big topic will likely be split into multiple bite-size episodes. Some will be new stuff, some might be flashbacks to old things I made before.

Let's get started!

Z3 and Crystal

Z3 is a theorem prover library, and I maintain a Ruby gem for it. I wrote about it previously in 100 Languages Speedrun: Episode 23: Ruby Z3
.

I want to play with Crystal a bit more, and since I already know Z3, that's a decent start.

Z3 C API

Z3 C API is super unfun to work with. We need to create a Context object (passing a Config), then we need to pass that damn context to every single function call. Due to limitations of C there's some weird calling convention for anything that takes variable number of arguments or returns multiple values. And worst of all, there are so many ways to pass arguments that pass the C type system, but will still hard crash Z3 - like trying to add an integer expression (type Ast) to a boolean expression (also type Ast) for an obvious example, but there are many others.

The way I solved it in Ruby is by layers. First I created the Z3::VeryLowLevel which directly maps to the C API, with functions like these:

module Z3
  module VeryLowLevel
    attach_function :Z3_mk_gt, [:ctx_pointer, :ast_pointer, :ast_pointer], :ast_pointer
  end
end

This means function Z3_mk_gt takes three arguments (Context, Ast, Ast), and returns one argument Ast.

Then there's second layer Z3::LowLevel which handles context, unwraps passed objects, and also handles peculiarities of C APIs like how arrays and multiple return values are handled:

module Z3
  module LowLevel
    def mk_gt(ast1, ast2) #=> :ast_pointer
      VeryLowLevel.Z3_mk_gt(_ctx_pointer, ast1._ast, ast2._ast)
    end
  end
end

Only on top of that I built the actual API, which did all the crash-prevention checks, automatic coercion, operators, and so on:

module Z3
  class Expr < AST
    class << self
      def Gt(a, b)
        a, b = coerce_to_same_sort(a, b)
        case a
        when ArithExpr
          BoolSort.new.new(LowLevel.mk_gt(a, b))
        when BitvecExpr
          raise Z3::Exception, "Use #signed_gt or #unsigned_gt for Bitvec, not >"
        else
          raise Z3::Exception, "Can't compare #{a.sort} values"
        end
      end
    end
  end
end

module Z3
  class ArithExpr < Expr
    def >(other)
      Expr.Gt(self, other)
    end
  end
end

The end result is that you can do this:

> Z3.Int("a") > 420
Bool<a > 420>

Which does a lot of Z3 calls behind the scene.

Crystal FFI

OK, let's get started with doing this in Crystal. First, manually doing just enough of the very low level API to get started:

@[Link("z3")]
lib Z3
  type Ast = Void*
  type Config = Void*
  type Context = Void*
  type Model = Void*
  type Solver = Void*
  type Sort = Void*
  type Symbol = Void*

  # Just list the ones we need, there's about 700 API calls total
  fun mk_add = Z3_mk_add(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_const = Z3_mk_const(ctx : Context, name : Symbol, sort : Sort) : Ast
  fun mk_context = Z3_mk_context(cfg : Config) : Context
  fun mk_contig = Z3_mk_config() : Config
  fun mk_eq = Z3_mk_eq(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_ge = Z3_mk_ge(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_gt = Z3_mk_gt(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_int_sort = Z3_mk_int_sort(ctx : Context) : Sort
  fun mk_le = Z3_mk_le(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_lt = Z3_mk_lt(ctx : Context, a : Ast, b : Ast) : Ast
  fun mk_distinct = Z3_mk_distinct(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_mul = Z3_mk_mul(ctx : Context, count : UInt32, asts : Ast*) : Ast
  fun mk_numeral = Z3_mk_numeral(ctx : Context, s : UInt8*, sort : Sort) : Ast
  fun mk_solver = Z3_mk_solver(ctx : Context) : Solver
  fun mk_string_symbol = Z3_mk_string_symbol(ctx : Context, s : UInt8*) : Symbol
  fun model_to_string = Z3_model_to_string(ctx : Context, model : Model) : UInt8*
  fun solver_assert = Z3_solver_assert(ctx : Context, solver : Solver, ast : Ast) : Void
  fun solver_check = Z3_solver_check(ctx : Context, solver : Solver) : Int32
  fun solver_get_model = Z3_solver_get_model(ctx : Context, solver : Solver) : Model
end

SEND + MORE = MONEY

And let's do a very simple problem, SEND + MORE = MONEY.

First, the global setup:

# Setup library
cfg = Z3.mk_contig()
ctx = Z3.mk_context(cfg)
solver = Z3.mk_solver(ctx)
int_sort = Z3.mk_int_sort(ctx)

There's no automatic conversion of numbers to Z3 objects, so we need to do this manually:

# Integer constants
nums = Hash(Int32, Z3::Ast).new
[0, 1, 9, 10, 100, 1000, 10000].each do |num|
  nums[num] = Z3.mk_numeral(ctx, num.to_s, int_sort)
end

And set up variables. They all need to be 0 to 9, but we can't have leading zeroes so M and S must be at least 1:

# Variables, all 0 to 9
vars = Hash(String, Z3::Ast).new
%w[s e n d m o r e m o n e y].uniq.each do |name|
  name_sym = Z3.mk_string_symbol(ctx, name)
  var = Z3.mk_const(ctx, name_sym, int_sort)
  vars[name] = var
  Z3.solver_assert(ctx, solver, Z3.mk_ge(ctx, var, nums[0]))
  Z3.solver_assert(ctx, solver, Z3.mk_le(ctx, var, nums[9]))
end

# m and s need to be >= 1, no leading zeroes
Z3.solver_assert(ctx, solver, Z3.mk_ge(ctx, vars["m"], nums[1]))
Z3.solver_assert(ctx, solver, Z3.mk_ge(ctx, vars["s"], nums[1]))

They also need to be all different:

# all letters represent different digits
all_distinct = Z3.mk_distinct(ctx, vars.size, vars.values)
Z3.solver_assert(ctx, solver, all_distinct)

Now SEND + MORE = MONEY. This is very verbose, but all the extra arguments like ctx and array sizes get in the way of doing it more concisely:

send_vars = [
  Z3.mk_mul(ctx, 2, [vars["s"], nums[1000]]),
  Z3.mk_mul(ctx, 2, [vars["e"], nums[100]]),
  Z3.mk_mul(ctx, 2, [vars["n"], nums[10]]),
  vars["d"],
]

more_vars = [
  Z3.mk_mul(ctx, 2, [vars["m"], nums[1000]]),
  Z3.mk_mul(ctx, 2, [vars["o"], nums[100]]),
  Z3.mk_mul(ctx, 2, [vars["r"], nums[10]]),
  vars["e"],
]

money_vars = [
  Z3.mk_mul(ctx, 2, [vars["m"], nums[10000]]),
  Z3.mk_mul(ctx, 2, [vars["o"], nums[1000]]),
  Z3.mk_mul(ctx, 2, [vars["n"], nums[100]]),
  Z3.mk_mul(ctx, 2, [vars["e"], nums[10]]),
  vars["y"],
]

send_sum = Z3.mk_add(ctx, send_vars.size, send_vars)
more_sum = Z3.mk_add(ctx, more_vars.size, more_vars)
money_sum = Z3.mk_add(ctx, money_vars.size, money_vars)
send_more_sum = Z3.mk_add(ctx, 2, [send_sum, more_sum])
equation = Z3.mk_eq(ctx, send_more_sum, money_sum)
Z3.solver_assert(ctx, solver, equation)

And finally let's print the results. Z3 at least saves us here, as it has some rudimentary model to string conversion, so we don't need to do anything complicated. Eventually we don't want to use that - we'd rather get Hash of results from Z3 Model and handle printing it out ourselves, but that's still far away.

Result code has three possibilities ("definitely no", "definitely yes", and "Z3 couldn't solve it"):

# Get the result

result_code = Z3.solver_check(ctx, solver)
puts "Result code is: #{result_code}"

model = Z3.solver_get_model(ctx, solver)
s = Z3.model_to_string(ctx, model)
puts String.new(s)

Let's run it:

$ ./send_more_money.cr
Result code is: 1
d -> 7
n -> 6
o -> 0
m -> 1
r -> 8
s -> 9
e -> 5
y -> 2

That is: 9567 + 1085 == 10652

Story so far

I put the code in crystal-z3 repo.

We got the point where we can run Z3 from Crystal, but the API is horrendous.

So far Crystal FFI handled everything without any issues, but a lot of complexity is still ahead, and there's also a lot of things I'm ignoring like integrating with Z3 memory management.

Coming next

In the next episode, we'll try to make Crystal handle Z3 Contexts and other very low level concerns for us, so we can make code look less like ass. It will take many iterations before we get something decent. One step at a time.