[spam][julia][wrong] Probabilistic Program Synthesis?

[Undiscussed Horrific Abuse, One Victim of Many]

https://www.cs.cornell.edu/~asampson/blog/minisynth.html

Program Synthesis is Possible
MAY 9, 2018

Program synthesis is not only a hip session title at programming
languages conferences. It’s also a broadly applicable technique that
people from many walks of computer-science life can use. But it can
seem like magic: automatically generating programs from specifications
sounds like it might require a PhD in formal methods. Wisconsin’s Aws
Albarghouthi wrote a wonderful primer on synthesis last year that
helps demystify the basic techniques with example code. Here, we’ll
expand on Aws’s primer and build a tiny but complete-ish synthesis
engine from scratch.

You can follow along with my Python code or start from an empty buffer.

Z3 is Amazing

We won’t quite start from scratch—we’ll start with Z3 and its Python
bindings. Z3 is a satisfiability modulo theories (SMT) solver, which
is like a SAT solver with theories that let you express constraints
involving integers, bit vectors, floating point numbers, and what have
you. We’ll use Z3’s Python bindings.

Let’s try it out:

>>> import z3

To use Z3, we’ll write a logical formula over some variables and then
solve them to get a model, which is a valuation of the variables that
makes the formula true. Here’s one formula, for example:

>>> formula = (z3.Int('x') / 7 == 6)

The z3.Int call introduces a Z3 variable. Running this line of Python
doesn’t actually do any division or equality checking; instead, the Z3
library overloads Python’s / and == operators on its variables to
produce a proposition. So formula here is a logical proposition of one
free integer variable, x, that says that x / 7 = 6.

Let’s solve formula. We’ll use a little function called solve to invoke Z3:

def solve(phi):
    s = z3.Solver()
    s.add(phi)
    s.check()
    return s.model()

Z3’s solver interface is much more powerful than what we’re doing
here, but this is all we’ll need to get the model for a single
problem:

>>> print(solve(formula))

On my machine, I get:

[x = 43]

which is admittedly a little disappointing, but at least it’s true:
using integer division, 43 \/ 7 = 6.

Z3 also has a theory of bit vectors, as opposed to unbounded integers,
which supports shifting and whatnot:

>>> y = z3.BitVec('y', 8)
>>> print(solve(y << 3 == 40))

There are even logical quantifiers:

>>> z = z3.Int('z')
>>> n = z3.Int('n')
>>> print(solve(z3.ForAll([z], z * n == z)))

Truly, Z3 is amazing. But we haven’t quite synthesized a program yet.

Sketching

In the Sketch spirit, we’ll start by synthesizing holes to make
programs equivalent. Here’s the scenario: you have a slow version of a
program you’re happy with; that’s your specification. You can sort of
imagine how to write a faster version, but a few of the hard parts
elude you. The synthesis engine’s job will be fill in those details so
that the two programs are equivalent on every input.

Take Aws’s little example: you have the “slow” expression x * 2, and
you know that there’s a “faster” version to be had that can be written
x << ?? for some value of ??. Let’s ask Z3 what to write there:

>>> x = z3.BitVec('x', 8)
>>> slow_expr = x * 2
>>> h = z3.BitVec('h', 8)  # The hole, a.k.a. ??
>>> fast_expr = x << h
>>> goal = z3.ForAll([x], slow_expr == fast_expr)
>>> print(solve(goal))

Nice! We get the model [h = 1], which tells us that the two programs
produce the same result for every byte x when we left-shift by 1.
That’s (a very simple case of) synthesis: we’ve generated a
(subexpression of a) program that meets our specification.

Without a proper programming language, however, it doesn’t feel much
like generating programs. We’ll fix that next.

.............

it's discouraging that the examples so far do not generate code other
than variables.

still seeming like the first julia library is more accessible.
above python library is at https://github.com/sampsyo/minisynth