带类型的内存谓词

内存模型中的堆由单个字节构成，C* 规约描述的则是 C 对象。连接二者的是以 ctype 为索引的 data_atdata_at 与 array_atarray_at 谓词族，它们出现在每一份 C* 规约中。本页说明带类型单元对地址和值提供了哪些保证，介绍表述这些保证所需的有效性、范围与转换函数，以及证明引擎拆解和重组这些断言所用的规则。

关于底层的堆以及下文用到的分离逻辑连接词（****、&&&&、||||、purepure、factfact、empemp、existsexists、|--|--、-|--|-），参见内存模型与断言。

data_at x ty vdata_at x ty v 表示拥有从 xx 开始的若干字节，按 C 类型 tyty 读取这些字节得到的值为 vv。这条断言包含三项保证，本页的各条规则都围绕它们展开：

• 地址对该类型有效且对齐——对象完整落在地址空间之内，且 xx 是该类型宽度的整数倍（即下文的 isvalidptr_*isvalidptr_* 谓词）；
• 恰好拥有 sizeof tysizeof ty 个连续字节——因此同一地址上的两个 data_atdata_at 互相矛盾，相邻的单元则可以用 **** 组合成数组；
• 值落在范围之内——min_of ty <= v /\ v <= max_of tymin_of ty <= v /\ v <= max_of ty。

data_atdata_at 根据 tyty 选择对应的带类型存储，每种标量类型对应一种。带类型存储由定宽字节存储与一组纯条件合取而成，这些条件保证它是该类型的合法 C 对象。字节存储用 sizeof tysizeof ty 个字节以小端序表示 vv，并分别拥有每个字节。本页不再展开字节存储，下文的规则也不需要展开它。

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。未初始化形式保留有效性条件而去掉范围条件，因为此时没有值需要约束；store_4byte_noninit xstore_4byte_noninit x 拥有同样的四个字节，但不说明其内容：

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)

有效性要求同时满足地址空间的界限和对齐条件。对齐是指地址在模所需字节数的意义下与零同余。

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。

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

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

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

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

下面各谓词按九个标量构造子分派。除 TaliasTalias 外，复合构造子都是不透明的：TstructTstruct、TenumTenum 与 TunionTunion 只携带 C 的标签名，任何谓词的子句都不提及它们。Talias name tyTalias name ty 是 tyty 的一个 typedeftypedef，下面的每个函数都会继续处理其中的内层类型。Tarray n tyTarray n ty 是 nn 个元素的数组。TfunTfun 记录一个 C 函数签名——参数名、参数类型、结果类型——只出现在下文所述的函数指针规约之内。

data_at x ty vdata_at x ty v 就是由 tyty 选出的带类型存储。九种标量 ctype 各有一条子句，另有一条处理 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

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

undef_data_atundef_data_at 以同样的方式选择未初始化存储，在有效且对齐的地址上拥有相应数量的字节，但不约束其中的内容：

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

还有两个常量用到 TfunTfun 构造子。它们是不透明的标记：理论不给出定义，由符号执行引擎把它们解释为函数规约：

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 表示地址 ff 处的函数（其 C 签名是 TfunTfun 型的 ctype tyty）满足契约 prepre / postpost，其中 TfunTfun 的参数名与 __return__return 以自由变量出现。fnspec_wfnspec_w 还引入了幽灵参数，写成 prepre 与 postpost 共用的一个 λ 绑定子（多个参数时写作 \(a,n). …\(a,n). …）。函数指针本身是普通的 TptrTptr 值，所以 data_atdata_at、min_ofmin_of 与 max_ofmax_of 都没有 TfunTfun 子句：TfunTfun 只出现在这两个应用之内。

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

所有无符号类型以及 TptrTptr 的 min_ofmin_of 都等于 &0&0；其余各项就是上文“各位宽的实例”一节中的位宽界（min_of(Tint) = int_min_signedmin_of(Tint) = int_min_signed、max_of(Tuint) = int_max_unsignedmax_of(Tuint) = int_max_unsigned，依此类推）。min_of_defmin_of_def 与 max_of_defmax_of_def 直接给出这些数值，每个标量构造子一条方程，证明中就用这些方程重写：

min_of_defmin_of_def、max_of_defmax_of_def——以方程合取式给出的数值。

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 的形式与之相同，取值依次为 --(&128)--(&128)、&0&0、--(&32768)--(&32768)、&0&0、--(&2147483648)--(&2147483648)、&0&0、--(&9223372036854775808)--(&9223372036854775808)、&0&0、&0&0，同样继续处理 TaliasTalias 中的内层类型。两者都没有 TstructTstruct、TenumTenum、TunionTunion、TarrayTarray 或 TfunTfun 的方程，因此这些类型的 min_ofmin_of 与 max_ofmax_of 保持不透明。由于每个合取项都是关于单个构造子的方程，用整条定理重写可以直接作用于 min_of Tintmin_of Tint。

sizeofsizeof 由 new_specificationnew_specification 引入，sizeof_defsizeof_def 是其刻画性质中的方程部分：除上表中的九条标量子句外还有两条，sizeof(Tfun fnamel tyl retty) = 8isizeof(Tfun fnamel tyl retty) = 8i（函数指针与指针同样大小），以及 sizeof(Talias name ty) = sizeof tysizeof(Talias name ty) = sizeof ty。TstructTstruct、TenumTenum、TunionTunion 与 TarrayTarray 没有方程；结构体的大小与布局在理论中没有建模，这与 field_offsetfield_offset 保持未解释是一致的。刻画性质的另一部分，是在每个 ctypectype 上都成立的那一条事实：

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。

另有两条规则（均已证明）揭示单个单元的字节布局：一个 4 字节无符号单元与四个 1 字节无符号单元描述同一块内存，后者的值按小端序组合后得到前者的值。字节与值之间的关系是 merge_intmerge_int，它只约束 vv 的低 32 位以及每个字节的低 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))

data_at_Tuint_Tuchardata_at_Tuint_Tuchar——把一个 TuintTuint 单元拆成它的四个字节，低字节在前；xx 的对齐与 vv 的范围以事实的形式给出。

!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——其逆向形式：4 字节对齐地址上的四个相邻字节，连同它们合并出的值及其范围，构成一个 TuintTuint 单元。

!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

这两条规则支持从字节缓冲区中读取一个字，或向其中写入一个字，整个过程无需经过未初始化的中间状态。

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

array_at_recarray_at_rec 是对列表 ll 递归定义的，每个元素对应一条位于 x + i * sizeof(ty)x + i * sizeof(ty) 的 data_atdata_at；它的展开式就是下文的 array_at_rec_defarray_at_rec_def。另一个谓词则描述从同一窗口中移除一个单元后剩余的部分。

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_ 谓词族——undef_array_at_rec x ty lo hi nundef_array_at_rec x ty lo hi n 及其带空洞形式 undef_array_at_missing_i_rec x ty i lo hi nundef_array_at_missing_i_rec x ty i lo hi n——拥有同样的地址，但不约束其中的内容。由于没有列表可供递归，这些谓词改为对元素个数 nn 递归，该个数以 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

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

这四个谓词按下列 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，即将前驱计数 mm 注入整数类型后得到的值。

名字中含 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. 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)))

数组断言用列表记录元素的值，上文的规则会相应地重排这些列表。下面的列表函数封装了 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——ll 的长度，以 intint 表示。
• 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。

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

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

两条 ireplicateireplicate 事实都带有前提 &0 <= n&0 <= n，因为 ireplicateireplicate 经由 num_of_intnum_of_int 定义，而后者在负整数上没有规定。

绝大多数证明无需按名称显式应用数组规则。这些引理由策略编码：策略文件反复对蕴含做模式匹配，再应用相应的规则，从而自动完成数组读写处的框架推断。 strategy_demo/array/strategy_demo/array/ 的数组策略中，以 checkcheck 守卫的规则会先确立 &0 <= i&0 <= i 与 i < ni < n 这两个附加条件，再触发需要这些条件的拆分规则。详情参见用策略纯化蕴含。

有些步骤过于特定，不适合交给策略，例如附带证明义务的定制资源重排。这时可以通过操作式证明应用同样的规则，每次重排对应一个具名操作；参见操作。

• data_at x ty vdata_at x ty v 保证地址有效且对齐、恰好拥有 sizeof tysizeof ty 个字节，并且 min_of ty <= v <= max_of tymin_of ty <= v <= max_of ty；它展开成的带类型存储形如 pure(…) && …pure(…) && …，纯部分是有效性与范围，空间部分是小端序的字节存储。
• 有效性要求满足地址界限与对齐条件（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 分派，并透过 TaliasTalias。复合构造子（TstructTstruct、TenumTenum、TunionTunion、TarrayTarray、TfunTfun）没有子句；结构体的字段是位于 field_addrfield_addr 的独立单元。
• fnspecfnspec 与 fnspec_wfnspec_w 针对函数指针的 TfunTfun 签名陈述其契约；赋予它们含义的是引擎，而非理论。
• 数组的第 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 的情形。
• 本页每一条规则都是已证明的定理，库没有添加任何公理。sizeofsizeof、data_atdata_at 与 undef_data_atundef_data_at 由 new_specificationnew_specification 引入而非定义，因此在 TstructTstruct、TenumTenum、TunionTunion 与 TarrayTarray 上（对两个 data_atdata_at 还有 TfunTfun）只有 sizeof_ge_0sizeof_ge_0 与四条 data_atdata_at 定律可用。