0a8e77e949
- Moved everything from ideas/passepartout/ to projects/passepartout/ - Moved legal structures to projects/flags/ - Created missing _index.org files for all subdirectories - Stripped redundant passepartout- prefix from filenames - Rewrote root _index.org as generalized brain index (projects + concepts) - Updated Hugo nav to Projects/Concepts - Updated build script section descriptions - Deleted stale ideas/passepartout-economics.md orphan
2.1 KiB
The Self-Driving Lisp Machine
A Tenstorrent P150 (~72 RISC-V Tensix cores) running Passepartout: 72 RISC-V cores running Lisp microcode, one core dedicated to ACL2, one to Screamer, the rest to gate verification and fact store operations.
The self-driving threshold: the system can synthesize and load its own FPGA microcode or Tensix dispatch programs from within the running Lisp image. The system profiles its own gate verification latency, proposes a new microcoded instruction for the hot path, compiles RISC-V assembly from ACL2-verified specifications, loads it via PCIe DMA from within SBCL, benchmarks it — and rolls back if slower.
Every subdomain involved is software — the most codifiable domain. RISC-V ISA, SBCL internals, ACL2 metafunctions, CIC type theory, compiler optimization — all can flip to symbolic sufficiency within days to weeks of ingestion.
Timeline: ~6,000 lines of new code (microcode, PCIe DMA, Tensix management, benchmark harness). ~60 cycles at current velocity. 2-4 weeks. Total from today: 6-10 weeks. See time estimates for the velocity model behind these numbers.
The Tenstorrent approach is dramatically simpler than FPGA because the microcode is RISC-V assembly (software), not FPGA bitstream (hardware with minutes-per-iteration synthesis). The Lisp Machine security model — unified memory, tagged architecture, no MMU — applies directly because the Tensix cores share the same address space. Verification appliance economics apply: a certified Lisp Machine at scale replaces compliance hardware. See why Lisp is economically viable now and upgrade lifecycle for the economic and deployment foundations.