refactor(spec): clean prose patterns across all modules

Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出, 臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意. No code definitions changed, only doc comments.
fix(spec): replace @Claude with @bot in Prelude and Run
2026-07-13 11:26:23 +08:00 · 2026-07-12 18:55:52 +08:00 · 2026-07-12 18:43:11 +08:00 · 2026-07-12 18:38:45 +08:00 · 2026-07-12 18:38:17 +08:00 · 2026-07-12 15:54:16 +08:00
47 changed files with 430 additions and 1067 deletions
@@ -11,6 +11,9 @@
 # regenerable, not for VCS. The embedded engine mounts cph-render directly.
 render/vendor/local-packages/

+# Environment
+.env
+
 # Node (hub/ TS workspace and any future JS package)
 node_modules/

@@ -1,59 +0,0 @@
-#!/usr/bin/env node
-
-import { readdir, readFile, realpath } from "node:fs/promises";
-import { dirname, relative, resolve, sep } from "node:path";
-
-const rootArgument = process.argv[2];
-if (!rootArgument) throw new Error("usage: build_legacy_project_manifest.mjs <legacy-workspaces-root>");
-const root = await realpath(rootArgument);
-const projectFiles = await findProjectFiles(root);
-const seenIds = new Set();
-const manifest = [];
-for (const projectFile of projectFiles) {
-  const metadata = JSON.parse(await readFile(projectFile, "utf8"));
-  if (typeof metadata.id !== "string" || metadata.id.trim() === "") {
-    throw new Error(`project metadata has no id: ${projectFile}`);
-  }
-  if (seenIds.has(metadata.id)) throw new Error(`duplicate project id: ${metadata.id}`);
-  seenIds.add(metadata.id);
-  if (typeof metadata.name !== "string" || metadata.name.trim() === "") {
-    throw new Error(`project metadata has no name: ${projectFile}`);
-  }
-  const projectRoot = dirname(projectFile);
-  const sourceRelativePath = relative(root, projectRoot).split(sep).join("/");
-  const physicalFolderPath = dirname(sourceRelativePath) === "."
-    ? []
-    : dirname(sourceRelativePath).split("/");
-  if (metadata.folderPath !== undefined && (
-    !Array.isArray(metadata.folderPath)
-    || metadata.folderPath.some((part) => typeof part !== "string")
-    || JSON.stringify(metadata.folderPath) !== JSON.stringify(physicalFolderPath)
-  )) {
-    process.stderr.write(`[legacy-manifest] stale metadata folderPath; using physical path: ${projectFile}\n`);
-  }
-  manifest.push({
-    legacyId: metadata.id,
-    name: metadata.name,
-    folderPath: physicalFolderPath,
-    sourceRelativePath,
-  });
-}
-manifest.sort((left, right) => left.sourceRelativePath.localeCompare(right.sourceRelativePath, "zh-CN"));
-process.stdout.write(`${JSON.stringify(manifest, null, 2)}\n`);
-
-async function findProjectFiles(directory) {
-  const entries = await readdir(directory, { withFileTypes: true });
-  const projectMetadata = entries.find((entry) => entry.isFile() && entry.name === "project.json");
-  if (projectMetadata !== undefined) return [resolve(directory, projectMetadata.name)];
-  const found = [];
-  for (const entry of entries) {
-    if (entry.name === ".trash") continue;
-    const path = resolve(directory, entry.name);
-    if (entry.isSymbolicLink()) {
-      process.stderr.write(`[legacy-manifest] skip untracked symbolic link: ${path}\n`);
-      continue;
-    }
-    if (entry.isDirectory()) found.push(...await findProjectFiles(path));
-  }
-  return found;
-}
@@ -1,12 +1,12 @@
 {
  "name": "@paradigm/hub",
-  "version": "0.0.22",
+  "version": "0.0.20",
  "lockfileVersion": 3,
  "requires": true,
  "packages": {
    "": {
      "name": "@paradigm/hub",
-      "version": "0.0.22",
+      "version": "0.0.20",
      "dependencies": {
        "@anthropic-ai/claude-agent-sdk": "^0.3.202",
        "@fastify/cookie": "^11.0.2",
@@ -1,6 +1,6 @@
 {
  "name": "@paradigm/hub",
-  "version": "0.0.22",
+  "version": "0.0.20",
  "private": true,
  "type": "module",
  "engines": {
@@ -1,48 +0,0 @@
-import { readFile } from "node:fs/promises";
-import { prisma } from "../db.js";
-import { importLegacyProjects, type LegacyProjectManifestEntry } from "./legacyProjectImport.js";
-import { readSiloOrganizationId } from "./silo.js";
-
-async function main(argv: readonly string[]): Promise<void> {
-  const options = parseOptions(argv);
-  const organizationId = readSiloOrganizationId();
-  const manifest = JSON.parse(await readFile(required(options, "manifest"), "utf8")) as unknown;
-  if (!Array.isArray(manifest)) throw new Error("legacy import manifest must be a JSON array");
-  const state = await importLegacyProjects({
-    prisma,
-    organizationId,
-    actorFeishuOpenId: required(options, "actor-open-id"),
-    workspaceRoot: required(options, "workspace-root"),
-    sourceRoot: required(options, "source-root"),
-    stateFile: required(options, "state-file"),
-    projects: manifest as LegacyProjectManifestEntry[],
-    onProgress: (message) => console.error(`[legacy-import] ${message}`),
-  });
-  console.log(JSON.stringify({ imported: Object.keys(state.projects).length }));
-}
-
-function parseOptions(args: readonly string[]): Map<string, string> {
-  const options = new Map<string, string>();
-  for (let index = 0; index < args.length; index += 2) {
-    const flag = args[index];
-    const value = args[index + 1];
-    if (flag === undefined || !flag.startsWith("--") || value === undefined) {
-      throw new Error(`expected --name value, got: ${args.slice(index).join(" ")}`);
-    }
-    options.set(flag.slice(2), value);
-  }
-  return options;
-}
-
-function required(options: ReadonlyMap<string, string>, name: string): string {
-  const value = options.get(name)?.trim();
-  if (!value) throw new Error(`--${name} is required`);
-  return value;
-}
-
-main(process.argv.slice(2))
-  .catch((error) => {
-    console.error(error instanceof Error ? error.message : String(error));
-    process.exitCode = 1;
-  })
-  .finally(async () => prisma.$disconnect());
@@ -1,369 +0,0 @@
-import { createHash } from "node:crypto";
-import { cp, lstat, mkdir, readFile, readdir, realpath, rename, rm, writeFile } from "node:fs/promises";
-import { dirname, isAbsolute, join, relative, resolve, sep } from "node:path";
-import type { PrismaClient } from "@prisma/client";
-import { createFolder, createProjectFromOrgAdmin } from "../projectOnboarding.js";
-
-export interface LegacyProjectManifestEntry {
-  readonly legacyId: string;
-  readonly name: string;
-  readonly folderPath: readonly string[];
-  readonly sourceRelativePath: string;
-}
-
-export interface LegacyProjectImportState {
-  readonly version: 1;
-  readonly projects: Readonly<Record<string, {
-    readonly status: "PENDING" | "COMPLETED";
-    readonly projectId: string;
-    readonly workspaceDir: string;
-    readonly importedAt: string;
-    readonly sourceRelativePath: string;
-  }>>;
-}
-
-export async function importLegacyProjects(input: {
-  readonly prisma: PrismaClient;
-  readonly organizationId: string;
-  readonly actorFeishuOpenId: string;
-  readonly workspaceRoot: string;
-  readonly sourceRoot: string;
-  readonly stateFile: string;
-  readonly projects: readonly LegacyProjectManifestEntry[];
-  readonly onProgress?: (message: string) => void;
-}): Promise<LegacyProjectImportState> {
-  const sourceRoot = await realpath(input.sourceRoot);
-  const state = await readState(input.stateFile);
-  const projects = { ...state.projects };
-  const seen = new Set<string>();
-  for (const entry of input.projects) {
-    validateEntry(entry);
-    if (seen.has(entry.legacyId)) throw new Error(`duplicate legacy project id: ${entry.legacyId}`);
-    seen.add(entry.legacyId);
-    const sourceDir = await confinedSourceDir(sourceRoot, entry.sourceRelativePath);
-    const projectId = importedProjectId(input.organizationId, entry.legacyId);
-    const existing = await input.prisma.project.findUnique({ where: { id: projectId } });
-    const recorded = projects[entry.legacyId];
-    if (recorded !== undefined && (recorded.projectId !== projectId || recorded.sourceRelativePath !== entry.sourceRelativePath)) {
-      throw new Error(`legacy import state identity conflict: ${entry.legacyId}`);
-    }
-    if (recorded?.status === "COMPLETED" && existing === null) {
-      throw new Error(`legacy import state references missing project: ${entry.legacyId} -> ${recorded.projectId}`);
-    }
-    if (existing !== null) {
-      if (existing.organizationId !== input.organizationId || (recorded !== undefined && recorded.projectId !== existing.id)) {
-        throw new Error(`legacy import identity conflict: ${entry.legacyId} -> ${existing.id}`);
-      }
-      if (await hasCompletionMarker(existing.workspaceDir, entry)) {
-        await ensureImportAudit(input.prisma, existing.id, entry);
-        projects[entry.legacyId] = {
-          status: "COMPLETED",
-          projectId: existing.id,
-          workspaceDir: existing.workspaceDir,
-          importedAt: recorded?.importedAt || new Date().toISOString(),
-          sourceRelativePath: entry.sourceRelativePath,
-        };
-        await writeState(input.stateFile, { version: 1, projects });
-        input.onProgress?.(`skip ${entry.legacyId}: recovered completed import`);
-        continue;
-      }
-      if (recorded?.status !== "PENDING") {
-        throw new Error(`refusing to remove legacy project without a matching pending record: ${entry.legacyId}`);
-      }
-      input.onProgress?.(`recover ${entry.legacyId}: remove incomplete target`);
-      await removeIncompleteTarget(input.prisma, existing.id, existing.workspaceDir, input.workspaceRoot);
-    }
-    projects[entry.legacyId] = {
-      status: "PENDING",
-      projectId,
-      workspaceDir: "",
-      importedAt: "",
-      sourceRelativePath: entry.sourceRelativePath,
-    };
-    await writeState(input.stateFile, { version: 1, projects });
-    const folderId = await ensureFolderPath(input.prisma, input.organizationId, ["旧教学资产", ...entry.folderPath]);
-    input.onProgress?.(`import ${entry.legacyId}: ${entry.name}`);
-    const created = await createProjectFromOrgAdmin(input.prisma, {
-      organizationId: input.organizationId,
-      actorFeishuOpenId: input.actorFeishuOpenId,
-      name: entry.name,
-      workspaceRoot: input.workspaceRoot,
-      folderId,
-      projectId,
-    });
-    try {
-      await copyLegacyProject(sourceDir, created.workspaceDir, entry);
-    } catch (error) {
-      try {
-        await removeIncompleteTarget(input.prisma, created.projectId, created.workspaceDir, input.workspaceRoot);
-        delete projects[entry.legacyId];
-        await writeState(input.stateFile, { version: 1, projects });
-      } catch (cleanupError) {
-        throw new AggregateError(
-          [error, cleanupError],
-          `legacy project import and target cleanup failed: ${entry.legacyId}`,
-        );
-      }
-      throw new Error(`legacy project import failed: ${entry.legacyId}: ${errorMessage(error)}`, { cause: error });
-    }
-    await ensureImportAudit(input.prisma, created.projectId, entry);
-    projects[entry.legacyId] = {
-      status: "COMPLETED",
-      projectId: created.projectId,
-      workspaceDir: created.workspaceDir,
-      importedAt: new Date().toISOString(),
-      sourceRelativePath: entry.sourceRelativePath,
-    };
-    await writeState(input.stateFile, { version: 1, projects });
-  }
-  return { version: 1, projects };
-}
-
-async function ensureFolderPath(
-  prisma: PrismaClient,
-  organizationId: string,
-  parts: readonly string[],
-): Promise<string> {
-  let parentId: string | undefined;
-  for (const name of parts) {
-    const existing = await prisma.folder.findFirst({
-      where: { organizationId, parentId: parentId ?? null, name, archivedAt: null },
-      select: { id: true },
-    });
-    if (existing !== null) {
-      parentId = existing.id;
-      continue;
-    }
-    const created = await createFolder(prisma, {
-      organizationId,
-      name,
-      ...(parentId !== undefined ? { parentId } : {}),
-    });
-    parentId = created.id;
-  }
-  if (parentId === undefined) throw new Error("legacy import folder path is empty");
-  return parentId;
-}
-
-async function copyLegacyProject(
-  sourceDir: string,
-  workspaceDir: string,
-  entry: LegacyProjectManifestEntry,
-): Promise<void> {
-  const sourceWorkspace = join(sourceDir, "workspace");
-  await assertNoSymlinks(sourceWorkspace);
-  const names = await readdir(sourceWorkspace);
-  for (const name of names) {
-    if (name === ".claude" || name === ".cph") continue;
-    await cp(join(sourceWorkspace, name), join(workspaceDir, name), {
-      recursive: true,
-      force: false,
-      errorOnExist: true,
-      preserveTimestamps: true,
-      filter: (source) => {
-        const parts = relative(sourceWorkspace, source).split(sep);
-        return !parts.includes(".claude") && !parts.includes(".cph");
-      },
-    });
-  }
-  const legacyDir = join(workspaceDir, ".legacy-source");
-  await mkdir(legacyDir, { mode: 0o750 });
-  await cp(join(sourceDir, "project.json"), join(legacyDir, "project.json"), {
-    force: false,
-    errorOnExist: true,
-    preserveTimestamps: true,
-  });
-  const rawDir = join(sourceDir, "_raw");
-  await assertNoSymlinks(rawDir).catch((error: unknown) => {
-    if (isMissing(error)) return;
-    throw error;
-  });
-  await cp(rawDir, join(legacyDir, "raw"), {
-    recursive: true,
-    force: false,
-    errorOnExist: true,
-    preserveTimestamps: true,
-  }).catch((error: unknown) => {
-    if (isMissing(error)) return;
-    throw error;
-  });
-  await writeFile(join(legacyDir, "migration.json"), `${JSON.stringify({
-    source: "teaching-material-host-service",
-    legacyProjectId: entry.legacyId,
-    legacyPath: entry.sourceRelativePath,
-    migratedAt: new Date().toISOString(),
-  }, null, 2)}\n`, { mode: 0o640 });
-}
-
-function importedProjectId(organizationId: string, legacyId: string): string {
-  const digest = createHash("sha256")
-    .update("teaching-material-host-service\0")
-    .update(organizationId)
-    .update("\0")
-    .update(legacyId)
-    .digest("hex")
-    .slice(0, 32);
-  return `legacy_${digest}`;
-}
-
-async function hasCompletionMarker(
-  workspaceDir: string,
-  entry: LegacyProjectManifestEntry,
-): Promise<boolean> {
-  try {
-    const marker = JSON.parse(await readFile(join(workspaceDir, ".legacy-source", "migration.json"), "utf8")) as unknown;
-    return typeof marker === "object" && marker !== null
-      && "legacyProjectId" in marker && marker.legacyProjectId === entry.legacyId
-      && "legacyPath" in marker && marker.legacyPath === entry.sourceRelativePath;
-  } catch (error) {
-    if (isMissing(error)) return false;
-    if (error instanceof SyntaxError) {
-      throw new Error(`invalid legacy completion marker: ${workspaceDir}`, { cause: error });
-    }
-    throw error;
-  }
-}
-
-async function ensureImportAudit(
-  prisma: PrismaClient,
-  projectId: string,
-  entry: LegacyProjectManifestEntry,
-): Promise<void> {
-  const existing = await prisma.auditEntry.findFirst({
-    where: { projectId, action: "legacy_project.imported" },
-    select: { id: true },
-  });
-  if (existing !== null) return;
-  await prisma.auditEntry.create({
-    data: {
-      projectId,
-      action: "legacy_project.imported",
-      metadata: {
-        source: "teaching-material-host-service",
-        legacyProjectId: entry.legacyId,
-        legacyPath: entry.sourceRelativePath,
-      },
-    },
-  });
-}
-
-async function removeIncompleteTarget(
-  prisma: PrismaClient,
-  projectId: string,
-  workspaceDir: string,
-  workspaceRoot: string,
-): Promise<void> {
-  await assertConfinedExistingPath(workspaceRoot, workspaceDir);
-  const failures: unknown[] = [];
-  try {
-    await prisma.project.delete({ where: { id: projectId } });
-  } catch (error) {
-    failures.push(error);
-  }
-  try {
-    await rm(workspaceDir, { recursive: true, force: true });
-  } catch (error) {
-    failures.push(error);
-  }
-  if (failures.length > 0) throw new AggregateError(failures, `failed to remove incomplete legacy target: ${projectId}`);
-}
-
-async function assertConfinedExistingPath(root: string, path: string): Promise<void> {
-  const trustedRoot = await realpath(root);
-  const candidate = await realpath(path);
-  const rel = relative(trustedRoot, candidate);
-  if (rel === "" || rel === ".." || rel.startsWith("../") || isAbsolute(rel)) {
-    throw new Error(`refusing to remove path outside workspace root: ${path}`);
-  }
-}
-
-async function assertNoSymlinks(path: string): Promise<void> {
-  const metadata = await lstat(path);
-  if (metadata.isSymbolicLink()) throw new Error(`legacy import rejects symbolic link: ${path}`);
-  if (!metadata.isDirectory()) return;
-  for (const entry of await readdir(path)) await assertNoSymlinks(join(path, entry));
-}
-
-async function confinedSourceDir(sourceRoot: string, relativePath: string): Promise<string> {
-  const candidate = await realpath(resolve(sourceRoot, relativePath));
-  const rel = relative(sourceRoot, candidate);
-  if (rel === "" || rel === ".." || rel.startsWith("../") || isAbsolute(rel)) {
-    throw new Error(`legacy source path escapes source root: ${relativePath}`);
-  }
-  return candidate;
-}
-
-function validateEntry(entry: LegacyProjectManifestEntry): void {
-  if (typeof entry !== "object" || entry === null) throw new Error("invalid legacy project entry");
-  if (typeof entry.legacyId !== "string") throw new Error("legacy project id must be a string");
-  if (!/^[A-Za-z0-9_-]+$/.test(entry.legacyId)) throw new Error(`invalid legacy project id: ${entry.legacyId}`);
-  if (typeof entry.name !== "string") throw new Error(`legacy project name must be a string: ${entry.legacyId}`);
-  if (entry.name.trim() === "") throw new Error(`legacy project name is empty: ${entry.legacyId}`);
-  if (typeof entry.sourceRelativePath !== "string") {
-    throw new Error(`legacy source path must be a string: ${entry.legacyId}`);
-  }
-  if (entry.sourceRelativePath === "" || resolve("/", entry.sourceRelativePath) === "/") {
-    throw new Error(`invalid legacy source path: ${entry.legacyId}`);
-  }
-  if (!Array.isArray(entry.folderPath)) throw new Error(`legacy folder path must be an array: ${entry.legacyId}`);
-  for (const part of entry.folderPath) {
-    if (typeof part !== "string" || part.trim() === "" || part === "." || part === ".." || part.includes("/") || part.includes("\\")) {
-      throw new Error(`invalid legacy folder part for ${entry.legacyId}: ${part}`);
-    }
-  }
-}
-
-async function readState(path: string): Promise<LegacyProjectImportState> {
-  try {
-    const parsed = JSON.parse(await readFile(path, "utf8")) as LegacyProjectImportState;
-    if (parsed.version !== 1 || typeof parsed.projects !== "object" || parsed.projects === null) {
-      throw new Error(`invalid legacy import state: ${path}`);
-    }
-    for (const [legacyId, record] of Object.entries(parsed.projects)) validateStateRecord(path, legacyId, record);
-    return parsed;
-  } catch (error) {
-    if (isMissing(error)) return { version: 1, projects: {} };
-    throw error;
-  }
-}
-
-function validateStateRecord(path: string, legacyId: string, record: unknown): void {
-  if (typeof record !== "object" || record === null || Array.isArray(record)) {
-    throw new Error(`invalid legacy import state record: ${path}#${legacyId}`);
-  }
-  const values = record as Record<string, unknown>;
-  const expectedKeys = ["importedAt", "projectId", "sourceRelativePath", "status", "workspaceDir"];
-  if (Object.keys(values).sort().join("\0") !== expectedKeys.join("\0")) {
-    throw new Error(`invalid legacy import state fields: ${path}#${legacyId}`);
-  }
-  if (values.status !== "PENDING" && values.status !== "COMPLETED") {
-    throw new Error(`invalid legacy import state status: ${path}#${legacyId}`);
-  }
-  for (const field of ["projectId", "workspaceDir", "importedAt", "sourceRelativePath"] as const) {
-    if (typeof values[field] !== "string") throw new Error(`invalid legacy import state ${field}: ${path}#${legacyId}`);
-  }
-  if (values.projectId === "" || values.sourceRelativePath === "") {
-    throw new Error(`invalid legacy import state identity: ${path}#${legacyId}`);
-  }
-  if (values.status === "PENDING" && (values.workspaceDir !== "" || values.importedAt !== "")) {
-    throw new Error(`invalid pending legacy import state: ${path}#${legacyId}`);
-  }
-  if (values.status === "COMPLETED" && (values.workspaceDir === "" || values.importedAt === "")) {
-    throw new Error(`invalid completed legacy import state: ${path}#${legacyId}`);
-  }
-}
-
-async function writeState(path: string, state: LegacyProjectImportState): Promise<void> {
-  await mkdir(dirname(path), { recursive: true, mode: 0o750 });
-  const temporary = `${path}.tmp`;
-  await writeFile(temporary, `${JSON.stringify(state, null, 2)}\n`, { mode: 0o600 });
-  await rename(temporary, path);
-}
-
-function isMissing(error: unknown): boolean {
-  return typeof error === "object" && error !== null && "code" in error && error.code === "ENOENT";
-}
-
-function errorMessage(error: unknown): string {
-  return error instanceof Error ? error.message : String(error);
-}
@@ -22,7 +22,6 @@ export function buildUnboundChatOnboardingCard(params: {
  readonly folders: readonly OnboardingFolderOption[];
  readonly projects: readonly OnboardingProjectOption[];
  readonly canCreateProject: boolean;
-  readonly searchQuery?: string | undefined;
 }): Record<string, unknown> {
  const actions: unknown[] = [];
  if (params.canCreateProject) {
@@ -65,14 +64,7 @@ export function buildUnboundChatOnboardingCard(params: {
        `这个飞书群还没有绑定项目。`,
        ``,
        `组织: **${escapeMarkdown(params.organizationName)}**`,
-        ...(params.searchQuery === undefined || params.searchQuery === ""
-          ? [`可以选择 folder 新建项目并绑定到本群，或绑定你已经有管理权限的未绑定项目。`]
-          : [
-              `项目搜索: **${escapeMarkdown(params.searchQuery)}**`,
-              params.projects.length === 0
-                ? `没有匹配的未绑定项目。请 @bot 后换一个项目关键词。`
-                : `请选择匹配项目绑定到本群；如未找到，请 @bot 后换一个更具体的关键词。`,
-            ]),
+        `可以选择 folder 新建项目并绑定到本群，或绑定你已经有管理权限的未绑定项目。`,
      ].join("\n"),
    },
  ];
@@ -1070,12 +1070,10 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {

    const settings = await ensureOrganizationProjectSettings(deps.prisma, organization.organizationId);
    const canCreateProject = settings.membersCanCreateProjects || isOrgAdminRole(organization.role);
-    const searchQuery = (extractPrompt(msg) ?? "").trim().slice(0, 100);
    const projects = await listBindableProjectsForActor({
      organizationId: organization.organizationId,
      actorFeishuOpenId: senderOpenId,
      isOrgAdmin: isOrgAdminRole(organization.role),
-      searchQuery,
    });
    const folders = await listCreatableRootFolders(organization.organizationId);

@@ -1088,7 +1086,6 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
        folders,
        projects,
        canCreateProject,
-        searchQuery,
      }),
      sendOptionsForTriggerMessage(msg),
    );
@@ -1185,32 +1182,22 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
    readonly organizationId: string;
    readonly actorFeishuOpenId: string;
    readonly isOrgAdmin: boolean;
-    readonly searchQuery: string;
  }): Promise<readonly OnboardingProjectOption[]> {
-    const allowed: OnboardingProjectOption[] = [];
-    let cursor: string | undefined;
-    while (allowed.length < 5) {
    const candidates = await deps.prisma.project.findMany({
      where: {
        organizationId: input.organizationId,
        archivedAt: null,
        groupBindings: { none: { archivedAt: null } },
-        ...(input.searchQuery === "" ? {} : {
-          OR: [
-            { name: { contains: input.searchQuery, mode: "insensitive" } },
-            { folder: { name: { contains: input.searchQuery, mode: "insensitive" } } },
-          ],
-        }),
      },
      select: {
        id: true,
        name: true,
        folder: { select: { name: true } },
      },
-        orderBy: [{ updatedAt: "desc" }, { id: "desc" }],
+      orderBy: { updatedAt: "desc" },
      take: 20,
-        ...(cursor === undefined ? {} : { cursor: { id: cursor }, skip: 1 }),
    });
+    const allowed: OnboardingProjectOption[] = [];
    for (const project of candidates) {
      if (!input.isOrgAdmin) {
        const decision = await authorizer.can({
@@ -1227,10 +1214,6 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
      });
      if (allowed.length >= 5) break;
    }
-      if (candidates.length < 20) break;
-      cursor = candidates.at(-1)?.id;
-      if (cursor === undefined) break;
-    }
    return allowed;
  }

@@ -27,8 +27,6 @@ export interface CreateOrgAdminProjectInput {
  readonly workspaceRoot: string;
  readonly folderId?: string | undefined;
  readonly sortKey?: string | undefined;
-  /** Stable internal identifier for resumable imports; ordinary callers must omit it. */
-  readonly projectId?: string | undefined;
 }

 export interface CreateFeishuChatProjectInput {
@@ -149,7 +147,6 @@ export async function createProjectFromOrgAdmin(
    workspaceRoot: input.workspaceRoot,
    folderId: input.folderId,
    sortKey: input.sortKey,
-    projectId: input.projectId,
    chatId: undefined,
  });
 }
@@ -294,7 +291,6 @@ async function createManagedProject(
    readonly workspaceRoot: string;
    readonly folderId: string | undefined;
    readonly sortKey?: string | undefined;
-    readonly projectId?: string | undefined;
    readonly chatId: string | undefined;
  },
 ): Promise<ProjectOnboardingResult> {
@@ -305,7 +301,7 @@ async function createManagedProject(
  if (organization === null) throw new Error(`organization not found: ${input.organizationId}`);
  requireActiveOrganizationStatus(organization.id, organization.status);

-  const projectId = input.projectId ?? createProjectId();
+  const projectId = createProjectId();
  const workspaceDir = projectWorkspaceDir({
    workspaceRoot: input.workspaceRoot,
    organizationSlug: organization.slug,
@@ -1,185 +0,0 @@
-import { mkdir, mkdtemp, readFile, rm, symlink, unlink, writeFile } from "node:fs/promises";
-import { tmpdir } from "node:os";
-import { join } from "node:path";
-import { afterAll, afterEach, beforeEach, describe, expect, it } from "vitest";
-import { importLegacyProjects } from "../../src/deployment/legacyProjectImport.js";
-import { DEFAULT_ORG_ID, prisma, resetDb } from "./helpers.js";
-
-const temporaryRoots: string[] = [];
-
-describe("legacy teaching-material project import", () => {
-  beforeEach(async () => {
-    await resetDb();
-    await prisma.user.create({
-      data: {
-        id: "legacy-import-owner",
-        feishuOpenId: "ou_legacy_owner",
-        displayName: "Legacy Import Owner",
-        organizationMemberships: { create: { organizationId: DEFAULT_ORG_ID, role: "OWNER" } },
-      },
-    });
-  });
-
-  afterEach(async () => {
-    while (temporaryRoots.length > 0) {
-      const root = temporaryRoots.pop();
-      if (root !== undefined) await rm(root, { recursive: true, force: true });
-    }
-  });
-
-  afterAll(async () => prisma.$disconnect());
-
-  it("imports each legacy project as an unbound resumable project under its old folder path", async () => {
-    const sourceRoot = await temporaryRoot("cph-legacy-source-");
-    const workspaceRoot = await temporaryRoot("cph-legacy-target-");
-    const projectSource = join(sourceRoot, "物理", "M-243-牛顿力学");
-    await mkdir(join(projectSource, "workspace", "chapters"), { recursive: true });
-    await mkdir(join(projectSource, "workspace", ".claude"), { recursive: true });
-    await mkdir(join(projectSource, "workspace", "chapters", ".cph"), { recursive: true });
-    await mkdir(join(projectSource, "_raw"), { recursive: true });
-    await writeFile(join(projectSource, "workspace", "project.toml"), "title = \"牛顿力学\"\n");
-    await writeFile(join(projectSource, "workspace", "chapters", "lesson.typ"), "= 牛顿第二定律\n");
-    await writeFile(join(projectSource, "workspace", ".claude", "session.json"), "{}\n");
-    await writeFile(join(projectSource, "workspace", "chapters", ".cph", "runtime.json"), "{}\n");
-    await writeFile(join(projectSource, "project.json"), "{\"id\":\"M-243\"}\n");
-    await writeFile(join(projectSource, "_raw", "source.txt"), "legacy source\n");
-    const stateFile = join(workspaceRoot, "migration-state", "state.json");
-    const manifest = [{
-      legacyId: "M-243",
-      name: "牛顿力学",
-      folderPath: ["物理"],
-      sourceRelativePath: "物理/M-243-牛顿力学",
-    }];
-
-    const first = await importLegacyProjects({
-      prisma,
-      organizationId: DEFAULT_ORG_ID,
-      actorFeishuOpenId: "ou_legacy_owner",
-      workspaceRoot,
-      sourceRoot,
-      stateFile,
-      projects: manifest,
-    });
-    const imported = first.projects["M-243"];
-    expect(imported).toBeDefined();
-    if (imported === undefined) throw new Error("missing imported project state");
-
-    const project = await prisma.project.findUniqueOrThrow({
-      where: { id: imported.projectId },
-      include: { folder: { include: { parent: true } }, groupBindings: true },
-    });
-    expect(project.name).toBe("牛顿力学");
-    expect(project.folder?.name).toBe("物理");
-    expect(project.folder?.parent?.name).toBe("旧教学资产");
-    expect(project.groupBindings).toEqual([]);
-    await expect(readFile(join(imported.workspaceDir, "chapters", "lesson.typ"), "utf8"))
-      .resolves.toBe("= 牛顿第二定律\n");
-    await expect(readFile(join(imported.workspaceDir, ".claude", "session.json"), "utf8"))
-      .rejects.toMatchObject({ code: "ENOENT" });
-    await expect(readFile(join(imported.workspaceDir, "chapters", ".cph", "runtime.json"), "utf8"))
-      .rejects.toMatchObject({ code: "ENOENT" });
-    await expect(readFile(join(imported.workspaceDir, ".legacy-source", "project.json"), "utf8"))
-      .resolves.toContain("M-243");
-    await expect(readFile(join(imported.workspaceDir, ".legacy-source", "raw", "source.txt"), "utf8"))
-      .resolves.toBe("legacy source\n");
-
-    await unlink(stateFile);
-    const second = await importLegacyProjects({
-      prisma,
-      organizationId: DEFAULT_ORG_ID,
-      actorFeishuOpenId: "ou_legacy_owner",
-      workspaceRoot,
-      sourceRoot,
-      stateFile,
-      projects: manifest,
-    });
-    expect(second.projects["M-243"]?.projectId).toBe(imported.projectId);
-    await expect(prisma.project.count({ where: { organizationId: DEFAULT_ORG_ID } })).resolves.toBe(1);
-    expect(JSON.parse(await readFile(stateFile, "utf8"))).toMatchObject({
-      version: 1,
-      projects: { "M-243": { projectId: imported.projectId } },
-    });
-    await expect(prisma.auditEntry.count({
-      where: { projectId: imported.projectId, action: "legacy_project.imported" },
-    })).resolves.toBe(1);
-
-    await writeFile(join(imported.workspaceDir, ".legacy-source", "migration.json"), "not json\n");
-    await expect(importLegacyProjects({
-      prisma,
-      organizationId: DEFAULT_ORG_ID,
-      actorFeishuOpenId: "ou_legacy_owner",
-      workspaceRoot,
-      sourceRoot,
-      stateFile,
-      projects: manifest,
-    })).rejects.toThrow(/invalid legacy completion marker/);
-    await expect(prisma.project.count({ where: { id: imported.projectId } })).resolves.toBe(1);
-  });
-
-  it("rejects symlinks instead of importing paths outside the staged project", async () => {
-    const sourceRoot = await temporaryRoot("cph-legacy-symlink-");
-    const workspaceRoot = await temporaryRoot("cph-legacy-target-");
-    const projectSource = join(sourceRoot, "legacy");
-    await mkdir(join(projectSource, "workspace"), { recursive: true });
-    await writeFile(join(projectSource, "project.json"), "{}\n");
-    await symlink("/etc/passwd", join(projectSource, "workspace", "outside"));
-
-    await expect(importLegacyProjects({
-      prisma,
-      organizationId: DEFAULT_ORG_ID,
-      actorFeishuOpenId: "ou_legacy_owner",
-      workspaceRoot,
-      sourceRoot,
-      stateFile: join(workspaceRoot, "state.json"),
-      projects: [{ legacyId: "symlink", name: "Symlink", folderPath: [], sourceRelativePath: "legacy" }],
-    })).rejects.toThrow(/rejects symbolic link/);
-    await expect(prisma.project.count()).resolves.toBe(0);
-  });
-
-  it("rejects a manifest path that escapes the staged source root", async () => {
-    const parent = await temporaryRoot("cph-legacy-escape-");
-    const sourceRoot = join(parent, "source");
-    const outside = join(parent, "outside");
-    await mkdir(sourceRoot);
-    await mkdir(outside);
-
-    await expect(importLegacyProjects({
-      prisma,
-      organizationId: DEFAULT_ORG_ID,
-      actorFeishuOpenId: "ou_legacy_owner",
-      workspaceRoot: await temporaryRoot("cph-legacy-target-"),
-      sourceRoot,
-      stateFile: join(parent, "state.json"),
-      projects: [{
-        legacyId: "escape",
-        name: "Escape",
-        folderPath: [],
-        sourceRelativePath: "../outside",
-      }],
-    })).rejects.toThrow(/escapes source root/);
-  });
-
-  it("rejects malformed resume state before creating a project", async () => {
-    const sourceRoot = await temporaryRoot("cph-legacy-state-source-");
-    const workspaceRoot = await temporaryRoot("cph-legacy-state-target-");
-    const stateFile = join(workspaceRoot, "state.json");
-    await writeFile(stateFile, JSON.stringify({ version: 1, projects: { broken: { status: "MAYBE" } } }));
-
-    await expect(importLegacyProjects({
-      prisma,
-      organizationId: DEFAULT_ORG_ID,
-      actorFeishuOpenId: "ou_legacy_owner",
-      workspaceRoot,
-      sourceRoot,
-      stateFile,
-      projects: [],
-    })).rejects.toThrow(/invalid legacy import state fields/);
-    await expect(prisma.project.count()).resolves.toBe(0);
-  });
-});
-
-async function temporaryRoot(prefix: string): Promise<string> {
-  const root = await mkdtemp(join(tmpdir(), prefix));
-  temporaryRoots.push(root);
-  return root;
-}
@@ -361,100 +361,6 @@ describe("trigger full lifecycle (integration)", () => {
    expect(cardHeaderTitle(rt.sentPatches.at(-1))).toBe("已绑定项目");
  });

-  it("uses unbound-chat mention text to search bindable projects", async () => {
-    await seedOnboardingUser("u-onboard-search", "ou_onboard_search", "OWNER");
-    const folder = await prisma.folder.create({
-      data: { organizationId: DEFAULT_ORG_ID, name: "物理竞赛" },
-    });
-    await prisma.project.createMany({
-      data: [
-        {
-          id: "p-search-newton",
-          organizationId: DEFAULT_ORG_ID,
-          folderId: folder.id,
-          name: "牛顿力学专题",
-          workspaceDir: join(await tempWorkspaceRoot(), "p-search-newton"),
-        },
-        {
-          id: "p-search-optics",
-          organizationId: DEFAULT_ORG_ID,
-          folderId: folder.id,
-          name: "几何光学专题",
-          workspaceDir: join(await tempWorkspaceRoot(), "p-search-optics"),
-        },
-      ],
-    });
-    const trigger = makeTriggerHandler({
-      prisma,
-      settings,
-      logger: silentLogger,
-      runAgent,
-      projectWorkspaceRoot: await tempWorkspaceRoot(),
-    });
-
-    await trigger(makeEvent("chat-onboard-search", "@_user_1 牛顿", "ou_onboard_search"), rt);
-
-    expect(cardActionValues(rt.sentCards[0])).toContainEqual({
-      project_onboarding: {
-        action: "bind_project",
-        organization_id: DEFAULT_ORG_ID,
-        project_id: "p-search-newton",
-      },
-    });
-    expect(cardActionValues(rt.sentCards[0])).not.toContainEqual(expect.objectContaining({
-      project_onboarding: expect.objectContaining({ project_id: "p-search-optics" }),
-    }));
-    expect(JSON.stringify(rt.sentCards[0])).toContain("牛顿");
-    expect(runAgentCalls).toHaveLength(0);
-  });
-
-  it("continues searching past unauthorized matches for a manageable project", async () => {
-    await seedOnboardingUser("u-onboard-page", "ou_onboard_page", "MEMBER");
-    const workspaceRoot = await tempWorkspaceRoot();
-    await prisma.project.createMany({
-      data: [
-        ...Array.from({ length: 20 }, (_, index) => ({
-          id: `z-search-denied-${String(index).padStart(2, "0")}`,
-          organizationId: DEFAULT_ORG_ID,
-          name: `迁移项目 ${index}`,
-          workspaceDir: join(workspaceRoot, `denied-${index}`),
-        })),
-        {
-          id: "a-search-allowed",
-          organizationId: DEFAULT_ORG_ID,
-          name: "迁移项目 可管理",
-          workspaceDir: join(workspaceRoot, "allowed"),
-        },
-      ],
-    });
-    await prisma.permissionGrant.create({
-      data: {
-        resourceType: "PROJECT",
-        resourceId: "a-search-allowed",
-        principalType: "USER",
-        principalId: "ou_onboard_page",
-        role: "MANAGE",
-      },
-    });
-    const trigger = makeTriggerHandler({
-      prisma,
-      settings,
-      logger: silentLogger,
-      runAgent,
-      projectWorkspaceRoot: workspaceRoot,
-    });
-
-    await trigger(makeEvent("chat-onboard-page", "@_user_1 迁移", "ou_onboard_page"), rt);
-
-    expect(cardActionValues(rt.sentCards[0])).toContainEqual({
-      project_onboarding: {
-        action: "bind_project",
-        organization_id: DEFAULT_ORG_ID,
-        project_id: "a-search-allowed",
-      },
-    });
-  });
-
  it("batches quick text messages from the same chat and sender into one run", async () => {
    await seedProject("proj-1b", "chat-1b");
    const trigger = makeTriggerHandler({
@@ -1,63 +0,0 @@
-import { execFile } from "node:child_process";
-import { mkdir, mkdtemp, rm, symlink, writeFile } from "node:fs/promises";
-import { tmpdir } from "node:os";
-import { join, resolve } from "node:path";
-import { promisify } from "node:util";
-import { afterEach, describe, expect, it } from "vitest";
-
-const execute = promisify(execFile);
-const temporaryRoots: string[] = [];
-
-describe("legacy project manifest builder", () => {
-  afterEach(async () => {
-    while (temporaryRoots.length > 0) {
-      const root = temporaryRoots.pop();
-      if (root !== undefined) await rm(root, { recursive: true, force: true });
-    }
-  });
-
-  it("stops at a project root and excludes trash projects", async () => {
-    const root = await mkdtemp(join(tmpdir(), "cph-legacy-manifest-"));
-    temporaryRoots.push(root);
-    const projectRoot = join(root, "物理", "legacy__牛顿力学");
-    await mkdir(join(projectRoot, "workspace", "nested"), { recursive: true });
-    await mkdir(join(projectRoot, "_raw"), { recursive: true });
-    await mkdir(join(root, ".trash", "deleted"), { recursive: true });
-    await writeFile(join(projectRoot, "project.json"), JSON.stringify({
-      id: "legacy",
-      name: "牛顿力学",
-      folderPath: ["物理"],
-    }));
-    await writeFile(join(projectRoot, "workspace", "nested", "project.json"), "not metadata");
-    await writeFile(join(projectRoot, "_raw", "project.json"), "not metadata");
-    await writeFile(join(root, ".trash", "deleted", "project.json"), JSON.stringify({
-      id: "deleted",
-      name: "Deleted",
-    }));
-
-    const { stdout } = await execute(process.execPath, [
-      resolve("deploy/build_legacy_project_manifest.mjs"),
-      root,
-    ]);
-
-    expect(JSON.parse(stdout)).toEqual([{
-      legacyId: "legacy",
-      name: "牛顿力学",
-      folderPath: ["物理"],
-      sourceRelativePath: "物理/legacy__牛顿力学",
-    }]);
-  });
-
-  it("reports untracked symlinked entries instead of silently omitting them", async () => {
-    const root = await mkdtemp(join(tmpdir(), "cph-legacy-manifest-link-"));
-    temporaryRoots.push(root);
-    await symlink("/tmp", join(root, "linked-project"));
-
-    const result = await execute(process.execPath, [
-      resolve("deploy/build_legacy_project_manifest.mjs"),
-      root,
-    ]);
-    expect(result.stderr).toContain("skip untracked symbolic link");
-    expect(JSON.parse(result.stdout)).toEqual([]);
-  });
-});
@@ -49,7 +49,7 @@ agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是

 ### 命名

- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。
+- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Agent.Run`、`Spec.Courseware.Validity`。
 - **类型**:PascalCase。
 - **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
 - **文件粒度**:原则上"一个带独立不变式的概念一个文件"。
@@ -16,6 +16,6 @@ import Spec.Courseware.Open
 - **`Check`** —— checker 语义:`Severity` + 6 类诊断 + **合法 lesson = 无 error 级
  诊断**(模型外设施诊断以抽象谓词 + `Oracle` 表示);检查管线的 5 阶段、序、compile
  门控。
- **`Open`** —— 留白骨架(核心关系 OPEN,已 surface 不臆造):题库 `QuestionBank`、
+- **`Open`** —— OPEN 骨架(核心关系 OPEN,已 surface):题库 `QuestionBank`、
  课程编排 `Course`。
 -/
@@ -6,7 +6,7 @@ import Spec.Courseware.Export.Render

 产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
 修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
-本模块:钉级别类型(二分);钉 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
+定级别类型(二分);定 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
 error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
 型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
 说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
@@ -50,7 +50,7 @@ inductive DiagKind where

 /-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯
 `renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
-钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
+全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
 def DiagKind.severity : DiagKind → Severity
  | .partPathMissing    => .error
  | .unknownKind        => .error
@@ -5,8 +5,8 @@ import Spec.Courseware.Check.Diagnostic

 checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。
 顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不
-显示,这是有意的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):只钉**阶段、序、
-门控**。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
+显示,这是有意的)。每阶段的**算法**不进 Lean(深度上限:只定**阶段、序、
+门控**)。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
 `schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。
 -/

@@ -2,7 +2,7 @@
 # Artifact —— export target 的产物(ADR-0009 / 0011)

 ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011
-钉死:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
+固定:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
 是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String`
 承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。
 -/
@@ -4,7 +4,7 @@ import Spec.Courseware.Export.Artifact
 /-!
 # Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)

-ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build
+ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 固定 build
 的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。

 - `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
@@ -20,7 +20,7 @@ ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR

 **shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把
 `run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配
-内容)。三条边界是真分歧点,故钉契约:
+内容)。三条边界是真分歧点,故定为契约:
 1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生,
   绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。
 2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷;
@@ -46,7 +46,7 @@ namespace Spec.Courseware
 variable (P : Primitives)

 /-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;
-`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的
+`steps` 是 list 因为 FileTree / 第三方 build 会需多步。不把模板内部、shell 命令的
 解析结构写进来(实现细节, ADR-0011 OPEN)。 -/
 inductive Step where
  /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由:
@@ -7,7 +7,7 @@ import Spec.Courseware.Model.Info
 /-!
 # Courseware.Model —— 工程文件的内容模型

-留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
+基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
 (`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。
 决策出处 ADR-0005 / 0006 / 0008。
 -/
@@ -3,7 +3,7 @@ import Spec.Courseware.Model.Primitives
 /-!
 # Element —— 课程内容的原子单位

-ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把它编码成
+ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。把它编码成
 依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。
 -/

@@ -5,7 +5,7 @@
 基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
 **有序列表**,不是单值或可选单值。

-另有一条值得钉的模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
+另一条模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
 `author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态**只活在加载
 边界**:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端始终是
 `List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 `RawInfo`
@@ -24,7 +24,7 @@ inductive RawAuthor where
  | many (names : List String)

 /-- raw 作者归一化为**有序作者列表**(`PINNED`, ADR-0008)。单作者 ⇒ 单元素列表;数组
-⇒ 原样。这条钉死"canonical 接收端始终是 `List String`"。 -/
+⇒ 原样。canonical 接收端始终是 `List String`。 -/
 def RawAuthor.normalize : RawAuthor → List String
  | .one n => [n]
  | .many ns => ns
@@ -1,26 +1,26 @@
 /-!
-# Primitives —— Courseware 契约的留白基元
+# Primitives —— Courseware 契约的基元

 课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据
 schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化
 ——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给
-实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 钉死)与其表示进 Lean
+实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 固定)与其表示进 Lean
 是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象
-类型承载。富内容的 prose 母本见 `Courseware.RichContent`。
+类型承载。富内容的母本见 `Courseware.RichContent`。
 -/

 namespace Spec.Courseware

 /-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/
 structure Primitives where
-  /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。刻意用抽象
+  /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。用抽象
      类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方),
      封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/
  KindId : Type
  /-- 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED`
      ADR-0006,表示仍抽象)。以 kind 为索引:`ElementData k` 即"符合 `k` schema 的
-      数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)是 ADR-0006
-      钉死的,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
+      数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)由 ADR-0006
+      固定,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
      kind schema"这条关系,故此处仍是抽象类型。 -/
  ElementData : KindId → Type
  /-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次
@@ -1,5 +1,5 @@
 /-!
-# RichContent —— 富内容(ADR-0006 的 prose 母本)
+# RichContent —— 富内容(ADR-0006 的母本)

 ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**源文本**,
 按其 **format** 决定语义(ADR-0015)。两种 format:
@@ -13,7 +13,7 @@ ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**
 的一等文件,坐落在一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。markdown format
 的富内容不参与 typst 求值,但同样由一个虚拟路径定位(供 markdown 装配 step 按序读取,见 `Export/Render`)。

-本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
+只立锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
 具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。
 -/

@@ -33,8 +33,8 @@ inductive ContentFormat where
  | markdown

 /-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006),并带一个
-**format**(`PINNED`, ADR-0015)。刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事);
-只钉"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
+**format**(`PINNED`, ADR-0015)。不建模源文本、不建模求值出的 `Content`(那是实现侧的事);
+"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
 structure RichContentRef where
  /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/
  vpath : VPath
@@ -2,8 +2,8 @@ import Spec.Courseware.Open.QuestionBank
 import Spec.Courseware.Open.Course

 /-!
-# Courseware.Open —— 留白骨架(核心关系 OPEN)
+# Courseware.Open —— OPEN 骨架(核心关系)

 题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
-但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。
+但未决策的 OPEN 分歧点,待专门 ADR 落定。
 -/
@@ -5,6 +5,6 @@ ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程
 **编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被
 引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。

-按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺
+此处不替它选解——不建 `Course := List Lesson`(那会偷偷承诺
 "扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。
 -/
@@ -5,6 +5,6 @@
 典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确
 指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存?

-这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建
+这是一个 `OPEN` 分歧点。此处不替它选解——不建 `QuestionRef` 也不建
 内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。
 -/
@@ -1,10 +1,10 @@
 /-!
 # Prelude —— System 层共享标识符

-平台层反复引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。其内部表示从未被决策
-(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体
-`Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
-**关系**,却不对标识符表示作承诺。
+平台层引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。
+其内部表示从未被决策(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque
+载体 `Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
+关系,却不对标识符表示作承诺。
 -/

 namespace Spec.System
@@ -15,23 +15,33 @@ structure Identifiers where
  ProjectId : Type
  /-- SaaS 租户/组织标识(`OPEN` 表示;ADR-0020 tenant root)。 -/
  OrganizationId : Type
+  /-- 租户层用户标识(`OPEN` 表示;独立实体,非飞书身份派生;见 `Hierarchy.User`)。 -/
+  UserId : Type
+  /-- 飞书用户 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
+  FeishuOpenId : Type
+  /-- 飞书 user_id(`OPEN` 表示;租户内唯一,换 app 不变)。 -/
+  FeishuUserId : Type
+  /-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
+  FeishuAppId : Type
+  /-- 飞书 app_secret 信封引用(`OPEN` 表示;ADR-0024)。 -/
+  FeishuAppSecretRef : Type
  /-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
  TeamId : Type
  /-- Project explorer folder 标识(`OPEN` 表示;ADR-0021 透明组织节点,非权限资源)。 -/
  FolderId : Type
  /-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关,
-  ADR-0017;`@Claude` 仅为触发品牌,不承诺 provider)。 -/
+  ADR-0017;`@bot` 仅为触发品牌,不承诺 provider)。 -/
  RunId : Type
  /-- 长生命周期 agent 会话标识(`OPEN` 表示;**provider/model 绑定, ADR-0017**——一次
  session 不跨 provider/model;切 model 即新 session,跨 session 连续性由 ADR-0003 项目
  记忆/锚点重建,不由 session 自带。同 provider/model 内可跨多 run 复用, ADR-0002)。 -/
  SessionId : Type
  /-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/…
-      子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/
+      子类型学未定且非分歧点,故只留 opaque 键)。 -/
  Principal : Type
  /-- 飞书项目群 chat 标识(`OPEN` 表示;ADR-0001 协作空间、ADR-0003 锚点引用、
      ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子
-      类型——principal 子类型学 OPEN 见上,本层不预设"chat 是 principal 的哪种子型")。 -/
+      类型——principal 子类型学 OPEN,这里不预设"chat 是 principal 的哪种子型")。 -/
  ChatId : Type
  /-- 平台管理员身份标识(`OPEN` 表示;ADR-0023,不复用客户 `User` 标识)。 -/
  PlatformIdentityId : Type
@@ -1,41 +1,49 @@
+import Spec.System.Hierarchy
 import Spec.System.ProjectGroup
 import Spec.System.Organization
+import Spec.System.User
+import Spec.System.Connections
 import Spec.System.ProjectWorkspace
 import Spec.System.Capacity
 import Spec.System.PlatformAdministration
-import Spec.System.Run
+import Spec.System.Agent.Run
+import Spec.System.Agent.AgentRole
+import Spec.System.Agent.Memory
+import Spec.System.Agent.AgentSurface
 import Spec.System.Lock
-import Spec.System.Memory
-import Spec.System.AgentSurface
 import Spec.System.Permission
 import Spec.System.PermissionGrant
 import Spec.System.Audit
 /-!
 # System —— Hub 平台层契约

-协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。likec4
-(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的
-**语义分歧点**:
+协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。
+likec4 已画出结构;这里补语义:

+- `Hierarchy` —— 三层主体:平台 → 组织 → 用户。
+- `User` —— 用户创建路径(管理员直接创建;飞书注册 `OPEN`)。
+- `Connections` —— 外部连接:提供商枚举(当前仅飞书) + 绑定/信息类型。
 - `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
- `Organization` —— SaaS tenant root(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
-  connection secret 使用本地主密钥信封与 fail-closed resolver(ADR-0024)。
+- `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
+  connection secret 信封与 fail-closed resolver(ADR-0024);
+  owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。
 - `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
  (ADR-0021)。
 - `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
  平台紧急工作负载制动(ADR-0022)。
 - `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员
  保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。
+- `AgentRole` —— org-scoped agent 角色配置 + 技能(ADR-0017/0018)。
 - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
+- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权。
 - `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交——
  Lock 限定并发,Surface 限定波及面。机制 OPEN。
- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。
- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构
-  (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。
- `Audit` —— customer Project/Run 审计有意从简(内容多为 plumbing,OPEN);Platform
-  Audit 由 `PlatformAdministration` 独立钉死。
+- `Permission` —— read⊂edit⊂manage 角色体系、能力推导、单调性;force-release 在格外。
+- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)
+  (ADR-0004);组合规则 OPEN。
+- `Audit` —— customer Project/Run 审计从简(内容 OPEN);Platform Audit 由
+  `PlatformAdministration` 独立承载。

 标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0024。
 -/
@@ -0,0 +1,60 @@
+import Spec.Prelude
+
+/-!
+# AgentRole —— Agent 角色与技能配置 (ADR-0017, ADR-0018)
+
+AgentRole 是 org-scoped 运行时配置:system prompt、tool allowlist、default model
+和 skill 绑定。通过 CLI 管理,不需重启进程生效。
+
+Role 的执行面(model/prompt/tools/skill 内容)变更时,该 role 的 active sessions
+归档——下次 run 不能在旧指令下创建的 provider context 上恢复。
+仅 label/排序变更不影响会话连续性(ADR-0017)。
+
+Run 时只读加载 role 选中的 skill 不可变版本到 run-scoped 目录,
+run 结束后删除(ADR-0018)。Skill 管理是 org-scoped;存储机制 `OPEN`。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- Agent 角色(`PINNED`, org-scoped, ADR-0017)。 -/
+structure AgentRole where
+  /-- 所属组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 斜杠命令名(`OPEN` 表示;如 /draft)。 -/
+  roleId : String
+  /-- system prompt(`PINNED`)。 -/
+  systemPrompt : String
+  /-- tool allowlist(`PINNED`;tool 标识集合 `OPEN`)。 -/
+  tools : List String
+  /-- 默认 model(`PINNED`;model ID 表示 `OPEN`)。 -/
+  defaultModel : String
+
+/-- Agent 技能(`PINNED`, org-scoped, ADR-0017/0018)。 -/
+structure AgentSkill where
+  /-- 所属组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 名称(`PINNED`)。 -/
+  name : String
+  /-- 版本(`PINNED`)。 -/
+  version : String
+  /-- 内容摘要(`PINNED`;SHA-256 content-addressed)。 -/
+  contentDigest : String
+  /-- 描述(`OPEN`)。 -/
+  description : String
+
+/-- Role-Skill 绑定(`PINNED`, ADR-0017)。一个 role 可绑定零或多个 skill。 -/
+structure AgentRoleSkillBinding where
+  /-- 所属组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 绑定的 role(`PINNED`)。 -/
+  roleId : String
+  /-- skill 名称(`PINNED`)。 -/
+  skillName : String
+  /-- skill 版本(`PINNED`)。 -/
+  skillVersion : String
+  /-- 排序(`PINNED`)。 -/
+  sortOrder : Nat
+
+end Spec.System
@@ -0,0 +1,40 @@
+import Spec.Prelude
+import Spec.System.Agent.Run
+
+/-!
+# AgentSurface —— Agent 执行面边界(ADR-0018)
+
+Agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project 的工作区目录内
+(ADR-0007)。逃逸即越权,拒绝。
+
+与 `Lock`(ADR-0002)正交:Lock 限定并发(谁在改),Surface 限定波及面(能改到哪)。
+二者都按 run × project 作用域。
+
+shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论。机制
+——路径校验、OS 级沙箱、SDK 权限钩子,或其组合——`OPEN`(ADR-0018)。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers) (Path : Type)
+
+/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
+指向某路径;是否越权由下方 `Authorized` 约束。 -/
+structure AgentFileOp where
+  /-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
+  run : I.RunId
+  /-- 操作目标路径(`PINNED`, ADR-0018)。 -/
+  path : Path
+
+
+/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
+(`PINNED` 安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 由平台提供
+(表示 `OPEN`);本谓词约束"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写
+宿主任意文件。 -/
+def AgentFileOp.Authorized
+    (op : AgentFileOp I Path)
+    (runWorkspace : I.RunId → Option Path)
+    (pathWithin : Path → Path → Prop) : Prop :=
+  ∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
+
+end Spec.System
@@ -3,13 +3,13 @@ import Spec.Prelude
 /-!
 # Memory —— 按需上下文:锚点与项目记忆(ADR-0003)

-ADR-0003:Hub **只存锚点与项目记忆**,不存全量飞书消息历史;Claude 需要更多上下文时经
-飞书 API 按需读取。本模块刻画所存锚点的**类别**(ADR 列定,枚举完整性 OPEN——ADR 是
-"例如"式列举,新增类别不违反契约),并钉死一条 likec4 画不出的安全不变式:**MCP 工具
-按 run/project 上下文授权,Claude 不得传任意 chat id**(ADR-0003 Consequences 末条)。
+ADR-0003:Hub 只存锚点与项目记忆,不存全量飞书消息历史;Claude 需要更多上下文时经
+飞书 API 按需读取。这里刻画所存锚点的类别(ADR 列定,枚举完整性 OPEN),并约束
+一条安全不变式:MCP 工具按 run/project 上下文授权,Claude 不得传任意 chat id
+(ADR-0003 Consequences 末条)。

 "chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载,
-本模块不重复声明,只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
+这里只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
 -/

 namespace Spec.System
@@ -17,9 +17,8 @@ namespace Spec.System
 variable (I : Identifiers)
 variable (MessageId CardId : Type)

-/-- 上下文锚点(`PINNED` 类别, ADR-0003 列定;**枚举完整性 `OPEN`**——ADR 是"例如"式
-列举,实现若需新类别须 surface,不得默认本枚举已穷尽)。承载 Hub 保留的飞书侧最小指针,
-而非消息正文。 -/
+/-- 上下文锚点(`PINNED` 类别, ADR-0003;枚举完整性 `OPEN`——ADR 是"例如"式列举,
+实现若需新类别须 surface)。承载 Hub 保留的飞书侧最小指针,而非消息正文。 -/
 inductive Anchor where
  /-- 触发某次 run 的消息(`PINNED` 类别, ADR-0003 "trigger message id")。 -/
  | triggerMessage : MessageId → Anchor
@@ -35,13 +34,11 @@ MCP tools to read … through Feishu APIs")。 -/
 structure McpReadRequest where
  /-- 发起请求的 run(授权上下文主体, ADR-0003)。 -/
  run : I.RunId
-  /-- 请求读取的 chat(是否允许越界由下方 `Authorized` 钉死:不允许)。 -/
+  /-- 请求读取的 chat(授权由下方 `Authorized` 约束:不允许越界)。 -/
  chat : I.ChatId

 /-- 请求获授权:其 chat 必须等于该 run 所属 project 的绑定群(`PINNED` 安全不变式,
-ADR-0003 Consequences "MCP tools must authorize by run/project context; Claude cannot
-pass arbitrary chat ids")。`runProject`/`boundChat` 由平台提供(表示 `OPEN`);本谓词只
-钉死"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id 越权读取。 -/
+ADR-0003)。"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id。 -/
 def McpReadRequest.Authorized
    (req : McpReadRequest I)
    (runProject : I.RunId → Option I.ProjectId)
@@ -1,16 +1,16 @@
 /-!
 # Run —— AgentRun 状态机

-一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
-合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止
-判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。
+一次 `@bot` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
+转移关系在任何 ADR 里都未定,这里只刻画状态与终止判定(后者是 Lock 排他不变式的
+依赖),不定义转移边。
 -/

 namespace Spec.System

-/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022 + likec4;
-**完整性 `OPEN`**——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须
-surface,不得默认本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
+/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022;完整性 `OPEN`
+——ADR 从未声明"状态就是这些";实现若需新状态(如 pending)须 surface)。终止态
+见 `RunState.Terminal`。 -/
 inductive RunState where
  | active
  | waitingForUser
@@ -1,44 +0,0 @@
-import Spec.Prelude
-import Spec.System.Run
-
-/-!
-# AgentSurface —— Agent 执行面边界(ADR-0018)
-
-ADR-0001/0002/0004 覆盖"协作治理"直到 `triggerAgent`:谁能触发一次 run。但触发之后
-agent 在执行层面能干什么——读哪些文件、跑什么命令——任何 ADR / 散文都未定。ADR-0017
-落地时采用 Claude Code SDK 的 `bypassPermissions` + 全量 Read/Write/Bash/Glob/Grep,
-agent 的文件与 shell 面对宿主**无界**:spec 与 ADR 均未钉死边界。本模块补这一层。
-
-钉死的不变式:agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project
-的工作区目录内(ADR-0007:工程文件是目录树;此 ADR 固定"agent 操作落在该树内")。
-逃逸即越权,拒绝。与 `Lock`(ADR-0002)正交:Lock 限定**并发**(谁在改),Surface
-限定**波及面**(能改到哪)。二者都按 run × project 作用域。
-
-shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论,但**机制**
-——路径校验工具包装、OS 级沙箱(bubblewrap/容器)、SDK 权限钩子,或其组合——`OPEN`
-(ADR-0018)。契约钉死不变式,不钉死机制。
-/
-
-namespace Spec.System
-
-variable (I : Identifiers) (Path : Type)
-
-/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
-指向某路径;是否越权由下方 `Authorized` 钉死。 -/
-structure AgentFileOp where
-  /-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
-  run : I.RunId
-  /-- 操作目标路径(`PINNED` 字段, ADR-0018)。 -/
-  path : Path
-
-/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
-(`PINNED` 平台核心安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 均由平台提供
-(表示 `OPEN`——路径如何表示、"在内"如何判定是纯 plumbing,非本层分歧点);本谓词只
-钉死"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写宿主任意文件。 -/
-def AgentFileOp.Authorized
-    (op : AgentFileOp I Path)
-    (runWorkspace : I.RunId → Option Path)
-    (pathWithin : Path → Path → Prop) : Prop :=
-  ∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
-
-end Spec.System
@@ -1,21 +1,18 @@
 import Spec.Prelude

 /-!
-# Audit —— Project/Run 审计日志(有意从简)
+# Audit —— Project/Run 审计日志

-likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
-但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
-未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定
-"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是
-契约的一部分:承诺此处尚无答案、勿填)。
+审计记录里装什么(事件 schema、保留策略、可查询维度)在任何 ADR 里都未决策,
+且大多是实现细节。这里只固定"审计以 run 为主体记录其生命周期事件"这一条已决策
+关系,其余 `OPEN`。ADR-0023 的 Platform Audit 是另一个控制面,见
+`Spec.System.PlatformAdministration`,不复用本结构。
 -/

 namespace Spec.System

 /-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
-关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
-对应 ADR 落定。ADR-0023 的 Platform Audit 是另一个 fail-closed 控制面,见
-`Spec.System.PlatformAdministration`,不复用本结构。 -/
+关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`。 -/
 structure AuditEntry (I : Identifiers) where
  /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
  run : I.RunId
@@ -4,8 +4,8 @@ import Spec.Prelude
 # Capacity —— SaaS capacity admission and abuse controls (ADR-0022)

 初始生产服务共享有限的单机资源,但不能让一个 Organization 垄断容量或让无界输入拖垮
-其他租户。ADR-0022 钉死分层限制、持久 admission、显式背压和紧急制动的领域语义;
-具体数值必须由生产式容量测试校准,因此保持 `OPEN`,不得把未经验证的数字冒充契约。
+其他租户。ADR-0022 定义分层限制、持久 admission、显式背压和紧急制动;具体数值由
+生产式容量测试校准,保持 `OPEN`。
 -/

 namespace Spec.System
@@ -0,0 +1,24 @@
+import Spec.System.Connections.Prelude
+import Spec.System.Connections.Feishu
+
+/-!
+# Connections —— 连接绑定与用户信息
+
+组织/用户的外部连接。提供商枚举见 `Connections.Prelude`;
+飞书具体类型见 `Connections.Feishu`。
+-/
+
+namespace Spec.System
+
+
+/-- 组织连接绑定(`PINNED`)。 -/
+inductive ConnectionBinding (I : Identifiers) where
+  /-- 飞书(`PINNED`)。 -/
+  | feishu : FeishuAppBinding I → ConnectionBinding I
+
+/-- 用户连接信息(`PINNED`)。 -/
+inductive ConnectionProfile (I : Identifiers) where
+  /-- 飞书(`PINNED`)。 -/
+  | feishu : FeishuProfile I → ConnectionProfile I
+
+end Spec.System
@@ -0,0 +1,31 @@
+import Spec.Prelude
+
+/-!
+# Feishu —— 飞书连接
+
+组织绑定一个飞书企业应用(1:1)。用户经此应用登录、调飞书 API。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- 组织的飞书应用绑定(`PINNED`, 1:1)。 -/
+structure FeishuAppBinding where
+  /-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
+  appId : I.FeishuAppId
+  /-- app_secret 信封引用(`PINNED`, ADR-0024)。 -/
+  appSecretEnvelope : I.FeishuAppSecretRef
+
+/-- 用户的飞书信息(`PINNED`)。 -/
+structure FeishuProfile where
+  /-- 应用内身份(`OPEN`);调 API 的直接句柄,换应用即变。 -/
+  openId : I.FeishuOpenId
+  /-- 租户内身份(`OPEN`);换应用不变,比 open_id 稳定。 -/
+  userId : I.FeishuUserId
+  /-- 显示名(`OPEN`)。 -/
+  name : Option String
+  /-- 头像 URL(`OPEN`)。 -/
+  avatarUrl : Option String
+
+end Spec.System
@@ -0,0 +1,15 @@
+/-!
+# Connections.Prelude —— 连接提供商
+
+用户/组织的外部身份连接。当前仅 IdP 类别(飞书)。
+模型 provider connection 是独立概念,见 `Spec.System.Organization`。
+-/
+
+namespace Spec.System
+
+/-- 连接提供商(`PINNED`;当前仅飞书,未来可扩展钉钉/企微)。 -/
+inductive ConnectionProvider where
+  /-- 飞书(`PINNED`)。 -/
+  | feishu
+
+end Spec.System
@@ -0,0 +1,46 @@
+import Spec.Prelude
+import Spec.System.Connections
+
+/-!
+# Hierarchy —— 主体层级
+
+整个服务中的主体: 平台 → 组织(租户)→ 用户。
+
+- **平台**(Platform): SaaS 提供方实体
+
+- **组织**(Organization): SaaS 租户
+
+- **用户**(User): 租户内的独立实体
+
+**术语**: "管理员"一词在文档中不单独出现，避免跨层歧义。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+/-- 平台(`PINNED`, SaaS 提供方)。只有一个,独立于组织。管理面见 `PlatformAdministration`(ADR-0023)。 -/
+structure Platform where
+  /-- 平台自有飞书应用(`PINNED`, ADR-0023)。 -/
+  application : I.PlatformFeishuApplicationId
+/-- 组织(`PINNED`, ADR-0020)。project/team 必须归属且仅归属一个 org。
+外部连接见 `Connections`。角色/tenancy/凭据见 `Spec.System.Organization`。 -/
+structure Organization where
+  /-- 组织标识(`OPEN` 表示)。 -/
+  id : I.OrganizationId
+  /-- 外部连接(`PINNED`)。 -/
+  connections : List (ConnectionBinding I)
+
+/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。外部连接见 `Connections`。 -/
+structure User where
+  /-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/
+  id : I.UserId
+  /-- 所属组织(`PINNED`, ADR-0020)。 -/
+  organization : I.OrganizationId
+  /-- 显示名(`PINNED`, 可改)。 -/
+  displayName : String
+  /-- 密码哈希(`OPEN` 表示;id + 密码登录)。 -/
+  passwordHash : String
+  /-- 外部连接(`PINNED`)。 -/
+  connections : List (ConnectionProfile I)
+
+end Spec.System
@@ -1,35 +1,32 @@
 import Spec.Prelude
-import Spec.System.Run
+import Spec.System.Agent.Run

 /-!
 # Lock —— 项目锁与排他不变式

-ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`**
-(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条
-likec4 画不出的语义不变式——**持锁者必为非终止 run**。
+ADR-0002:防止并发 agent 同改一个项目,锁的 owner 是当前 `AgentRun`(不是
+teacher / chat / session)。持锁者必为非终止 run。
 -/

 namespace Spec.System

 variable (I : Identifiers)

-/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型
-上编码"lock owner = run_id":锁不可能被 session / teacher 持有。 -/
+/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`从类型上编码"lock owner = run_id":
+锁不可能被 session / teacher 持有。 -/
 structure ProjectAgentLock where
-  /-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/
+  /-- 作用域:项目级(`PINNED`, ADR-0002)。 -/
  scope : I.ProjectId
-  /-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/
+  /-- 持有者:一个 run(`PINNED`, ADR-0002)。 -/
  owner : I.RunId

 /-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
-的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/
+的结构本身即排他——不可能为同一项目登记两个并发 owner。 -/
 def LockTable := I.ProjectId → Option I.RunId

-/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。
+/-- 锁表良构:持锁者必为非终止 run(`PINNED`, ADR-0002)。

-"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条
-把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即
-必须释放"这个约束;它正是契约相对结构图的增量。 -/
+若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。锁在 run 终止时释放。 -/
 def LockTable.WellFormed
    (lt : LockTable I) (statusOf : I.RunId → RunState) : Prop :=
  ∀ p r, lt p = some r → ¬ (statusOf r).Terminal
@@ -1,18 +1,12 @@
 import Spec.Prelude

 /-!
-# Organization —— SaaS tenant root (ADR-0020, ADR-0024)
+# Organization —— SaaS 租户 (ADR-0020, ADR-0024)

-ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root。
-`Project` 与 `Team` 都必须归属且只归属一个 organization;team 对 project 的授权
-必须在同一 organization 内。平台运营控制面(platform staff / break-glass / 账单)
-不复用 project 的 `read/edit/manage` 角色格,而是另一个控制面。
-
-本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
-不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录
-provider 细节仍为 `OPEN`;平台控制面身份/角色/审计已由 ADR-0023 与
-`Spec.System.PlatformAdministration` 独立决定。连接凭据的本地主密钥信封、不可变版本、
-writer authority 与 fail-closed resolver 由 ADR-0024 固定。
+组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
+组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
+`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。Agent 角色配置见
+`Spec.System.Agent.AgentRole`。
 -/

 namespace Spec.System
@@ -41,19 +35,17 @@ structure TeamProjectGrantScope where
  project : I.ProjectId
  /-- 获得授权的 team principal(`PINNED`, ADR-0020)。 -/
  team : I.TeamId
-
 /-- Team-project grant 是良构的 iff project 与 team 解析到同一 organization
-(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);本谓词钉死
-跨 org team grant 必须被拒绝。 -/
+(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);跨 org
+team grant 必须被拒绝。 -/
 def TeamProjectGrantScope.WellScoped
    (grant : TeamProjectGrantScope I)
    (projectOrg : I.ProjectId → Option I.OrganizationId)
    (teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
  ∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o

-/-- Organization 的 model provider 凭据归属模式(`PINNED`, ADR-0021):BYOK 由 org
-管理员提供和管理;platform-managed 由平台管理员为该 org 单独提供和管理。两种模式
-都不允许无关 org 共用 process-global provider key。模式切换过程仍为 `OPEN`。 -/
+/- BYOK 由组织所有者/管理员管理;platform-managed 由平台管理员管理。两种模式都不允许
+跨 org 共用 process-global key。模式切换 `OPEN`。 -/
 inductive ProviderCredentialMode where
  | byok
  | platformManaged
@@ -78,7 +70,7 @@ inductive OrganizationConnectionStatus where

 /-- Organization secret version 的信封绑定上下文(`PINNED`, ADR-0024):认证附加数据必须
 同时绑定 organization、connection、secret version 与 purpose,因此密文不能跨行、跨 org、
-跨 connection 或跨用途替换。各标识符的数据库表示属于 plumbing,这里保持 opaque。 -/
+跨 connection 或跨用途替换。各标识符的数据库表示为实现细节,这里保持 opaque。 -/
 structure OrganizationSecretBinding
    (OrganizationId ConnectionId SecretVersionId Purpose : Type) where
  /-- secret 所属 organization(`PINNED`, ADR-0024)。 -/
@@ -104,4 +96,34 @@ def OrganizationSecretResolvable
  organizationActive && connectionActive &&
    (binding.organization == requestedOrganization) && authenticatedEnvelope

+
+/-- 组织成员角色(`PINNED` 封闭三档)。与项目层 `Role`、平台层 `PlatformRole` 互不相交。 -/
+inductive OrganizationRole where
+  /-- 组织所有者(`PINNED`):bootstrap,独家管 owner 群体,受最后所有者保护。 -/
+  | owner
+  /-- 组织管理员(`PINNED`):管成员/policy/BYOK,不能管 owner 群体。 -/
+  | admin
+  /-- 组织成员(`PINNED`):普通成员。 -/
+  | member
+
+/-- 组织成员关系(`PINNED`)。 -/
+structure OrganizationMembership where
+  /-- 成员(`PINNED`;独立实体,见 `Hierarchy.User`)。 -/
+  user : I.UserId
+  /-- 组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 角色(`PINNED`)。 -/
+  role : OrganizationRole
+
+/-- 只有组织所有者能管 owner 群体(`PINNED`)。 -/
+def CanManageOwnerGroup (actorRole : OrganizationRole) : Prop :=
+  actorRole = .owner
+
+/-- 最后所有者保护(`PINNED`):撤销 owner 时同 org 必须还有一个不同的 owner。 -/
+def LastOwnerProtected
+    (target : OrganizationMembership I)
+    (otherOwnersInOrg : List I.UserId) : Prop :=
+  target.role ≠ .owner ∨
+    ∃ other, other ∈ otherOwnersInOrg ∧ other ≠ target.user
+
 end Spec.System
@@ -5,8 +5,7 @@ import Spec.Prelude

 ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
 分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
-强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低
-role 全部能力"的单调性钉死。
+强制释放锁是 **admin-only**,在 role 体系之外。
 -/

 namespace Spec.System
@@ -4,16 +4,14 @@ import Spec.System.Permission
 /-!
 # PermissionGrant —— 授权与设置(ADR-0004)

-ADR-0004 的"飞书云文档式"权限:**grant**(`resource × principal × role`)与 **settings**
-(各 policy 旋钮)分离;role 决定"谁能"(能力,见 `Permission`),settings 决定"此资源
-是否开某类操作"(策略)。本模块把 grant/settings 的结构钉死——`Permission` 已落 role 能
-力格,本模块补"授权如何挂到资源/主体上"。
+ADR-0004 的"飞书云文档式"权限:grant(`resource × principal × role`)与 settings
+(各 policy 旋钮)分离;role 决定能力(见 `Permission`),settings 决定"此资源是否
+开某类操作"。

-principal 子类型学(user/chat/department/…)与各 policy 值域均为 `OPEN`(ADR 未定,非本
-层分歧点)。**role-capability 与 settings-policy 如何组合成最终授权决策**亦 `OPEN`——
-ADR-0004 把二者列为分离的闸,但未明文规定组合规则(AND?settings 能否超出 role?),实现
-须 surface,不得默认。ADR-0020 另行钉死 TEAM principal 授权 PROJECT resource 时必须
-同 organization;该 tenant well-scopedness 见 `Spec.System.Organization`。
+principal 子类型学(user/chat/department/…)与各 policy 值域 `OPEN`。role-capability
+与 settings-policy 如何组合成最终授权决策亦 `OPEN`——ADR-0004 把二者列为分离的闸,
+但未明文规定组合规则。ADR-0020 约束 TEAM principal 授权 PROJECT resource 时必须同
+organization,见 `Spec.System.Organization`。
 -/

 namespace Spec.System
@@ -45,9 +43,8 @@ structure PermissionGrant where
  role : Role

 /-- 资源策略设置(`PINNED` 结构 + 六旋钮, ADR-0004 `PermissionSettings`):与 grant 分离,
-控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定,非本层
-分歧点)。共享同一 opaque `Policy` 类型:契约只钉死"旋钮存在且相互独立",不钉死"各旋钮
-值域互异"——值域是实现/后续 ADR 的事。 -/
+控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定)。
+共享同一 opaque `Policy` 类型:契约只约束"旋钮存在且相互独立";值域是实现/后续 ADR 的事。 -/
 structure PermissionSettings where
  /-- 设置所属资源(`PINNED`, ADR-0004)。 -/
  resource : Resource I ArtifactId
@@ -8,8 +8,8 @@ import Spec.Prelude
 单一平级管理员角色、绑定身份的 invitation、可撤销服务端 session、mutation 与平台审计
 同成同败、最后管理员保护,以及无常驻账号的双因子离线恢复。

-本模块只钉死这些会导致安全边界分歧的语义。cookie 属性、token hash、具体 TTL、审计
-字段表示/保留期、recovery key 介质和 CLI/SQL 机制仍为 `OPEN`,由对应实现决策承载。
+这些安全边界语义见下。cookie 属性、token hash、具体 TTL、审计
+字段表示/保留期、recovery key 介质和 CLI/SQL 机制 `OPEN`。
 -/

 namespace Spec.System
@@ -3,26 +3,23 @@ import Spec.Prelude
 /-!
 # ProjectGroup —— 飞书项目群作为协作空间(ADR-0001)

-ADR-0001 的核心:一个 project 对应一个**长生命周期**飞书项目群;群是协作空间,**不是锁
-owner**(锁归 `AgentRun`,见 `Lock` / ADR-0002),不是临时处理 session。群可在无 Claude
-处理时保持开启;教师离群/静音与项目权限、与 Claude 生命周期相互独立。本模块钉死
-project↔group 的**active**一对一绑定——likec4 画得出"project has group",画不出"恰好一个、
-且群不持锁"。
+一个 project 对应一个长生命周期飞书项目群;群是协作空间,不持锁(锁归 `AgentRun`,
+见 `Lock` / ADR-0002)。群可在无 agent 处理时保持开启;教师离群/静音与项目权限、
+与 agent 生命周期相互独立。

-**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可以保留 archived
-historical binding rows 供审计/纠错,但 `GroupBinding` 谓词只刻画当前 active 快照。
-群解散/不可达的自动化处理仍为 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
+**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可保留 archived
+historical binding rows 供审计,但 `GroupBinding` 谓词只刻画当前 active 快照。
+群解散/不可达的自动化处理 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
 -/

 namespace Spec.System

 variable (I : Identifiers)

-/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的绑定;
-**不是锁 owner**(锁归 `AgentRun`,见 `Lock`);不是临时 session。 -/
+/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的
+绑定;不持锁(锁归 `AgentRun`,见 `Lock`)。 -/
 structure ProjectGroup where
-  /-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001 "one project has one Feishu project
-  group";chat 标识见 `Identifiers.ChatId`)。 -/
+  /-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001;chat 标识见 `Identifiers.ChatId`)。 -/
  chat : I.ChatId

 /-- 项目↔active 群绑定表(`PINNED` 每项目至多一个 active 群, ADR-0001/0021)。
@@ -30,9 +27,9 @@ structure ProjectGroup where
 自带);良构补另一半——单射。 -/
 def GroupBinding := I.ProjectId → Option I.ChatId

-/-- Active 绑定良构:**单射**——不同 project 不绑同一 active chat(`PINNED` 1:1 的另一半,
-ADR-0001/0021)。"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个
-project"。archived historical bindings 不在本快照不变式内。 -/
+/-- Active 绑定良构:单射——不同 project 不绑同一 active chat(`PINNED`, ADR-0001/0021)。
+"每 project 至多一个群"由 `Option` 结构自带;这条约束"每群至多属于一个 project"。
+archived historical bindings 不在本快照不变式内。 -/
 def GroupBinding.WellFormed (b : GroupBinding I) : Prop :=
  ∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂

@@ -3,12 +3,11 @@ import Spec.Prelude
 /-!
 # ProjectWorkspace —— project explorer 与飞书建项入口(ADR-0021)

-ADR-0021 把 org 后台里的"文件管理器式"项目管理收口为透明 folder + project:
-folder 只负责导航、排序、层级与用量聚合,当前不是权限资源。project 仍是授权边界。
+org 后台里的"文件管理器式"项目管理:folder 只负责导航、排序、层级与用量聚合,当前
+不是权限资源。project 仍是授权边界。

-本模块只钉死会影响实现分歧的不变量:folder/project 同 org、folder 不参与权限、普通成员
-从飞书群创建 project 必须受 org policy 控制。folder visibility/team policy/继承授权仍为
-未来扩展,不得在当前实现中半隐式加入。
+不变量:folder/project 同 org、folder 不参与权限、普通成员从飞书群创建 project 受
+org policy 控制。folder visibility/team policy/继承授权 `OPEN`。
 -/

 namespace Spec.System
@@ -39,7 +38,7 @@ def ProjectFolderPlacement.WellScoped
  ∃ o, projectOrg placement.project = some o ∧ folderOrg placement.folder = some o

 /-- Folder 当前透明(`PINNED`, ADR-0021):folder 不是权限资源,不持有 grants,移动 project
-不改变 project 自身授权。未来 folder policy 若出现,必须新增显式语义而不是复用本谓词。 -/
+不改变 project 自身授权。未来 folder policy 若出现,须新增显式语义。 -/
 structure FolderTransparent where
  /-- 透明性命题本身;字段存在是为了让 contract 明确可引用(`PINNED`, ADR-0021)。 -/
  current : True
@@ -0,0 +1,12 @@
+import Spec.Prelude
+
+/-!
+# User —— 用户创建路径
+
+用户实体见 `Hierarchy.User`;外部连接见 `Spec.System.Connections`。
+
+用户创建当前只定义管理员直接创建;飞书自助注册→管理员审批 `OPEN`。
+-/
+
+namespace Spec.System
+end Spec.System
Author	SHA1	Message	Date
sjfhsjfh	3ebe4b754d	refactor(spec): clean prose patterns across all modules Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出, 臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意. No code definitions changed, only doc comments.	2026-07-13 11:26:23 +08:00
sjfhsjfh	3fa6a5a5a5	fix(spec): replace @Claude with @bot in Prelude and Run	2026-07-12 18:55:52 +08:00
sjfhsjfh	be4260bcd0	refactor(spec): move AgentRole/Run/Memory/AgentSurface into System/Agent/ subdir	2026-07-12 18:43:11 +08:00
sjfhsjfh	a4449f03c4	chore: ignore .env	2026-07-12 18:38:45 +08:00
sjfhsjfh	01bc20d25f	feat(spec): add AgentRole, AgentSkill, RoleSkillBinding (ADR-0017/0018)	2026-07-12 18:38:17 +08:00
sjfhsjfh	38c3231190	refactor(spec): generalize Feishu to Connections - Connections/Prelude.lean: ConnectionProvider 枚举 (当前仅飞书) - Connections/Feishu.lean: FeishuAppBinding + FeishuProfile - Connections.lean: ConnectionBinding/ConnectionProfile inductive - Organization.feishu → connections: List ConnectionBinding - User.feishu → connections: List ConnectionProfile - 删除 FeishuConnection.lean	2026-07-12 15:54:16 +08:00
sjfhsjfh	63416e06ea	refactor(spec): move FeishuProfile to FeishuConnection, clean docs - FeishuProfile 从 User.lean 移到 FeishuConnection.lean - User.lean 只留用户创建路径声明 - 清理所有 doc comment	2026-07-12 09:33:33 +08:00
sjfhsjfh	39bd2c9ff7	feat(spec): pin org-feishu app binding to 1:1 - FeishuConnection.lean: FeishuAppBinding (appId + appSecretEnvelope) - Organization.feishu: Option FeishuAppBinding (Option 自带 1:1) - 删除 FeishuConnectionId (不再需要游离类型) - FeishuProfile 删除 connection 字段 (由 org 隐含)	2026-07-12 09:29:41 +08:00
sjfhsjfh	e17e038232	feat(spec): add FeishuUserId to FeishuProfile 飞书 user_id 是租户内身份,换应用不变;open_id 是应用内身份,换应用即变。两者都存:user_id 更稳定,open_id 是 API 调用句柄。	2026-07-12 09:26:13 +08:00
sjfhsjfh	678bc9f56c	refactor(spec): tighten prose, replace jargon - 角色格→角色体系 (3处) - 租户根/tenant root→租户 (3处) - 清理 Hierarchy/Organization/System 的 doc 注释	2026-07-12 09:23:39 +08:00
sjfhsjfh	3a50ed0ce2	feat(spec): add three-tier subject hierarchy and org role lattice - Hierarchy.lean: Platform/Organization/User struct, 三层主体层级 - User.lean: FeishuProfile, 飞书身份是绑定不是本体 - User struct: id/displayName/passwordHash/feishu - Organization.lean: OrganizationRole(owner/admin/member) + 成员管理规则 - Prelude.lean: UserId/FeishuOpenId/FeishuConnectionId 实现偏离: spec 钉 User 为独立实体, 实现 User.id 由飞书身份派生 lake build 35/35 全绿	2026-07-12 00:21:13 +08:00