ai-town-rust

AI Town with a Rust backend, PostgreSQL, and game rules extracted to Lean 4 through h5i-app. The React/PixiJS client talks to HTTP and WebSocket endpoints. Agents use NVIDIA NIM or a deterministic stub.

Run

mkdir -p /dev/shm/ai-town-rust/pgdata
docker compose up -d
export DATABASE_URL=postgres://h5i:h5i@127.0.0.1:55432/h5i
export H5I_APP_SECRET=dev-secret
cargo run -p ai-town-server

In another shell:

cd frontend
npm install
npm run dev

Open http://127.0.0.1:5173/ai-town/. The backend listens on port 8080. Set NVIDIA_API_KEY to use NIM; NVIDIA_MODEL overrides the default model, google/diffusiongemma-26b-a4b-it.

Verification

cargo test --workspace
h5i app prove
h5i app mutate

Proof extraction needs Charon, Aeneas, and Lean 4.31.0 (h5i app doctor). h5i app check checks the committed Lean files without extracting again.

Every CPU movement tick checks placement and restores the previous positions if the check fails. Optional CUDA movement writes through Relocate, which checks walkable tiles and player separation before accepting coordinates. GPU mode currently skips agent, conversation, facing, and clock updates. Lean proves placement safety; GPU/CPU behavioral equivalence and the whole server are outside these proofs. See the proof boundary.

Performance

60 ticks of uncontested movement, medians in milliseconds (2026-10-21):

Players	Original AI Town	Rust CPU	GPU with placement check
1,000	1,476.3	14.2	7.4
10,000	128,668.4	147.9	63.5

GPU timing includes preparation, copies, and checked write-back. The original also records position history. This is an in-memory movement comparison; methods, grid-check costs, server latency, and raw samples give the scope and reproduction commands.

Code

• kernel/: pure game transitions; proofs/: generated Lean and theorems.
• server/: HTTP, WebSocket, PostgreSQL, simulation, and agent worker.
• frontend/: React/PixiJS client; gpu/: optional CUDA movement.
• Design notes: port mapping, movement rules, and proof scope.