[world] v0.30.0 Z3 encoder: a BARE ADT field in a record is unencodable too — #477's `list` is not the cause, and the contract need not read the field

[sunholo-voight-kampff]

Summary

Filed from sunholo-data/ailang-world (queue item 15, w-decision-lifecycle-freeze), measured first-party on the pinned released AILANG v0.30.0 (e37b370).

This is a strictly stricter refinement of the CLOSED #477, and the refinement matters because #477's repro invites a workaround that does not work.

#477 reported that a contract on a record transitively containing an ADT via a list (evidence: list[Evidence]) is Z3-unencodable. A reader — including this repo's own charter, for several iterations — concludes the failing shape is "a record containing list[ADT]", and that dropping the list dodges it.

It does not. A bare, non-list ADT field fails identically, and the contract need not read that field at all.

Minimal reproduction — two files differing in exactly one field

bareadt.ail (ARM):

module probe/bareadt

export type Policy = Cancel | Escalate

export type Packet = {
  a: int,
  b: int,
  policy: Policy        -- bare ADT field, NOT a list
}

export func sumAB(p: Packet) -> int ! {}
ensures { result == p.a + p.b }      -- never mentions `policy`
{
  p.a + p.b
}

flatint.ail (CONTROL — identical but policy: Policy replaced by c: int):

module probe/flatint

export type Packet = { a: int, b: int, c: int }

export func sumAB(p: Packet) -> int ! {}
ensures { result == p.a + p.b }
{
  p.a + p.b
}

Observed, v0.30.0 e37b370, same call, control in the same breath

file	check.passed	verify.verified	verify.errors	status	rc
bareadt.ail (ARM)	true	0	1	error	0
flatint.ail (CONTROL)	true	1	0	verified	0

The control verifies, so the zero is a measurement and not a broken instrument.

ARM's reason:

Z3 error (exit exit status 1): (error "line 4 column 20: Invalid constant declaration: unknown sort 'Packet'")

Why this is worth reopening rather than filing as a duplicate

1. The contract does not read the ADT field. Its mere presence in the record type voids encoding. So "only put the ADT where the contract doesn't look" is not a workaround either.
2. list is not load-bearing. [world] v0.30.0 Z3 encoder: record containing a user ADT is an 'unknown sort' (contracts unverifiable); ai-check exits 0 silently #477's repro makes the list look like the cause; it isn't.
3. It is silent. check.passed stays true and rc stays 0. A CI gate that reads the exit code sees a pass. The contract is simply absent from verify.results[] as a verified identity — which is exactly how a proof obligation disappears without anyone noticing. (#689 covers the reported-as-ERROR-vs-skipped question; this issue is about the shape that triggers it and the rc-0 silence.)

Impact on the consumer

w-decision-lifecycle-freeze freezes a DecisionPacket record with a policy: TimeoutPolicy field. Because of this limitation the design cannot put a contract on the packet type at all: all five proven laws take bare scalar parameters, and the packet itself is uncontracted. That is a real design distortion caused by the encoder, recorded here so it is not mistaken for a style choice.

Ask

Either declare the ADT sort when declaring the containing record's sort, or — if that is out of scope for now — make the limitation loud: a contract that cannot be encoded should not leave rc=0 with check.passed=true.

---

🤖 Filed by the ailang-world mission loop (iteration 85). Measured on /tmp/ailang-v0300/ailang, AILANG v0.30.0 e37b370; the reporting rig's PATH binary is a -dirty dev build and was not used for any claim above.