Summary
A refinement whose base carries a non-plain type argument — { @Array<{ @Int | @Int.0 > 0 }> | array_length(...) > 0 }, or an Array<fn(...)> base — gets no runtime guard at any boundary: _refinement_guard_parts (vera/codegen/contracts.py) returns None when a base type-arg is not a plain NamedType (the binder slot name cannot be spelt), so _emit_refinement_check never fires. This affects named-function parameters and returns and (since #1034) closure formals and returns identically — the predicate is simply unchecked at run time for these bases.
Found by PR #1034's adversarial review (repro battery under the reviewer's scratch dir; the shape apply_fn an empty array through a NonEmpty-style refined boundary returns silently).
Current state (post-#1034)
The verifier now discloses the gap honestly: _refined_boundary_codegen_guardable mirrors codegen's bail conditions, so these obligations record tier3_unguarded (E506 warning, excluded from the runtime-checked totals) instead of claiming a runtime guard that never fires — the same disclosure convention as the #754/#757 narrowing residuals. Before that alignment the stream said tier3 guarded — an unfulfilled promise on both the named path and the new closure path.
Fix direction
Teach the guard machinery to spell (or bypass) the binder for non-plain-arg bases — e.g. key the synthetic binder slot on the canonicalised base spelling the way _translate_slot_ref's truncation convention already handles nested generic names, or lower the predicate against an anonymous local without a named binder. When the guard lands, flip _refined_boundary_codegen_guardable in the same commit (it carries a KEEP IN SYNC marker) and the disclosed tier3_unguarded rows become guarded tier3 — differential-test the flip on both the named and closure paths.
Summary
A refinement whose base carries a non-plain type argument —
{ @Array<{ @Int | @Int.0 > 0 }> | array_length(...) > 0 }, or anArray<fn(...)>base — gets no runtime guard at any boundary:_refinement_guard_parts(vera/codegen/contracts.py) returnsNonewhen a base type-arg is not a plainNamedType(the binder slot name cannot be spelt), so_emit_refinement_checknever fires. This affects named-function parameters and returns and (since #1034) closure formals and returns identically — the predicate is simply unchecked at run time for these bases.Found by PR #1034's adversarial review (repro battery under the reviewer's scratch dir; the shape
apply_fnan empty array through aNonEmpty-style refined boundary returns silently).Current state (post-#1034)
The verifier now discloses the gap honestly:
_refined_boundary_codegen_guardablemirrors codegen's bail conditions, so these obligations recordtier3_unguarded(E506 warning, excluded from the runtime-checked totals) instead of claiming a runtime guard that never fires — the same disclosure convention as the #754/#757 narrowing residuals. Before that alignment the stream saidtier3guarded — an unfulfilled promise on both the named path and the new closure path.Fix direction
Teach the guard machinery to spell (or bypass) the binder for non-plain-arg bases — e.g. key the synthetic binder slot on the canonicalised base spelling the way
_translate_slot_ref's truncation convention already handles nested generic names, or lower the predicate against an anonymous local without a named binder. When the guard lands, flip_refined_boundary_codegen_guardablein the same commit (it carries a KEEP IN SYNC marker) and the disclosedtier3_unguardedrows become guardedtier3— differential-test the flip on both the named and closure paths.