Artifact for "Proof of Delivery: Mechanized Mailbox Types"

This is the artifact for the paper "Proof of Delivery: Programming with Mailbox Types". The artifact is compromised of a Docker image mailbox-types-rocq.tar containing The Rocq source code (inside the mailbox-types/theories directory) A HTML documentation (inside the mailbox-types/doc directory) and just the Rocq source code and documentation in mailbox-types-rocq.zip. The following table shows a mapping from definitions in the paper to corresponding Rocq definitions: Definition Paper Rocq File Rocq Name Notation Mailbox configuration Section 2.1 Message.v MailboxConfig Empty mailbox Section 2.1 Message.v EmptyMailbox ⟨⟩ Singleton mailbox Section 2.1 Message.v SingletonMailbox ⟨ M ⟩ Mailbox union Section 2.1 Message.v mailbox_union m1 ⊎ m2 Mailbox equality Section 2.1 Message.v mailbox_eq m1 =ᵐᵇ m2 Mailbox patterns Section 2.1 MailboxPatterns.v MPattern Pattern power Section 2.1 MailboxPatterns.v Pow Mailbox pattern semantics Section 2.1 MailboxPatterns.v valueOf m ∈ E Pattern inclusion Section 2.1 MailboxPatterns.v MPInclusion E ⊑ F Pattern equivalence Section 2.1 MailboxPatterns.v MPEqual E ≈ F Pattern residual Section 2.1 MailboxPatterns.v PatternResidual E // F ~= G Pattern Normal Form Section 2.1 MailboxPatterns.v PNFLit E ⊧ F Mailbox types Section 2.2 Types.v MType ! E, ? E Base types Section 2.2 Types.v BType Types Section 2.2 Types.v TType Pattern permutation Section 2.2 Types.v PatternEq Type permutation Section 2.2 Types.v TypeEq Type combinations Section 2.2 Types.v TypeCombination T ⊞ U ~= V Usage annotations Section 3.1 Types.v UsageAnnotation ◦, • Usage-annotated types Section 3.1 Types.v TUsage T ^^ n Type operation (second class) Section 3.1 Types.v secondType, secondUsage ⌈ T ⌉, ⌈ T ⌉ⁿ Type operation (returnable) Section 3.1 Types.v returnType, returnUsage ⌊ T ⌋, ⌊ T ⌋ⁿ Usage-annotated type combinations Section 3.1 Types.v TypeUsageCombination J ▷ K ~= L Usage combinations Section 3.1 Types.v UsageCombination n1 ▷ⁿ n2 ~= n Usage subtyping Section 3.1 Types.v UsageSubtype n1 ≤ⁿ n2 Subtyping Section 3.1 Types.v Subtype A ≤ B Unrestricted Type Section 3.1 Types.v Unrestricted Definition name Section 3.2 Syntax.v IDefinitionName Function defintions Section 3.2 Syntax.v FunctionDefinition Values Section 3.2 Syntax.v Value Terms Section 3.2 Syntax.v Term Guards Section 3.2 Syntax.v Guard Environments Section 3.2 Environment.v Env Program Section 3.2 Syntax.v Prog Environment subtyping Section 3.3 Environment.v EnvironmentSubtype Env1 ≤ₑ Env2 Environment combination Section 3.3 Environment.v EnvironmentCombination Env1 ▷ₑ Env2 ~= Env Disjoint environment combination Section 3.3 Environment.v EnvironmentDisjointCombination Env1 +ₑ Env2 ~= Env Empty environment Section 3.3 Environment.v EmptyEnv Typing rule for program Section 3.4 TypingRules.v WellTypedProgram Typing rule for definition Section 3.4 TypingRules.v WellTypedDefinition Typing rules for terms Section 3.4 TypingRules.v WellTypedTerm Typing rules for guard sequences Section 3.4 TypingRules.v WellTypedGuards Typing rules for guards Section 3.4 TypingRules.v WellTypedGuard The following table shows a mapping from lemmas in the paper to corresponding Rocq proofs: Property Paper Rocq File Rocq Name Pattern inclusion is reflexive Lemma 1 MailboxPatterns.v MPInclusion_refl Pattern inclusion is transitive Lemma 1 MailboxPatterns.v MPInclusion_trans Pattern inclusion compatible wrt. composition Lemma 1 MailboxPatterns.v MPInclusion_compatable_Comp Pattern inclusion compatible wrt. choice Lemma 1 MailboxPatterns.v MPInclusion_compatable_Choice Pattern equality is reflexive Lemma 2 MailboxPatterns.v MPEqual_refl Pattern equality is transitive Lemma 2 MailboxPatterns.v MPEqual_trans Pattern equality is symmetric Lemma 2 MailboxPatterns.v MPEqual_sym Patterns form a commutative Kleene algebra Section 2.1 MailboxPatterns.v MPattern_props Balancing lemma Lemma 3 MailboxPatterns.v Balancing Substitution lemma Lemma 4 Substitution.v subst_lemma Software Requirements Docker or Rocq (>= 9.0) and make Building the Project (Docker) Import the provided Docker image: docker load -i mailbox-types-rocq.tar Run the Docker image: docker run -it mailbox-types-rocq:latest A prompt of the form rocq@daf52d3edbb8:~/mailbox-types$ should open. Now run make to build the project A successful compilation indicates all theorems and lemmas hold Building the Project (Manually) You can also build the project using your native Rocq installation: Extract mailbox-types-rocq.zip Navigate into the extracted directory Run make to build the project A successful compilation indicates all theorems and lemmas hold