c_operational_semantics_lean4

This project contains a Lean 4 port of the CompCert C front-end operational semantics. The port is co-developed with Codex. This is an experimental project.

Ported source snapshot:

• CompCert version: 3.17
• Local commit: 049312757b748055ac26b270b04af32911b5bb4d
• Source files ported from: cfrontend/Ctypes.v, cfrontend/Cop.v, cfrontend/Csyntax.v, cfrontend/Csem.v, cparser/Cabs.v, cparser/Lexer.mll, and cparser/Parser.vy.

The port is organized by role. Shared value, integer, pointer, float, target configuration, and memory definitions live under CSem/Common; CompCert C frontend types, operators, syntax, and small-step semantics live under CSem/Cfrontend; parser and lexer code lives under CSem/Cparser; and the generic LR parser-generator infrastructure lives under CSem/Parsing/LR. External behavior that is intentionally target- or environment-specific is parameterized through ExternalCallOracle; built-in volatile access, malloc/free, memcpy, annotation, debug, and common runtime cases are modeled directly in CSem.Cfrontend.Csem.

Build with:

lake build CSem

Run parser tests with:

lake exe parser_tests
lake exe parser_generator_tests
lake exe parser_vy_importer_tests
lake exe parser_vy_full_grammar_tests

Generate a Lean module containing the Cabs AST for a C translation unit with:

lake exe c_parse_export --namespace GeneratedCParse.Example input.c Generated/Example.lean

The generated file defines sourcePath, source, and translationUnit. By default it also includes a parser replay check over the printed AST; pass --no-check to emit only the AST module for faster bulk generation.

Generate a Lean module containing the elaborated CProgram for a C translation unit with:

lake exe c_elab_export --namespace GeneratedCProgram.Example --main main input.c Generated/Example.lean

The generated elaboration file records sourcePath, source, mainName, identifiers, functionNames, and program.

The parser test runner reads a case manifest from Tests/parser_cases.txt by default. Each manifest entry points at a .c source file under Tests/parser_cases/. Pass another manifest path as the first argument to use a different fixture.

Regenerate or inspect the imported Parser.vy grammar with the repo-local Rust importer:

tools/parser_vy_importer path/to/Parser.vy --emit summary

The wrapper dispatches to the Cargo project in tools/rust.

The Lean toolchain is pinned in lean-toolchain.

License:

This project is distributed under the GNU Lesser General Public License, version 2.1 or, at your option, any later version. Portions are derived from the CompCert verified compiler 3.17, whose relevant cfrontend/, cparser/, common/, and lib/ files are available under LGPL-2.1-or-later. See LICENSE and NOTICE.

Parser status:

• CSem.Cparser.Cabs ports the raw Cabs AST produced by CompCert's C parser.
• CSem.Cparser.Lexer ports the keyword, operator, comment, literal, and source-location lexer layer. Raw identifiers are classified by the parser state using the typedef context.
• CSem.Parsing.LR is a generic LR parser generator with table construction, conflict handling, runtime driver, and a correctness theorem surface.
• CSem.Cparser.ParserVyGenerated contains the imported CompCert Parser.vy grammar data, including the 337 generated productions and translated semantic actions.
• CSem.Cparser.ParserVyGeneratedParser lowers that imported grammar through the generic parser generator, runs it with stateful typedef-name feedback, and decodes generated values back to Cabs.Definition.
• CSem.Cparser.Parser is the public parser umbrella. Its translationUnitFile entry point uses the imported Parser.vy parser; recursive parser helpers remain available for expression-level utilities and tests.