v0.0.174

Verification of refinement-type predicates — static and runtime (#746)

A user refinement type { @T | P } (e.g. type PosInt = { @Int | @Int.0 > 0 }) previously parsed but its predicate was never checked — a violating value verified silently (a Tier-0 silent failure). This release makes refinement predicates real, both at verify time and at run time.

Static verification (the verifier)

The predicate is discharged as a Tier-1 obligation at every site where a value narrows into a refined slot, and at a refined return position:

• let bindings, call arguments (incl. piped and generic-instantiated formals), constructor fields, effect-operation arguments, match bindings, ADT sub-pattern binds
• tuple construction components (recovered from the construction site's expected type — Tuple is not a user-registered constructor, so it is obligated separately from ADT fields)
• literal / projected tuple-destructure components

A refined parameter is dually assumed to satisfy its predicate in the body (sound precisely because every call site discharges the obligation). A provably-violating narrowing is an E505 error with a counterexample; a refinement over a non-primitive base ({ @Array<Int> | array_length(...) > 0 }) or an undecidable predicate is an E506 Tier-3 warning — never a silent pass. This generalises the @Nat >= 0 machinery to an arbitrary translated predicate (the forward-promise in the 0.0.172 notes).

Runtime guard (#762)

Codegen compiles the predicate to WebAssembly and checks it at every function boundary — a refined parameter at entry, a refined return at exit (via $vera.contract_fail) — so even a program compiled without vera verify traps on a violating value, including at a public/FFI entry point an untrusted caller can't bypass (call arguments are covered transitively).

• Collection bases ({ @Array<Int> | array_length(...) > 0 }) are Tier-3 statically but lowered directly by codegen, so an empty array into a @NonEmptyArray parameter traps.
• A tuple with refined / @Nat components (Tuple<PosInt, Int>) carries no top-level refinement, so codegen decomposes it at the boundary — loading and guarding each component (recursively, for nested tuples) at both entry and exit. An external caller passing Tuple(-5, 3) traps on the violating component.
• A predicate codegen can't lower to a guard (e.g. one calling a generic function with no monomorphised instance at the guard site) now reports a clean E617 diagnostic rather than crashing the compiler.

Review hardening

A long tail of soundness and completeness fixes from the PR review. In every case a genuine narrowing stays obligated — source-type facts never launder an unproven value into a false Tier-1:

• Generic tuple aliases (type Box<T> = Tuple<T, Int>) substitute their type argument when resolving component types, so Box<PosInt> still guards its refined component.
• A mutually-recursive (infinite) tuple alias fails closed with E617 rather than silently emitting partial guards.
• Nested RefinedType components unwrap to their base Z3 sort, so Tuple<PosInt, Int> gets a proper datatype sort rather than degrading to a scalar model.
• Refinement over a tuple (type Pair = { @Tuple<PosInt, Int> | true }) unwraps the refined base so components are obligated statically and guarded at the boundary (recursively through Tuple<Pair, Int>), with component guards emitted before the enclosing top-level predicate.
• Refined-ADT sub-pattern binds (Some(@PosInt) on Option<PosInt>) carry the field's source-type predicate into the arm body — both to the narrowing walk (fixing a false E503) and, via an SMT match-translation hook, to the arm body's call preconditions (fixing a false E501).
• A refined value returned from a match arm (Some(@PosInt) -> @PosInt.0) discharges its refined-return goal via a global arm-matched ⇒ source-fact SMT implication — on the generic fast path too.
• A callee's alias-base refined return ({ @Age | @Age.0 >= 18 }, type Age = Nat) is assumed by the caller through the predicate's binder name (@Age.0), not the resolved Nat.
• Nested constructor sub-pattern narrowings (Some(Some(@PosInt)) on Option<Option<Int>>) are recursed and obligated statically — previously an unguarded false Tier-1 — with the nested-bind runtime guard tracked as #765.
• Refined ADT scrutinees (match on { @Option<Int> | P }) and refined tuple sources (a let-destructure of { @Tuple<PosInt, Int> | P }) unwrap the refined base before reading the constructor's / tuple's type args.

---

Internal: hardened the @Nat narrowing guard data structures (#759)

Single-sourced the checker→verifier side-table span key through ast.span_key (previously hand-rolled at three sites), and added a ConstructorLayout.__post_init__ assertion that nat_fields stays length-aligned with field_offsets, so a drifted built-in literal fails loudly at construction rather than as a silently mis-indexed guard. Also pinned the #757 generic-instantiated-constructor-field runtime deferral with a codegen test (#760). No behaviour change — internal robustness follow-ups from the #756 review.