shttpd/coq/S/Lucid/Sequential.v

(* Copyright © 2019 Ariadne Devos
   SPDX-License-Identifier: GPL-2.0 or GPL-3.0 *)

Require Import S.Lucid.Arrow.
Require Import Coq.Sets.Ensembles.

Section definitions.

Variable World : Type.

Variable A B C : Type.

(* The signature of the sequential composition of two arrows.
   (This only gives the properties of such a composition,
   the resulting pre-condition may be impossible.)

   TODO: whether this is correct, will be verified if
   some Arrow type is lowered to some concurrent Monad (or
   C, or ... assembly) and a bisimulation is proven to
   be maintained *)
Definition seq_sig (stop : ArrowSig World A B) (start : ArrowSig World B C) : ArrowSig World A C
  := {| rely := fun p w => rely stop p w /\ forall q, post stop p q -> rely start q w;
        (* guaranteed-p? Both arrows must keep up with the promise.
           (Remember, the frame condition specifies instants in time)

           `guarantee stop p w`: first arrow.
           `forall q, post stop p q -> _`: like the first arrow,
             except that the intermediate value must be introduced.
             Since we are speaking of *guarantees*, it must hold for
             all *posssible* (hence post stop p q) intermediates. *)
        guarantee := fun (p : Situation A) w => guarantee stop p w
          /\ forall (q : Situation B), post stop p q -> guarantee start q w;
        (* In the original formulation,
             { P } S1 { Q }, { Q } S2 { R }
             |- { P } S1 S2 { R }.
           In ours,
             { P } S1 { Q }, { R } S2 { S }
             |- { P /\ Q -> R } S1 { S }
             (except for the qualifiers and binders)
           (Is this weakest precondition?) *)
        pre := fun (p : Situation A) => pre stop p /\ (forall (q : Situation B), post stop p q -> pre start q);
        (* The post-condition is given as a set of possibilities dependent on the input.
           Possible -> exists.
           This is an ordinary Hoare composition rule. *)
        post := fun (p : Situation A) (r : Situation C) =>
         exists (q : Situation B), post stop p q /\ post start q r;
      |}.

End definitions.

Arguments seq_sig { _ _ _ _ } _ _.