Instruction Sets, Programs, and Proofs: Semantics, Equivalence, and Optimization develops instruction-set reasoning from a small abstract machine through source-pinned slices of RV64 and x86-64.

The project is both a book and a reproducible evidence system. The 553-page PDF and reflowable EPUB are built from 182,000 words of chapter source with 67 figures. Definitions, claims, computations, and implementation obligations are represented in a dependency-aware ledger rather than asserted only in prose.

Evidence model

Active checked routes include exhaustive byte round trips, observation separation, addition steps, memory and branch traces, runner classifications, and canonical encoding of every legal structured instruction in the small A0 machine. Each route has a source-bound checker and a negative control designed to fail. Finite computations are labeled as such rather than promoted to general theorems.

The repository publishes the manuscript, PDF, EPUB, checksums, build provenance, semantic objects, evidence artifacts, and validation commands together.