sprawling-kernel 0.0.10

-- 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

/-!
# kernel::registry

规定 `kernel::registry`（`crates/kernel/src/registry.rs`）：产物、资产与居民的登记。本文件是 `crates/kernel/Spec.lean` 的一个分部；下面每一节保留它在 kernel 规格里的标签 §8-n，别处引作 `crates/kernel/Spec.lean §8-n`。

这一分部只有文字：它是说明文档，不是形式规格，这里没有一句是被证明的；它写下的接口形状与取舍由 Rust 的类型与 `kernel::registry` 旁的测试守住。
-/

/-!
### 8-18 kernel::registry

```rust
pub struct ResidentId(String);               // 非空；`role@building.n` 文法 P1 随 city::resident 收紧
impl ResidentId { pub fn new(raw: impl Into<String>) -> Option<ResidentId>;  // 空串即 None
                  pub fn as_str(&self) -> &str; }
pub struct Claim { pub locator: Locator, pub by: String }        // 证词：未验证产出
pub struct Artifact { /* locator, verified_by —— 私有 */ }
impl Artifact {
    /// Sole constructor: player–referee in the type. Verification evidence
    /// must cite a kind in `completion::CITABLE`, else E_EVIDENCE_MISSING.
    pub fn verify(claim: Claim, evidence: EventRef) -> Result<Artifact, AxError>;
    pub fn locator(&self) -> &Locator;  pub fn verified_by(&self) -> &EventRef;
}

pub struct Registry { /* artifacts: BTreeMap<String, Artifact>, assets: BTreeSet<String>,
                         residents: BTreeSet<ResidentId> —— 私有 */ }
pub enum RegisterVerdict { Registered, AlreadyRegistered }
impl Registry {
    pub fn new() -> Registry;
    pub fn register_artifact(&mut self, artifact: Artifact) -> RegisterVerdict;   // 键＝locator 规范拼写
    pub fn promote_asset(&mut self, locator: &Locator) -> Result<RegisterVerdict, AxError>; // 未登记 → E_PATH_NOT_FOUND
    pub fn register_resident(&mut self, id: ResidentId) -> RegisterVerdict;
    pub fn artifact(&self, locator: &Locator) -> Option<&Artifact>;
    pub fn is_asset(&self, locator: &Locator) -> bool;
    pub fn is_asset_at(&self, addr: &Address) -> bool;           // 有一条 file: 资产恰在此地址（内容钉不同，地方相同）
    pub fn is_resident(&self, id: &ResidentId) -> bool;
}
```

- Registry 是值不是存储：状态住调用方；kernel 只定登记规则与查询面。
- 评分归 eval（P3）；promotion 只登记不评分。
- **资产不让删除停下来**：Discard 门不读 `is_asset` 与 `is_asset_at`（§8-26「规模与归属不改答」）；登记的用处是保存把资产放回去所需的凭据。两个查询只回答登记里有什么。
-/