[darcs-devel] checking primitive commute rules with Z3

Ben Franksen ben.franksen at online.de
Sun May 30 20:08:03 UTC 2021


Am 30.05.21 um 11:03 schrieb Ganesh Sittampalam:
> Hi,
> 
> For years I've been trying off and on (more off than on!) to find a
> systematic way to check that our primitive commute rules are correct.
> 
> Some pencil and paper playing around led me to the so-called "relaxed
> hunk commutation" side-condition for hunk-hunk commute, but the level of
> detail quickly got out of control when considering laws like permutivity
> or more complicated patch types like hunk move.
> 
> I recently tried out doing this with Z3, and it turns out to work
> remarkably well so far:
> 
> https://hub.darcs.net/ganesh/commutation-rules/browse/z3/commute.smt2
> 
> So far it checks various properties of hunk-hunk commute like symmetry,
> inverse commutes, commute squares and permutivity. This is an exhaustive
> verification based on the properties of integers so proves that the
> commute rules are correct, subject of course to any weaknesses in how I
> modelled those rules in the first place.

Wow, this is cool. The z3 code is quite readable, much more so than e.g.
the stuff that Ian did with Coq.

> Running the code
> ----------------
> 
> Just install Z3 and run it on commute.smt2

I installed z3 from my distro and cloned your repo but

ben at home[1]:.../darcs/commutation-rules>z3 z3/commute.smt2
             √
(error "line 40 column 8: invalid qualified/indexed identifier, '_' or
'as' expected")
(error "line 66 column 8: invalid qualified/indexed identifier, '_' or
'as' expected")
(error "line 89 column 41: unknown function/constant commuteAbove")
(error "line 96 column 53: unknown function/constant commuteUnique")
sat
(model
)
(error "line 115 column 33: unknown function/constant commuteAbove")
(error "line 127 column 21: unknown function/constant commuteHunk")
(error "line 138 column 56: unknown function/constant commuteSymmetric")
sat
(model
)
(error "line 154 column 21: unknown function/constant commuteHunk")
(error "line 165 column 54: unknown function/constant commuteInverse")
sat
(model
)
(error "line 173 column 21: unknown function/constant commuteHunk")
(error "line 201 column 53: unknown function/constant commuteSquare")
sat
(model
)
(error "line 208 column 36: unknown function/constant commuteHunk")
(error "line 268 column 89: unknown function/constant permutivity")
sat
(model
)
ben at home[1]:.../darcs/commutation-rules>z3 --version
             1
Z3 version 4.4.1

I guess version 4.4.1 may be too old?

> - the expected output is that
> it prints this for each of the checks:
> 
>> unsat
>> (error "line <X> column <Y>: model is not available")
> 
> This is because the way to prove a property is to ask if the negation of
> the property is satisfiable. If it is not satisfiable, the property is
> true. If it is satisfiable, then we have a counter-example, named a
> "model" in the lingo, which can be printed out.

Okay.

> Taking this further
> -------------------
> There are various possible directions to take this further, which I will
> explore as time and interest allow.
> 
> (1)
> 
> Use it to verify more patch types, for example the full current V1
> primitives, or things like hunk move.

I guess proving RepoPatchV3 correct, assuming correctness of the
underlying prim type and uniqueness of prim patch IDs, is out of scope
because it requires making decuctions from arbitrary assumptions, right?

> Raw Z3/the SMT-LIB format don't support any real abstraction, the idea
> is to use a language binding and then meta-programming in that host
> language to achieve that. So keeping going with that would require a lot
> of copy and paste for each patch type.
> 
> Switching to a programming language could either be done with a raw
> binding (there are many on hackage) or with a more sophisticated
> embedding like the sbv package.

So do such Haskell bindings allow to /express/ the z3 code in Haskell in
some way?

> (2)
> 
> Integrate more directly with a language that supports refinement types,
> For example, Liquid Haskell or F*, which both use Z3 under the hood. One
> of my previous experiments was with F* but I got a bit stuck mainly
> because of lack of familiarity and partly because the details of how Z3
> is being used are not very visible. Liquid Haskell would of course be
> quite attractive if we could use it on the real darcs code.

Does Liquid Haskell understand all of GHC Haskell including all the
extensions we use?

> (3)
> 
> Find a way to actually reason backwards from "these are the laws we need
> to satisfy" to "these are the logically necessary side-conditions".
> 
> With an SMT solver like Z3, we either get "this can be proved" or
> "here's a single counter-example". So we can iterate to find a set of
> conditions that are valid, but we don't get much high-level insight.
> 
> Ideally we could give a high-level specification of how we expect
> commute to behave, and then instantiate each of the commute laws and
> simplify the resulting conditions to get some insight into what the gaps
> are. For example if we started with rules that say "all touching hunks
> can commute" then we might hope for a concise description of which kinds
> of patches fail which rules.
> 
> I did have a go at doing this using code with some ad hoc simplification
> rules for the relevant arithmetic expressions, but got a bit stuck
> making it usable. I recently discovered Fourier-Motzkin elimination,
> which might help a bit with doing this more systematically.

Very interesting work, keep it up!

Cheers
Ben
-- 
I would rather have questions that cannot be answered, than answers that
cannot be questioned.  -- Richard Feynman




More information about the darcs-devel mailing list