v0.0.177

Primitive-operation safety obligations (#680). Closes the last item in the Tier-0 "silent failures" line: the verifier now auto-synthesises a proof obligation at every integer division / modulo (E526) and array index (E527) — proved at Tier 1 where decidable, a loud compile error where provably unsafe, else honestly runtime-guarded at Tier 3 — so vera verify no longer reports a division or index as proven safe and then traps at runtime.

Added

• Auto-synthesised safety obligations for trapping primitive operations (#680). The verifier now emits a Tier-1 proof obligation at every integer division and modulo (b != 0, E526) and every array index (0 <= i < array_length(arr), E527), discharged from preconditions and path conditions exactly like @Nat subtraction underflow (E502) and @Int → @Nat narrowing (E503) — closing the last item in the Tier-0 "silent failures" roadmap section, where vera verify reported a division or index as proven safe and it then trapped at runtime. Division and modulo are Tier-1-decidable: an unguarded divisor with a zero counterexample is now a compile error (a genuinely undecidable divisor would fall to Tier 3, but integer division is decidable; float division is exempt — f64.div by zero yields inf/NaN, not a trap). Array bounds depend on the uninterpreted array_length, so the obligation is tiered honestly — proved at Tier 1 where a literal length, refinement, precondition, or path condition pins it; a compile error (E527) where the index provably exceeds a statically-known length (e.g. [1, 2, 3][5]); otherwise a runtime-guarded Tier 3, counted in vera verify --json rather than silently passed. Lifting dynamic or closure-captured array bounds to a Tier-1 proof is part of the Tier 2 work (#427). The @Nat subtraction walker generalises to a single _walk_for_primitive_op_obligations pass over operand-trapping sites — direct positions, array-literal elements, assert conditions, interpolated-string parts, let-destructure values, and the standard call / control-flow positions (an op inside a closure / quantifier / handler body stays runtime-guarded, tracked in #779); codegen is unchanged — the divide_by_zero / out_of_bounds runtime traps already existed.

Changed

• spec §6.4.3 "Primitive Operation Safety" rewritten to state that division, modulo, and array-index obligations are now auto-synthesised (previously documented as not synthesised and tracked in #680); README and FAQ updated to match. With this, the ROADMAP Tier 0 — Close the silent failures section is done: every known case where vera verify accepted a program that then did something weaker than promised is closed.