Compositional proof rules for stateful clients

These semantic Hoare rules generate demonic admissibility and postcondition obligations for pure results, calls, sequential composition and consequence. They apply before choosing a backend; implementation transports their results to native execution. Resource obligations are separate.

Main definitions

• StateTransitionSpec.Hoare: demonic Hoare triple asserting D.DemonicValid s p and post v s' for every valid D.ClientRun s p v s' tr.

Main results

• StateTransitionSpec.Hoare.pure, StateTransitionSpec.Hoare.call, StateTransitionSpec.Hoare.call_ofFn, StateTransitionSpec.Hoare.bind, StateTransitionSpec.Hoare.consequence: compositional verification rules.
• StateTransitionSpec.hoare_iff_ofFn: equivalence with the functional runClient formulation on deterministic specifications ([D.HasStepFn f]).
• StateTransitionSpec.Hoare.realize: a semantic client proof transports through any implementation.
• StateTransitionSpec.Hoare.link: transport a semantic client contract across an interface implementation.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapter 17.

def Cslib.DataStructure.StateTransitionSpec.Hoare {D : StateTransitionSpec} {α : Type y} (pre : D.State → Prop) (p : D.Client α) (post : α → D.State → Prop) : Prop

Demonic Hoare triple: from any state satisfying pre s, the client p is demonically admissible (D.DemonicValid s p) and every valid ClientRun establishes post v s'.

theorem Cslib.DataStructure.StateTransitionSpec.hoare_iff_ofFn {D : StateTransitionSpec} {α : Type y} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (pre : D.State → Prop) (p : D.Client α) (post : α → D.State → Prop) : Hoare pre p post ↔ ∀ (s : D.State), pre s → D.ValidHistory s (D.clientHistory s p) ∧ post (D.clientResult s p) (D.clientState s p)

On a deterministic specification ([D.HasStepFn f]), D.Hoare is equivalent to D.ValidHistory s (D.clientHistory s p) ∧ post (D.clientResult s p) (D.clientState s p).

theorem Cslib.DataStructure.StateTransitionSpec.Hoare.pure {D : StateTransitionSpec} {α : Type y} (pre : D.State → Prop) (a : α) (post : α → D.State → Prop) (h : ∀ (s : D.State), pre s → post a s) : Hoare pre (PFunctor.FreeM.pure a) post

Returning a value leaves the represented state unchanged.

theorem Cslib.DataStructure.StateTransitionSpec.Hoare.call {D : StateTransitionSpec} (pre : D.State → Prop) (o : D.Op) (post : D.Result o → D.State → Prop) (h : ∀ (s : D.State), pre s → D.valid s o ∧ ∀ (s' : D.State) (a : D.Result o), D.step s o s' a → post a s') : Hoare pre (PFunctor.FreeM.liftBind o fun (a : D.signature.B o) => PFunctor.FreeM.pure a) post

Calling an operation requires D.valid s o and establishes post a s' for every permitted outcome D.step s o s' a.

theorem Cslib.DataStructure.StateTransitionSpec.Hoare.call_ofFn {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (pre : D.State → Prop) (o : D.Op) (post : D.Result o → D.State → Prop) (h : ∀ (s : D.State), pre s → D.valid s o ∧ post (D.stepFn s o).2 (D.stepFn s o).1) : Hoare pre (PFunctor.FreeM.liftBind o fun (a : D.signature.B o) => PFunctor.FreeM.pure a) post

On a deterministic specification ([D.HasStepFn f]), calling an operation requires its precondition and exposes (D.stepFn s o).

theorem Cslib.DataStructure.StateTransitionSpec.Hoare.bind {D : StateTransitionSpec} {α β : Type y} {pre : D.State → Prop} {mid : α → D.State → Prop} {post : β → D.State → Prop} {p : D.Client α} {k : α → D.Client β} (hp : Hoare pre p mid) (hk : ∀ (a : α), Hoare (mid a) (k a) post) : Hoare pre (PFunctor.FreeM.bind p k) post

Sequencing exposes only the intermediate abstract postcondition to its continuation.

theorem Cslib.DataStructure.StateTransitionSpec.Hoare.consequence {D : StateTransitionSpec} {α : Type y} {pre pre' : D.State → Prop} {post post' : α → D.State → Prop} {p : D.Client α} (h : Hoare pre p post) (hp : ∀ (s : D.State), pre' s → pre s) (hq : ∀ (a : α) (s : D.State), post a s → post' a s) : Hoare pre' p post'

Strengthen preconditions and weaken postconditions without reopening a client proof.

theorem Cslib.DataStructure.StateTransitionSpec.Hoare.realize {D : StateTransitionSpec} {α : Type y} {C Trace : Type x} {exec : Execution D.signature C Trace} (R : StateTransitionImpl D exec) {pre : D.State → Prop} {post : α → D.State → Prop} {p : D.Client α} (h : Hoare pre p post) {s : D.State} {c c' : C} {a : α} {traces : List Trace} (hp : pre s) (hr : R.rep s c) (he : Executes exec p c a c' traces) : ∃ (s' : D.State), R.rep s' c' ∧ post a s'

Every native execution of a verified client satisfies its abstract postcondition.

theorem Cslib.DataStructure.StateTransitionSpec.Hoare.link {D : StateTransitionSpec} {α : Type w} {E : StateTransitionSpec} (M : Module D E) {pre : D.State → Prop} {post : α → D.State → Prop} {p : D.Client α} (h : Hoare pre p post) : Hoare (fun (e : E.State) => ∃ (s : D.State), pre s ∧ M.rep s e) (DataStructure.link M.methods p) fun (a : α) (e : E.State) => ∃ (s : D.State), post a s ∧ M.rep s e

Linking preserves a client contract while existentially hiding the module representation.