Added CP mechanization

Beluga-lang · Mar 7, 2024 · 8df5506 · 8df5506
1 parent a3e6919
commit 8df5506
Show file tree

Hide file tree

Showing 9 changed files with 1,004 additions and 0 deletions.
diff --git a/case-studies/classical-processes/LICENSE b/case-studies/classical-processes/LICENSE
@@ -0,0 +1,13 @@
+Copyright 2023 Chuta Sano, Ryan Kavanagh, Brigitte Pientka
+
+Permission to use, copy, modify, and/or distribute this software for any purpose
+with or without fee is hereby granted, provided that the above copyright notice
+and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED “AS IS” AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH
+REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT,
+INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS
+OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER
+TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF
+THIS SOFTWARE.
diff --git a/case-studies/classical-processes/README.md b/case-studies/classical-processes/README.md
@@ -0,0 +1,95 @@
+# Overview
+
+This artifact contains the Beluga mechanization for the paper
+
+    Mechanizing Session-Types Using a Structural View
+    C. Sano, R. Kavanagh, B. Pientka
+    Proceedings of the ACM on Programming Languages, Volume 7,
+    Number OOPSLA2, Article No. 235 (October 2023),
+    https://doi.org/10.1145/3622810
+
+and is a copy of the accompanying artifact (https://doi.org/10.5281/zenodo.8329645)
+
+Below are files that are included in this artifact.
+
+	cp.cfg         - Collects all used Beluga source files
+	cp_base.bel    - Contains encodings of session types and processes
+	cp_linear.bel  - Contains encoding of the linearity predicate
+	cp_statics.bel - Contains encoding of the type judgment
+	cp_dyn.bel     - Contains encoding of the reductions and congruences
+	cp_lemmas.bel  - Contains proofs of intermediary lemmas
+	cp_thrm.bel    - Proof of type preservation
+
+There are some minor differences in code snippets as written in the
+paper for presentation purposes compared to the code in the artifact,
+which we summarize below.
+
+| Item                    | On-paper Notation | Artifact     |
+|-------------------------|-------------------|--------------|
+| Reduction rule names    | βcut1 and βinl    | β∥1 and β⊕&1 |
+| Structural Equivalences | equiv P Q         | P ≡ Q        |
+| Reductions              | step P Q          | P ⇛ Q        |
+| Abstractions            | λx. M             | \x. M        |
+
+## Paper to Artifact Table
+
+| Definition/Proofs                                     | Paper                        | File           | Definition Name                                    |
+|-------------------------------------------------------|------------------------------|----------------|----------------------------------------------------|
+| Session types, duality, and processes                 | Sections 4.1 and 4.2         | cp_base.bel    | tp, dual, and proc                                 |
+| Linearity predicate                                   | Section 4.3                  | cp_linear.bel  | linear                                             |
+| Type judgments                                        | Section 4.4                  | cp_statics.bel | wtp                                                |
+| Reductions and Structural Equivalences                | Section 4.5                  | cp_dyn.bel     | ⇛ and ≡ (used as infix operators)                  |
+| Symmetricity and Uniqueness of dual                   | Section 6.1                  | cp_lemmas.bel  | dual_sym and dual_uniq                             |
+| Strengthening Lemmas                                  | Section 6.2, Lemma 6.1 (1-5) | cp_lemmas.bel  | str_hyp, str_lin, str_wtp, str_step, and str_equiv |
+| Linearity implies usage                               | Section 6.3, Lemma 6.2       | cp_lemmas.bel  | lin_name_must_appear                               |
+| Structural equivalence preserves linearity and typing | Section 6.3, Lemma 6.3       | cp_thrm.bel    | lin_s≡ and wtp_s≡                                  |
+| Type preservation                                     | Section 6.4, Theorem 6.4     | cp_thrm.bel    | lin_s and wtp_s                                    |
+
+
+# Installation and Execution
+
+This mechanization is compatible with Beluga version 1.1.
+
+## Installation
+
+The easiest way to install Beluga is using `opam`:
+
+    >> opam install beluga.1.1
+
+Beluga can also be installed from source by following the "Installation
+from the source" instructions on
+https://github.com/Beluga-lang/Beluga/tree/v1.1
+
+Alternatively, we have provided a virtual machine based on OpenBSD 7.3
+that has Beluga 1.1, its sources, and our mechanization pre-installed.
+This QCOW2 disk image can be run using QEMU using the command:
+
+    >> qemu-system-amd64 -hda artifact.qcow2 -m 1G
+
+For a better user experience, we suggest the following options, which
+give the virtual machine 4 gigabytes of memory, four CPUs, and allow
+the machine to be accessed over SSH on localhost port 60022 using
+username `artifact` and password `artifact`:
+
+    >> qemu-system-amd64 -hda artifact.qcow2 -m 4G -smp 4 \
+                         -nic user,hostfwd=tcp::60022-:22
+    >> ssh artifact@127.0.0.1 -p 60022
+
+## Execution
+
+Once Beluga is installed, it can be run on the file `cp.cfg`. The
+following is the expected output:
+
+	>> beluga cp.cfg
+	## Type Reconstruction begin: ./cp_base.bel ##
+	## Type Reconstruction done:  ./cp_base.bel ##
+	## Type Reconstruction begin: ./cp_linear.bel ##
+	## Type Reconstruction done:  ./cp_linear.bel ##
+	## Type Reconstruction begin: ./cp_statics.bel ##
+	## Type Reconstruction done:  ./cp_statics.bel ##
+	## Type Reconstruction begin: ./cp_dyn.bel ##
+	## Type Reconstruction done:  ./cp_dyn.bel ##
+	## Type Reconstruction begin: ./cp_lemmas.bel ##
+	## Type Reconstruction done:  ./cp_lemmas.bel ##
+	## Type Reconstruction begin: ./cp_thrm.bel ##
+	## Type Reconstruction done:  ./cp_thrm.bel ##
diff --git a/case-studies/classical-processes/cp.cfg b/case-studies/classical-processes/cp.cfg
@@ -0,0 +1,7 @@
+cp_base.bel
+cp_linear.bel
+cp_statics.bel
+cp_dyn.bel
+cp_lemmas.bel
+cp_thrm.bel
+
diff --git a/case-studies/classical-processes/cp_base.bel b/case-studies/classical-processes/cp_base.bel
@@ -0,0 +1,49 @@
+% Basic shared definitions of CP
+% Defines types, duality, processes, and equality predicates on types/processes
+
+name : type.      % channel names
+
+tp : type.        % channel types
+① : tp.           % termination ("provider")
+⊥ : tp.           % termination ("client")
+⊗ : tp → tp → tp. % channel output
+⅋ : tp → tp → tp. % channel input
+& : tp → tp → tp. % receive choice
+⊕ : tp → tp → tp. % send choice
+
+--infix ⊗ 5 left.
+--infix ⅋ 5 left.
+--infix ⊕ 4 left.
+--infix & 4 left.
+
+eq : tp → tp → type.
+refl : eq A A.
+
+% duality condition
+dual : tp → tp → type.
+D1 : dual ① ⊥.
+D⊥ : dual ⊥ ①.
+D⊗ : dual A A' → dual B B' → dual (A ⊗ B) (A' ⅋ B').
+D⅋ : dual A A' → dual B B' → dual (A ⅋ B) (A' ⊗ B').
+D& : dual A A' → dual B B' → dual (A & B) (A' ⊕ B').
+D⊕ : dual A A' → dual B B' → dual (A ⊕ B) (A' & B').
+
+% processes
+proc : type.
+
+eq_proc : proc → proc → type.
+refl_proc : eq_proc P P.
+
+fwd : name → name → proc.                             % fwd x y
+pcomp : tp → (name → proc) → (name → proc) → proc.    % nu x:A (P | Q)
+
+close : name → proc.                                  % close x
+wait : name → proc → proc.                            % wait x; P
+
+out : name → (name → proc) → (name → proc) → proc.    % out x; (y.P | w.Q)
+inp : name → (name → name → proc) → proc.             % inp x; w.y.P
+
+inl : name → (name → proc) → proc.                    % x[inl]; w.P
+inr : name → (name → proc) → proc.                    % x[inr]; w.P
+choice : name → (name → proc) → (name → proc) → proc. % case x {w.P | w.Q}
+
diff --git a/case-studies/classical-processes/cp_dyn.bel b/case-studies/classical-processes/cp_dyn.bel
@@ -0,0 +1,52 @@
+% Dynamics of CP
+
+% Structural Equivalences
+≡ : proc → proc → type.
+--infix ≡ 10 left.
+≡comm : dual A A' → (pcomp A  P Q) ≡ (pcomp A' Q  P).
+≡assoc: (pcomp B (\y. pcomp A P (\x. Q x y)) R)
+      ≡ (pcomp A P (\x. pcomp B (Q x) R)).
+
+% Beta reductions, commuting conversions, and congruence for pcomp
+⇛ : proc → proc → type.
+--infix ⇛ 10 left.
+
+% Note: keep in mind ⇛ is an infix type constructor and is therefore unrelated to
+% →, which constructs LF functions
+% principal reductions
+βfwd : (pcomp A (\x. fwd x Y) P)
+     ⇛ (P Y).
+β1⊥  : (pcomp ① (\x. close x) (\x. wait x P))
+     ⇛ P.
+β⊗⅋  : (pcomp (A ⊗ B) (\x. (out x P Q)) (\x. inp x R))
+     ⇛ (pcomp A P (\y. pcomp B Q (\x. R x y))).
+β⊕&1 : (pcomp (A ⊕ B) (\x. inl x P) (\x. choice x Q R))
+     ⇛ (pcomp A P Q).
+β⊕&2 : (pcomp (A ⊕ B) (\x. inr x P) (\x. choice x Q R))
+     ⇛ (pcomp B P R).
+
+% commuting conversions
+κ⊥  : (pcomp C (\z. wait X (P z)) R)
+    ⇛ (wait X (pcomp C P R)).
+κ⊗1 : (pcomp C (\z. out X (\y. P y z) Q) R)
+    ⇛ (out X (\y. pcomp C (\z. P y z) R) Q).
+κ⊗2 : (pcomp C (\z. out X P (\x. Q x z)) R)
+    ⇛ (out X P (\x. pcomp C (\z. Q x z) R)).
+κ⅋  : (pcomp C (\z. inp X (\x.\y. P x y z)) Q)
+    ⇛ (inp X (\x.\y. pcomp C (\z. P x y z) Q)).
+κ⊕1 : (pcomp C (\z. inl X (\x. P x z)) Q)
+    ⇛ (inl X (\x. pcomp C (\z. P x z) Q)).
+κ⊕2 : (pcomp C (\z. inr X (\x. P x z)) Q)
+    ⇛ (inr X (\x. pcomp C (\z. P x z) Q)).
+κ&  : (pcomp C (\z. choice X (\x. P x z) (\x. Q x z)) R)
+    ⇛ (choice X (\x. pcomp C (\z. (P x z)) R) (\x. pcomp C (\z. Q x z) R)).
+
+% reduction under cut
+β∥1 : ({x:name} ((P x) ⇛ (P' x)))
+    → (pcomp A P Q) ⇛ (pcomp A P' Q).
+β∥2 : ({x:name}((Q x) ⇛ (Q' x)))
+    → (pcomp A P Q) ⇛ (pcomp A P Q').
+
+% Reductions commute with equivalences
+β≡: (P ≡ Q) → (Q ⇛ R) → (R ≡ S) → P ⇛ S.
+