no-C・Pure-Rust のプロジェクトは今週、計算のより難しい隅の一つ ——形式手法と計算機代数——に到達し、その周りに一挙にクラスタが 育った。z3rs は Z3 定理証明器のゼロからの移植、puremp は それが立つ任意精度の数値コア、latticefoundry は z3rs を 使って 超最適化する LLVM 型コンパイラ、mathesis は両者を surface するブラウザ数式ノートブック。別途、puregit が git を ——クライアントとサーバで——Pure-Rust で実装した。

z3rs：Pure-Rust の Z3

z3rs は「Pure-Rust、 no_std の Z3 定理証明器 移植、 サードパーティやネイティブ依存なし」だ。Z3（v4.17.0 に固定）を GMP なし、C なし、-sys クレートなし の単一クレートとして 再実装する——唯一の依存は puremp。Z3 は SMT ソルバだ：理論 （整数、実数、ビットベクタ、配列、浮動小数点、…）上の論理式が 充足可能かを判定し、業界中の記号実行・プログラム検証器・制約 ソルバの下に座る。

今週は理論の断片を丸ごと進めた：

• 浮動小数点（QF_FP） — 共通断片が判定できる。記号演算を ビットベクタにビットブラストして：fp.mul、fp.div、fp.sqrt、 fp.fma、fp.roundToIntegral、to_fp 変換、各々が Z3 の構築の 移植で、フォーマット横断にビット厳密。
• 非線形実数演算（QF_NRA） — CAD（円筒代数分解）で判定、 Bareiss 行列式／終結式の連鎖と cofactor 展開フォールバック付き。
• Horn 節 / CHC（Phase G） — 単一および複数述語の制約付き Horn 節、非巡回系を両方向で厳密に判定し、巡回系は素早く辞退 ——プログラム検証器が問題を立てる形だ。

puremp：数値コア

puremp は「Pure-Rust、 クリーンルームの任意精度演算」——整数、有理数、MPFR 級の浮動小数、 十進、複素、多項式、行列、区間、代数的数、no_std。z3rs が必要と する GMP / MPFR の置き換えで、それ自体が小さな計算機代数システム に育っている。今週は塔全体に及んだ：

• 素因数分解 — Montgomery 領域での Pollard rho と ECM、加えて single-large-prime 変種付きの SIQS（自己初期化二次篩）。
• 多項式 — 有限体 GF(q) 上の Cantor–Zassenhaus 因数分解、 Newton 高速除算、Half-GCD、Kronecker 乗算。
• 線形代数 — 任意の環上の除算フリーな行列式と特性多項式 （Berkowitz）、有理行列の厳密固有値、Strassen–Winograd 乗算。
• 汎用代数層 — Ring と Field トレイトで Poly と Matrix が ModInt、GF(pᵏ)、任意の環の上で動く、加えて GF(p) と ℚ 上の 楕円曲線 y² = x³ + ax + b。
• 超越関数 — AGM（Brent–Salamin）の ln、digamma / polygamma、 beta、Bessel 関数。

latticefoundry：LLVM、しかもソルバを使う

latticefoundry は「Pure-Rust のクリーンルームなコンパイラ構築フレームワーク」 ——おおよそ LLVM の役割を独立に作ったもの：型付き SSA IR、検証器、 パスパイプライン、ターゲット非依存のコード生成、機械語／オブジェクト ファイル層、そしてリンカコア。今週の進み方は目覚ましかった： x86-64 ターゲット（SysV ABI、命令選択、本物の機械語エンコーダ）、 続いて再ターゲット性を証明する二つ目の AArch64 ターゲット、 動くネイティブ実行ファイルを生む .lf リンカ、クロスモジュール LTO 付きの -O 最適化パイプライン、DWARF デバッグ情報 （lf build -g）、そして——クラスタへの結びつき——z3rs 超最適化 付きのインプロセス JIT と、proof-carrying な refinement 証明書を 出す「certified」層。さらに lf-cc、C を LatticeFoundry IR に コンパイルするクリーンルームの C フロントエンド（完全な プリプロセッサ、集約型、switch/goto、関数ポインタ）も生やした。

mathesis：その全部の上のノートブック

mathesis は 「ブラウザ内で完結する Mathematica 風の計算ノートブック」—— Wolfram 風の式を打つと、サーバ往復なしにクライアント側で計算した 厳密な 答えが返る。Vue 3 のノートブック UI が WebAssembly に コンパイルした Rust 数式エンジンを包んでおり、そのエンジンは 今週の土台への素直なフロントエンドだ：演算に puremp（楕円曲線、 Gamma / Bessel、任意精度）、求解に z3rs（SatisfiableQ、その双対 TautologyQ、視覚的な Solve ビルダ）。今週はセッション変数、 暗号学的に安全な RNG、シグネチャヘルプ付き autocomplete、 (* … *) コメントを追加した。GitHub Pages で公開中——z3rs / puremp スタックの人間向けの端だ。

puregit：git、クライアントとサーバ

puregit は libgit2 の精神での git の Pure-Rust 実装だ——オブジェクトモデル、 パックファイル、参照、インデックス、そして smart 転送 プロトコルを、クライアントとサーバの両方で、HTTP と SSH 越しに、 オブジェクトハッシュに purecrypto を使って。今週（80 コミット）は 深く行った：デルタ圧縮したパック書き込み、push と fetch の thin pack、upload-pack の side-band-64k 多重化、サーバの SSH upload-pack エントリと post-receive フック、lockfile ベースの ref 更新、commit-graph と multi-pack-index の形式、SHA-256 オブジェクト形式の交渉、リンクされた worktree、reflog の期限切れ。 同じ no-C ツールチェーンのバージョン管理層だ。

erigon-seg：Ethereum の状態ファイル

erigon-seg は Erigon 3 の seg 状態ファイル（.kv / .bt / .kvei）を Pure-Rust で読み・照会・書き・マージする——Erigon が Ethereum の 歴史的状態に使うオンディスク形式だ。v1.0.1 に到達した：本物の Erigon ファイルに対して検証したリーダ、続いて書き込み側（seg パターン圧縮、両レイアウトの .bt ライタ、.kvei bloom ライタ）、 k-way ドメインマージ、KvStack のマルチファイル面。

今週その他

• kataan は test262 を 挽き続けた——イテレータヘルパ、ジェネレータ、重複名の regex グループ、関数と Date のセルへの freeze/seal——さらに約 100 コミットで既知失敗の台帳を削った。
• graphitesql は SQLite エンジンで週百コミットのペースを保った。
• decryptd — 分散 計算プロジェクトの GPU ワーカー：作業チャンクを引き、NVIDIA GPU で走らせ、NVML の温度／電力／スループットをトレイに報告 （いまは ldtray 経由）、 RunPod 向けのコンテナで出荷。
• rsupd — Rust プログラムの署名付きリリース配布とインプレース自動更新（goupd の 後継）で、プログラムは焼き込まれた 32 バイトのフィンガープリント だけで更新を信頼する。
• TibaneApp ＋ libwallet — ウォレットのリカバリ／バックアップ再設計：デシンクした 2FA シェアの修復、reshare セレモニーの確実なタイムアウト、Help & FAQ 画面。
• oxideav-vc2（SMPTE VC-2）と oxideav-ape （Monkey's Audio）——クリーンルームのコーデックが二つ。

来週

z3rs は判定できる断片を SMT-LIB の理論集合全体へ広げる。puremp は その下の CAS 面を埋め続ける。latticefoundry と mathesis は両者に より強く寄りかかる。puregit はプロトコルの穴を塞ぐ。そして先週の システム層——pebbledb、graphitesql、httpsd、usbmagic——も、それぞれの 安定したペースで成熟し続ける。