Typed Memory Predicates

The memory model provides a heap of individual bytes; C* specifications talk about C objects. This page gives the chain of definitions that connects the two — single-byte ownership, little-endian merging into 2-, 4-, and 8-byte cells, per-type stores that add validity and range side conditions, and finally the ctype-indexed data_atdata_at and array_atarray_at families that appear in every C* specification — together with the rules the proof engine uses to take those assertions apart and put them back together.

The definitions live in the server library’s cst_interface.mlcst_interface.ml and cst_predefined.mlcst_predefined.ml; the derived lemmas are in cst_aux.mlcst_aux.ml; the user-facing rules are introduced in cstarlib.mlcstarlib.ml. For the underlying heap and the separation-logic connectives used below (****, &&&&, ||||, purepure, factfact, empemp, existsexists, |--|--, -|--|-), see Memory Model and Assertions.

Typed memory predicates are built in four layers. Each layer is a definition, not an axiom: everything in this section unfolds to a predicate over the byte-level memory of the memory model.

mstoremstore and mstore_noninitmstore_noninit lift the model’s one-cell memories (single_byte_memsingle_byte_mem, single_noninit_memsingle_noninit_mem) to heap propositions.

mstore (p:addr) (v:int) = (\st. ?v'. byte_eqm v v' /\ st = single_byte_mem p v')

mstore (p:addr) (v:int) = (\st. ?v'. byte_eqm v v' /\ st = single_byte_mem p v')

mstore_noninit (p:addr) = (\st. st = single_noninit_mem p \/ (?v. st = single_byte_mem p v))

mstore_noninit (p:addr) = (\st. st = single_noninit_mem p \/ (?v. st = single_byte_mem p v))

Two things are already visible here.

First, mstore p vmstore p v does not pin down vv exactly: it holds of the single-byte memory containing any v'v' that is byte-equivalent to vv, that is, congruent modulo . Storing --&1--&1 and storing &255&255 produce the same assertion. This is the mod-256 equivalence that makes the byte layer insensitive to whether a byte is read as signed or unsigned; sign is imposed one layer up, by the range condition of the typed store.

Second, mstore_noninit pmstore_noninit p is the assertion “I own the byte at pp, and I promise nothing about its contents”: the cell may be genuinely uninitialized, or it may hold some value the assertion refuses to name. It is the byte-level source of the whole undef_undef_ family.

byte_eqmbyte_eqm is eqmeqm at width 8, and eqmeqm is congruence modulo a power of two.

eqm (n:int) (x:int) (y:int) = (x == y) (mod exp_2 n)

eqm (n:int) (x:int) (y:int) = (x == y) (mod exp_2 n)

byte_eqm = eqm (&8)

byte_eqm = eqm (&8)

The mod-256 slack in mstoremstore gives a proved entailment that lets any two byte-equivalent values be exchanged under a store_bytestore_byte:

store_byte_vstore_byte_v (proved) — byte-equivalent values denote the same byte cell.

!v1 v2 p. byte_eqm v1 v2 ==> (store_byte p v1 |-- store_byte p v2)

!v1 v2 p. byte_eqm v1 v2 ==> (store_byte p v1 |-- store_byte p v2)

Wider cells are assembled from bytes by the little-endian merge relations. merge_short z1 z2 vmerge_short z1 z2 v says that the byte pair z1z1, z2z2 — low byte first — represents vv at width 16; merge_intmerge_int and merge_int64merge_int64 say the same at widths 32 and 64. Each is stated as an equation on remainders, so it constrains only the low bits of vv and only the low byte of each zizi.

merge_short (x1:int) (x2:int) (y:int) =
  (y rem exp_2(&16) = x2 rem exp_2(&8) * exp_2(&8)
                    + x1 rem exp_2(&8))

merge_short (x1:int) (x2:int) (y:int) =
  (y rem exp_2(&16) = x2 rem exp_2(&8) * exp_2(&8)
                    + x1 rem exp_2(&8))

merge_int (x1:int) (x2:int) (x3:int) (x4:int) (y:int) =
  (y rem exp_2(&32) = x4 rem exp_2(&8) * exp_2(&24)
                    + x3 rem exp_2(&8) * exp_2(&16)
                    + x2 rem exp_2(&8) * exp_2(&8)
                    + x1 rem exp_2(&8))

merge_int (x1:int) (x2:int) (x3:int) (x4:int) (y:int) =
  (y rem exp_2(&32) = x4 rem exp_2(&8) * exp_2(&24)
                    + x3 rem exp_2(&8) * exp_2(&16)
                    + x2 rem exp_2(&8) * exp_2(&8)
                    + x1 rem exp_2(&8))

merge_int64 (x1:int) (x2:int) (x3:int) (x4:int) (x5:int) (x6:int) (x7:int) (x8:int) (y:int) =
  (y rem exp_2(&64) = x8 rem exp_2(&8) * exp_2(&56)
                    + x7 rem exp_2(&8) * exp_2(&48)
                    + x6 rem exp_2(&8) * exp_2(&40)
                    + x5 rem exp_2(&8) * exp_2(&32)
                    + x4 rem exp_2(&8) * exp_2(&24)
                    + x3 rem exp_2(&8) * exp_2(&16)
                    + x2 rem exp_2(&8) * exp_2(&8)
                    + x1 rem exp_2(&8))

merge_int64 (x1:int) (x2:int) (x3:int) (x4:int) (x5:int) (x6:int) (x7:int) (x8:int) (y:int) =
  (y rem exp_2(&64) = x8 rem exp_2(&8) * exp_2(&56)
                    + x7 rem exp_2(&8) * exp_2(&48)
                    + x6 rem exp_2(&8) * exp_2(&40)
                    + x5 rem exp_2(&8) * exp_2(&32)
                    + x4 rem exp_2(&8) * exp_2(&24)
                    + x3 rem exp_2(&8) * exp_2(&16)
                    + x2 rem exp_2(&8) * exp_2(&8)
                    + x1 rem exp_2(&8))

store_bytestore_byte and store_byte_noninitstore_byte_noninit are mstoremstore and mstore_noninitmstore_noninit under another name; the wider stores existentially quantify the constituent bytes and tie them to the value with a merge relation.

store_byte:addr->int->expr = mstore
store_byte_noninit:addr->expr = mstore_noninit

store_byte:addr->int->expr = mstore
store_byte_noninit:addr->expr = mstore_noninit

(exprexpr is the type abbreviation :model->bool:model->bool that hprophprop also names.)

store_2byte x v = exists z1 z2.
  pure(merge_short z1 z2 v) && store_byte x z1 ** store_byte (x + &1) z2

store_2byte x v = exists z1 z2.
  pure(merge_short z1 z2 v) && store_byte x z1 ** store_byte (x + &1) z2

store_4byte x v = exists z1 z2 z3 z4.
  pure(merge_int z1 z2 z3 z4 v) &&
  store_byte x z1 ** store_byte (x + &1) z2 ** store_byte (x + &2) z3 ** store_byte (x + &3) z4

store_4byte x v = exists z1 z2 z3 z4.
  pure(merge_int z1 z2 z3 z4 v) &&
  store_byte x z1 ** store_byte (x + &1) z2 ** store_byte (x + &2) z3 ** store_byte (x + &3) z4

store_8bytestore_8byte follows the same shape with eight bytes and merge_int64merge_int64. The uninitialized counterparts need no merge, only ownership of the right number of consecutive bytes:

store_2byte_noninit x = store_byte_noninit x ** store_byte_noninit (x + &1)

store_2byte_noninit x = store_byte_noninit x ** store_byte_noninit (x + &1)

store_4byte_noninit x =
  store_byte_noninit x ** store_byte_noninit (x + &1) **
  store_byte_noninit (x + &2) ** store_byte_noninit (x + &3)

store_4byte_noninit x =
  store_byte_noninit x ** store_byte_noninit (x + &1) **
  store_byte_noninit (x + &2) ** store_byte_noninit (x + &3)

A typed store is a fixed-width byte store conjoined with the pure conditions that make it a legal C object of that type: the address must be a valid, correctly aligned pointer for the type, and the value must be in the type’s range.

store_int x v = pure(isvalidptr_int x /\ int_min_signed <= v /\ v <= int_max_signed) && store_4byte x v

store_int x v = pure(isvalidptr_int x /\ int_min_signed <= v /\ v <= int_max_signed) && store_4byte x v

The nine typed stores and their uninitialized forms:

Each store also asserts the validity predicate for its width — isvalidptr_charisvalidptr_char for the 1-byte stores, isvalidptr_shortisvalidptr_short for 2 bytes, isvalidptr_intisvalidptr_int for 4, isvalidptr_int64isvalidptr_int64 for 8, and isvalidptrisvalidptr for store_ptrstore_ptr. The uninitialized forms keep the validity condition and drop the range condition, since there is no value to constrain:

undef_store_int (x:addr) = (pure(isvalidptr_int x) && store_4byte_noninit x)

undef_store_int (x:addr) = (pure(isvalidptr_int x) && store_4byte_noninit x)

These are ordinary theorems of the model, not axioms. They are what the layering buys.

• store_char_rangestore_char_range, store_uchar_rangestore_uchar_range, …, store_ptr_rangestore_ptr_range (proved) — each typed store entails its range condition as a pure proposition, e.g. !p v. store_int p v |-- pure(int_min_signed <= v /\ v <= int_max_signed)!p v. store_int p v |-- pure(int_min_signed <= v /\ v <= int_max_signed).
• store_char_undef_store_charstore_char_undef_store_char, …, store_ptr_undef_store_ptrstore_ptr_undef_store_ptr (proved) — a typed store entails its uninitialized form: !p v. store_int p v |-- undef_store_int p!p v. store_int p v |-- undef_store_int p. These rest on store_byte_store_byte_noinitstore_byte_store_byte_noinit and its 2-, 4-, and 8-byte liftings.
• dup_mstoredup_mstore, dup_mstore_noninitdup_mstore_noninit, dup_store_byte_noninitdup_store_byte_noninit (proved) — a byte cannot be owned twice: !p v1 v2. mstore p v1 ** mstore p v2 |-- hfalse!p v1 v2. mstore p v1 ** mstore p v2 |-- hfalse. This is the model-level fact behind the data_at_dupdata_at_dup rule below.
• store_int_store_charstore_int_store_char, store_uint_store_charstore_uint_store_char, store_int_store_ucharstore_int_store_uchar, store_uint_store_ucharstore_uint_store_uchar (proved) — a 4-byte cell is equivalent to four 1-byte cells plus the merge relation, the alignment fact, and the range fact; this is the byte-reinterpretation rule at the store layer, mirrored at the data_atdata_at layer by data_at_Tuint_Tuchardata_at_Tuint_Tuchar and data_at_Tuchar_Tuintdata_at_Tuchar_Tuint.

Validity is a conjunction of an address-space bound and an alignment condition; alignment is congruence to zero modulo the required byte count.

aligned_n (n:int) (x:int) = (x == &0) (mod n)

aligned_n (n:int) (x:int) = (x == &0) (mod n)

isvalidptr_char (x:int) = (&0 <= x /\ x <= int64_max_unsigned)
isvalidptr_short (x:int) = (&0 <= x /\ x + &1 <= int64_max_unsigned /\ aligned_n (&2) x)
isvalidptr_int (x:int) = (&0 <= x /\ x + &3 <= int64_max_unsigned /\ aligned_n (&4) x)
isvalidptr_int64 (x:int) = (&0 <= x /\ x + &7 <= int64_max_unsigned /\ aligned_n (&8) x)
isvalidptr (x:int) = (&0 <= x /\ x + &7 <= int64_max_unsigned /\ aligned_n (&8) x)

isvalidptr_char (x:int) = (&0 <= x /\ x <= int64_max_unsigned)
isvalidptr_short (x:int) = (&0 <= x /\ x + &1 <= int64_max_unsigned /\ aligned_n (&2) x)
isvalidptr_int (x:int) = (&0 <= x /\ x + &3 <= int64_max_unsigned /\ aligned_n (&4) x)
isvalidptr_int64 (x:int) = (&0 <= x /\ x + &7 <= int64_max_unsigned /\ aligned_n (&8) x)
isvalidptr (x:int) = (&0 <= x /\ x + &7 <= int64_max_unsigned /\ aligned_n (&8) x)

The bound is stated on the address of the object’s last byte, so an intint object must fit entirely inside the 64-bit address space. Note that &0 <= x&0 <= x is a lower bound, not a non-null condition: the null address satisfies every one of these predicates. Non-nullness of a pointer is a separate fact, and in practice it comes from owning the pointee — data_atdata_at at address &0&0 is not contradictory by itself, but the specifications that need non-nullness state it.

exp_2exp_2 is the integer power of two; the bound constants are derived from it, and the casts are Euclidean remainder operations.

exp_2 (n:int) : int = &(2 EXP (num_of_int n))
max_unsigned (n:int) = (exp_2 n) - &1
max_signed (n:int) = (exp_2 (n - &1)) - &1
min_signed (n:int) = --exp_2 (n - &1)

exp_2 (n:int) : int = &(2 EXP (num_of_int n))
max_unsigned (n:int) = (exp_2 n) - &1
max_signed (n:int) = (exp_2 (n - &1)) - &1
min_signed (n:int) = --exp_2 (n - &1)

cast_unsigned (n:int) (z:int) = z rem (exp_2 n)

cast_unsigned (n:int) (z:int) = z rem (exp_2 n)

cast_signed (n:int) (z:int) =
  let x = cast_unsigned n z in
    if x < (exp_2 (n - &1)) then x else x - exp_2 n

cast_signed (n:int) (z:int) =
  let x = cast_unsigned n z in
    if x < (exp_2 (n - &1)) then x else x - exp_2 n

HOL Light’s remrem on integers is Euclidean: for a positive modulus the remainder is always non-negative. cast_unsigned n zcast_unsigned n z therefore lands in for every zz, including negative ones — it is truncation to the low nn bits, not the C %% operator. cast_signedcast_signed then reinterprets the top bit by subtracting when the truncated value is at least . Both facts are proved:

cast_unsigned_boundcast_unsigned_bound (proved)

!n z. &0 <= cast_unsigned n z /\ cast_unsigned n z <= max_unsigned n

!n z. &0 <= cast_unsigned n z /\ cast_unsigned n z <= max_unsigned n

cast_signed_boundcast_signed_bound (proved)

!n z. &0 < n ==> min_signed n <= cast_signed n z /\ cast_signed n z <= max_signed n

!n z. &0 < n ==> min_signed n <= cast_signed n z /\ cast_signed n z <= max_signed n

Two further proved lemmas say the casts are transparent modulo — cast_unsigned_remcast_unsigned_rem and cast_signed_remcast_signed_rem both state cast_* n v rem exp_2 n = v rem exp_2 ncast_* n v rem exp_2 n = v rem exp_2 n — from which cast_unsigned_byte_eqmcast_unsigned_byte_eqm and cast_signed_byte_eqmcast_signed_byte_eqm follow at width 8.

The named constants used in the typed stores are max_unsignedmax_unsigned, max_signedmax_signed, and min_signedmin_signed at widths 8, 16, 32, and 64.

byte_eqm            = eqm (&8)
byte_max_unsigned   = max_unsigned (&8)
byte_max_signed     = max_signed (&8)
byte_min_signed     = min_signed (&8)
short_max_unsigned  = max_unsigned (&16)
short_max_signed    = max_signed (&16)
short_min_signed    = min_signed (&16)
int_max_unsigned    = max_unsigned (&32)
int_max_signed      = max_signed (&32)
int_min_signed      = min_signed (&32)
int64_max_unsigned  = max_unsigned (&64)
int64_max_signed    = max_signed (&64)
int64_min_signed    = min_signed (&64)

byte_eqm            = eqm (&8)
byte_max_unsigned   = max_unsigned (&8)
byte_max_signed     = max_signed (&8)
byte_min_signed     = min_signed (&8)
short_max_unsigned  = max_unsigned (&16)
short_max_signed    = max_signed (&16)
short_min_signed    = min_signed (&16)
int_max_unsigned    = max_unsigned (&32)
int_max_signed      = max_signed (&32)
int_min_signed      = min_signed (&32)
int64_max_unsigned  = max_unsigned (&64)
int64_max_signed    = max_signed (&64)
int64_min_signed    = min_signed (&64)

There is no byte_min_unsignedbyte_min_unsigned and so on: the unsigned lower bound is written &0&0 directly everywhere it is needed.

data_atdata_at dispatches on a ctypectype, the datatype of C types:

ctype = Tchar  | Tuchar  |
        Tshort | Tushort |
        Tint   | Tuint   |
        Tint64 | Tuint64 |
        Tptr   | Tstruct string (string)list (ctype)list

ctype = Tchar  | Tuchar  |
        Tshort | Tushort |
        Tint   | Tuint   |
        Tint64 | Tuint64 |
        Tptr   | Tstruct string (string)list (ctype)list

A TstructTstruct carries the struct’s name, its field names, and its field types, in that order.

data_at x ty vdata_at x ty v is the typed store selected by tyty. Nine clauses, one per scalar ctype:

data_at x Tchar v    = store_char x v /\
data_at x Tuchar v   = store_uchar x v /\
data_at x Tshort v   = store_short x v /\
data_at x Tushort v  = store_ushort x v /\
data_at x Tint v     = store_int x v /\
data_at x Tuint v    = store_uint x v /\
data_at x Tint64 v   = store_int64 x v /\
data_at x Tuint64 v  = store_uint64 x v /\
data_at x Tptr v     = store_ptr x v

data_at x Tchar v    = store_char x v /\
data_at x Tuchar v   = store_uchar x v /\
data_at x Tshort v   = store_short x v /\
data_at x Tushort v  = store_ushort x v /\
data_at x Tint v     = store_int x v /\
data_at x Tuint v    = store_uint x v /\
data_at x Tint64 v   = store_int64 x v /\
data_at x Tuint64 v  = store_uint64 x v /\
data_at x Tptr v     = store_ptr x v

The value argument is an intint in every clause, including TptrTptr: an address is an integer in this model, so a pointer-valued cell and an int64int64-valued cell differ only in their validity and range conditions.

The same dispatch over the uninitialized stores — ownership of the right number of bytes at a valid, aligned address, with no claim about contents:

undef_data_at x Tchar   = undef_store_char x /\
undef_data_at x Tuchar  = undef_store_uchar x /\
undef_data_at x Tshort  = undef_store_short x /\
undef_data_at x Tushort = undef_store_ushort x /\
undef_data_at x Tint    = undef_store_int x /\
undef_data_at x Tuint   = undef_store_uint x /\
undef_data_at x Tint64  = undef_store_int64 x /\
undef_data_at x Tuint64 = undef_store_uint64 x /\
undef_data_at x Tptr    = undef_store_ptr x

undef_data_at x Tchar   = undef_store_char x /\
undef_data_at x Tuchar  = undef_store_uchar x /\
undef_data_at x Tshort  = undef_store_short x /\
undef_data_at x Tushort = undef_store_ushort x /\
undef_data_at x Tint    = undef_store_int x /\
undef_data_at x Tuint   = undef_store_uint x /\
undef_data_at x Tint64  = undef_store_int64 x /\
undef_data_at x Tuint64 = undef_store_uint64 x /\
undef_data_at x Tptr    = undef_store_ptr x

Each scalar ctype has a size in bytes and a value range. These three functions are what the array rules use to do address arithmetic and to state bounds.

min_ofmin_of and max_ofmax_of are defined in terms of the named width constants — min_of(Tint) = int_min_signedmin_of(Tint) = int_min_signed, max_of(Tuint) = int_max_unsignedmax_of(Tuint) = int_max_unsigned, and so on, with min_ofmin_of of every unsigned type and of TptrTptr equal to &0&0. The numerals in the table above come from two match-form axioms that evaluate those constants once and for all:

min_of_defmin_of_def, max_of_defmax_of_def (axiom) — the numeric values, in match form.

!ty:ctype.
  max_of(ty) =
    match ty with
    | Tchar    ->  &127
    | Tuchar   ->  &255
    | Tshort   ->  &32767
    | Tushort  ->  &65535
    | Tint     ->  &2147483647
    | Tuint    ->  &4294967295
    | Tint64   ->  &9223372036854775807
    | Tuint64  ->  &18446744073709551615
    | Tptr     ->  &18446744073709551615

!ty:ctype.
  max_of(ty) =
    match ty with
    | Tchar    ->  &127
    | Tuchar   ->  &255
    | Tshort   ->  &32767
    | Tushort  ->  &65535
    | Tint     ->  &2147483647
    | Tuint    ->  &4294967295
    | Tint64   ->  &9223372036854775807
    | Tuint64  ->  &18446744073709551615
    | Tptr     ->  &18446744073709551615

min_of_defmin_of_def has the same shape with --(&128)--(&128), &0&0, --(&32768)--(&32768), &0&0, --(&2147483648)--(&2147483648), &0&0, --(&9223372036854775808)--(&9223372036854775808), &0&0, &0&0. Neither axiom has a TstructTstruct case, so min_ofmin_of and max_ofmax_of of a struct type stay opaque.

sizeofsizeof is defined by mutual recursion with sizesofsizesof and then given a direct characterization, sizeof_defsizeof_def (proved), whose struct clause is sizeof(Tstruct name fnamel tyl) = ITLIST (+) (MAP sizeof tyl) 0isizeof(Tstruct name fnamel tyl) = ITLIST (+) (MAP sizeof tyl) 0i — the sum of the field sizes, with no padding. One further fact is an axiom:

sizeof_ge_0sizeof_ge_0 (axiom) — sizes are non-negative.

!ty:ctype. sizeof ty >= &0

!ty:ctype. sizeof ty >= &0

data_at_to_undef_data_atdata_at_to_undef_data_at (axiom) — forget the value, keep the ownership.

!x ty v. data_at x ty v |-- undef_data_at x ty

!x ty v. data_at x ty v |-- undef_data_at x ty

data_at_rangedata_at_range (axiom) — a data_atdata_at cell carries its type’s value range as a pure fact, without giving up the cell.

!x ty v. data_at x ty v |-- data_at x ty v ** fact(min_of(ty) <= v && v <= max_of(ty))

!x ty v. data_at x ty v |-- data_at x ty v ** fact(min_of(ty) <= v && v <= max_of(ty))

data_at_dupdata_at_dup (axiom) — a cell cannot be owned twice.

!x ty v1 v2. data_at x ty v1 ** data_at x ty v2 |-- false

!x ty v1 v2. data_at x ty v1 ** data_at x ty v2 |-- false

undef_data_at_dupundef_data_at_dup (axiom) — nor can an uninitialized cell.

!x ty. undef_data_at x ty ** undef_data_at x ty |-- false

!x ty. undef_data_at x ty ** undef_data_at x ty |-- false

data_at_rangedata_at_range is the standard way to obtain a bound on a value that was read out of memory: the fact(…)fact(…) conjunct is a pure proposition that survives into the SMT-facing part of a goal. data_at_dupdata_at_dup is the source of most “these two pointers must be different” arguments — assume they are equal, derive falsefalse.

array_atarray_at is the lo = &0lo = &0 case, which is the form that appears in almost every specification:

array_at (x:addr) (ty:ctype) (n:int) (l:(int)list) = array_at_rec x ty (&0) n l

array_at (x:addr) (ty:ctype) (n:int) (l:(int)list) = array_at_rec x ty (&0) n l

The recursive predicates are instances of generic array-of-store combinators, specialized by the element-placement function \y i v. data_at (y + i * sizeof(ty)) ty v\y i v. data_at (y + i * sizeof(ty)) ty v:

array_at_rec (x:addr) (ty:ctype) (lo:int) (hi:int) (l:(int)list) =
  store_array_rec (\y i v. data_at (y + i * sizeof(ty)) ty v) x lo hi l

array_at_rec (x:addr) (ty:ctype) (lo:int) (hi:int) (l:(int)list) =
  store_array_rec (\y i v. data_at (y + i * sizeof(ty)) ty v) x lo hi l

array_at_missing_i_rec (x:addr) (ty:ctype) (i:int) (lo:int) (hi:int) (l:(int)list) =
  store_array_missing_i_rec (\y i v. data_at (y + i * sizeof(ty)) ty v) x i lo hi l

array_at_missing_i_rec (x:addr) (ty:ctype) (i:int) (lo:int) (hi:int) (l:(int)list) =
  store_array_missing_i_rec (\y i v. data_at (y + i * sizeof(ty)) ty v) x i lo hi l

array_at_missing_i_rec x ty i lo hi larray_at_missing_i_rec x ty i lo hi l is the array with a hole: it owns every element of the range lo..hi-1lo..hi-1 except the one at index ii, whose cell has been split off. The list ll still has the full length of the range — the value at the hole is present in ll but the corresponding memory is not owned — which is what makes it possible to put the cell back with a different value and read off the result as replace_inthreplace_inth.

The undef_undef_ family owns the same addresses but says nothing about contents. Because there is no list to recurse on, these predicates recurse on the element count, passed as an intint and converted with num_of_intnum_of_int:

undef_array_at_rec (x:addr) (ty:ctype) (lo:int) (hi:int) (n:int) =
  store_undef_array_rec (\y i. undef_data_at (y + i * sizeof(ty)) ty) x lo hi (num_of_int n)

undef_array_at_rec (x:addr) (ty:ctype) (lo:int) (hi:int) (n:int) =
  store_undef_array_rec (\y i. undef_data_at (y + i * sizeof(ty)) ty) x lo hi (num_of_int n)

undef_array_at_missing_i_rec (x:addr) (ty:ctype) (i:int) (lo:int) (hi:int) (n:int) =
  store_undef_array_missing_i_rec (\y i. undef_data_at (y + i * sizeof(ty)) ty) x i lo hi (num_of_int n)

undef_array_at_missing_i_rec (x:addr) (ty:ctype) (i:int) (lo:int) (hi:int) (n:int) =
  store_undef_array_missing_i_rec (\y i. undef_data_at (y + i * sizeof(ty)) ty) x i lo hi (num_of_int n)

undef_array_at (x:addr) (ty:ctype) (n:int) = undef_array_at_rec x ty (&0) n n

undef_array_at (x:addr) (ty:ctype) (n:int) = undef_array_at_rec x ty (&0) n n

Note that undef_array_atundef_array_at passes nn twice: once as the upper index bound hihi and once as the recursion count. The two coincide only because lolo is &0&0.

The definitions above are stated through the generic combinators, which makes them awkward to rewrite with directly. cst_aux.mlcst_aux.ml proves the following match-form equations, which are the practical unfolding rules; all four are proved, not assumed.

array_at_rec_defarray_at_rec_def (proved)

!x:addr ty:ctype lo:int hi:int l:(int)list.
  array_at_rec x ty lo hi l =
    match l with
    | [] -> fact(lo == hi && l == [])
    | h :: t -> data_at (x + lo * sizeof(ty)) ty h ** array_at_rec x ty (lo + &1) hi t

!x:addr ty:ctype lo:int hi:int l:(int)list.
  array_at_rec x ty lo hi l =
    match l with
    | [] -> fact(lo == hi && l == [])
    | h :: t -> data_at (x + lo * sizeof(ty)) ty h ** array_at_rec x ty (lo + &1) hi t

array_at_missing_i_rec_defarray_at_missing_i_rec_def (proved)

!x:addr ty:ctype i:int lo:int hi:int l:(int)list.
  array_at_missing_i_rec x ty i lo hi l =
    match l with
    | [] -> false
    | h :: t -> ( fact(i == lo) ** array_at_rec x ty (lo + &1) hi t ) ||
                ( fact(i > lo) ** data_at (x + lo * sizeof(ty)) ty h ** array_at_missing_i_rec x ty i (lo + &1) hi t )

!x:addr ty:ctype i:int lo:int hi:int l:(int)list.
  array_at_missing_i_rec x ty i lo hi l =
    match l with
    | [] -> false
    | h :: t -> ( fact(i == lo) ** array_at_rec x ty (lo + &1) hi t ) ||
                ( fact(i > lo) ** data_at (x + lo * sizeof(ty)) ty h ** array_at_missing_i_rec x ty i (lo + &1) hi t )

undef_array_at_rec_defundef_array_at_rec_def (proved)

!x:addr ty:ctype lo:int hi:int n:int.
  undef_array_at_rec x ty lo hi n =
    match num_of_int n with
    | 0 -> fact(lo == hi)
    | SUC m -> undef_data_at (x + lo * sizeof(ty)) ty ** undef_array_at_rec x ty (lo + &1) hi (&m)

!x:addr ty:ctype lo:int hi:int n:int.
  undef_array_at_rec x ty lo hi n =
    match num_of_int n with
    | 0 -> fact(lo == hi)
    | SUC m -> undef_data_at (x + lo * sizeof(ty)) ty ** undef_array_at_rec x ty (lo + &1) hi (&m)

undef_array_at_missing_i_rec_defundef_array_at_missing_i_rec_def (proved)

!x:addr ty:ctype i:int lo:int hi:int n:int.
  undef_array_at_missing_i_rec x ty i lo hi n =
    match num_of_int n with
    | 0 -> false
    | SUC m -> ( fact(i == lo) ** undef_array_at_rec x ty (lo + &1) hi (&m) ) ||
               ( fact(i > lo) ** undef_data_at (x + lo * sizeof(ty)) ty ** undef_array_at_missing_i_rec x ty i (lo + &1) hi (&m) )

!x:addr ty:ctype i:int lo:int hi:int n:int.
  undef_array_at_missing_i_rec x ty i lo hi n =
    match num_of_int n with
    | 0 -> false
    | SUC m -> ( fact(i == lo) ** undef_array_at_rec x ty (lo + &1) hi (&m) ) ||
               ( fact(i > lo) ** undef_data_at (x + lo * sizeof(ty)) ty ** undef_array_at_missing_i_rec x ty i (lo + &1) hi (&m) )

The two undef_undef_ equations split on the count reaching zero rather than on a list being empty, and the recursive occurrence re-enters through &m&m, the integer injection of the predecessor count; the round trip cancels by NUM_OF_INT_OF_NUMNUM_OF_INT_OF_NUM.

All statements in this section are axioms introduced in cstarlib.mlcstarlib.ml; see the provenance note above. Rules whose name contains recrec work on an arbitrary index window lo..hi-1lo..hi-1; the others are the lo = &0lo = &0 specializations that appear in practice.

array_at_lengtharray_at_length (axiom) — an array assertion carries its length.

!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(ilength(l) == n)

!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(ilength(l) == n)

array_at_rec_lengtharray_at_rec_length (axiom) — the same for a window, where the length is the width of the window.

!x ty lo hi l. array_at_rec x ty lo hi l |-- array_at_rec x ty lo hi l ** fact(ilength(l) == hi - lo)

!x ty lo hi l. array_at_rec x ty lo hi l |-- array_at_rec x ty lo hi l ** fact(ilength(l) == hi - lo)

array_at_rangearray_at_range (axiom) — every element is within its type’s range.

!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(!i. &0 <= i ==> i < n ==> (min_of(ty) <= inth i l && inth i l <= max_of(ty)))

!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(!i. &0 <= i ==> i < n ==> (min_of(ty) <= inth i l && inth i l <= max_of(ty)))

These are the rules behind an indexed read or write: split the cell at index nn out of the array, use it, then merge it back — possibly with a new value, which is why the merge rules produce replace_inthreplace_inth.

array_at_splitarray_at_split (axiom) — take out the cell at index nn, leaving an array with a hole.

!x ty n m l. (&0 <= n) ==> (n < m) ==>
  (array_at x ty m l |-- data_at (x + n * sizeof(ty)) ty (inth n l) ** array_at_missing_i_rec x ty n (&0) m l)

!x ty n m l. (&0 <= n) ==> (n < m) ==>
  (array_at x ty m l |-- data_at (x + n * sizeof(ty)) ty (inth n l) ** array_at_missing_i_rec x ty n (&0) m l)

array_at_mergearray_at_merge (axiom) — put a cell back at index nn, updating the list.

!x ty n m a l. (&0 <= n) ==> (n < m) ==>
  (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n (&0) m l |-- array_at x ty m (replace_inth n a l))

!x ty n m a l. (&0 <= n) ==> (n < m) ==>
  (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n (&0) m l |-- array_at x ty m (replace_inth n a l))

array_at_rec_splitarray_at_rec_split (axiom) — the windowed form; note inth (n - lo) linth (n - lo) l, because ll is indexed relative to lolo.

!x ty lo n m l. (lo <= n) ==> (n < m) ==>
  (array_at_rec x ty lo m l |-- data_at (x + n * sizeof(ty)) ty (inth (n - lo) l) ** array_at_missing_i_rec x ty n lo m l)

!x ty lo n m l. (lo <= n) ==> (n < m) ==>
  (array_at_rec x ty lo m l |-- data_at (x + n * sizeof(ty)) ty (inth (n - lo) l) ** array_at_missing_i_rec x ty n lo m l)

array_at_rec_mergearray_at_rec_merge (axiom)

!x ty lo n m a l. (lo <= n) ==> (n < m) ==>
  (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n lo m l |-- array_at_rec x ty lo m (replace_inth (n - lo) a l))

!x ty lo n m a l. (lo <= n) ==> (n < m) ==>
  (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n lo m l |-- array_at_rec x ty lo m (replace_inth (n - lo) a l))

Peeling one element off either end. The recrec forms move the index bound and leave the base address alone; the non-recrec forms move the base address by one element and leave the index origin at &0&0.

array_at_rec_headarray_at_rec_head (axiom) — split off the first element of a window; the remainder is described by sublistsublist.

!x ty lo hi l. (lo < hi) ==>
  (array_at_rec x ty lo hi l |-- data_at (x + lo * sizeof(ty)) ty (inth (&0) l) ** array_at_rec x ty (lo + &1) hi (sublist (&1) (hi - lo) l))

!x ty lo hi l. (lo < hi) ==>
  (array_at_rec x ty lo hi l |-- data_at (x + lo * sizeof(ty)) ty (inth (&0) l) ** array_at_rec x ty (lo + &1) hi (sublist (&1) (hi - lo) l))

array_at_rec_head_mergearray_at_rec_head_merge (axiom) — the converse, producing a cons.

!x ty lo hi a l. (lo < hi) ==>
  (data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l |-- array_at_rec x ty lo hi (a :: l))

!x ty lo hi a l. (lo < hi) ==>
  (data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l |-- array_at_rec x ty lo hi (a :: l))

array_at_array_rec_consarray_at_array_rec_cons (axiom) — the same split stated on a list that is already in cons form, which avoids introducing a sublistsublist.

!x ty lo hi a l. (lo < hi) ==>
  (array_at_rec x ty lo hi (a :: l) |-- data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l)

!x ty lo hi a l. (lo < hi) ==>
  (array_at_rec x ty lo hi (a :: l) |-- data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l)

array_at_rec_tail_mergearray_at_rec_tail_merge (axiom) — extend a window by one element on the right; note the side condition is lo <= hilo <= hi, so an empty window may be extended.

!x ty lo hi a l. (lo <= hi) ==>
  (data_at (x + hi * sizeof(ty)) ty a ** array_at_rec x ty lo hi l |-- array_at_rec x ty lo (hi + &1) (l ++ [a]))

!x ty lo hi a l. (lo <= hi) ==>
  (data_at (x + hi * sizeof(ty)) ty a ** array_at_rec x ty lo hi l |-- array_at_rec x ty lo (hi + &1) (l ++ [a]))

array_at_split_firstarray_at_split_first (axiom) — peel the head off an array_atarray_at, rebasing the remainder one element to the right.

!x ty n v l. (n >= &1) ==> (array_at x ty n (v :: l) |-- data_at x ty v ** array_at (x + sizeof(ty)) ty (n - &1) l)

!x ty n v l. (n >= &1) ==> (array_at x ty n (v :: l) |-- data_at x ty v ** array_at (x + sizeof(ty)) ty (n - &1) l)

array_at_merge_firstarray_at_merge_first (axiom) — the converse; unconditional.

!x ty n v l. data_at x ty v ** array_at (x + sizeof(ty)) ty n l |-- array_at x ty (n + &1) (v :: l)

!x ty n v l. data_at x ty v ** array_at (x + sizeof(ty)) ty n l |-- array_at x ty (n + &1) (v :: l)

array_at_split_lastarray_at_split_last (axiom) — peel the last element off.

!x ty n v l. (n >= &1) ==> (array_at x ty n (l ++ [v]) |-- array_at x ty (n - &1) l ** data_at (x + (n - &1) * sizeof(ty)) ty v)

!x ty n v l. (n >= &1) ==> (array_at x ty n (l ++ [v]) |-- array_at x ty (n - &1) l ** data_at (x + (n - &1) * sizeof(ty)) ty v)

array_at_merge_lastarray_at_merge_last (axiom) — the converse; unconditional.

!x ty n v l. array_at x ty n l ** data_at (x + n * sizeof(ty)) ty v |-- array_at x ty (n + &1) (l ++ [v])

!x ty n v l. array_at x ty n l ** data_at (x + n * sizeof(ty)) ty v |-- array_at x ty (n + &1) (l ++ [v])

Rebasing converts between “same base, shifted window” and “shifted base, same window”. Division cuts an array into two adjacent pieces; all the division rules are equivalences (-|--|-), so they work in both directions.

array_at_rec_basearray_at_rec_base (axiom) — shift the index origin by kk and the base address by kk elements; unconditional.

!x ty m k n l. array_at_rec x ty (m + k) n l -|- array_at_rec (x + k * sizeof(ty)) ty m (n - k) l

!x ty m k n l. array_at_rec x ty (m + k) n l -|- array_at_rec (x + k * sizeof(ty)) ty m (n - k) l

array_at_rec_dividearray_at_rec_divide (axiom) — cut a &0&0-based window at mm.

!x ty m n l. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==>
  (array_at_rec x ty (&0) n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))

!x ty m n l. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==>
  (array_at_rec x ty (&0) n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))

array_at_dividearray_at_divide (axiom) — cut an array_atarray_at at mm; the second piece is rebased to its own start address.

!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==>
  (array_at x ty n l -|- array_at x ty m (sublist (&0) m l) ** array_at (x + m * sizeof(ty)) ty (n - m) (sublist m n l))

!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==>
  (array_at x ty n l -|- array_at x ty m (sublist (&0) m l) ** array_at (x + m * sizeof(ty)) ty (n - m) (sublist m n l))

array_at_divide2array_at_divide2 (axiom) — the same cut expressed on an appended list, which is the convenient direction when the two halves already have names.

!x ty n m l1 l2. (ilength(l1) == n) ==> (ilength(l2) == m) ==>
  (array_at x ty (n + m) (l1 ++ l2) -|- array_at x ty n l1 ** array_at (x + n * sizeof(ty)) ty m l2)

!x ty n m l1 l2. (ilength(l1) == n) ==> (ilength(l2) == m) ==>
  (array_at x ty (n + m) (l1 ++ l2) -|- array_at x ty n l1 ** array_at (x + n * sizeof(ty)) ty m l2)

array_at_divide_recarray_at_divide_rec (axiom) — cut an array_atarray_at into two windows on the same base address, which is the form loop invariants over index ranges want.

!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==>
  (array_at x ty n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))

!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==>
  (array_at x ty n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))

A more general division on an arbitrary window is available as array_at_rec_divide_auxarray_at_rec_divide_aux (axiom), of which array_at_rec_dividearray_at_rec_divide is the lo = &0lo = &0 case:

!x ty lo m n l. (lo <= m) ==> (m <= n) ==> (ilength(l) == n - lo) ==>
  (array_at_rec x ty lo n l -|- array_at_rec x ty lo m (sublist (&0) (m - lo) l) ** array_at_rec x ty m n (sublist (m - lo) (n - lo) l))

!x ty lo m n l. (lo <= m) ==> (m <= n) ==> (ilength(l) == n - lo) ==>
  (array_at_rec x ty lo n l -|- array_at_rec x ty lo m (sublist (&0) (m - lo) l) ** array_at_rec x ty m n (sublist (m - lo) (n - lo) l))

array_at_zeroarray_at_zero (axiom) — a zero-length array is the empty heap.

!x ty n l. (n == &0) ==> (l == []) ==> (array_at x ty n l -|- emp)

!x ty n l. (n == &0) ==> (l == []) ==> (array_at x ty n l -|- emp)

undef_array_at_zeroundef_array_at_zero (axiom)

!x ty n. (n == &0) ==> (undef_array_at x ty n -|- emp)

!x ty n. (n == &0) ==> (undef_array_at x ty n -|- emp)

Neither rule constrains xx: an empty array carries no ownership and therefore no validity condition.

The undef_undef_ rules mirror the initialized ones, minus everything that mentions values — no inthinth, no sublistsublist, no length fact, only element counts.

undef_array_at_divideundef_array_at_divide (axiom) — cut an uninitialized array at mm.

!x ty n m. (&0 <= m) ==> (m <= n) ==>
  (undef_array_at x ty n -|- undef_array_at x ty m ** undef_array_at (x + m * sizeof(ty)) ty (n - m))

!x ty n m. (&0 <= m) ==> (m <= n) ==>
  (undef_array_at x ty n -|- undef_array_at x ty m ** undef_array_at (x + m * sizeof(ty)) ty (n - m))

undef_array_at_split_firstundef_array_at_split_first (axiom)

!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty (n - &1))

!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty (n - &1))

undef_array_at_merge_firstundef_array_at_merge_first (axiom)

!x ty n. undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty n |-- undef_array_at x ty (n + &1)

!x ty n. undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty n |-- undef_array_at x ty (n + &1)

undef_array_at_split_lastundef_array_at_split_last (axiom)

!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_array_at x ty (n - &1) ** undef_data_at (x + (n - &1) * sizeof(ty)) ty)

!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_array_at x ty (n - &1) ** undef_data_at (x + (n - &1) * sizeof(ty)) ty)

undef_array_at_merge_lastundef_array_at_merge_last (axiom)

!x ty n. undef_array_at x ty n ** undef_data_at (x + n * sizeof(ty)) ty |-- undef_array_at x ty (n + &1)

!x ty n. undef_array_at x ty n ** undef_data_at (x + n * sizeof(ty)) ty |-- undef_array_at x ty (n + &1)

undef_array_at_rec_baseundef_array_at_rec_base (axiom) — rebasing for the windowed form.

!x ty m k n len. undef_array_at_rec x ty (m + k) n len -|- undef_array_at_rec (x + k * sizeof(ty)) ty m (n - k) len

!x ty m k n len. undef_array_at_rec x ty (m + k) n len -|- undef_array_at_rec (x + k * sizeof(ty)) ty m (n - k) len

undef_Tuchar_array_at_splitundef_Tuchar_array_at_split (axiom) — carve a typed cell out of a raw byte buffer. This is the rule that turns an untyped block of bytes, the shape an allocation specification naturally hands back, into typed uninitialized storage. It is the only array rule that changes the element type.

!x ty n. n >= sizeof(ty) ==>
  (undef_array_at x Tuchar n -|- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) Tuchar (n - sizeof(ty)))

!x ty n. n >= sizeof(ty) ==>
  (undef_array_at x Tuchar n -|- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) Tuchar (n - sizeof(ty)))

Array assertions carry a list of element values, and the rules above rearrange those lists. The list functions come from cst_predefined.mlcst_predefined.ml and are integer-indexed wrappers around HOL Light’s numnum-indexed list recursions, converted with num_of_intnum_of_int.

ilength [] = &0 /\ ilength ((h:A) :: t) = &1 + ilength t
inth (n:int) (l:(A)list) = NTH (num_of_int n) l
replace_inth (n:int) (a:A) (l:(A)list) = REPLACE_NTH (num_of_int n) a l
ifirstn (n:int) (l:(A)list) = FIRSTN (num_of_int n) l
iskipn (n:int) (l:(A)list) = SKIPN (num_of_int n) l
ireplicate (n:int) (v:A) = REPLICATE (num_of_int n) v
sublist (lo:int) (hi:int) (l:(A)list) = SKIPN (num_of_int lo) (FIRSTN (num_of_int hi) l)

ilength [] = &0 /\ ilength ((h:A) :: t) = &1 + ilength t
inth (n:int) (l:(A)list) = NTH (num_of_int n) l
replace_inth (n:int) (a:A) (l:(A)list) = REPLACE_NTH (num_of_int n) a l
ifirstn (n:int) (l:(A)list) = FIRSTN (num_of_int n) l
iskipn (n:int) (l:(A)list) = SKIPN (num_of_int n) l
ireplicate (n:int) (v:A) = REPLICATE (num_of_int n) v
sublist (lo:int) (hi:int) (l:(A)list) = SKIPN (num_of_int lo) (FIRSTN (num_of_int hi) l)

In one line each:

• ilength lilength l — the length of ll as an intint.
• inth n linth n l — the element at index nn, counting from &0&0.
• replace_inth n a lreplace_inth n a l — ll with the element at index nn replaced by aa; the list is returned unchanged if the index is out of range.
• ifirstn n lifirstn n l — the first nn elements (all of ll if nn is too large).
• iskipn n liskipn n l — ll with the first nn elements dropped.
• ireplicate n vireplicate n v — the list of nn copies of vv.
• sublist lo hi lsublist lo hi l — elements at indices lo..hi-1lo..hi-1: take the first hihi, then drop the first lolo. The half-open convention matches array_at_recarray_at_rec.
• l1 ++ l2l1 ++ l2 — HOL Light’s APPENDAPPEND.

Four are proved in cst_predefined.mlcst_predefined.ml; the two about ireplicateireplicate are axioms in cstarlib.mlcstarlib.ml.

ILENGTH_NONNEGILENGTH_NONNEG (proved)

!l:(A)list. &0 <= ilength l

!l:(A)list. &0 <= ilength l

ILENGTH_APPENDILENGTH_APPEND (proved)

!l1:(A)list l2:(A)list. ilength(l1 ++ l2) = ilength(l1) + ilength(l2)

!l1:(A)list l2:(A)list. ilength(l1 ++ l2) = ilength(l1) + ilength(l2)

ISKIPN_SPLIT_FIRSTISKIPN_SPLIT_FIRST (proved) — the head of a suffix is the element at that index; the step that drives index-by-index loops.

!i:int l:(A)list. &0 <= i /\ i < ilength l ==> (iskipn i l = CONS (inth i l) (iskipn (i + &1) l))

!i:int l:(A)list. &0 <= i /\ i < ilength l ==> (iskipn i l = CONS (inth i l) (iskipn (i + &1) l))

ISKIPN_ILENGTHISKIPN_ILENGTH (proved) — dropping everything leaves the empty list, which is how a loop over an array is shown to terminate with nothing left.

!l:(A)list. iskipn (ilength(l)) l = []

!l:(A)list. iskipn (ilength(l)) l = []

ILENGTH_IREPLICATEILENGTH_IREPLICATE (axiom)

!n:int v:A. &0 <= n ==> ilength(ireplicate n v) == n

!n:int v:A. &0 <= n ==> ilength(ireplicate n v) == n

IREPLICATE_APPENDIREPLICATE_APPEND (axiom)

!n:int v:A. (ireplicate n v) ++ [v] == ireplicate (n + &1) v

!n:int v:A. (ireplicate n v) ++ [v] == ireplicate (n + &1) v

Most proofs never apply the array rules by name. They are the lemmas that strategies encode: a strategy file pattern-matches an entailment, applies one of these rules, and repeats, so that the frame inference at an array read or write happens automatically. See Purifying Entailments with Strategies for the array strategies of strategy_demo/array/strategy_demo/array/, including the checkcheck-guarded rules that establish the &0 <= i&0 <= i and i < ni < n side conditions the split rules require before firing.

When a step is too specific for a strategy — a bespoke resource rearrangement with a proof obligation attached — the same rules are applied through the operational route instead, as one named operation per rearrangement; see Operations.

• The typed predicates are a four-layer stack: single_byte_memsingle_byte_mem in the model, mstoremstore/mstore_noninitmstore_noninit as one-byte heap propositions, store_2bytestore_2byte/store_4bytestore_4byte/store_8bytestore_8byte assembling bytes little-endian through merge_shortmerge_short/merge_intmerge_int/merge_int64merge_int64, and typed stores adding validity and range as pure(…) && …pure(…) && ….
• mstoremstore is insensitive to a value’s representation modulo 256; signedness enters only through the range condition of the typed store.
• Validity is bounds plus alignment (aligned_naligned_n), stated on the object’s last byte. It does not exclude the null address.
• cast_unsigned n z = z rem exp_2 ncast_unsigned n z = z rem exp_2 n uses Euclidean remainder, so it truncates to the low nn bits for negative zz as well; cast_signedcast_signed reinterprets the top bit.
• data_atdata_at and undef_data_atundef_data_at dispatch on ctypectype over the nine scalar types. There is no TstructTstruct clause; struct_atstruct_at is declared but unaxiomatized.
• Element ii of an array lives at x + i * sizeof(ty)x + i * sizeof(ty); array_at_rec x ty lo hi larray_at_rec x ty lo hi l covers indices lo..hi-1lo..hi-1 with ll relative to lolo, and array_atarray_at is the lo = &0lo = &0 case.
• The four data_atdata_at rules and the thirty array rules are new_axiomnew_axiom in cstarlib.mlcstarlib.ml — assumed, not derived — while the store-layer lemmas and the match-form unfoldings are proved.