Net IR v0.1（draft）

目标：一个确定性、可哈希、可跨语言的网表示。Netbook 的 JSON、aind 的字节码、trace 的快照都从这里派生。

1. 数据模型

type NetId = string;          // 例如 "research/8f3a"
type CellId = string;         // 单 net 内唯一；建议 "c<base36>"
type PortIndex = number;      // 0 = principal；1..n = auxiliary

type PortRef = {
  cell: CellId;
  port: PortIndex;
};

type Cell = {
  id: CellId;
  agent: string;              // 符号名： "gamma" | "delta" | "epsilon" | "user:Planner_Idle"
  label?: number;             // δ/γ 标签；用户构造子 id
  state?: unknown;            // 小状态（JSON）；大状态用 payload 引用
  payload?: string;           // 大 payload 的 content hash（外部 store）
  loc?: string;               // 节点 id；单机可省略
};

type Wire = {
  a: PortRef;
  b: PortRef;
};

type Net = {
  version: 1;
  id: NetId;
  cells: Cell[];
  wires: Wire[];
  free: PortRef[];            // 接口；顺序有意义
  meta?: {
    fuel?: number;
    step?: number;
    hash?: string;
  };
};

约束：

1. 每个 PortRef 至多出现在一条 Wire 或 free 中。
2. free 中的端口不能同时出现在 wires 中。
3. cells[].id 唯一。
4. wires 无向；序列化时按 (a.cell, a.port, b.cell, b.port) 排序，保证 hash 稳定。
5. cells 按 id 排序；free 按接口声明顺序。
6. payload 只存 hash；实际内容在 ValueStore（内容寻址，可跨 net 共享）。

2. 规则

type Rule = {
  version: 1;
  name: string;               // "gamma_gamma" | "user:Planner_Idle__Task"
  left: {
    agent: string;
    label?: number;
    state?: unknown;
  };
  right: {
    agent: string;
    label?: number;
    state?: unknown;
  };
  // RHS 是一个以 LHS 的 aux 端口为 free ports 的网模板
  rhs: NetTemplate;
  cost?: {
    interactions?: number;
    usd?: number;
    latency_us?: number;
  };
};

type NetTemplate = {
  cells: TemplateCell[];      // 局部 id，允许引用 LHS 绑定
  wires: TemplateWire[];
  free: TemplatePortRef[];    // 必须与 LHS 的 aux 端口一一对应
  bindings?: Record<string, string>; // 变量绑定（状态字段/消息字段）
};

规则约束：

• 对每对 (left.agent, right.agent)，至多一条规则（在状态展开后）。
• rhs.free 的顺序必须与 LHS 的 aux 端口顺序一致；类型检查保证类型匹配。
• 规则是局部的：rhs 不能引用 LHS 之外的 cell（除非通过 free port）。

3. 二进制表示（纯网）

64-bit term：

bit 63     : sub (1 = substitution)
bits 62..58: tag (5)
bits 57..40: label (18)
bits 39..0 : value (40)

Tag（v0.1）：

节点：

CON/DUP/CTR: [term0, term1]    // 两个 aux 端口
ERA:         []                // 无 aux
EFFECT:      [term_req, term_res, term_cancel]
JOIN(k):     [term_1..term_k, term_out]
SELECT(k):   [term_1..term_k, term_out]

40-bit 地址限制单节点堆 ≤ 1TB；v1 足够。需要更大时用 128-bit CellId + 间接表。

4. 哈希与相等

• net_hash = sha256(canonical_json(net))；canonical_json 按 1.4 排序。
• 规则 RHS 的 net_hash 包含模板变量名；变量名不影响语义，但影响 hash（v1 接受；v2 做 alpha-normalization）。
• 两个网语义相等（bisimulation）不等于 hash 相等；hash 只用于快照/重放校验。

5. 例子

{
  "version": 1,
  "id": "demo/add",
  "cells": [
    { "id": "c0", "agent": "gamma" },
    { "id": "c1", "agent": "gamma" },
    { "id": "c2", "agent": "epsilon" }
  ],
  "wires": [
    { "a": { "cell": "c0", "port": 0 }, "b": { "cell": "c1", "port": 0 } },
    { "a": { "cell": "c0", "port": 1 }, "b": { "cell": "c2", "port": 0 } }
  ],
  "free": [
    { "cell": "c0", "port": 2 },
    { "cell": "c1", "port": 1 },
    { "cell": "c1", "port": 2 }
  ]
}

6. 版本与兼容

• version: 1 是当前唯一版本。
• 新增 agent tag / 可选字段 → minor；删除/改语义 → major。
• 运行时拒绝未知 major；对未知 minor 字段忽略（向前兼容）。
• tests/golden/ir/*.json 是兼容性测试向量；任何序列化变更必须更新并审阅。

7. 已知限制（v0.1 / M0）

1. 自由端口属于 cell：v0.1 没有"独立于 cell 的自由端点"。规则删除一个带自由辅助端口的 cell 时，该接口端口会消失。M0 的演示通过显式 ctr 上下文 cell 避免悬空接口；完整的接口保持（自由端点/名字）在 M1 实现。
2. 只有二元 cell：Join/Select/Barrier 等多 principal 原语尚未进入 IR；specs/ain-sync.md 是设计，不是实现。
3. 标签无语义：label 字段已保留，但 v0.1 的规则匹配忽略标签（γ/δ 的标签化共享/commutation 在 M2 加入）。
4. 无 effects / locations / supervision：这些是 L3–L6，M2 之后逐步加入。
5. 规则接口顺序：RHS 的 Free { index } 按 left[0] 的 aux 端口在前、left[1] 在后编号；RuleBook 会对未排序的规则做归一化并重映射索引。
6. 无类型检查：v0.1 只校验端口/线/二进制结构；线性/session/effect 类型在 ain-lang（M2）。

这些限制在 docs/04-ain-model.md 的 L1–L6 路线中有对应计划；M0 的目标是先把"图重写 + 归约 + trace"跑通。

在 GitHub 编辑本文