Chapter 6.4 — Arrays

Verified Python lists, bounds proofs, and NumPy sidecar verification

Python Lists as Mutable Arrays

Python's list is a dynamic, heap-allocated, mutable array. Under the hood, CPython stores a contiguous C array of PyObject* pointers with an over-allocated capacity for amortised O(1) appends. For verification purposes, we model a list as a heap region that owns a sequence of indexed cells:

from deppy.separation import array_pts_to, SLProp

# array_pts_to(arr, seq) asserts:
#   1. arr is a list on the heap
#   2. arr contains exactly the elements in seq
#   3. We have exclusive ownership of arr

arr: list[int] = [10, 20, 30]
prop: SLProp = array_pts_to(arr, [10, 20, 30])

Element-level access is modelled through index assertions:

from deppy.separation import elem_at

# elem_at(arr, i, v) ≡ "arr[i] == v" as a heap assertion
# array_pts_to(arr, seq) ≡ ★ᵢ elem_at(arr, i, seq[i])

Bounds Checking Proofs

Python raises IndexError on out-of-bounds access. While this prevents memory corruption, it crashes your program at runtime. Deppy lets you prove at verification time that indices are always valid:

@requires(
    array_pts_to(arr, 'seq') and
    pure(0 <= i) and pure(i < len('seq'))
)
@ensures(lambda result:
    array_pts_to(arr, 'seq') and result == 'seq[i]')
def safe_get(arr: list[int], i: int) -> int:
    """Verified bounds-safe element access."""
    return arr[i]

Without the bounds precondition, verification fails:

@requires(array_pts_to(arr, 'seq'))
def unsafe_get(arr: list[int], i: int) -> int:
    return arr[i]  # ✗ Cannot prove 0 ≤ i < len(seq)

Array Initialization and Fill

@ensures(lambda result:
    array_pts_to(result, '[v] * n') and
    pure(len('[v] * n') == n))
def create_filled(n: int, v: int) -> list[int]:
    """Create a list of n copies of v."""
    return [v] * n

@requires(
    array_pts_to(arr, 'seq') and
    pure(len('seq') > 0))
@ensures(lambda _:
    array_pts_to(arr, '[v] * len(seq)'))
def fill(arr: list[int], v: int):
    """Fill all elements with value v."""
    for i in range(len(arr)):
        # loop invariant: arr[:i] == [v]*i, arr[i:] == seq[i:]
        arr[i] = v

Binary Search with Verified Bounds

Binary search is a classic verification target. We must prove:

1. All array accesses are within bounds
2. The loop terminates (the search window strictly shrinks)
3. If found, the returned index actually contains the target
4. If not found, the target is not present

@requires(
    array_pts_to(arr, 'seq') and
    pure('is_sorted(seq)'))
@ensures(lambda result:
    array_pts_to(arr, 'seq') and
    pure('(result == -1 and target not in seq) or seq[result] == target'))
@decreases('hi - lo')
def binary_search(arr: list[int], target: int) -> int:
    """Binary search returning index or -1."""
    lo, hi = 0, len(arr) - 1

    while lo <= hi:
        # invariant: target in seq ⟹ target in seq[lo..hi]
        # invariant: 0 ≤ lo ≤ hi+1 ≤ len(seq)
        mid = (lo + hi) // 2   # bounds: lo ≤ mid ≤ hi
        if arr[mid] == target:   # safe: 0 ≤ mid < len(seq)
            return mid
        elif arr[mid] < target:
            lo = mid + 1         # window shrinks: new_lo > old_lo
        else:
            hi = mid - 1         # window shrinks: new_hi < old_hi

    return -1

Sorting with Swap Verification

Array swaps are the building block of in-place sorts. We verify each swap preserves the array's contents (permutation property):

@requires(
    array_pts_to(arr, 'seq') and
    pure(0 <= i) and pure(i < len('seq')) and
    pure(0 <= j) and pure(j < len('seq')))
@ensures(lambda _:
    array_pts_to(arr, 'swap_at(seq, i, j)') and
    pure('is_permutation(swap_at(seq, i, j), seq)'))
def array_swap(arr: list[int], i: int, j: int):
    """Swap elements at indices i and j."""
    arr[i], arr[j] = arr[j], arr[i]

Selection Sort

@requires(array_pts_to(arr, 'seq'))
@ensures(lambda _:
    array_pts_to(arr, 'sorted_seq') and
    pure('is_sorted(sorted_seq)') and
    pure('is_permutation(sorted_seq, seq)'))
def selection_sort(arr: list[int]):
    """In-place selection sort with verified correctness."""
    n = len(arr)
    for i in range(n):
        # invariant: arr[:i] is sorted ∧ arr[:i] ≤ arr[i:]
        # invariant: arr is a permutation of original seq
        min_idx = i
        for j in range(i + 1, n):
            if arr[j] < arr[min_idx]:
                min_idx = j
        arr[i], arr[min_idx] = arr[min_idx], arr[i]

NumPy Array Verification via Sidecar

NumPy arrays are implemented in C and live outside Python's managed heap. Deppy cannot inspect their internal memory, so we use a sidecar proof (see Part 4) to verify properties about NumPy operations based on their documented semantics:

import numpy as np
from deppy.sidecar import numpy_spec

@numpy_spec
@requires(
    np_array(a, shape='(m, k)', dtype='float64') **
    np_array(b, shape='(k, n)', dtype='float64'))
@ensures(lambda result:
    np_array(result, shape='(m, n)', dtype='float64') and
    np_array(a, shape='(m, k)', dtype='float64') and
    np_array(b, shape='(k, n)', dtype='float64'))
def matmul(a: np.ndarray, b: np.ndarray) -> np.ndarray:
    """Matrix multiply with verified shape compatibility."""
    return a @ b

Verified Matrix Operations

Transpose Properties

@numpy_spec
@requires(np_array(a, shape='(m, n)'))
@ensures(lambda result:
    np_array(result, shape='(n, m)') and
    pure('transpose(transpose(a)) == a'))
def transpose(a: np.ndarray) -> np.ndarray:
    """Transpose with shape verification."""
    return a.T

Matrix Multiply with Shape Checking

@numpy_spec
@requires(
    np_array(a, shape='(m, k)') **
    np_array(b, shape='(k, n)') **
    np_array(c, shape='(n, p)'))
@ensures(lambda result:
    np_array(result, shape='(m, p)') and
    pure('result == (a @ b) @ c') and
    pure('result == a @ (b @ c)'))  # associativity
def triple_matmul(a, b, c):
    """Three-matrix product with associativity check."""
    return a @ b @ c

Array Slicing

Python's slice syntax creates a new list (unlike NumPy views). Deppy verifies slice bounds:

@requires(
    array_pts_to(arr, 'seq') and
    pure(0 <= lo) and pure(lo <= hi) and pure(hi <= len('seq')))
@ensures(lambda result:
    array_pts_to(arr, 'seq') and
    array_pts_to(result, 'seq[lo:hi]') and
    pure(len('seq[lo:hi]') == hi - lo))
def safe_slice(arr: list[int], lo: int, hi: int) -> list[int]:
    """Verified array slice."""
    return arr[lo:hi]

Example: In-Place Array Reversal

@requires(array_pts_to(arr, 'seq'))
@ensures(lambda _:
    array_pts_to(arr, 'list(reversed(seq))'))
def reverse_inplace(arr: list[int]):
    """Reverse array in place using two-pointer swap."""
    lo, hi = 0, len(arr) - 1
    while lo < hi:
        # invariant: arr[:lo] == rev(seq)[:lo]
        # invariant: arr[hi+1:] == rev(seq)[hi+1:]
        # invariant: arr[lo:hi+1] == seq[lo:hi+1]
        arr[lo], arr[hi] = arr[hi], arr[lo]
        lo += 1
        hi -= 1

Memory Safety in Python Context

Python already prevents buffer overflows — the runtime checks bounds and raises IndexError. So why verify array indices?

Comparison with Pulse Arrays

fn swap_arr
  (a: array int) (i j: nat)
  requires
    pts_to a 's' **
    pure (i < length s) **
    pure (j < length s)
  ensures
    pts_to a 'swap s i j'
{
  let vi = a.(i);
  let vj = a.(j);
  a.(i) <- vj;
  a.(j) <- vi;
}

@requires(
    array_pts_to(a, 's') and
    pure(i < len('s')) and
    pure(j < len('s')))
@ensures(lambda _:
    array_pts_to(a, 'swap(s,i,j)'))
def swap_arr(a, i, j):
    a[i], a[j] = a[j], a[i]