Scallion Proofs

Overview

This project proves the correctness of the parsing with derivatives algorithm used in Scallion, which is presented in this PLDI paper.

Roadmap

• Structures.v contains the definition of the Syntax type.
• Matches.v describes when does a syntax associate a value with a token sequence.
• FocusedSyntax.v contains the definition of focused syntaxes, and the unfocus function that returns a standard Syntax.
• The FocusedSyntax*.v files contain the definitions of functions on focused syntaxes and their associated lemmas.
• Description.v contains the definition of descriptions, which allow to
• The *Descr.v files contains the descriptions for the functions on syntaxes: nullable, productive, first, should-not-follow, has-conflict. specify functions on syntaxes using inductive rules.
• DescriptionInd.v contains the inductive semantics of descriptions
• PropagatorNetwork.v contains a formalisation of propagator networks with termination guarantees.
• DescriptionToFunction.v builds propagator networks to create functions based on descriptions.
• The DescriptionToFunctionSoundness.v and DescriptionToFunctionCompleteness.v files contain the proofs of soundness and completeness of this construction.
• FocusedSyntaxParse.v contains the proof of correctness (soundness and completeness) for the parsing algorithm based on derivatives of focused syntaxes.
• dependencies.pdf contains a graph of the dependencies between the files.

Installing the dependencies

These proofs require Coq 8.11.0 and Coq Equations 1.2.1+8.11. If you have opam version 2 installed, these can be installed using the following commands (tested on Linux). Replace "new-switch-name" by a name you like for the fresh switch.

The opam binaries are available on https://github.com/ocaml/opam/releases.

opam init # if you've never used opam before
opam switch create new-switch-name 4.09.0
eval $(opam env)
opam install coq.8.11.0
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-equations.1.2.1+8.11

With older versions of opam, replace the first two commands with:

opam init # if you've never used opam before
opam switch new-switch-name --alias-of 4.09.0
eval `opam config env`

If you have trouble installing, please refer to the official webpages:

• https://coq.inria.fr/download
• https://github.com/mattam82/Coq-Equations

Compiling the proofs

The proofs can be compiled using:

./configure
make -j4      # takes 15/20 minutes to complete

Cross-references with the PLDI paper

• Theorem 3.1: The matches predicate in Matches.v forces this type
• Theorem 4.1: productive_ind_correct in ProductiveInd.v
• Theorem 4.2: nullable_ind_correct in NullableInd.v
• Theorem 4.3: first_ind_correct in FirstInd.v
• Theorem 4.4: should_not_follow_ind_sound in ShouldNotFollowInd.v
• Theorem 4.6: non_ambiguous_ll1 in FocusedSyntaxParse.v
• Theorem 4.7: should_not_follow_ind_correct in ShouldNotFollowComplete.v
• Theorem 4.8: productive_left_recursive_not_ll1 in LeftRecursive.v
• Theorems of Section 5 are not in Coq, as they are not relevant for the zippy algorithm with focused syntaxed.
• Theorem 6.2: plug_correct in FocusedSyntaxPlug.v
• Theorem 6.3: locate_not_none2 in FocusedSyntaxLocateMatches.v
• Theorem 6.4: locate_first_ind in FocusedSyntaxLocate.v
• Theorem 6.5: locate_correct in FocusedSyntaxLocateMatches.v
• Theorem 6.6: pierce_correct in FocusedSyntaxPierceMatches.v
• Theorem 6.7: matches_unfocus_elem in FocusedSyntax.v
• Theorem 6.8: derive_preserves_ll1 in FocusedSyntaxDerive.v
• Theorem 6.9: derive_none in FocusedSyntaxDerive.v
• Theorem 6.10: derive_sound in FocusedSyntaxDerive.v
• Theorem 6.11: result_correct in FocusedSyntaxNullable.v
• Theorem 6.12: parse_correct in FocusedSyntaxParse.v

Acknowledgements

We thank the anonymous reviewers of the artifact evaluation for their suggestions on improving the presentation of the proofs.