Artifact for "Scaling Up Mechanized Proof Automation for Small-step Semantics"

This is the companion artifact to the paper "Scaling Up Mechanized Proof Automation for Small-step Semantics".

This artifact contains the Rocq code described in the paper.

Detailed File Description

The file CLAIMS.md links statements made in the paper with this artifact.

The file sequences.v is adapted from previous work by François Pottier, which was based on work by Xavier Leroy, with a few additions by the authors of this artifact.

| File Name | Spec | Proof | Comments | Description | |------------------------------------|----------|-----------|--------------|-------------| | common.v | 48 | 70 | 3 | Contains common definitions and utilities used across multiple modules. | | tactics.v | 224 | 3 | 69 | Contains custom tactics for automated proof strategies in Rcoq. | | sequences.v | 242 | 220 | 25 | Defines operations and properties of sequences of reduction (star, plus and related lemmas). | | miniml/miniml.v | 650 | 763 | 70 | Defines syntax and proofs for mini-ML. | | miniml/miniml_ifthenelse.v | 393 | 137 | 40 | Defines syntax and proofs for mini-ML + if-then-else. | | catala/syntax.v | 521 | 250 | 9 | Defines the syntax of the fragment of $\lambda^\delta$ we are dealing with. | | catala/small_step.v | 315 | 122 | 11 | Describes the traditional small-step semantics of the language. | | catala/continuations.v | 452 | 181 | 35 | Describes the continuation-based small-step semantics of the language. | | catala/typing.v | 394 | 90 | 35 | Provides the typing rules and their verification for the language. | | catala/simulation_cred_to_sred.v | 213 | 219 | 15 | Provides a simulation proof from continuation steps to small steps semantic. | | catala/simulation_sred_to_cred.v | 606 | 609 | 45 | Provides a simulation proof from small steps to continuation steps semantic. | | catala/trans.v | 203 | 182 | 26 | Handles the transformation that removes default terms from $\lambda^\delta$ intermediate languages. | | Total | 4261 | 2846 | 383 | |

This table was computed using the coqwc utility

Hardware Dependencies

Minimal dependencies are required. The entire proof builds in 1 minute on a recent laptop.

Building and Installation

To start developing, you first need to install opam using your package manager. According to [https://opam.ocaml.org/doc/Install.html], you can run the following commands:

bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
opam init

Then, you can execute the following commands to install the artifact dependencies (including Rocq):

opam switch create rocq-catala 4.14.0
opam repo add coq-released https://coq.inria.fr/opam/released
eval $(opam env --switch=rocq-catala --set-switch)
opam repository add rocq-released --all-switches
opam install . --deps-only

Step-by-Step Instructions

Once you have installed the dependencies, you can use Dune to build the Rcoq development:

dune build

Then, start your favorite interactive proof interface for Rcoq.