Summary
The refined-predicate narrowing dual of #1017 at the apply_fn argument boundary. #1017 added the @Int -> @Nat narrowing obligation + guard, which covers the >= 0 base invariant of a refinement-over-@Nat formal. But the full refinement predicate (e.g. > 0) is still not checked at apply_fn: passing a value that satisfies >= 0 yet violates the predicate verifies clean and runs without trapping.
The generic call-argument path obligates this via _refined_binding_target + _check_refined_binding_obligation (verifier) and the corresponding runtime refinement guard (codegen); the apply_fn branch has neither refined arm — only the @Nat (#1017) and @Nat -> @Int widening (#820) arms.
Reproduction
type Pos = { @Nat | @Nat.0 > 0 };
type PosToInt = fn(Pos -> Int) effects(pure);
private fn f(@PosToInt -> @Int) requires(true) ensures(true) effects(pure)
{ apply_fn(@PosToInt.0, 0) }
vera verify — clean (2 verified, Tier 1). Should reject: 0 narrows into { @Nat | @Nat.0 > 0 } but 0 > 0 is false. A named-call take(0) with the same @Pos formal correctly reports the refinement violation (Value narrowing into a refined call argument … may violate the refinement predicate @Nat.0 >= 0 && @Nat.0 > 0).
At runtime, apply_fn(clo_pos_formal, 0) returns the closure body value silently rather than trapping — the #1017 nat guard's >= 0 passes 0, and the strict > 0 is unguarded.
Root cause (located)
Provenance
Found during the #1017 completeness sweep (the refined dual of the @Nat narrowing). #1017 covers the >= 0 base — a negative value now correctly traps (run(-5)); this issue is the residual strict-predicate gap (run(0) on > 0). Grouped with the refined-binding family (#746) and the apply_fn narrowing family (#1017 / #820).
Summary
The refined-predicate narrowing dual of #1017 at the
apply_fnargument boundary. #1017 added the@Int -> @Natnarrowing obligation + guard, which covers the>= 0base invariant of a refinement-over-@Natformal. But the full refinement predicate (e.g.> 0) is still not checked atapply_fn: passing a value that satisfies>= 0yet violates the predicate verifies clean and runs without trapping.The generic call-argument path obligates this via
_refined_binding_target+_check_refined_binding_obligation(verifier) and the corresponding runtime refinement guard (codegen); theapply_fnbranch has neither refined arm — only the@Nat(#1017) and@Nat -> @Intwidening (#820) arms.Reproduction
vera verify— clean (2 verified, Tier 1). Should reject:0narrows into{ @Nat | @Nat.0 > 0 }but0 > 0is false. A named-calltake(0)with the same@Posformal correctly reports the refinement violation (Value narrowing into a refined call argument … may violate the refinement predicate @Nat.0 >= 0 && @Nat.0 > 0).At runtime,
apply_fn(clo_pos_formal, 0)returns the closure body value silently rather than trapping — the #1017 nat guard's>= 0passes0, and the strict> 0is unguarded.Root cause (located)
vera/verifier.pyapply_fnbranch (~L3218): has the@Natnarrowing arm (Verifier: @Int->@Nat narrowing into an apply_fn closure formal is not obligated (false Tier-1) #1017) and the@Nat -> @Intwidening arm (@Nat → @Int widening: remaining deferred coercion sites (follow-up to #813) #820) but not the refined-first arm the generic call-arg path carries (_refined_binding_target(arg, formal)+_narrows_into_refined->_check_refined_binding_obligation).vera/wasm/closures.py_translate_apply_fn: emits the@Natnarrowing guard (Verifier: @Int->@Nat narrowing into an apply_fn closure formal is not obligated (false Tier-1) #1017) and the widen guard (@Nat → @Int widening: remaining deferred coercion sites (follow-up to #813) #820) but not the refinement-predicate guard.Provenance
Found during the #1017 completeness sweep (the refined dual of the
@Natnarrowing). #1017 covers the>= 0base — a negative value now correctly traps (run(-5)); this issue is the residual strict-predicate gap (run(0)on> 0). Grouped with the refined-binding family (#746) and the apply_fn narrowing family (#1017 / #820).