Summary

User refinement-type predicates (e.g. type PosInt = { @Int | @Int.0 > 0 }) are not verified anywhere in the compiler. RefinedType (vera/types.py:53) preserves the predicate as an opaque AST node ("kept opaque — not verified in C3"), and the verifier strips RefinedType to its base at every site (vera/smt.py:1102), discarding the predicate. A value violating a refinement predicate is accepted silently — tests/conformance/ch02_refinement_types.vera exercises parsing/aliasing, not enforcement.

@Nat is a distinct primitive with a hardcoded >= 0 invariant (declare_nat), not a RefinedType, so #552's binding-site obligation does not generalise to arbitrary predicates.

Scope

Implement refinement-predicate verification end to end:

• Translate a RefinedType predicate to Z3, substituting the refinement's binder variable with the value being refined (a substitute_predicate(pred, value) -> z3.BoolRef helper).
• Discharge the predicate as a proof obligation at every site that introduces a refined value: function parameters, return positions, let bindings, constructor fields, and @Int-into-refinement narrowing (the refinement analogue of Generalize @Nat invariant check to all binding sites (broader generalisation of #520) #552).
• Emit a runtime guard fallback where Z3 cannot discharge statically, and a diagnostic with a counterexample on violation.
• Conformance + unit tests asserting both discharge and violation.

Context

Surfaced while scoping #552 (@nat binding-site narrowing). #552 was deliberately scoped to the built-in @Nat >= 0 invariant; general refinement-predicate verification is this separate, larger piece (the C4 milestone).