A Verified Cyclicity Checker

This is an introduction to the artifact of our ITP 2022 submission. The formalisation is part of the CakeML development repository and available at the paths:

• candle/overloading/syntax for the theory, mainly in holSyntaxCyclicityScript.sml
• candle/overloading/ml_kernel for the theorem prover kernel
• candle/overloading/ml_checker for the verified checker

In the following we describe the files contained in our executable artifact, how to run this binary cyclicity checker and its file format, and how to reproduce the binary from the HOL4 implementation.

Files in the Compressed Archive

The following files are part of the compressed archive:

• checker - a cyclicity checker x86 binary (64 bit)
• cyclicity_checker.sexp - the synthesised S-expression, produced from our verified implementation and an unverified parser

Apart from the executable, the artifact also contains the following dependency relations:

• Small examples (of two dependencies each)
  • cyclic.deps - cyclic with overloading
  • cyclic2.deps - cyclic without overloading
  • non_composable.deps - not composable
• Isabelle/HOL theory exports
  • fun.deps
  • hol.deps
  • main.typeless.deps
  • orderings.deps
  • set.deps
  • transitive_closure.deps
  • transitive_closure.typeless.deps

Running the Checker

The executable checker receives a dependency relation on stdin.

./checker < cyclic.deps

This produces the following output, with type constructors written postfix.

Found a cycle!
  The path from c : (num list,bool) fun
  to c : ((num,num list) prod,bool) fun
  starts a cycle c : (num list,bool) fun

For checking larger dependency files one can modify the environment variables CML_HEAP_SIZE and CML_STACK_SIZE, which contain the heap and stack size in MB, and defaults to 1024 MB.

env CML_HEAP_SIZE=1024 CML_STACK_SIZE=1024 ./checker < cyclic.deps

The Dependency File Format

The cyclicity checker parses dependency relations in the following format:

• A list of elements is empty [] or starts with [, contains elements delimited by semicolons ; and ends with ].
• A tuple starts with ( followed by the first component, that is separated by a comma , from the second component and ends in ).
• A string starts by " and ends with ". E.g. "bool".
• A type is either a Tyvar followed by a string name or a Tyapp with a string name followed by a list of type arguments.
  E.g. Tyapp "list" [Tyvar "'a"]
• A constant has a name as string followed by its type.
  E.g. "identity" Tyapp "fun" [Tyvar "'a"; Tyvar "'a"]
• A dependency relation is a list of pairs of constants and types

Reproducing the Binary

To reproduce cyclicity_checker.sexp from our HOL4 implementation, it is necessary to compile HOL4 and our proofs, which we will describe first. Then we describe how to reproduce checker from cyclicity_checker.sexp.

Reproducing cyclicity_checker.sexp

Compiling our proofs requires polyml and a specific version of HOL4.

1. Get a recent version 5.9 or 5.8.2 of PolyML following the instructions on the PolyML Website
2. Check out commit 9d2d0e89bd165c1ea71279ed6f2ed14ed6c15d27 from the HOL4 repository and follow the installation instructions in the INSTALL file. For the following steps the bin/ folder in the HOL directory needs to be in $PATH.
3. Check out commit 62355d1569fbecf5ed8d03eb7c503322622c95aa of our fork of the CakeML repository and run Holmake in the directory candle/overloading/ml_checker/, in order to recompile all our proofs and their dependencies, and to produce cyclicity_checker.sexp.
4. To examine our theories interactively, consult the HOL4 documentation on how to set up HOL4 interactive modes in vim or emacs. Each directory within candle/overloading contains a README file, that gives an overview over the files in the mechanisation.

Reproducing checker

The S-expression cyclicity_checker.sexp that is produced by our formalisation (and also part of this artifact) can be compiled into an executable using the CakeML compiler. Obtain a recent version of the CakeML compiler, extract the archive and run make, to produce a binary CakeML compiler cake. This compiler can compile the S-expression cyclicity_checker.sexp:

./cake \
  --skip_type_inference=true \
  --exclude_prelude=true \
  --sexp=true \
  < cyclicity_checker.sexp > checker.S

In a last step link checker.S with basis_ffi.c (from the compiler archive) to produce an executable checker binary.

cc checker.S basis_ffi.c -o checker