Structured Resource Profiles

This file defines a compositional resource profile for open computations.

A ResourceProfile ω κ separates two kinds of cost:

• intrinsic : ω, the concrete runtime cost of the code itself;
• usage : κ →₀ ℕ, a symbolic count of how often the code invokes each external capability.

This split is useful for reduction proofs. We can first analyze an open reduction body in terms of its intrinsic overhead and interface usage, and only later instantiate those interface calls with the cost profiles of the adversaries or subroutines that implement them.

structure ResourceProfile (ω : Type u_1) (κ : Type u_2) : Type (max u_1 u_2)

Structured resource profile for open computations.

intrinsic is the concrete cost paid by the computation itself. usage k counts how many times the computation invokes external capability k.

• intrinsic : ω
• usage : κ →₀ ℕ

theorem ResourceProfile.ext {ω : Type u_1} {κ : Type u_2} {x y : ResourceProfile ω κ} (intrinsic : x.intrinsic = y.intrinsic) (usage : x.usage = y.usage) : x = y

theorem ResourceProfile.ext_iff {ω : Type u_1} {κ : Type u_2} {x y : ResourceProfile ω κ} : x = y ↔ x.intrinsic = y.intrinsic ∧ x.usage = y.usage

def ResourceProfile.ofIntrinsic {ω : Type u_1} {κ : Type u_2} (w : ω) : ResourceProfile ω κ

Pure intrinsic cost with no external capability usage.

def ResourceProfile.ofUsage {ω : Type u_1} {κ : Type u_2} [Zero ω] (u : κ →₀ ℕ) : ResourceProfile ω κ

Pure external usage with zero intrinsic cost.

noncomputable def ResourceProfile.single {ω : Type u_1} {κ : Type u_2} [Zero ω] (k : κ) (n : ℕ := 1) : ResourceProfile ω κ

A single capability use counted n times, with zero intrinsic cost.

@[implicit_reducible]

instance ResourceProfile.instZero {ω : Type u_1} {κ : Type u_2} [Zero ω] : Zero (ResourceProfile ω κ)

@[implicit_reducible]

noncomputable instance ResourceProfile.instAdd {ω : Type u_1} {κ : Type u_2} [Add ω] : Add (ResourceProfile ω κ)

@[simp]

theorem ResourceProfile.intrinsic_zero {ω : Type u_1} {κ : Type u_2} [Zero ω] : intrinsic 0 = 0

@[simp]

theorem ResourceProfile.usage_zero {ω : Type u_1} {κ : Type u_2} [Zero ω] : usage 0 = 0

@[simp]

theorem ResourceProfile.intrinsic_add {ω : Type u_1} {κ : Type u_2} [Add ω] (a b : ResourceProfile ω κ) : (a + b).intrinsic = a.intrinsic + b.intrinsic

@[simp]

theorem ResourceProfile.usage_add {ω : Type u_1} {κ : Type u_2} [Add ω] (a b : ResourceProfile ω κ) : (a + b).usage = a.usage + b.usage

@[simp]

theorem ResourceProfile.intrinsic_ofIntrinsic {ω : Type u_1} {κ : Type u_2} (w : ω) : (ofIntrinsic w).intrinsic = w

@[simp]

theorem ResourceProfile.usage_ofIntrinsic {ω : Type u_1} {κ : Type u_2} (w : ω) : (ofIntrinsic w).usage = 0

@[simp]

theorem ResourceProfile.ofIntrinsic_zero {ω : Type u_1} {κ : Type u_2} [Zero ω] : ofIntrinsic 0 = 0

@[simp]

theorem ResourceProfile.intrinsic_ofUsage {ω : Type u_1} {κ : Type u_2} [Zero ω] (u : κ →₀ ℕ) : (ofUsage u).intrinsic = 0

@[simp]

theorem ResourceProfile.usage_ofUsage {ω : Type u_1} {κ : Type u_2} [Zero ω] (u : κ →₀ ℕ) : (ofUsage u).usage = u

@[simp]

theorem ResourceProfile.intrinsic_single {ω : Type u_1} {κ : Type u_2} [Zero ω] (k : κ) (n : ℕ := 1) : (single k n).intrinsic = 0

@[simp]

theorem ResourceProfile.usage_single {ω : Type u_1} {κ : Type u_2} [Zero ω] (k : κ) (n : ℕ := 1) : (single k n).usage = Finsupp.single k n

@[implicit_reducible]

noncomputable instance ResourceProfile.instAddMonoid {ω : Type u_1} {κ : Type u_2} [AddMonoid ω] : AddMonoid (ResourceProfile ω κ)

@[simp]

theorem ResourceProfile.intrinsic_nsmul {ω : Type u_1} {κ : Type u_2} [AddMonoid ω] (n : ℕ) (a : ResourceProfile ω κ) : (n • a).intrinsic = n • a.intrinsic

@[simp]

theorem ResourceProfile.usage_nsmul {ω : Type u_1} {κ : Type u_2} [AddMonoid ω] (n : ℕ) (a : ResourceProfile ω κ) : (n • a).usage = n • a.usage

@[implicit_reducible]

noncomputable instance ResourceProfile.instAddCommMonoid {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] : AddCommMonoid (ResourceProfile ω κ)

def ResourceProfile.toProd {ω : Type u_1} {κ : Type u_2} (c : ResourceProfile ω κ) : ω × (κ →₀ ℕ)

@[implicit_reducible]

instance ResourceProfile.instLE {ω : Type u_1} {κ : Type u_2} [LE ω] : LE (ResourceProfile ω κ)

@[simp]

theorem ResourceProfile.toProd_mk {ω : Type u_1} {κ : Type u_2} (intrinsic : ω) (usage : κ →₀ ℕ) : { intrinsic := intrinsic, usage := usage }.toProd = (intrinsic, usage)

@[simp]

theorem ResourceProfile.le_def {ω : Type u_1} {κ : Type u_2} [LE ω] {a b : ResourceProfile ω κ} : a ≤ b ↔ a.intrinsic ≤ b.intrinsic ∧ a.usage ≤ b.usage

@[implicit_reducible]

instance ResourceProfile.instPreorder {ω : Type u_1} {κ : Type u_2} [Preorder ω] : Preorder (ResourceProfile ω κ)

@[implicit_reducible]

instance ResourceProfile.instPartialOrder {ω : Type u_1} {κ : Type u_2} [PartialOrder ω] : PartialOrder (ResourceProfile ω κ)

instance ResourceProfile.instIsOrderedAddMonoid {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] [PartialOrder ω] [IsOrderedAddMonoid ω] : IsOrderedAddMonoid (ResourceProfile ω κ)

def ResourceProfile.eval {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] (c : ResourceProfile ω κ) (w : κ → ω) : ω

Evaluate a structured resource profile against concrete per-capability costs.

noncomputable def ResourceProfile.instantiate {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (c : ResourceProfile ω κ) (impl : κ → ResourceProfile ω κ') : ResourceProfile ω κ'

Instantiate the symbolic capability usage in c with open implementations impl.

def ResourceProfile.intrinsicAddMonoidHom {ω : Type u_1} {κ : Type u_2} [AddMonoid ω] : ResourceProfile ω κ →+ ω

Additive monoid hom extracting the intrinsic component of a resource profile.

def ResourceProfile.usageAddMonoidHom {ω : Type u_1} {κ : Type u_2} [AddMonoid ω] : ResourceProfile ω κ →+ κ →₀ ℕ

Additive monoid hom extracting the symbolic capability-usage component of a resource profile.

noncomputable def ResourceProfile.evalAddMonoidHom {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] (weights : κ → ω) : ResourceProfile ω κ →+ ω

Additive monoid hom evaluating a structured resource profile against concrete per-capability weights.

@[simp]

theorem ResourceProfile.intrinsic_sum {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] {ι : Type u_5} (s : Finset ι) (f : ι → ResourceProfile ω κ) : (∑ a ∈ s, f a).intrinsic = ∑ a ∈ s, (f a).intrinsic

@[simp]

theorem ResourceProfile.usage_sum {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] {ι : Type u_5} (s : Finset ι) (f : ι → ResourceProfile ω κ) : (∑ a ∈ s, f a).usage = ∑ a ∈ s, (f a).usage

@[simp]

theorem ResourceProfile.intrinsic_instantiate {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (c : ResourceProfile ω κ) (impl : κ → ResourceProfile ω κ') : (c.instantiate impl).intrinsic = c.intrinsic + c.usage.sum fun (k : κ) (n : ℕ) => n • (impl k).intrinsic

@[simp]

theorem ResourceProfile.usage_instantiate {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (c : ResourceProfile ω κ) (impl : κ → ResourceProfile ω κ') : (c.instantiate impl).usage = c.usage.sum fun (k : κ) (n : ℕ) => n • (impl k).usage

@[simp]

theorem ResourceProfile.eval_ofIntrinsic {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] (w : ω) (weights : κ → ω) : (ofIntrinsic w).eval weights = w

@[simp]

theorem ResourceProfile.eval_ofUsage {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] (u : κ →₀ ℕ) (weights : κ → ω) : (ofUsage u).eval weights = u.sum fun (k : κ) (n : ℕ) => n • weights k

@[simp]

theorem ResourceProfile.eval_single {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] (k : κ) (n : ℕ) (weights : κ → ω) : (single k n).eval weights = n • weights k

@[simp]

theorem ResourceProfile.eval_zero {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] (weights : κ → ω) : eval 0 weights = 0

@[simp]

theorem ResourceProfile.eval_add {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] (a b : ResourceProfile ω κ) (weights : κ → ω) : (a + b).eval weights = a.eval weights + b.eval weights

@[simp]

theorem ResourceProfile.eval_nsmul {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] (n : ℕ) (a : ResourceProfile ω κ) (weights : κ → ω) : (n • a).eval weights = n • a.eval weights

@[simp]

theorem ResourceProfile.eval_sum {ω : Type u_1} {κ : Type u_2} [AddCommMonoid ω] {ι : Type u_5} (s : Finset ι) (f : ι → ResourceProfile ω κ) (weights : κ → ω) : (∑ a ∈ s, f a).eval weights = ∑ a ∈ s, (f a).eval weights

@[simp]

theorem ResourceProfile.instantiate_ofIntrinsic {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (w : ω) (impl : κ → ResourceProfile ω κ') : (ofIntrinsic w).instantiate impl = ofIntrinsic w

@[simp]

theorem ResourceProfile.instantiate_zero {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (impl : κ → ResourceProfile ω κ') : instantiate 0 impl = 0

@[simp]

theorem ResourceProfile.instantiate_ofUsage {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (u : κ →₀ ℕ) (impl : κ → ResourceProfile ω κ') : (ofUsage u).instantiate impl = u.sum fun (k : κ) (n : ℕ) => n • impl k

@[simp]

theorem ResourceProfile.instantiate_single {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (k : κ) (n : ℕ) (impl : κ → ResourceProfile ω κ') : (single k n).instantiate impl = n • impl k

noncomputable def ResourceProfile.instantiateAddMonoidHom {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (impl : κ → ResourceProfile ω κ') : ResourceProfile ω κ →+ ResourceProfile ω κ'

Additive monoid hom instantiating the symbolic capabilities in a resource profile with open implementations.

@[simp]

theorem ResourceProfile.instantiate_add {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (a b : ResourceProfile ω κ) (impl : κ → ResourceProfile ω κ') : (a + b).instantiate impl = a.instantiate impl + b.instantiate impl

@[simp]

theorem ResourceProfile.instantiate_nsmul {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (n : ℕ) (a : ResourceProfile ω κ) (impl : κ → ResourceProfile ω κ') : (n • a).instantiate impl = n • a.instantiate impl

@[simp]

theorem ResourceProfile.instantiate_assoc {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} {κ'' : Type u_4} [AddCommMonoid ω] (c : ResourceProfile ω κ) (impl₁ : κ → ResourceProfile ω κ') (impl₂ : κ' → ResourceProfile ω κ'') : (c.instantiate impl₁).instantiate impl₂ = c.instantiate fun (k : κ) => (impl₁ k).instantiate impl₂

Instantiating symbolic capabilities is associative.

Substituting impl₁ into a profile c, and then substituting impl₂ into the resulting profile, is the same as substituting the composite implementation fun k ↦ (impl₁ k).instantiate impl₂ into c directly.

@[simp]

theorem ResourceProfile.eval_instantiate_ofIntrinsic {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (w : ω) (impl : κ → ResourceProfile ω κ') (weights : κ' → ω) : ((ofIntrinsic w).instantiate impl).eval weights = (ofIntrinsic w).eval fun (k : κ) => (impl k).eval weights

Evaluating a purely intrinsic profile after instantiation leaves the intrinsic cost unchanged.

@[simp]

theorem ResourceProfile.eval_instantiate_ofUsage {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (u : κ →₀ ℕ) (impl : κ → ResourceProfile ω κ') (weights : κ' → ω) : ((ofUsage u).instantiate impl).eval weights = (ofUsage u).eval fun (k : κ) => (impl k).eval weights

Evaluating a purely symbolic usage profile after instantiation amounts to evaluating each capability implementation and summing the resulting scalar costs.

@[simp]

theorem ResourceProfile.eval_instantiate {ω : Type u_1} {κ : Type u_2} {κ' : Type u_3} [AddCommMonoid ω] (c : ResourceProfile ω κ) (impl : κ → ResourceProfile ω κ') (weights : κ' → ω) : (c.instantiate impl).eval weights = c.eval fun (k : κ) => (impl k).eval weights

Evaluating a resource profile after instantiating its symbolic capabilities is the same as evaluating the outer profile against the scalar costs induced by the implementations.