Hoare/Static.lean

View source on GitHub

iteration_stable_is_triple

IterationStable is exactly a Hoare triple where precondition equals postcondition: {c} f {c}. This is a loop invariant — the predicate survives application of f.

theorem iteration_stable_is_triple [Monad M] [Support M]
    {f : Kernel M α α} {c : Contract α}
    : IterationStable f c ↔ Triple c f c

StaticOn

A kernel is static on predicate c if: for any input satisfying c, the only possible output is the input itself. This is Fritz's "e acts as identity on its own image" — strictly stronger than IterationStable (which only requires the output to satisfy the predicate, not to equal the input).

def StaticOn [Monad M] [Support M]
    (f : Kernel M α α) (c : α → Prop) : Prop :=
  ∀ a : α, c a → ∀ b : α, Support.support (f a) b → b = a

static_implies_stable

StaticOn implies IterationStable: if the output equals the input, and the input satisfies c, the output trivially satisfies c. The converse does not hold in general.

iteration_stable_comp

Composing two iteration-stable kernels for the same contract gives an iteration-stable kernel. The invariant propagates through composition — like a loop invariant through sequential code.

theorem iteration_stable_comp [Monad M] [LawfulMonad M] [Support M]
    {f g : Kernel M α α} {c : Contract α}
    (hf : IterationStable f c) (hg : IterationStable g c)
    : IterationStable (Kernel.comp f g) c

The proof decomposes the bind: an intermediate value mid satisfies c (from hf), then the final value satisfies c (from hg applied to mid).

iteration_stable_id

The identity kernel is trivially iteration-stable for any contract. Since the output is the input, the contract is preserved.

Connections

• Hoare/Core.lean — imported; iteration stability is a self-loop triple
• Contracts.lean — IterationStable is defined there; this file gives the Hoare characterization
• Handshake.lean — iteration stability ensures the pipeline loop survives re-application