A struct with a field of user-declared type never certifies

[maxinelevesque]

A struct with a field of user-declared type never certifies

Found while porting a kernel subsystem: every struct in the port has a field whose type is another struct or enum, and none of them certify.

Reproduction

Three lines, no contracts involved:

struct Regs  { ip: u64 }
struct Frame { regs: Regs, generation: u64 }

error[E0425]: cannot find type `Regs` in this scope
 --> /tmp/forge_Frame_check_.../Frame_check.rs:5:15
  |
5 |     pub regs: Regs,
  |               ^^^^ not found in this scope

project assurance: FAILED. The same happens when the field type is a user-declared enum:

enum Privilege { Kernel, User }
struct Frame { privilege: Privilege, generation: u64 }   // same E0425

A struct whose fields are all primitives certifies at L3, so the fault is specific to user-declared field types. Note also that the containing function's own obligations still discharge — it is the struct's own harness that fails, and that fails the project.

Cause

The transitive ADT-weaving from #68 is present and does handle this shape. reachable_adt_deps seeds a worklist from the referrers and then runs a fixed point that follows struct fields into further ADTs through collect_decl_field_adt_refs, which has a correct Item::Struct arm walking s.fields.

The gap is in seeding. forge/src/check.rs:5453, in collect_item_adt_refs:

// A struct/enum decl's own field types are followed by the type-graph
// fixed point (`collect_decl_field_adt_refs`), not here.
Item::Struct(_) | Item::Enum(_) | Item::Forge(_) => {}

When the checked item is a fn, the Item::Fn arm seeds names from its signature, contract and body, and the fixed point then closes over the type graph. When the checked item is itself a struct, it is the sole referrer, this arm collects nothing, names starts empty, and reachable_adt_deps returns before the fixed point runs. The harness is emitted with no declaration for Regs.

The comment is accurate for a struct reached as a dependency of a fn, where the fixed point does the walking. It does not hold for a struct that is the root of the referrer set.

That also explains the shape of the symptom: a fn referencing an ADT works, a primitive-only struct works, and only a struct-as-checked-item with user-declared field types fails.

Why it survived

No .th in conformance/ has a struct with a user-declared field type. A scan of the corpus for struct X { f: Y } where Y is declared in the same file returns nothing, so the case is unreached by the suite. REQ-LOWER-ADT-STRUCT and REQ-LOWER-L1-STRUCT-INVARIANTS both exist and neither covers it.

Suggested shape

Seed the checked item's own field types when it is an ADT decl — delegating that arm to collect_decl_field_adt_refs would do it — and add a conformance case with a struct-typed field and an enum-typed field so the corpus reaches it.

Adjacent, smaller: inv loses its receiver for is

Same area, separate code path. A struct invariant written with the variant-test operator does not bind:

enum Privilege { Kernel, User }
struct Frame { privilege: Privilege } inv privilege is User

error[E0425]: cannot find value `privilege` in this scope
  |     (privilege is User)
  |      help: you might have meant to use the available field: `self.privilege`

Writing the same invariant as inv privilege == Privilege::User binds correctly, so this is confined to is in an inv clause. b8dc394 ("Bind struct invariant fields through unary operators") addressed the neighbouring case, which suggests the binding pass enumerates expression forms and is was missed.

Scope

Small, and it is a missing dependency in harness construction rather than a semantics question. It currently blocks any port that models state as nested records, which for a kernel is most of them.

🤖 Generated with Claude Code

[maxinelevesque]

Evidence that this is a design constraint rather than a papercut, from a direction that surprised me.

We hit this within hours of attempting a port — a 194-line Rust file with Registers, Privilege and TrapOrigin as field types. So I went looking at how a larger Thermite codebase handles it, expecting to find a workaround worth copying.

Surveying Thermite-Microkernel's 2,649 lines of .th:

• 9 structs, and none has a field of user-declared type
• 12 enums, all payload-carrying
• AddressPlanState is thirteen fields of u32 / u64 / bool

I can't tell from outside whether that reflects a deliberate workaround or is simply how those subsystems came out, and I'm not claiming either. What's observable is the shape: a substantial, working Thermite codebase has a data model that sits entirely inside what this bug permits. Composition happens only in enum payloads, never in struct fields.

The consequence shows up in the contracts. Postconditions carry clauses like:

kind >= 1 && kind <= 6

That's a numeric encoding of what would otherwise be an enum variant, with a range check standing in where a type would do the work. It's a perfectly reasonable thing to write when composition isn't available — but it moves an invariant that could be structural into something that has to be restated and re-proved at every use.

So the finding isn't about anyone's code. It's that G4 is already shaping how Thermite gets written, quietly, before anyone hits an error message — flat records with primitive fields are what you converge on, and that's a narrower design space than the language otherwise offers.

Which also explains our own experience: we didn't hit G4, G4b and G5 through bad luck. We hit them because we ported code shaped for Rust rather than designing shapes for Thermite. Anything that models state as composed records will meet this immediately.

Fixing it widens the expressible design space rather than just clearing an error, and it's the difference between "invariants live in types" and "invariants live in postcondition range-checks."