# Pleasant Imperative Program Proofs with GallinaC

Frédéric Fort, David Nowak, Vlad Rusu

► To cite this version:

Frédéric Fort, David Nowak, Vlad Rusu. Pleasant Imperative Program Proofs with GallinaC. Working Formal Methods Symposium (FROM 2025), Sep 2025, Iași, Romania. pp.24-32, 10.4204/EPTCS.427.2 . hal-05405959

HAL Id: hal-05405959

https://hal.science/hal-05405959v1

Submitted on 9 Dec 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Pleasant Imperative Program Proofs with GallinaC

Frédéric Fort¹

David Nowak¹

Vlad Rusu²

¹ Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRISTAL, F-59000 Lille, France

² Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRISTAL, F-59000 Lille, France

## 1 Introduction

Even with the increase of popularity of functional programming, imperative programming remains a key programming paradigm, especially for programs operating at lower levels of abstraction. When such software offers key components of a Trusted Computing Base (TCB), e.g. an operating system kernel, it becomes desirable to provide mathematical correctness proofs.

However, current real-world imperative programming languages possess “expressive”, i.e. overly permissive, semantics. Thus, producing correctness proofs of such programs becomes tedious and error-prone, requiring to take care of numerous “administrative” details. Ideally, a proof-oriented imperative language should feature well-behaved semantics while allowing typical imperative idioms.

To obtain a high-degree of confidence in the correctness of such a language, its tools should be developed inside a proof-assistant such that program proofs, be it that the compiler passes preserve semantics or any proof written by language users, are machine checked.

Such an *embedding* of a programming language may either be deep or shallow [19]. With *deep embedding*, the language is defined using the available data structures of the implementation language, e.g. inductive types in the Rocq proof assistant [15]. With *shallow embedding*, the programming language is directly a subset of the implementation language.

Historically, deep embedding has been considered the preferred approach for sufficiently complex languages. Indeed, deep embedding allows to define arbitrary complex languages independent from the limitations of implementation language. For instance, Gallina, the functional programming language of the Rocq proof assistant is total for soundness reasons, excluding turing-completeness. Yet, inductive proposition may define the semantics of a turing-complete language, such as C [8].

However our experience has shown that, deep embedding poses practicability issues. Indeed, since the language is completely constructed bottom-up, every property, theorem, proof tactic has to be defined and proven from the ground up. On the opposite, since shallow embedding uses a subset of the implementation language, if the language is sound, certain theorems are for free and the usual proof tactics are available.

Previous work using shallow embedding has produced substantial programs and their correctness proofs such as a hypervisor with formally-proven isolation guarantees [4, 5] or a real-time scheduler using the Earliest-Deadline First policy [16]. However, their source languages were not turing-complete. In particular, they lacked a generic recursion mechanism: Their *while* loop construct used fuel, i.e. an at compile time defined maximum iteration count.

Recent work [2] has shown how to define partial (co-)recursive functions directly inside the Gallina language. This enables us to define a shallow embedding of a potentially unbounded *while* loop, bringing turing-completeness to the Gallina language.
## Contributions

In this paper, we present *GallinaC*, a shallow embedding of a Turing-complete imperative language directly inside the functional programming language of the Rocq proof assistant, Gallina. In particular, it features a truly generic and unbounded *while* loop. Having a functional core means proofs about *GallinaC* programs may use the same tactics as proofs about pure functional ones.

Compilation from *GallinaC* to binary is possible through the CompCert certified compiler. A chain of forward simulations guarantees that compilation passes preserve semantics.

Work on *GallinaC* is still under progress, but we present first promising results. A prototype implementation has shown the viability of *GallinaC* with the correctness proof of a list reversal procedure for linked-lists of unknown size. We currently focus on the forward simulation between the *GallinaC* intermediate representation (IR) and Cminor, the entry language of the CompCert back-end. The *GallinaC* sources are available online (https://gitlab.cristal.univ-lille.fr/ffort/gallinac).

## 2 Motivational Example

```
Definition reverse ptr :=
  var node <- ptr;
  var new_next <- NULL;
  let deref_next :=
    do ptr <- read_var node;
    do val <- read_ptr (ptr + 1);
    ret val
  in
  let cond :=
    do curr <- read_var node;
    ret (negb (curr =? NULL))
  in
  while cond {{
    do curr <- read_var node;
    do next <- deref_next;
    do prev <- read_var new_next;
    write_ptr (ptr + 1) prev;;
    write_var node next;;
    write_var new_next curr
  }};;
read_var new_next
```

<caption>Figure 1: List reversal in *GallinaC*</caption>

As a motivational example, let us consider the program from Figure 1. Provided a pointer that points to a member of a simply-linked list, it performs an in-place list reversal by swapping pointers. Linked list nodes are composed of two memory words, one holding the value and one holding the pointer to the next list node.

The first two lines declare mutable variables which hold respectively the list node currently under consideration and the node's new next pointer. Obviously, at program start these are initialized to the list's entry pointer and the typical sentinel value NULL.

Next, two helper functions are declared. The first, *deref_next*, loads the list node pointed to by the current node's next pointer. The second, *cond*, is the while loop's invariant: the pointer to the next node to consider is not NULL.

The remainder is the “main” function of the program. The core is a while loop that breaks once node holds the NULL pointer. At each loop iteration, the current node’s next field is updated. For the next iteration, node and new_next are set respectively to the current node’s next field and the current node. The program terminates by returning the address of the list’s new first node.

This program illustrates *GallinaC*'s new *while* loop. Note that the loop is not annotated with a fuel amount or any other kind of restriction: a programming error could produce an infinite loop.
<figure><img src="image_2.png" /><figcaption>Figure 2: GallinaC expressions and commands</figcaption></figure>

## 3 Language Design

GallinaC programs are Gallina terms with type program S A. The program monad incorporates state, failure and non-termination effects. While it could theoretically be constructed using monad transformers, its current implementation is a custom monad. The type parameter S is the type of the state, i.e. the heap and store of the program. The type parameter A is the return type of the monadic computation, assuming it doesn't fail.

The non-termination monad is adapted from [2]. The monad functor is the option type where None encodes bottom, i.e. non-termination. We first define the *while functional*:

```
Definition whileF
{S : Type} (cond : program S bool)
(W : program S unit -> program S unit)
(body : program S unit) : program S unit :=
If cond then (body ;; W body) else ret tt.
```

As can be seen, the recursive, non-guarded, call is replaced by a call to an additional argument W. We then leverage Kleene's fixed-point theorem stating that a continuous function with signature $A \to A$ where A is equipped with a CPO has a least fixed-point. For our `whileF` this fixed-point is the “true” `while`. Continuity itself is proven using Haddock's theorem [2].

For convenience, we offer the classical monadic notations to simplify the writing of GallinaC programs: return (`ret`) and bind (`do x <- ret 5; ret (x + 3)`), as well as immediate failure (`fail`), infinite loop (`loop`) and discarding bind (`some_side_effect ;; ret true`).
<figure><img src="image_3.png" /><figcaption>Figure 3: Shallow separation logic definitions</figcaption></figure>

The language distinguishes *expressions* from *commands*. Expressions include operations on variables, the unit expression `tt`, booleans, and natural numbers with fixed-width unsigned integer semantics, as well as pointers.

Commands contain the side-effectful part of the language. Monadic return and bind use the typical notations and semantics. Control-flow (function calls, `if` branches and turing-complete `while` loops) is reserved to commands. Note in particular that the condition of the `while` loop is itself a command.

A *store* is accessible using the `var`-family of commands. Variables in the store are accessible by their name and possess a unique location in memory for their entire lifetime, enabling both reads and writes to them. This distinguishes them from variables bound with `do` which may only be read from once set and may be moved around and dropped by the compiler for optimization reasons. A similar distinction exists in CompCert between temporaries and locals which are respectively equivalent to `do` and `var` variables.

A *heap* is accessible using the `alloc`, `free` and `*-ptr` commands. Pointers are distinct from integers in that they possess not only an address but also a *provenance* [9]. A provenance records the memory region a pointer may access, typically the region it was allocated from. It is a programming error to use a pointer to access memory outside its provenance. Note that this does not prevent to use a pointer to a data structure field to access other fields, nor to traverse a linked-list by following successive pointers. Provenance formalizes concepts already existing in the C standard [17, 18] and MISRA C [1].

# 4 Shallow Separation Logic

Separation logic [11, 12, 13] is an extension of Hoare logic [3] aimed at reasoning about mutable data structures with pointers. Recall that the *Hoare triple* `{ P } c { Q }` states that executing some code `c` in a state where proposition `P` holds does not produce a “crash” (more specifically any incoherent state) and that proposition `Q` holds in the final state.

Separation logic introduces two logical connectives, `**` and `-*`, called respectively *separating conjunction* and *separating implication*. If the separating conjunction `P**Q` holds, then the program state
<figure><img src="image_4.png" /><figcaption>Figure 4: GallinaC workflow</figcaption></figure>

can be divided into two clearly disjoint parts such that *P* holds for the first part and *Q* for the second part. The separating implication *P*\*\* *Q* states that if the current heap were extended such that *P* held, then *Q* would also hold. More intuitively, if code execution resulted in a state where *P* held, then so would *Q*.

Together with the *frame rule*, separation logic simplifies the proof process for realistic imperative programs. It states that any Hoare triple {*P*} *c* {*Q*} can be extended to a more complete context {*P*\*\* *R*} *c* {*Q*\*\* *R*} provided that *c* does not mutate any free variables in *R*.

Logically, our implementation of separation logic is shallow as well. We solved common issues with shallow embeddings [19] by leveraging Rocq's automated proof-search utilities. Lemmas may be collected in proof databases which the *auto/eauto* tactics may leverage to solve the given goal.

Moreover, note that unlike [10], we opted for an “initially weakly-typed” approach to separation logic. All programs have a type of the form *program S A*. Predicates are a proof-only construct added on top. Indeed, in our experience working both with system and proof engineers, requiring the right proof annotations upfront does not scale to large programs such as OS kernels [4].

Figure 3 shows the definitions of the core definitions. Predicates *P*, *R* discussed above are terms with type *S* → *Prop*, i.e. propositions which depend of the state. Output predicates like *Q* above additionally may depend upon the output produced by the program code.

*Separating conjunction* is defined as *star* (a notation for the infix \*\* is provided), a predicate stating that for any state *s*, we can define sub-states *s*1 and *s*2 such that their stores are equal to the store of *s*, their heaps are a partitioning of the heap of *s*, and *P* and *R* hold in their relative states. *Separating implication* is defined as predicate *wand* (and a notation \*-\* ) stating that for any states *s*, *s*′ and heap *hp*, if *hp* is the union of the states’ heaps and *P* is true in *s*’, then *R* is true in the state with the extended heap.

# 5 Architecture

The typical workflow when using GallinaC is presented in Figure 4. Green arrows represent computation steps which are associated with formal proofs. Orange arrows represent computation of not formally-proven dependencies, but for which validation tools exist. Red arrows represent computation steps which are essentially unprovable, we will discuss how to address this below. Recall that GallinaC programs are monadic Gallina terms with type *program S A* where *S* is the heap and *store* and *A* is the return type.

Development starts inside the “perfect Rocq world” where programs can be composed and defined using typical Rocq commands (Figure 1). From there, propositions on these programs can be proven
<figure><img src="image_5.png" /><figcaption>(b) Deep GallinaC</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>(c) Correctness by denotation</figcaption></figure>

<caption>Figure 5: Shallow and Deep GallinaC comparison</caption>

directly on the monadic program using the typical commands and tactics for proofs. To produce a binary, an extraction process operates on a deep embedding (Figure 5). A chain of forward simulation proofs guarantees the compilation process’ correctness.

## 5.1 Reification

Producing a binary which may be used outside the Rocq proof assistant requires an *extraction plugin*. However, the default extraction plugins target high-level garbage-collected functional languages (OCaml, Haskell) which are incompatible with bare-metal programming. Thus, we provide a custom extraction path relying on MetaCoq [14] and CompCert [8].

Provided a Rocq term `t`, MetaCoq allows to *reify* it into an inductive term representing the term's AST. This inductive term is then processed, resulting in an AST for deeply-embedded GallinaC as shown in Figure 5b.

Note however, that this reification process is happening necessarily outside the Rocq proof assistant, producing a break in trust. To regain confidence in the deeply-embedded GallinaC, we equip it with a denotational semantics.

The denotational semantics undoes the reification process directly inside the proof assistant. Thus, if the reification process is correct, denotation should yield the original shallow GallinaC program. In essence, while we can't prove the reification process correct for *all* programs, we can show it correct for *any* program by simple reflexivity (Figure 5c).
## 5.2 Compilation

Instead of writing our own compiler, we rely on CompCert [8], a formally-verified compiler for a reasonable subset of C. Our entry-point is the Cminor language, the highest-level language of the back-end [7]. While still resembling C, Cminor is much “simpler”, e.g. types are completely discarded and the stack is a primitive value that must be allocated with the correct size at function entry. To bridge the gap between the deep GallinaC and Cminor, we first compile to an Intermediate Representation (IR).

Our IR still resembles GallinaC, with a distinction between commands and expressions for instance, but it simultaneously follows the conventions of CompCert languages. For instance, identifiers are no more strings, but positives. Moreover, all side-effectful operations are both performed in lockstep inside the CompCert memory and the GallinaC state to guarantee coherence.

Once the IR is translated to Cminor, the usual CompCert passes are applied. Note in particular that we did not patch CompCert, we use for all our developments the publicly available stable version. The correctness of these compilation passes is guaranteed by a chain of forward simulations, i.e. the proof that the behaviors of the source program are preserved in the compiled program.

Note that while we verified the correctness of the MetaCoq reification using a denotational semantics, CompCert uses for its compilation an operational semantics. As such, the step from deep GallinaC to our IR could potentially distort the semantics of our programs. To dispel all such doubts, we have proven that the denotational and operational semantics of deep GallinaC *agree*. More specifically: evaluation of the operational semantics preserves denotation.

Finally, the last step, code generation, must necessarily execute outside the Rocq environment. This last step is thus, necessarily less trusted. The CompCert team having been faced with the same issues, they provide tools to validate such programs nonetheless [6, 8].

## 6 Prototype

Work on GallinaC is still ongoing. We developed a first prototype version to show the feasibility of our approach. We programmed the list reversal program shown above, showed its correctness and extracted a binary from it. However, many aspects were left explicitly simplistic. Most notably, the store consisted only of two global read-write variables and there existed no distinction between integers, pointers and addresses.

This approach however hit a wall when trying to prove the forward simulation of compilation passes. Thus, a considerable amount of time was invested in designing sound interfaces for the different aspects of imperative programming. These new interfaces introduced breaking changes in the user-facing monadic language. Our current approach is bottom-up and we are focusing on the proof of forward simulation between the IR and Cminor. We will return to the user-facing language and tooling after this.

We plan also to increase the expressivity of the language. For instance, early loop exit is not yet supported. To preserve the adequacy, with program proofs, we are looking into replacing the program monad with a Freer or Continuation monad.

## 7 Conclusion and Future Work

In this paper, we presented GallinaC, a collection of programming tools for formally-proven low-level imperative code. Developers write programs in a monadic subset of Rocq's functional language, Gallina. Proofs about these programs may be performed directly in the same programming environment and
separation logic makes proofs feasible. The extraction to concrete binary code is performed in two steps. First, MetaCoq allows to reify the program into a deep embedding. A denotational semantics guarantees the correctness of this step. Second, the deep embedding is compiled using the CompCert compiler to assembly. A chain of forward simulation proofs on operational semantics guarantee the correctness of this process. We have proven the equivalence of these semantics, showing that the compilation process is truly correct end-to-end.

Current work focuses on integrating all components and finalizing the correctness proofs of compilation. In future work, we will want to design tools to guarantee that any proof on monadic GallinaC holds for the compiled assembly.

## References

[1] Roberto Bagnara, Abramo Bagnara & Patricia M. Hill (2018): *The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software*. In Andreas Podelski, editor: *Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings, Lecture Notes in Computer Science* 11002, Springer, pp. 5-23, doi:10.1007/978-3-319-99725-4_2.

[2] Horatiu Cheval, David Nowak & Vlad Rusu (2024): *Formal definitions and proofs for partial (co)recursive functions*. *J. Log. Algebraic Methods Program.* 141, p. 100999, doi:10.1016/J.JLAMP.2024.100999.

[3] C. A. R. Hoare (1969): *An Axiomatic Basis for Computer Programming*. Commun. ACM 12(10), pp. 576-580, doi:10.1145/363235.363259.

[4] Narjes Jomaa, David Nowak, Gilles Grimaud & Samuel Hym (2018): *Formal proof of dynamic memory isolation based on MMU*. *Sci. Comput. Program.* 162, pp. 76-92, doi:10.1016/J.SCICO.2017.06.012.

[5] Narjes Jomaa, Paolo Torrini, David Nowak, Gilles Grimaud & Samuel Hym (2018): *Proof-Oriented Design of a Separation Kernel with Minimal Trusted Computing Base*. 76, doi:10.14279/TUJ.ECEASST.76.1080.

[6] Daniel Kästner, Ulrich Wünsche, Jörg Barrho, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy & Sandrine Blazy (2018): *CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler*. In: *ERTS 2018: Embedded Real Time Software and Systems*, SEE. Available at http://xavierleroy.org/publi/erts2018_compcert.pdf.

[7] Xavier Leroy (2009): *A Formally Verified Compiler Back-end*. *J. Autom. Reason.* 43(4), pp. 363-446, doi:10.1007/S10817-009-9155-4.

[8] Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister & Christian Ferdinand (2016): *CompCert - A Formally Verified Optimizing Compiler*. In: *ERTS 2016: Embedded Real Time Software and Systems*, SEE. Available at http://xavierleroy.org/publi/erts2016_compcert.pdf.

[9] Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson & Peter Sewell (2019): *Exploring C semantics and pointer provenance*. *Proc. ACM Program. Lang. 3*(POPL), pp. 67:1-67:32, doi:10.1145/3290380.

[10] Aleksandar Nanevski, J. Gregory Morrisett & Lars Birkedal (2008): *Hoare type theory, polymorphism and separation*. *J. Funct. Program.* 18(5-6), pp. 865-911, doi:10.1017/S0956796808006953.

[11] Peter W. O'Hearn (2019): *Separation logic*. Commun. ACM 62(2), pp. 86-95, doi:10.1145/3211968.

[12] John C. Reynolds (2002): *Separation Logic: A Logic for Shared Mutable Data Structures*. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, IEEE Computer Society, pp. 55-74, doi:10.1109/LICS.2002.1029817.

[13] John C. Reynolds (2005): *An Overview of Separation Logic*. In Bertrand Meyer & Jim Woodcock, editors: *Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions, Lecture Notes in Computer Science* 4171, Springer, pp. 460-469, doi:10.1007/978-3-540-69149-5_49.
[14] Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau & Théo Winterhalter (2020): *The MetaCoq Project*. *J. Autom. Reason.* 64(5), pp. 947-999, doi:10.1007/S10817-019-09540-0.

[15] The Rocq Development Team (2025): *The Rocq Reference Manual*. https://rocq-prover.org/doc/master/refman/index.html.

[16] Florian Vanhems, Vlad Rusu, David Nowak & Gilles Grimaud (2022): *A Formal Correctness Proof for an EDF Scheduler Implementation*. In: 28th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2022, Milano, Italy, May 4-6, 2022, IEEE, pp. 281-292, doi:10.1109/RTAS54340.2022.00030.

[17] WG14 (2001): *Defect Report 260*. Available at https://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_260.htm.

[18] WG14 (2011): *ISO/IEC 9899:2011*.

[19] Martin Wildmoser & Tobias Nipkow (2004): *Certifying Machine Code Safety: Shallow Versus Deep Embedding*. In Konrad Slind, Annette Bunker & Ganesh Gopalakrishnan, editors: *Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, Lecture Notes in Computer Science* 3223, Springer, pp. 305-320, doi:10.1007/978-3-540-30142-4_22.