V5002 refinement_checked_at_runtime (retired)
Retired (design §17.87, §12.3): never reported.
An error from the contract phase. sakura explain V5002 prints this explanation offline.
Retired (design §17.87, §12.3): never reported. It warned that a literal into a refined type
was checked at start-up. The predicate is now evaluated on the literal at compile time: a
literal that satisfies it compiles silently, one that cannot is V5004, and one the compiler
cannot decide is checked once through T.from when the module is initialised (D010 before
main), with no diagnostic; sakura audit lists it. See sakura explain V5004.
Retired codes are never reported, so no program triggers this one.
V5001 impure_contract
Predicates in where, requires, ensures and property bodies must be pure, terminating and deterministic: no loops, no recursion, and calls only to @total functions in the contract subset (design §7.1).
V5003 validate_target_not_refined
Untrusted.validate(u) takes its target V from the expected type Result<V, Violation>.