Combinators are not collected from a struct `inv`, so they do not resolve there

[maxinelevesque]

---

A struct invariant naming a combinator fails to resolve, because the walk that
decides which combinator definitions to emit has no arm for an ADT.

Reproduction

struct S { xs: Vec<u32> } inv forall_in(xs, |x| x < 100)

level: L0
error[E0425]: cannot find function `forall_in` in this scope

A struct invariant can call a user spec fn — that certifies at L3.
Combinators are spec functions, and nothing semantic distinguishes them here.

Mechanism

Combinator definitions are emitted on demand, from a walk collecting the names a
program references. The driver (thermite-lower/src/lower.rs:1783) has an arm
for a function's req and ens, an arm for its body's loop clauses, and an arm
for a spec fn's dec and body:

collect_combinators_in_expr(&f.contract.req.expr, f.span, &mut names);
collect_combinators_in_expr(&ens.expr, f.span, &mut names);
collect_combinators_in_block_specs(body, f.span, &mut names);
collect_combinators_in_expr(&s.dec.expr, s.span, &mut names);
collect_combinators_in_block_specs(&s.body, s.span, &mut names);

There is no arm for a struct or enum inv. A combinator named there is never
collected, so its definition is never emitted, so the reference does not resolve.

Suggested fix

An arm walking the inv expression of Item::Struct and Item::Enum.

Not the same defect as #122

Worth saying, because they look alike and I initially assumed they were one. Both
are the ADT path failing to gather something it needs, and they are different
code with different fixes:

#122	item_subprogram's ADT arm not weaving a declaration, in forge/src/check.rs
this	the combinator collection walk in thermite-lower having no ADT arm

Environment

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