Add minimal LinCCAL-style case study

.gitignore

@@ -1,5 +1,6 @@
 Makefile
 Makefile.conf
+ResearchOptions.md
 .coqdeps.d
 .lia.cache
 *.vo
@@ -15,4 +16,4 @@ Makefile.conf
 *.snm
 *.toc
 *.vrb
-*~
+*~

RBGS.v

@@ -0,0 +1,8 @@
+(** Convenience re-exports for the refinement-based game semantics
+    development so examples can depend on a single module name. *)
+
+Require Export models.IntStrat.
+Require Export models.EffectSignatures.
+Require Export models.IntSpec.
+Require Export models.LinCCAL.
+

_CoqProject

@@ -28,7 +28,15 @@ models/Coherence.v
 models/DCPO.v
 models/IntStrat.v
 models/LinCCAL.v
+models/Pi/Syntax.v
+models/Pi/Semantics.v
+RBGS.v
 examples/CAL.v
+examples/LinCCALFlip.v
+examples/PiCalculus.v
+examples/KappaCalc.v
+examples/PFPLParallel.v
+examples/PiRBGS.v
 interfaces/Category.v
 interfaces/Functor.v
 interfaces/MonoidalCategory.v

examples/KappaCalc.v

@@ -0,0 +1,43 @@
+Require Import Coq.Lists.List.
+Import ListNotations.
+
+(** A small typed kappa-calculus skeleton (first-order internal language)
+    using de Bruijn variables for ground constants. *)
+
+Module Kappa.
+
+  (** Types: unit and binary products only. *)
+  Inductive kty :=
+  | kunit
+  | kprod (A B : kty).
+
+  Notation "A × B" := (kprod A B) (at level 40).
+
+  (** Variables for ground constants of type [1 -> A]. *)
+  Inductive var : list kty -> kty -> Type :=
+  | vz A Γ : var (A :: Γ) A
+  | vs A B Γ : var Γ A -> var (B :: Γ) A.
+
+  (** Terms are morphisms [A -> B] with constants in [Γ]. *)
+  Inductive term : list kty -> kty -> kty -> Type :=
+  | tid Γ A : term Γ A A
+  | tbang Γ A : term Γ A kunit
+  | tcomp Γ A B C : term Γ A B -> term Γ B C -> term Γ A C
+  | tlift Γ A B : term Γ kunit A -> term Γ B (A × B)
+  | tvar Γ A : var Γ A -> term Γ kunit A
+  | tkappa Γ A B C : term (A :: Γ) B C -> term Γ (A × B) C.
+
+  Arguments tid {Γ A}.
+  Arguments tbang {Γ A}.
+  Arguments tcomp {Γ A B C} _ _.
+  Arguments tlift {Γ A B} _.
+  Arguments tvar {Γ A} _.
+  Arguments tkappa {Γ A B C} _.
+
+  Notation "f ∘ g" := (tcomp g f) (at level 40, left associativity).
+
+  (** Example: drop the unit component from a pair. *)
+  Definition drop_unit {Γ A} : term Γ (A × kunit) A :=
+    tkappa (tvar (vz A Γ)).
+
+End Kappa.

examples/LinCCALFlip.v

@@ -0,0 +1,183 @@
+Require Import Coq.Program.Equality.
+Require Import Classical.
+Require Import models.EffectSignatures.
+Require Import models.LinCCAL.
+
+(* A small LinCCAL case study: an atomic boolean flip protected by a lock and
+   register, built using existing components from LinCCALExample. *)
+Module LinCCALFlip.
+  Import LinCCAL.
+  Import LinCCALExample.
+  Module Sig := EffectSignatures.Sig.
+  Import (coercions, canonicals, notations) Sig.
+  Import (canonicals) Sig.Plus.
+  Import (notations) LinCCAL.
+  Open Scope term_scope.
+
+  Variant Eflip_op :=
+    | flip.
+
+  Canonical Structure Eflip :=
+    {|
+      Sig.op := Eflip_op;
+      Sig.ar _ := bool;
+    |}.
+
+  Definition Σflip : LinCCAL.Spec.lts Eflip bool :=
+    fun b _ 'flip => LinCCAL.Spec.ret (m:=flip) b (negb b).
+
+  Definition Lflip : LinCCAL.t :=
+    {| LinCCAL.li_spec := LinCCAL.Spec.gen Σflip false |}.
+
+  Definition flip_impl :
+    Sig.term (LinCCAL.li_sig (LinCCALExample.Llock * LinCCALExample.Lreg false)%obj) bool :=
+    inl LinCCALExample.acq >= _ =>
+    inr LinCCALExample.get >= b =>
+    inr (LinCCALExample.set (negb b)) >= _ =>
+    inl LinCCALExample.rel >= _ =>
+    Sig.var b.
+
+  Variant flip_threadstate (i : LinCCAL.tid) h :
+    bool -> option (LinCCAL.threadstate _ _) -> Prop :=
+    | flip_rdy b :
+      h <> Some i ->
+      flip_threadstate i h b None
+    | flip_acq b :
+      h <> Some i ->
+      flip_threadstate i h b (Some (LinCCAL.mkts flip flip_impl None))
+    | flip_get b :
+      h = Some i ->
+      flip_threadstate i h b
+        (Some (LinCCAL.mkts flip (inr LinCCALExample.get >= b =>
+                                     inr (LinCCALExample.set (negb b)) >= _ =>
+                                     inl LinCCALExample.rel >= _ =>
+                                     Sig.var b) None))
+    | flip_set b :
+      h = Some i ->
+      flip_threadstate i h b
+        (Some (LinCCAL.mkts flip (inr (LinCCALExample.set (negb b)) >= _ =>
+                                     inl LinCCALExample.rel >= _ =>
+                                     Sig.var b) None))
+    | flip_rel b :
+      h = Some i ->
+      flip_threadstate i h (negb b)
+        (Some (LinCCAL.mkts flip (inl LinCCALExample.rel >= _ =>
+                                     Sig.var b) (Some b)))
+    | flip_ret b b' :
+      h <> Some i ->
+      flip_threadstate i h b'
+        (Some (LinCCAL.mkts flip (Sig.var b) (Some b))).
+
+  Variant flip_state : _ -> Prop :=
+    flip_state_intro h b s :
+      (forall i, flip_threadstate i h b (LinCCAL.TMap.find i s)) ->
+      flip_state (LinCCAL.mkst (LinCCAL.Spec.gen Σflip b)
+                               s
+                               (LinCCAL.Spec.gen Σlock h *
+                                LinCCAL.Spec.gen (Σreg _) b)).
+
+  Lemma flip_threadstate_convert i h h' b b' s :
+    flip_threadstate i h b s ->
+    h <> Some i ->
+    h' <> Some i ->
+    flip_threadstate i h' b' s.
+  Proof.
+    destruct 1; intros; try congruence; constructor; auto.
+  Qed.
+
+  Program Definition Mflip :
+    LinCCAL.m (LinCCALExample.Llock * LinCCALExample.Lreg false) Lflip :=
+    {| LinCCAL.li_impl 'flip := flip_impl |}.
+  Next Obligation.
+    eapply LinCCAL.correctness_invariant_sound with (P := flip_state).
+    - split.
+      + intros _ [h b s Hs] _ i q r R Hsi. cbn in *.
+        specialize (Hs i).
+        dependent destruction Hs; unfold flip_impl in *; try congruence.
+        rewrite Hsi in x. dependent destruction x. reflexivity.
+      + intros _ [h b s Hs] _ i q m k R Hsi. cbn in Hsi |- *.
+        specialize (Hs i). cbn in Hs. rewrite Hsi in Hs.
+        dependent destruction Hs; cbn; try congruence.
+        * destruct h; cbn; try congruence.
+          destruct LinCCAL.TMap.E.eq_dec; congruence.
+        * destruct LinCCAL.TMap.E.eq_dec; congruence.
+      + intros _ [h b s Hs] _ [t Ht]. cbn in *.
+        destruct h as [i | ].
+        * exists i; cbn. specialize (Hs i). clear Ht.
+          dependent destruction Hs;
+            rewrite <- x; cbn;
+            try destruct LinCCAL.TMap.E.eq_dec;
+            try congruence; eauto.
+        * exists t; cbn. specialize (Hs t).
+          destruct LinCCAL.TMap.find as [st | ]; try tauto.
+          dependent destruction Hs; cbn; eauto.
+      + intros _ [h b s Hs] _ s' Hs'.
+        dependent destruction Hs'.
+        * destruct q.
+          pose proof (Hs t0) as Hst. rewrite H in Hst. dependent destruction Hst.
+          apply LinCCAL.reachable_base. constructor.
+          intro i. destruct (classic (i = t0)); subst.
+          -- rewrite LinCCAL.TMap.gss. constructor; auto.
+          -- rewrite LinCCAL.TMap.gso; auto.
+        * destruct q.
+          pose proof (Hs t0) as Hst. dependent destruction Hst; try congruence.
+          -- rewrite H in x. dependent destruction x.
+             cbn in H0.
+             destruct h; try discriminate. cbn in H0.
+             destruct LinCCAL.TMap.E.eq_dec; try discriminate.
+             cbn in H0. dependent destruction H0.
+             apply LinCCAL.reachable_base. constructor.
+             intros i. destruct (classic (i = t0)); subst.
+             ++ rewrite LinCCAL.TMap.gss. constructor. auto.
+             ++ rewrite LinCCAL.TMap.gso; auto.
+                eapply flip_threadstate_convert; eauto; congruence.
+          -- rewrite H in x. dependent destruction x.
+             apply LinCCAL.reachable_base. constructor.
+             intros i. destruct (classic (i = t0)); subst.
+             ++ rewrite LinCCAL.TMap.gss. constructor. auto.
+             ++ rewrite LinCCAL.TMap.gso; auto.
+          -- rewrite H in x. dependent destruction x.
+             eapply LinCCAL.reachable_step.
+             2: {
+               eapply (LinCCAL.lcommit t0 flip b); eauto.
+               ** rewrite LinCCAL.TMap.gss. reflexivity.
+               ** cbn. reflexivity.
+             }
+             apply LinCCAL.reachable_base. constructor.
+             intros i. destruct (classic (i = t0)); subst.
+             ++ rewrite LinCCAL.TMap.gss. constructor. auto.
+             ++ rewrite !LinCCAL.TMap.gso; auto.
+                eapply flip_threadstate_convert; eauto; congruence.
+          -- rewrite H in x. dependent destruction x.
+             cbn in H0.
+             destruct LinCCAL.TMap.E.eq_dec; cbn in H0; try congruence.
+             dependent destruction H0.
+             apply LinCCAL.reachable_base. constructor.
+             intros i. destruct (classic (i = t0)); subst.
+             ++ rewrite LinCCAL.TMap.gss. constructor. congruence.
+             ++ rewrite !LinCCAL.TMap.gso; auto.
+                eapply flip_threadstate_convert; eauto; congruence.
+        * destruct q.
+          pose proof (Hs t0) as Hst. rewrite H in Hst. dependent destruction Hst.
+          apply LinCCAL.reachable_base. constructor.
+          intro i. destruct (classic (i = t0)); subst.
+          -- rewrite LinCCAL.TMap.grs. constructor; auto.
+          -- rewrite LinCCAL.TMap.gro; auto.
+    - constructor.
+      intro i.
+      rewrite LinCCAL.TMap.gempty.
+      constructor.
+      congruence.
+  Qed.
+
+  Lemma flip_state_init :
+    flip_state
+      (LinCCAL.mkst (LinCCAL.Spec.gen Σflip false)
+                    (LinCCAL.TMap.empty _)
+                    (LinCCAL.Spec.gen Σlock None *
+                     LinCCAL.Spec.gen (Σreg _) false)).
+  Proof.
+    constructor. intros i. rewrite LinCCAL.TMap.gempty. constructor; congruence.
+  Qed.
+
+End LinCCALFlip.

examples/PFPLParallel.v

@@ -0,0 +1,65 @@
+Require Import Coq.Arith.PeanoNat.
+Require Import models.EffectSignatures.
+Require Import models.IntStrat.
+
+(** A light PFPL-inspired parallel fragment expressed with the
+    polynomial signature machinery. *)
+
+Module PFPLParallel.
+  Module Sig := EffectSignatures.Sig.
+  Import (coercions, canonicals) Sig.
+  Open Scope term_scope.
+
+  Variant par_op :=
+  | op_tick
+  | op_fork
+  | op_join.
+
+  Canonical Structure ParSig :=
+    {|
+      Sig.op := par_op;
+      Sig.ar _ := unit;
+    |}.
+
+  Definition par_term (X : Type) := Sig.term ParSig X.
+
+  Definition tick {X} (k : unit -> par_term X) : par_term X :=
+    Sig.cons op_tick k.
+
+  Definition fork {X} (k : unit -> par_term X) : par_term X :=
+    Sig.cons op_fork k.
+
+  Definition join {X} (k : unit -> par_term X) : par_term X :=
+    Sig.cons op_join k.
+
+  Fixpoint op_count {X} (t : par_term X) : nat :=
+    match t with
+    | Sig.var _ => 0
+    | Sig.cons _ k => S (op_count (k tt))
+    end.
+
+  Definition two_ticks : par_term nat :=
+    tick (fun _ => tick (fun _ => Sig.var 0)).
+
+  Lemma two_ticks_count : op_count two_ticks = 2.
+  Proof. reflexivity. Qed.
+
+  Definition fork_join : par_term nat :=
+    fork (fun _ => join (fun _ => Sig.var 0)).
+
+  Lemma fork_join_count : op_count fork_join = 2.
+  Proof. reflexivity. Qed.
+
+  (** Interaction-structure view of the same signature. *)
+  Module IS := IntStrat.
+
+  Definition Par_esig : IS.esig :=
+    {|
+      IS.op := par_op;
+      IS.ar _ := unit;
+    |}.
+
+  Definition par_app (o : par_op) : IS.application Par_esig unit :=
+    IS.econs (E:=Par_esig) o (fun _ => tt).
+
+End PFPLParallel.