带类型的内存谓词

内存模型提供的是一个由单个字节构成的堆，而 C* 规约谈论的是 C 对象。本页给出连接 二者的定义链条——单字节所有权、按小端序合并为 2 字节、4 字节和 8 字节单元、为每种 类型补上有效性与范围附加条件的带类型存储，最后是出现在每一份 C* 规约中的、以 ctype 为索引的 data_atdata_at 与 array_atarray_at 谓词族——并一并给出证明引擎用来拆解和重组 这些断言的规则。

这些定义位于服务器库的 cst_interface.mlcst_interface.ml 和 cst_predefined.mlcst_predefined.ml 中；导出引理在 cst_aux.mlcst_aux.ml 中； 面向用户的规则在 cstarlib.mlcstarlib.ml 中引入。关于底层的堆以及下文用到的分离逻辑连接词 （****、&&&&、||||、purepure、factfact、empemp、existsexists、|--|--、-|--|-），参见 内存模型与断言。

带类型的内存谓词分四层构建。每一层都是定义而非公理：本节的一切最终都会展开为 内存模型中字节级内存上的谓词。

mstoremstore 与 mstore_noninitmstore_noninit 把模型中的单单元内存 （single_byte_memsingle_byte_mem、single_noninit_memsingle_noninit_mem）提升为堆命题。

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

这里已经可以看出两点。

第一，mstore p vmstore p v 并不精确锁定 vv：只要单字节内存中存放的 v'v' 与 vv 字节等价，也就是模 同余，该断言就成立。存入 --&1--&1 与存入 &255&255 得到的是同一个断言。正是这种模 256 的等价关系使得字节层对“某个字节按有符号还是 无符号读取”不敏感；符号性由上一层施加，即带类型存储的范围条件。

第二，mstore_noninit pmstore_noninit p 表达的断言是“我拥有 pp 处的字节，但对其内容不作任何承诺”： 该单元可能确实未初始化，也可能存放着某个断言拒绝指明的值。它是整个 undef_undef_ 谓词族在字节层的源头。

byte_eqmbyte_eqm 是位宽为 8 的 eqmeqm，而 eqmeqm 是模 2 的幂的同余关系。

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)

mstoremstore 中模 256 的松弛给出一条已证明的蕴含，使得任意两个字节等价的值可以在 store_bytestore_byte 下互换：

store_byte_vstore_byte_v（已证明）——字节等价的值指称同一个字节单元。

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

更宽的单元由小端序的合并关系从字节组装而成。merge_short z1 z2 vmerge_short z1 z2 v 表示字节对 z1z1、z2z2——低字节在前——在 16 位宽下表示 vv；merge_intmerge_int 与 merge_int64merge_int64 在 32 位和 64 位宽下表达同样的意思。每条关系都写成关于余数的等式，因此它只约束 vv 的低位，以及每个 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 与 store_byte_noninitstore_byte_noninit 就是换了个名字的 mstoremstore 与 mstore_noninitmstore_noninit； 更宽的存储则对各个组成字节施加存在量词，并用合并关系把它们与值联系起来。

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 是类型缩写 :model->bool:model->bool，hprophprop 指的也是同一个类型。）

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 的形状相同，只是用八个字节和 merge_int64merge_int64。未初始化的对应形式不需要 合并关系，只需拥有相应数量的连续字节：

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)

带类型存储就是定宽字节存储与那些使之成为该类型合法 C 对象的纯条件的合取：地址 必须是该类型下有效且正确对齐的指针，值必须落在该类型的范围之内。

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

九种带类型存储及其未初始化形式：

每种存储还断言与其位宽相应的有效性谓词——1 字节存储用 isvalidptr_charisvalidptr_char， 2 字节用 isvalidptr_shortisvalidptr_short，4 字节用 isvalidptr_intisvalidptr_int，8 字节用 isvalidptr_int64isvalidptr_int64， store_ptrstore_ptr 用 isvalidptrisvalidptr。未初始化形式保留有效性条件而去掉范围条件，因为此时 没有值需要约束：

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)

以下都是模型的普通定理，不是公理。它们正是分层带来的收益。

• store_char_rangestore_char_range、store_uchar_rangestore_uchar_range、…、store_ptr_rangestore_ptr_range（已证明）——每种 带类型存储都蕴含其范围条件这一纯命题，例如 !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（已证明）——带类型 存储蕴含其未初始化形式：!p v. store_int p v |-- undef_store_int p!p v. store_int p v |-- undef_store_int p。 它们建立在 store_byte_store_byte_noinitstore_byte_store_byte_noinit 及其 2、4、8 字节的提升之上。
• dup_mstoredup_mstore、dup_mstore_noninitdup_mstore_noninit、dup_store_byte_noninitdup_store_byte_noninit（已证明）——一个字节 不能被拥有两次：!p v1 v2. mstore p v1 ** mstore p v2 |-- hfalse!p v1 v2. mstore p v1 ** mstore p v2 |-- hfalse。 这是下文 data_at_dupdata_at_dup 规则背后的模型层事实。
• 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（已证明）——一个 4 字节单元等价于四个 1 字节单元 加上合并关系、对齐事实和范围事实；这是存储层的字节重解释规则，在 data_atdata_at 层对应的是 data_at_Tuint_Tuchardata_at_Tuint_Tuchar 与 data_at_Tuchar_Tuintdata_at_Tuchar_Tuint。

有效性是地址空间的界与对齐条件的合取；对齐则是模所需字节数与零同余。

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)

这个界是就对象最后一个字节的地址给出的，因此一个 intint 对象必须完整地落在 64 位地址空间之内。注意 &0 <= x&0 <= x 是一个下界，而不是非空条件：空地址满足上述每一个 谓词。指针的非空性是另一条独立的事实，实践中它来自对被指对象的所有权——地址 &0&0 处的 data_atdata_at 本身并不矛盾，只是那些需要非空性的规约会把它明确写出来。

exp_2exp_2 是 2 的整数次幂；各个界常量由它导出，而转换则是欧几里得取余运算。

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 中整数上的 remrem 是欧几里得取余：对正模数而言余数总是非负的。因此对 任意 zz（包括负数），cast_unsigned n zcast_unsigned n z 都落在 之内——它是 截取低 nn 位，而不是 C 的 %% 运算符。随后 cast_signedcast_signed 在截断后的值不小于 时减去 ，从而重新解释最高位。这两点都已证明：

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

另有两条已证明的引理说明这些转换在模 意义下是透明的—— cast_unsigned_remcast_unsigned_rem 与 cast_signed_remcast_signed_rem 都断言 cast_* n v rem exp_2 n = v rem exp_2 ncast_* n v rem exp_2 n = v rem exp_2 n——由此在位宽 8 上得到 cast_unsigned_byte_eqmcast_unsigned_byte_eqm 与 cast_signed_byte_eqmcast_signed_byte_eqm。

带类型存储中用到的具名常量，是 max_unsignedmax_unsigned、max_signedmax_signed 和 min_signedmin_signed 在位宽 8、16、32、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)

并没有 byte_min_unsignedbyte_min_unsigned 之类的常量：无符号类型的下界在需要的地方一律直接写作 &0&0。

data_atdata_at 按 ctypectype 分派，后者是 C 类型的数据类型：

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

TstructTstruct 依次携带结构体的名字、字段名和字段类型。

data_at x ty vdata_at x ty v 就是由 tyty 选出的带类型存储。共九条子句，每种标量 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

每条子句中值参数都是 intint，TptrTptr 也不例外：在这个模型里地址就是整数，因此指针值 单元与 int64int64 值单元的区别仅在于各自的有效性条件与范围条件。

在未初始化存储上做同样的分派——在有效且对齐的地址上拥有相应数量的字节，而对内容 不作任何声称：

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

每种标量 ctype 都有以字节计的大小和一个取值范围。数组规则正是用这三个函数来做 地址算术、并陈述各种界的。

min_ofmin_of 与 max_ofmax_of 是用具名的位宽常量定义的——min_of(Tint) = int_min_signedmin_of(Tint) = int_min_signed、 max_of(Tuint) = int_max_unsignedmax_of(Tuint) = int_max_unsigned，依此类推，其中所有无符号类型以及 TptrTptr 的 min_ofmin_of 都等于 &0&0。上表中的数字来自两条 match 形式的公理，它们把那些常量一次性 求值出来：

min_of_defmin_of_def、max_of_defmax_of_def（公理）——以 match 形式给出的数值。

!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 的形状与之相同，取值依次为 --(&128)--(&128)、&0&0、--(&32768)--(&32768)、&0&0、 --(&2147483648)--(&2147483648)、&0&0、--(&9223372036854775808)--(&9223372036854775808)、&0&0、&0&0。两条公理都没有 TstructTstruct 情形，因此结构体类型的 min_ofmin_of 与 max_ofmax_of 保持不透明。

sizeofsizeof 由与 sizesofsizesof 的互递归定义，随后被赋予一个直接的刻画 sizeof_defsizeof_def （已证明），其结构体子句是 sizeof(Tstruct name fnamel tyl) = ITLIST (+) (MAP sizeof tyl) 0isizeof(Tstruct name fnamel tyl) = ITLIST (+) (MAP sizeof tyl) 0i——即各字段大小 之和，不含填充。另有一条事实是公理：

sizeof_ge_0sizeof_ge_0（公理）——大小非负。

!ty:ctype. sizeof ty >= &0

!ty:ctype. sizeof ty >= &0

data_at_to_undef_data_atdata_at_to_undef_data_at（公理）——忘掉值，保留所有权。

!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（公理）——data_atdata_at 单元以纯事实的形式携带其类型的取值范围，而 无需交出该单元。

!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（公理）——一个单元不能被拥有两次。

!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（公理）——未初始化单元同样不能。

!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：其中的 fact(…)fact(…) 合取项是一条纯命题，会一直保留到目标中面向 SMT 的部分。data_at_dupdata_at_dup 则是大多数 “这两个指针必然不同”论证的来源——假设它们相等，推出 falsefalse。

array_atarray_at 是 lo = &0lo = &0 的特例，几乎每一份规约中出现的都是这种形式：

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

这些递归谓词是通用的“存储数组”组合子的实例，由元素放置函数 \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 是带洞的数组：它拥有范围 lo..hi-1lo..hi-1 中除索引 ii 之外的每一个元素，索引 ii 处的单元已被拆分出去。列表 ll 仍保持整个 范围的完整长度——洞处的值仍在 ll 中，只是相应的内存不再被拥有——正因如此，才可以 把该单元以另一个值放回去，并把结果表述为 replace_inthreplace_inth。

undef_undef_ 谓词族拥有同样的地址，但对内容不作任何声称。由于没有列表可供递归，这些 谓词改为对元素个数递归，该个数以 intint 传入并用 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

注意 undef_array_atundef_array_at 把 nn 传了两次：一次作为索引上界 hihi，一次作为递归计数。 二者一致仅仅是因为 lolo 为 &0&0。

上面的定义是通过通用组合子给出的，直接用它们做改写并不方便。cst_aux.mlcst_aux.ml 证明了 下列 match 形式的等式，它们才是实际使用的展开规则；四条全部是已证明的，而非 假设的。

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

两条 undef_undef_ 等式按计数是否降到零来分情形，而不是按列表是否为空；递归出现处通过 &m&m（前驱计数的整数注入）重新进入，这一往返由 NUM_OF_INT_OF_NUMNUM_OF_INT_OF_NUM 抵消。

本节所有语句都是 cstarlib.mlcstarlib.ml 中引入的公理，参见上文关于来源的说明。名字中含 recrec 的规则作用于任意索引窗口 lo..hi-1lo..hi-1；其余的则是实践中出现的 lo = &0lo = &0 特化形式。

array_at_lengtharray_at_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（公理）——窗口形式的同一规则，此时长度即窗口的宽度。

!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（公理）——每个元素都落在其类型的范围之内。

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

这几条是索引读写背后的规则：把索引 nn 处的单元从数组中拆分出来，使用它，然后再 合并回去——回去时值可能已经改变，这正是合并规则产生 replace_inthreplace_inth 的原因。

array_at_splitarray_at_split（公理）——取出索引 nn 处的单元，留下一个带洞的数组。

!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（公理）——把单元放回索引 nn 处，并更新列表。

!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（公理）——窗口形式；注意其中的 inth (n - lo) linth (n - lo) l，因为 ll 是相对于 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))

从两端各剥离一个元素。recrec 形式移动索引界而基地址不变；非 recrec 形式则把基地址 移动一个元素，索引原点仍留在 &0&0。

array_at_rec_headarray_at_rec_head（公理）——拆分出窗口的第一个元素；剩余部分由 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（公理）——其逆向形式，产生一个 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（公理）——同一个拆分，但陈述在已经是 cons 形式的列表 上，从而避免引入 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（公理）——把窗口向右扩展一个元素；注意附加条件是 lo <= hilo <= hi，因此空窗口也可以扩展。

!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（公理）——从 array_atarray_at 剥离头部，并把剩余部分向右换基 一个元素。

!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（公理）——其逆向形式；无附加条件。

!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（公理）——剥离最后一个元素。

!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（公理）——其逆向形式；无附加条件。

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

换基是在“同一基地址、平移窗口”与“平移基地址、同一窗口”之间转换。划分则把数组切成 两段相邻的部分；所有划分规则都是等价（-|--|-），因此双向都可使用。

array_at_rec_basearray_at_rec_base（公理）——把索引原点平移 kk，同时把基地址平移 kk 个元素； 无附加条件。

!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（公理）——在 mm 处切开一个以 &0&0 为起点的窗口。

!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（公理）——在 mm 处切开一个 array_atarray_at；第二段换基到它自己的 起始地址。

!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（公理）——同一个切分，但表述在拼接后的列表上；当两半已经各有 名字时，这个方向更方便。

!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（公理）——把一个 array_atarray_at 切成同一基地址上的两个窗口， 这正是以索引范围表述的循环不变式所需要的形式。

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

任意窗口上更一般的划分由 array_at_rec_divide_auxarray_at_rec_divide_aux（公理）给出， array_at_rec_dividearray_at_rec_divide 是它 lo = &0lo = &0 的情形：

!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（公理）——长度为零的数组就是空堆。

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

两条规则都不约束 xx：空数组不携带所有权，因而也没有有效性条件。

undef_undef_ 规则与已初始化的规则一一对应，只是去掉了一切涉及值的部分——没有 inthinth， 没有 sublistsublist，也没有长度事实，只有元素个数。

undef_array_at_divideundef_array_at_divide（公理）——在 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（公理）——窗口形式的换基。

!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（公理）——从原始字节缓冲区中切出一个带类型的单元。 分配规约自然交回的形状正是无类型的字节块，这条规则把它转换为带类型的未初始化 存储。它是唯一改变元素类型的数组规则。

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

数组断言携带一个元素值的列表，而上文的规则会重排这些列表。这些列表函数来自 cst_predefined.mlcst_predefined.ml，是对 HOL Light 中以 numnum 为索引的列表递归的整数索引封装， 用 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)

各用一句话概括：

• ilength lilength l——以 intint 表示的 ll 的长度。
• inth n linth n l——索引 nn 处的元素，从 &0&0 开始计数。
• replace_inth n a lreplace_inth n a l——把 ll 中索引 nn 处的元素替换为 aa；若索引超出范围则 原样返回该列表。
• ifirstn n lifirstn n l——前 nn 个元素（若 nn 过大则为整个 ll）。
• iskipn n liskipn n l——去掉前 nn 个元素后的 ll。
• ireplicate n vireplicate n v——由 nn 个 vv 重复构成的列表。
• sublist lo hi lsublist lo hi l——索引 lo..hi-1lo..hi-1 处的元素：先取前 hihi 个，再丢掉前 lolo 个。 这一半开区间约定与 array_at_recarray_at_rec 一致。
• l1 ++ l2l1 ++ l2——HOL Light 的 APPENDAPPEND。

其中四条在 cst_predefined.mlcst_predefined.ml 中已证明；关于 ireplicateireplicate 的两条则是 cstarlib.mlcstarlib.ml 中的公理。

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（已证明）——后缀的头部就是该索引处的元素；这是驱动逐索引 循环的那一步。

!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（已证明）——全部丢弃后剩下空列表，遍历数组的循环正是借此证明 终止时不再剩下任何元素。

!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. (ireplicate n v) ++ [v] == ireplicate (n + &1) v

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

绝大多数证明从不按名字应用数组规则。它们是策略所编码的引理：策略文件对蕴含做 模式匹配，应用其中一条规则，如此反复，于是数组读写处的框架推断就自动完成了。 关于 strategy_demo/array/strategy_demo/array/ 中的数组策略，包括在拆分规则触发前建立其所需的 &0 <= i&0 <= i 与 i < ni < n 附加条件的那些以 checkcheck 守卫的规则，参见 用策略纯化蕴含。

当某一步过于特定、不适合交给策略时——例如一次附带证明义务的定制资源重排——同样的 规则会改由操作式路线应用，每次重排对应一个具名操作；参见 操作。

• 带类型谓词是一个四层结构：模型中的 single_byte_memsingle_byte_mem，作为单字节堆命题的 mstoremstore/mstore_noninitmstore_noninit，通过 merge_shortmerge_short/merge_intmerge_int/merge_int64merge_int64 按小端序组装字节的 store_2bytestore_2byte/store_4bytestore_4byte/store_8bytestore_8byte， 以及以 pure(…) && …pure(…) && … 补上有效性与范围的带类型存储。
• mstoremstore 对值的表示在模 256 意义下不敏感；符号性只通过带类型存储的范围条件 进入。
• 有效性是界加上对齐（aligned_naligned_n），并且是就对象最后一个字节陈述的。它并不排除 空地址。
• cast_unsigned n z = z rem exp_2 ncast_unsigned n z = z rem exp_2 n 使用欧几里得余数，因此对负的 zz 同样是截取 低 nn 位；cast_signedcast_signed 随后重新解释最高位。
• data_atdata_at 与 undef_data_atundef_data_at 在九种标量类型上按 ctypectype 分派。没有 TstructTstruct 子句；struct_atstruct_at 已声明但未公理化。
• 数组的第 ii 个元素位于 x + i * sizeof(ty)x + i * sizeof(ty)；array_at_rec x ty lo hi larray_at_rec x ty lo hi l 覆盖索引 lo..hi-1lo..hi-1，其中 ll 相对于 lolo，而 array_atarray_at 是 lo = &0lo = &0 的情形。
• 四条 data_atdata_at 规则与三十条数组规则在 cstarlib.mlcstarlib.ml 中都是 new_axiomnew_axiom——被假设 而非推导得出——而存储层的引理与 match 形式的展开则是已证明的。