Andrew Hirsch
Pirouette Coq Code

Repository



Pirouette: Typed Functional Choreographies

Getting The Code
You can find this via MPI-SWS Gitlab instance at https://gitlab.mpi-sws.org/akhirsch/pirouette-coq

Mapping from Theorems in the Paper to Code
The equations for substitutions required for local programs can be found in LocalLang.v.
Likewise, the required-admissable rules for type systems can be found in TypedLocalLang.v.


Theorem Name (From Paper)
Theorem Number (From Paper)
Coq File(s)
Coq Name(s)


Lambda Calculus Example

LambdaCalc.v


STLC Example

STLC.v and STLCSound.v


Natural-Numbers Example

NatLang.vo, TypedNatLang.vo, and SoundlyTypedNatLang.vo


Relative Preservation
Theorem 1
TypedPirouette.v
RelativePreservation


Relative Progress
Theorem 2
TypedPirouette.v
RelativeProgress


Relative Soundness
Corollary 1
SoundlyTypedPirouette.v
Preverstion, StepsPreservation, and Progress


Equivalence Respects Types
Theorem 3
TypedPirouette.v
EquivTyping


Operational Semantics Simulates Equivalence
Theorem 4
Pirouette.v
EquivSimulation


Weak Semantics
Theorem 5
RestrictedSemantics.v
StdToRStep and RStepToStd


Equivalence Begets Equality
Theorem 6
EndPointProjection.v
EPPEquivToEq


Lifting System Steps
Theorem 7 (Part 1)
CtrlLang.v
LiftSystemNondetStep


Lowering System Steps
Theorem 7 (Part 2)
EndPointProjection.v
LowerCompiledSystemStep


Local Completeness
Theorem 8
EndPointProjection.v
FullLocalCompleteness


Global Completeness
Theorem 9
EndPointProjection.v
FullCompleteness


Local Soundness (Iota)
Theorem 10 (Part 1)
EndPointProjection.v
LocalIotaSoundness


Local Soundness (Comm)
Theorem 10 (Part 2)
EndPointProjection.v
LocalCommSoundness


Local Soundness (Sync)
Theorem 10 (Part 3)
EndPointProjection.v
LocalSyncSoundness


Local Soundness (SyncIota)
Theorem 10 (Part 4)
EndPointProjection.v
LocalSyncIotaSoundness


Global Soundness
Theorem 11
EndPointProjection.v
Soundness


Deadlock Fredom by Design
Theorem 12
EndPointProjection.v
DeadlockFreedomByDesign


The following table refers to theorems found only in Appendix G of the technical-report version of the paper:


Theorem Name (From Paper)
Theorem Number (From Paper)
Coq File(s)
Coq Name(s)


Pirouette Types Structural Rules
Theorem 13
TypedPirouette.v
TypeLocalWeakening, TypePirExprWeakening and PirExprClosedAboveTyping


Equivalence Preserves Variables
Theorem 14 (Part 1)
Pirouette.v
PirExprClosedAboveEquiv


Equivalence Preserves Location Names
Theorem 14 (Part 2)
Pirouette.v
LocsInPirExprInvariant


Equivalence Preserves Values
Theorem 14 (Part 3)
Pirouette.v
PirExprValStableEquiv


Equivalence Preserves Local Substitution
Theorem 14 (Part 4)
Pirouette.v
EquivStableLocalSubst


Equivalence Preserves Global Substitution
Theorem 14 (Part 5)
Pirouette.v
WeakSubstExt


Merge is Idempotent
Theorem 15 (Part 1)
CtrlLanguage.v
MergeIdempotent


Merge is Commutative
Theorem 15 (Part 2)
CtrlLanguage.v
MergeComm


Merge is Associative
Theorem 15 (Part 3)
CtrlLanguage.v
MergeAssoc and MergeAssocNone


Merge Preserves Free Vars
Theorem 16 (Part 1)
CtrlLanguage.v
MergeClosed


Merge Preserves Local Substitution
Theorem 16 (Part 2)
CtrlLanguage.v
MergeExprSubst


Merge Preserves Global Substitution
Theorem 16 (Part 3)
CtrlLanguage.v
MergeSubst


Merge Preserves Values
Theorem 16 (Part 4)
CtrlLanguage.v
MergeCtrlExprVals and MergeRelToVal


Merge Preserves Reduction
Theorem 17
CtrlLanguage.v
MergeStep' and MergeStep'Exists


Merge Creates Reduction
Theorem 17
CtrlLanguage.v
UnmergeRelStep


EPP Preserves Variables
Theorem 18 (Part 1)
EndPointProjection.v
EPPClosedAbove


EPP Preserves Local Substitution
Theorem 18 (Part 2)
EndPointProjection.v
EPPLocalSubst


EPP Preserves Global Substitution
Theorem 18 (Part 3)
EndPointProjection.v
EPPSubst


EPP Preserves Values
Theorem 18 (Part 4)
EndPointProjection.v
EPPValue


EPP Creates Values
Theorem 18 (Part 5)
EndPointProjection.v
ValueSoundness


LND is Reflexive
Theorem 19 (Part 1)
CtrlLanguage.v
LessNondetRefl


LND is Antisymmetric
Theorem 19 (Part 2)
CtrlLanguage.v
LessNondetAntisym


LND is Transitive
Theorem 19 (Part 3)
CtrlLanguage.v
LessNondetTrans


LND Preserves Local Substitition
Theorem 20 (Part 1)
CtrlLanguage.v
LessNondetExprSubst


LND Preserves Global Substitition
Theorem 20 (Part 2)
CtrlLanguage.v
LessNondetSubst


Merging Creates LND
Thoerem 20 (Part 3)
CtrlLanguage.v
MergeLessNondet


Merging Preserves LND
Theorem 20 (Part 4)
CtrlLanguage.v
LessNondetMerge


LND is Reflexivity on Values
Theorem 20 (Part 5)
CtrlLanguage.v
LessNondetVals


Steps Lift Across LND
Theorem 21
CtrlLanguage.v
LiftStepWithNondet


Lowering steps Across LND
Theorem 22
CtrlLanguage.v
LowerStepNondet


Compiling
This has been tested with vanilla Coq 8.13.2.
To generate the makefile, type coq_makefile -f Makefile -o _CoqProject.
Then, you can simply type make in order to build the entire project, and make clean to remove compiled files.
In order to rebuild the makefile, type coq_makefile -f Makefile -o _CoqProject again.
Note that compiling takes a while, so get yourself a cup of coffee or something after typing make!

Compile time
Sadly, make take quite a while.
In particular, several files (Pirouette.v, RestrictedSemantics.v, CtrlLang.v, and EndPointProjection.v) take several minutes to compile,
and both Pirouette.v and RestrictedSemantics.v take many minutes.
Here are the times per file, as reported by make pretty-timed TIMING_REAL=1:


Time
Peak Mem
File Name


41m09.94s
17445240 ko
Total Time / Peak Mem


15m10.11s
778832 ko
Pirouette.vo


14m00.01s
763140 ko
RestrictedSemantics.vo


6m53.25s
17445240 ko
EndPointProjection.vo


5m00.33s
1195096 ko
CtrlLang.vo


0m02.85s
494208 ko
TypedPirouette.vo


0m00.51s
355152 ko
STLCSound.vo


0m00.49s
352468 ko
FunLMap.vo


0m00.45s
344880 ko
LambdaCalc.vo


0m00.43s
366200 ko
SoundlyTypedPirouette.vo


0m00.31s
346908 ko
STLC.vo


0m00.22s
266176 ko
TypedNatLang.vo


0m00.20s
221656 ko
NatLang.vo


0m00.17s
184740 ko
LocationMap.vo


0m00.15s
176296 ko
SoundlyTypedNatLang.vo


0m00.15s
166828 ko
UnitypedLC.vo


0m00.08s
82076 ko
LocalLang.vo


0m00.07s
71816 ko
TypedLocalLang.vo


0m00.06s
63984 ko
SoundlyTypedLocalLang.vo


0m00.06s
65832 ko
SyncLabels.vo


0m00.05s
61996 ko
Locations.vo


Size
This is a nontrivially large project.
It consists of 13,502 lines of Coq code in total.
Here is the breakdown of the lines of code as reported by cloc --by-file-by-lang . --exclude-lang=make,D,Markdown:


File
blank
comment
code


./EndPointProjection.v
139
123
3849


./CtrlLang.v
204
257
3408


./Pirouette.v
147
226
1825


./TreeLocationMap.v
96
3
1604


./RestrictedSemantics.v
31
66
567


./TypedPirouette.v
31
77
456


./FunLMap.v
54
16
455


./LambdaCalc.v
41
52
323


./ListLMap.v
44
107
152


./NatLang.v
30
12
145


./STLC.v
11
3
129


./LocationMap.v
32
23
105


./UnitypedLC.v
17
0
103


./TypedNatLang.v
15
3
90


./LocalLang.v
26
71
88


./STLCSound.v
6
3
65


./TypedLocalLang.v
16
58
51


./SoundlyTypedPirouette.v
5
0
35


./SoundlyTypedNatLang.v
5
0
30


./SoundlyTypedLocalLang.v
3
9
12


./SyncLabels.v
1
5
6


./Locations.v
5
5
4


SUM
959
1119
13502