VST中EnqueueLink函数正确性证明遇forward战术栈溢出求助

我正在用VST验证一个有序链表插入函数的正确性，已经完成相关辅助引理的证明，目前在定义函数规格（funspec）时存疑，同时使用forward战术时出现栈溢出。

待验证的C代码 #

void EnqueueLink(unsigned int *list, unsigned int id, unsigned int prio)
{
    unsigned int qAct = list[0];
    unsigned int lAct = 0;

    while ( (qAct != 0) && (FindPrio(qAct) >= prio) )
    {
        lAct = qAct;
        qAct = list[qAct];
    }

    /* Now we insert tAct between lAct and qAct and recompute the queue head.
    */
    list[lAct] = id;
    list[id] = qAct;
    // update task-head.
}

代码语义：EnqueueLink接收三个参数，第一个是数组实现的有序链表（下标对应节点id，存储值为下一个节点的id，0代表链表尾），第二个是待插入的节点id，第三个是该节点的优先级。函数通过while循环遍历链表，找到合适的插入位置lAct，将新节点插入到lAct和qAct之间。

已定义的Funspec #

Definition enqueue_spec : ident * funspec :=
DECLARE _EnqueueLink
WITH list : val, id: Z, prio: Z, sh : share, tasks : list Z
 PRE [ tptr tuint, tuint, tuint ]
  PROP  (writable_share sh; 0 <= prio <= Int.max_unsigned;
         Forall (fun x => 0 <= x <= Int.max_unsigned) tasks; LocallySorted Z.ge tasks)
  PARAMS (list; Vint(Int.repr id); Vint (Int.repr prio))
  SEP   (data_at sh (tarray tuint Int.max_unsigned) (map Vint (map Int.repr tasks)) taskActivations)
 POST [ tvoid ]
  PROP (LocallySorted Z.ge (insert id tasks)) RETURN ()
  SEP  (data_at sh (tarray tuint Int.max_unsigned) (map Vint (map Int.repr (insert tAct tasks))) taskActivations).

Definition Gprog := [enqueue_spec].

Lemma body_enqueuelink: semax_body Vprog Gprog f_EnqueueLink enqueue_spec.

Proof.

start_function. forward.

Admitted.

数学层面的插入引理 #

已通过以下Fixpoint证明有序链表插入元素后仍保持有序：

Fixpoint insert (x : Z) (l:list Z) : list Z :=
  match l with
  | nil => x :: nil 
  | (h :: t) =>
    match Z_ge_dec x h with
    | right _ => h :: (insert x t)
    | left _ => x :: (h :: t) end
  end.

当前问题 #

1. 不确定上述enqueue_spec的定义是否正确，需要验证。
2. 证明body_enqueuelink时，执行start_function. forward.后出现栈溢出。
3. 作为VST新手，需要后续证明的推进思路。

问题解答 #

一、Funspec的正确性修正 #

你的enqueue_spec存在几个核心问题：

1. 未定义变量tAct：POST部分使用insert tAct tasks，但tAct未在WITH或其他区域声明，属于笔误，应替换为待插入的id。
2. 链表抽象模型不匹配：C代码是数组实现的链式结构，但你用tarray tuint直接映射tasks列表，未体现链式关系。需改用VST的链表分离逻辑（如自定义list_linked谓词）来抽象这种结构。
3. 缺少FindPrio的约束：函数依赖FindPrio(qAct)获取节点优先级，但PRE未声明该函数的行为，需补充forall x, x ∈ tasks → FindPrio(x) = 对应优先级这类条件，确保优先级获取逻辑合法。
4. id合法性约束缺失：PRE未限制id的范围（0 <= id <= Int.max_unsigned）以及id ∉ tasks，可能导致插入重复或非法节点。

修正后的funspec示例：

Definition enqueue_spec : ident * funspec :=
DECLARE _EnqueueLink
WITH list : val, id: Z, prio: Z, sh : share, 
     tasks : list Z,  (* 链表节点id的有序列表 *)
     prio_map : Z -> Z (* 节点id到优先级的映射 *)
 PRE [ tptr tuint, tuint, tuint ]
  PROP  (writable_share sh;
         0 <= prio <= Int.max_unsigned;
         0 <= id <= Int.max_unsigned;
         id ∉ tasks;
         Forall (fun x => 0 <= x <= Int.max_unsigned) tasks;
         LocallySorted (fun a b => prio_map a >= prio_map b) tasks; (* 链表按优先级降序排列 *)
         Forall (fun x => prio_map x <= Int.max_unsigned) tasks)
  PARAMS (list; Vint(Int.repr id); Vint (Int.repr prio))
  SEP   (* 自定义链表谓词，描述数组实现的链式结构 *)
        (list_linked sh list tasks prio_map)
 POST [ tvoid ]
  PROP (LocallySorted (fun a b => prio_map a >= prio_map b) (insert id tasks))
  RETURN ()
  SEP  (list_linked sh list (insert id tasks) (prio_map ++ [(id, prio)]))

二、栈溢出问题的解决 #

forward战术栈溢出通常由两个原因导致：

• Funspec的SEP部分抽象不准确，VST无法正确推导内存状态，陷入无限递归。
• 未提前定义循环不变式，forward尝试直接处理循环时无法终止。

解决步骤：

1. 先修正funspec的抽象模型，确保SEP部分准确反映链表的链式结构，而非简单数组映射。
2. 拆分证明步骤，不要直接用forward处理整个函数：
   • 先用forward处理初始化语句（qAct = list[0];和lAct = 0;），手动维护内存状态。
   • 为while循环定义循环不变式，这是VST证明循环的核心，需包含：
     • lAct和qAct的合法性（在数组范围内或为0）。
     • 链表头到lAct的部分有序，且所有节点优先级>=待插入节点优先级。
     • qAct之后的节点优先级<待插入节点优先级。
     • 内存状态的分离逻辑保持有效。

三、后续证明推进思路 #

作为VST新手，建议按以下步骤推进：

1. 完善辅助定义：
   • 定义链表分离逻辑谓词list_linked，描述数组实现的链式结构：list_linked sh base l pm表示以base为起始地址的数组中，存储着节点id列表l，每个节点x的优先级为pm x，链表以0结尾。
   • 证明list_linked的基本性质，比如遍历、插入后的保持性等。
2. 修正并验证Funspec：
   • 确保PRE和POST的PROP、SEP部分完全匹配C代码语义，特别是FindPrio的行为、链表有序性的定义。
3. 分步证明函数体：
   • 初始化阶段：用forward处理变量赋值，将内存状态从PRE的链表谓词转换为包含qAct和lAct的状态。
   • 循环阶段：
     1. 用forward_while战术传入提前定义的循环不变式。
     2. 证明循环不变式的初始化成立（进入循环前满足）。
     3. 证明循环体执行后，不变式仍然保持。
     4. 证明循环终止条件满足时，不变式能推导出POST的条件。
   • 插入阶段：处理list[lAct] = id;和list[id] = qAct;，用forward更新内存状态，证明此时的链表状态符合POST中的list_linked谓词。
4. 复用已有辅助引理：
   • 你已证明insert函数的有序性，在证明POST的PROP时，可直接调用该引理，结合循环不变式中的有序条件，推导出插入后的链表仍保持有序。

内容的提问来源于stack exchange，提问作者Drona Nagarajan