文件列表:

benchmark_data/
code/
cpp_prototypes/
docs/
ex/
isabelle_llvm
plots/
thys/
LICENSE
Makefile
ROOTS
cert_cadical.sh
mkhtml.sh
mkpkg.sh

# A Fast and Verified UNSAT Certificate Checker lrat_isa is a checker for unsatisfiability certificates in the LRUP format, formally verified in Isabelle/HOL. It is implemented time and memory efficiently, and can be run in parallel to the SAT solver at low overhead. Here are some [benchmark plots](https://github.com/lammich/lrat_isa/blob/master/plots/README.md) or the [raw data](https://github.com/lammich/lrat_isa/blob/master/benchmark_data). The verification is done wrt. a grammar of the DIMACS CNF format, and down to the LLVM code implementing the checker. ## Prerequisites For building the tool from the generated LLVM test, you need: * Clang compiler (I used version 14.0.0, but everything >10.0 should be fine), and make * Boost C++ Libraries with iostreams library For checking the proofs, or viewing the proofs inside Isabelle, you additionally need: * Working installation of [Isabelle/HOL](https://github.com/lammich/lrat_isa/blob/master/https://isabelle.in.tum.de) with the [Archive of Formal Proofs](https://github.com/lammich/lrat_isa/blob/master/https://www.isa-afp.org) installed as described [here](https://github.com/lammich/lrat_isa/blob/master/https://www.isa-afp.org/using.shtml). We require version = Isabelle-2023. ## Building the tool In the main directory, run make This will generate the executables `./code/lrat_isa` and `./code/lrat_isa_dbg`, and do a quick check that they've been correctly build. The former is the formally verified proof checker. The latter has been generated by modifying the exported LLVM code to include output of debug information. ## Using the tool Invoke the tool as lrat_isa [] If no lrat-file is specified, the certificate is read from standard input. On successful verification, it will print the line s VERIFIED UNSAT and exit with exit-code 0. Otherwise, it will print an error message and exit with a non-zero exit code. Check out the example. From the main directory, run: ./code/lrat_isa ex/ex1.cnf ex/ex1.lrat To stream the certificate directly from CaDiCaL (requires [CaDiCaL](https://github.com/lammich/lrat_isa/blob/master/https://github.com/arminbiere/cadical)>=v1.9.4): cadical -n -q --lrat ex/ex1.cnf - | ./code/lrat_isa ex/ex1.cnf We have also build a prototype script that uses a named pipe, and handles satisfiable and unsatisfiable formulas. It assumes cadical and lrat_isa on the path. ./cert_cadical.sh ex/ex1.cnf ## Inspecting the Proof You can browse the [html version](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/index.html) of the theories. Note that the presentation in the paper has been simplified for better readability, and typically uses shorter names than the actual formalization. Good starting points for browsing: * [Main Theory](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/LRAT_Checker_Impl.html) contains code generation and [final correctness theorem](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/LRAT_Checker_Impl.html#LRAT_Checker_Impl.lrat_checker_correct|fact) at end. * [DIMACS Grammar](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/CNF_Grammar.html) contains our [grammar](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/CNF_Grammar.html#CNF_Grammar.cnf_dimacs|const) for Dimacs CNF, a succinct characterization of it's [language](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/CNF_Grammar.html#CNF_Grammar.dimacs_reg_language|fact), and a [proof that it is unambiguous](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/CNF_Grammar.html#CNF_Grammar.unamb_dimacs|fact). * [Semantics of CNF](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/SAT_Basic.html), with our definition of [satisfiability](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/SAT_Basic.html#SAT_Basic.sat|const). * [Abstract Checker](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/Relaxed_Assignment.html#Relaxed_Assignment.checker_state|type) contains the abstract transition relation for the checker, and it's [correctness](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/Relaxed_Assignment.html#Relaxed_Assignment.checker_trans_rtrancl_unsatI|thm) * [Unit checking (check_uot)](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/LRAT_Checker_Impl.html#LRAT_Checker_Impl.cdb_check_uot|const) the inner loop of our checker. * Data Structures (the theories contain the abstract versions and the LLVM implementations) * [Literal Encoding](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/Unsigned_Literal.html) * [Reversible Partial Assignment](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/Trailed_Assignment.html) * [Clauses, Builder, and Database](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/Zero_Term.html) * Concrete checker states: [outside proof (op)](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/LRAT_Checker_Impl.html#LRAT_Checker_Impl.checker_state_out_proof|type) [build-clause (bc)](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/LRAT_Checker_Impl.html#LRAT_Checker_Impl.checker_state_build_lemma|type) [in proof (ip)](https://github.com/lammich/lrat_isa/blob/master/https://lammich.github.io/lrat_isa/Unsorted/lrat_isa/LRAT_Checker_Impl.html#LRAT_Checker_Impl.checker_state_in_proof|type) ## Inspecting the proof inside Isabelle Run isabelle jedit -d . -l Isabelle_LLVM thys/LRAT_Checker_Impl.thy On the first invocation of this command, a base image with the required libraries is built, which may take several minutes. When invoked, the IDE will display the last theory of the formal development, where the exported code is generated, and the final correctness theorem is proved. Moreover, the IDE will start to verify all dependent theories. If verification is finished (may take another few minutes), you can use the navigation features of the IDE to navigate the formalization and inspect the proof state. ## Checking the Proofs and Regenerating the LLVM code In the main directory, run make check_thys This will invoke Isabelle to check all proofs and re-generate the exported code, which is written to `code/lrat_isa_export.ll` This may take a while, in particular on the first invocation, when Isabelle builds some prerequisites.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：