Vibe under constraint | NGrislain

Vibe coding is great. You describe what you want, the agent writes it, the tests pass, you ship. It keeps working right up to the moment it does not: the job gets killed by the OOM reaper in production, or it opens ten thousand file descriptors and falls over, or it runs fine on the sample and melts on the real dataset. The code was correct. It just assumed it had infinite memory and infinite file handles, because nothing in the problem statement said otherwise.

These are not logic bugs. They are resource bugs, and they surface late: at integration, at scale, in production. Tests rarely catch them because the test data fits in memory. Code review rarely catches them because the offending line looks completely reasonable. "Load the file, sort it, write the result" is a perfectly good sentence until the file is 400GB.

In a previous post I argued that Lean 4's type system can encode correctness specifications, so the compiler verifies them and the AI cannot ship code that violates them. This post is about the same idea applied to a different class of property: resource constraints. What if "this program never holds more than 100 records in memory" and "this program never has more than 3 files open at once" were facts the compiler checks, not hopes you have at review time?

The full experiment is on GitHub. The short version: encode the limits in the types, hand the agent the unconstrained version, then turn the limits on and watch the implementation reorganize itself into something correct under the budget.

Resource-aware types

The trick is to make resources count in the type. Two resources here: open files and live records in memory. Both follow the same pattern, so I will sketch one carefully and the other quickly.

Start with a single configuration point. A cap is either none (unlimited) or some k (at most k). The proof obligation at every allocation site is capOk:

def capOk (n : Nat) : Option Nat → Prop<br>| some k => n True -- unlimited: always fine

-- both branches are decidable, so `by decide` discharges the proof automatically<br>instance (n : Nat) (cap : Option Nat) : Decidable (capOk n cap) := ...

Now files. The key idea is to thread the number of currently open files through the type. FileIO filesCap n m α is an IO action that starts with n files open, ends with m open, and produces an α. Opening a file goes from n to n + 1; closing goes from n + 1 back to n.

-- a phantom witness: "there are currently n files open"<br>-- the private constructor means only our API can create or transform these tokens<br>structure FileToken (n : Nat) where<br>private mk ::

-- an indexed IO: takes a token witnessing n open files,<br>-- returns a token witnessing m open files, plus a result α<br>def FileIO (filesCap : Option Nat) (n m : Nat) (α : Type) :=<br>FileToken n → IO (FileToken m × α)

-- opening requires a proof that we are under the cap, then increments the count<br>def FileIO.openRead (path : FilePath) (_ : capOk n filesCap := by decide)<br>: FileIO filesCap n (n + 1) (Handle FileMode.Read) := ...

-- closing decrements the count<br>def FileIO.closeHandle (handle : Handle mode) : FileIO filesCap (n + 1) n Unit := ...

-- running requires you to start and end at zero open files<br>-- the only way to get a FileToken 0 is here, so the caller cannot cheat<br>def FileIO.run (env : Env) (x : FileIO env.filesCap 0 0 α) : IO α :=<br>let (tok, a) ← x (FileToken.mk) -- hand out the initial token<br>pure a -- the final token is FileToken 0, enforced by the type

Two things make this airtight. The Handle constructor is private, so the only way to get a handle is through openRead / openWrite, which charge you for it. And FileIO.run demands you start and end at zero, so every file you open must be closed. You cannot leak a handle, and you cannot open one past the cap, because the capOk n filesCap proof would not check.

Memory works the same way, with a twist. Records do not live in your program; they live in a fixed-size Pool. You never hold an Event, you hold a Ref into the pool, and the pool has cap slots. MemM cap n m α tracks the number of live refs from n to m:

-- a bounded pool of `cap` slots; allocation physically fails when full<br>structure Pool (α : Type) where<br>cap : Option Nat<br>data : Array (Option α)<br>...

-- an opaque reference into the pool — constructor is private<br>structure Ref (α : Type) where<br>private mk ::<br>private idx : Nat

-- same pattern as FileIO: a phantom token counts live refs<br>structure MemToken (n : Nat) where<br>private mk ::

-- MemM cap n m α: starts with n live refs, ends with m, produces α<br>-- threads both the token (for the count) and the pool (for the data)<br>def MemM (cap : Option Nat) (n m : Nat) (α : Type) :=<br>MemToken n → Pool Event → IO (MemToken m × Pool Event × α)

-- allocating a ref needs room (n<br>The Ref constructor is private and the record content never escapes the pool, so the pool's slot count is a hard physical ceiling on how many records can exist at once. This is not a soft limit...