From 052643168a775ea543a649a0fcb901a95ce99735 Mon Sep 17 00:00:00 2001 From: "R. Philip Stetson IV" Date: Mon, 15 Dec 2025 13:15:20 -0500 Subject: [PATCH 1/3] Add minimal LinCCAL-style case study --- _CoqProject | 1 + examples/LinCCALFlip.v | 173 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 174 insertions(+) create mode 100644 examples/LinCCALFlip.v diff --git a/_CoqProject b/_CoqProject index 971795e..4f9801c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -29,6 +29,7 @@ models/DCPO.v models/IntStrat.v models/LinCCAL.v examples/CAL.v +examples/LinCCALFlip.v interfaces/Category.v interfaces/Functor.v interfaces/MonoidalCategory.v diff --git a/examples/LinCCALFlip.v b/examples/LinCCALFlip.v new file mode 100644 index 0000000..f2a9e64 --- /dev/null +++ b/examples/LinCCALFlip.v @@ -0,0 +1,173 @@ +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. + +End LinCCALFlip. From 2f20b55bcc5b3f876b1d7ada57f436ba8aad7e53 Mon Sep 17 00:00:00 2001 From: "R. Philip Stetson IV" Date: Tue, 16 Dec 2025 12:16:58 -0500 Subject: [PATCH 2/3] Add kappa/PFPL stepping stones and Pi RBGS bridge --- .gitignore | 3 +- _CoqProject | 4 + examples/KappaCalc.v | 43 ++++++++ examples/LinCCALFlip.v | 10 ++ examples/PFPLParallel.v | 65 ++++++++++++ examples/PiCalculus.v | 223 ++++++++++++++++++++++++++++++++++++++++ examples/PiRBGS.v | 62 +++++++++++ 7 files changed, 409 insertions(+), 1 deletion(-) create mode 100644 examples/KappaCalc.v create mode 100644 examples/PFPLParallel.v create mode 100644 examples/PiCalculus.v create mode 100644 examples/PiRBGS.v diff --git a/.gitignore b/.gitignore index 59bf8e0..1b98e37 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ Makefile Makefile.conf +ResearchOptions.md .coqdeps.d .lia.cache *.vo @@ -15,4 +16,4 @@ Makefile.conf *.snm *.toc *.vrb -*~ +*~ \ No newline at end of file diff --git a/_CoqProject b/_CoqProject index 4f9801c..e03d4d7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -30,6 +30,10 @@ models/IntStrat.v models/LinCCAL.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 diff --git a/examples/KappaCalc.v b/examples/KappaCalc.v new file mode 100644 index 0000000..9251182 --- /dev/null +++ b/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. diff --git a/examples/LinCCALFlip.v b/examples/LinCCALFlip.v index f2a9e64..b83dfa5 100644 --- a/examples/LinCCALFlip.v +++ b/examples/LinCCALFlip.v @@ -170,4 +170,14 @@ Module LinCCALFlip. 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. diff --git a/examples/PFPLParallel.v b/examples/PFPLParallel.v new file mode 100644 index 0000000..66e8d94 --- /dev/null +++ b/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. diff --git a/examples/PiCalculus.v b/examples/PiCalculus.v new file mode 100644 index 0000000..2844ad2 --- /dev/null +++ b/examples/PiCalculus.v @@ -0,0 +1,223 @@ +(** A minimal formalization of the π-calculus using the existing + infrastructure. We keep to a lightweight labelled transition + semantics and package it so it can be reused as an LTS. *) + +Require Import Coq.Arith.PeanoNat. +Require Import Coq.Bool.Bool. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Relations.Relation_Operators. + +Module Pi. + + (** * Names and actions *) + + Definition name := nat. + + Inductive action := + | tau + | in_act (c : name) (v : name) + | out_act (c : name) (v : name). + + Definition action_uses (x : name) (a : action) : bool := + match a with + | tau => false + | in_act c v => (x =? c) || (x =? v) + | out_act c v => (x =? c) || (x =? v) + end. + + (** * Syntax *) + + Inductive proc := + | zero + | tau_prefix (p : proc) + | send (c v : name) (p : proc) + | recv (c x : name) (p : proc) (* input binds [x] in [p] *) + | par (p q : proc) + | choice (p q : proc) + | nu (x : name) (p : proc) (* restriction of [x] in [p] *) + | rep (p : proc). + + (** Capture-avoiding substitution of channel [x] by [y]. *) + Fixpoint subst (x y : name) (p : proc) : proc := + match p with + | zero => zero + | tau_prefix p1 => tau_prefix (subst x y p1) + | send c v p1 => + send (if c =? x then y else c) (if v =? x then y else v) (subst x y p1) + | recv c x' p1 => + let c' := if c =? x then y else c in + if x' =? x then recv c' x' p1 else recv c' x' (subst x y p1) + | par p1 p2 => par (subst x y p1) (subst x y p2) + | choice p1 p2 => choice (subst x y p1) (subst x y p2) + | nu x' p1 => if x' =? x then nu x' p1 else nu x' (subst x y p1) + | rep p1 => rep (subst x y p1) + end. + + (** Free-name test used for α-conversion side-conditions. *) + Fixpoint occurs (x : name) (p : proc) : bool := + match p with + | zero => false + | tau_prefix p1 => occurs x p1 + | send c v p1 => (x =? c) || (x =? v) || occurs x p1 + | recv c x' p1 => (x =? c) || if x' =? x then false else occurs x p1 + | par p1 p2 => occurs x p1 || occurs x p2 + | choice p1 p2 => occurs x p1 || occurs x p2 + | nu x' p1 => if x' =? x then false else occurs x p1 + | rep p1 => occurs x p1 + end. + + (** * Structural congruence *) + + Inductive cong : proc -> proc -> Prop := + | cong_refl p : cong p p + | cong_sym p q : cong p q -> cong q p + | cong_trans p q r : cong p q -> cong q r -> cong p r + | cong_par_comm p q : cong (par p q) (par q p) + | cong_par_assoc p q r : cong (par (par p q) r) (par p (par q r)) + | cong_par_zero p : cong (par p zero) p + | cong_choice_comm p q : cong (choice p q) (choice q p) + | cong_choice_assoc p q r : cong (choice (choice p q) r) (choice p (choice q r)) + | cong_choice_zero p : cong (choice p zero) p + | cong_nu_alpha x y p : + x <> y -> + occurs y p = false -> + cong (nu x p) (nu y (subst x y p)) + | cong_rep_unfold p : cong (rep p) (par p (rep p)). + + #[export] Instance cong_equiv : Equivalence cong. + Proof. + constructor. + - intro p. apply cong_refl. + - intros x y Hxy. apply cong_sym. exact Hxy. + - intros x y z Hxy Hyz. eapply cong_trans; eauto. + Qed. + + (** * One-step transitions *) + + Inductive step : action -> proc -> proc -> Prop := + | step_tau p : + step tau (tau_prefix p) p + | step_out c v p : + step (out_act c v) (send c v p) p + | step_in c x p v : + step (in_act c v) (recv c x p) (subst x v p) + | step_choice_l a p p' q : + step a p p' -> + step a (choice p q) (choice p' q) + | step_choice_r a p q q' : + step a q q' -> + step a (choice p q) (choice p q') + | step_par_l a p p' q : + step a p p' -> + step a (par p q) (par p' q) + | step_par_r a p q q' : + step a q q' -> + step a (par p q) (par p q') + | step_comm c v p p' q q' : + step (out_act c v) p p' -> + step (in_act c v) q q' -> + step tau (par p q) (par p' q') + | step_nu a x p p' : + step a p p' -> + action_uses x a = false -> + step a (nu x p) (nu x p') + | step_rep a p p' : + step a (par p (rep p)) p' -> + step a (rep p) p'. + + Definition transition (a : action) (p q : proc) : Prop := + exists p1 p2, cong p p1 /\ step a p1 p2 /\ cong p2 q. + + Notation "p -[ a ]-> q" := (transition a p q) (at level 40). + + Lemma step_transition a p q : + step a p q -> p -[ a ]-> q. + Proof. + intro Hs. exists p, q. split; [apply cong_refl|]. + split; auto. apply cong_refl. + Qed. + + (** * Observable semantics: strong and weak bisimulations *) + + Definition is_tau (a : action) : bool := + match a with tau => true | _ => false end. + + Inductive tau_star : proc -> proc -> Prop := + | tau_refl p : tau_star p p + | tau_step p q r : + p -[ tau ]-> q -> + tau_star q r -> + tau_star p r. + + Inductive weak_step (a : action) : proc -> proc -> Prop := + | weak_step_silent p q : + tau_star p q -> + is_tau a = true -> + weak_step a p q + | weak_step_obs p p1 p2 q : + tau_star p p1 -> + is_tau a = false -> + p1 -[ a ]-> p2 -> + tau_star p2 q -> + weak_step a p q. + + Notation "p ==[ a ]=> q" := (weak_step a p q) (at level 40). + + Lemma tau_star_trans p q r : + tau_star p q -> tau_star q r -> tau_star p r. + Proof. + intros H1 H2. induction H1; eauto using tau_star. + Qed. + + Lemma weak_step_tau_closure p q : + tau_star p q -> weak_step tau p q. + Proof. + intro Htau. constructor; [exact Htau|reflexivity]. + Qed. + + Module Notations. + Notation "p || q" := (par p q) (at level 50, left associativity). + Notation "p [+] q" := (choice p q) (at level 50, left associativity). + Notation "'tau.' p" := (tau_prefix p) (at level 40). + End Notations. + + Definition handshake (c v : name) : proc := + par (send c v zero) (recv c v zero). + + Lemma handshake_tau (c v : name) : + handshake c v -[ tau ]-> par zero zero. + Proof. + unfold handshake. + apply step_transition. + eapply step_comm. + - constructor. + - cbn. replace (subst v v zero) with zero by reflexivity. constructor. + Qed. + + CoInductive bisim : proc -> proc -> Prop := + | bisim_intro p q : + (forall a p', p -[ a ]-> p' -> exists q', q -[ a ]-> q' /\ bisim p' q') -> + (forall a q', q -[ a ]-> q' -> exists p', p -[ a ]-> p' /\ bisim p' q') -> + bisim p q. + + CoInductive weak_bisim : proc -> proc -> Prop := + | weak_bisim_intro p q : + (forall a p', p ==[ a ]=> p' -> exists q', q ==[ a ]=> q' /\ weak_bisim p' q') -> + (forall a q', q ==[ a ]=> q' -> exists p', p ==[ a ]=> p' /\ weak_bisim p' q') -> + weak_bisim p q. + + CoFixpoint bisim_refl (p : proc) : bisim p p := + bisim_intro p p + (fun (a : action) (p1 : proc) (Hp : p -[ a ]-> p1) => + ex_intro _ p1 (conj Hp (bisim_refl p1))) + (fun (a : action) (p1 : proc) (Hp : p -[ a ]-> p1) => + ex_intro _ p1 (conj Hp (bisim_refl p1))). + + CoFixpoint weak_bisim_refl (p : proc) : weak_bisim p p := + weak_bisim_intro p p + (fun (a : action) (p1 : proc) (Hp : p ==[ a ]=> p1) => + ex_intro _ p1 (conj Hp (weak_bisim_refl p1))) + (fun (a : action) (p1 : proc) (Hp : p ==[ a ]=> p1) => + ex_intro _ p1 (conj Hp (weak_bisim_refl p1))). + +End Pi. diff --git a/examples/PiRBGS.v b/examples/PiRBGS.v new file mode 100644 index 0000000..f54b09c --- /dev/null +++ b/examples/PiRBGS.v @@ -0,0 +1,62 @@ +Require Import Coq.Lists.List. +Import ListNotations. +Require Import models.IntStrat. +Require Import models.EffectSignatures. +Require Import examples.PiCalculus. + +(** Bridge the lightweight π-calculus LTS to the RBGS signature/interaction + structures. We keep this as a thin wiring layer: a signature, a trace + embedding as polynomial terms, and an interaction-structure view. *) + +Module PiRBGS. + Module P := Pi. + Module Sig := EffectSignatures.Sig. + Import (coercions, canonicals) Sig. + Open Scope term_scope. + + (** Signature for observable π actions as a polynomial signature. *) + Variant pi_op := + | op_tau + | op_in (c v : P.name) + | op_out (c v : P.name). + + Canonical Structure PiSig := + {| + Sig.op := pi_op; + Sig.ar _ := unit; + |}. + + Definition op_of_action (a : P.action) : pi_op := + match a with + | P.tau => op_tau + | P.in_act c v => op_in c v + | P.out_act c v => op_out c v + end. + + (** Encode a finite trace of actions as a term over the signature. *) + Definition trace_term (tr : list P.action) : Sig.term PiSig unit := + fold_right (fun a acc => Sig.cons (op_of_action a) (fun _ => acc)) + (Sig.var tt) tr. + + (** Basic interaction-structure view using [IntStrat.esig/application]. *) + Module IS := IntStrat. + + Definition Pi_esig : IS.esig := + {| + IS.op := pi_op; + IS.ar _ := unit; + |}. + + Definition action_app (a : P.action) : IS.application Pi_esig unit := + IS.econs (E:=Pi_esig) (op_of_action a) (fun _ => tt). + + (** A simple stateful handler that records the trace as a list of [pi_op]. *) + Definition pi_state := list pi_op. + + Definition handle_action (s : pi_state) (a : P.action) : pi_state := + s ++ [op_of_action a]. + + Definition run_trace (tr : list P.action) : pi_state := + fold_left handle_action tr []. + +End PiRBGS. From a87d66cda64798c0b39aa568a03cb16602d6ca81 Mon Sep 17 00:00:00 2001 From: "R. Philip Stetson IV" Date: Thu, 18 Dec 2025 14:48:23 -0500 Subject: [PATCH 3/3] Updated --- RBGS.v | 8 ++ _CoqProject | 3 + examples/PiRBGS.v | 66 +----------- models/Pi/Semantics.v | 240 ++++++++++++++++++++++++++++++++++++++++++ models/Pi/Syntax.v | 109 +++++++++++++++++++ 5 files changed, 365 insertions(+), 61 deletions(-) create mode 100644 RBGS.v create mode 100644 models/Pi/Semantics.v create mode 100644 models/Pi/Syntax.v diff --git a/RBGS.v b/RBGS.v new file mode 100644 index 0000000..a9e9392 --- /dev/null +++ b/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. + diff --git a/_CoqProject b/_CoqProject index e03d4d7..e89b6e0 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,6 +28,9 @@ 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 diff --git a/examples/PiRBGS.v b/examples/PiRBGS.v index f54b09c..c12ecc1 100644 --- a/examples/PiRBGS.v +++ b/examples/PiRBGS.v @@ -1,62 +1,6 @@ -Require Import Coq.Lists.List. -Import ListNotations. -Require Import models.IntStrat. -Require Import models.EffectSignatures. -Require Import examples.PiCalculus. +Require Import models.Pi.Semantics. -(** Bridge the lightweight π-calculus LTS to the RBGS signature/interaction - structures. We keep this as a thin wiring layer: a signature, a trace - embedding as polynomial terms, and an interaction-structure view. *) - -Module PiRBGS. - Module P := Pi. - Module Sig := EffectSignatures.Sig. - Import (coercions, canonicals) Sig. - Open Scope term_scope. - - (** Signature for observable π actions as a polynomial signature. *) - Variant pi_op := - | op_tau - | op_in (c v : P.name) - | op_out (c v : P.name). - - Canonical Structure PiSig := - {| - Sig.op := pi_op; - Sig.ar _ := unit; - |}. - - Definition op_of_action (a : P.action) : pi_op := - match a with - | P.tau => op_tau - | P.in_act c v => op_in c v - | P.out_act c v => op_out c v - end. - - (** Encode a finite trace of actions as a term over the signature. *) - Definition trace_term (tr : list P.action) : Sig.term PiSig unit := - fold_right (fun a acc => Sig.cons (op_of_action a) (fun _ => acc)) - (Sig.var tt) tr. - - (** Basic interaction-structure view using [IntStrat.esig/application]. *) - Module IS := IntStrat. - - Definition Pi_esig : IS.esig := - {| - IS.op := pi_op; - IS.ar _ := unit; - |}. - - Definition action_app (a : P.action) : IS.application Pi_esig unit := - IS.econs (E:=Pi_esig) (op_of_action a) (fun _ => tt). - - (** A simple stateful handler that records the trace as a list of [pi_op]. *) - Definition pi_state := list pi_op. - - Definition handle_action (s : pi_state) (a : P.action) : pi_state := - s ++ [op_of_action a]. - - Definition run_trace (tr : list P.action) : pi_state := - fold_left handle_action tr []. - -End PiRBGS. +(** Compatibility shim: re-export the RBGS-flavoured π semantics from + [models/Pi/Semantics.v]. *) +Module PiRBGS := PiSemantics. +Export PiSemantics. diff --git a/models/Pi/Semantics.v b/models/Pi/Semantics.v new file mode 100644 index 0000000..1133563 --- /dev/null +++ b/models/Pi/Semantics.v @@ -0,0 +1,240 @@ +Require Import Coq.Lists.List. +Require Import Coq.Arith.PeanoNat. +Require Import Coq.Logic.FunctionalExtensionality. +Require Import RBGS. +Require Import models.Pi.Syntax. + +(** RBGS-compatible semantics for the locally-nameless π-calculus. + Behaviors are finite traces of observable actions encoded as + polynomial terms over the π signature. Refinement is inclusion of + trace sets, and parallel composition is compositional. *) + +Module PiSemantics. + Module Syn := PiSyntax. + Import Syn. + + Module Sig := EffectSignatures.Sig. + Import (coercions, canonicals) Sig. + Open Scope list_scope. + Open Scope term_scope. + + (** * Actions and small-step semantics *) + + Definition name := atom. + + Inductive action := + | tau + | in_act (c v : name) + | out_act (c v : name). + + Definition action_uses (x : name) (a : action) : bool := + match a with + | tau => false + | in_act c v => (x =? c) || (x =? v) + | out_act c v => (x =? c) || (x =? v) + end. + + (** A lightweight operational semantics that respects binding via + [open]/[close] from the locally-nameless syntax. *) + Inductive step : action -> proc -> proc -> Prop := + | step_tau p : + step tau (tau_prefix p) p + | step_out c v p : + step (out_act c v) (send (FVar c) (FVar v) p) p + | step_in c p v : + step (in_act c v) (recv (FVar c) p) (open v p) + | step_choice_l a p p' q : + step a p p' -> + step a (choice p q) (choice p' q) + | step_choice_r a p q q' : + step a q q' -> + step a (choice p q) (choice p q') + | step_par_l a p p' q : + step a p p' -> + step a (par p q) (par p' q) + | step_par_r a p q q' : + step a q q' -> + step a (par p q) (par p q') + | step_comm c v p p' q q' : + step (out_act c v) p p' -> + step (in_act c v) q q' -> + step tau (par p q) (par p' q') + | step_nu a p p' x : + step a (open x p) p' -> + action_uses x a = false -> + step a (nu p) (nu (close x p')) + | step_rep a p p' : + step a (par p (rep p)) p' -> + step a (rep p) p'. + + (** * Traces and RBGS signature view *) + + Inductive trace : proc -> list action -> Prop := + | trace_nil p : + trace p [] + | trace_cons a p q tr : + step a p q -> + trace q tr -> + trace p (a :: tr). + + Variant pi_op := + | op_tau + | op_in (c v : name) + | op_out (c v : name). + + Canonical Structure PiSig := + {| + Sig.op := pi_op; + Sig.ar _ := unit; + |}. + + Definition op_of_action (a : action) : pi_op := + match a with + | tau => op_tau + | in_act c v => op_in c v + | out_act c v => op_out c v + end. + + Definition trace_term (tr : list action) : Sig.term PiSig unit := + fold_right (fun a acc => Sig.cons (op_of_action a) (fun _ => acc)) + (Sig.var tt) tr. + + (** Interaction-structure view to plug into the RBGS refinement tower. *) + Module IS := IntStrat. + + Definition Pi_esig : IS.esig := + {| + IS.op := pi_op; + IS.ar _ := unit; + |}. + + Definition action_app (a : action) : IS.application Pi_esig unit := + IS.econs (E:=Pi_esig) (op_of_action a) (fun _ => tt). + + (** * Semantics as trace sets and refinement *) + + Definition sem_proc (p : proc) (t : Sig.term PiSig unit) : Prop := + exists tr, trace p tr /\ t = trace_term tr. + + Definition refines (p q : proc) : Prop := + forall t, sem_proc p t -> sem_proc q t. + + Lemma refines_refl p : refines p p. + Proof. firstorder. Qed. + + Lemma refines_trans p q r : + refines p q -> refines q r -> refines p r. + Proof. firstorder. Qed. + + Lemma trace_term_injective tr1 tr2 : + trace_term tr1 = trace_term tr2 -> + tr1 = tr2. + Proof. + revert tr2. induction tr1 as [|a1 tr1 IH]; intros [|a2 tr2]; cbn; intro H. + - reflexivity. + - inversion H. + - inversion H. + - injection H as _ Hk. + apply (f_equal (fun k => k tt)) in Hk. + cbn in Hk. + apply IH in Hk. + f_equal; assumption. + Qed. + + (** * Compositionality of parallel composition *) + + Inductive sync_interleave : list action -> list action -> list action -> Prop := + | sync_nil : + sync_interleave [] [] [] + | sync_left a trl trr tr : + sync_interleave trl trr tr -> + sync_interleave (a :: trl) trr (a :: tr) + | sync_right a trl trr tr : + sync_interleave trl trr tr -> + sync_interleave trl (a :: trr) (a :: tr) + | sync_comm_out_in c v trl trr tr : + sync_interleave trl trr tr -> + sync_interleave (out_act c v :: trl) (in_act c v :: trr) (tau :: tr) + | sync_comm_in_out c v trl trr tr : + sync_interleave trl trr tr -> + sync_interleave (in_act c v :: trl) (out_act c v :: trr) (tau :: tr). + + Lemma trace_par_split p q tr : + trace (par p q) tr -> + exists trp trq, + trace p trp /\ + trace q trq /\ + sync_interleave trp trq tr. + Proof. + revert p q. + induction tr as [|a tr IH]; intros p q Htr. + - inversion Htr; subst. exists [], []. repeat constructor. + - inversion Htr as [a' pq r Hstep Hrest]; subst. + inversion Hstep; subst. + + specialize (IH _ _ Hrest) as (trp & trq & Hp & Hq & Hinter). + exists (a :: trp), trq. repeat split; try constructor; auto. + constructor; auto. + + specialize (IH _ _ Hrest) as (trp & trq & Hp & Hq & Hinter). + exists trp, (a :: trq). repeat split; try constructor; auto. + constructor; auto. + + specialize (IH _ _ Hrest) as (trp & trq & Hp & Hq & Hinter). + exists (out_act c v :: trp), (in_act c v :: trq). + repeat split; try constructor; auto. + constructor; auto. + + specialize (IH _ _ Hrest) as (trp & trq & Hp & Hq & Hinter). + exists (in_act c v :: trp), (out_act c v :: trq). + repeat split; try constructor; auto. + constructor; auto. + + specialize (IH _ _ Hrest) as (trp & trq & Hp & Hq & Hinter). + exists (a :: trp), trq. repeat split; try constructor; auto. + constructor; auto. + + specialize (IH _ _ Hrest) as (trp & trq & Hp & Hq & Hinter). + exists (a :: trp), trq. repeat split; try constructor; auto. + constructor; auto. + Qed. + + Lemma trace_par_combine p q trp trq tr : + trace p trp -> + trace q trq -> + sync_interleave trp trq tr -> + trace (par p q) tr. + Proof. + revert p q trp trq. + induction tr; intros p q trp trq Hp Hq Hinter; inversion Hinter; subst; clear Hinter. + - inversion Hp; inversion Hq; subst. constructor. + - inversion Hp as [ ? ? ? Hpstep Hp' ]; subst. + econstructor; [eapply step_par_l; eauto|]. + apply IHtr; auto. + - inversion Hq as [ ? ? ? Hqstep Hq' ]; subst. + econstructor; [eapply step_par_r; eauto|]. + apply IHtr; auto. + - inversion Hp as [ ? ? ? Hpstep Hp' ]; subst. + inversion Hq as [ ? ? ? Hqstep Hq' ]; subst. + econstructor; [eapply step_comm; eauto|]. + apply IHtr; auto. + - inversion Hp as [ ? ? ? Hpstep Hp' ]; subst. + inversion Hq as [ ? ? ? Hqstep Hq' ]; subst. + econstructor; [eapply step_comm; eauto|]. + apply IHtr; auto. + Qed. + + Theorem par_refines p1 q1 p2 q2 : + refines p1 q1 -> + refines p2 q2 -> + refines (par p1 p2) (par q1 q2). + Proof. + intros H1 H2 t [tr [Htr Ht]]. + apply trace_par_split in Htr as (trp & trq & Hp & Hq & Hinter). + assert (sem_proc q1 (trace_term trp)) as Hsem1 by (apply H1; eauto). + assert (sem_proc q2 (trace_term trq)) as Hsem2 by (apply H2; eauto). + destruct Hsem1 as [trp' [Hp' Heqp]]. + destruct Hsem2 as [trq' [Hq' Heqq]]. + apply trace_term_injective in Heqp; subst. + apply trace_term_injective in Heqq; subst. + exists tr. split. + - eapply trace_par_combine; eauto. + - assumption. + Qed. + +End PiSemantics. + diff --git a/models/Pi/Syntax.v b/models/Pi/Syntax.v new file mode 100644 index 0000000..ef804a3 --- /dev/null +++ b/models/Pi/Syntax.v @@ -0,0 +1,109 @@ +Require Import Coq.Arith.PeanoNat. +Require Import Coq.Bool.Bool. + +(** Locally-nameless π-calculus syntax with explicit open/close and + substitution operations. Bound names are de Bruijn indices; free + names are natural numbers. *) + +Module PiSyntax. + + Definition atom := nat. + + Inductive nvar := + | BVar : nat -> nvar + | FVar : atom -> nvar. + + Inductive proc := + | zero + | tau_prefix (p : proc) + | send (c v : nvar) (p : proc) + | recv (c : nvar) (p : proc) (* binds one name in [p] *) + | par (p q : proc) + | choice (p q : proc) + | nu (p : proc) (* binds one name in [p] *) + | rep (p : proc). + + (** Opening replaces the bound index [k] by a free name [x]. *) + Definition open_name_rec (k : nat) (x : atom) (n : nvar) : nvar := + match n with + | BVar i => if Nat.eqb i k then FVar x else n + | FVar _ => n + end. + + Fixpoint open_rec (k : nat) (x : atom) (p : proc) : proc := + match p with + | zero => zero + | tau_prefix p1 => tau_prefix (open_rec k x p1) + | send c v p1 => send (open_name_rec k x c) (open_name_rec k x v) (open_rec k x p1) + | recv c p1 => recv (open_name_rec k x c) (open_rec (S k) x p1) + | par p1 p2 => par (open_rec k x p1) (open_rec k x p2) + | choice p1 p2 => choice (open_rec k x p1) (open_rec k x p2) + | nu p1 => nu (open_rec (S k) x p1) + | rep p1 => rep (open_rec k x p1) + end. + + Definition open (x : atom) (p : proc) : proc := open_rec 0 x p. + + (** Closing turns a free name [x] into the bound index [k]. *) + Definition close_name_rec (k : nat) (x : atom) (n : nvar) : nvar := + match n with + | BVar i => BVar i + | FVar y => if Nat.eqb y x then BVar k else FVar y + end. + + Fixpoint close_rec (k : nat) (x : atom) (p : proc) : proc := + match p with + | zero => zero + | tau_prefix p1 => tau_prefix (close_rec k x p1) + | send c v p1 => send (close_name_rec k x c) (close_name_rec k x v) (close_rec k x p1) + | recv c p1 => recv (close_name_rec k x c) (close_rec (S k) x p1) + | par p1 p2 => par (close_rec k x p1) (close_rec k x p2) + | choice p1 p2 => choice (close_rec k x p1) (close_rec k x p2) + | nu p1 => nu (close_rec (S k) x p1) + | rep p1 => rep (close_rec k x p1) + end. + + Definition close (x : atom) (p : proc) : proc := close_rec 0 x p. + + (** Capture-avoiding substitution on free names. *) + Definition subst_name (x y : atom) (n : nvar) : nvar := + match n with + | BVar i => BVar i + | FVar z => if Nat.eqb z x then FVar y else FVar z + end. + + Fixpoint subst (x y : atom) (p : proc) : proc := + match p with + | zero => zero + | tau_prefix p1 => tau_prefix (subst x y p1) + | send c v p1 => send (subst_name x y c) (subst_name x y v) (subst x y p1) + | recv c p1 => recv (subst_name x y c) (subst x y p1) + | par p1 p2 => par (subst x y p1) (subst x y p2) + | choice p1 p2 => choice (subst x y p1) (subst x y p2) + | nu p1 => nu (subst x y p1) + | rep p1 => rep (subst x y p1) + end. + + (** Local closure: [k] counts how many surrounding binders are in scope. *) + Definition lc_name (k : nat) (n : nvar) : Prop := + match n with + | BVar i => i < k + | FVar _ => True + end. + + Fixpoint lc_rec (k : nat) (p : proc) : Prop := + match p with + | zero => True + | tau_prefix p1 => lc_rec k p1 + | send c v p1 => lc_name k c /\ lc_name k v /\ lc_rec k p1 + | recv c p1 => lc_name k c /\ lc_rec (S k) p1 + | par p1 p2 => lc_rec k p1 /\ lc_rec k p2 + | choice p1 p2 => lc_rec k p1 /\ lc_rec k p2 + | nu p1 => lc_rec (S k) p1 + | rep p1 => lc_rec k p1 + end. + + Definition lc (p : proc) : Prop := lc_rec 0 p. + +End PiSyntax. +