Summary
#746 added static verification of refinement-type predicates: a value narrowing into a refined slot (let, call argument, constructor field, effect-op argument, match binding, tuple-destructure component) or returned at a refined return position carries a Tier-1 proof obligation that the predicate holds. A provably-violating narrowing is an E505 error; an untranslatable one is an E506 Tier-3 warning.
What #746 did not add is a runtime guard for arbitrary refinement predicates. Unlike the built-in @Nat narrowing — whose codegen emits an i64.lt_s trap at concrete binding sites (#754/#757) — a general refinement predicate that falls to Tier 3 (untranslatable predicate, non-primitive base such as { @Array<Int> | array_length(...) > 0 }, or solver timeout) is neither statically proved nor runtime-checked. The same exposure exists at a public/FFI boundary, where an untrusted caller supplies the refined value.
This is the refinement-predicate analogue of the @Nat runtime-guard residual tracked in #754/#757.
Scope
Emit a runtime guard for a refinement narrowing the verifier could not discharge statically, so that an unverified vera compile / vera run traps instead of silently storing a predicate-violating value. Two candidate mechanisms:
- Predicate → WAT lowering — compile the refinement predicate to a Wasm boolean expression and trap when it is false (works for predicates in the decidable fragment but currently untranslatable to Z3, e.g. some array/string shapes).
- Contract-fail host channel — route a failed refinement check through the existing contract-failure host import so the runtime reports a structured diagnostic rather than a bare
unreachable.
Acceptance
Notes
No statically-verified program is weakened by the current state — this only bounds the Tier-3 runtime fallback. Documented as a limitation in KNOWN_ISSUES.md, SKILL.md, vera/README.md, and spec/02-types.md §2.6.4.
Follow-up to #746.
Summary
#746 added static verification of refinement-type predicates: a value narrowing into a refined slot (
let, call argument, constructor field, effect-op argument, match binding, tuple-destructure component) or returned at a refined return position carries a Tier-1 proof obligation that the predicate holds. A provably-violating narrowing is anE505error; an untranslatable one is anE506Tier-3 warning.What #746 did not add is a runtime guard for arbitrary refinement predicates. Unlike the built-in
@Natnarrowing — whose codegen emits ani64.lt_strap at concrete binding sites (#754/#757) — a general refinement predicate that falls to Tier 3 (untranslatable predicate, non-primitive base such as{ @Array<Int> | array_length(...) > 0 }, or solver timeout) is neither statically proved nor runtime-checked. The same exposure exists at apublic/FFI boundary, where an untrusted caller supplies the refined value.This is the refinement-predicate analogue of the
@Natruntime-guard residual tracked in #754/#757.Scope
Emit a runtime guard for a refinement narrowing the verifier could not discharge statically, so that an unverified
vera compile/vera runtraps instead of silently storing a predicate-violating value. Two candidate mechanisms:unreachable.Acceptance
unreachable.KNOWN_ISSUES.mdlimitation row added by Implement refinement-type predicate verification #746 is updated/removed as coverage lands.Notes
No statically-verified program is weakened by the current state — this only bounds the Tier-3 runtime fallback. Documented as a limitation in
KNOWN_ISSUES.md,SKILL.md,vera/README.md, andspec/02-types.md§2.6.4.Follow-up to #746.