Kotaro Chikuba mizchi

Zig 0.16で小さなSIMD WebAssemblyを生成する

English version: README.md

Zigの@Vectorを使うと、SIMDカーネルを型安全に記述しつつ、wasm32-freestandingから手書きWATに近い小さなWebAssemblyを生成できる。ただし、ベクトル型で書いたことはSIMD命令の生成を保証しない。Wasm SIMDを明示的に有効化し、出力されたモジュールを検査し、後処理ごとのサイズを実測する必要がある。

このガイドはWASIアプリケーション全体ではなく、ブラウザから呼ぶ小さなleaf kernelを対象にする。コマンドとバイト数は次の環境で確認した。

Zig 0.16.0
wasm-tools 1.245.1

JS から prebuilt Wasm SIMD を呼ぶ実験

MoonBit JS ターゲットの Bytes と同じ Uint8Array を入力とし、単一バイトの miss scan を比較する最小実験です。

本題のend-to-endサンプルは moonbit-demo/main.mbt です。MoonBit自身をJSへコンパイルし、extern "js" グルーから埋め込み済みWasm SIMDを呼びます。

cd experiments/js-wasm-simd/moonbit-demo

WalTier execution flow, in Quint

A model of src/wal.rs written while reading danthegoodman1/waltier, and the four issues it turned up. Each issue has its own PR against the repo; this gist is what those PRs link to for the reasoning.

#	issue	PR
1	`reconcile` runs when nothing was committed	danthegoodman1/waltier#1

celld wake-entry model

A small Quint model of the alarm wake-entry gate in celld v0.2.0 (3f22aedd1ea4d413b93e84afb1ce385f04be84f1), written while investigating denoland/celld#146.

The safety property is the externally visible half of alarm liveness:

oxc_minifier — fuzzing report

Follow-up to #25594 (the ufuzz-style semantic fuzzer). This extends tasks/minifier_fuzz with four more ways of asking whether the minifier preserves meaning, and reports what they found.

Nothing here is a PR yet. Reproductions are included so each finding can be filed or dismissed independently.

Code: mizchi/oxc@feat/minifier-fuzz-expand

celld node lease: clock skew で二重 owner が成立する反例

Author-review copy in Japanese. See the English version for the main write-up.

実験資料。Quintモデルと検証環境をこのディレクトリだけで完結させ、本体へ含めるかは別途判断する。

要約

celldはnode leaseの期限を「書き手の壁時計」で保存し、「読み手の壁時計」で

Using Lean as an Executable Test Oracle

Summary

Lean is useful even when you do not verify the implementation itself. You can encode a specification as a small executable model, generate a test corpus from that model, feed the same inputs to a real checker, compiler, or runtime, and report disagreements as counterexamples.

The essential separation is:

Correctness inside the model: Lean checks the semantic decision procedure and its theorems.
Correspondence with the implementation: an external adapter runs the implementation and compares its observations with Lean's decisions.

SIMD Lexer Pipelines: Classify, Carve, Coalesce, Compress

I prototyped a v128-based lexer optimization using the JSON parser in moonbitlang/core as the target. This note distills the design into a SIMD lexer pipeline that can be applied to JSON, JavaScript, and other languages.

The short version is that bitmasks are indeed the key abstraction. However, the main opportunity is not matching CST node kinds after construction. It is classifying input bytes and extracting only the positions where lexical context can change.

The pipeline

A typical pipeline can be decomposed as follows:

	import { DurableObject } from "cloudflare:workers";
	import { Hono } from "hono";

	interface AppRecord {
	code: string;
	version: number;
	}

	export interface Env {
	WORKSPACES: DurableObjectNamespace<Workspace>;

	[package]
	name = "cognitive-rhythm-eval"
	version = "0.1.0"
	edition = "2024"
	rust-version = "1.85"
	description = "A measurable proxy evaluator for Japanese cognitive writing rhythm"
	license = "MIT"

	[dependencies]
	encoding_rs = "0.8"