Hoare/Comp.lean

View source on GitHub

PipelineTriples

A pipeline where each stage has a Hoare triple with the handshake threading through: postcondition of stage N is precondition of stage N+1. Bundles predicates at each interface point and proofs that each stage satisfies its triple.

structure PipelineTriples (M : Type → Type) [Monad M] [Support M]
    (I : InterfaceTypes) (p : Pipeline M I) where
  P_raw : I.raw → Prop
  Q_encoded : I.encoded → Prop
  Q_indexed : I.indexed → Prop
  Q_selected : I.selected → Prop
  Q_ranked : I.ranked → Prop
  h_perceive : Triple P_raw p.perceive Q_encoded
  h_cache : Triple Q_encoded p.cache Q_indexed
  h_filter : Triple Q_indexed p.filter Q_selected
  h_attend : ∀ pol : I.policy, Triple Q_selected (p.attend pol) Q_ranked

Multi-stage composition lemmas

Convenience wrappers around triple_comp: two_stage_comp, three_stage_comp, four_stage_comp. Each chains one more stage through the COMP rule. Generic — not specific to pipeline stages.

forward_triple

The forward pipeline satisfies {P_raw} forward {Q_ranked} when each individual stage satisfies its triple. Applies four_stage_comp to the pipeline's specific stages.

theorem forward_triple [Monad M] [LawfulMonad M] [Support M]
    {I : InterfaceTypes} {p : Pipeline M I}
    (t : PipelineTriples M I p) (policy : I.policy)
    : Triple t.P_raw (p.forwardKernel policy) t.Q_ranked :=
  four_stage_comp t.h_perceive t.h_cache t.h_filter (t.h_attend policy)

forward_triple'

Corollary connecting the abstract kernel composition to the concrete Pipeline.forward function. Shows that the actual forward pass (defined with explicit binds) satisfies the triple proved for the Kleisli composition.

Connections

• Hoare/Bridge.lean — imported; provides the bridge between contracts and triples
• Hoare/Core.lean — triple_comp is the workhorse
• Pipeline.lean — the Pipeline structure whose forward pass is proved correct
• Handshake.lean — the handshake conditions that enable composition