-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
-- Copyright (c) 2026 2youg1 and the sprawling contributors
/-!
# wire::answer::sessions
规定 `answer::sessions`（`crates/wire/src/` 下同名的文件）。一个房间的各段 session，新的在前。本文件是 `crates/wire/Spec.lean` 的一个分部；下面每一节保留它在 wire 规格里的标签 §8-n，别处引作 `crates/wire/Spec.lean §8-n`，决定引作 `wire D<n>`。
这一分部只有文字：它是说明文档，不是形式规格，这里没有一句是被证明的；它写下的帧形状由 Rust 的类型与 `crates/wire/tests/wire_contract.rs` 钉住的 wire schema（`wire::schema_hash`）守住。
-/
/-!
### 8-71 一个房间的各段 session：`Query::Sessions { room }`、`Answer::Sessions`
```rust
Query::Sessions { room: Address }
Answer::Sessions(SessionsAnswer)
pub const SESSIONS_MAX: usize = 64;
pub struct SessionsAnswer {
pub room: Address, // 问题的回声
pub sessions: Vec<SessionLine>, // 新的在前，至多 SESSIONS_MAX 段
pub earlier: u64, // 比这一答最旧的一段还早、没列出的段数
}
pub struct SessionLine {
pub began: Seq, // 这一段的第一行：它的 `session_opened`，或房间由派活打开时的第一个 `run_started`
pub start: SessionStart,
pub runs: u64, // 这一段里起过的 run
pub last: Seq, // 这一段里账本记在这个地址下的最后一行
pub at: TimeMs, // 那一行的时刻
}
pub enum SessionStart {
Dispatched { by: Option<Who> }, // 房间由派活打开，没有 `session_opened`；`by` 见 D40
Opened { carry: Carry, from: Option<Origin> }, // `/new`：带过去的是什么，从哪里分叉（分叉时）
}
```
- **为什么。** 页面对一个房间的历史只知道热视图里的 run（最近冻结的 32 个加上在跑的）和本次打开以后收到的记录，所以重载之后看不到更早一段的边界，房间信箱的「最近」段（refrain 路线图 S7.5）没有东西可列。session 是房间的一段（`docs/glossary.md` 的 Session），它的边界与起法都在账本里：`session_opened` 带着 `carried` 与 `from`，房间第一次被派活打开时没有这一行，第一行是那个 `run_started`。
- **字段读自账本的哪一行。** `began` 是那一段的第一行；`start` 是 `Opened` 时，`carry` 由 `session_opened.carried` 读出（`true` 即 `Carry::Handoff`：上一段的交接真的带过去了），`from` 原样是它的 `from`；`runs` 数这一段里地址是这个房间的 `run_started`；`last` 与 `at` 是这一段里地址是这个房间的最后一行与它的 `t`，与 `storage::sessions` 为这个房间切的那份切片是同一组行（`crates/storage/Spec.lean` §8-24）。地址不是房间的记录（模型调用、工具调用）不挪 `last`：它们属于 run，run 的进度由 `Query::RunView` 回答。
- **作答在锁内，不读盘。** 视图折叠一张按地址的表（`crates/accounting/Spec.lean` §8-19(c)），`Query::Sessions` 只从这张表里拷出这个房间最新的至多 `SESSIONS_MAX` 段，没有一行账本被读；一个房间从没有过 session 时答空表、`earlier` 为 0，与「这个地址不存在」不作区分，因为房间是目录，答它在不在是 `Query::Listing` 的事。
- **新的在前，一次至多 64 段，没有翻页。** 读它的是「最近」段，要的是最近几段；`earlier` 说出更早的还有多少，页面据此说「更早的 n 段不在此处」而不是假装没有。
- **只动名字表，不进 `WIRE_V`。** 新加一个查询与一个答复，旧帧一个也没改形；名字表多一项，schema 哈希随之变（D1、§4）。
-/
/-! D9 一个房间的 session 列表从视图折叠作答，不从按地址的索引读账本
**决定**：视图多折一张按地址的表，每个地址一列 `SessionLine`；`Query::Sessions` 在锁内拷出这个房间最新的至多 64 段（§8-71）。问题只带 `room`，不带翻页游标。
**理由**：每一段要的四个事实（起点、起法、run 数、最近一次活动）在折叠时一行一行就能定下，表的大小与 session 数同阶，而 session 数不超过 run 数；40 万行夹具城（8,000 个 run、40 个房间）上这张表让视图快照多 948 B（共 15,859,057 B），一个房间作答在 25 µs 以内，不读账本。按地址的索引要在作答时把这个房间的每个 `run_started` 与 `session_opened` 从盘上读回、解析，才能数出 run 数与起法；同一座夹具城上一个房间就是 200 行。
**被否**：①`storage::index` 加一张按地址的表——索引多出与带地址的行同阶的条目（夹具城上 80,000 条），每次作答再读几百行；②问题带 `before` 与 `limit` 翻页——读者是「最近」段，最近 64 段之外它只需要知道还有多少，`earlier` 已经说出。
**重开参数**：页面要浏览一个房间全部的段（不只是最近）时，加 `before` 游标；房间数或 session 数大到这张表在视图快照里成为可见的一段解码时间时，改成按地址的索引。
-/
/-! D27 一段 session 带出显示名、模型、思考强度、工作区与最后一条回复；改名与改运行策略各是一帧命令
**决定**：`SessionLine` 多五件，全是 `#[serde(default)]`：
```rust
pub struct SessionLine {
// …既有字段…
pub name: Option<String>, // 最后一行 `session_named` 的名字（kernel D22）；缺席即显示地址
pub model: Option<String>, // 这一段最后一次 run 的 `model_called.model`
pub effort: Option<Effort>, // 这一段最后一次 run 的 `run_started.effort`
pub workspace: Option<String>, // 这一段最后一次 run 被借给的工作树的名字（`worktree_opened`）
pub preview: Option<String>, // 最后一条回复的正文开头，至多 SESSION_PREVIEW_MAX 个字符，裁剪由页面按宽度再做
}
```
命令面多两帧，都是 `Reach::client`、`VerbClass::Act`：`Command::NameSession { room: Address, began: Seq, name: String, idem }` 写 `session_named`；`Command::ChangeRunPolicy { room: Address, policy: kernel::RunPolicy, idem }` 写 `run_policy_changed`（kernel D21），正在跑的 run 在下一个安全点生效。标签不加帧：它们照旧经 `PutPreferences` 的 `tags`（D21）；没有标签时页面按 `workspace` 给一个默认标签。两帧与上面的五件随 V0.0.9 的那一次 `WIRE_V` 进位（D22）；`Command` 的 `inductive` 由实现它们的变更集同时加臂（`specalign` 逐臂对账），`client/src/wire.ts` 与 `xtask wiring` 的可达表同改。
**理由**：检阅页要每行说出模型、思考强度与工作区，预览要最后一条回复（roadmap A28）；这些都在视图已经折叠的那张按地址的表能读到的行里，所以作答仍在锁内、不读盘。`preview` 设上限，是因为一条回复可以很长，而这一答一次带至多 `SESSIONS_MAX` 段。
**被否**：①页面为每段再问一次 `Rounds` 拼出这几件：一屏几十次往返；②`preview` 带整条回复：答复的大小随回复长度无界。
**重开参数**：页面要一段里多个模型的历史时（会话中不换模型，今天只有一个），`model` 改成表。
-/
/-! D40 一个被派出的 run 说出派它的 run；一段由派活打开的 session 说出是谁派的
**决定**：`Opening` 多一件 `#[serde(default)] parent: Option<RunId>`，原样读自这个 run 的 `run_started.parent`；`SessionStart::Dispatched` 由单元臂改成 `Dispatched { by: Option<Who> }`，`by` 读自这一段第一个 `run_started` 的 `dispatched_by`。两处都只读账本已经写下的那一行，旧行没有这个键时为 `None`，页面不猜。改形，`WIRE_V` 进一位。
**理由**：被派出的孩子的对话页要链回派它的那个 session，房间信箱的每一段要说出谁派的（roadmap UC6）；`Opening` 只带派活的房间（`dispatched_by`），一个房间里先后有很多 run，从房间猜不出是哪一个 run 派的。信箱若为每一段再问一次 `Rounds` 才知道派活者，一屏是几十次往返（与 D27 被否的①同理）。
**被否**：①页面从 `RunSummary` 的列表里按时间猜父 run：同一房间并发的两个 run 会猜错；②在 `SessionLine` 上另加一个 `dispatched_by` 字段：它只对 `Dispatched` 有意义，挂在 `Opened` 段上永远是 `None`，一个不可能的组合就能写出来。
**重开参数**：一个 run 可以由多个父 run 共同派出时，`parent` 改成表。
**三个平台**：只读账本、只折叠，Windows、macOS、Linux 相同。
-/