Typed Memory Predicates

The memory model provides a heap of individual bytes; C* specifications talk about C objects. This page specifies the ctype-indexed data_atdata_at and array_atarray_at families that connect the two and appear in every C* specification — what a typed cell guarantees about its address and its value, the validity, range and cast functions those guarantees are stated with — together with the rules the proof engine uses to take those assertions apart and put them back together.

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

data_at x ty vdata_at x ty v says that the bytes starting at xx are owned and hold the value vv, read at the C type tyty. Three guarantees are built into the assertion, and the rules on this page are stated in terms of them:

• 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 (the isvalidptr_*isvalidptr_* predicates below);
• exactly sizeof tysizeof ty consecutive bytes are owned — which is why two data_atdata_at at the same address are contradictory, and why 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 dispatches on tyty to one typed store per scalar type, and 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 byte store itself is the little-endian representation of vv in sizeof tysizeof ty bytes, each byte owned individually; this page does not unfold it further, and no rule below needs it to be unfolded.

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

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 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 | 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 nine scalar constructors are the ones the predicates below dispatch on. The compound ones, TaliasTalias aside, 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 passes through it. 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.

data_at x ty vdata_at x ty v is the typed store selected by tyty. Nine clauses, one per scalar ctype, plus one that looks through 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.

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 (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. These three functions are what the array rules use to do address arithmetic and to state 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, one equation per scalar constructor, and are the form a proof rewrites with:

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. Because every conjunct is an equation about one constructor, rewriting with the whole theorem fires on min_of Tintmin_of Tint directly.

sizeofsizeof is introduced by specification, and sizeof_defsizeof_def is its equational half: the nine scalar clauses of 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, 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 — 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 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.

Two further rules, both proved, expose the byte layout of one cell: a 4-byte unsigned cell is the same memory as four 1-byte unsigned cells whose values combine little-endian. 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 come out 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 a value they merge to 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 are the rules behind reading a word out of a byte buffer, or writing one into it, without going through an uninitialized intermediate.

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 — 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 — 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 four predicates unfold by the following match-form equations, which are the practical 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, and the recursive occurrence re-enters through &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)))

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

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 — 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 — 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 — 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 — 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 — 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 — 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 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 — 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, 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, minus everything that mentions values — no inthinth, no sublistsublist, no length fact, 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 — 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. 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)

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.

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

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

• 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(…) && …, 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. 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, 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 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.
• 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.