Making TLA+ and x86 Kiss Via Z3Py | Hey There Buddo!
I’ve been trying my hand at translating a reasonable subset of TLA+ into z3py for the purposes of connecting specs to Verus, CBMC, and my assembly checker and also for maybe a little interactive theorem proving as a treat.
I do have a sense that TLA+ has made good inroads into acceptance by a more general software engineering. It is relatively low barrier while delivering useful value.
https://learntla.com/
https://lamport.azurewebsites.net/tla/tla.html
https://docs.tlapl.us/
I think a deficiency of the TLA+ ecosystem where maybe I could deliver some value is to offer some tooling to help validate correspondences of specs and implementations. The flexibility of a library approach vs a tool approach seems useful here.
This is all a work in progress, but I’ll show what I’ve got. The TLA+ ingester is here https://github.com/philzook58/knuckledragger/blob/main/src/kdrag/solvers/tla.py . It’d be nice to hear if this is something people want.
Hour Clock
A basic example from Specifying Systems is the hour clock example. A clock should keep it’s hours between 1 and 12 inclusive.
%%file /tmp/HourClock.tla<br>---- MODULE HourClock ----<br>EXTENDS Naturals
VARIABLE hr
HCini == hr \in (1 .. 12)
HCnxt == hr' = IF hr = 12 THEN 1 ELSE hr + 1<br>(* Alternately expressed as: hr' = (hr % 12) + 1 *)
HC == HCini /\ [][HCnxt]_hr
Overwriting /tmp/HourClock.tla
We can load this module and infer the sorts
import kdrag.solvers.tla as tla<br>import kdrag as kd<br>import kdrag.smt as smt
mod = tla.Module.of_file("/tmp/HourClock.tla")<br>mod.infer_sorts()<br>mod
Module(name='HourClock', variables=['hr'], definitions={'HCini': \in(hr, ..(1, 12)), 'HCnxt': =('(hr), $IfThenElse(=(hr, 12), 1, +(hr, 1))), 'HC': \land(HCini, []($SquareAct(HCnxt, hr)))}, def_params={'HCini': [], 'HCnxt': [], 'HC': []}, theorems=[], decls={'HCini': HCini, 'HCnxt': HCnxt, 'HC': HC, 'hr': hr})
Alternatively or in combination with infer_sorts, we can manually declare the sorts of our variables. Unfortunately (?), these sort annotations really are a part of the spec. Sometimes infer_sorts is not powerful enough to actually infer all the sorts without help. Or perhaps you want to narrow their meaning or pick a non default representation like BitVectors. Making a choice like that may completely change the interpretation of the spec (+ becomes wraparound addition for example). I’d like to have a better story here, but for now, the power user capability is nice.
mod = tla.Module.of_file("/tmp/HourClock.tla")<br>hr = mod.Var("hr", smt.IntSort())
Now that we have sorts, we can get the transition relation as an expression over hr' and hr as a z3py BoolRef
HCnxt = mod.action("HCnxt")<br>print(type(HCnxt))<br>HCnxt
hr’ = If(hr = 12, 1, hr + 1)
This is a little ugly looking because of how it uses a z3 lambda to talk about sets of ints $hr \in 1..12$
mod.action("HCini")
λx!46 : 1 ≤ x!46 ∧ 12 ≥ x!46[hr]
The simplified form is less ugly
smt.simplify(mod.action("HCini"))
1 ≤ hr ∧ 12 ≥ hr
We can do whatever wacky stuff we want to do with these expressions. Programmatically rip them apart, build a custom model checker, etc, but here is a routine that builds an assertion that checks an invariant. Basically mod.invariant constructs the z3py formula $ (init(hr) \implies inv(hr)) \land (inv(hr) \land step(hr,hr’)\implies inv(hr’))$. Knuckledragger is a proof asssitant and in principle we can semi-autoamtically discharge more difficult goals that might include quantifiers etc by using knuckledragger tactics.
kd.prove(kd.smt.simplify(mod.invariant(inv="HCini", init="HCini", step="HCnxt")))
⊨Or(Not(And(hr’ == If(hr == 12, 1, 1 + hr),<br>1 = hr)),<br>And(1 = hr’))
One thing I’m still thinking about is outputting the TLA as a spec to Verus, a rust verification tool. Verus is designed to hew pretty close to z3 and offers datatypes that correpond to z3 datatypes. That ought to make it a bit easier. Here for example, Verus has an unbounded int type that maps to z3’s.
I also have C printers, but they don’t support Int, so more chewing has to be done to convert to the uint_t that it does support (C uint should map reasonably well to z3 bitvectors I think. C’s int is a nastier beast.).
import kdrag.printers.rust as rust<br>print(rust.of_expr(smt.simplify(mod.action("HCini"))))
((1 = hr))
Assembly
I’ve been tinkering on an assembly verifier for a while https://www.philipzucker.com/refine_assembly/ . I think it makes sense to use that to plug into a TLA spec
Here’s an x86_64 program that ticks a clock in %rdi
%%file /tmp/clock.s<br>.global tick<br>.global reset
reset:<br>mov $1, %rdi<br>jmp tick<br>tick:<br>cmp $12, %rdi<br>je reset<br>add $1, %rdi<br>jmp tick
Overwriting /tmp/clock.s
Assemble it
! gcc -c /tmp/clock.s -o /tmp/clock.o
Already I had stuff to check a high level python model (I have a symbolic executor from a subset of python to z3py) against the assembly.<br>We want to show that each step of the model corresponds to a step of the assembly. This sort...