Hoare/Graded.lean

View source on GitHub

PreorderedMonoid

A typeclass for grade structures: a carrier type G with addition, zero, a preorder, and a toNat extraction. The key laws: addition is associative with unit, the preorder respects addition, and toNat is both order-preserving and additive. The canonical instance is Nat itself.

class PreorderedMonoid (G : Type) where
  add : G → G → G
  zero : G
  le : G → G → Prop
  toNat : G → Nat
  -- ... associativity, unit laws, monotonicity, toNat laws

GradedTriple

A graded Hoare triple {P} f {Q} @ g combines a behavioral guarantee (every reachable output satisfies Q) with a cost bound (the information drop is bounded by toNat g). The cost is stated additively to avoid natural number subtraction.

def GradedTriple [Monad M] [Support M] {G : Type} [PreorderedMonoid G]
    (P : α → Prop) (f : Kernel M α β) (Q : β → Prop)
    (mα : InfoMeasure α) (mβ : InfoMeasure β) (g : G) : Prop :=
  Triple P f Q ∧
  ∀ a, P a → ∀ b, Support.support (f a) b →
    mα.measure a ≤ mβ.measure b + PreorderedMonoid.toNat g

# Graded triple: {P} f {Q} @ cost
# Behavioral guarantee + information budget.
# Grades are additive: composing costs g1+g2.
import math

def info(items):
    """Information = log2 of number of possibilities"""
    return math.log2(max(len(items), 1))

def filter_stage(items):
    return items[:len(items)//2]  # drop half

def attend_stage(items):
    return items[:3]  # keep top 3

data = list(range(16))
after_filter = filter_stage(data)
after_attend = attend_stage(after_filter)

g1 = info(data) - info(after_filter)
g2 = info(after_filter) - info(after_attend)

print(f"filter: {len(data)} -> {len(after_filter)}"
      f"  cost = {g1:.1f} bits")
print(f"attend: {len(after_filter)} -> {len(after_attend)}"
      f"  cost = {g2:.1f} bits")
print(f"composed cost: {g1:.1f} + {g2:.1f}"
      f" = {g1+g2:.1f} bits (additive)")
print(f"total drop: {info(data):.1f} -> {info(after_attend):.1f}"
      f" = {info(data)-info(after_attend):.1f} bits")

graded_contract_bridge

One direction of the bridge: ContractPreserving plus a supplied cost bound gives a GradedTriple. The grade is whatever the caller provides.

graded_comp

Graded triples compose with additive grades. If {P} f {R} @ g1 and {R} g {Q} @ g2, then {P} f;g {Q} @ (g1 + g2). The cost chain uses toNat_add to convert the composed grade into the sum of costs.

graded_skip

The identity kernel has unit grade: {P} id {P} @ zero. Since the only output is the input itself, the information drop is zero.

graded_weaken

Weakening: a graded triple at grade g1 implies a graded triple at any larger grade g2. Larger grade means a looser cost bound, which is easier to satisfy. Uses toNat_mono for the numeric comparison.

Connections

• Hoare/Bridge.lean — imported; contract_is_triple bridges to the graded version
• Handshake.lean — InfoMeasure and NonExpanding are the ungraded versions of the cost bound
• Hoare/Effects.lean — Boolean effect embedding, a different cost algebra