Reading Notes: Program Logics via Distributive Monoidal Categories

# A Hoare triple {P} c {Q} means:
# "If P holds before c runs, Q holds after."

def hoare_triple(P, c, Q):
    """Check: for every state where P holds, Q holds after running c."""
    def check(state):
        if P(state):
            result = c(state)
            assert Q(result), f"Postcondition failed: {state} -> {result}"
    return check

# Example: {x > 0} double(x) {y > 0}
P = lambda x: x > 0
c = lambda x: x * 2
Q = lambda y: y > 0

check = hoare_triple(P, c, Q)
for x in range(-10, 10):
    try:
        check(x)  # Only checks when P holds (x > 0)
    except AssertionError as e:
        print(e)  # Never fires — the triple is valid

# {P} skip {P}  — for any predicate P

skip = lambda x: x

# If P holds before, P holds after, because nothing changed.
# This is so obvious it feels dumb. But it's a theorem, not an assumption.

# If {P} c1 {R} and {R} c2 {Q}, then {P} c1;c2 {Q}
#
# This is the HANDSHAKE in your framework.
# R is the intermediate condition — the contract between stages.

def compose(c1, c2):
    return lambda x: c2(c1(x))

# Example:
# {x > 0} double {y > 0}  — P=positive, R=positive
# {y > 0} add_one {z > 1}  — R=positive, Q=greater than 1
# Therefore: {x > 0} double;add_one {z > 1}

double = lambda x: x * 2
add_one = lambda x: x + 1
pipeline = compose(double, add_one)

assert pipeline(3) == 7  # 3 -> 6 -> 7, and 7 > 1 ✓

# If {b and P} c {P}, then {P} while b do c {P and not b}
#
# Translation: if the body preserves the invariant,
# the loop preserves it too, and when it exits, b is false.

def while_loop(b, c, state):
    """while b(state): state = c(state)"""
    while b(state):
        state = c(state)
    return state

# Example: count down to zero
# Invariant P: x >= 0
# Guard b: x > 0
# Body c: x - 1
# After loop: x >= 0 AND x <= 0, so x == 0

result = while_loop(
    b=lambda x: x > 0,
    c=lambda x: x - 1,
    state=10
)
assert result == 0  # Invariant held throughout, guard is now false

# If {P} c1 {Q} and {P} c2 {Q}, then {P} if b then c1 else c2 {Q}

def if_then_else(b, c1, c2):
    return lambda x: c1(x) if b(x) else c2(x)

# Example: abs(x) preserves "result >= 0" regardless of branch
absolute = if_then_else(
    b=lambda x: x >= 0,
    c1=lambda x: x,       # positive branch: keep it
    c2=lambda x: -x,      # negative branch: negate it
)

for x in range(-10, 10):
    assert absolute(x) >= 0  # Both branches satisfy Q

# If P1 implies P2, and {P2} c {Q2}, and Q2 implies Q1,
# then {P1} c {Q1}.
#
# You can always demand MORE of the input and LESS of the output.

# We know: {x > 0} double {y > 0}
# Strengthen precondition: x > 5 implies x > 0 ✓
# Weaken postcondition: y > 0 implies y >= 0 ✓
# Therefore: {x > 5} double {y >= 0}

# If {P1} c {Q1} and {P2} c {Q2}, then {P1 and P2} c {Q1 and Q2}
#
# If c separately preserves two properties, it preserves both at once.

# double preserves "positive" AND "even-if-even"
# {x > 0} double {y > 0}
# {x is even} double {y is even}
# Therefore: {x > 0 and x is even} double {y > 0 and y is even}

double = lambda x: x * 2
assert double(4) > 0 and double(4) % 2 == 0  # 4 > 0 and even -> 8 > 0 and even

# TOP:  {P} c {True}   — any command satisfies "True" as postcondition
# BOT:  {False} c {Q}  — if precondition is impossible, triple is vacuously true

# TOP: I don't care what double does, the result "exists" (True)
# BOT: There's no x where x > 0 AND x < 0, so anything goes

# Your nontriviality counterexample proves Q ≠ False (Q ≠ ⊥).
# Without it, your spec could be vacuously true — the BOT case.

# {P} abort {Q}  — a crashing program never produces output,
# so it vacuously satisfies any postcondition.

def abort(x):
    raise RuntimeError("abort")

# {x > 0} abort {y is a unicorn}  — valid! abort never returns,
# so the postcondition is never tested.
# This is why you need the nontriviality counterexample.

# A copy-discard category has two special operations per type:
# - copy(x) = (x, x)     "duplicate the state"
# - discard(x) = ()       "throw the state away"

copy = lambda x: (x, x)
discard = lambda x: None

# A morphism f is DETERMINISTIC if:
#   f(copy(x)) == copy(f(x))
#   "applying f then copying = copying then applying f to both"

# Deterministic example: double
double = lambda x: x * 2
x = 5
assert (double(x), double(x)) == tuple(map(double, copy(x)))
# (10, 10) == (10, 10) ✓  — double is deterministic

# Non-deterministic example: coin flip
import random
def coin_flip(x):
    return x if random.random() > 0.5 else -x

# coin_flip(copy(5)) might give (5, -5) or (-5, 5)
# but copy(coin_flip(5)) always gives (r, r) for some r
# They DON'T match — coin_flip is stochastic.
#
# In your framework:
#   Filter is deterministic (same input, same gate)
#   Attend is stochastic (must be, by the pigeonhole argument)

# The Kleisli category of the subdistribution monad is a
# posetal imperative category.
#
# Translation: stochastic matrices (your pipeline morphisms)
# live in a category where ALL Hoare rules are theorems.

# A stochastic matrix is a function X -> Distribution(Y)
# In Python, it's a function that returns a dict of {outcome: probability}

def stochastic_matrix(x):
    """Example: given input x, return a distribution over outputs."""
    return {x: 0.7, x+1: 0.3}  # 70% stay, 30% increment

# Kleisli composition = compose stochastic functions by marginalizing
def kleisli_compose(f, g):
    """Compose f: X -> D(Y) and g: Y -> D(Z) into X -> D(Z)."""
    def composed(x):
        result = {}
        for y, py in f(x).items():
            for z, pz in g(y).items():
                result[z] = result.get(z, 0) + py * pz
        return result
    return composed

# This composition is what makes the pipeline work.
# The COMP rule for Hoare triples is a THEOREM about this composition.
# Your contract_compose in Lean proves the same thing.

# Your Lean code:
#   ContractPreserving f Q = ∀ input, ∀ output ∈ support(f(input)), Q(output)
#
# In Hoare logic:
#   {⊤} f {Q} = for all inputs (⊤ = no restriction), outputs satisfy Q
#
# They're the same thing.

def contract_preserving(f, Q):
    """Check: for every input, every output in f's support satisfies Q."""
    def check(inputs):
        for x in inputs:
            dist = f(x)
            for y in dist:  # y is in the support if dist[y] > 0
                if dist[y] > 0:
                    assert Q(y), f"Contract violated: f({x}) -> {y}"
    return check

def hoare_top_Q(f, Q):
    """Check: {⊤} f {Q} — precondition is True, so check all inputs."""
    def check(inputs):
        for x in inputs:  # ⊤ means every input qualifies
            dist = f(x)
            for y in dist:
                if dist[y] > 0:
                    assert Q(y), f"Postcondition violated: f({x}) -> {y}"
    return check

# These two functions are literally the same code.
# That's the bridge theorem.
# Lean proves it; Python shows it.

# If stage 1 preserves Q1, and stage 2 preserves Q2,
# does the pipeline preserve Q2?
#
# Only if Q1 is strong enough to serve as the precondition for stage 2.
# But wait — ContractPreserving uses ⊤ as precondition.
# So Q1 doesn't need to be the precondition. The COMP rule says:
#
#   {⊤} f {R}  and  {⊤} g {Q}   implies   {⊤} g∘f {Q}
#
#   ...but only if g preserves Q UNCONDITIONALLY (for all inputs).
#
# That's exactly what ContractPreserving means.
# The handshake isn't about R linking f's output to g's input.
# It's about each stage independently guaranteeing its postcondition.

def compose_contracts(f, Q_f, g, Q_g, inputs):
    """Both stages independently preserve their contracts."""
    contract_preserving(f, Q_f)(inputs)

    # The outputs of f become inputs to g
    all_intermediates = set()
    for x in inputs:
        for y in f(x):
            if f(x)[y] > 0:
                all_intermediates.add(y)

    contract_preserving(g, Q_g)(all_intermediates)
    print("Both contracts preserved through composition ✓")

# The paper derives three kinds of triples from the SAME structure:

# 1. CORRECTNESS (Theorem 79)
#    {P} c {Q}: if input satisfies P, output satisfies Q
#    "Good inputs produce good outputs"
#    YOUR CONTRACTS LIVE HERE.

# 2. INCORRECTNESS (Theorem 81)
#    {S} c {T}: if output matches T, some input matching S reached it
#    "Bad outputs came from bad inputs"
#    This is for BUG FINDING — proving bad states are reachable.

# 3. PREDICATE-CORRECTNESS (Theorem 83)
#    Hybrid: precondition and postcondition are both predicates
#    Includes a SAMPLE rule for stochastic assignment
#    {p[u\s]} u ← s {p}: drawing from distribution s, then checking p

# All three are theorems in any posetal imperative category.
# Stoch is one. So all three work for stochastic pipelines.