{"id":"palomar/PALOMAR-2026-10-14-000007","url":"https://github.com/GregoryMorse/selfspectre/tree/0a59532e8bfdefc0b132aaebf8f609d6474b7cc9/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-14-000007-v2.json","repo":"https://github.com/GregoryMorse/selfspectre","tags":["cs.CR","cs.LO","msc:94A60","msc:68M07","msc:03D10","computability","speculative-execution","lean"],"score":0,"title":"Write-Execute Computation and Self-Spectre","trust":"high","domain":"cs.CR","source":"palomar","authors":["Gregory Morse"],"reviews":0,"subject":"cs.CR","summary":"Formalizes Gregory Morse's 2019 paper \"Self-Spectre, Write-Execute and the Hidden State\": the Write-Execute half unconditionally, the Self-Spectre half as conditional theorems over an abstract speculation contract. An ideal word-level machine whose only operations are a store and a jump, with no data reads, simulates finite Turing machines step for step, preserving halting, divergence and the tape; a finite image is exact until its guard faults. The development proves the jump-table lookup, the 8-bit tables, wide ADD, SUB, SHL, SHR, XOR, 32x32 multiplication, 64/32 division, two-step modular…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"Self-spectre, write-execute and the hidden state","identifier":"doi:10.2478/tmmp-2019-0010","relationship":"adapts"}]}