A `spec fn` over an ADT has its declared `bool` return rewritten to `nat`

[maxinelevesque]

---

A spec fn whose body matches over an ADT and calls through a Box deref is
lowered with a nat return regardless of what its signature declares.

Reproduction

enum Tree { Leaf(u64), Node(Box<Tree>, Box<Tree>) }

spec fn all_below(t: Tree, limit: u64) -> bool
  dec t
{ match t { Leaf(v) => v < limit, Node(l, r) => all_below(*l, limit) && all_below(*r, limit) } }

error[E0308]: mismatched types
10 | pub open spec fn all_below(t: Tree, limit: u64) -> nat
   |                                                    --- expected `nat` because of return type
14 |     Tree::Leaf(v) => v < limit,

It is not about recursion, and not about the measure

This is the part I'd have got wrong without checking. A non-recursive
function reproduces it:

spec fn depth(t: Tree) -> u64
  dec t
{ match t { Tree::Leaf(v) => 1, Tree::Node(l, r) => 1 + depth(*l) } }

spec fn calls_it(t: Tree) -> bool          // calls itself nowhere
  dec t
{ match t { Tree::Leaf(v) => true, Tree::Node(l, r) => depth(*l) > 0 } }

20 | pub open spec fn calls_it(t: Tree) -> nat
24 |             Tree::Leaf(v) => true,

depth certifies at L3. calls_it does not.

Mechanism

is_adt_fold_sum (thermite-lower/src/lower.rs:4078) classifies a body as a
numeric fold when its tail is a Match and any arm contains a call with a
deref argument — f(*x) — via expr_has_deref_call_arg (:4096). A body so
classified joins the program-wide nat_fns set (:891) and is lowered with a
nat return.

The declared return type is not consulted anywhere on that path.

The classifier is right for what it was built for. Its own comment says the base
arms "are coerced to nat uniformly with the recursive arm by the nat return",
which is what sum_list needs. It fires on any ADT match that calls through a
Box deref, whatever the signature says.

Suggested fix

Gate the classification on the declared return type — a spec fn declared
-> bool does not join nat_fns. The guard fits at the filter_map building
that set, where the item is in hand.

Why this one is worth doing first

Structural induction yielding a predicate is how you state a property of a tree.
A page table is a four-level tree, and "this table maps no address outside the
partition" is the property memory isolation rests on. With this, a kernel can
validate an address space it was handed; without it, only build one itself.

Environment

Thermite 84d276e76ed02509ea58812efc15861d58580a42, Verus
0.2026.05.24.ecee80a. Found while designing a verified kernel against the pin
(bulla-systems/bulla).