# How it works `docs/architecture.md` says what the design *is* and why each decision was taken. This file traces what actually happens, component by component, when you run `lake exe my_infra apply` — the call chain, the types it moves through, and the shape of each piece. It is the document to read before changing the engine. Everything here is checked against the code rather than remembered; where a mechanism has a gap, the gap is named. ## The whole pipeline One apply, end to end. Each box is a real function; the names are searchable. ``` Fleet.lean (your source) ──────────────────────── fleet myApp in paris where resource aws objectStore "assets" { versioning := true } │ │ ELABORATION — happens while the file compiles. │ Infra/Core/Declare.lean's `fleet` command. ▼ ┌──────────────────────────────────────────────────────────┐ │ myApp.keys : Keys one finite key type per │ │ (provider, kind) │ │ myApp.plan : Plan κ a total function from keys │ │ to Status (SpecOf k …) │ │ myApp.regions : Regions where each slot lives │ │ myApp.forgets : List (Released κ) │ │ │ │ myApp : Fleet the four above, as one value │ └──────────────────────────────────────────────────────────┘ │ │ Everything above is a *value*. Nothing has run. │ A wrong region, a dangling reference or a │ nonexistent instance size never gets this far — │ see "Where the compiler stops you" below. ▼ Infra.Cli.run myApp Infra/Cli.lean │ ├─ Ansi.wanted ......... colour on, only if stdout is a terminal ├─ liveFor κ regions ... build Backends; authenticate ONLY the │ clouds κ declares resources in ├─ checkAccounts ....... refuse the wrong account before touching it └─ Ledger.load ......... what this fleet already manages │ ▼ ┌─ OBSERVE ─────────────────────────────────────────────────┐ │ Engine.observe → Engine.pullEntries │ │ │ │ for each (provider, kind) with keys: │ │ for each region in bs.listers p k: │ │ b.list k ................. what is out there │ │ match names against κ.name │ │ for each match: b.read k handle ... its config │ │ │ │ → List (Entry κ) = (p, k, key, {observed, reported}) │ │ → Persistence.save (the cache) │ └───────────────────────────────────────────────────────────┘ │ │ worldOf entries : World κ │ (a *function* from key to Option Sighting) ▼ ┌─ DIFF ────────────────────────────────────────────────────┐ │ Engine.plan → Action.actions │ │ │ │ actionsDeclared T W ... over κ's keys │ │ ++ actionsOrphaned κ rows forgets ... over ledger rows │ │ │ │ → List (Action κ) │ └───────────────────────────────────────────────────────────┘ │ ▼ ┌─ ORDER ───────────────────────────────────────────────────┐ │ Engine.orderActions │ │ builds = non-destructive, Kahn-sorted by HasDeps │ │ kills = destructive, Kahn-sorted then REVERSED │ │ → builds ++ kills.reverse │ └───────────────────────────────────────────────────────────┘ │ ▼ ┌─ APPLY ───────────────────────────────────────────────────┐ │ Engine.push │ │ 1. dry run? print "would …" and return. No writes. │ │ 2. brake: refuse to destroy most of the ledger while │ │ still declaring things (T.declaresAnything) │ │ 3. ADOPT: record every declared resource that exists, │ │ action or not — but only if it is ours; warn about │ │ one that exists and is not (Ownership.describe) │ │ 4. for each action: runAction, then persist both │ │ records if they changed │ └───────────────────────────────────────────────────────────┘ │ ▼ .infra//infra.ledger.json what is managed .infra///.json what was last seen ``` ## The type stack Four layers, each of which the one above cannot see through. This is the part worth understanding first, because every guarantee in the ledger of `docs/diff-semantics.md` is a consequence of it. ``` ProviderId × Kind .aws, .scaleway, .gcp × 14 kinds │ Infra/Core/Kind.lean │ SpecOf is indexed by Kind ALONE, never by provider. │ That is what makes a spec portable. ▼ SpecOf : Kind → … ObjectStoreSpec, QueuesSpec, … │ Infra/Specs/Basic.lean │ Each field is wrapped by `Field`: │ │ Field .required o f α = f α ← NOT wrapped in `o` │ Field .optional o f α = o (f α) │ │ so a required field cannot be "unsaid". Omitting one leaves │ you holding a function, not an incomplete record. ▼ Partial α unknown │ known α │ the "author chose not to say" modality │ Expr K α lit │ observed │ secretValue │ map │ ap │ the "not known until apply" modality │ Infra/Core/Expr.lean ▼ Status V unmanaged │ absent │ present V ⊥ DELETE CREATE/UPDATE ``` Two modalities, and they are not interchangeable: | | `Partial` | `Expr` | |---|---|---| | Means | you did not say | nobody can know yet | | Resolved by | `Fillable`, at plan time | `settleSpec`, at apply time | | Comparable? | yes — `unknown` refines anything | no — it holds functions | `unknown` is not drift. The comparison is *observed ⊑ target*, never the reverse, so a field the target does not mention is never a reason to change anything. ## The `fleet` command A macro, and the only place in the library that manipulates syntax. It runs at elaboration and emits ordinary definitions. ``` fleet myApp in paris where provider aws where resource objectStore "assets" as a { versioning := true } in oregon where resource s3Bucket "logs" { } forget aws queues "old" │ ▼ flatten ── walks the item tree, carrying the enclosing `provider` and `in` context DOWN into each item. Blocks are *scoping*, and scoping is finished before anything is generated. │ ├──▶ Array Res (cloud, kind, name, binding, fields, place) └──▶ Array Rel (cloud, kind, name) │ ▼ group by (provider, kind), preserving declaration order │ ▼ emits: myApp.names.aws.objectStore : List String ["assets"] myApp.keys : Keys via Keys.build myApp.regions : Regions via Regions.covering myApp.plan : Plan via assignFromNamed myApp.forgets : List (Released myApp.keys) myApp : Fleet the four, bundled a : myApp.keys.Key .aws .objectStore ``` Indentation is load-bearing: `withPosition`/`colGt` is what makes a `provider` block a block. Without it the item list is greedy and a block swallows every sibling that follows it — which it did, silently, putting a later `provider scaleway` group inside an earlier `in oregon` one. ## Where the compiler stops you Two different mechanisms, and the difference matters when you add a check. ``` STRUCTURAL — there is nothing to write down ─────────────────────────────────────────── a reference : κ.Key p k an index into THIS fleet a missing required : Field .required unwrapped, so the literal field is incomplete a kind a cloud : Key p k = Nothing no inhabitant, so no key lacks a plan whose shape : Expr has no `bind` cardinality cannot depend depends on an on a post-apply value unknown DECIDABLE — you can write it, and `decide` refuses it ───────────────────────────────────────────────────── @[reducible] def Assert (b : Bool) : Prop := b = true used as an auto-param nobody types: (h : Assert (f.sizes.contains s) := by decide) InstanceType.of .t3 .xlarge32 ← t3 has no 32xlarge Region.of .aws "fr-par" ← not an AWS code Locality.covers ← AWS has no Warsaw region releasing (forget) ← still declared by this fleet NamedKey.of ← name not in this fleet ``` The error is the compiler evaluating your own predicate: ``` could not synthesize default value for parameter '_h' using tactics Tactic `decide` proved that the proposition Assert (InstanceFamily.t3.sizes.contains InstanceSize.xlarge32) is false ``` ## Expressions, and the constructor that is missing ``` inductive Expr (K : ProviderId → Kind → Type) : Type → Type 1 │ ├─ lit α a value you have ├─ observed K p k → ObservedOf k what the cloud will report ├─ secretValue K p .secrets → String this fleet's own secret ├─ map (α → β) → … put a recipe through a function └─ ap Expr (α → β) → … combine two recipes and deliberately NOT: bind : Expr K α → (α → Expr K β) → Expr K β ``` `K` is the load-bearing parameter. `observed` and `secretValue` both take a `K p k` — an index into this fleet — so a recipe can only ever read from a resource that exists in this file. That is where "a reference cannot dangle" comes from. The missing `bind` is the whole design. With `map` and `ap` an unknown value can flow into a *field*; nothing lets it decide *how many things exist*, so the dependency graph is fixed before anything runs. Terraform has the same rule and enforces it per attribute at plan time (`for_each` over an unknown fails); here there is no syntax in which to write it. `expr!` is sugar over exactly that `map`/`ap` chain: ``` expr!"postgres://{secretValueOf pw}@{endpointOf db}/main" ┌─ secrets "pw" ──secretValueOf──┐ │ ├──▶ secrets "db-url" └─ postgres "db" ──endpointOf────┘ Two holes → two dependency edges → both created first, one apply. ``` ## The scheduler Edges come from `HasDeps`, one instance per spec, which reports every reference a spec holds. `Need` distinguishes a handle from a value; ordering ignores the distinction, because both are the same edge. ``` actions ──▶ List (Action κ) │ ├─ builds (create/update/replace/forget) │ stepOf ── dependsOn ── HasDeps │ │ │ ▼ │ schedule (Kahn's algorithm, bounded by │ the step count so the measure is real and │ exhausting it *is* the cycle diagnosis) │ │ │ ▼ dependencies first │ └─ kills (delete/deleteOrphan) same sort, then REVERSED │ ▼ a resource goes before what it needs ``` Reversing a topological sort is the answer wherever the enum happens to sit. Deletion order used to come from the reverse of the `Kind` enumeration, and that deleted a database before the secret that read its endpoint, because `secrets` precedes `postgres` in the enum. *Orphans have no edges, and are ordered by the provider instead.* An orphan carries no spec — its declaration is gone — so it contributes nothing to sort by (`stepOf`'s `.deleteOrphan` case returns `[]`), and the ledger records names and regions rather than references, because recording references too would make it a second copy of the declaration. So `push` does not compute that order, it *discovers* it: a refused `deleteOrphan` is held back rather than fatal, and tried again after the rest of the work-list has run. ``` main pass ─── orphan delete refused ("DependencyViolation") ──┐ │ held ┌─── retry round: everything still deferred ◄─────────────────┘ │ │ │ │ one went none went │ │ │ └─────────┘ ▼ (bounded by the number throw the provider's of deferred orphans) own words, naming the slot ``` Every other verb keeps edges and keeps failing immediately; only orphan deletion converges by repetition. That is the same answer `test/Live.lean`'s `sweepPass` gives to the same question — a sweep has no declaration at all — and the same one AWS's security-group delete already gave for one kind on one cloud (`docs/providers.md`). A refusal that never clears still fails the apply, so a real error is delayed rather than swallowed. ## Divergence: the four outcomes ``` Divergent k : ProviderSpec k → Reported k → List (String × Mutability) │ divergence ──┤ ▼ repairOf k t r │ ┌───────────────────────────┼───────────────────────────┐ ▼ ▼ ▼ empty all .mutable any .forcesReplace │ │ │ ▼ ▼ ▼ NOTHING UPDATE REPLACE already right destroy + create and separately, from extent alone: target present, world absent ──▶ CREATE target absent, world present ──▶ DELETE ``` The first outcome is the one an extent-only comparison could never produce, and it is what makes a second apply come back empty. Two rules that Terraform providers implement ad hoc per attribute, stated once here: - **`unknown` is not drift.** Treating "could not see" as "differs" would rewrite every resource on every apply. - **Lists compare as sets.** Tags, policies and environment variables come back in whatever order the service felt like. `Diverge.lean` sorts first, and the comment there says it is not cosmetic. ## Membership: what is mine The question that decides whether deleting a line destroys the resource. It is answered by the **ledger**, and by nothing else. ``` .infra//infra.ledger.json ┌─────────────────────────────────────────────┐ │ Ledger.Row = cloud, kind, name, region │ │ │ │ NOT indexed by κ.Key — deliberately. │ │ A CachedEntry κ is, so it structurally │ │ cannot hold a row for a resource the │ │ current declaration no longer names, │ │ which is exactly the row that matters. │ └─────────────────────────────────────────────┘ ``` Three ways a row appears or leaves: ``` ADOPT apply, and the declaration names it, and it exists → recorded, even when there is nothing to do. (An apply that only recorded what it *changed* would never claim a converged resource, and nothing could then destroy it. That was a real leak.) ORPHAN the declaration no longer names it → Action.deleteOrphan, addressed by name and routed on the region the row recorded, because the placement table cannot answer for a slot it does not contain. FORGET `forget ""` in the declaration → the row goes, the cloud is untouched. ``` The five-stage live test is this mechanism as a sequence (AWS's counts; see `test/Live.lean`): ``` stage 1 full declare 12 ──▶ 12 managed stage 2 ramp-up declare 12 ──▶ 12 managed same names, same graph, larger numbers → UPDATE stage 3 ramp-down declare 12 ──▶ 12 managed the same paths back down stage 4 trimmed declare 11 ──▶ 11 managed │ drops 2 (lines GONE — only the ledger knows) └── adds 1 → CREATE stage 5 empty declare 0 ──▶ 0 managed everything is an orphan; this is `apply` reaching the same place `destroy` does, and it is `Plan.absent` over stage 1's own key family — see "Which clouds get authenticated" below for why that last clause is load-bearing ``` *What the ledger is not.* It is local and gitignored, so it does not survive a CI job. `Infra.Core.Ownership` is what actually decides membership now — a marker tag written on create for the kinds `Backend.ownershipInfo` covers (`.objectStore` on all three clouds, `.awsInstance` on AWS), plus a realm and an exclusion list — so the ledger for those kinds is a rebuildable cache (`infra discover`) rather than the sole record. A kind `ownershipInfo` cannot yet read tags for still falls back to ledger membership alone, so `lake test -- sweep` remains what finds debris a ledger cannot name for those: it asks the account, matching on the `ci-tests-infra-` prefix. The procedure — that verb versus `destroy`, the Cleanup workflow and its review gate, and the three things a sweep structurally cannot reach — is in [`../ci/README.md`](../ci/README.md). ## Backends: three ways to reach a cloud ``` structure Backends where backend : ProviderId → Backend the cloud's default region backendFor : ProviderId → Kind → String → Backend by SLOT — resolves the region from `Regions.codeFor`. Used for read/create/update/delete/secretValue. backendAt : ProviderId → String → Backend by REGION, named directly. For an orphan, whose slot the placement table no longer contains. listers : ProviderId → Kind → List (Backend × (String → Bool)) one entry per region in play, each paired with the test for which slot names belong to it. `list` is the one call with no slot to route on: it asks a REGION what is in it, and its answers must be matched only against the slots placed there. ``` Routing lives here rather than in the engine because the engine has no credentials and no idea what a region is. It knows only slots. `Backend` itself is a record rather than a class, so `Backends` can be a total function over `ProviderId` without sigma gymnastics. ### Which clouds get authenticated, and the hole that leaves `Infra.Cli.liveFor` builds all four of those from **`κ.providers`** — the clouds the declaration's key family names. That is what lets an all-Scaleway fleet run without AWS credentials, and it is deliberate. The consequence is not: a provider `κ` does not name gets `Infra.Providers.placeholderBackend`, whose `delete` returns `()` and whose `list` returns `[]`. For a declaration that names *nothing at all* — which is the same statement as a teardown, see `Plan.absent` — that means every backend is a placeholder, and a teardown of a full ledger becomes a loop of successful no-ops that empties the ledger and touches no cloud. It takes milliseconds and reports success. That is not a hypothetical: it is what the 2026-09-08 live runs did on GCP and Scaleway. Both printed `ok — all 5 stages`, both left their whole estate standing, and only AWS came out clean — because its run *failed*, and the workflow's backstop sweep deleted the twelve resources the teardown had not. So a live apply now **refuses the substitution rather than performing it**. `Backend.unreachable : Option String` is how a backend says it cannot reach its cloud and why; `liveFor` sets it on every placeholder it substitutes, and `push`, before running any action, throws if the ledger holds a row for a provider whose backend answers `some`: ``` the ledger records aws/object-store/old-bucket, but no aws credentials were loaded, because this declaration names no aws resources. Refusing to apply: this would report every aws resource as destroyed without deleting any of them. Declare the cloud, or point the ledger elsewhere ``` The field, rather than a test for "is this the placeholder", is what keeps the rule narrow: a placeholder used *deliberately* as a test double answers `none` and is unaffected, so the offline suite — which is placeholders throughout, including its own teardown checks — keeps working. `Main.lean`'s `checkUnreachableRefusal` pins both halves, since neither is visible any other way offline. The other half of the fix is in the test driver: `Live.emptyStage` builds its teardown as `Plan.absent κ` over the cloud's *own* key family rather than as an empty `fleet` of its own, so `κ.providers` still names the cloud and the credentials still load. `#guard (at! awsStages 4).κ.providers = [.aws]` is what stops that regressing — `declared = []`, the guard that was already there, cannot see the difference. The general shape is worth naming, because the fix above closes one instance of it: **a placeholder is indistinguishable from a cloud that agreed.** Every placeholder method answers the way a successful call would. That is the right default for an offline suite and a live-fire hazard everywhere else, so the question to ask of any new path through `Backends` is what it does when the credentials for a cloud were never loaded. ## The two records ``` LEDGER CACHE Holds cloud, kind, name, region ObservedOf per resource Answers what do I manage? what did I last see? Path .infra// .infra///.json infra.ledger.json Written by apply and destroy every refresh Committed no no If lost orphans: resources nothing. One re-read nothing can name restores it ``` Neither can hold a secret. `SecretsObserved` is a handle and a version, no `ObservedOf` has a value field, and `Backend.read` for `.secrets` deliberately never fetches one — `Backend.secretValue` is the only inbound plaintext path, its result goes straight to one create call, and it is never stored. ## The CLI verbs ``` check offline. Placeholder backends, no credentials, no charges. refresh observe + write the CACHE. Never the ledger: observing is not a decision about what is managed. plan observe + diff + print. No mutation, and it does not reach a write — a dry run returns before them. apply the pipeline above. --force overrides the brake. destroy apply against Plan.absent, which is the empty declaration. Not a second mechanism: `.delete` and `.deleteOrphan` share one body and one `Backend.delete` call, addressed by name. ``` ## Reading order - `docs/architecture.md` — what the design is, and why - `docs/diff-semantics.md` — the two axes, the refinement order, and the ledger of what is a compile error and what is not - `docs/persistence.md` — the two records, and why membership is not intent - `docs/coverage.md` — what actually exists and how far it has been run - `docs/tutorial.md` — how to use it