inductive Hex.PermGroup.Execution.Resource : Type

Independent cumulative work allowances. These count logical operations and slots, not bytes or elapsed time. sifts counts visited chain levels (including terminal levels); points counts point visits; pairs counts Schreier pairs. images counts permutation-image slots. certificates counts program and certificate nodes, including reserved copies. storage counts auxiliary container slots. Search nodes and refinement tests have their own counters.

• nodes : Resource
• refinements : Resource
• sifts : Resource
• certificates : Resource
• points : Resource
• pairs : Resource
• images : Resource
• storage : Resource

@[instance_reducible]

instance Hex.PermGroup.Execution.instDecidableEqResource : DecidableEq Resource

Equations

• Hex.PermGroup.Execution.instDecidableEqResource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.PermGroup.Execution.instBEqResource : BEq Resource

Equations

• Hex.PermGroup.Execution.instBEqResource = { beq := Hex.PermGroup.Execution.instBEqResource.beq }

def Hex.PermGroup.Execution.instBEqResource.beq : Resource → Resource → Bool

Equations

• Hex.PermGroup.Execution.instBEqResource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Hex.PermGroup.Execution.instReprResource.repr : Resource → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.PermGroup.Execution.instReprResource : Repr Resource

Equations

• Hex.PermGroup.Execution.instReprResource = { reprPrec := Hex.PermGroup.Execution.instReprResource.repr }

structure Hex.PermGroup.Execution.Work : Type

Cumulative producer reservations. Batches may reserve an upper bound before execution; unused reservations are retained, so surplus budget never changes the reported usage. Image slots count permutation storage separately from program nodes and traversal work.

• nodes : Nat
• refinements : Nat
• sifts : Nat
• certificates : Nat
• points : Nat
• pairs : Nat
• images : Nat
• storage : Nat

def Hex.PermGroup.Execution.instDecidableEqWork.decEq (x✝ x✝¹ : Work) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.PermGroup.Execution.instDecidableEqWork : DecidableEq Work

Equations

• Hex.PermGroup.Execution.instDecidableEqWork = Hex.PermGroup.Execution.instDecidableEqWork.decEq

def Hex.PermGroup.Execution.instBEqWork.beq : Work → Work → Bool

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Execution.instBEqWork.beq x✝¹ x✝ = false

@[instance_reducible]

instance Hex.PermGroup.Execution.instBEqWork : BEq Work

Equations

• Hex.PermGroup.Execution.instBEqWork = { beq := Hex.PermGroup.Execution.instBEqWork.beq }

@[instance_reducible]

instance Hex.PermGroup.Execution.instReprWork : Repr Work

Equations

• Hex.PermGroup.Execution.instReprWork = { reprPrec := Hex.PermGroup.Execution.instReprWork.repr }

def Hex.PermGroup.Execution.instReprWork.repr : Work → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Hex.PermGroup.Execution.Budget : Type

Equations

• Hex.PermGroup.Execution.Budget = Hex.PermGroup.Execution.Work

def Hex.PermGroup.Execution.Work.get (w : Work) : Resource → Nat

Equations

• w.get Hex.PermGroup.Execution.Resource.nodes = w.nodes
• w.get Hex.PermGroup.Execution.Resource.refinements = w.refinements
• w.get Hex.PermGroup.Execution.Resource.sifts = w.sifts
• w.get Hex.PermGroup.Execution.Resource.certificates = w.certificates
• w.get Hex.PermGroup.Execution.Resource.points = w.points
• w.get Hex.PermGroup.Execution.Resource.pairs = w.pairs
• w.get Hex.PermGroup.Execution.Resource.images = w.images
• w.get Hex.PermGroup.Execution.Resource.storage = w.storage

def Hex.PermGroup.Execution.Work.add (w : Work) (r : Resource) (k : Nat) : Work

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.PermGroup.Execution.Work.get_add (w : Work) (r s : Resource) (k : Nat) : (w.add r k).get s = w.get s + if s = r then k else 0

structure Hex.PermGroup.Execution.Meter (budget : Budget) : Type

Counters never exceed the supplied allowances. Every successful charge retains this invariant, including when a later operation exhausts its budget.

• used : Work
• bounded (r : Resource) : self.used.get r ≤ Work.get budget r

def Hex.PermGroup.Execution.Meter.empty (budget : Budget) : Meter budget

Equations

• Hex.PermGroup.Execution.Meter.empty budget = { used := { }, bounded := ⋯ }

def Hex.PermGroup.Execution.Meter.available {budget : Budget} (m : Meter budget) (r : Resource) : Nat

Equations

• m.available r = Hex.PermGroup.Execution.Work.get budget r - m.used.get r

def Hex.PermGroup.Execution.Meter.charge {budget : Budget} (m : Meter budget) (r : Resource) (k : Nat) (h : k ≤ m.available r) : Meter budget

Equations

• m.charge r k h = { used := m.used.add r k, bounded := ⋯ }

theorem Hex.PermGroup.Execution.Meter.charge_mono {budget : Budget} (m : Meter budget) (r : Resource) (k : Nat) (h : k ≤ m.available r) (s : Resource) : m.used.get s ≤ (m.charge r k h).used.get s

@[simp]

theorem Hex.PermGroup.Execution.Meter.available_charge {budget : Budget} (m : Meter budget) (r : Resource) (k : Nat) (h : k ≤ m.available r) : (m.charge r k h).available r = m.available r - k

structure Hex.PermGroup.Execution.Exhausted (budget : Budget) : Type

An unmet charge identifies both the exhausted resource and the counters at the stopping point. It makes no claim that the search has finished.

• meter : Meter budget
• resource : Resource
• requested : Nat
• insufficient : self.meter.available self.resource < self.requested

def Hex.PermGroup.Execution.Meter.spend {budget : Budget} (m : Meter budget) (r : Resource) (k : Nat) : Except (Exhausted budget) (Meter budget)

Equations

• m.spend r k = if h : k ≤ m.available r then Except.ok (m.charge r k h) else Except.error { meter := m, resource := r, requested := k, insufficient := ⋯ }

inductive Hex.PermGroup.Execution.Measured (budget : Budget) (α : Type) : Type

A primitive operation either returns its result and updated counters or the exact stopping point. Both alternatives retain the budget invariant.

• ok {budget : Budget} {α : Type} (value : α) (meter : Meter budget) : Measured budget α
• exhausted {budget : Budget} {α : Type} (failure : Exhausted budget) : Measured budget α

@[reducible, inline]

abbrev Hex.PermGroup.Execution.Run (budget : Budget) (α : Type) : Type

A computation threads one meter through all nested operations. Failure retains the counters at the first reservation that could not be met.

Equations

• Hex.PermGroup.Execution.Run budget α = StateT (Hex.PermGroup.Execution.Meter budget) (Except (Hex.PermGroup.Execution.Exhausted budget)) α

def Hex.PermGroup.Execution.Meter.execute {α : Type} {budget : Budget} (meter : Meter budget) (computation : Run budget α) : Measured budget α

Continue an operation with an existing meter; nested work never receives fresh allowances.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Execution.reserve {budget : Budget} (r : Resource) (k : Nat) : Run budget Unit

Reserve work before invoking the operation that uses it.

Equations

• Hex.PermGroup.Execution.reserve r k = do let meter ← get match meter.spend r k with | Except.error failure => throw failure | Except.ok meter => set meter

def Hex.PermGroup.Execution.run {α : Type} (budget : Budget) (computation : Run budget α) : Measured budget α

Evaluate a producer from zero usage. Replay uses a separate invocation and its own allowances; it cannot consume a producer's remaining budget.

Equations

• Hex.PermGroup.Execution.run budget computation = (Hex.PermGroup.Execution.Meter.empty budget).execute computation