Summary

Two related accuracy issues in spec/06-contracts.md at v0.0.127:

1. forall(...) in contracts is documented as Tier-1-decidable in §6.3.3 but actually falls to Tier 3 at runtime, contradicting §6.3.2 and §6.8 which both flag quantifiers as Tier 2 NYI.
2. Calls to pure functions in ensures are listed as Tier 2 NYI in §6.3.2 and §6.8 but actually verify Tier 1 in v0.0.127 — the spec is behind the implementation here.

Both observations are derived from minimal repros below. Each is a one-line spec edit, but the current state misleads agents reading the spec as authoritative for "what verifies and what doesn't."

Issue 1 — forall is Tier 3, not Tier 1

spec/06-contracts.md §6.3.3:

Bounded quantification is decidable for finite bounds and is handled by Z3 via finite unrolling for small bounds or inductive reasoning for symbolic bounds.

That phrasing reads as "this is in the decidable fragment" — i.e. Tier 1. But §6.3.2 lists "Quantified expressions" under "Additionally Allowed in Contracts (Tier 2)" with the Status: Not yet implemented banner. §6.8's tier table also lists quantifiers under Tier 2.

Repro:

public fn check(@Array<Int> -> @Bool)
  requires(true)
  ensures(@Bool.result ==> forall(@Nat, array_length(@Array<Int>.0), fn(@Nat -> @Bool) effects(pure) {
    @Array<Int>.0[@Nat.0] > 0
  }))
  effects(pure)
{
  false
}

$ vera verify repro.vera

  Postcondition in 'check' uses constructs outside the decidable fragment.
  Contract will be checked at runtime.

OK: repro.vera
Verification: 1 verified (Tier 1), 1 runtime checks (Tier 3)

So the implementation matches §6.3.2/§6.8 (Tier 2 NYI → Tier 3), and §6.3.3's "decidable for finite bounds" is misleading.

Suggested fix: in §6.3.3, replace "is decidable for finite bounds and is handled by Z3 …" with something like:

When fully implemented (Tier 2, #427), bounded quantification will be decidable for finite bounds via Z3 finite unrolling. At v0.0.127 quantifiers fall to Tier 3 (runtime check) — they are syntactically accepted but not statically verified.

This aligns §6.3.3 with §6.3.2 and §6.8 and stops promising verification capability that isn't there yet.

Issue 2 — Pure fn calls in ensures already work, contrary to spec

spec/06-contracts.md §6.3.2 lists "Calls to pure functions that have their own contracts" under the Tier 2 NYI banner. §6.8's tier-summary table also says "function calls" in contracts are Tier 2.

Repro:

private fn double(@Int -> @Int)
  requires(true)
  ensures(@Int.result == @Int.0 * 2)
  effects(pure)
{
  @Int.0 * 2
}

public fn quad(@Int -> @Int)
  requires(true)
  ensures(@Int.result == double(@Int.0) * 2)
  effects(pure)
{
  @Int.0 * 4
}

$ vera verify repro.vera
OK: repro.vera
Verification: 4 verified (Tier 1)

Z3 verifies quad's postcondition statically, using double's ensures-clause as an axiom at the call site (modular VC, exactly as §6.4.2 describes). This is full Tier 1 — no runtime check, no warning.

So §6.3.2's claim that pure-fn calls in contracts are NYI is wrong: simple modular call-site reasoning has been working all along. What §6.3.2 probably means to gate behind Tier 2 is the more aggressive case where Z3 needs to inline or reason inside a function body (not just assume its postcondition) — but that distinction isn't currently visible to a reader.

Suggested fix: in §6.3.2, either remove "Calls to pure functions that have their own contracts" from the Tier-2-NYI list, or split it: "Calls to pure functions where the postcondition alone is sufficient" → already works (Tier 1, modular); "Reasoning into the body of a called function" → Tier 2 NYI. The §6.8 table needs the matching update.

Why it matters

An agent reading spec/06-contracts.md and §6.8 will believe:

• forall over array contents is verifiable statically → writes contracts assuming Tier 1, ships code with silent Tier 3 fallback.
• Calls to pure functions in ensures are Tier 3 → falls back to weaker contracts, misses real Tier 1 capability.

Both errors are pure documentation. The fix is a small edit to §6.3.2, §6.3.3, and the §6.8 tier table. No code change needed.

Environment

• Vera v0.0.127 (editable install from aallan/vera@main)
• Python 3.14.3, macOS 25.4 (arm64)