3e32ea9959
All 31 files from ideas/passepartout-economics/ promoted to ideas/ root. - Subfolder's passepartout-economics.org (42-line index) renamed to triad-index.org to avoid collision with root-level full doc - index.org removed (redundant — triad-index.org replaces it) - Root-level passepartout-economics.org: stripped file:passepartout-economics/ prefix from all cross-references (now simple file:foo.org links) - compliance-framework-mapping.org: same prefix cleanup - All internal file: links within the economics docs already used simple names (no prefix) — they resolve correctly from ideas/ root
16 lines
2.0 KiB
Org Mode
16 lines
2.0 KiB
Org Mode
:PROPERTIES:
|
|
:ID: 13e6ae54-2d24-5aa0-b1cd-a7e8e749aa70
|
|
:END:
|
|
#+title: The Self-Driving Lisp Machine
|
|
#+filetags: :passepartout:lisp-machine:hardware:riscv:tenstorrent:
|
|
|
|
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 [[file:sufficiency-flip.org][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 [[file:time-estimates.org][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 [[file:lisp-machine-security.org][Lisp Machine security model]] — unified memory, tagged architecture, no MMU — applies directly because the Tensix cores share the same address space. [[file:verification-appliance.org][Verification appliance]] economics apply: a certified Lisp Machine at scale replaces compliance hardware. See [[file:lisp-economics.org][why Lisp is economically viable now]] and [[file:upgrade-lifecycle.org][upgrade lifecycle]] for the economic and deployment foundations.
|