Mtg.Engine

A Lean 4 rules engine for Magic: The Gathering, built with Lake.

The engine follows the Magic: The Gathering Comprehensive Rules effective 25 September 2026. The official text is published by Wizards of the Coast at:

https://media.wizards.com/2026/downloads/MagicCompRules%2020260925.txt

Prerequisites

Lean is managed by elan. Installing elan and then running any Lake command inside this repository downloads the toolchain pinned in lean-toolchain.

curl -fsSL https://elan.lean-lang.org/elan-init.sh | sh -s -- -y
export PATH="$HOME/.elan/bin:$PATH"

Build

lake build

Demo

Mtg.Demo is a console application that starts a game using the Hobbit Welcome Decks (40-card limited) and either runs a heuristic demonstration or lets you play interactively. Repeat --name NAME and --deck COLOR or --deck FILE once per player (paired in order). COLOR is white, blue, black, red, or green (also W, U, B, R, G). FILE is a text deck list of supported catalog card names (optional N or Nx counts; # comments; Sideboard ignored). Default is Chandra (red) and Nissa (green). A game needs at least two players:

lake exe mtg-demo
lake exe mtg-demo -- --name Elspeth --deck white --name Jace --deck blue
lake exe mtg-demo -- --name Alice --deck alice.txt --name Bob --deck bob.txt
lake exe mtg-demo -- --name Elspeth --deck white --name Jace --deck blue --name Liliana --deck black
lake exe mtg-demo -- --name Liliana --deck black --name Chandra --deck red --interactive
lake exe mtg-demo -- --interactive
lake exe mtg-demo -- --interactive --visible
lake exe mtg-demo -- --interactive --input opening.txt
lake exe mtg-demo -- --interactive --output session.txt
lake exe mtg-demo -- --interactive --input session.txt --output session.txt
lake exe mtg-demo -- --multiplayer
lake exe mtg-demo -- --multiplayer --visible
lake exe mtg-demo -- --multiplayer --input opening.txt
lake exe mtg-demo -- --multiplayer --output session.txt
lake exe mtg-demo -- --multiplayer --input session.txt --output session.txt
lake exe mtg-demo -- --decides Nissa
lake exe mtg-demo -- --interactive --decides Chandra
lake exe mtg-demo -- --seed 42 --fuel 200
lake exe mtg-demo -- --norandom --decides Chandra --interactive
lake exe mtg-demo -- --norandom --input opening.txt
lake exe mtg-demo -- --constructed --name Alice --deck alice.txt --name Bob --deck bob.txt

--interactive is the first named player against heuristic opponents. --multiplayer lets you issue every player's actions from the console; the prompt names who must act. --decides NAME names the player who chooses who takes the first turn (CR 103.1). By default the demo picks one at random using --seed. --constructed validates decks as constructed play (CR 100.2a: minimum 60, four-of except basic lands). Without it the demo is limited play (CR 100.2b), matching the 40-card Welcome Decks. --norandom stops the engine from shuffling or rolling. The demo asks who was chosen at random to decide (unless --decides is set) and asks for each later random result: shuffle [id...] (library order, bottom first; no ids keeps the current order), order [id...] (a subset put into a zone in that order), pick <id> (a randomly selected object), random <n> (a 0-based index), or flip heads / flip tails. --input / --output may be used with --norandom even in --auto so those answers can be replayed. In --interactive, the first named player is prompted for first <name> when they are deciding; a heuristic opponent otherwise chooses to go first. In --multiplayer, the deciding player is prompted. In --auto, the deciding player (heuristic) chooses to go first. --input FILE (one command per line) runs those commands first in either interactive mode, then further commands come from the console. Lines that start with -- are additional flags instead of commands. --output FILE writes accepted game-state commands from the input file and from the console (one per line), so a session can be replayed with --input. When --output is a different file, flags read from --input are written first. Incorrect commands and commands that do not change the game (state, quit, help, visible) are omitted. autopay is written as the individual tap and pay commands it performs. your turn, my turn, main phase, and attack step keep passing until the named step (or until a player must take a non-pass action). Those shortcuts and ignore only pass for the player who issued them; other players may still act. Other players' pass-until shortcuts (written as pass sequences) do not interrupt those commands. ignore keeps passing until your next main phase and is not interrupted at all. Those shortcuts are written as the individual pass commands they perform. your turn, my turn, main phase, and ignore use noattack when declaring attackers; noblock is used when that is the only legal declaration. When --input and --output are the same file, the existing flags and commands are replayed and new accepted console commands are appended. After those commands are exhausted (or when no input file is given), a cost with only one legal payment is paid automatically; the demo writes the individual commands (tap, pay, sacrifice) to --output. Put --decides NAME among the input-file flags (or pass it on the command line) and first <name> after those flags when the first named player is the one deciding, so a replay asks the same player.

In either interactive mode, visible prints the board as the acting player sees it (other players' hand sizes but not the cards themselves). visible on (or the --visible flag) keeps state and later log/zone updates in that player view. With --interactive, that player is the first named player; with --multiplayer, the view follows whoever currently must act.

Project layout

Path	Purpose
lakefile.toml	Lake package (Mtg.Engine library with the precompiled Mtg.Engine.Card, Mtg.Engine.Game, and Mtg.Engine.Fixture plugins, MtgDemo demo library, mtg-demo and oracle-roundtrip executables).
lean-toolchain	Pinned Lean toolchain version.
Mtg/Engine.lean, Mtg/Engine/	The Mtg.Engine library.
Mtg/Engine/Catalog/	Oracle cards used by the demo decks (engine remains card-agnostic).
Mtg/Engine/Tests/	Compile-time engine smoke tests, one file per topic.
Mtg/Demo.lean, Mtg/Demo/	Console demonstration, text rendering, Welcome Deck lists, and deck-list file parsing.
Mtg/OracleRoundtrip.lean	lake exe oracle-roundtrip: parses sample printed cards with the compiled Oracle parser.

Current coverage

The first slice of the engine models the two-player game:

• colors and mana (CR 105–107, 202)
• cards, types, zones, and turn structure (CR 108–110, 205, 300, 400, 500)
• starting a game, choosing who takes the first turn, opening hands, London mulligans (including the free first mulligan in multiplayer and Brawl, CR 103.5c), first-turn skipped draw (CR 103, 103.1, 103.5, 103.8a)
• ending a game via life, empty library, or concession (CR 104, 704.5), the legend rule (CR 704.5j), and a player leaving a multiplayer game (CR 800.4 and 800.4a–p: owned objects leave, control effects end, leftover controlled objects are exiled, leftover combat damage and costs are skipped, the turn continues without an active player, and until-next-turn effects expire when that turn would have begun)
• playing lands, including additional land plays this turn (CR 305.2b), activating mana abilities (including {T}: Add for each permanent of a listed type, and {T}: Add X mana of any color equal to power that may be spent only on Elf spells and abilities), activating other abilities of permanents (CR 602, including modal abilities at 601.2b / 700.2), playing granted cards from exile, and casting spells (CR 601.2, including choosing modes at 601.2b / 700.2, announcing a value for {X} at 107.3a / 601.2b, announcing additional or alternative costs at 601.2b before targets, announcing targets at 601.2c (every target of one instance of the word “target” together; each instance sequentially), then determining and paying costs such as sacrificing an artifact or creature at 601.2f / 601.2h or paying extra generic mana as an alternative additional cost, or paying life at 118.3b / 119.4, cost reductions if a creature died this turn or the target was dealt damage this turn, the target is tapped, or the target is an attacking nontoken creature, graveyard activations, and mana abilities at 601.2g)
• combat declaration and combat damage assignment (CR 510.1c–d), including first strike (CR 702.7b), islandwalk (CR 702.14), menace, “can't be blocked except by N or more”, “can't be blocked if power is N or less”, and lifelink
• static abilities that grant trample, pump other creatures of listed types, pump an enchanted or equipped creature, set power and toughness equal to the number of lands you control (in all zones), or restrict blocking unless you control a Goblin or Orc; an until-end-of-turn restriction that creatures without flying can't block; attack triggers that pump power, set another creature's base power and toughness, give another creature +2/+0 and trample, scry, scry when you attack with one or more Elves, or gain life while you control a creature with power 4 or greater (Ferocious); scry triggers that pump for each card looked at; becomes-blocked triggers that damage blocking creatures, flash, Aura spells that enchant a creature (including overwriting its creature types), Equipment (including Equip), enters triggers that scry (any number to the bottom, the rest on top in any order), draw a card, search the library for a Forest card, may discard a card to draw, make a target opponent sacrifice a creature, or deal damage divided as you choose among one, two, or three targets (including whenever a creature enters or attacks), return an Elf card from your graveyard and gain life equal to its power, pumps when another Elf you control enters, landfall triggers that put +1/+1 counters on a target creature you control or give this creature +1/+1 until end of turn, triggered abilities waiting until a player would receive priority and going on the stack in APNAP order with each player choosing the order of their own (CR 603.3b), activated pumps that last until end of turn (including paying life), activated abilities that put +1/+1 counters on the source, dies triggers that deal damage equal to last-known power to a creature an opponent controls, cast triggers that deal damage to each opponent when you cast an instant or sorcery, {4}, {T} making a target creature unblockable until end of turn, typecycling from hand (Mountaincycling, Swampcycling: discard this card, search for a land of that type, put it into your hand, then shuffle), and adventurer cards (casting an Adventure, then the creature from exile), countering spells (including unless the controller pays, and exiling a permanent spell with a free recast), scry-then-draw, tapping one or two creatures, exchanging control, putting a creature on top or bottom of its owner's library, hope counters, linked exile until a source leaves, draw and second-card triggers, Equip Human, and instant/sorcery-restricted mana
• modal instants, destroy (including target creature, or a target artifact or land, after which creatures without flying can't block this turn), mass until-end-of-turn P/T changes, drawing and losing life (Night's Whisper), +1/+1 counters, hexproof, indestructible, deathtouch, lifelink, menace, vigilance, until-end-of-turn keyword grants including can't be blocked, until-end-of-turn loss of indestructible, replacing death with exile this turn (CR 614.6: the die event never happens; the modified exile may trigger leaves-the-battlefield abilities; impossible return instructions are ignored), destroying permanents or dealing damage with activated abilities, a creature you control dealing damage equal to its power to a creature an opponent controls, enters triggers that make each player sacrifice a creature, a target opponent sacrifice a creature, or each opponent discard a card, and lasting type-changing animations (a permanent that becomes a Bear creature with power and toughness equal to lands you control)
• Saga enchantments (CR 714): lore counters as a Saga enters and as the first main phase begins, chapter abilities on the stack with the catalog effects (damage, destroy, mana, tutor, landfall, pumps, discard, amass, life drain, hexproof and damage prevention while the Saga remains, draw, linked exile, delayed blink, Treasure-into-Dragon, recruit, and graveyard return), and sacrificing a Saga after its final chapter leaves the stack (CR 714.4)
• planeswalkers: entering with loyalty (CR 306.5b), loyalty abilities once per turn at sorcery speed with loyalty costs including −X (CR 606), abilities granted to planeswalkers you control, attacking planeswalkers (CR 506.3 / 508.1b; demo: attack <id> at <planeswalker id>), damage removing loyalty (CR 120.3c), and the 0-loyalty state-based action (CR 704.5i); emblems and effects that last until your next turn in the command zone
• Reality Fracture mechanics checked against its judge rulings: Empower Jace, prepare, surveil (CR 701.25), split second (CR 702.61), convoke (CR 702.51), proliferate with a choice of permanents and players (CR 701.34), stun counters (CR 122.1d), exhaust (CR 702.177), and instants and sorceries that don't resolve when all their targets are illegal (CR 608.2b); every Reality Fracture card is fully parsed and modeled, including its activated, loyalty, and static abilities, restricted mana, and ward costs other than mana
• cleanup without priority except the CR 514.3a state-based-action window
• a console demo with a heuristic opponent or multiplayer interactive play, including choosing the starting player (CR 103.1), autopay to activate mana abilities and pay a locked-in cost (recorded as tap and pay), pass-until shortcuts (your turn, my turn, main phase, attack step, ignore) recorded as individual pass commands (your turn, my turn, main phase, and ignore use noattack when declaring attackers; each shortcut only passes for the player who issued it) — other players' pass shortcuts do not interrupt a pending shortcut, and ignore is never interrupted — and attach to attach an Equipment when asked (e.g. Vow to Erebor)