Summary

vera verify generates no call-site precondition obligation at all when the called function's requires() constrains ADT-typed parameters — no obligation record, no E501, no Tier-3 demotion warning. The identical program with Int parameters correctly produces a call_pre obligation (E501 violated). Enforcement is runtime-only: vera run traps with a precondition violation, so this is not a false Tier-1 — it is a silent static-coverage gap: verify reports ok: true with a clean summary for a call it never statically examined, in exactly the class (structural ADT equality in requires) where #871 showed static checking matters.

Verified on main at c0af1b9; found during PR #879's model-parity panel.

Repro (verified)

private data P { MkP(Int) }

private fn g(@P, @P -> @Bool)
  requires(@P.1 == @P.0) ensures(true) effects(pure)
{
  true
}

public fn main(@Unit -> @Bool)
  requires(true) ensures(true) effects(pure)
{
  g(MkP(1), MkP(2))
}

• vera verify --json → ok: true, {'tier1_verified': 4, 'tier3_runtime': 0, 'total': 4} — no call_pre obligation for the g call site, no diagnostic, no warning.
• Control with g(@Int, @Int -> @Bool) / g(1, 2) → ok: false, [E501] (call-site precondition violated) — same obligation machinery, so the walker demonstrably skips only the ADT-typed case.
• vera run → exit 1, precondition violation at runtime (loud, correct).

Expected

Per DESIGN.md (maximise static guarantees; degrade loudly): the call site should generate a call_pre obligation. With #879 merged, ADT equality over concrete fields is statically modellable (per-field, fpEQ for floats), so the obligation should discharge or produce a counterexample (MkP(1) vs MkP(2) is statically refutable). Where the argument expression genuinely can't be modelled, the obligation must demote to a loud Tier-3 (E522), never silently not exist — the verify summary currently overstates coverage.

Pointers

• The call-site precondition walker in vera/verifier.py (wherever call_pre obligations are built) — it evidently bails on ADT-typed argument translation before recording an obligation.
• Interaction: if-path narrowing on FP-ADT equality IS correctly routed post-fix(verifier): ADT equality over Float64 fields models per-field fpEQ, not structural datatype = (#871) #879, so the equality modelling exists; only the call-site obligation construction skips ADTs.