设备管理包设计（转自动化的前提）
状态：设计经过一轮独立复核（复核记录，读了代码和模型），复核意见已并入本稿。第一阶段的核心已合并：C1 到 C5 和租约的续期与释放（任务页 device-lease-ops.md），P1 的清单、台架事实和匹配函数也已合并；P2 到 P5 的台架包在做。编译半边等所有者的三样输入（编译设计）。起因：所有者 2026-10-22 定，转自动化要的是真实设备管理能力，做成 Hub 的一个任务包，把硬件设备的占用、IP 地址管理、版本管理等组合起来用（进度决定 16）。模型依据：node tools/show-element.ts D04 D07 D03 D02 C07 K03 T04 B05。
1. 它要解决什么
转自动化要把评审过的用例编成可执行的脚本，在共享的实验室台架上跑。台架是共享的真实硬件：同一时间只能一个人用，地址不能冲突，脚本能不能跑取决于设备上装的是哪个构建。现在这三件事靠人记。这个包让它们在 Hub 里有记录、有规则、能核对，并合成一个动作：“给我一个能跑构建 X 的台架，用 2 小时。”
2. 阶段，以及每个阶段证明什么
| 阶段 | 内容 | 要所有者给的 | 能证明 | 证明不了 |
|---|---|---|---|---|
| 1 | 台架清单（管理员上传的拓扑文件，声明）、占用、地址分配、版本报告（声明）。全部是 Hub 内部的记录，不接触任何设备 | 无 | 冲突、期限、围栏、地址不重复、选台架和版本比对的逻辑；真实 Circle 里整条流程走得通 | 设备上实际装的是什么；台架上有没有人手工操作 |
| 2 | 只读观察：经执行器（D07）在设备上执行允许的只读命令类，取版本和接口地址，写入观察，与声明比对，报漂移 | 台架、账号、允许的只读命令类、执行器所在的机器 | 声明与观察一致，或漂移了 | 观察之外的状态；本地操作 |
| 3 | 改动：升级到指定构建、改配置。至多一次、丢回复即冻结、核对；永不重启 | 另行批准每一类命令 | 经 Hub 派发的改动有记录、有结局 | 本地入口的改动（目标不执行同一租约时排除不了，D02） |
阶段 1 就能交付“转自动化”里最有价值的一半：台架事实。编译用例时，字面地址要解析成台架上的实体或分配值（T04）；监听地址必须是某台设备的接口地址，而且同一网段上要有能发起请求的客户端或路由器，没有触发设备的网段上的地址不能当监听地址（旧系统的做法，只取行为描述，不取代码和值）。这些都由包里的纯函数从清单算出。
3. 三类状态，各落在模型的哪里（不新增概念）
| 状态 | 例子 | 家 | 谁写 | 变化 |
|---|---|---|---|---|
| 清单 | 台架有哪些设备，类型，接口地址段，服务 | 管理员发布的命名文档：上传的拓扑文件按内容寻址存为源文件（B02），一个命名指针指向当前那份；来源类型“声明”；每次发布是新的一份，旧的不变；运行开始时把摘要冻结进运行 | 管理员 | 少 |
| 占用与地址 | 谁在什么时候占着哪台设备、哪个地址 | 租约（D04）：当前状态是一张按键唯一的表，每次变更追加一条 Hub 动作记录（B05，新增一个动作种类“租约”，先例是 move_root）；表可以由动作记录重建 |
只有 Hub | 频繁 |
| 版本 | 某设备上装的构建 | 阶段 1：写在管理员发布的清单文档里（每台设备可带 installed：构建名和基础构建，来源类型“声明”）；阶段 2 起观察层（K03）里的“观察”，等级高于声明 |
管理员，之后是执行器 | 少到中 |
声明与观察永远分开显示；没有观察支持的版本，结论里写“声明，未核对”，不升成事实（I03）。
4. 核心要加的东西（通用，不含设备、台架或产品的词）
C1 模型和合约先行。 动作种类加“租约”；D04 R[0] 的“租约按运行持有”补一句预订类租约按血缘（W06）持有，以预订运行为前驱的运行沿用同一份租约，由 Hub 在派发时核对前驱关系——这是模型修订，不是澄清，要告诉所有者；运行上下文的封闭列表（现在只有 builds）加 leases；工作流声明里加 leases: { prefix, max_ttl }；运行记录加 leases 字段；租约相关的错误码进登记表（LEASE_UNAVAILABLE、LEASE_EXPIRED、FENCING_STALE，现有登记表里还没有）。生成器重新生成。
C2 租约服务（hub/leases）。 一张表，键唯一；取得就是插入：键上有未过期的行则 LEASE_UNAVAILABLE（带上那行的到期时刻当最早空闲时刻），有过期的行则在一条语句里原子抢占，抢不到说明刚被别人拿走。多个键要么全成功、要么全失败。围栏令牌是行上单调递增的数，每次取得或续期加一。过期一律按数据库的时钟算（expires_at <= now() 写在 SQL 里），Hub 进程的时钟只用来显示。期限由持有者申请、受包声明的上限约束；续期、释放；管理员强制释放，留下动作记录和理由。持有者记运行号和用户；令牌不交给客户端，客户端只拿租约号。没有后台清理任务：过期行留在原地，下一次取得时抢占。复核否决了先前稿里“比较并交换加最多三次重试”：两个人同时订同一台架恰好一个该赢，不需要重算，唯一约束更简单，也更好测（两条连接同时插入）。
C3 start_run 接线。 先例是 context: ["builds"]：工作流声明要什么上下文，运行开始时冻结。leases 给出按前缀过滤的当前租约表，附冻结时刻。纯函数投影可以在结果里返回 lease_requests（键、期限）。顺序：投影 → Hub 检查键都在声明的前缀下、期限不超上限 → 取得租约（自带事务）→ 把租约号、键、到期写进运行记录 → 存运行。存运行失败就立刻释放刚取得的租约；进程在取得和存运行之间崩溃留下的行，因为它引用的运行不存在，一分钟后被当作空闲。取得失败时 start_run 不受理（D05：效果写入不受理才算 isError），错误码 LEASE_UNAVAILABLE，修正说明里写最早空闲时刻；这是确定的否定回答，不是未知，运行也不存。投影之前先取一次租约视图交给投影（投影要靠它避开已被占的台架），这份视图原样存进运行记录，用记录里的上下文重跑投影得到同样的请求。不加工具：全部经 start_run。
C4 管理员命名文档。 circle-hub doc put <名字> <文件>（只有管理员）把文件存成源文件并移动命名指针；外部标识 doc:<名字>（当前那份）和 doc:<名字>@<摘要>（指定那份）由 Hub 内部读取器作答；工作流把它绑到输入槽，用核心的 JSON 解析器解析，包里的函数校验结构并建出台架模型。这是通用的：以后别的管理员声明的参考文档（地址规划、策略表的部署行）用同一条路。复核比较过的另外两条路：把清单挂成知识树（知识的读取以产品线为键，同步循环读的是外部对象，product@1 的名称族、版本线、发布等字段在这里没有意义，要么凑数、要么改知识包 300 到 500 行）和把设备登记成资源（资源的形状全是 HTTP 基址和只读路由，要泛化，400 到 600 行），都比这条重。
5. 包里放什么（test-bed 包族）
- 清单：拓扑文件的形状是设备
{name, type, ipv4[], ipv6[]}加服务{host, ip, proto, port}；设备类型取负载均衡、路由器、客户端、服务器、控制台这几类。包里的函数负责校验：重复的地址、落不进任何接口地址段的地址、同一设备同一地址出现两次，一律整份拒绝并指出位置。 - 工作流
bed-search（只产生事实）：输入需要的设备类型和数量、构建、时长；输出满足条件的台架，各写明：Hub 记录里现在空闲，或最早空闲时刻；设备上的构建与要求的是否一致（精确同名，或 FAMY 名字对应同一 FAMX 构建，沿用构建别名的规则）；不一致写“需要升级”；版本来源是声明还是观察。 - 工作流
bed-booking，参数action：acquire（选定台架或让包按最佳匹配选）、extend、release。投影函数产出租约意图，Hub 取得。结果：台架、租约号、到期时刻；否定时写原因。 - 工作流
bed-facts（只产生事实）：对一个台架算环境事实：可达网段、监听地址与触发设备的配对、没有触发设备的网段上的“盲”地址、可分配的空闲地址（扣除保留段和别人占着的）。 - 用户自报版本（
bed-version）阶段 1 不做：阶段 1 的版本只来自管理员发布的清单文档（改版本就发布新的一份），因为用户自报要有一条写声明类主张的通道，现在没有；阶段 2 有了执行器观察，自报也就不需要了。 - 地址分配：
bed-booking的参数addresses要几个、在哪个地址段；分配的地址也是租约键（ip/<地址段>/<地址>），期限与预订相同，释放时一并释放。
阶段 2 加 bed-observe（执行器取版本和接口地址，写观察，与声明比对）。阶段 3 加 bed-upgrade。两个都要所有者先给出第 2 节表里列的东西。
6. 角色、可见性和诚实的未知
- 用户：搜索，预订自己要用的，续期和释放自己的，给自己持有的设备报告版本。管理员：发布和替换清单，强制释放，设上限。仍然只有用户和管理员两种角色（R01）；这个包族像别的包一样按分配使用。
- 占用者对其他用户是否可见：建议同一个包的使用者能看到“被占用至 HH:MM，占用者是谁”，因为实验室里要知道找谁；这是实验室信息，不是用例数据。所有者定。
- D02 的前提默认为假：阶段 1 的一切占用结论都写“Hub 记录里空闲（未排除本地操作）”，不写“台架空闲”。租约只对经 Hub 派发的操作强制；台架上有人直接登录，Hub 排除不了。要等目标一侧能强制同一租约（例如设备控制台只能经持有租约的通道进入），这句限定才能去掉。
- 过期不等于干净：阶段 3 的操作在过期时还在进行，则操作记未知、台架冻结、等处置（D04），不自动重派。
- 失败路径（复核补的，已定）：Hub 重启不丢租约（在数据库里），没提交的取得随事务回滚；同一用户对同一键再订一次得到
LEASE_UNAVAILABLE，最早空闲时刻是自己的到期时刻，要续就用extend；清单修订不检查占用（清单是事实，占用是意图），清单里没有了的设备如果还被占着，bed-facts报未知并警告，管理员可以强制释放；强制释放不作废持有者的运行（运行是不可变记录），但之后对这台设备的派发会因为围栏令牌变了被拒。
7. 验收（阶段 1，合成数据，真实 Circle 客户端经 Otty 驱动已部署的 Hub）
- 搜索：三个台架（一个空闲且构建一致，一个占用中，一个构建不一致）得到正确的排序和原因。
- 预订成功：租约号、到期时刻；再预订同一台设备被拒，写明最早空闲时刻。
- 两条连接同时预订同一台架：恰好一个成功（并发测试，直接插入，不靠运气）。
- 续期未过期的成功、过期后的被拒；超过总上限被拒；释放后别人能订；管理员强制释放留下记录；过期行被下一个预订者原子抢占。
- 地址：分配不重复；释放后可再分；保留段不会被分出。
- 拓扑文件有重复地址或落不进地址段：整份拒绝并指明位置；合法的新文档发布后，新运行用新摘要，旧运行里冻结的摘要不变。
- 版本：清单里写了
installed的设备，搜索结果按“声明”显示它装的构建；没有installed的设备写“无记录”，不当作不一致；FAMY 名字和它基于的 FAMX 构建算同一构建。 - 环境事实：监听地址落在没有触发设备的网段上，被标为盲地址；有触发设备的网段上的接口地址可用。
- 崩溃窗口：取得租约之后、存运行之前失败，租约被补偿释放；孤儿行一分钟后被当作空闲。
- 非管理员和未分配该包的人：同样的“对你不可用”和空集。
- 每一步都在调用日志里一行；参数只有摘要和大小。
8. 拆分
核心先行，包随后；C1 最先，C4 可以和 C2 并行。
| 项 | 内容 | 大小 |
|---|---|---|
| C1 | 模型、合约、生成物（4 节 C1） | 300 到 400 行 |
| C2 | hub/leases（4 节 C2），含并发、抢占、强制释放、围栏的测试 |
500 到 700 行 |
| C3 | start_run 接线，含补偿和孤儿的测试（4 节 C3） |
200 到 300 行 |
| C4 | 管理员命名文档和内部读取器（4 节 C4） | 300 到 450 行 |
| C5 | 管理员命令 lease list、lease release … --reason（强制释放），生产装配接上租约服务 |
100 到 200 行 |
| P1 | 清单校验函数和模型 | 200 到 300 行 |
| P2 | bed-search |
200 行 |
| P3 | bed-booking（含地址） |
300 行 |
| P4 | bed-facts |
200 到 300 行 |
| P5 | 验收和真实 Circle 场景（第 7 节） | 200 到 300 行 |
9. 还没证明、要所有者给或定的
- 阶段 1 证明的是 Hub 的逻辑，不是设备上的事实：版本是声明的，占用是 Hub 内的，台架上的本地操作排除不了。
- 要所有者知道的模型修订：D04 R[0] 加一句血缘持有；动作种类加“租约”（4 节 C1）。
- 要所有者定：占用者是否对其他用户可见（6）；预订的默认和最大期限（建议默认 2 小时、单次最多 8 小时、累计最多 24 小时）；拓扑文件由谁、从哪里导出。
- 阶段 2 要所有者给：用哪几个台架、用哪个账号（密钥只经密钥库命令进 Hub）、允许的只读命令类（建议只列“查看版本”“查看接口地址”两类）、执行器跑在哪台机器上。阶段 3 另行批准，每一类命令一条。
- 编译半边（用例转成执行用的工作簿并过静态检查）不在本页：它依赖这里的
bed-facts，还要一份执行用的函数合约（哪些步骤函数可用）和执行入口，这两样现在不在本仓库，也不能从旧系统抄；设计在这里的核心落地之后另写。