Local resource profiles are mandatory at untrusted input boundaries. These counters are maintained by the receiver, never supplied as trusted claims by the sender. Termination proofs do not establish a practical resource bound.

structure ResourceBudget : Type

• wireBytes : ℕ
• expandedBytes : ℕ
• nodes : ℕ
• depth : ℕ
• arrayItems : ℕ
• signatures : ℕ
• schemaBranches : ℕ
• regexSteps : ℕ

instance instReprResourceBudget : Repr ResourceBudget

Equations

• instReprResourceBudget = { reprPrec := reprResourceBudget✝ }

def consumeWork (remaining cost : ℕ) : Option ℕ

Consume actual work before executing it; exhaustion is rejection.

Equations

• consumeWork remaining cost = if cost ≤ remaining then some (remaining - cost) else none

def admitBytes (budget : ResourceBudget) (wire expanded : ℕ) : Bool

Streaming parser must enforce both limits while receiving/decompressing, not after allocating the entire object. Unknown sizes require bounded streaming.

Equations

• admitBytes budget wire expanded = (decide (wire ≤ budget.wireBytes) && decide (expanded ≤ budget.expandedBytes))

def boundedRegex (run : ℕ → String → String → Option Bool) (budget : ResourceBudget) (pattern text : String) : Bool

A bounded regex backend returns none on exhaustion or unsupported syntax. The backend must enforce the supplied step budget (or an equivalent hard deadline).

Equations

• boundedRegex run budget pattern text = if pattern.utf8ByteSize + text.utf8ByteSize > budget.expandedBytes then false else run budget.regexSteps pattern text == some true

theorem exhausted_work_rejected (remaining cost : ℕ) (h : remaining < cost) : consumeWork remaining cost = none