Type mutable-array length/reads and emit bounds obligations (closes #1117)

[jsiek]

Phase 2h: type mutable-array length/reads and emit bounds obligations

Closes #1117 (parent umbrella #854). Depends only on the already-merged
#1111 (proc signatures/contracts) and #1112 (obligation API), so this runs in
parallel with the #1113–#1116 chain exactly as the issue's parallelization note
describes.

What changed

Type checking (checker_types.py)

• a[i] on a mutable [T]! handle now type-checks to the element type T,
  mirroring the pure [T] path, and requires a UInt index (length(a) is
  UInt and < compares homogeneous pairs, so only a UInt index can form a
  provable i < length(a) bound). The pure ArrayType path is left
  byte-for-byte unchanged, so existing pure-array behavior (which never checked
  the index type) is preserved.
• length(a) on a mutable [T]! handle type-checks to the array-length type
  (UInt) via a new symbolic ArrayLength term node. The result type is read
  off the in-scope length function's return type rather than fabricated, so
  length(a) on an array agrees with length on a list. Any other length(...)
  call — including on a pure [T] array — falls back to ordinary list-length
  resolution. The intercept is applied in both type_synth_term and
  type_check_term so it works in synthesis, call-argument, and equality
  positions.

Obligation API (imperative_verifier.py)

• array_bounds_goal(read) builds the source-located i < length(a)
  bounds goal for a mutable-array read, using the same post-typecheck
  ResolvedVar constructor idiom mkEqual uses for =.
• ArrayBoundsObligations collects ARRAY_BOUNDS obligations for the reads
  seen in one verification pass and deduplicates repeated reads of the same
  source access, so a given a[i] yields at most one bounds goal.

New AST node

• ArrayLength in abstract_syntax/terms.py. It is produced only by the type
  checker (never parsed), so both parsers still see the surface length(a) as
  an ordinary Call and parser-equivalence/round-trip coverage is unaffected.
  It has no runtime reduction (an array's length is immutable for the handle's
  lifetime in Phase 2). The proof-rewrite walkers (count_marks / find_mark /
  replace_mark / rewrite_aux) are taught about it so replace/simplify/
  rewrite tactics work on formulas mentioning length(a). Scoping the length
  intercept to [T]! keeps ArrayLength confined to procedure specs and bounds
  obligations, which never reach the recursive-call or compiler walkers that
  pure runtime terms use.

Acceptance criteria

• In-bounds reads verify when a precondition supplies the bound — unit test
  discharges the obligation against a matching requires i < length(a) given.
• Missing bounds evidence produces the array-bounds diagnostic — unit test.
• Wrong index and element expectations are rejected by type checking —
  should-error fixture (bool index) plus unit tests; element mismatch is
  rejected by the existing = check over the read's element type.
• Pure-array regression fixtures are unchanged — full suite green.
• Unit tests distinguish ArrayType and MutableArrayType paths —
  test/unit/test_array_bounds.py.

Scope boundary

This slice delivers the typing and the obligation-construction/dedup
machinery. The pass that walks a verified procedure body and feeds each read
into ArrayBoundsObligations.record(...) is straight-line VC generation
(#1115+), which does not exist on main yet; the API here is the tool that
slice will call. Everything in this PR is exercised end-to-end through the
type checker (specs are type-checked today via #1111) and at the unit level.

Review response (Codex on 4f39468)

• Rewrite walkers: added ArrayLength cases to count_marks, find_mark,
  replace_mark, and rewrite_aux so rewriting/simplifying a formula with
  length(a) no longer hits internal_error.
• Index type: mutable-array indexes are now restricted to UInt (was
  UInt/Nat/Int), so a read always admits a provable i < length(a) bound.
• Intercept scope: length(a) typing is restricted to mutable [T]! only,
  keeping ArrayLength out of the recursive-call/compiler walkers.

Testing

• python3 test-deduce.py (full default incl. parser equivalence) — green.
• python3 test-deduce.py --imperative — green (both parsers; flag enrollment).
• ruff check ., mypy ., keywords.py, reference_grammar.py — all green.
• New test/unit/test_array_bounds.py — 9/9 (run manually; pytest not present
  in this container).
• LALR parity smoke-checked on both new fixtures.

Resume this session on ginger: ~/deduce-runner/resume.sh ce1bb127-0e51-4624-8b17-22ff0279807e routine/20260728-040201

🤖 Generated with Claude Code

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 4f39468747

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Add ArrayLength to rewrite walkers

Adding this new Term subclass without teaching the explicit rewrite helpers about it makes proof tactics fail on otherwise type-checked formulas that mention length(a): apply_rewrites calls count_marks before replace/simplify, and count_marks/find_mark/replace_mark/rewrite_aux all enumerate known node types and fall through to internal_error for ArrayLength. In practice, a theorem or future imperative obligation containing length(a) cannot be rewritten or simplified unless the rewrite happens to avoid these walkers entirely.

Useful? React with 👍 / 👎.

[chatgpt-codex-connector]

Keep mutable indexes compatible with length bounds

Including Nat and Int here lets a[i] type-check for index types that cannot use the emitted bounds shape: length(a) is typed as the stdlib list length result (UInt), while the existing < overloads compare homogeneous pairs, so a user cannot type-check the natural precondition i < length(a) for a Nat or Int index. Those reads will later produce unprovable or ill-typed bounds obligations unless the checker either restricts mutable-array indexes to UInt or builds/coerces the bounds goal in the index's type.

Useful? React with 👍 / 👎.

[jsiek]

Thanks — both P2 comments addressed in 2add2f8:

1. Rewrite walkers: ArrayLength is now handled in count_marks, find_mark, replace_mark, and rewrite_aux, so replace/simplify/rewrite on a formula mentioning length(a) no longer falls through to internal_error (verified: count_marks/find_mark/replace_mark recurse into the subject).
2. Index type: mutable-array indexes are restricted to UInt (was UInt/Nat/Int), matching the UInt-typed length(a) and the homogeneous < overloads, so a read always admits a provable i < length(a) bound.

I also scoped the length(a) intercept to mutable [T]! handles only (pure [T] length still falls back to list resolution as before), which keeps ArrayLength out of the recursive-call/compiler walkers entirely. Full suite + ruff/mypy green.