@ fairfox/ polly (英语)

多文本应用的活性状态——从单进程信号到对等加密网格——有正式的验证.

投篮

定义状态一次。 随处读取. 波利让他们同步.

// src/shared/state.ts
import { $sharedState } from "@fairfox/polly/state";

export const counter = $sharedState("counter", 0);

// src/background/index.ts — service worker, extension background, Node process
import { createBackground } from "@fairfox/polly/background";
import { counter } from "../shared/state";

const bus = createBackground();

bus.on("INCREMENT", () => {
  counter.value++;
  return { count: counter.value };
});

// src/popup/index.tsx — browser popup, any Preact/React UI
import { render } from "preact";
import { counter } from "../shared/state";

function App() {
  return (
    <div>
      <p>Count: {counter.value}</p>
      <button onClick={() => counter.value++}>+</button>
    </div>
  );
}

render(<App />, document.getElementById("root")!);

背景写道: counter弹出会读出 两者保持同步——没有消息传递,没有订阅管理. 国家是 预告信号,因此当值变化时,UI会自动重报.

各地同步状态

现代应用在多个孤立的情况下运行代码:服务工作者,内容脚本,服务器进程. 保持它们之间的状态一致意味着为每一个数据写同步逻辑. 波利用四个原始人来代替它:

所有四个回回预告信号. 读取 .value,用 .value =。 。 。 .

import { $sharedState, $syncedState, $persistedState, $state } from "@fairfox/polly/state";

const user = $sharedState("user", { name: "Guest", loggedIn: false });
const wsConnected = $syncedState("ws", false);
const draft = $persistedState("draft", "");
const loading = $state(false);

对于同步数据, $resource 当依赖关系发生变化时自动获取并重排:

import { $resource } from "@fairfox/polly/resource";

const todos = $resource("todos", {
  source: () => ({ userId: user.value.id }),
  fetcher: async ({ userId }) => {
    const res = await fetch(`/api/todos?userId=${userId}`);
    return res.json();
  },
  initialValue: [],
});

todos.data;   // Signal<Todo[]>
todos.status; // Signal<"idle" | "loading" | "success" | "error">
todos.refetch();

同级第一状态(v0.210

上面的4个原始人保持状态一致 在单一的部署。 但有些应用程序需要能够活过服务器离开的状态,或者说服务器根本没有看到. Polly现在提供三层抗御能力, 每一个不同的原始家庭:

$peerState 每个设备都装满了 自动合并 CRDT复制版. 服务器也持有一个,因此cron和HTTP处理器可以读取并变换文档. 如果服务器丢失了存储,任何重新连接的客户端都会通过正常的同步协议重新聚集.

import { createPeerStateClient, configurePeerState, $peerState } from "@fairfox/polly/peer";

const client = createPeerStateClient({ url: "wss://yourapp.com/polly/peer" });
configurePeerState(client.repo);

const settings = $peerState("settings", { theme: "dark" });
await settings.loaded;
settings.value = { theme: "light" }; // syncs to every peer

$meshState ——同行直接通过WebRTC数据通道进行交换操作,与Ed25519签约,并用XSalsa20-Poly1305加密. 没有服务器看到数据 。 一个小型的无国籍信号服务器可以帮助同伴找到对方;去除它不会影响运行中的连接.

import { configureMeshState, $meshState, MeshNetworkAdapter, MeshWebRTCAdapter } from "@fairfox/polly/mesh";

const repo = new Repo({ network: [new MeshNetworkAdapter({ base: webrtcAdapter, keyring })] });
configureMeshState(repo);

const notes = $meshState("notes", { entries: [] });
// Operations flow peer-to-peer, signed and encrypted

设备之间的第一次密钥交换使用以QR代码显示的对接符. 通过向每个同行传播的签名吊销记录,撤销妥协装置.

三层并存在一个应用程序中——公共环境 $sharedState中协作文档 $peerState,私人笔记 $meshState。见 文件/统计数据库 整个决策树和 文件/RFC-041-Choosing.md 设计原理.

节点和邦是一等的网状同龄人

Archive cron, LLM 代理, admin CLIs, 无头桥——每名总参与者都会得到与浏览器相同的状态原始, 而不使用猴子- patching globals 或写作活塞运输接线. Polly 将一个接受注射式运输和储存的工厂:

import { createMeshClient, $meshState } from "@fairfox/polly/mesh";
import { bootstrapCliKeyring, fileKeyringStorage } from "@fairfox/polly/mesh/node";
import { RTCPeerConnection } from "werift";              // or '@roamhq/wrtc'

const storage = fileKeyringStorage("~/.fairfox/keyring.json");
const keyring = await bootstrapCliKeyring({ storage });   // first run prompts for a pairing token

const client = await createMeshClient({
  signaling: { url: "wss://example.com/polly/signaling", peerId: "cli-a1b2" },
  rtc:       { RTCPeerConnection },
  keyring,
});

const doc = $meshState("agenda", { items: [] });
await doc.loaded;
await client.close();

createMeshClient 是运行时间不可知的——在浏览器中 rtc 选项是可选的,因为 globalThis.RTCPeerConnection 已存在。 这个 @fairfox/polly/mesh/node 子路径添加文件系统支持的密钥环存储, 原子写到 0600 权限, 并有固定的靴子。 也没有 werift 也没有 @roamhq/wrtc 捆绑; 两者被宣布为可选的对等依赖。 选一个适合你部署的 werift 安装干净的任何地方(纯类型脚本,没有本地的脚本), @roamhq/wrtc 更快, 但需要为您的平台预建二进制 .

大文件的 Blob 存储

CRDT文件不应携带二进制有效载荷——操作历史随着每次同步而增长. Poly 运送一个内容地址为blob的商店,通过与WebRTC相同的WebRTC频道传输文件对等 $meshState,没有服务器存储。 文档具有轻量级 BlobRef 值; 字节活在本地索引 DB 缓存中, 在64 Kib 块的同位素之间移动.

import { createBlobStore, createBlobRef } from "@fairfox/polly/mesh";

const blobs = createBlobStore(webrtcAdapter, { encrypt: { key: docKey } });

// Sender
const bytes = new Uint8Array(await file.arrayBuffer());
const ref = await createBlobRef({ bytes, filename: file.name, mimeType: file.type });
await blobs.put(ref, bytes);       // caches locally, announces to peers
doc.value = { ...doc.value, attachment: ref };

// Receiver (on any connected peer)
const received = await blobs.get(ref.hash);  // fetches from peers, verifies hash
const url = await blobs.url(ref.hash);        // object URL for <img src>

SHA-256内容涉及同行和文件之间的重复。 加密是可选的——当配置时,发送者会加密一次(XSalsa20-Poly1305),并将密码文本块块;接收者会重新组装,解密,并验证平正文字散列相对于 BlobRef。见 文件/RFC-042-blob-sync.md 为设计.

插入的验证

一个弹出和一个背景脚本都写给同一个州. 内容剧本读取中后期. 测试错过这些bug,因为它们取决于时机.

Polly 生成 TLA+ 东加 ,然后用 TLC 检查。 不学一新语. 你记下你已经写的.

第1步:向管理人员增加合同

requires() 财务报告和审定财务报表 ensures() 是运行时间 无操作. polly verify 静地读取.

import { createBackground } from "@fairfox/polly/background";
import { requires, ensures } from "@fairfox/polly/verify";
import { user, todos } from "./state";

const bus = createBackground();

bus.on("TODO_ADD", (payload: { text: string }) => {
  requires(user.value.loggedIn === true, "Must be logged in");
  requires(payload.text !== "", "Text must not be empty");

  todos.value = [...todos.value, {
    id: Date.now().toString(),
    text: payload.text,
    completed: false,
  }];

  ensures(todos.value.length > 0, "Todos must not be empty after add");

  return { success: true };
});

步骤2: 定义状态界限

一个验证配置告诉 TLC 需要探索的值 :

// specs/verification.config.ts
import { defineVerification } from "@fairfox/polly/verify";

export const verificationConfig = defineVerification({
  state: {
    "user.loggedIn": { type: "boolean" },
    "user.role": { type: "enum", values: ["guest", "user", "admin"] },
    todos: { maxLength: 1 },
  },
  messages: {
    maxInFlight: 2,
    maxTabs: 1,
  },
});

第三步:运行它

$ polly verify

Generating TLA+ specification...
Running TLC model checker...

  Model checking complete.
  States explored: 1,247
  Distinct states: 312
  No errors found.

All properties verified.

A 类 requires() 不坚持勘探: 处理者不是 被带走了,所以模特儿永远无法到达守卫后面的状态. 这就是为什么 requires() 便宜,这也是为什么一个绿色跑步 不说是否 警卫可能被侵犯——安全财产是已经停止的系统.

添加 liveness: true (每个配置,或每个子系统)检查另一半: 任何寄出的东西都会永远等待 TLC 然后报告准确的顺序 信息永远无法解决。 因为它是默认关闭的 价格昂贵——在11个子系统模型上测出,一个验证门从~110到 ~512 (英语).

对于更大的应用程序, 子系统范围核查 将状态空间拆分, 以快速检查 .

第4步: 抓住模特儿从未见过的道路

每次跑步都报告 模式覆盖 ——宣布每个处理者写字的字段,而模型上的任何字段都不触及. 它捕捉到的bug是信息总线上赋予的能力: a register() 设定方法 canSend 而不是直接通过一个派出的 守卫的操作员。 TLC对此没有过渡性,突变测试没有模拟线来进行突变,而绿色跑道则一言不发.

没有处理器写入的字段被标记为无法到达状态 。 未分配的函数或方法写作的字段——即使是真正的处理者也写作的字段——被标记为在任何模式过渡外被变异. 添加 --strict 无法关闭,所以没有模型的写作不能滑出绿色.

$ polly verify --strict

⚠️  1 declared state field write(s) outside any modelled transition:
   • session.canSend mutated in RecoveryFlow.register() — src/background/index.ts:42

❌ Strict mode: model coverage incomplete

没有Docker的安全通道更快

polly verify --engine bun 使用花粉公司自己的模型检查器检查同一生成的光谱,正在进行中:变化和僵局,没有多克克,没有JVM. 举例来说,它报告TLC精确的状态计数为2.5–9×所有核心的TLC速度,为记忆的五分之一到一半. 它不检查时间属性( ensures 附加条件:它列出这些条件没有检查 --strict 失败了 用于您发车前的编辑和检查回路和 TLC(默认) 。 Bun 检查器无法读取的光谱返回到 TLC 。 设定 verification: { engine: "bun" } 让它成为工程默认.

链接到模型的可执行规格

polly bdd 加上第三个核查层 verify (TLA+)和 (中文(简体) ) mutate (模拟测试):从用户角度撰写的接受实例,如Gherkin,横穿 真实工厂边界 一样 createBackground 你的扩展靴子,从来没有一个手电线公交车 静悄悄地记录了真正的路径的缺口.

# features/auth.feature
Feature: Signing in
  Scenario: A signed-out user can sign in
    Given the user is signed out
    When the user signs in as "admin"
    Then the user is signed in
    And their role is "admin"

一个 defineStep 约束是双重用途, 同样的把戏使 requires()编号 :ensures() (单位:千美元) given编号 :when编号 :then 驱动运行时间, 而其运行时间 message编号 :stateExpr 静态读取。 因此,示例层,形式层和突变层都描述了相同的处理器和状态.

polly bdd          Run the scenarios across the real boundary (red before green)
polly bdd check    Cross-check every scenario against the verification config (Docker-free)
polly bdd new      Scaffold a feature stub seeded from the verify vocabulary

丢弃 .feature 文件输入您的工程和 polly test 发现一个 bdd 自动分级.

可接触性证人

polly verify --witness 关闭示例层和模型之间的循环。 它将每个场景的结果变成每场场景的TLC可达性检查:一个场景,详尽的模型证明 无法到达 是一个在跑道上是绿色的,在模型上是不可能的,它失败了跑道。 诚实的人可以回来,反例追踪是用户为了到达那里而会走的道路. 无法观察的结果(只检查反应)被报告为跳过.

标记一个情景 @forbidden 维护 相对:一个绝不能发生的州. 然后,当模型证明这种状态无法达到时,证人才会通过,如果能够达到这种状态,就会失败——有缺陷的痕迹。 从同名Gherkin那里看,可以证明是可能的、不可取的结果是不可能的.

$ polly verify --witness

Reachability witnesses (--witness)
  ✓ reachable   Signing in › A signed-out user can sign in
  ✓ reachable   Signing in › Signing out returns the user to a guest session
  · skipped     Todos › Completing a todo that does not exist is refused

Witness result: ✓ PASS

快开始

bun add @fairfox/polly preact @preact/signals

作者工具加载一个生产安装的包并不需要,所以它们是可选的对等依赖. 添加您作为 dev 依赖运行的命令 :

# all of them
bun add -d typescript-7@npm:[email protected] [email protected] [email protected] \
  @cucumber/[email protected] @cucumber/[email protected]

typescript-7 必须保留该别名:花粉进口 typescript-7/async。其软件包缺失并打印安装命令.

脚手架项目:

polly init my-app --type=extension  # or: pwa, websocket, generic

或者从其中一个例子开始:

git clone https://github.com/AlexJeffcott/polly.git
cd polly/examples/minimal
bun install && bun run dev

实例

国 际

polly init [name] [--type=TYPE]   Scaffold a new project (extension | pwa | websocket | generic)
polly build [--prod]              Build for development or production
polly dev                         Build with watch mode
polly check                       Run all checks (typecheck, lint, test, build)
polly typecheck                   Type-check your code
polly lint [--fix]                Lint (and optionally auto-fix)
polly format                      Format your code
polly test [args]                 Run unit tests (bun test)
polly test --tier=T | --all | --list
                                  Run the multi-tier suite (unit → integration → browser
                                  → e2e → verify) with timed reports
polly test:browser [dir]          Run *.browser.{ts,tsx} in Puppeteer
polly coverage                    Per-file coverage policy and orphaned-test detection
polly verify                      Run formal verification (TLA+/TLC)
  --setup | --validate | --estimate   Generate, check, or size the verification config
  --strict                        Fail on model-coverage gaps
  --engine bun                    Safety pass on polly's own checker, no Docker
  --witness                       Per-scenario reachability checks for your BDD outcomes
polly bdd [run|check|new]         Executable Gherkin across the real boundary, linked to the model
polly mutate [init|run|report|verify|decisions|migrate]
                                  Mutation testing and useless/redundant-test detection
polly visualize                   Generate architecture diagrams (Structurizr DSL)
  --snapshot <path>               Overlay a captured mesh peer-state snapshot
  --model <file.ts>               Write a declared C4 model instead of analysing source
  --export | --serve              Static diagram site (export needs Docker) and a local server
polly gallery [--build|--open]    Serve or export the polly-ui component gallery
polly quality [args]              Run conformance checks (no-as-casting, boundaries, secrets,
                                  server-imports, forbidden-deps, banners, marketing, ...)

每个命令都要 --help。 。 。 . polly mutate 记录在 工具/元件/README.md。 。 。 .

质量工具

Poly ship 兼容性检查和浏览器测试工具,消耗应用程序可以直接采用.

无所现相. 禁止类型脚本 as 类型断言全码基(仅限 as const 和明确的逃生舱门 as unknown as (允许)。 违规行为包括特定模式的固定建议。 运行为 CLI :

polly quality [--root <dir>] [--exclude-packages <names>] [--exclude-files <names>]

或按程序导入, 以便融入自定义检查脚本 :

import { checkNoAsCasting } from "@fairfox/polly/quality";

const result = await checkNoAsCasting({ rootDir: process.cwd() });
if (result.violations.length > 0) {
  result.print();
  process.exit(1);
}

浏览器测试用具. 一个基于 Puppeteer 的用于测试仅浏览器代码的套接字(WebRTC适配器,Preact组件,任何需要真实的 DOM ). 用 Bun.build 装入每个测试文件,在麻黄口上服务,并收集结果:

import { describe, test, expect, done, flush, cleanup } from "@fairfox/polly/test/browser";

describe("my component", () => {
  test("renders", async () => {
    render(<MyComponent />, app);
    await flush();
    expect(app.querySelector("h1")).toHaveTextContent("Hello");
    cleanup(app);
  });
});

done();

运行 polly test:browser tests/browser。 。 。 .

用克劳德代码

这艘反转船有一个 Claude 代码技能 覆盖了完整的 Polly API —— 状态原始,同位素第一和网状状态,验证,质量工具,以及浏览器测试用具. 安装在您的工程中, 这样克劳德可以帮助您将 Polly 与 完整 上下文 整合 :

# From your project directory
claude install-skill /path/to/polly/.claude/skills

那就问问克洛德吧

• "Polly会怎样融入这个项目?"
• "给我的处理者增加核查"
• "用爱丽西亚服务器设置美国"
• 拨打CI的不挂号检查

如果你保持你自己的克洛德代码技能,考虑在您的项目特有技能中加入波利的状态级决策树和验证模式,这样克洛德就可以为每一个状态推荐合适的原始.

许可证

麻省理工学院

GitHub 图像 • 妇女 问题 • 妇女 实例