Core Erlang Formalization

In this repository you can find the formalisation of a subset of Core Erlang in Coq Proof Assistant. The main features of the formalisation include:

• The syntax of Core Erlang
• A big-step, a functional big-step and a frame stack semantics of sequential Core Erlang
• A frame stack semantics for a subset of concurrent Core Erlang
• Proofs of semantic properties
• Program correctness proofs
• Program equivalence concepts, program equivalence proofs
• An interpreter for Core Erlang based on the semantics

Meta

• Author(s):
  • Péter Bereczky
  • Dániel Horpácsi
  • Simon Thompson
  • M.Sc. students from Eötvös Loránd University
• License: GNU Lesser General Public License v3 or later
• Compatible Rocq/Coq versions: 8.20
• Additional dependencies:
  • Stdpp 1.11.0 is required
• Rocq/Coq namespace: CoreErlang
• Related publication(s):
  • A Proof Assistant Based Formalisation of Core Erlang
  • Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
  • Validating Formal Semantics by Property-Based Cross-Testing
  • A Comparison of Big-step Semantics Definition Styles
  • Program equivalence in an untyped, call-by-value functional language with uncurried functions
  • A Formalisation of Core Erlang, a Concurrent Actor Language
  • A frame stack semantics for sequential Core Erlang
  • Program Equivalence in the Erlang Actor Model

Compiling the project

Necessary requirements: Coq v8.20.0, stdpp v1.11.0 and Erlang/OTP v23.0 (not necessary for the Coq developments). The library is compilable by using make. In the following list, we give a brief description about the contents of the files.

Structure of the formalisation

The main module CoreErlang includes the common features for all semantics:

• src/Basics.v: fundamental types, and lemmas about them and the built-in features of Coq;
• src/Syntax.v: the abstract syntax of Core Erlang;
• src/Induction.v: induction principles for the syntax;
• src/Equalities.v: decidable and boolean equalities and comparison based on the abstract syntax;
• src/SideEffects.v: side effect tracing concepts;
• src/Scoping.v: the static semantics (scoping relation) of Core Erlang;
• src/Auxiliaries.v: functions simulating built-in features of the standard library of Erlang, and corresponding tests and lemmas;
• src/Maps.v: concepts supporting the syntax of Core Erlang's maps;
• src/Manipulation.v: definition of substitution, and corresponding theorems;
• src/ScopingLemmas.v: theorems and lemmas about the connection between the static semantics and substitutions;
• src/Matching.v: concepts describing pattern matching for Core Erlang.

The submodule FrameStack includes a frame stack semantics for Core Erlang:

• src/FrameStack/Frames.v: the syntax of frames (which express continuation);
• src/FrameStack/SubstSemantics.v: the definition of a substitution-based frame stack semantics;
• src/FrameStack/Tests/Tests.v: tests about the frame stack semantics;
• src/FrameStack/Tests/ExceptionTests.v: tests about the frame stack semantics;
• src/FrameStack/Termination.v: the definition of an inductive frame stack termination relation;
• src/FrameStack/SubstSemanticsLemmas.v: lemmas and theorems about the properties of the semantics and termination;
• src/FrameStack/LogRel.v: the definition of program equivalence based on logical relations;
• src/FrameStack/Compatibility.v: the compatibility property (a form of congruence) of the logical relations;
• src/FrameStack/CIU.v: the definition of CIU equivalence, and a proof that this definition coincides with the definition based on logical relations;
• src/FrameStack/Examples.v: example program equivalence proofs (based on CIU equivalence);
• src/FrameStack/CTX.v: the definition of contextual equivalence.

Natural and functional big-step semantics are included in the submodule BigStep. We note that in the future the syntax for the big-step semantics (listed below) will be removed, and these semantics will also use the syntax defined in the main module.

• src/BigStep/Syntax.v: the abstract syntax of Core Erlang for the big-step approaches;
• src/BigStep/Induction.v: the induction principle for this syntax;
• src/BigStep/Equalities.v: decidable and boolean equalities and comparison based on the abstract syntax;
• src/BigStep/Helpers.v: helper functions for the semantics;
• src/BigStep/Environment.v: evaluation environment;
• src/BigStep/SideEffects.v: side effect concepts;
• src/BigStep/Auxiliaries.v: the semantics of natively implemented functions and primitive operations;
• src/BigStep/ModuleAuxiliaries.v: auxiliary definitions for handling modules;
• src/BigStep/FunctionalBigStep.v: a functional big-step semantics for testing purposes;
• src/BigStep/BigStep.v: the traditional natural semantics itself;
• src/BigStep/Coverage.v: the previous functional big-step semantics equipped with an additional configuration cell to enable coverage measuring;
• src/BigStep/Tactics.v: evaluation tactic for the traditional big-step semantics.
• src/BigStep/DeterminismHelpers.v: helper lemmas for the proof of determinism;
• src/BigStep/SemanticsProofs.v: some proofs about the properties of the big-step semantics (e.g. determinism);
• src/BigStep/SemanticsEquivalence.v: proof of equivalence of big-step and functional big-step semantics.
• src/BigStep/FullEquivalence.v: a strict program equivalence concept;
• src/BigStep/WeakEquivalence.v: a weakened program equivalence concept;
• src/BigStep/WeakEquivalenceExamples.v: example program equivalences;
• src/BigStep/EquivalenceProofs.v: further example program equivalences.

Tests about the natural and functional big-step semantics:

• src/BigStep/Tests/AutomatedTests.v;
• src/BigStep/Tests/AutomatedSideEffectTests.v;
• src/BigStep/Tests/AutomatedExceptionTests.v;
• src/BigStep/Tests/AutomatedSideEffectExceptionTests.v.

Concurrent semantics based on the sequential semantics of FrameStack is defined in the submodule Concurrent.

• src/Concurrent/PIDRenaming.v: the defintion of renaming for process identifiers and theorems about its properties (w.r.t. the sequential semantics);
• src/Concurrent/ProcessSemantics.v: the semantics for processes (process-local semantics) based on actions propagated from the inter-process semantics;
• src/Concurrent/NodeSemantics.v: the semantics of nodes consisting of processes (inter-process semantics);
• src/Concurrent/NodeSemanticsLemmas.v: theorems about the properties of the concurrent (both process-local and inter-process) semantics;
• src/Concurrent/StrongBisim.v: a definition of program equivalence based on strong bisimulation;
• src/Concurrent/WeakBisim.v: a definition of program equivalence based on weak bisimulation;
• src/Concurrent/BarbedBisim.v: a definition of program equivalence expressed as a barbed bisimulation (which is less restrictive than weak bisimulations);
• src/Concurrent/BisimRenaming.v: a proof that process idenfier renaming is a barbed bisimulation;
• src/Concurrent/BisimReductions.v: further properties of barbed bisimulations, proof of silent evaluation being a bisimulation;
• src/Concurrent/MapPmap.v: a case study about the equivalence of sequential and concurrent list transformation;
• experimental/work-in progress features are included in src/Concurrent/Experimental.

Formally based interpreter for Core Erlang

The interpreter based on the formal semantics is implemented in src/Interpreter, which features function-based variants for the frame stack semantics defined in src/FrameStack and src/Concurrent. The interpreter is based on Coq's extraction mechanism.

• src/Interpreter/Equivalences.v: proves the equivalence of the frame stack semantics and its function-based variants (implemented in StepFunctions.v) for both the sequential and concurrent sublanguages.
• src/Interpreter/ExampleProgExtraction.v: includes a Coq script to extract the (parsed Erlang) programs defined in src/interpreter/ExampleASTs/coqAST.
• src/Interpreter/HaskellExtraction.v: includes a Coq script to extract the (functional) semantics to Haskell. This script also optimises the semantics in several aspects with extraction commands.
• src/Interpreter/HaskellExtractionQuickCheck.v: includes a Coq script to extract the (functional) semantics to Haskell without optimisations.
• src/Interpreter/InterpreterAux.v: defines a number of helper functions for the function-based semantics.
• src/Interpreter/InterpreterAuxLemmas.v: proves a number of properties of the helper functions mentioned above.
• src/Interpreter/OCamlExtraction.v: includes a Coq script to extract the (functional) semantics to OCaml without optimisations.
• src/Interpreter/Scheduler.v: defines a number of helper functions used by the scheduler implemented in Haskell.
• src/Interpreter/StepFunctions.v: defines the function-based variants of the frame stack semantics.
• src/Interpreter/Tests.v: includes a number of unit tests for the function-based semantics.

Furthermore, the folder HaskellSrc includes the implementation of the formally-based, extracted interpreter, as well as an execution tree drawer component (to inspect possible schedulings of a node). In HaskellSrc/QuickCheck we include a script that tests the optimisations made by the extraction to Haskell. In OCamlSrc, we included a preliminary version of the formally based interpreter extracted to OCaml.

Acknowledgement

This project has been supported by the European Union, co-financed by the European Social fund (EFOP-3.6.2-16-2017-00013, EFOP-3.6.3.-VEKOP-16-2017-00002, Thematic Fundamental Research Collaborations Grounding Innovation in Informatics and Infocommunications), and by the Hungarian scholarship programmes ÚNKP-23-1, ÚNKP-23-2, and ÚNKP-23-3.