The #667 issue body claimed FloatLit / IndexExpr / ArrayLit in
contract predicates were blocked by the contract grammar.
Reality-check against `vera check` showed the parser and type
checker already accept all three — only the SMT translator was
missing the cases.  Pre-fix all three returned `None` from
`vera/smt.py::translate_expr`, dropping every affected predicate
to Tier 3 (runtime check).

What ships:

**1. SMT translation cases (`vera/smt.py::translate_expr`)**

- `FloatLit` → `z3.RealVal(value)`.  Float64 already maps to
  Z3's `Real` sort (sound for relational properties; not a full
  IEEE-754 model — real arithmetic is decidable in Z3, FP isn't).
- `IndexExpr` → uninterpreted `index_<sort>(arr, i)` function
  call.  Sound (function congruence: two references to
  `arr[i]` with the same `i` produce the same value) but
  partial — the verifier can't reason about element structure
  beyond what explicit predicates assert.  Quantified
  contracts ("for all valid i, arr[i] > 0") remain Tier 2 /
  Tier 3 territory.
- `ArrayLit` → fresh `Array_<elt>` constant with
  `length(lit) == N` and per-element `index(lit, i) == elt_i`
  axioms asserted to the solver.  Element types that can't
  be sorted (e.g. function-typed) fail cleanly via None.

**2. Array-sort infrastructure (`vera/smt.py`)**

Added `_get_array_sort`, `_get_index_fn`, `declare_array_var`,
and a sibling `_index_fns` dict.  `Array<T>` parameters are
now declared as constants of uninterpreted `Array_<T>` sorts;
pre-fix they fell through to `declare_int(z3_name)` because
`Array` isn't in the SMT layer's `_adt_registry`, making
`Array<Int>` slots numerically-typed in Z3.

**3. Verifier routing (`vera/verifier.py`)**

Added `_is_array_type` (peels RefinementType, checks
`AdtType("Array", ...)`) and `_declare_array_var` (resolves
element type → Z3 sort, delegates to `smt.declare_array_var`).
Routed `Array<T>` params and return types through the new path
in `_verify_decl`.

**4. WALKER_COVERAGE checklist update (`vera/smt.py`)**

Moved FloatLit / IndexExpr / ArrayLit from the "Latent gap"
section to "Handled" with rationale strings.  Cited #427 on
the still-unsupported `ForallExpr` / `ExistsExpr` entries.

**5. Honest contract relaxations**

Closing the gap exposed two contracts the pre-fix verifier
was vacuously verifying — the untranslatable literal masked
the body's semantics, so the postcondition's negation was
unsatisfiable in the resulting incomplete model.  Two
contracts relaxed with explanatory comments:

- `examples/json.vera::main`:
  `ensures(@Int.result == 0)` → `ensures(true)`.  The static
  return value depends on the specific hardcoded JSON literal
  parsing successfully; none of `parse_current_temp` /
  `parse_average_temp` / `round1` carries a postcondition
  strong enough to let the verifier conclude
  `@Int.result == 0` statically.
- `tests/conformance/ch06_quantifiers.vera::main` and
  `::test_has_zero`: both `ensures(@Bool.result == true)`
  → `ensures(true)`.  Helpers `all_positive` / `has_zero`
  carry `ensures(true)`; the static verifier can't conclude
  the postcondition from the specific array literals.

**6. New tests (`tests/test_verifier_coverage.py::TestSmtCoverage667`)**

5 tests pinning that FloatLit / IndexExpr / ArrayLit contracts
verify at Tier 1, asserting `tier1_verified >= N` so a
regression dropping back to Tier 3 fails (Tier 3 is also
error-free).

**7. Pre-existing edge-case test updates**

Four tests used FloatLit as a sentinel for "untranslatable
expr" — swapped to UnitLit, which is still intentionally-
unsupported in the SMT translator (predicates are Bool, not
Unit).  `test_overall_tier_counts` updated: 252/26/278 →
253/25/278 (net +1 T1, -1 T3, total unchanged — one
previously-T3 example contract using a float-comparison
predicate now verifies T1).

**8. Spec update (`spec/06-contracts.md`)**

§6.3.1 "Allowed in All Contracts" now lists Float64 literals,
array index expressions, array literals, and String literals
(the last was pre-existing but undocumented).  Each new entry
cross-links to #667.

**9. ROADMAP cleanup**

Removed #667 from the Stabilisation tier (was Order 5).
Agent-integration tier renumbered 5-7 (was 6-8).

Release prep:

- Version bumped to v0.0.153 across `__init__.py`,
  `pyproject.toml`, `uv.lock`, `docs/index.html`, `README.md`.
- CHANGELOG.md v0.0.153 entry with Added + Fixed + Tests
  sections.
- HISTORY.md row added (one-line template-compliant).
- TESTING.md totals: 3,877 → 3,882 tests; per-file counts
  updated for `test_verifier.py` and `test_verifier_coverage.py`.

Validation:

- `pytest tests/ -q` → 3,854 passed, 14 skipped, 14 deselected
- `mypy vera/` → clean
- `python scripts/check_walker_coverage.py` → clean
- `python scripts/check_doc_counts.py` → consistent
- `python scripts/check_spec_examples.py` → 74 verify OK,
  1 allowlisted, 0 failed
- Doc sweep across SKILL/CLAUDE/AGENTS/README/vera/README/
  spec/docs/examples → no stale "FloatLit/IndexExpr/ArrayLit
  fall to Tier 3" claims

Closes #667

Co-Authored-By: Claude <noreply@anthropic.invalid>

Sweep flagged that `test_overall_tier_counts`'s first-line summary
still said "252 T1 / 26 T3 / 278 total (current)" while the
assertion below already enforces 253/25/278.  The trajectory log
in the docstring is correct; only the header line drifted.

One-line fix.  Not a behaviour change — only a comment.

Refs #667 #670

Co-Authored-By: Claude <noreply@anthropic.invalid>

The PR review surfaced three issues that #670's initial commits
missed:

**CR-X1** (`spec/06-contracts.md:157`) — §6.3.2 still listed
"Array element access" as Tier 2, contradicting the §6.3.1
addition in `657f5d1`.  Removed the bullet and added a clarifier
paragraph noting that array element access + array literals are
Tier 1 (with the uninterpreted-function encoding from §6.3.1),
not Tier 2; Tier 2 (#427) is reserved for predicates that need
user-provided lemmas.

**CR-X2/X4** (`vera/smt.py::_get_element_sort_for_array`) — the
reverse-lookup parsed the Z3 sort name string and looked up in
`_z3_sorts` under the unqualified element key.  Worked for
nullary ADTs by coincidence, but generic ADTs like `List<Int>`
have canonical key `"List<Int>"` (from `_adt_sort_key`) while
the Z3 sort name is `"List_Int"` (post `<`/`>` strip in
`_get_or_create_adt_sort`).  The round-trip failed, returning
None and dropping the predicate to Tier 3.

Fix: added an explicit `_array_element_sorts: dict[str, z3.SortRef]`
dict on `SmtContext`, populated whenever `_get_array_sort`
creates a new `Array_<T>` sort.  `_get_element_sort_for_array`
now does a 3-tier lookup: direct map → primitive pattern match
→ `_z3_sorts` fallback with canonical-key variants.  Storing
the association at creation time sidesteps the fragile string
round-trip.

**CR-X3/X5** (`vera/smt.py::_translate_call_with_info`) — the
call-result fresh-var declaration handled only NAT / BOOL /
AdtType, falling back to `declare_int` for String / Float64 /
Array<T>.  Callers couldn't reason about helper return values
of those types in postconditions because the result var had
the wrong Z3 sort.

Fix: added explicit branches for STRING, FLOAT64, and `AdtType
("Array", ...)` mirroring the parameter-declaration dispatch in
`vera/verifier.py::_verify_decl`.  String returns now get
`declare_string`, Float64 returns get `declare_float64`, Array
returns get `declare_array_var` (with element-sort resolution
via `_vera_type_to_z3_sort`).  Imported `FLOAT64` and `STRING`
constants from `vera.types`.

Added 4 new tests in `tests/test_verifier_coverage.py::TestSmtCoverage667`:

- `test_adt_element_array_indexing_verifies_tier1` — pins the
  ADT-element lookup via the direct map (CR-X2/X4).
- `test_string_return_type_typed_at_call_site` — pins String
  return type propagation through `_translate_call_with_info`
  (CR-X3/X5).
- `test_float64_return_type_typed_at_call_site` — same for
  Float64.
- `test_array_return_type_typed_at_call_site` — same for
  Array<T>, with `result[i]` in the callee postcondition
  verifying.

Doc counts auto-updated: test count 3,882 → 3,886 (+4),
test_verifier_coverage.py 84/1,382 → 88/1,483 (tests/lines).

Validation:

- `pytest tests/ -q` → 3,858 passed, 14 skipped, 14 deselected
- `mypy vera/` → clean
- `python scripts/check_walker_coverage.py` → clean
- `python scripts/check_doc_counts.py` → consistent
- All 9 `TestSmtCoverage667` tests pass (5 originals + 4 new)

Refs #667 #670

Co-Authored-By: Claude <noreply@anthropic.invalid>

The pr-review-toolkit audit on `66a9939` surfaced one critical
factual narrative error and three important findings.  This
commit addresses all four; suggestions and defensive-hardening
items kept as-is with rationale documented on the PR comment.

**CRITICAL — narrative correction across 5 surfaces**

Comment-analyzer empirically verified that the pre-#667
verifier did NOT vacuously verify the affected contracts at
Tier 1.  When `body_expr` translated to None (because of
FloatLit / ArrayLit blackouts), `vera/verifier.py:564` dropped
the contract to **Tier 3 with an E522 warning** ("Cannot
statically verify postcondition…"), not Tier 1.  There was no
soundness gap — the verifier was already honest about its
inability to translate the body.

My narrative across 5 files was wrong:

- `examples/json.vera::main` comment
- `tests/conformance/ch06_quantifiers.vera::main` /
  `::test_has_zero` comment
- `CHANGELOG.md` v0.0.153 "Fixed" section
- `tests/test_verifier.py::test_overall_tier_counts` docstring
- The issue comment on #667 (will post a correcting comment)

Corrected framing across all 5: the pre-fix contracts were
classified T3-with-warning; post-fix the verifier reaches the
contradiction and would report E500 instead; the contracts
were honestly relaxed to `ensures(true)` which trivially
verifies T1.  The 252/26 → 253/25 shift comes entirely from
the relaxation of `examples/json.vera::main` (T3-warning →
T1-trivial), not from any SMT-widening-driven movement.

**IMPORTANT 1 — CHANGELOG test count drift**

CHANGELOG said "5 new tests" in `TestSmtCoverage667`; actually
9 (5 from initial commit + 4 from call-result-typing follow-up).
Updated to "9 new tests in two clusters" with the cluster
breakdown.

**IMPORTANT 2 — `_translate_array_lit` defensive sort-mismatch
check**

Comment-analyzer flagged that the docstring claims mismatched
sorts "fail the translation" (return None), but the code has
no sort guard — Z3 raises `Z3Exception: sort mismatch` on the
`index_fn(lit, i) == elt` axiom.  Type checker rejects
heterogeneous arrays upstream so this is latent, but I'm going
with the defensive fix rather than the docstring-only fix:
added `if any(e.sort() != element_sort for e in
element_z3s[1:]): return None` before the axiom assertions.
Cheaper than fixing the docstring while leaving the actual
behaviour fragile.

**IMPORTANT 3 — `_get_element_sort_for_array` docstring**

Docstring described "three candidates" in tier 3 but the code
constructs two.  Rewrote the docstring to match: two candidates
(raw stripped key + angle-bracketed generic form).

**Three new negative / boundary tests**

Pr-test-analyzer flagged that all 9 existing #667 tests are
positive cases — a regression that reverts FloatLit / IndexExpr
/ ArrayLit to `return None` would silently pass.  Added 3 new
tests in `TestSmtCoverage667`:

- `test_floatlit_deliberately_false_contract_reports_e500` —
  `ensures(@Float64.result == 0.0)` over a body returning 1.5
  must report E500, not Tier 3 with warning.
- `test_arraylit_element_axiom_deliberately_false_reports_e500`
  — `ensures([1, 2, 3][0] == 999)` must report E500 (pins the
  per-element axiom is actually asserted to the solver, not
  just declared).
- `test_indexexpr_congruence_in_contract_verifies_tier1` —
  `@arr.0[i] == @arr.0[i]` must verify trivially via Z3
  function congruence (pins the `index_<sort>` is keyed by
  sort, not per call-site, so two references to the same
  arr[i] are recognised as identical).

**Skipped suggestions (with rationale on PR)**

- `import z3` ordering nit in `verifier.py` (PEP 8 nit; project
  style is lighter-touch).
- `smt._vera_type_to_z3_sort` encapsulation suggestion (the
  verifier is in the same architectural layer; promoting the
  helper is renaming churn for marginal value).
- `or self.declare_int(...)` fallback hardening (silent-failure-
  hunter flagged as "latent under current surface grammar";
  current is defensible until grammar relaxes — would file as
  a future-hardening issue if seen again).
- Replace `startswith("Array_")` with explicit sort set (current
  check is correct given `_get_array_sort`'s exclusive ownership
  of `Array_*` keys).

Doc counts auto-updated: test count 3,886 → 3,889 (+3 negative
tests), test_verifier_coverage.py 88/1,483 → 91/1,557.

Validation:

- `pytest tests/ -q` → 3,861 passed, 14 skipped, 14 deselected
- `mypy vera/` → clean
- `python scripts/check_doc_counts.py` → consistent
- 12/12 TestSmtCoverage667 tests pass (9 originals + 3 new)

Refs #667 #670

Co-Authored-By: Claude <noreply@anthropic.invalid>

Three new + two duplicates.  Skipping the duplicates with
rationale; fixing all three new findings + the test-shape
issue the warning-strict assertion surfaced.

**CR-Y3** (`tests/test_verifier_coverage.py:1236-1307`) — the
call-site typing tests asserted no errors but not no warnings.
Tier 3 fallback emits a warning (E522 / E523), not an error,
so the test could pass even if the call-result typing wasn't
being respected.

Adding `warnings == []` assertions immediately surfaced a
second issue: the original tests used `(())` (UnitLit) as the
call argument.  UnitLit returns None from `translate_expr`, so
the whole call's argument-translation short-circuits at
`_translate_call_with_info:1037` (`if z3_arg is None: return
None`), the call returns None, the body returns None, and the
verifier falls to Tier 3 with E522.  The call-result-typing
code path was never exercised.

Restructured the 3 tests with `@Int.0` slot-ref args (which
translate cleanly to Z3 Int vars).  Now the calls actually
succeed, the call-result typing is actually exercised, and
the warning-strict assertion catches any future regression
that drops back to Tier 3.

**CR-Y4** (`vera/smt.py::_translate_call_with_info` Array
branch) — the fallback `ret_var = self.declare_int(fresh)`
when `element_sort is None` is the same silent-failure pattern
silent-failure-hunter flagged earlier in this PR.  Replaced
with `return None`, signalling Tier 3 cleanly to the caller.
The caller's postcondition translation then sees None,
classifies as Tier 3, emits an E522 warning — visible failure
mode rather than silent type-erasure to Int.

**CR-Y5** (`spec/06-contracts.md:342`) — the Tier summary
table at §6.8 still listed "arrays" as a Tier 2 concern,
contradicting §6.3.1's Tier 1 classification.  Updated both
rows of the table:

- Tier 1 scope expanded to mention real/float (Z3 Real sort),
  strings, array literals + indexing via uninterpreted
  `index_<T>` functions (citing #667).
- Tier 2 scope narrowed to "quantifiers, lemma/assert hints"
  (the actual remaining Tier 2 surface, removing the now-
  Tier-1 arrays).

**Skipped duplicates**:

- `_get_element_sort_for_array` (`vera/smt.py:665-697`) — same
  finding as earlier CR; addressed in `66a9939` via
  `_array_element_sorts` direct map + 3-tier lookup.
- `_translate_call_with_info` Array branch routing
  (`vera/verifier.py:466-475`) — same finding as earlier CR;
  addressed in `66a9939`.  (Note: CR pointed at verifier.py
  but the actual code path is in smt.py.)

Doc counts auto-updated: test_verifier_coverage.py 1,557 →
1,590 lines (3 tests restructured with longer fixtures +
warning-strict assertions).

Validation:

- `pytest tests/ -q` → 3,861 passed, 14 skipped, 14 deselected
- `mypy vera/` → clean
- 12/12 `TestSmtCoverage667` tests pass with warning-strict
  assertions

Refs #667 #670

Co-Authored-By: Claude <noreply@anthropic.invalid>

Spec §6.8 Tier 1 row claimed "QF_LIA, real/float (Z3 `Real`
sort)" — internally inconsistent.  QF_LIA is Quantifier-Free
**Linear Integer** Arithmetic by SMT-LIB definition; reals are
in QF_LRA / QF_LIRA.  Vera's verifier uses `z3.IntSort()` AND
`z3.RealSort()` (for Float64), so the actual logic is QF_LIRA
(mixed integer + real) plus strings + uninterpreted functions
/ sorts.

Rewrote the row to "Z3 decidable fragment: linear integer +
real arithmetic (QF_LIRA), bool, strings (Z3 `String` sort),
uninterpreted sorts/functions (length, array literals and
indexing via `index_<T>` functions — #667)".  Drops the
contradiction; the QF_LIRA label is the right SMT-LIB name for
mixed integer+real LRA.

Validation
- `python scripts/check_spec_examples.py` -> clean
- `grep -n "QF_LIA"` -> 0 matches (no other stale references)

Refs #667 #670

Co-Authored-By: Claude <noreply@anthropic.invalid>

The QF_LIRA label from `127cdf8` was still misleading — QF_LIRA
is mixed Linear Integer + Real Arithmetic but doesn't include
strings or uninterpreted functions / sorts.  CR's escalation
of the previous round's nit catches that no single SMT-LIB
logic name covers Vera's full theory portfolio.

Rewrote the row to:

1. Drop the contradiction-inducing single label.
2. Describe the theories prose-style ("linear integer + real
   arithmetic, bool, strings, uninterpreted sorts/functions").
3. Add a clarifier sentence noting that QF_UFLIRA is the
   closest standard logic (LIA + LRA + UF) and that strings
   are a Z3-specific extension to the SMT-LIB standard.

The clarifier acknowledges the formal-name limitation rather
than picking a wrong-but-shorter label.  Future spec edits
that add a theory (e.g. fixed-precision bit vectors) just
extend the prose list without invalidating a formal-logic
claim.

Validation
- `python scripts/check_spec_examples.py` -> clean
- `grep -n "QF_LIA\|QF_LIRA\|QF_UFLIRA\|QF_LRA"` -> single
  occurrence (the new QF_UFLIRA clarifier reference)

Refs #667 #670

Co-Authored-By: Claude <noreply@anthropic.invalid>