Summary
A @Nat tuple-component binding at CONSTRUCTION is recorded by the verifier as verified (Tier 1, zero diagnostics) while the compiled program traps at runtime for a negative input — a proved obligation whose guard fires, the #392-class false-Tier-1 signature.
Repro (measured on the v0.1.12 release branch during PR #1330's review round)
public fn f(@Int -> @Int)
requires(true) ensures(true) effects(pure)
{
let @Tuple<Nat, Int> = Tuple(@Int.0, 5);
match @Tuple<Nat, Int>.0 { Tuple(@Nat, @Int) -> nat_to_int(@Nat.0) }
}
vera verify --json: the construction's nat_bind obligation is verified, no diagnostics.vera run --fn f -- 7 → 7; vera run --fn f -- -1 → trap at the destructure guard.- Control: the identical construction in return position correctly reports
violated/E503.
A Tier-1 verified on this obligation asserts the negative can never reach the component; the trap proves it can. (Distinct from the E504 disclosure gap the same probe documented — #1331's sibling spec/06 correction and the four-site KNOWN_ISSUES #754 row — which concerns unguarded sites; this one is a site the verifier claims to have PROVED.)
Suspected shape
The construction-site nat_bind walk appears to prove against the wrong environment or the wrong value (the let-bound tuple's component vs the argument's sign), where the return-position walk gets it right. Needs the ensures+run differential treatment per the soundness-probing rule (TESTING.md): the distinguishing test is verify-says-proved + run-traps on the same program.
Found by the release PR's full-cycle review round (PR #1330). Carried to the v0.1.13 queue; soundness-class, should lead it.
Summary
A
@Nattuple-component binding at CONSTRUCTION is recorded by the verifier asverified(Tier 1, zero diagnostics) while the compiled program traps at runtime for a negative input — a proved obligation whose guard fires, the #392-class false-Tier-1 signature.Repro (measured on the v0.1.12 release branch during PR #1330's review round)
vera verify --json: the construction'snat_bindobligation isverified, no diagnostics.vera run --fn f -- 7→7;vera run --fn f -- -1→ trap at the destructure guard.violated/E503.A Tier-1
verifiedon this obligation asserts the negative can never reach the component; the trap proves it can. (Distinct from the E504 disclosure gap the same probe documented — #1331's sibling spec/06 correction and the four-site KNOWN_ISSUES #754 row — which concerns unguarded sites; this one is a site the verifier claims to have PROVED.)Suspected shape
The construction-site
nat_bindwalk appears to prove against the wrong environment or the wrong value (the let-bound tuple's component vs the argument's sign), where the return-position walk gets it right. Needs the ensures+run differential treatment per the soundness-probing rule (TESTING.md): the distinguishing test is verify-says-proved + run-traps on the same program.Found by the release PR's full-cycle review round (PR #1330). Carried to the v0.1.13 queue; soundness-class, should lead it.