Hello, I'm Yong Kyung, and I'm going to be telling you today about the new verified tool for set-proof checking called KEG-LPR, which I have developed jointly with Moran and Magnus. Here's an outline of the talk. I'm going to start by introducing set-proof checking, and then I'll go into the contributions of this work in more detail in later sections.

Hopefully everyone who's watching this talk has some familiarity with set solvers. The input to a set solver is a formula of propositional logic, and the task of a set solver is to decide whether that formula is satisfiable,

whether there is a Boolean assignment to the propositional variables p, q, and r, so that the overall formula evaluates the truth. So a set solver has two possible outputs. It could say that the input formula is actually satisfiable. In that case, set solvers typically also report a so-called satisfying assignment, which is the assignment that makes the formula evaluate to true.

And these satisfying assignments can be used, for example, in a counterexample search, where the assignment itself could correspond to a counterexample. And again, this counterexample can be used as part of a larger loop, cigar loop, counterexample-guided abstraction refinement loop.

I have a simple example below, the formula p or q and not p or not q. This is structurally satisfied by the assignment, p maps to true, q maps to false, and it's relatively straightforward to check the correctness of such an assignment. We just plug in true for p and false for q, and then we evaluate the formula.

The other possible output of a set solver is that the input formula is actually unsatisfiable, and this has important applications as well. One such application is what supports we have two circuit implementations, circuit 1 and circuit 2, where we have applied some optimizations.

One thing we want to ensure is that the two circuits continue to implement the same arithmetic operation over their input. And we can encode this as a set problem by asking the set solver, is it not the case that these two circuits are equivalent? And of course, if the set solver tells us that this negated question is unsatisfiable, that means that the two circuits are indeed equivalent.

Now, another example I've shown below. Peirce's law is a tautology, so of course its negation is going to be unsatisfiable. But notice that if a set solver tells me that this formula is unsatisfiable, it's a bit more tricky to check such a claim.

One kind of naive way to check a claim is to write out a truth table, as I've done above, for the negation of Peirce's law. For every assignment to p and q, we can check whether Peirce's law evaluates to true or false. But this is not a good way to check answers by ability, because it's actually exponential in the number of variables that you have in your formula.

And suppose you have one of these circuits, it could go into hundreds of thousands of these variables. So it's not feasible to check those with truth tables. So, one approach that has gained popularity with the set-solving community is to instead have

the set solver also output an unsatisfiability proof when it claims that the input is unsatisfiable. And this unsatisfiability proof can now be checked by a set proof checker to determine whether it's a valid proof or not.

And really the idea that makes this work is to have a strong enough proof system so that set solvers can efficiently generate proofs corresponding to the techniques that they apply at runtime for set-solving. And at the same time, we want the proof system to be efficiently checkable by these set proof checkers.

In fact, in all recent set competitions, such an unset proof is required. Okay. But again, we can ask the same kind of question, right? If we didn't want to trust the set solver's output of unsatisfiability, why should we trust the set proof checker when it outputs that something is a valid proof?

Of course, the situation with set proof checkers is significantly improved in the sense that a set proof checker might just consist of a few hundred lines of C, which can be carefully inspected. But prior work has already improved on this state of affairs by developing verified proof checkers,

right, which are verified in so-called general purpose proof assistants like ACL2, Coq, and Isabelle. And this gives us a really strong correctness guarantee that when these tools report that something is a valid proof, it is really a valid proof of, valid proof of unsatisfiability.

So, so far we have seen kind of an increasing trust story for unset claims. Now what this work is about is actually increasing this trust story even further. We are going to be developing a new verified set proof checker.

But in addition, this proof checker is going to be verified down to its machine code implementation. So that is the thing that you actually run on your computer. And this is going to be achieved by using a tool chain built around the Kick ML verified compiler. Another improvement that we introduced in this work is direct support for a stronger proof system.

So now set solvers can directly generate proofs in this system, in this proof system called PR. And I'll go into more details about this proof system later when we reach there. Okay, so a summary comparison. Kick LPR is in the rightmost column.

We're going to support a stronger proof system. We're going to support a stronger trust story for the executable code while having pretty fast proof checking speeds as well. I'll talk about these three roles in the respective sections of this talk. Okay. Now let me get started with the proof system.

Okay, and to introduce the system, I actually need to define some terminology. So the typical input to a set solver is not just an arbitrary propositional formula. We're actually going to have to first normalize the formula to a standard format called conjunctive normal form. Some terminology here.

We call a propositional variable p or their negation, not p or p with a bar on top. We call these literals. A clause is a disjunction over a set of literals. And a formula is a conjunction over a set of clauses. A formula in conjunctive normal form.

So, and now I can define what it means to have a clausal proof system. We say that a clause C is redundant with respect to a formula F, if and only if. When I add the clause C to F, I remember F is in conjunctive normal form. Then the resulting formula is equally satisfiable with the, the formula F.

And how this works is as follows. Let me start with a formula F on the left-hand side of this chain of formulas. Okay. I'm going to add a redundant clause C1, okay, and that gives me F and C1. And remember that this preserves satisfiability.

I'm going to add another redundant clause C2 with respect to F and C1, and so on and so forth, going from left to right, until at the rightmost formula, I add a redundant clause bot, all right? And bot is my representation of the empty clause. But remember that the empty clause is unsatisfiable,

because, I mean, it has no literals, there's no way to satisfy it. And, and therefore, the rightmost formula is now unsatisfiable, okay? But because I've preserved satisfiability going from left to right, that means that unsatisfiability is preserved going from right to left. And therefore, what this implies is that the input formula F is actually also unsatisfiable.

Okay, so we can view the sequence C1, C2, C3, all the way to bot. We can view this as, as a causal proof of unsatisfiability of F, okay? So this is the kind of semantic notion of redundancy. Of course, the difference between different proof systems

is how they actually verify that a given clause is redundant. And here I have one pretty strong notion of redundancy called propagation redundancy. And, and I won't go into the full details of the definition. This notion was introduced, I think, two or three years ago.

And now the, the high-level idea is we, we still have the formula F, we have the clause C, which we want to show as redundant, right? What propagation redundancy also requires is an additional witness, omega, and the idea is for any satisfying assignment to F, okay,

we can modify it using omega to obtain a satisfying assignment for F and C, and therefore adding C preserves satisfiability, okay? And the thing that makes this practical proof system is that when, when we are given omega, then this notion of propagation redundancy

can be efficiently checked using unit propagation, which is, I would say, a fundamental operation for modern set solvers, okay? And, and of course the idea of unit propagation is that when we have a unit clause, so a clause with only one literal, then assignments must commit to, to, to assigning that particular literal

and then we can look at implications of that commitment in, in subsequent steps. Okay, so what does all of this look like in practice? In practice, formulas are given to set solvers in so-called D-max format. This is shown on the left. Basically each, each line is going to correspond to a clause in, in a numerical format.

And they are also given a, a proof file, so on the right I have a file, a PR proof file, and you can see each row again corresponds to a clause and its corresponding witness, okay? So, what this one shows is we can extend the standard PR proof format to,

to the so-called LPR proof format, and what LPR does is it essentially adds hints for unit propagation. This is, these are shown in blue, and what the hints allow for is these verified proof checkers to check the, the PR property efficiently without doing too much search, okay?

I should mention that, of course, this idea of adding hints for unit propagation comes from prior work, for example, on the LRAT format, okay? And in, in the paper also we describe an algorithm for checking LPR

and the point is we have actually designed this algorithm to be a minimal extension of the existing algorithm for checking the LRAT format, and you can see from this picture here, you know, we basically changed two lines of the algorithm. Now, you know, the point is, if you have an existing tool that's able to generate LRAT proofs,

then we can easily tweak it to also generate LPR proofs. Also, if you have a, if you have a tool that currently accepts or is able to check LPR, LRAT proofs, then we can easily extend it to check LPR proofs as well. Okay, so that, that is our contribution to the proof system.

Now I want to talk about the implementation or verification of the tool itself, and to do that I want to kind of revisit the picture again where I said that in, in prior work, you know, various authors have already looked at verification of these proof checkers. However, the verification kind of essentially

ends at the level of the proof checking algorithm, meaning there is some logical specification of the algorithm within the given proof assistance like ACL2, Coq, or Isabel, okay? But that's not quite the whole story, right,

to, to, to get from that specification down to the implementation. So for example, one might first need to extract those specifications from your proof, proof assistant out into a source language, say OCaml or ML, okay? And then we, we're going to need to add passing or file IO code. These are, these are unverified bits of code,

but we, these are needed in order to handle, for example, the file in the DMAX format or in, in the text file in the, in the PR format, okay? And then we need to compile this source file down to actual machine code that we can now run, okay? And of course, the compilation is not verified either.

In, in, in our tool, we actually extend the blue box, right, the verified proof assistant box. We extend it to encompass all three of the steps that I just mentioned, and, and we achieve this using KKML's so-called binary code extraction tool chain for each of these steps. So we have a verified way of extracting source KKML code

out from a proof checker algorithm. We can verify the parsing and file IO code with respect to the KKML specification of the file system. And finally, we can have, apply KKML's verified compiler to turn that proof checker source code

down to the machine code implementation while preserving the correctness guarantees, okay? And of course, once we have the machine code, we can actually run it, we can try and profile it, and these, this profiling is gonna tell us, you know, the kinds of optimizations that we should, can implement

to improve the proof checker, and we have many examples of this mentioned in the paper as well, okay? So, of course, now that we have a tool, the, the sort of final thing to do is to actually benchmark it Okay? I'm gonna show you two sets of benchmarks, okay? The first set is where we ran our tool on PR proofs

that are generated by a set solver called Setico. So Setico implements a relatively new paradigm called set-section-driven clause learning, or SDCL for short, and it's able to generate proofs directly in this stronger PR proof format, and you can see the checking time using KKLPR, these types are in seconds,

KKLPR is significantly faster than checking using the existing tools, and the reason for this is because, in order to use the existing verified tools, we actually need to first convert these PR proofs into a more, into a less expressive format called RAT,

and that introduces, for example, a polynomial size blow-up in the proofs, okay? So direct checking using our tool significantly reduces the checking time and makes actually PR proof checking feasible.

Another set of benchmarks that we did was to run these proof checkers on the unset proofs from the set race 2019, the set competition, and here we were also able to run KKLPR on these proofs because the LPR format is actually designed to be backwards compatible with LRAT itself, and so what this picture shows is,

well, KKLPR is actually able to check essentially most of the proofs, and it actually performs on par with the existing ACL2 proof checker, although both checkers are somewhat slower than the GRAT toolchain which is verified in Isabelle, but overall this shows that we have achieved the strong machine code guarantees

without significantly sacrificing the performance of our tool. So, as a conclusion, say that now KKLPR, it provides a stronger proof system, it provides a stronger trust array for the executable code, and retains the checking speed, so KKLPR enables efficient, verified PR proof checking,

and this opens up, for example, the use of SDCL-based set solvers, perhaps in set competitions. Another thing that KKLPR demonstrates is that binary code extraction using KKML is now a feasible technique for developing useful verified implementations of critical verification tools.

Thank you.