C*：开发与证明一体化

带类型的内存谓词

EN | 中文

带类型的内存谓词

内存模型提供的是一个由单个字节构成的堆，而 C* 规约谈论的是 C 对象。本页刻画连接二者、并出现在每一份 C* 规约中的、以 ctype 为索引的 data_atdata_at 与 array_atarray_at 谓词族——一个带类型单元对其地址与值作出了哪些保证，陈述这些保证所用的有效性、范围与转换函数——并一并给出证明引擎用来拆解和重组这些断言的规则。

关于底层的堆以及下文用到的分离逻辑连接词（****、&&&&、||||、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 对象的纯条件的合取。字节存储本身是 vv 在 sizeof tysizeof ty 个字节中的小端序表示，每个字节单独被拥有；本页不再进一步展开它，下文也没有任何规则需要把它展开。

定义 1（store_intstore_int 与所有带类型存储的共同形状）。 
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
store_4byte x vstore_4byte x v 是其中的空间部分：位于 xx、x + &1x + &1、x + &2x + &2、x + &3x + &3 的四个字节已被拥有，并按小端序存放着 vv。pure(P) && Hpure(P) && H 这一模式贯穿全篇：pure(P)pure(P) 是这样一个堆命题——恰当 PP 成立时它对 任意内存都成立——因此 pure(P) && Hpure(P) && H 刻画的内存与 HH 相同，但只要 PP 不真它 就不可满足。它并不是 fact(P) ** Hfact(P) ** H：fact(P)fact(P) 即 pure(P) && emppure(P) && emp， 因而把空堆声明为自己的那一份，这也正是二者在分离合取中可以互换 （fact(p) ** hp -|- pure(p) && hpfact(p) ** hp -|- pure(p) && hp）、单独出现时却不能互换的原因。

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

存储 未初始化形式 字节数 取值范围
store_charstore_char undef_store_charundef_store_char 1 byte_min_signedbyte_min_signed … byte_max_signedbyte_max_signed
store_ucharstore_uchar undef_store_ucharundef_store_uchar 1 &0&0 … byte_max_unsignedbyte_max_unsigned
store_shortstore_short undef_store_shortundef_store_short 2 short_min_signedshort_min_signed … short_max_signedshort_max_signed
store_ushortstore_ushort undef_store_ushortundef_store_ushort 2 &0&0 … short_max_unsignedshort_max_unsigned
store_intstore_int undef_store_intundef_store_int 4 int_min_signedint_min_signed … int_max_signedint_max_signed
store_uintstore_uint undef_store_uintundef_store_uint 4 &0&0 … int_max_unsignedint_max_unsigned
store_int64store_int64 undef_store_int64undef_store_int64 8 int64_min_signedint64_min_signed … int64_max_signedint64_max_signed
store_uint64store_uint64 undef_store_uint64undef_store_uint64 8 &0&0 … int64_max_unsignedint64_max_unsigned
store_ptrstore_ptr undef_store_ptrundef_store_ptr 8 &0&0 … int64_max_unsignedint64_max_unsigned

每种存储还断言与其位宽相应的有效性谓词——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_at 与 undef_data_at

ctype 索引

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

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_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 只出现在这两个应用之内。

sizeof、min_of、max_of

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

ctype sizeofsizeof min_ofmin_of max_ofmax_of
TcharTchar 1i1i --(&128)--(&128) &127&127
TucharTuchar 1i1i &0&0 &255&255
TshortTshort 2i2i --(&32768)--(&32768) &32767&32767
TushortTushort 2i2i &0&0 &65535&65535
TintTint 4i4i --(&2147483648)--(&2147483648) &2147483647&2147483647
TuintTuint 4i4i &0&0 &4294967295&4294967295
Tint64Tint64 8i8i --(&9223372036854775808)--(&9223372036854775808) &9223372036854775807&9223372036854775807
Tuint64Tuint64 8i8i &0&0 &18446744073709551615&18446744073709551615
TptrTptr 8i8i &0&0 &18446744073709551615&18446744073709551615

所有无符号类型以及 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 的规则

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

从字节缓冲区中读出一个字、或把一个字写入其中而不经过未初始化的中间状态，背后就是这两条规则。

数组

定义 2（数组索引约定）。

在 array_at_rec x ty lo hi larray_at_rec x ty lo hi l 中，索引为 ii 的元素位于地址 x + i * sizeof(ty)x + i * sizeof(ty)，而该断言恰好覆盖索引 lo, lo + &1, …, hi - &1lo, lo + &1, …, hi - &1。列表 ll 按顺序存放这些元素的值，因此 ilength(l)ilength(l) 等于 hi - lohi - lo，且 ll 的头部是索引 lolo 处的元素，其地址为 x + lo * sizeof(ty)x + lo * sizeof(ty)。

因此基地址 xx 并不随 lolo 平移：在地址算术中索引是绝对的，而列表则是相对于 lolo 的。这也是为什么绝对索引 nn 处的元素是 inth (n - lo) linth (n - lo) l，以及为什么对 array_at_recarray_at_rec 换基时必须同时移动 xx 和索引界。

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 形式的展开

这四个谓词按下列 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（前驱计数的整数注入）重新进入。

数组规则

名字中含 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——以 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。

配套定理

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/ 中的数组策略，包括在拆分规则触发前建立其所需的 &0 <= i&0 <= i 与 i < ni < n 附加条件的那些以 checkcheck 守卫的规则，参见 用策略纯化蕴含。

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

小结

  • 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 定律可用。