feat(ghost): 支持用户自定义 ghost resources 与 ghost-aware C 程序推理 · Pull Request !43 · cstarlang/CStar Examples

## 背景

本 PR 为 C* 用户端接入用户自定义 ghost resources，使程序断言能够同时描述：

- 现有 C physical memory；
- 用户选择的 ghost resource algebra；
- 模块 invariant 与客户端 token；
- 只更新 ghost state、保持 physical memory 不变的 viewshift。

目标是支持 modular module/client reasoning，并为后续concurrency reasoning的支持做准备。

## 依赖

本 PR 依赖以下配套修改：

- proof stdlib submodule：
  - `da9dd55` → `f11c5be`
  - 提供 RA core、通用 RA constructions、ghost heap、resource assertions、C memory RA、ghost-only basic update/viewshift 和相应 proof rules。
- verifier/runtime 分支 `ghost-resources-phased`：
  - assertion-model descriptor；
  - ghost-aware symbolic-state codec；
  - QCP assertion serializer；
  - batched QCP boundary/transition theorem RPC；
  - symbolic-state source 一致性检查。

应先合并 proof stdlib 和 runtime PR，再合并本 PR。

## 核心设计

对于一个闭合、单态的用户 ghost-cell RA `G : (A)ra`，C 程序资源模型为：

```text
c_resource_ra G = prod_ra mem_ra (ghost_heap_ra G)
Prop_G          = carrier(c_resource_ra G) -> bool
```

物理 ownership 和 ghost ownership 因而处于同一个 linear separation logic 中。

C basic update 特意比一般的 `r_bupd (c_resource_ra G)` 更严格：

- physical `FST` projection 必须保持不变；
- 只允许对 ghost `SND` projection 执行 frame-preserving update。

因此 viewshift 不能凭空修改、分配或释放 C physical memory。

## 主要修改

### 1. 按文件选择 ghost RA

新增 `userlib/qcp/c_logic.{h,c}`，负责在一次验证会话中安装一个选定的 C assertion model。

```c
PROOF int c_logic_install(const term G);
```

安装器要求 `G` 是闭合、单态的 RA，并一次性完成：

1. 构造 `c_resource_ra G`；
2. 创建闭合、单态的 SL operator aliases；
3. 证明并注册选定的 SL、C memory 和 ghost update rules；
4. 安装 QCP assertion descriptor；
5. 注册 `data_at`、`undef_data_at` 和 opaque `own`；
6. 发布可通过 `get_theorem_by_name` 和 IDE 搜索的定理。

普通 C 文件默认通过 `c_logic_default` 选择 `unit_ra`；需要自定义 ghost resources 的文件可延后默认安装并显式调用 `c_logic_install(G)`。

### 2. Ghost-aware assertion 与 QCP symbolic state

安装后的 assertion carrier 同时包含 physical memory 和 ghost heap。

公开断言接口包括：

```text
emp, **, -*, &&, ||, exists, |--, -||-
fact, pure, data_at, undef_data_at, own
bupd, ==*=>
```

设计约束：

- QCP 只特殊处理选定的 `data_at` 和 `undef_data_at`；
- `own(name, a)` 在 symbolic state 中作为普通 opaque spatial atom；
- ghost name 对 QCP 只是普通 `num`；
- module invariant 与 client token 通过同一个 ghost name 建立联系；

### 3. 完整 symbolic-state transition

`set_symbolic_state(transition)` 现在接收完整的 entailment 或 viewshift theorem：

```text
source |-- target
```

或：

```text
source ==*=> target
```

descriptor-backed 路径会：

1. 读取精确的 QCP current state；
2. 通过 kernel-certified boundary theorem 解码；
3. 用当前选定的 SEP ACU laws 对齐 theorem source；
4. 将 transition rebase 到精确 native source；
5. 只编码 target；
6. 交给 native setter 再次核对 current source。

最终实现使用单个 theorem-producing HOL RPC 完成 decode、SEP-ACU alignment、target encode 和 theorem transport。所有 operator 与 laws 都作为显式参数传入，HOL server 不保存隐式 SL theory state。

### 4. Ghost protocol rules

选定 C logic 发布以下规则：

```text
C_LOGIC_GHOST_OWN_OP
C_LOGIC_GHOST_OWN_VALID
C_LOGIC_GHOST_OWN_UPDATE
C_LOGIC_GHOST_OWN_UPDATE_ND
C_LOGIC_GHOST_OWN_DEALLOC
C_LOGIC_GHOST_OWN_ALLOC_EMPTY
C_LOGIC_GHOST_OWN_ALLOC
```

同时提供 physical memory 相关规则：

```text
C_LOGIC_DATA_AT_VALUE_RANGE
C_LOGIC_ALLOCATED_AT_ZERO
C_LOGIC_ALLOCATED_AT_APPEND
C_LOGIC_DATA_AT_ALLOCATED_AT
C_LOGIC_UNDEF_DATA_AT_ALLOCATED_AT
C_LOGIC_ALLOCATED_AT_TO_UNDEF_DATA_AT
C_LOGIC_DATA_AT_TO_UNDEF_DATA_AT
```

所有发布定理均在安装时检查：

- hypothesis-free；
- closed；
- monomorphic；
- theorem database 名称无冲突。

### 5. Modular allocator example

新增实际 free-list allocator 的 ghost-state 验证。

allocator module 使用共享 ghost name 将：

- module invariant 中的 authoritative allocation state；
- client 持有的 local malloc token；

联系起来。

公开规格满足：

- `malloc` 产生对应 block 的 client token；
- `free` 要求并消费同名 token；
- client 无需知道 free-list 的具体 physical representation；
- allocator invariant 显式维护 free-list 和 authoritative ghost state；
- ghost cell 可在 module 生命周期结束时安全 deallocate。

### 6. Monotonic counter

实现 monotonic counter 的 module/client reasoning：

- module invariant 内部存在量化真实 current value；
- client 只持有 lower-bound token；
- authority 与 fragment validity 推导公开 lower bound；
- increment 通过 ghost update 同步更新 physical counter 和 logical protocol；
- client 不接触 module internal state。

### 7. Fictional Separation Logic examples

实现并验证以下 FSL 风格示例：

- fractional permissions；
- bit pair；
- two modules。

Bit-pair invariant 已收紧为：

```text
BPInv(γ,p) =
  exists b1 b2.
    Bit(b1) *
    Bit(b2) *
    p |-> (b1 + 2*b2) *
    own γ (authoritative (b1,b2))
```

公开接口只保留：

- ghost name `γ`；
- physical object `p`；
- client fictional tokens。

内部 `b1`、`b2` 不再作为 invariant 参数暴露，避免 representation state 泄漏。

Two Modules example 进一步组合 bit-pair 与 monotonic-counter algebras，并通过独立 token 和共享组合 RA 验证模块组合。

### 8. 全量 examples 迁移

现有 examples、tutorial、PSI、LiveVerif、VeriFast 和 VST 迁移到选定的 ghost-aware C logic。

没有自定义 ghost state 的文件统一使用 `unit_ra`，因此仍获得原有 physical-only 推理体验，同时不再依赖 legacy `cstarlib.ml` separation-logic definitions。

当前 physical heap 继续采用现有 memory representation；本 PR 聚焦 logical resources 与程序推理接口。

## 性能修复

ghost-aware migration 初期出现明显性能回归。调查确认主要瓶颈不是 product RA 增大 assertion AST，而是同一 symbolic-state term 上的重复 RPC 和 serializer dispatch。

已完成：

- 缓存 descriptor-certified SL operator names；
- model/generic printer 共享 application decomposition；
- `is_sl_exists` / `is_sl_forall` 使用已安装 HOL constant name 识别；
- QCP boundary normalization 下沉为单次 theorem RPC；
- 完整 symbolic-state transition 下沉为单次 theorem RPC；
- 保留 kernel theorem、SEP-ACU alignment 和 native exact-source guard。

最终完整回归测量：

| 项目 | 时间 |
|---|---:|
| sorted-bintree | 40.214 s |
| VST malloc | 147.620 s |
| 完整 `verify_all.sh` | 801.147 s |

## 验证结果

```text
./verify_all.sh
Verified 152 file(s): 152 passed, 0 failed.
Ignored 11 file(s) via .verifyignore.
Total cstarc time: 801.147s.
```

覆盖范围包括：

- proof stdlib source 与 regression tests；
- 所有 RA constructions 和 ghost heap theories；
- QCP boundary 与 symbolic-state transition regressions；
- allocator module/client；
- monotonic counter module/client；
- fractional permissions；
- bit pair module/client；
- two-modules composition；
- PSI examples；
- LiveVerif、VeriFast、VST migrations；
- tutorial 和 strategy examples。

Bit-pair 等最终提交示例均没有未声明 VC。测试中显式保留的 axiom/expected-failure 文件继续由现有测试约定管理。

## 建议审阅顺序

1. proof submodule 更新及 `userlib/qcp/c_logic.h`；
2. `c_logic_install` 的 fail-stop installation transaction；
3. `veriftime` symbolic-state transition；
4. allocator 和 monotonic-counter protocols；
5. FSL bit-pair、fractional permissions、two-modules；
6. 普通 examples 的 `unit_ra` 迁移；
7. performance analysis 与 QCP regressions。

类型	指派人员	状态
审查	王迪	进行中 (0/1人)
测试	王迪	进行中 (0/1人)

cstarlang / CStar Examples .gitee-modal { width: 500px !important; }

搜索帮助

cstarlang / CStar Examples