This repository contains pre-compiled versions of LPR proof checkers produced using the CakeML compiler and associated toolchains (https://cakeml.org/).

Source and proof files are available in the main CakeML repository (https://github.com/CakeML/cakeml/tree/master/examples/lpr_checker)

The file cake_lpr.S is built from the following repository versions

HOL4: 0ae7030322cdf2b0d46dc9d5503e2d5eae2fa726

CakeML: fb377b4bb704497c921cde68ccc8da3b4f0e9132

News

New (22 Jul 2026): Incompatibility: heap/stack sizes are no longer read from the CML_HEAP_SIZE/CML_STACK_SIZE environment variables; pass the command-line flags --CML_HEAP_SIZE=<n>/--CML_STACK_SIZE=<n> (in MB) instead.

New (16 Feb 2025): Improved cake_lpr performance by around 5-10% and reduced its compiled binary size by around 20%.

New (11 Mar 2024): cake_lpr now natively supports LRAT/LPR proof files in binary format.

Instructions

Running make will build the the proof checker cake_lpr.

To build for Mac (or other machines with ARMv8 chips), run make cake_lpr_arm8.

Read the Makefile for other variations.

This help string is printed to stdout when cake_lpr is run with no arguments:

Usage:  cake_lpr <DIMACS formula file>
Parses the DIMACS file and prints the parsed formula.

Usage:  cake_lpr <DIMACS formula file> <LPR proof file>
Run LPR unsatisfiability proof checking

Usage:  cake_lpr <DIMACS formula file> <LPR proof file> <DIMACS transformation file>
Run LPR transformation proof checking

Usage:  cake_lpr <DIMACS formula file> <summary proof file> i-j <LPR proof file>
Run two-level transformation proof checking for lines i-j

Usage:  cake_lpr <DIMACS formula file> <summary proof file> -check <output file>
Check that output intervals cover all lines of summary proof file

Examples

• Running the checker with a CNF file and an LPR proof: ./cake_lpr example.cnf example.lpr

  Output (stdout):

  s VERIFIED UNSAT
  

• Running the checker with a CNF file and an incorrect LPR proof: touch foo.lpr; ./cake_lpr example.cnf foo.lpr

  Output (stderr):

  c empty clause not derived at end of proof
  

  Other errors are possible during LPR proof checking. These will all be reported on stderr.

• Running the checker with a CNF file only dumps the file (after parsing): ./cake_lpr example.cnf

  Output (stdout):

  p cnf 12 22
  1 2 3 0
  4 5 6 0
  7 8 9 0
  10 11 12 0
  -1 -4 0
  -2 -5 0
  -3 -6 0
  ...
  

• It is possible for the checker to run out of stack/heap space on large proofs, e.g., with:

  Output (stderr):

  CakeML heap space exhausted.
  

• To increase heap/stack size (in MB), pass the following flags, e.g., as follows:

  ./cake_lpr --CML_HEAP_SIZE=4000 --CML_STACK_SIZE=4000 example.cnf example.lpr
  

  These flags are handled by the C wrapper (basis_ffi.c) and are not passed on to the checker; run ./cake_lpr --h for the wrapper's help message.

• Alternatively, modify the default values of CML_HEAP_SIZE and CML_STACK_SIZE in basis_ffi.c.