Formal description of Coq’s termination checker

Question

Coq’s built-in termination checker accepts some rather intricate recursion patterns with functional values in data types, as shown by this example

Inductive Z_inf_branch_tree : Set :=
  Z_inf_leaf : Z_inf_branch_tree
| Z_inf_node : Z→(nat→Z_inf_branch_tree)→Z_inf_branch_tree.

Fixpoint n_sum_all_values (n:nat)(t:Z_inf_branch_tree){struct t} : Z :=
(match t with
| Z_inf_leaf ⇒ 0
| Z_inf_node v f ⇒ v + sum_f n (fun x:nat ⇒ n_sum_all_values n (f x)) end ).

(taken from from Chapter 7.3.5.2 here https://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf).

I am looking for a formal description of the termination checker at work here, in order to reimplement it in a different system? Is it written down somewhere accessible?

Answer 1

Lennard Gäher has implemented Coq's guard checker in Coq on top of MetaCoq as part of a lecture project I advised here:

https://github.com/lgaeher/metacoq/blob/guarded/guarded/guardchecker.v

It has lots of comments and examples is the most accessible description I know of, the other two existing descriptions I am aware of being the comments in the OCaml code of Coq's implementation and this slide set by Bruno Barras, both of which served as sources for Lennard's code.

Lennard's code turns Coq's guardedness checker off to avoid making some functions structurally recursive, and thus there are no proofs about it. In principle it should however be possible to turn everything into "proper" Coq functions with some work and then prove the properties postulated in MetaCoq here.