A Gallina Subset for C Extraction of Non-structural Recursion
Akira Tanaka htanaka-akira aist.go.jpi
National Institute of Advanced Industrial Science and Technology (AIST)
Motivation and Approach: We want a Gallina-to-C translator that is trustworthy and that produces realistic C
code which uses loop structures without stack consumption and doesn’t use polymorphic types.
One particular technical problem is how to handle non-structural recursion. It is required for realistic algorithms
such as breadth-first search. Previous work does not handle non-structural recursion so as to generate realistic C code.
For example, Œuf [2] is another Gallina-to-C translator in Gallina. It uses recursion schemes, such as nat_rect, todescribe recursion and pattern matching. This does not lead to realistic C code.
In this talk, we propose an approach to handle non-structural recursion. Our approach is similar to Œuf in that it
uses a GADT-style typed AST to reflect Gallina terms. However, we do that in such a way as to handle non-structural
recursion. Let us use a running example to explain how we handle non-structural recursion. This loop iterates i to N
increasingly: for (; i < N; i++) {} return true;
In Gallina, the above program corresponds to a non-structural recursion. It requires dependent types such as
well_founded. We assume a user writes our example as follows (N is a parameter; R x y is the relation: N - x < N - y;
Rwf is a proof of well_founded R):
Definition upto_F (i : nat) (f : ∀ (i’ : nat), R i’ i → bool) : bool. Proof.
match i < N as b’ return (b’ = (i < N)) → bool with| false ⇒ fun (H : false = (i < N)) ⇒ true
| true ⇒ fun (H : true = (i < N)) ⇒ f i.+1 _(* hole of type R i.+1 i *)end erefl). ... proof for R i.+1 i snipped ... Defined.
Definition upto := Fix Rwf (fun _ ⇒ bool) upto_F.

refine (We can translate upto to a C-friendly form by reducing Fix. Fix of the standard library Coq.Init.Wf generates arecursive function: upto is a term convertible with fun x ⇒ (fix upto_rec i a := upto_body upto_rec i a) x (Rwf x).
upto_body represents the body of the fix-term which can be defined as follows (the proof part is separated as upto_lemma).
Definition upto_body (upto_rec : ∀ (i : nat), Acc R i → bool) (i : nat) (a : Acc R i) : bool :=let n := N in let Hn : n = N := erefl in let b := i < n in let Hb : b = (i < n) := erefl inmatch b as b’ return b’ = b → bool with| false ⇒ fun Hm : false = b ⇒ true
| true ⇒ fun Hm : true = b ⇒ let j := i.+1 in let Hj : j = i.+1 := erefl inlet a’ := upto_lemma i n b j a Hn Hb Hm Hj in upto_rec j a’end erefl.

In the rest of this abstract, we explain the design of a GADT-style AST with an evaluator with which one can reflect
non-structurally recursive Gallina programs so as to generate realistic C code. Using our AST, it will be possible torepresent upto_body in an inductive type.

1

GA to Represent Non-structural Recursion

We define an intermediate language, GA (Gallina A-normal form). It corresponds to a Gallina subset which includes
dependent type for non-structural recursion. In Coq, it is represented by an inductive type. Here, we explain only thesyntax informally.
We use GA to represent the body of a fix-term because an AST for fix-term is not evaluable1 . GA is A-normal
form: arguments of an application must be local variables. This makes the evaluation order of a GA expression explicit2 .
The body of upto_body (i.e. upto_body without its arguments) is described in GA as follows. upto_rec, i and a are thearguments of upto_body.
leta n Hn := N in leta b Hb := ltn i n in
dmatch b with| false Hm ⇒ true
| true Hm ⇒ leta j Hj := S i in letp a’ := upto_lemma i n b j a Hn Hb Hm Hj in upto_rec j a’end
1 An evaluator for fix-term is not termination checkable.
2 Another critical reason to use A-normal form is that the evaluator is not typable without A-normal form. The type checker cannot unfold
the evaluator (recursive function) when type checking the evaluator. A-normal form avoids appearance of the evaluator in a dependent type.

1

Most constructs of GA correspond directly to Gallina but GA distinguishes non-dependent type and proof (dependenttype) syntactically, hence the variants leta, letp, etc. Functions also have three variants: global functions (ltn, S, true
and N) which are of non-dependent type; lemmas (upto_lemma) which are of dependent type; and recursive functions(upto_rec) whose arguments can be dependently typed but whose return type is non-dependent type.
leta and dmatch correspond to let and match but have extra binders for equality proofs. The equality for leta is anequality between the bound variable and its definition. The equality for dmatch is an equality between the constructor
form and the match item. leta b Hb := ltn i n in E corresponds tolet b := ltn i n in let Hb : b = ltn i n := erefl in E in Gallina. Hb, whose type is b = ltn i n, is used to rewriteb to its definition. dmatch b with | true H1 ⇒ E1 | false H2 ⇒ E2 end, corresponds tomatch b as b’ return b’ = b → T with | true ⇒ fun H1 ⇒ E1 | false ⇒ fun H2 ⇒ E2 end erefl which uses the convoy pattern, and where T is the type of the dmatch expression. H1, whose type is true = b, is used to rewrite b to its
constructor form.
Translating Gallina to GA is easy because we require a source Gallina term convertible with a term in the Gallina
subset defined by GA: polymorphic types are removed by specializing functions with respect to type arguments; ζexpansion inserts let to make a term A-normal form.

2

Coq Implementation of GA and its Evaluator

We have implemented GA in the form of an inductive type. Let us explain this type using a concrete example: thebody of upto_body.
...
Let nT2 := [:: (*n*)nat; (*i*)nat].
Let pT2 := [:: (*Hn*)fun (genv : genviron GT5) (nenv : nenviron nT2) ⇒ (*n*)nenv.1 = glookup GT5 genv "N" tt;(*a*)fun (_ : genviron GT5) (nenv : nenviron nT2) ⇒ Acc R (*i*)nenv.2.1].
...
Definition upto_body_AST : exp GT5 LT5 rT nT1 pT1 bool :=leta GT5 LT5 rT nT1 pT1 nat bool (* n Hn := *) "N" [::] erefl(* leta n Hn := N in*)(leta GT5 LT5 rT nT2 pT2 bool bool (* b Hb := *) "ltn" [:: (*i*)1; (*n*)0] erefl(* leta b Hb := ltn i n in*)
(dmatch GT5 LT5 rT nT3 pT3 bool (*b*)0(* dmatch b with*)(dmatch_cons GT5 LT5 rT nT3 pT3 (*b*)0 bool (* | false Hm *) bool_false [::](* | false Hm ⇒*)(app GT5 LT5 rT nT3 pT4 bool "true" [::] erefl)
(*
true
*)
(dmatch_cons GT5 LT5 rT nT3 pT3 (*b*)0 bool (* | true Hm *) bool_true [:: bool_false](* | true Hm ⇒*)(leta GT5 LT5 rT nT3 pT5 nat bool (* j Hj := *) "S" [:: (*i*)2] erefl(*
leta j Hj := S i in*)
(letp GT5 LT5 rT nT4 pT6 bool (* a’ := *) "upto_lemma" upto_lemma_P(*
letp a’ := upto_lemma*)[:: (*j*)0; (*b*)1; (*n*)2; (*i*)3] [:: (*Hj*)0; (*Hm*)1; (*Hb*)2; (*Hn*)3; (*a*)4](*
i n b j a Hn Hb Hm Hj in *)upto_lemma_pt upto_lemma_P erefl erefl erefl(rapp GT5 LT5 rT nT4 pT7 bool "upto_rec" [:: (*j*)0] [:: (*a’*)0] rtyF erefl erefl)))(*upto_rec j a’*)(dmatch_nil GT5 LT5 rT nT3 pT3 (*b*)0 bool [:: bool_true; bool_false] bool_matcher))))).
(* end*)The inductive type for GA AST has five environment type parameters and an expression type as an index. There aremany environments because we want to distinguish variables to perform proof elimination syntactically. Dependently
typed variables are in pTn and LTn, non-dependently typed variables are in nTn and GTn, rT is for recursive functions(they require special treatment). Moreover, we have both local and global variables. The local variables use de Bruijn
indices: they will be generated automatically inside the translator and invisible to the user.
The main technical features of this type are: (1) We represent a dependent type as a function from global and local
non-dependent environment to a proposition. For example, pT2 contains n = N and Acc R i. (2) We use a matcher torepresent a pattern matching because match-expressions in Gallina are not type-generic. Therefore, we define a matcher
for each inductive type, such as bool_matcher for bool. It contains a function containing just a match-expression. eval
invokes the function for pattern matching. (3) We verify the AST as upto_body = eval upto_body_AST. Since thisevaluation of GA AST is convertible with the original Gallina term, reflexivity is enough to prove it.
After the verification, we import the recursive function into the global environment. Repeating this translation, we
can reflect the whole program into the GA AST3 .
The translation from GA to C should be easy. Proof elimination can be implemented syntactically. After proof
elimination, GA constructs should be translated to C directly: application to function call, dmatch to switch, let tovariable initialization. One non-trivial translation is tail-recursion using goto to avoid stack consumption. It should becompiled similar as a usual loop structure by a SSA-based optimizing compiler.
Conclusion: GA is usable to reflect a Gallina term to a GADT-style AST and its verification. We plan to rewrite
codegen [1] to use GA. We will tackle BFS and its various applications including succinct data structures.
Acknowledgements: This work is supported by JSPS-CNRS Bilateral Program, “FoRmal tools for IoT sEcurity”.

References[1] codegen plugin for Coq, hhttps://github.com/akr/codegen/i.
[2] Mullen, E., et al. Œuf: minimizing the Coq extraction TCB. Proceedings of the 7th ACM SIGPLAN International
Conference on Certified Programs and Proofs. (2018).
[3] Full version of this abstract including the syntax of GA, hhttps://staff.aist.go.jp/tanaka-akira/succinct/i.
3 We import the original recursive function because the AST-based one (fix (eval2AST)) is too complex for the termination checker.

A

The Syntax of GA
f : global function namev : non-dependent type local variabler : recursive function namep : proof variable (dependent type)h : lemma nameC : constructor

app = f v1 . . . vn

global function applicationrapp = r v1 . . . vn p1 . . . pm

recursive function application

papp = h v1 . . . vn p1 . . . pm

lemma application

exp = v
| app
| rapp| nmatch v0 with (| Ci vi1 . . . vimi ⇒ exp)i=1...n end| dmatch v0 with (| Ci vi1 . . . vimi pi ⇒ exp)i=1...n end

pi : Ci vi1 . . . vimi = v0

| leta v p := app in exp

p : v = app| letr v := rapp in exp| letp p := papp in exp| letn v := match v0 with (| Ci vi1 . . . vimi ⇒ exp)i=1...n in exp| letd v := match v0 with (| Ci vi1 . . . vimi pi ⇒ exp)i=1...n in exp

pi : Ci vi1 . . . vimi = v0

Most constructs of GA correspond directly to Gallina (variable, application, match and let). exp represents an
A-normal form expression of non-dependent type. app, rapp and papp corresponds to application in Gallina. app is anapplication whose arguments are non-dependent type values and returns a non-dependent type value. rapp is similar toapp but it can take proof type values. papp is an application which arguments are non-dependent and proof type values
and returns a proof type value. nmatch and dmatch correspond to match-expression. leta, letr, letp corresponds tolet. However dmatch and leta has extra binders as described in Sect. 1. letn and letd are combinations of let withnmatch and dmatch.

B

Overall Structure of Future codegen [1]Hand-written
source term
Coq
OCaml

proof
elimination GA
eval GAGADT AST
non-GADT AST

C AST

C text or
CompCert AST

reflection
source ASTThis abstract explains the design of GADT AST of GA.

C

A-normal Form of upto

upto_body is an A-normal form version of the body of upto. upto_noFix is defined using upto_body and it corresponds
to upto, verified as upto = upto_noFix.

Full source code is available at hhttps://github.com/akr/codegen/blob/ast/sample/ast.vi.
From mathcomp Require Import all_ssreflect.
Require Import Wf_nat.
Parameter N:nat.
Definition m i := N - i.
Definition R := Wf_nat.ltof nat m.
Definition Rwf : well_founded R := Wf_nat.well_founded_ltof _ m.
Lemma upto_lemma (i : nat) (n : nat) (b : bool) (j : nat)(a : Acc R i) (Hn : n = N) (Hb : b = (i < n)) (Hm : true = b) (Hj : j = i.+1) : Acc R j.
Proof. ... Defined.
Definition upto_body (upto_rec : ∀ (i : nat), Acc R i → bool) (i : nat) (a : Acc R i) : bool :=let n := N in let Hn : n = N := erefl in let b := i < n in let Hb : b = (i < n) := erefl in3

match b as b’ return b’ = b → bool with| false ⇒ fun Hm : false = b ⇒ true
| true ⇒ fun Hm : true = b ⇒ let j := i.+1 in let Hj : j = i.+1 := erefl inlet a’ := upto_lemma i n b j a Hn Hb Hm Hj in upto_rec j a’end erefl.
Fixpoint upto_rec (i : nat) (a : Acc R i) {struct a} : bool := upto_body upto_rec i a.
Definition upto_noFix (i : nat) : bool := upto_rec i (Rwf i).
Lemma upto_ok : upto = upto_noFix. Proof. reflexivity. Qed.

D

Type Definitions for the AST of GA (Excerpt)

Full source code is available at hhttps://github.com/akr/codegen/blob/ast/sample/ast.vi.
Definition nenvtype : Type := seq Set.
Definition ntnth (nT : nenvtype) (i : nat) := nth unit nT i.
Fixpoint nenviron (nT : nenvtype) : Set :=match nT with
| [::] ⇒ unit
| T :: nT’ ⇒ prod T (nenviron nT’)
end.
Fixpoint nlookup (nT : nenvtype) (nenv : nenviron nT) (i : nat) : ntnth nT i := ...
Definition gty : Type := nenvtype * Set.
Definition gtype (G : gty) : Set := nenviron G.1 → G.2.
Definition genvtype : Type := seq (string * gty).
Fixpoint gtlookup (gT : genvtype) (name : string) : gty := ...
Fixpoint genviron (gT : genvtype) : Set :=match gT with
| [::] ⇒ unit
| name_G :: gT’ ⇒ prod (gtype name_G.2) (genviron gT’)end.
Fixpoint glookup (gT : genvtype) (genv : genviron gT) (name : string) : gtype (gtlookup gT name) := ...
Definition pty (gT : genvtype) (nT : nenvtype) : Type := genviron gT → nenviron nT → Prop.
Definition ptype (gT : genvtype) (nT : nenvtype) (P : pty gT nT)(genv : genviron gT) (nenv : nenviron nT) : Prop := P genv nenv.
Record cstrT (Tv : Set) : Type := CstrT {cstr_Tms : seq Set;
cstr_cstr : arrow_ntS cstr_Tms Tv; }.
Record Matcher (Tv : Set) (Cts : seq (cstrT Tv)) : Type := mkMatcher {nmatcher (Tr : Set) (v : Tv) : arrow_ntS (nmatcher_branch_types Tv Cts Tr) Tr;
dmatcher (Tr : Set) (v : Tv) : arrow_ntS (dmatcher_branch_types Tv Cts Tr v) Tr }.
Definition bool_true := CstrT bool [::] true.
Definition bool_false := CstrT bool [::] false.
Definition bool_nmatcher (Tr : Set) (v : bool)(branch_true : Tr) (branch_false : Tr) : Tr :=match v with| true ⇒ branch_true| false ⇒ branch_false
end.
Definition bool_dmatcher (Tr : Set) (v : bool)(branch_true : true = v → Tr) (branch_false : false = v → Tr) : Tr :=match v as v’ return v’ = v → Tr with| true ⇒ branch_true| false ⇒ branch_false
end erefl.
Definition bool_matcher := mkMatcher bool [:: bool_true; bool_false] bool_nmatcher bool_dmatcher.
Definition nat_O := CstrT nat [::] O.
Definition nat_S := CstrT nat [:: nat] S.

4

Section Exp_Global_Parameter.
Variables (gT : genvtype) (lT : lenvtype gT) (rT : renvtype gT).
Inductive papp_exp (nT : nenvtype) (pT : penvtype gT nT) (P : pty gT nT) : Type :=| papp_expC : ∀ (name : string) (nargs pargs : seq nat) (nT’ := map (ntnth nT) nargs)(pT’ : penvtype gT nT’) (P’ : pty gT nT’)
(H1 : ltyC gT nT’ pT’ P’ = ltlookup gT lT name)(H2 : transplant_pt gT nT nargs pT’ = map (ptnth gT nT pT) pargs)(H3 : transplant_pty gT nT nargs P’ = P), papp_exp nT pT P.
Inductive rapp_exp (nT : nenvtype) (pT : penvtype gT nT) (Tr : Set) : Type :=| rapp_expC : ∀ (name : string) (nargs pargs : seq nat) (nT’ := map (ntnth nT) nargs)(pT’ : penvtype gT nT’)
(H1 : rtyC gT nT’ pT’ Tr = rtlookup gT rT name)(H2 : transplant_pt gT nT nargs pT’ = map (ptnth gT nT pT) pargs),
rapp_exp nT pT Tr.
Inductive exp (nT : nenvtype) (pT : penvtype gT nT) : Set → Type :=| var : ∀ (i : nat), exp nT pT (ntnth nT i)| app : ∀ (Tr : Set) (name : string) (nargs : seq nat)(nT’ := map (ntnth nT) nargs) (H : gtyC nT’ Tr = gtlookup gT name), exp nT pT Tr| leta : ∀ (Tv Tr : Set) (name : string) (nargs : seq nat)(nT’ := map (ntnth nT) nargs) (H : gtyC nT’ Tv = gtlookup gT name)(Peq : pty gT (Tv :: nT) := leta_eq nT Tv name nargs H),
exp (Tv :: nT) (Peq :: pt_shift0 gT Tv nT pT) Tr → exp nT pT Tr| rappC : ∀ (Tr : Set), rapp_exp nT pT Tr → exp nT pT Tr| letrC : ∀ (Tv Tr : Set), rapp_exp nT pT Tv → exp (Tv :: nT) (pt_shift0 gT Tv nT pT) Tr → exp nT pT Tr| letpC : ∀ (Tr : Set) (P : pty gT nT), papp_exp nT pT P → exp nT (P :: pT) Tr → exp nT pT Tr| nmatch : ∀ (Tr : Set) (i : nat) (Tv := ntnth nT i), nmatch_exp nT pT Tv Tr [::] → exp nT pT Tr| letn : ∀ (Tv2 Tr : Set) (i : nat) (Tv1 := ntnth nT i), nmatch_exp nT pT Tv1 Tv2 [::] →exp (Tv2 :: nT) (pt_shift0 gT Tv2 nT pT) Tr → exp nT pT Tr| dmatch : ∀ (Tr : Set) (i : nat), dmatch_exp nT pT i Tr [::] → exp nT pT Tr| letd : ∀ (Tv2 Tr : Set) (i : nat), dmatch_exp nT pT i Tv2 [::] →exp (Tv2 :: nT) (pt_shift0 gT Tv2 nT pT) Tr → exp nT pT Tr
with nmatch_exp (nT : nenvtype) (pT : penvtype gT nT) :∀ (Tv : Set) (Tr : Set) (Cts : seq (cstrT Tv)), Type :=| nmatch_nil : ∀ (Tv Tr : Set) (Cts : seq (cstrT Tv)), Matcher Tv Cts → nmatch_exp nT pT Tv Tr Cts| nmatch_cons : ∀ (Tv Tr : Set) (Ct : cstrT Tv) (Cts : seq (cstrT Tv))
(Ts : seq Set := Tms4Ct Tv Ct),
let nT’ := nt_shift0s Ts nT in let pT’ := pt_shift0s gT Ts nT pT in
exp nT’ pT’ Tr → nmatch_exp nT pT Tv Tr (Ct :: Cts) → nmatch_exp nT pT Tv Tr Cts
with dmatch_exp (nT : nenvtype) (pT : penvtype gT nT) :∀ (i:nat) (Tv := ntnth nT i) (Tr : Set) (Cts : seq (cstrT Tv)), Type :=| dmatch_nil : ∀ (i : nat) (Tv := ntnth nT i)(Tr : Set) (Cts : seq (cstrT Tv)), Matcher Tv Cts → dmatch_exp nT pT i Tr Cts| dmatch_cons : ∀ (i : nat) (Tv := ntnth nT i)(Tr : Set) (Ct : cstrT Tv) (Cts : seq (cstrT Tv)) (Ts : seq Set := Tms4Ct Tv Ct)(c : arrow_ntS Ts Tv := cstr4Ct Tv Ct), let nT’ := nt_shift0s Ts nT in
let pT’ := (dmatch_pty gT nT i Ts c) :: (pt_shift0s gT Ts nT pT) in
exp nT’ pT’ Tr → dmatch_exp nT pT i Tr (Ct :: Cts) → dmatch_exp nT pT i Tr Cts.
Definition rapp nT pT Tr name nargs pargs pT’ H1 H2 :=rappC nT pT Tr (rapp_expC nT pT Tr name nargs pargs pT’ H1 H2).
Definition letr nT pT Tv Tr name nargs pargopt Popt H1 H2 body :=letrC nT pT Tv Tr (rapp_expC nT pT Tv name nargs pargopt Popt H1 H2) body.
Definition letp nT pT Tr name P nargs pargs pT’ P’ H1 H2 H3 body :=letpC nT pT Tr P (papp_expC nT pT P name nargs pargs pT’ P’ H1 H2 H3) body.
End Exp_Global_Parameter.

E

Reasoning and Multiple Arguments

upto uses Fix to define the non-structurally recursive function. It makes us possible to reason about it using Fix_eq inthe standard library Coq.Init.Wf and the axiom of functional extensionality.
However, Fix can represent a recursive function with only one argument. We can define multiple arguments versionof Fix for each number of arguments. Fix_eq-like reasoning lemma is also provable using primitive projections.

5