Hakkadaikon

wired のパフォーマンス改善の記録

wired は、libc に依存しない C で書かれた自前実装の QUIC サーバー SDK である。 QUIC は TLS による暗号化を組み込んだ、UDP 上のトランスポートプロトコルで、HTTP/3 の土台になっている。 wired は暗号（TLS ハンドシェイク、楕円曲線署名、パケット暗号化）も標準ライブラリなしで自前実装し、システムコールを直接呼ぶ。

この文書は、これまでに行われたパフォーマンス改善を、症状、原因、対策、効果の順で追えるようにまとめたものである。 数値はすべて当時の作業台帳と教訓集に記録された実測値で、それぞれの作業日のベースラインに対する比較として読む（日をまたいだ絶対値には、同時に入った他の改善や測定ノイズ分の揺れがある）。

測定に使う指標は次の 4 つである。

Hakkadaikon

wired tree

Level: 1

src  
├── app  
├── common  
├── crypto  
├── tls  

Hakkadaikon

Lessons — 性能改善(QUIC ハンドシェイク 4.6s → 17ms)

curl の HTTP/3 ハンドシェイクが appconnect ≈ 4.6 秒かかっていたのを 17ms まで 落とした一連の流れ。再現したい「診断の順序」と「やってしまった遠回り」を残す。

結果サマリ

段階	appconnect	何を直したか	倍率
初期	4.6 s	—	—

Hakkadaikon

 $ tree src                                                                                                                                                                       Tue 30 Jun 2026 08:29:16 PM JST
src
├── app
│   ├── datagram
│   │   ├── datagram
│   │   │   ├── datagram.c
│   │   │   ├── datagram.h
│   │   │   ├── dgcc.c
│   │   │   ├── dgcc.h
│   │   │   ├── dgcheck.c

Hakkadaikon

QUIC RFC 実装カバレッジ

各 RFC の機能要素ごとに実装状況をチェックボックスで示す。判定は実コードと テストを照合した結果(2026-06 時点)。

凡例:

• [x] 実装済み(コードあり + テストで検証)
• [~] 部分実装(コードはあるが簡略 / 一部のみ / 未検証)
• [ ] 未実装

Hakkadaikon

形式検証の効果レポート — 優先度付き信頼性メッセージキュー

対象: src/ の Rust 実装(reliable_queue) 検証層: TLA+(設計のモデル検査)+ Lean 4(実装の数学的証明) このレポート自体と tasks/ 配下は git 管理外の裏方成果物。

---

要約

Hakkadaikon

形式検証ふりかえり — WebSocket プロトコルスタック SDK

libc 非依存(freestanding C23)の RFC 6455 WebSocket SDK を作る過程で、TLA+ による設計検証と Lean 4 による数学的証明を実際に使った。 その体験を、効いた点・摩擦・改善に分けて記録する。

数字で見ると、最終的に次の検証資産が残った。

• TLA+: WsLifecycle(接続ライフサイクル、INV1–6)と WsStream(ストリーミング driver、SINV1–8)の 2 spec。後者は 109 distinct states を網羅探索。
• Lean 4: Basic.lean(P1–P7、マスキング・長さ・opcode・close コード)と Utf8.lean(P8、UTF-8 健全性)。すべて sorry 無し、依存公理は標準 3 つのみ。
• 実装は三層の性質を橋渡しテストで固定する TDD で駆動した。

Hakkadaikon

0. 概要

項目	websocket/	websocket-vibe/
言語	C	C
実装規模 (src)	約 5,166 行	約 1,971 行
テスト規模	約 305 行 (C++ unit)	約 881 行 (C unit + Python E2E)
形式検証	なし	Lean 4 で 1,315 行 (28 仕様性質)
I/O モデル	epoll/kqueue 直結イベントループ	Sans-IO コア + epoll デモサーバ
プラットフォーム抽象化	arch/ で直接 syscall(asm 含む)、Linux/macOS	platform/ で syscall ラッパ、freestanding

Hakkadaikon

{
    "sig": "6c047ad5f557b83f1e2637fe778a00cbcd9acf5d3590a51ffb149c086123f36c35299ccd890682ddda39e68f621c113804ea0f9ceb00a5fd5c6ae4de869e6b93",
    "kind": 3,
    "created_at": 1782031763,
    "id": "07013a1e354f8a837b08592201ecec212943f0c18083314143793b66af9f5b67",
    "content": "{\"wss://relay.primal.net\":{\"write\":true,\"read\":true},\"wss://relay.mostr.pub\":{\"read\":true,\"write\":true},\"wss://relay-jp.shino3.net\":{\"read\":true,\"write\":true},\"wss://relay.nostr.band\":{\"read\":true,\"write\":true},\"wss://eden.nostr.land\":{\"read\":true,\"write\":true},\"wss://nostr.wine\":{\"read\":true,\"write\":true},\"wss://r.kojira.io\":{\"read\":true,\"write\":true},\"wss://nos.lol\":{\"read\":true,\"write\":true},\"wss://nrelay.c-stellar.net\":{\"read\":true,\"write\":true},\"wss://relay.yozora.world\":{\"write\":true,\"read\":true},\"wss://welcome.nostr.wine\":{\"read\":true,\"write\":true},\"wss://bitcoiner.social\":{\"read\":true,\"write\":true},\"wss://relay.damus.io\":{\"read\":true,\"write\":true

Hakkadaikon

[
  {
    "serif": "このお菓子、おいしくなかったからあげる",
    "location": "宮城県仙台市泉区向陽台",
    "category": "声かけ",
    "date": "2026/05/13"
  },
  {
    "serif": "お菓子あげるからおいで",
    "location": "福岡県福岡市南区高木",