alaskahoffman/leandoom

(Lean)DOOM: a native Lean 4 DOOM engine with original-WAD support and kernel-checked movement and autoaim proofs. - alaskahoffman/leandoom

9 stars · 2 forks

README

(Lean)DOOM A native Lean 4 reimplementation of the classic DOOM engine, targeting original DOOM and DOOM II WADs. It now loads vanilla-format levels and renders first-person views with WAD artwork, interactive doors, pickups, and a growing combat loop. The fist, pistol, shotgun, four enemy types, damage, and death/restart work. Full gameplay and level progression remain in development. The goal is a faithful port expressed idiomatically in Lean. The current playable build is a prototype: its movement, combat, and rendering still contain approximations and have not demonstrated vanilla demo or pixel compatibility. Replacing those approximations now takes priority over expanding gameplay. Map/artwork decoding, BSP traversal, rendering, and player movement are written in Lean. A small C adapter provides SDL2 window, input, clock, and framebuffer presentation. Python constructs independent test fixtures, drives executable tests, and serves the optional local proof view. There are no Lean package dependencies and no embedded C DOOM engine. Play E1M1 Requires Lean 4.33.0 (via elan), Python 3, SDL2, and pkg-config. On macOS, install the latter tools with brew install python sdl2 pkg-config; on Debian/Ubuntu use sudo apt install python3 libsdl2-dev pkg-config. git clone https://github.com/alaskahoffman/leandoom.git cd leandoom ./scripts/fetch-shareware ./scripts/viewer For the live movement and autoaim proof visualizations, run ./scripts/demo instead of ./scripts/viewer. Place the wide proof window below the game. WASD moves, arrows turn, Shift runs, Ctrl or left click fires, Space uses doors, and 1/2/3 select fist/pistol/shotgun once acquired. Esc quits; R restarts. The engine and audio synthesis run in Lean; SDL handles the platform boundary. The formal proofs cover selected arithmetic and geometry properties, not the whole engine. See the proof companion and the roadmap for the exact scope. Proved against original machine-code bytes: the four core fixed-point operations match DOOM 1.9 under explicit x86 semantics: addition, subtraction and multiplication return identical bits for every input pair; division matches both results and divide-error causes, including INT_MIN quirks. The RNG returns the same values and final indices for any finite sequence of gameplay draws, miscellaneous draws and resets. Run ./scripts/verify-original-mul and ./scripts/verify-original-arithmetic after fetching shareware to regenerate kernel-checked certificates from the original executable. See the arithmetic/RNG proofs and exact scope. These prove the core operations, not all engine arithmetic, random-call ordering, or whole-engine compatibility. Source code is GPL-2.0-or-later; see COPYING.md and the upstream attributions in the source files. DOOM game data belongs to its respective rights holders and is not included in this repository. The fetch script obtains and verifies the original shareware distribution separately. Run Install elan if needed; the lean-toolchain file pins Lean 4.33.0, matching the current edition of Functional Programming in Lean. ./scripts/fetch-shareware ./scripts/lake build ./scripts/lake exe lean-doom inspect artifacts/doom-shareware-1.9/doom1.wad ./scripts/lake exe lean-doom validate artifacts/doom-shareware-1.9/doom1.wad ./scripts/lake exe lean-doom map E1M1 e1m1.svg artifacts/doom-shareware-1.9/doom1.wad ./scripts/lake exe lean-doom render-combat E1M1 '1:0' e1m1.ppm artifacts/doom-shareware-1.9/doom1.wad The default development assets are id Software's original DOOM shareware 1.9, containing Episode 1 (E1M1–E1M9). The fetch script downloads the original shareware archive, checks SHA-256 for both the archive and WAD, and extracts the WAD without running DOS executables. It retains the original archive and readme locally. Expected hashes and map identities are in tests/reference/shareware.json; files stay under ignored artifacts/doom-shareware-1.9/. No game assets are included in the source repository or covered by its source-code license. --offline verifies an existing WAD or extracts a previously downloaded archive without networking. Use MAP01 with a separately supplied DOOM II WAD. Open the generated SVG in an image viewer or browser. The diagnostic automap shows all geometry: red walls, blue special linedefs, gray ordinary two-sided lines, green player starts, and gold other things. Secrets and hidden lines are deliberately visible in this development tool. PWADs go after the base archive, in load order: ./scripts/lake exe lean-doom map MAP01 map01.svg /path/to/doom2.wad /path/to/patch.wad Later duplicate lump names and map markers win. A replacement map must contain its complete map group in a single archive; incomplete replacements are errors. On the development machine, scripts/lake also recognizes the official macOS ARM64 compiler unpacked into .tools/lean-4.33.0-darwin_aarch64. That ignored, local toolchain does not alter the system installation. Other machines can use elan. Interactive viewer Install SDL2 and pkg-config (brew install sdl2 pkg-config on macOS, or the SDL2 development package and pkg-config on Linux), then run: ./scripts/viewer

Explicit map/WAD selection remains available:

Control Action

W/S or up/down arrows Forward/back

A/D Strafe

Left/right arrows Turn

Ctrl or left mouse button Fire selected weapon (hold to repeat)

1 / 2 / 3 Select fist / pistol / owned shotgun

Space Use a nearby door or switch

F Toggle walking / free camera

Q/E Fly down/up (free camera only)

Shift Move faster

R Reset the level, inventory, doors, and player

Escape or window close Quit

The viewer starts in walking mode, with wall/solid-thing collision, a 16-unit player radius, 56-unit height, 24-unit step limit, headroom checks, and gravity. Walking updates at 35 Hz independently of presentation. F enables free flight; pressing F again returns to the last walking position. R resets to player start. Walls, floors, ceilings, skies, transparent midtextures, and animated idle sprites use WAD artwork. Space traces 64 units ahead to use a door or a door switch. The window title shows interaction feedback, keys, health, armor, and ammo. Combat uses the WAD-backed status bar: health, armor, ammo, weapon ownership, keys, and the animated face. Original PLAYPAL damage/pickup/power feedback colors the screen. Walk over keys and pickups to collect them; unusable health/ammo items remain. Zombiemen, shotgun enemies, and demons can see you, pursue, attack, take damage, and die. On death, press R to reset the whole level. Free flight pauses combat. The framebuffer is 320×200 with a 90-degree horizontal field of view. Combat uses a 320×168 world view above the 320×32 status bar; inspection flight remains 320×200. Headless rendering needs no SDL dependency. render uses player 1's start, with the eye 41 units above the containing sector's floor. render-at takes integer x/y/z world coordinates and an angle in degrees, where zero faces east: ./scripts/lake exe lean-doom render-at E1M1 frame.ppm -416 256 41 90 artifacts/doom-shareware-1.9/doom1.wad render and render-at require valid artwork resources and report missing or malformed assets. Use render-flat / render-flat-at with the same arguments for the original diagnostic colors or geometry-only WADs. Scripted walking is available without SDL or artwork resources: ./scripts/lake exe lean-doom walk E1M1 350 2 /path/to/doom.wad This applies one key mask for up to 10,000 ticks and prints position x y feet vz. Masks: forward 2, back 4, strafe left/right 8/16, turn left/right 32/64, fast 512; add masks to combine keys. These are exploration controls, not vanilla ticcmds. The interaction simulation also supports reproducible scripts:

Walk for 27 ticks, press Space once, wait for the door:

`asset patch <lump-name> ...` exports a raw patch.

Bounds-checked IWAD/PWAD directories and little-endian binary reads. Signed coordinates, case-insensitive lump lookup, zero-length markers, and ordered archive overrides. Vanilla THINGS, LINEDEFS, SIDEDEFS, VERTEXES, SEGS, SSECTORS, NODES, SECTORS, and BLOCKMAP decoding. REJECT bytes are retained. Geometry references, subsector ranges, BSP references/cycles, and blockmap lists checked before automap rendering. Command-line inspection, validation of every map, and SVG automap export. Signed 16.16 camera storage, wrapping 32-bit angles, and tested arithmetic primitives. Fixed.divChecked implements reference saturation and signed truncation, including zero-divisor saturation. It explicitly rejects raw INT_MIN operands whose abs behavior is undefined in the C reference. The older Fixed.div? remains a separate diagnostic helper. Exact sine, tangent, and arctangent tables from the pinned source, with lengths encoded as Lean vectors and proof-checked lookup bounds. SlopeDiv retains unsigned wrapping; point-to-angle conversion retains the original octant/axis asymmetries. These foundations are tested independently; the current viewer's movement/projection still use the earlier floating-point implementation. BSP sector queries and bounded front-to-back traversal. Side classification now follows the reference's wrapping differences, sign shortcut, and rounded fixed-point products, including near-partition ties. Near-plane/screen clipping, one-sided walls, upper/lower portal spans, floor/ceiling regions, and per-column occlusion, rendered in Lean. RGB24/PPM output and an optional SDL2 walking/free-camera viewer. PLAYPAL palettes and COLORMAP index remapping, including original damage, pickup, berserk and radiation-suit palette selection in combat. Fixed player colormaps and high-detail invisibility fuzz are connected as described below. PNAMES, TEXTURE1/TEXTURE2, column/post patches, clipped patch composition, transparency, and 64×64 flats. Required patches are cached while composing a map's textures; all map artwork is loaded once before the viewer loop. Perspective-correct wall coordinates, sidedef offsets, upper/lower/one-sided pegging, world-coordinate floor/ceiling mapping, and masked midtexture composition. Episode/map sky selection and suppression of upper walls between sky sectors. Spawn/idle appearance for 115 vanilla thing editor numbers, including directional rotations, paired mirrored frames, sprite offsets, ceiling attachment, and fullbright frames. Single-player medium-difficulty flags select map things. Player starts, teleport/spawner markers, and unknown thing types are not drawn. Per-pixel depth tests for sprites, opaque surfaces, and transparent midtextures. Reference-tested player acceleration, friction, BLOCKMAP collision, three-corner wall sliding, gravity, step recovery, and view bobbing. The free camera remains available. Shared 35 Hz simulation for the SDL viewer and scripted CLI: manual doors, keyed doors, tagged door switches, repeatable buttons, and moving ceiling collision. Normal doors move 2 units/tick, fast doors 8, and raised doors wait 150 ticks. Movement and door thinker kernels now use original fixed-point arithmetic, strict destination tests, countdowns, obstruction responses and removal rules. Closing raise-doors reopen when blocked by the player or a solid map actor; close-only doors wait at the obstruction instead of crushing it. Original map-spawned sector light effects: broken-light flashes, fast/slow strobes (including synchronized ones), glow and fire flicker. The original countdowns, gameplay RNG calls and signed-short light writes are reference-tested. Walkover triggers turn tagged lights on/off or start strobes, preserving one-shot clearing, repeat behavior, callback order and the shared-brightness quirk. Blue/red/yellow cards and skulls, health and armor, ammo, backpack capacity, weapon ownership/ammo grants, and power-up inventory/timers. Collected items disappear; closed walls prevent collecting items through them. Idle/spawn frame sequences with individual tick durations and fullbright flags. Decorations and unsupported monsters animate in place. The initial combat roster has explicit chase, attack, pain, and death states. Pistol windup, first-shot accuracy, repeated-shot spread, ammo use, WAD weapon overlays, muzzle flash, and original fixed-point hitscan and portal-clipped vertical autoaim. Zombieman (3004), shotgun enemy (9), and demon (3002) combat. Sight and bullets check wall intersections and vertical portal clearance. Pursuit respects walls, monster-blocking lines, steps, actors, and the player. Enemy bullets are blocked by shootable actors, including barrels; killed enemies lose solidity at their original A_Fall state action. Green/blue armor absorption, invulnerability protection, player death and full restart. Zombiemen drop five-bullet clips; shotgun enemies drop a shotgun with four shells. Existing pickup caps and ownership rules apply. Separate gameplay and presentation random streams with byte indices, reset, and ordered subtraction. Their lookup bounds and stream independence are proved in Lean; full table sequences are checked against the pinned C reference. Combat uses the gameplay stream, but its call order and AI decisions still do not match vanilla demos.

Resource lumps use last-definition-wins archive lookup. Within the selected TEXTURE1 followed by TEXTURE2, the first matching texture definition wins, as in vanilla. Patch sprite offsets are decoded separately and do not alter texture placement origins. Nonempty patch/texture dimensions are limited to 2048×2048; extended tall-patch conventions and modern texture formats are unsupported. Projection uses floating point. Actual WAD colors/light tables are used, but light-table selection and sky projection are approximate. Texture wrapping uses the image dimensions rather than emulating vanilla's non-power-of-two quirks. Texture/flat animations and most actor AI/action callbacks remain unimplemented. Frames are repeatable on the tested platform, but are not bit-exact vanilla output or guaranteed identical across platforms. The renderer trusts structurally validated map references; it does not prove that an arbitrary map's BSP describes valid convex subsectors. Sprite frame names resolve within each archive's S_START/S_END or SS_START/SS_END namespace, with standalone unnamespaced PWAD replacements also supported. This avoids collisions with unrelated names such as BOSSBACK. Each matching later view overrides earlier views. Missing required rotations and malformed sprite patches are errors. The actor catalog contains spawn/idle appearance, timing, and dimensions, with no DeHackEd or custom actor support. Animated modes validate all required frames before running; missing frames or paired switch textures produce an error. Idle cycles currently start in sync instead of reproducing vanilla's randomized initial state delays. Walking now uses the reference-tested fixed-point player movement sequence: keyboard tic commands, acceleration, original split moves, BLOCKMAP collision, wall sliding, friction, view bobbing, and gravity/step recovery. It honors the WAD's BLOCKMAP, including omissions, and propagates unsupported-domain errors instead of falling back to approximate movement. Door movement/thinker kernels are reference-tested; use dispatch, obstruction detection, combat and actor spawning/updating still include prototype behavior. No demo or full-tick parity is claimed. Original walkover lighting handlers are wired into crossing callbacks; E1M1’s fast lowering floor (36) and repeatable lift (88) also use original spawn/movement rules. Other floor/lift kinds and crushers remain future work. The F toggle never places a walking player at an unchecked free-camera location. Supported use-activated door specials:

Family Linedef numbers

Manual raise/open; normal, locked, fast 1, 26–28, 31–34, 117–118

Tagged raise/open/close switches and buttons 29, 42, 50, 61, 63, 103, 111–116

Tagged locked fast-open switches/buttons 99, 133–137

Door switches change their SW1/SW2 texture; repeatable buttons restore it after 35 ticks. Switch actions target matching nonzero sector tags. Unsupported use specials report their number. Other walkover actions and floor/lift kinds, crushers, exit transitions, and timed sector specials are still pending. Normal exit switch 11 now flips its texture and queues completion; gameplay holds there until the original intermission and next-map stages are implemented. The fist, pistol and shotgun are usable. Keys 1/2/3 select them; picking up the shotgun equips it through the original lowering/raising sequence. Other weapon pickups retain ownership and ammo for later implementation. Zombi

source