Verified Software Toolchain (VST)

This directory contains the Coq files used for the 'Verified Compilation for Shared-Memory C' paper (ESOP'14). The files are organized by the sections of the paper they support:

Section 3: Core Semantics and Memory

• core_semantics.v: Definitions of core_semantics, cooperative core_semantics, and multistep relation lemmas.
• mem_lemmas.v: Auxiliary definitions including mem_forward and mem_wd ("closed").

Section 4: Forward Simulations and Compiler Correctness

• forward_simulations.v: Logical simulations on cores. Module Forward_simulation_inj (starting at line 299) corresponds to Definition 4.1 in the paper.
• forward_simulations_lemmas.v: Lemmas regarding the simulation definitions.
• compiler_correctness.v: Lifts simulations to programs.
• compcert_compiler_correctness.v: Relates compiler correctness to CompCert 2.0's memory-oblivious whole-program simulations.

Transitivity Proof Files:

• FiniteMaps.v: Auxiliary data structure for interpolating memories.
• mem_interpol*.v: Interpolation lemmas (EE, EI, etc.) and constructions; all collected in mem-interpolants.v.
• forward_simulations_trans.v: Proof of transitivity using interpolations.
• compiler_correctness_trans.v: Lifts transitivity of core forward simulations to programs.

Section 5: Safety Preservation

• safety_preservation.v: Safety and semantics preservation, including restricted program safety for closed whole programs. (General program safety is in step_lemmas.v).

Section 6: CompCert Integration

• Includes files from CompCert 2.0 (e.g., Switch.v, Ordered.v, Cminor.v, Csharpminor.v, Cminorgen.v, Cminorgenproof.v).
• CminorgenproofRestructured.v: Restructured version of Cminorgenproof.v to isolate instruction cases.
• Cminor_coop.v & Csharpminor_coop.v: Cooperative core semantics formulations.
• CminorgenproofSIM.v: Adapted proof of CompCert's Cminorgen phase.

Linking and File Systems (Not discussed in paper)

• linking.v: Extensional model of core semantics linking.
• linking_simulations.v: States the linking simulation theorem.
• linking_proof.v: Proves the linking simulation theorem.
• fs_linking.v: Model of a simple file system and its linking simulation theorem.

This directory contains the formalization of "Structured logical simulation relations for blunderless separate compilation". The files are organized by the sections of the corresponding research paper:

Section 2: Core Semantics and Memory

• mem_lemmas.v: Auxiliary definitions, mem_forward, and CompCert memory model lemmas.
• core_semantics.v: Definitions for core_semantics, cooperative core_semantics, and multistep relations.

Section 4: Injections and Effects

• StructuredInjections.v: Structured injections and associated lemmas.
• effect_semantics.v: Single- and multi-step execution decorated with memory effects.
• effect_simulations.v: Contains Lemma 1 (inject_restrict and REACH_inject).

Section 5: Structured Logical Simulation Relations (SLSRs)

• effect_simulations.v: Defines SLSRs (at the end of the file). Includes replace_locals/replace_externs (corresponding to leakOut/leakIn).
• effect_simulations_lemmas.v: SLSR composition and multistep simulation diagrams.

Section 6: Transitivity and Interpolation

• rg_lemmas.v: Rely-guarantee propositions 1 and 2.
• effect_simulations_trans.v: Main transitivity proof (Theorem 1: eff_sim_trans).
• effect_corediagram_trans.v: Transitivity of the core diagram of SLSRs.
• effect_interpolants.v: Interpolation lemma as a Coq module type.
• effect_interpolation_II.v: Construction of interpolating memory.
• effect_interpolation_proofs.v: Formal instantiation of the interpolation module.

Section 7: CompCert Adaptations

Located in ./compcert_adapt, these files adapt CompCert semantics (Clight, Csharpminor, Cminor, CminorSel, RTL) to the Core Semantics interface and support effect annotations.

• [Language]_coop.v: Cooperative core semantics adaptations.
• [Language]_eff.v: Effect annotation adaptations.
• [Language]genproofEFF.v: Adaptations of CompCert simulation proofs to SLSRs.
• effect_properties.v: Contains Lemma 2 (REACH_Store).

Section 8: External Specs and Trace Semantics

• extspec.v: Axiomatic specifications of external functions.
• trace_semantics.v: Memory-instrumented events and trace semantics.
• closed_safety.v: Safety for trace semantics.
• open_semantics_preservation.v: Proof of Theorem 2 (trace_refinement) and Corollary 1 (corollary).

To prove a program correct using VST, the recommended approach is a multilevel verification strategy. This involves two distinct steps that can be composed into a single theorem:

1. Low-level Verification: Prove that a low-level program (e.g., a C program) correctly implements a functional model (often written in Coq/Gallina). This step uses separation logic to specify how C variables and data structures encode the functional model's values.
2. High-level Verification: Separately prove that the functional model satisfies a high-level specification (the desired mathematical property).

Key Concepts for Verification Quality:

• Multilevel/High-level: The verification includes both the implementation-to-model and model-to-specification steps.
• Unified: The low-level and high-level proofs are performed in the same logical framework so they can be composed into one machine-checkable theorem.
• Modular/Semimodular: Verification is done in the style of Verified Software Units (VSU), where each function is verified against its own specification, and callers depend only on the callee's specification, not its body.