Compositional proof rules for stateful clients

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

Main definitions

• Spec.Hoare: an admissible terminating mathematical client with a postcondition.

Main results

• Spec.Hoare.pure, Spec.Hoare.call, Spec.Hoare.bind: compositional verification rules.
• Spec.Hoare.realize: a semantic client proof transports through any realization.

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

A semantic contract includes admissibility of the selected history and the postcondition.

theorem Cslib.Stateful.Spec.Hoare.pure {D : Spec} {α : 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.Stateful.Spec.Hoare.call {D : Spec} (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.step s o).2 (D.step s o).1) : Hoare pre (PFunctor.FreeM.liftBind o fun (a : D.signature.B o) => PFunctor.FreeM.pure a) post

Calling an operation requires its precondition and exposes its mathematical result.

theorem Cslib.Stateful.Spec.Hoare.bind {D : Spec} {α β : 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.Stateful.Spec.Hoare.consequence {D : Spec} {α : 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.Stateful.Spec.Hoare.realize {D : Spec} {α : Type y} {C Trace : Type x} {exec : Execution D C Trace} (R : Realization 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.Stateful.Spec.Hoare.link {D : Spec} {α : Type w} {E : Spec} (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) (Stateful.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.