Skip to content

feature/graph anchored regions #39

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
dslsdzc wants to merge 2 commits into
base: main
Choose a base branch
from
Open

feature/graph anchored regions #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
077cd0b
docs: 图锚定区域内存模型设计（graph-anchored regions）——保留竞技场双价值（零碎片/有界碎片），区域锚定数据流…
dslsdzc Aug 11, 2026
22b8c35
docs: 图锚定区域设计落地——memory-model.md 重写（区域=子图字节域/图活性生命周期/split-merge-shar…
dslsdzc Aug 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 30 additions & 1 deletion docs/ir-schema/coreir-schema.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,6 +151,34 @@ DFNode 覆盖两种节点：普通指令节点（opcode ≤ IR_AWAIT）和规约
| 4 | 4 | kind | 符号类型：0=func, 1=var, 2=type, 3=field |
| 8 | 4 | scope | 作用域（函数索引或 -1 表示全局） |

### ALLOC_AT 节点（声明式放置，2026-08-13）

固定地址放置的声明式进图节点（图锚定区域内存模型，见 `docs/memory-model.md` 机制 #3）：

| 字段 | 含义 |
|------|------|
| opcode | ALLOC_AT（编号待实现时分配，不与 SPEC_* 冲突为前提） |
| dest_var | 结果指针变量 |
| src1 | 固定地址（编译期常量或部署配置值） |
| src2 | 大小（字节） |
| src3 | 对齐（字节） |
| type_kind | 指向的元素类型 |

与 ALLOC 同路径获得 provenance；ProvenanceVerify 验证边界+宽度（`offset ∈ [0, size)` 且 `off + width <= size`）。声明是唯一信任点，之后全图追踪。

### 布局元数据（Layout Descriptor，2026-08-13）

struct 类型关联布局描述符。**默认由编译器推导自然布局**（字段顺序 + 自然对齐），用户 `layout(...)` 声明时显式给出（packed/强制对齐/硬件结构逃生门）：

| 字段 | 含义 |
|------|------|
| packed | 是否紧凑（无填充） |
| align | 整体对齐要求（字节） |
| field_count | 字段数 |
| fields | 每字段：(name_idx, offset, width, align)——name_idx 索引字符串表 |

布局元数据是**图数据**：后端与验证器消费同一来源（语义保鲜），DEREF 的偏移+宽度检查对着布局走。

---

## 三、规约操作码（新增 DFNode opcode）
Expand Down Expand Up @@ -179,7 +207,7 @@ DFNode 覆盖两种节点：普通指令节点（opcode ≤ IR_AWAIT）和规约
| `#pure` | 函数的所有 DFNode 中：无 CALL 到非纯函数、无 STORE 到外部全局变量 | 无副作用 |
| `#deterministic` | #pure + 无依赖于外部状态（IO、env、随机源）的路径 | 确定性 |
| `#terminating` | 所有循环（DFNode 中的回边）有可识别的单调递减度量 | 终止性 |
| `#no_alloc` | 无 ALLOC / ALLOC_ARRAY / ALLOC_STRUCT 节点 | 不分配 |
| `#no_alloc` | 无 ALLOC / ALLOC_ARRAY / ALLOC_STRUCT / ALLOC_AT 节点 | 不分配 |
| `#no_throw` | 无可达的异常路径（无分支导向 panic/error 节点） | 不抛异常 |
| `#safe_index` | 所有 LOAD_INDEX/STORE_INDEX 节点的索引输入 ≤ 数组长度变量 | 安全索引 |
| `#len_preserved` | 输入集合变量和输出集合变量之间的 DFNode 无插入/删除操作（STORE_INDEX 不超出边界，无 ALLOC 替换） | 长度守恒 |
Expand Down Expand Up @@ -269,6 +297,7 @@ store_index_var, make_enum, ref, // 15-17
branch, jump, label, phi, load_enum_tag, // 18-23
slice, deref, store_ptr, // 24-26
spawn, yield, await, // 27-29
alloc_at, // 编号待实现时分配（声明式放置，2026-08-13）
spec_constraint, spec_forall, spec_exists, // 30-32
spec_imply, spec_old, spec_assume // 33-35
```
Expand Down
Loading