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

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))

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

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 `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:
+  if _type_named(index.typeof, 'UInt'):
+    return
+  user_error(index.location,
+             '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
+  # 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 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, 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)

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)

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",

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]
+{
+}

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, not bool

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]
+}

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)