Typed Memory Predicates

The memory model represents a heap as individual bytes; C* specifications describe C objects. The ctype-indexed data_atdata_at and array_atarray_at families connect the two and appear in every C* specification. This page describes their guarantees about addresses and values, the validity, range, and cast functions used to state those guarantees, and the rules the proof engine uses to split and recombine these assertions.

For the underlying heap and the separation-logic connectives used below (****, &&&&, ||||, purepure, factfact, empemp, existsexists, |--|--, -|--|-), see Memory Model and Assertions.

For a modeled scalar type or a transparent alias of one, data_at x ty vdata_at x ty v says that the bytes starting at xx are owned and hold the value vv when read as the C type tyty. The assertion provides three guarantees, which the rules on this page use:

• the address is valid and aligned for the type — the object fits in the address space and xx is a multiple of the type’s width, as expressed by the isvalidptr_*isvalidptr_* predicates below;
• exactly sizeof tysizeof ty consecutive bytes are owned, so two data_atdata_at assertions at the same address contradict each other, and adjacent cells compose with **** into arrays;
• the value is in range — min_of ty <= v /\ v <= max_of tymin_of ty <= v /\ v <= max_of ty.

data_atdata_at selects a typed store according to the scalar type tyty. Each typed store is a fixed-width byte store conjoined with the pure conditions that make it a legal C object of that type. The byte store represents vv in little-endian order using sizeof tysizeof ty bytes, each owned individually. This page does not unfold the byte store further; none of the rules below requires it. For opaque compound types, only the general laws stated later apply; no unfolding equation specifies their byte layout or address validity.

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; store_4byte_noninit xstore_4byte_noninit x owns the same four bytes without specifying their contents:

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)

Validity requires both an address-space bound and an alignment condition. Alignment means 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. Neither validity nor ownership implies non-nullness in this model: data_atdata_at at address &0&0 is not contradictory by itself. Specifications that require non-nullness must state it explicitly.

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 lies 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 theorems:

cast_unsigned_boundcast_unsigned_bound

!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

!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 lemmas state that the casts preserve the remainder 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.

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_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_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 or corresponding constant for the other widths: the unsigned lower bound is written as &0&0 wherever 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 | Tenum string | Tunion string |
        Talias string ctype | Tarray int ctype |
        Tfun (string)list (ctype)list ctype

ctype = Tchar  | Tuchar  |
        Tshort | Tushort |
        Tint   | Tuint   |
        Tint64 | Tuint64 |
        Tptr   |
        Tstruct string | Tenum string | Tunion string |
        Talias string ctype | Tarray int ctype |
        Tfun (string)list (ctype)list ctype

The predicates below dispatch on the nine scalar constructors. The compound constructors, apart from TaliasTalias, are opaque: TstructTstruct, TenumTenum and TunionTunion carry only the C tag name, and no clause of any predicate mentions them. Talias name tyTalias name ty is a typedeftypedef of tyty, and every function below processes its underlying type. Tarray n tyTarray n ty is an array of nn elements. TfunTfun records a C function signature — parameter names, parameter types, result type — and appears only inside the function-pointer specifications described below.

For scalar storage and transparent aliases, data_at x ty vdata_at x ty v is the typed store selected by tyty. It has nine clauses for the scalar ctypes and one for the underlying type of a typedeftypedef:

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 (Talias name ty) v = data_at x ty 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 /\
data_at x (Talias name ty) v = data_at x ty 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.

For these same types, the dispatch selects an uninitialized store, asserting ownership of the required number of bytes at a valid, aligned address without constraining their 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 (Talias name ty) = undef_data_at x ty

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 (Talias name ty) = undef_data_at x ty

Two more constants use the TfunTfun constructor. They are opaque markers: the theory gives them no definition, and the symbolic engine interprets them as function specifications:

fnspec   : addr->ctype->hprop->hprop->hprop
fnspec_w : addr->ctype->(A->hprop)->(A->hprop)->hprop

fnspec   : addr->ctype->hprop->hprop->hprop
fnspec_w : addr->ctype->(A->hprop)->(A->hprop)->hprop

fnspec f ty pre postfnspec f ty pre post says that the function at address ff, whose C signature is the TfunTfun ctype tyty, satisfies the contract prepre / postpost, in which the TfunTfun parameter names and __return__return occur free. fnspec_wfnspec_w adds ghost parameters as one lambda binder shared by prepre and postpost (\(a,n). …\(a,n). … for several). A function pointer itself is an ordinary TptrTptr value, which is why data_atdata_at, min_ofmin_of and max_ofmax_of have no TfunTfun clause: TfunTfun occurs only inside these two applications.

Each scalar ctype has a size in bytes and a value range. The array rules use these three functions for address arithmetic and value bounds.

min_ofmin_of of every unsigned type and of TptrTptr is &0&0; the other entries are the width bounds of the “Width instantiations” section above (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). min_of_defmin_of_def and max_of_defmax_of_def give the numerals directly, with one equation per scalar constructor, for use in rewriting:

min_of_defmin_of_def, max_of_defmax_of_def — the numeric values, as a conjunction of equations.

max_of Tchar   = &127 /\
max_of Tuchar  = &255 /\
max_of Tshort  = &32767 /\
max_of Tushort = &65535 /\
max_of Tint    = &2147483647 /\
max_of Tuint   = &4294967295 /\
max_of Tint64  = &9223372036854775807 /\
max_of Tuint64 = &18446744073709551615 /\
max_of Tptr    = &18446744073709551615 /\
(!name ty. max_of (Talias name ty) = max_of ty)

max_of Tchar   = &127 /\
max_of Tuchar  = &255 /\
max_of Tshort  = &32767 /\
max_of Tushort = &65535 /\
max_of Tint    = &2147483647 /\
max_of Tuint   = &4294967295 /\
max_of Tint64  = &9223372036854775807 /\
max_of Tuint64 = &18446744073709551615 /\
max_of Tptr    = &18446744073709551615 /\
(!name ty. max_of (Talias name ty) = max_of ty)

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, and the same TaliasTalias pass-through. Neither has an equation for TstructTstruct, TenumTenum, TunionTunion, TarrayTarray or TfunTfun, so min_ofmin_of and max_ofmax_of of those types stay opaque. Each conjunct is an equation about one constructor, so rewriting with the whole theorem applies directly to min_of Tintmin_of Tint.

sizeofsizeof is introduced by specification. The equations in sizeof_defsizeof_def comprise the nine scalar clauses in the table above and two more: sizeof(Tfun fnamel tyl retty) = 8isizeof(Tfun fnamel tyl retty) = 8i, a function pointer being pointer-sized, and sizeof(Talias name ty) = sizeof tysizeof(Talias name ty) = sizeof ty. There is no equation for TstructTstruct, TenumTenum, TunionTunion or TarrayTarray; a struct’s size and layout are not modelled in the theory, in keeping with field_offsetfield_offset being left uninterpreted. The other half of the specification is the one fact that holds at every ctypectype:

sizeof_ge_0sizeof_ge_0 — 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 — 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 — a data_atdata_at cell carries its type’s value range as a pure fact while preserving ownership of 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 — 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 — 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 from memory: the fact(…)fact(…) conjunct is a pure proposition retained in the part of a goal handled by SMT. data_at_dupdata_at_dup supports most proofs that two pointers must differ: assume they are equal and derive falsefalse.

Two further rules, both proved, expose the byte layout of one cell: a 4-byte unsigned cell describes the same memory as four 1-byte unsigned cells whose values combine in little-endian order. The relation between the bytes and the value is merge_intmerge_int, which constrains only the low 32 bits of vv and the low 8 bits of each byte:

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

data_at_Tuint_Tuchardata_at_Tuint_Tuchar — split a TuintTuint cell into its four bytes, low byte first; the alignment of xx and the range of vv are returned as facts.

!x v. data_at x Tuint v |--
  exists v1 v2 v3 v4.
    fact(merge_int v1 v2 v3 v4 v) **
    fact(&0 <= v && v <= int_max_unsigned) **
    fact(aligned_n (&4) x) **
    data_at x Tuchar v1 **
    data_at (x + &1) Tuchar v2 **
    data_at (x + &2) Tuchar v3 **
    data_at (x + &3) Tuchar v4

!x v. data_at x Tuint v |--
  exists v1 v2 v3 v4.
    fact(merge_int v1 v2 v3 v4 v) **
    fact(&0 <= v && v <= int_max_unsigned) **
    fact(aligned_n (&4) x) **
    data_at x Tuchar v1 **
    data_at (x + &1) Tuchar v2 **
    data_at (x + &2) Tuchar v3 **
    data_at (x + &3) Tuchar v4

data_at_Tuchar_Tuintdata_at_Tuchar_Tuint — the converse: four adjacent bytes at a 4-aligned address, together with their combined value and its range, form a TuintTuint cell.

!x v1 v2 v3 v4 v.
  fact(merge_int v1 v2 v3 v4 v) **
  fact(&0 <= v && v <= int_max_unsigned) **
  fact(aligned_n (&4) x) **
  data_at x Tuchar v1 **
  data_at (x + &1) Tuchar v2 **
  data_at (x + &2) Tuchar v3 **
  data_at (x + &3) Tuchar v4 |--
  data_at x Tuint v

!x v1 v2 v3 v4 v.
  fact(merge_int v1 v2 v3 v4 v) **
  fact(&0 <= v && v <= int_max_unsigned) **
  fact(aligned_n (&4) x) **
  data_at x Tuchar v1 **
  data_at (x + &1) Tuchar v2 **
  data_at (x + &2) Tuchar v3 **
  data_at (x + &3) Tuchar v4 |--
  data_at x Tuint v

These rules support reading a word from a byte buffer or writing one into it without an uninitialized intermediate state.

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

array_at_recarray_at_rec is defined by recursion on the list ll, one data_atdata_at per element at x + i * sizeof(ty)x + i * sizeof(ty); its unfolding is array_at_rec_defarray_at_rec_def below. A second predicate describes the same window with one cell removed.

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. Thus, after putting the cell back with a different value, the updated list can be expressed using replace_inthreplace_inth.

The undef_undef_ family — undef_array_at_rec x ty lo hi nundef_array_at_rec x ty lo hi n and its holed form undef_array_at_missing_i_rec x ty i lo hi nundef_array_at_missing_i_rec x ty i lo hi n — owns the same addresses but says nothing about contents. Because there is no list to recurse on, these predicates recurse on the element count nn, passed as an intint:

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 following match-form equations unfold the four predicates and serve as rewriting rules.

array_at_rec_defarray_at_rec_def

!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

!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

!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

!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. Each recursive call passes &m&m, the integer injection of the predecessor count.

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

An indexed read or write uses these rules to split the cell at index nn from the array and merge it back after use. The value may have changed, so the merge rules use replace_inthreplace_inth to describe the updated list.

array_at_splitarray_at_split — 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 — 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 — 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

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

These rules split off one element at either end. The recrec forms move the index bound and preserve the base address; 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 — 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 — 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 — 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 — 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 — split the head from 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 — 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 — split off the last element.

!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 — 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 a shift in the index window into a shift in the base address, and vice versa. Division splits an array into two adjacent pieces; all division rules are equivalences (-|--|-), so they work in both directions.

array_at_rec_basearray_at_rec_base — 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 — 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 — 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 — the same cut expressed on an appended list, which is convenient when both 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 — cut an array_atarray_at into two windows on the same base address, a form used in loop invariants over index ranges.

!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, 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 — 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

!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 but omit the parts that mention values: inthinth, sublistsublist, and length facts. They use only element counts.

undef_array_at_divideundef_array_at_divide — 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

!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

!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

!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

!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 — 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 — split a typed cell from a raw byte buffer. This rule converts an untyped block of bytes, as typically returned by an allocation specification, into typed uninitialized storage. It is the only array rule that changes the element type.

!x ty n. is_scalar_ctype ty ==> aligned_n (sizeof(ty)) x ==> 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. is_scalar_ctype ty ==> aligned_n (sizeof(ty)) x ==> 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 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)

The operations have the following meanings:

• 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.

ILENGTH_NONNEGILENGTH_NONNEG

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

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

ILENGTH_APPENDILENGTH_APPEND

!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 — the head of a suffix is the element at that index; this rule supports loops that advance one index at a time.

!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 — dropping all elements leaves the empty list. This establishes that no elements remain when traversal completes; it does not prove termination.

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

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

ILENGTH_IREPLICATEILENGTH_IREPLICATE

!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

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

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

Both ireplicateireplicate facts carry the &0 <= n&0 <= n guard because ireplicateireplicate goes through num_of_intnum_of_int, which is unspecified on negative integers.

Most proofs do not apply the array rules by name. Instead, strategies encode these lemmas: a strategy file repeatedly pattern-matches an entailment and applies a rule, automating frame inference at array reads and writes. 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, such as a custom resource rearrangement with an associated proof obligation, operational proofs apply the same rules through one named operation per rearrangement; see Operations.

• For modeled scalar storage and transparent aliases, data_at x ty vdata_at x ty v guarantees a valid, aligned address, ownership of exactly sizeof tysizeof ty bytes, and min_of ty <= v <= max_of tymin_of ty <= v <= max_of ty; the typed store it unfolds to has the shape pure(…) && …pure(…) && …, with validity and range in the pure part and a little-endian byte store in the spatial part.
• Validity is bounds plus alignment (aligned_naligned_n), stated on the object’s last byte. Neither validity nor ownership excludes the null address; specifications that require non-nullness must state it explicitly.
• 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, looking through TaliasTalias. There is no clause for the compound constructors (TstructTstruct, TenumTenum, TunionTunion, TarrayTarray, TfunTfun); struct fields are separate cells at field_addrfield_addr.
• fnspecfnspec and fnspec_wfnspec_w state a function pointer’s contract against its TfunTfun signature; their meaning is given by the engine rather than the theory.
• Element ii of an array is 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.
• Every rule on this page is a proved theorem, and the library adds no axioms. sizeofsizeof, data_atdata_at and undef_data_atundef_data_at are specified rather than defined, so on TstructTstruct, TenumTenum, TunionTunion and TarrayTarray (and, for the two data_atdata_ats, TfunTfun) only sizeof_ge_0sizeof_ge_0 and the four data_atdata_at laws are known.