Program core

inductive Prog (C : Type) (R : C → Type) (A : Type) : Type where
  | ret : A → Prog C R A
  | call : (c : C) → (R c → Prog C R A) → Prog C R A

structure Contract (C : Type) (R : C → Type) (S : Type) where
  pre : S → C → Prop
  next : (s : S) → (c : C) → R c → S
  post : S → (c : C) → R c → Prop

structure Impl (C : Type) (R : C → Type) (M : Type) where
  step : M → (c : C) → R c × M

def Safe {C : Type} {R : C → Type} {S A : Type}
    (K : Contract C R S) (Q : S → A → Prop) : Prog C R A → S → Prop :=
  Prog.rec (fun a s => Q s a)
    (fun c _ ih s => K.pre s c ∧ ∀ r, K.post s c r → ih r (K.next s c r))

def Implements {C : Type} {R : C → Type} {S M : Type}
    (K : Contract C R S) (h : Impl C R M) (Inv : S → M → Prop) : Prop :=
  ∀ s m c, Inv s m → K.pre s c →
    K.post s c (h.step m c).1 ∧ Inv (K.next s c (h.step m c).1) (h.step m c).2

def Simulates {C : Type} {R : C → Type} {S M N : Type}
    (K : Contract C R S) (first : Impl C R M) (second : Impl C R N)
    (Rel : S → M → N → Prop) : Prop :=
  ∀ s m n c, Rel s m n → K.pre s c →
    ∃ r m' n', first.step m c = (r, m') ∧ second.step n c = (r, n') ∧
      K.post s c r ∧ Rel (K.next s c r) m' n'

def bind {C : Type} {R : C → Type} {A B : Type}
    (p : Prog C R A) (f : A → Prog C R B) : Prog C R B :=
  match p with
  | .ret a => f a
  | .call c k => Prog.call c (fun r => bind (k r) f)

def interp {C D : Type} {R : C → Type} {E : D → Type} {A : Type}
    (module : (d : D) → Prog C R (E d)) (p : Prog D E A) : Prog C R A :=
  match p with
  | .ret a => Prog.ret a
  | .call d k => bind (module d) (fun r => interp module (k r))

def run {C : Type} {R : C → Type} {M A : Type}
    (h : Impl C R M) (p : Prog C R A) : M → A × M :=
  match p with
  | .ret a => fun m => (a, m)
  | .call c k => fun m => let answer := h.step m c
                         run h (k answer.1) answer.2

def trace {C : Type} {R : C → Type} {M A : Type}
    (h : Impl C R M) (p : Prog C R A) : M → List (Sigma R) :=
  match p with
  | .ret _ => fun _ => []
  | .call c k => fun m => let answer := h.step m c
                         Sigma.mk c answer.1 :: trace h (k answer.1) answer.2

def after {C : Type} {R : C → Type} {S : Type}
    (K : Contract C R S) (s : S) : List (Sigma R) → S
  | [] => s
  | event :: rest => after K (K.next s event.1 event.2) rest

def Allowed {C : Type} {R : C → Type} {S : Type}
    (K : Contract C R S) (s : S) : List (Sigma R) → Prop
  | [] => True
  | event :: rest => K.pre s event.1 ∧ K.post s event.1 event.2 ∧
      Allowed K (K.next s event.1 event.2) rest

def unpromised {C : Type} {R : C → Type} {S : Type}
    (pre : S → C → Prop) (next : (s : S) → (c : C) → R c → S) : Contract C R S :=
  ⟨pre, next, fun _ _ _ => True⟩

theorem sound {C : Type} {R : C → Type} {S M A : Type}
    (K : Contract C R S) (h : Impl C R M) (Inv : S → M → Prop)
    (law : Implements K h Inv) (Q : S → A → Prop) (p : Prog C R A) :
    ∀ s m, Safe K Q p s → Inv s m →
      Allowed K s (trace h p m) ∧
      Inv (after K s (trace h p m)) (run h p m).2 ∧
      Q (after K s (trace h p m)) (run h p m).1

theorem replacement {C : Type} {R : C → Type} {S M N A : Type}
    (K : Contract C R S) (first : Impl C R M) (second : Impl C R N)
    (Rel : S → M → N → Prop) (law : Simulates K first second Rel)
    (Q : S → A → Prop) (p : Prog C R A) :
    ∀ s m n, Safe K Q p s → Rel s m n →
      (run first p m).1 = (run second p n).1 ∧
      trace first p m = trace second p n ∧
      Rel (after K s (trace first p m)) (run first p m).2 (run second p n).2

theorem safe_bind {C : Type} {R : C → Type} {S A B : Type}
    (K : Contract C R S) (Q : S → B → Prop)
    (p : Prog C R A) (f : A → Prog C R B) :
    ∀ s, Safe K Q (bind p f) s ↔
      Safe K (fun t a => Safe K Q (f a) t) p s

theorem safe_interp {C D : Type} {R : C → Type} {E : D → Type}
    {S T A : Type} (K : Contract C R S) (G : Contract D E T)
    (Rel : T → S → Prop) (module : (d : D) → Prog C R (E d))
    (law : ∀ t s d, Rel t s → G.pre t d →
      Safe K (fun s' r => G.post t d r ∧ Rel (G.next t d r) s') (module d) s)
    (Q : T → A → Prop) (p : Prog D E A) :
    ∀ t s, Safe G Q p t → Rel t s →
      Safe K (fun s' a => ∃ t', Rel t' s' ∧ Q t' a) (interp module p) s

theorem safe_mono {C : Type} {R : C → Type} {S A : Type}
    (K : Contract C R S) (P Q : S → A → Prop)
    (implies : ∀ s a, P s a → Q s a) (p : Prog C R A) :
    ∀ s, Safe K P p s → Safe K Q p s

theorem run_bind {C : Type} {R : C → Type} {M A B : Type}
    (h : Impl C R M) (p : Prog C R A) (f : A → Prog C R B) :
    ∀ m, run h (bind p f) m = run h (f (run h p m).1) (run h p m).2

theorem trace_bind {C : Type} {R : C → Type} {M A B : Type}
    (h : Impl C R M) (p : Prog C R A) (f : A → Prog C R B) :
    ∀ m, trace h (bind p f) m =
      trace h p m ++ trace h (f (run h p m).1) (run h p m).2

theorem safe_unpromised {C : Type} {R : C → Type} {S A : Type}
    (pre : S → C → Prop) (next : (s : S) → (c : C) → R c → S)
    (Q : S → A → Prop) (c : C) (k : R c → Prog C R A) (s : S) :
    Safe (unpromised pre next) Q (Prog.call c k) s ↔
      pre s c ∧ ∀ r, Safe (unpromised pre next) Q (k r) (next s c r)

def Replaces {C : Type} {R : C → Type} {S M N : Type} (s0 : S) (m0 : M) (n0 : N)
    (K : Received.Contract C R S) (first : Received.Impl C R M) (second : Received.Impl C R N)
    (Rel : S → M → N → Prop) : Prop :=
  Rel s0 m0 n0 ∧ Received.Simulates K first second Rel

def Refines {C : Type} {R : C → Type} {S T : Type}
    (new : Received.Contract C R T) (old : Received.Contract C R S) (Rel : S → T → Prop) : Prop :=
  (∀ s, ∃ t, Rel s t) ∧
  ∀ s t c, Rel s t → Received.pre old s c →
    Received.pre new t c ∧ ∀ r, Received.post new t c r →
      Received.post old s c r ∧ Rel (Received.next old s c r) (Received.next new t c r)

def Transported {S T A : Type} (Rel : S → T → Prop) (Q : S → A → Prop) (t : T) (a : A) : Prop :=
  ∃ s, Rel s t ∧ Q s a