From 00f0c93962bf58e2fe906475a5feeb804543b0d0 Mon Sep 17 00:00:00 2001 From: "deduce-routine (ginger)" Date: Tue, 28 Jul 2026 04:34:07 +0000 Subject: [PATCH 1/2] Type mutable-array length/reads and add bounds-obligation API (closes #1117) Phase 2h of the imperative verification layer (#854). - checker_types: type-check `a[i]` on a mutable `[T]!` handle to the element type with an unsigned/integer index requirement (pure `[T]` unchanged), and type `length(a)` on an array handle as the array-length type via a new symbolic ArrayLength node. - imperative_verifier: build the source-located `i < length(a)` ARRAY_BOUNDS obligation for a mutable-array read, with a per-pass dedup collector keyed on source access. - Unit tests distinguishing the ArrayType/MutableArrayType paths and covering obligation construction, dedup, and discharge; .pf fixtures for a valid read/length contract (should-warn) and a rejected non-integer index (should-error). Co-Authored-By: Claude Opus 4.8 (1M context) --- abstract_syntax/terms.py | 18 +++ checker_types.py | 76 +++++++++ imperative_verifier.py | 59 ++++++- test-deduce.py | 2 + .../imperative_mutable_array_bad_index.pf | 9 ++ .../imperative_mutable_array_bad_index.pf.err | 1 + test/should-warn/imperative_mutable_array.pf | 15 ++ .../imperative_mutable_array.pf.warn | 1 + test/unit/test_array_bounds.py | 147 ++++++++++++++++++ test/unit/test_ast_invariants.py | 5 + 10 files changed, 331 insertions(+), 2 deletions(-) create mode 100644 test/should-error/imperative_mutable_array_bad_index.pf create mode 100644 test/should-error/imperative_mutable_array_bad_index.pf.err create mode 100644 test/should-warn/imperative_mutable_array.pf create mode 100644 test/should-warn/imperative_mutable_array.pf.warn create mode 100644 test/unit/test_array_bounds.py diff --git a/abstract_syntax/terms.py b/abstract_syntax/terms.py index 8ffdd325..7325178b 100644 --- a/abstract_syntax/terms.py +++ b/abstract_syntax/terms.py @@ -1665,6 +1665,24 @@ def reduce(self, env: Env) -> Term: return new_get.reduce(env) return ArrayGet(self.location, self.typeof, subject_red, position_red) +@dataclass +class ArrayLength(Term): + # `length(a)` for a mutable-array handle (or a pure array). Produced only + # by the type checker when `length` is applied to an array-typed argument + # (issue #1117, Phase 2h); it is never parsed, so both parsers still see + # the surface `length(a)` as an ordinary `Call`. In Phase 2 an array's + # length is immutable for the lifetime of the handle, so this node has no + # runtime reduction -- the default `_map_children` walk only reduces the + # `subject`, leaving `length(a)` symbolic for use inside specifications and + # array-bounds obligations. + subject: Term + + def __eq__(self, other: object) -> bool: + return eq_fields(self, other, 'subject') + + def __str__(self) -> str: + return 'length(' + str(self.subject) + ')' + @dataclass class TLet(Term): var: str diff --git a/checker_types.py b/checker_types.py index 6c3208e6..fe3a9029 100644 --- a/checker_types.py +++ b/checker_types.py @@ -24,6 +24,7 @@ And, Array, ArrayGet, + ArrayLength, ArrayType, Bool, BoolType, @@ -114,6 +115,51 @@ def _var_ref_base_name(term: Term) -> str | None: return cast(str, term.get_name()).split('.')[0] return None +# A mutable-array index must be an unsigned/integer type, consistent with the +# pure-array reduction (which handles UInt and Nat positions). Checked only on +# the mutable-array path (#1117); pure-array indexing is left untouched. +_ARRAY_INDEX_TYPES = ('UInt', 'Nat', 'Int') + +def _check_array_index_type(index: Term) -> None: + ty = index.typeof + if isinstance(ty, IntType) \ + or any(_type_named(ty, name) for name in _ARRAY_INDEX_TYPES): + return + user_error(index.location, + 'a mutable-array index must be a ' + + ', '.join(_ARRAY_INDEX_TYPES) + ', not ' + str(ty)) + +def _array_length_result_type(loc: Meta, rator: Term) -> Type: + # The result type of `length` applied to an array handle is whatever the + # in-scope `length` function returns for a list (`UInt` in the stdlib). We + # read it off the resolved operator so no `UInt` node is fabricated here and + # `length(a)` on an array agrees with `length` on a list. + match rator.typeof: + case FunctionType(_, _, _, return_type): + return return_type + case OverloadType(_, overloads): + for _, overload_type in overloads: + if isinstance(overload_type, FunctionType): + return overload_type.return_type + user_error(loc, 'cannot determine the result type of length for an array; ' + 'is the standard library imported?') + +def _length_of_array( + loc: Meta, rator: Term, args: list[Term], env: Env, + recfun: RecursiveName, subterms: SubtermNames, +) -> Term | None: + # `length(a)` where `a` is an array handle (pure `[T]` or mutable `[T]!`) + # types as the array-length type (`UInt`) and stays symbolic (#1117). + # Returns None for any other `length` call so the caller falls back to the + # ordinary list-`length` resolution. + if len(args) != 1 or _var_ref_base_name(rator) != 'length': + return None + new_arg = type_synth_term(args[0], env, recfun, subterms) + if not isinstance(new_arg.typeof, (ArrayType, MutableArrayType)): + return None + new_rator = type_synth_term(rator, env, recfun, subterms) + return ArrayLength(loc, _array_length_result_type(loc, new_rator), new_arg) + def _nat_constructor_literal_value(term: Term) -> int | None: match term: case Mark(_, _, subject) | TAnnote(_, _, subject, _): @@ -988,8 +1034,26 @@ def type_synth_term( match new_array.typeof: case ArrayType(loc2, elt_type): ret = ArrayGet(loc, elt_type, new_array, new_index) + case MutableArrayType(loc2, elt_type): + # A mutable-array read `a[i]` has the element type, requires an + # unsigned/integer index, and (in a later verifier pass) carries an + # `i < length(a)` bounds obligation built by imperative_verifier. + _check_array_index_type(new_index) + ret = ArrayGet(loc, elt_type, new_array, new_index) case _: user_error(loc, 'expected an array, not ' + str(new_array.typeof)) + + case Call(loc, _, rator, [arg]) if _var_ref_base_name(rator) == 'length': + # `length(a)` on an array handle types as the array-length type (`UInt`) + # and stays symbolic (#1117); on any other argument it is an ordinary + # `length` call on a list, handled by the general Call path. + length_term = _length_of_array(loc, rator, [arg], env, recfun, subterms) + if length_term is not None: + ret = length_term + else: + ret = type_check_call(loc, rator, [arg], env, recfun, subterms, None, + term) + check_recursive_call(ret, recfun, subterms) case Call(loc, _, (OverloadedVar(loc2, ty2, [op_name, *_]) | ResolvedVar(loc2, ty2, op_name)), args) \ @@ -1237,6 +1301,18 @@ def type_check_term( + ' but got ' + str(ty)) return new_term + case Call(loc, _, rator, [arg]) if _var_ref_base_name(rator) == 'length': + length_term = _length_of_array(loc, rator, [arg], env, recfun, subterms) + if length_term is not None: + if length_term.typeof != typ: + user_error(loc, 'expected a term of type ' + str(typ) + + '\nbut got ' + str(length_term) + ' of type ' + + str(length_term.typeof)) + return length_term + ret = type_check_call(loc, rator, [arg], env, recfun, subterms, typ, term) + check_recursive_call(ret, recfun, subterms) + return ret + case Call(loc, _, rator, args): ret = type_check_call(loc, rator, args, env, recfun, subterms, typ, term) check_recursive_call(ret, recfun, subterms) diff --git a/imperative_verifier.py b/imperative_verifier.py index e2876d09..b4032f1f 100644 --- a/imperative_verifier.py +++ b/imperative_verifier.py @@ -28,12 +28,15 @@ from dataclasses import dataclass, field from enum import Enum -from typing import List, Optional, Tuple +from typing import List, Optional, Sequence, Set, Tuple, cast from lark.tree import Meta import style -from abstract_syntax import And, Bool, Env, Formula, Proof, is_true +from abstract_syntax import ( + And, ArrayGet, ArrayLength, Bool, Call, Env, Formula, Proof, ResolvedVar, + is_true, +) class ObligationKind(Enum): @@ -147,3 +150,55 @@ def _report_incomplete(self, env: Env) -> None: + style.orange('Goal:') + '\n\t' + str(self.goal) + givens_str(env), formula=self.goal, env=env) + + +# --- array-bounds obligations for mutable-array reads (issue #1117) ---------- + +def array_bounds_goal(read: ArrayGet) -> Formula: + """The bounds proof goal ``i < length(a)`` for a mutable-array read ``a[i]``. + + ``read`` is an already-type-checked ``ArrayGet`` over a mutable array. The + goal is built with a base-name ``ResolvedVar('<')`` over an ``ArrayLength`` + node -- the same post-typecheck constructor idiom ``mkEqual`` uses for ``=`` + -- so it matches a ``requires i < length(a)`` precondition (or loop + invariant) of the same shape once ``discharge`` reduces both sides.""" + loc = read.location + length = ArrayLength(read.subject.location, None, read.subject) + return cast(Formula, Call(loc, None, ResolvedVar(loc, None, '<'), + [read.position, length])) + + +def _read_key(read: ArrayGet) -> Tuple[object, object, str]: + """Identity of a source array access: its source span plus its rendered + form, so the same syntactic ``a[i]`` visited more than once in a pass is + recorded only once while two distinct accesses stay separate.""" + loc = read.location + return (getattr(loc, 'start_pos', None), getattr(loc, 'end_pos', None), + str(read)) + + +@dataclass +class ArrayBoundsObligations: + """Collect array-bounds obligations for the mutable-array reads seen in one + verification pass, deduplicating repeated reads of the same source access so + a given ``a[i]`` yields at most one ``i < length(a)`` goal (#1117).""" + + _seen: Set[Tuple[object, object, str]] = field(default_factory=set) + _obligations: List[ImperativeObligation] = field(default_factory=list) + + def record(self, read: ArrayGet, + givens: Sequence[Tuple[str, Formula]] = ()) -> None: + """Record the bounds obligation for one mutable-array read. A read whose + source access was already recorded in this pass is ignored.""" + key = _read_key(read) + if key in self._seen: + return + self._seen.add(key) + self._obligations.append( + ImperativeObligation(read.location, array_bounds_goal(read), + ObligationKind.ARRAY_BOUNDS, + givens=list(givens))) + + def obligations(self) -> List[ImperativeObligation]: + """The recorded obligations, in first-seen order.""" + return list(self._obligations) diff --git a/test-deduce.py b/test-deduce.py index 783766e2..c835907a 100644 --- a/test-deduce.py +++ b/test-deduce.py @@ -268,6 +268,8 @@ def _patched_check_system_limits() -> None: "./test/should-error/proc_call_as_term.pf", "./test/should-warn/imperative_false_proc.pf", "./test/should-warn/imperative_allocation.pf", + "./test/should-warn/imperative_mutable_array.pf", + "./test/should-error/imperative_mutable_array_bad_index.pf", "./test/should-error/imperative_new_pure_term.pf", "./test/should-error/imperative_new_operator_name.pf", "./test/should-validate/imperative_import.pf", diff --git a/test/should-error/imperative_mutable_array_bad_index.pf b/test/should-error/imperative_mutable_array_bad_index.pf new file mode 100644 index 00000000..72df0023 --- /dev/null +++ b/test/should-error/imperative_mutable_array_bad_index.pf @@ -0,0 +1,9 @@ +// Phase 2h (issue #1117): a mutable-array read must be indexed by an +// unsigned/integer type. Indexing a `[UInt]!` handle by a `bool` is a type +// error, caught while type-checking the postcondition. +import UInt + +proc bad_index(a: [UInt]!) + ensures a[true] = a[true] +{ +} diff --git a/test/should-error/imperative_mutable_array_bad_index.pf.err b/test/should-error/imperative_mutable_array_bad_index.pf.err new file mode 100644 index 00000000..3aa6d0ff --- /dev/null +++ b/test/should-error/imperative_mutable_array_bad_index.pf.err @@ -0,0 +1 @@ +./test/should-error/imperative_mutable_array_bad_index.pf:7.13-7.17: a mutable-array index must be a UInt, Nat, Int, not bool diff --git a/test/should-warn/imperative_mutable_array.pf b/test/should-warn/imperative_mutable_array.pf new file mode 100644 index 00000000..e3bf5f91 --- /dev/null +++ b/test/should-warn/imperative_mutable_array.pf @@ -0,0 +1,15 @@ +// Phase 2h (issue #1117): `length(a)` and mutable-array reads `a[i]` on a +// `[T]!` handle are now typed inside procedure specifications -- `length(a)` +// has the array-length type (`UInt`) and `a[i]` the element type, so a +// `requires i < length(a)` / `ensures result = a[i]` contract type-checks. +// Bodies and specs are still only recognized, so the proc emits the Phase 1m +// "accepted but not verified" warning (issue #1108). +import UInt +import List + +proc read_demo(a: [UInt]!, i: UInt) -> UInt + requires i < length(a) + ensures result = a[i] +{ + return a[i] +} diff --git a/test/should-warn/imperative_mutable_array.pf.warn b/test/should-warn/imperative_mutable_array.pf.warn new file mode 100644 index 00000000..7e4a924c --- /dev/null +++ b/test/should-warn/imperative_mutable_array.pf.warn @@ -0,0 +1 @@ +./test/should-warn/imperative_mutable_array.pf:10.1-15.2: warning: proc 'read_demo' is accepted but not verified -- parsing and declaration plumbing succeeded, but no verifier has run on its body or specs yet (experimental imperative layer, issue #854) diff --git a/test/unit/test_array_bounds.py b/test/unit/test_array_bounds.py new file mode 100644 index 00000000..e2cf58a3 --- /dev/null +++ b/test/unit/test_array_bounds.py @@ -0,0 +1,147 @@ +"""Unit tests for mutable-array read typing and array-bounds obligations +(issue #1117, Phase 2h). + +Two halves, both exercised without the CLI or the stdlib: + + * ``type_synth_term`` on an ``ArrayGet`` distinguishes the pure ``[T]`` path + (unchanged) from the mutable ``[T]!`` path (element type + index check); + * ``imperative_verifier`` builds and deduplicates the ``i < length(a)`` + bounds obligation for a mutable-array read. +""" + +from lark.tree import Meta + +from abstract_syntax import ( + ArrayGet, ArrayLength, ArrayType, BoolType, Call, Env, IntType, + MutableArrayType, ResolvedVar, Var, +) +from checker_types import type_synth_term +from error import IncompleteProof, UserError +from imperative_verifier import ( + ArrayBoundsObligations, ImperativeObligation, ObligationKind, + array_bounds_goal, +) + + +def _meta(start: int = 0, end: int = 1) -> Meta: + m = Meta() + m.empty = False + m.filename = 'test.pf' + m.line = 3 + m.column = 5 + m.start_pos = start + m.end_line = 3 + m.end_column = 6 + m.end_pos = end + return m + + +def _env() -> Env: + return Env({'__current_module__': 'test'}) + + +def _rv(name: str) -> ResolvedVar: + return ResolvedVar(_meta(), None, name) + + +def _typing_env() -> Env: + # A bare env with array/scalar term vars -- no stdlib needed because the + # ArrayGet path only reads the subject's `typeof` and (for the mutable path) + # the index's `typeof`. + env = _env() + env = env.declare_term_var(_meta(), 'marr', + MutableArrayType(_meta(), BoolType(_meta()))) + env = env.declare_term_var(_meta(), 'parr', + ArrayType(_meta(), BoolType(_meta()))) + env = env.declare_term_var(_meta(), 'idx', IntType(_meta())) + env = env.declare_term_var(_meta(), 'flag', BoolType(_meta())) + return env + + +def _read(subject: str = 'marr', index: str = 'idx', + start: int = 0, end: int = 5) -> ArrayGet: + return ArrayGet(_meta(start, end), None, _rv(subject), _rv(index)) + + +# --- ArrayType vs MutableArrayType typing ----------------------------------- + +def test_mutable_read_has_element_type() -> None: + ret = type_synth_term(_read('marr', 'idx'), _typing_env(), None, []) + assert isinstance(ret, ArrayGet) + assert ret.typeof == BoolType(_meta()) + + +def test_pure_read_is_unchanged_and_skips_index_check() -> None: + # The pure `[T]` path never checked the index type; a `bool` index that the + # mutable path rejects must still be accepted here so pure-array behavior is + # unchanged. + ret = type_synth_term(_read('parr', 'flag'), _typing_env(), None, []) + assert isinstance(ret, ArrayGet) + assert ret.typeof == BoolType(_meta()) + + +def test_mutable_read_rejects_non_integer_index() -> None: + try: + type_synth_term(_read('marr', 'flag'), _typing_env(), None, []) + assert False, 'expected a UserError for a bool index' + except UserError as e: + assert 'index must be' in str(e) + + +def test_read_of_non_array_is_rejected() -> None: + try: + type_synth_term(_read('flag', 'idx'), _typing_env(), None, []) + assert False, 'expected a UserError for a non-array subject' + except UserError as e: + assert 'expected an array' in str(e) + + +# --- bounds-obligation construction ----------------------------------------- + +def test_bounds_goal_is_index_less_than_length() -> None: + goal = array_bounds_goal(_read('marr', 'idx')) + assert isinstance(goal, Call) + assert isinstance(goal.rator, ResolvedVar) and goal.rator.get_name() == '<' + index, length = goal.args + assert index == _rv('idx') + assert isinstance(length, ArrayLength) and length.subject == _rv('marr') + + +def test_recording_a_read_yields_one_array_bounds_obligation() -> None: + collector = ArrayBoundsObligations() + collector.record(_read()) + obligations = collector.obligations() + assert len(obligations) == 1 + ob = obligations[0] + assert isinstance(ob, ImperativeObligation) + assert ob.kind is ObligationKind.ARRAY_BOUNDS + # Source-located at the read. + assert ob.location.start_pos == 0 and ob.location.end_pos == 5 + + +def test_duplicate_source_access_is_recorded_once() -> None: + collector = ArrayBoundsObligations() + collector.record(_read(start=0, end=5)) + collector.record(_read(start=0, end=5)) # same source access + collector.record(_read(start=6, end=11)) # a distinct access + assert len(collector.obligations()) == 2 + + +# --- discharge -------------------------------------------------------------- + +def test_in_bounds_read_verifies_when_precondition_supplies_the_bound() -> None: + collector = ArrayBoundsObligations() + collector.record(_read(), + givens=[('pre', array_bounds_goal(_read()))]) + collector.obligations()[0].discharge(_env()) # returns normally + + +def test_missing_bounds_evidence_reports_array_bounds_diagnostic() -> None: + collector = ArrayBoundsObligations() + collector.record(_read()) + try: + collector.obligations()[0].discharge(_env()) + assert False, 'expected an IncompleteProof' + except IncompleteProof as e: + assert 'array bounds' in str(e) + assert 'test.pf:3.5' in str(e) diff --git a/test/unit/test_ast_invariants.py b/test/unit/test_ast_invariants.py index a0c748fb..fa683d8a 100644 --- a/test/unit/test_ast_invariants.py +++ b/test/unit/test_ast_invariants.py @@ -211,6 +211,10 @@ def _spec_ArrayGet() -> ast.ArrayGet: return ast.ArrayGet(_meta(), None, _var("xs"), ast.Int(_meta(), None, 0)) +def _spec_ArrayLength() -> ast.ArrayLength: + return ast.ArrayLength(_meta(), None, _var("xs")) + + def _spec_TLet() -> ast.TLet: return ast.TLet(_meta(), None, "x", _var("rhs"), _var("body")) @@ -618,6 +622,7 @@ def _spec_AssociativeBinding() -> ast.AssociativeBinding: ast.Array: _spec_Array, ast.MakeArray: _spec_MakeArray, ast.ArrayGet: _spec_ArrayGet, + ast.ArrayLength: _spec_ArrayLength, ast.TLet: _spec_TLet, ast.And: _spec_And, ast.Or: _spec_Or, From 2add2f8c61607af85e9c5f9f8888fd4533ab3135 Mon Sep 17 00:00:00 2001 From: "deduce-routine (ginger)" Date: Thu, 30 Jul 2026 19:26:28 +0000 Subject: [PATCH 2/2] Address review: scope ArrayLength to [T]!, teach rewrite walkers, UInt index Codex review on PR #1150: - Teach the explicit rewrite walkers (count_marks/find_mark/replace_mark/ rewrite_aux) about ArrayLength so `replace`/`simplify`/rewrite tactics no longer internal_error on a formula mentioning `length(a)`. - Restrict the `length` intercept to mutable `[T]!` handles only, keeping ArrayLength confined to procedure specs and bounds obligations (never reaching the recursive-call/compiler walkers that pure runtime terms use). - Require a mutable-array index to be UInt: `length(a)` is UInt and `<` compares homogeneous pairs, so only a UInt index can form a provable `i < length(a)` bound. Co-Authored-By: Claude Opus 4.8 (1M context) --- abstract_syntax/rewrite.py | 12 +++++++- checker_types.py | 30 +++++++++---------- .../imperative_mutable_array_bad_index.pf.err | 2 +- test/unit/test_array_bounds.py | 12 ++++++-- 4 files changed, 36 insertions(+), 20 deletions(-) diff --git a/abstract_syntax/rewrite.py b/abstract_syntax/rewrite.py index 3b905ad0..b6e1aa71 100644 --- a/abstract_syntax/rewrite.py +++ b/abstract_syntax/rewrite.py @@ -104,6 +104,8 @@ def count_marks(formula: AST) -> int: return sum([count_marks(elt) for elt in elements]) case MakeArray(_, _, subject): return count_marks(subject) + case ArrayLength(_, _, subject): + return count_marks(subject) case _: internal_error(formula.location, 'in count_marks function, unhandled ' + str(formula)) @@ -165,6 +167,8 @@ def find_mark(formula: AST) -> None: find_mark(elt) case MakeArray(_, _, subject): find_mark(subject) + case ArrayLength(_, _, subject): + find_mark(subject) case _: internal_error(formula.location, 'in find_mark function, unhandled ' + str(formula)) @@ -238,6 +242,8 @@ def replace_mark(formula: Term | SwitchCase, replacement: Term) -> Term | Switch [replace_mark(elt, replacement) for elt in elements]) case MakeArray(loc2, tyof, subject): return MakeArray(loc2, tyof, replace_mark(subject, replacement)) + case ArrayLength(loc2, tyof, subject): + return ArrayLength(loc2, tyof, replace_mark(subject, replacement)) case _: internal_error(formula.location, 'in replace_mark function, unhandled ' + str(formula)) @@ -436,7 +442,11 @@ def rewrite_aux(loc: Meta, formula: Term | SwitchCase, equation: Formula | AutoR case MakeArray(loc2, tyof, subject): return MakeArray(loc, tyof, rewrite_aux(loc, subject, equation, env, depth - 1)) - + + case ArrayLength(loc2, tyof, subject): + return ArrayLength(loc, tyof, + rewrite_aux(loc, subject, equation, env, depth - 1)) + case TLet(loc2, tyof, var, rhs, body): return TLet(loc2, tyof, var, rewrite_aux(loc, rhs, equation, env, depth - 1), rewrite_aux(loc, body, equation, env, depth - 1)) diff --git a/checker_types.py b/checker_types.py index fe3a9029..cde4b7b8 100644 --- a/checker_types.py +++ b/checker_types.py @@ -115,19 +115,16 @@ def _var_ref_base_name(term: Term) -> str | None: return cast(str, term.get_name()).split('.')[0] return None -# A mutable-array index must be an unsigned/integer type, consistent with the -# pure-array reduction (which handles UInt and Nat positions). Checked only on -# the mutable-array path (#1117); pure-array indexing is left untouched. -_ARRAY_INDEX_TYPES = ('UInt', 'Nat', 'Int') - +# A mutable-array index must be `UInt`: `length(a)` is typed as the stdlib list +# length (`UInt`) and the `<` overloads compare homogeneous pairs, so only a +# `UInt` index can form the natural `i < length(a)` bound. Checked on the +# mutable-array path only (#1117); pure-array indexing is left untouched. def _check_array_index_type(index: Term) -> None: - ty = index.typeof - if isinstance(ty, IntType) \ - or any(_type_named(ty, name) for name in _ARRAY_INDEX_TYPES): + if _type_named(index.typeof, 'UInt'): return user_error(index.location, - 'a mutable-array index must be a ' - + ', '.join(_ARRAY_INDEX_TYPES) + ', not ' + str(ty)) + 'a mutable-array index must be a UInt, not ' + + str(index.typeof)) def _array_length_result_type(loc: Meta, rator: Term) -> Type: # The result type of `length` applied to an array handle is whatever the @@ -148,14 +145,17 @@ def _length_of_array( loc: Meta, rator: Term, args: list[Term], env: Env, recfun: RecursiveName, subterms: SubtermNames, ) -> Term | None: - # `length(a)` where `a` is an array handle (pure `[T]` or mutable `[T]!`) - # types as the array-length type (`UInt`) and stays symbolic (#1117). - # Returns None for any other `length` call so the caller falls back to the - # ordinary list-`length` resolution. + # `length(a)` where `a` is a mutable-array handle `[T]!` types as the + # array-length type (`UInt`) and stays symbolic (#1117). Returns None for any + # other `length` call -- including on a pure `[T]` array -- so the caller + # falls back to the ordinary list-`length` resolution. Scoping the intercept + # to `[T]!` keeps `ArrayLength` confined to procedure specifications and + # array-bounds obligations, which never reach the recursive-call or compiler + # walkers that pure runtime terms do. if len(args) != 1 or _var_ref_base_name(rator) != 'length': return None new_arg = type_synth_term(args[0], env, recfun, subterms) - if not isinstance(new_arg.typeof, (ArrayType, MutableArrayType)): + if not isinstance(new_arg.typeof, MutableArrayType): return None new_rator = type_synth_term(rator, env, recfun, subterms) return ArrayLength(loc, _array_length_result_type(loc, new_rator), new_arg) diff --git a/test/should-error/imperative_mutable_array_bad_index.pf.err b/test/should-error/imperative_mutable_array_bad_index.pf.err index 3aa6d0ff..1a5c7ad3 100644 --- a/test/should-error/imperative_mutable_array_bad_index.pf.err +++ b/test/should-error/imperative_mutable_array_bad_index.pf.err @@ -1 +1 @@ -./test/should-error/imperative_mutable_array_bad_index.pf:7.13-7.17: a mutable-array index must be a UInt, Nat, Int, not bool +./test/should-error/imperative_mutable_array_bad_index.pf:7.13-7.17: a mutable-array index must be a UInt, not bool diff --git a/test/unit/test_array_bounds.py b/test/unit/test_array_bounds.py index e2cf58a3..90109c89 100644 --- a/test/unit/test_array_bounds.py +++ b/test/unit/test_array_bounds.py @@ -12,8 +12,8 @@ from lark.tree import Meta from abstract_syntax import ( - ArrayGet, ArrayLength, ArrayType, BoolType, Call, Env, IntType, - MutableArrayType, ResolvedVar, Var, + ArrayGet, ArrayLength, ArrayType, BoolType, Call, Env, MutableArrayType, + ResolvedVar, ) from checker_types import type_synth_term from error import IncompleteProof, UserError @@ -44,6 +44,12 @@ def _rv(name: str) -> ResolvedVar: return ResolvedVar(_meta(), None, name) +def _uint_type() -> ResolvedVar: + # A stand-in for the `UInt` type: `_check_array_index_type` only inspects the + # type's base name, so a bare `UInt` reference is enough here -- no stdlib. + return ResolvedVar(_meta(), None, 'UInt') + + def _typing_env() -> Env: # A bare env with array/scalar term vars -- no stdlib needed because the # ArrayGet path only reads the subject's `typeof` and (for the mutable path) @@ -53,7 +59,7 @@ def _typing_env() -> Env: MutableArrayType(_meta(), BoolType(_meta()))) env = env.declare_term_var(_meta(), 'parr', ArrayType(_meta(), BoolType(_meta()))) - env = env.declare_term_var(_meta(), 'idx', IntType(_meta())) + env = env.declare_term_var(_meta(), 'idx', _uint_type()) env = env.declare_term_var(_meta(), 'flag', BoolType(_meta())) return env