-
Notifications
You must be signed in to change notification settings - Fork 0
/
README.html
724 lines (702 loc) · 79.5 KB
/
README.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<title>Fair Termination of Binary Sessions - Artifact</title>
<style>
/* From extension vscode.markdown-math */
@font-face{font-family:KaTeX_AMS;src:url(fonts/KaTeX_AMS-Regular.woff2) format("woff2"),url(fonts/KaTeX_AMS-Regular.woff) format("woff"),url(fonts/KaTeX_AMS-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Caligraphic;src:url(fonts/KaTeX_Caligraphic-Bold.woff2) format("woff2"),url(fonts/KaTeX_Caligraphic-Bold.woff) format("woff"),url(fonts/KaTeX_Caligraphic-Bold.ttf) format("truetype");font-weight:700;font-style:normal}@font-face{font-family:KaTeX_Caligraphic;src:url(fonts/KaTeX_Caligraphic-Regular.woff2) format("woff2"),url(fonts/KaTeX_Caligraphic-Regular.woff) format("woff"),url(fonts/KaTeX_Caligraphic-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Fraktur;src:url(fonts/KaTeX_Fraktur-Bold.woff2) format("woff2"),url(fonts/KaTeX_Fraktur-Bold.woff) format("woff"),url(fonts/KaTeX_Fraktur-Bold.ttf) format("truetype");font-weight:700;font-style:normal}@font-face{font-family:KaTeX_Fraktur;src:url(fonts/KaTeX_Fraktur-Regular.woff2) format("woff2"),url(fonts/KaTeX_Fraktur-Regular.woff) format("woff"),url(fonts/KaTeX_Fraktur-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Main;src:url(fonts/KaTeX_Main-Bold.woff2) format("woff2"),url(fonts/KaTeX_Main-Bold.woff) format("woff"),url(fonts/KaTeX_Main-Bold.ttf) format("truetype");font-weight:700;font-style:normal}@font-face{font-family:KaTeX_Main;src:url(fonts/KaTeX_Main-BoldItalic.woff2) format("woff2"),url(fonts/KaTeX_Main-BoldItalic.woff) format("woff"),url(fonts/KaTeX_Main-BoldItalic.ttf) format("truetype");font-weight:700;font-style:italic}@font-face{font-family:KaTeX_Main;src:url(fonts/KaTeX_Main-Italic.woff2) format("woff2"),url(fonts/KaTeX_Main-Italic.woff) format("woff"),url(fonts/KaTeX_Main-Italic.ttf) format("truetype");font-weight:400;font-style:italic}@font-face{font-family:KaTeX_Main;src:url(fonts/KaTeX_Main-Regular.woff2) format("woff2"),url(fonts/KaTeX_Main-Regular.woff) format("woff"),url(fonts/KaTeX_Main-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Math;src:url(fonts/KaTeX_Math-BoldItalic.woff2) format("woff2"),url(fonts/KaTeX_Math-BoldItalic.woff) format("woff"),url(fonts/KaTeX_Math-BoldItalic.ttf) format("truetype");font-weight:700;font-style:italic}@font-face{font-family:KaTeX_Math;src:url(fonts/KaTeX_Math-Italic.woff2) format("woff2"),url(fonts/KaTeX_Math-Italic.woff) format("woff"),url(fonts/KaTeX_Math-Italic.ttf) format("truetype");font-weight:400;font-style:italic}@font-face{font-family:"KaTeX_SansSerif";src:url(fonts/KaTeX_SansSerif-Bold.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Bold.woff) format("woff"),url(fonts/KaTeX_SansSerif-Bold.ttf) format("truetype");font-weight:700;font-style:normal}@font-face{font-family:"KaTeX_SansSerif";src:url(fonts/KaTeX_SansSerif-Italic.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Italic.woff) format("woff"),url(fonts/KaTeX_SansSerif-Italic.ttf) format("truetype");font-weight:400;font-style:italic}@font-face{font-family:"KaTeX_SansSerif";src:url(fonts/KaTeX_SansSerif-Regular.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Regular.woff) format("woff"),url(fonts/KaTeX_SansSerif-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Script;src:url(fonts/KaTeX_Script-Regular.woff2) format("woff2"),url(fonts/KaTeX_Script-Regular.woff) format("woff"),url(fonts/KaTeX_Script-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Size1;src:url(fonts/KaTeX_Size1-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size1-Regular.woff) format("woff"),url(fonts/KaTeX_Size1-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Size2;src:url(fonts/KaTeX_Size2-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size2-Regular.woff) format("woff"),url(fonts/KaTeX_Size2-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Size3;src:url(fonts/KaTeX_Size3-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size3-Regular.woff) format("woff"),url(fonts/KaTeX_Size3-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Size4;src:url(fonts/KaTeX_Size4-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size4-Regular.woff) format("woff"),url(fonts/KaTeX_Size4-Regular.ttf) format("truetype");font-weight:400;font-style:normal}@font-face{font-family:KaTeX_Typewriter;src:url(fonts/KaTeX_Typewriter-Regular.woff2) format("woff2"),url(fonts/KaTeX_Typewriter-Regular.woff) format("woff"),url(fonts/KaTeX_Typewriter-Regular.ttf) format("truetype");font-weight:400;font-style:normal}.katex{font:normal 1.21em KaTeX_Main,Times New Roman,serif;line-height:1.2;text-indent:0;text-rendering:auto;border-color:currentColor}.katex *{-ms-high-contrast-adjust:none!important}.katex .katex-version:after{content:"0.13.0"}.katex .katex-mathml{position:absolute;clip:rect(1px,1px,1px,1px);padding:0;border:0;height:1px;width:1px;overflow:hidden}.katex .katex-html>.newline{display:block}.katex .base{position:relative;white-space:nowrap;width:-webkit-min-content;width:-moz-min-content;width:min-content}.katex .base,.katex .strut{display:inline-block}.katex .textbf{font-weight:700}.katex .textit{font-style:italic}.katex .textrm{font-family:KaTeX_Main}.katex .textsf{font-family:KaTeX_SansSerif}.katex .texttt{font-family:KaTeX_Typewriter}.katex .mathnormal{font-family:KaTeX_Math;font-style:italic}.katex .mathit{font-family:KaTeX_Main;font-style:italic}.katex .mathrm{font-style:normal}.katex .mathbf{font-family:KaTeX_Main;font-weight:700}.katex .boldsymbol{font-family:KaTeX_Math;font-weight:700;font-style:italic}.katex .amsrm,.katex .mathbb,.katex .textbb{font-family:KaTeX_AMS}.katex .mathcal{font-family:KaTeX_Caligraphic}.katex .mathfrak,.katex .textfrak{font-family:KaTeX_Fraktur}.katex .mathtt{font-family:KaTeX_Typewriter}.katex .mathscr,.katex .textscr{font-family:KaTeX_Script}.katex .mathsf,.katex .textsf{font-family:KaTeX_SansSerif}.katex .mathboldsf,.katex .textboldsf{font-family:KaTeX_SansSerif;font-weight:700}.katex .mathitsf,.katex .textitsf{font-family:KaTeX_SansSerif;font-style:italic}.katex .mainrm{font-family:KaTeX_Main;font-style:normal}.katex .vlist-t{display:inline-table;table-layout:fixed;border-collapse:collapse}.katex .vlist-r{display:table-row}.katex .vlist{display:table-cell;vertical-align:bottom;position:relative}.katex .vlist>span{display:block;height:0;position:relative}.katex .vlist>span>span{display:inline-block}.katex .vlist>span>.pstrut{overflow:hidden;width:0}.katex .vlist-t2{margin-right:-2px}.katex .vlist-s{display:table-cell;vertical-align:bottom;font-size:1px;width:2px;min-width:2px}.katex .vbox{display:inline-flex;flex-direction:column;align-items:baseline}.katex .hbox{width:100%}.katex .hbox,.katex .thinbox{display:inline-flex;flex-direction:row}.katex .thinbox{width:0;max-width:0}.katex .msupsub{text-align:left}.katex .mfrac>span>span{text-align:center}.katex .mfrac .frac-line{display:inline-block;width:100%;border-bottom-style:solid}.katex .hdashline,.katex .hline,.katex .mfrac .frac-line,.katex .overline .overline-line,.katex .rule,.katex .underline .underline-line{min-height:1px}.katex .mspace{display:inline-block}.katex .clap,.katex .llap,.katex .rlap{width:0;position:relative}.katex .clap>.inner,.katex .llap>.inner,.katex .rlap>.inner{position:absolute}.katex .clap>.fix,.katex .llap>.fix,.katex .rlap>.fix{display:inline-block}.katex .llap>.inner{right:0}.katex .clap>.inner,.katex .rlap>.inner{left:0}.katex .clap>.inner>span{margin-left:-50%;margin-right:50%}.katex .rule{display:inline-block;border:0 solid;position:relative}.katex .hline,.katex .overline .overline-line,.katex .underline .underline-line{display:inline-block;width:100%;border-bottom-style:solid}.katex .hdashline{display:inline-block;width:100%;border-bottom-style:dashed}.katex .sqrt>.root{margin-left:.27777778em;margin-right:-.55555556em}.katex .fontsize-ensurer.reset-size1.size1,.katex .sizing.reset-size1.size1{font-size:1em}.katex .fontsize-ensurer.reset-size1.size2,.katex .sizing.reset-size1.size2{font-size:1.2em}.katex .fontsize-ensurer.reset-size1.size3,.katex .sizing.reset-size1.size3{font-size:1.4em}.katex .fontsize-ensurer.reset-size1.size4,.katex .sizing.reset-size1.size4{font-size:1.6em}.katex .fontsize-ensurer.reset-size1.size5,.katex .sizing.reset-size1.size5{font-size:1.8em}.katex .fontsize-ensurer.reset-size1.size6,.katex .sizing.reset-size1.size6{font-size:2em}.katex .fontsize-ensurer.reset-size1.size7,.katex .sizing.reset-size1.size7{font-size:2.4em}.katex .fontsize-ensurer.reset-size1.size8,.katex .sizing.reset-size1.size8{font-size:2.88em}.katex .fontsize-ensurer.reset-size1.size9,.katex .sizing.reset-size1.size9{font-size:3.456em}.katex .fontsize-ensurer.reset-size1.size10,.katex .sizing.reset-size1.size10{font-size:4.148em}.katex .fontsize-ensurer.reset-size1.size11,.katex .sizing.reset-size1.size11{font-size:4.976em}.katex .fontsize-ensurer.reset-size2.size1,.katex .sizing.reset-size2.size1{font-size:.83333333em}.katex .fontsize-ensurer.reset-size2.size2,.katex .sizing.reset-size2.size2{font-size:1em}.katex .fontsize-ensurer.reset-size2.size3,.katex .sizing.reset-size2.size3{font-size:1.16666667em}.katex .fontsize-ensurer.reset-size2.size4,.katex .sizing.reset-size2.size4{font-size:1.33333333em}.katex .fontsize-ensurer.reset-size2.size5,.katex .sizing.reset-size2.size5{font-size:1.5em}.katex .fontsize-ensurer.reset-size2.size6,.katex .sizing.reset-size2.size6{font-size:1.66666667em}.katex .fontsize-ensurer.reset-size2.size7,.katex .sizing.reset-size2.size7{font-size:2em}.katex .fontsize-ensurer.reset-size2.size8,.katex .sizing.reset-size2.size8{font-size:2.4em}.katex .fontsize-ensurer.reset-size2.size9,.katex .sizing.reset-size2.size9{font-size:2.88em}.katex .fontsize-ensurer.reset-size2.size10,.katex .sizing.reset-size2.size10{font-size:3.45666667em}.katex .fontsize-ensurer.reset-size2.size11,.katex .sizing.reset-size2.size11{font-size:4.14666667em}.katex .fontsize-ensurer.reset-size3.size1,.katex .sizing.reset-size3.size1{font-size:.71428571em}.katex .fontsize-ensurer.reset-size3.size2,.katex .sizing.reset-size3.size2{font-size:.85714286em}.katex .fontsize-ensurer.reset-size3.size3,.katex .sizing.reset-size3.size3{font-size:1em}.katex .fontsize-ensurer.reset-size3.size4,.katex .sizing.reset-size3.size4{font-size:1.14285714em}.katex .fontsize-ensurer.reset-size3.size5,.katex .sizing.reset-size3.size5{font-size:1.28571429em}.katex .fontsize-ensurer.reset-size3.size6,.katex .sizing.reset-size3.size6{font-size:1.42857143em}.katex .fontsize-ensurer.reset-size3.size7,.katex .sizing.reset-size3.size7{font-size:1.71428571em}.katex .fontsize-ensurer.reset-size3.size8,.katex .sizing.reset-size3.size8{font-size:2.05714286em}.katex .fontsize-ensurer.reset-size3.size9,.katex .sizing.reset-size3.size9{font-size:2.46857143em}.katex .fontsize-ensurer.reset-size3.size10,.katex .sizing.reset-size3.size10{font-size:2.96285714em}.katex .fontsize-ensurer.reset-size3.size11,.katex .sizing.reset-size3.size11{font-size:3.55428571em}.katex .fontsize-ensurer.reset-size4.size1,.katex .sizing.reset-size4.size1{font-size:.625em}.katex .fontsize-ensurer.reset-size4.size2,.katex .sizing.reset-size4.size2{font-size:.75em}.katex .fontsize-ensurer.reset-size4.size3,.katex .sizing.reset-size4.size3{font-size:.875em}.katex .fontsize-ensurer.reset-size4.size4,.katex .sizing.reset-size4.size4{font-size:1em}.katex .fontsize-ensurer.reset-size4.size5,.katex .sizing.reset-size4.size5{font-size:1.125em}.katex .fontsize-ensurer.reset-size4.size6,.katex .sizing.reset-size4.size6{font-size:1.25em}.katex .fontsize-ensurer.reset-size4.size7,.katex .sizing.reset-size4.size7{font-size:1.5em}.katex .fontsize-ensurer.reset-size4.size8,.katex .sizing.reset-size4.size8{font-size:1.8em}.katex .fontsize-ensurer.reset-size4.size9,.katex .sizing.reset-size4.size9{font-size:2.16em}.katex .fontsize-ensurer.reset-size4.size10,.katex .sizing.reset-size4.size10{font-size:2.5925em}.katex .fontsize-ensurer.reset-size4.size11,.katex .sizing.reset-size4.size11{font-size:3.11em}.katex .fontsize-ensurer.reset-size5.size1,.katex .sizing.reset-size5.size1{font-size:.55555556em}.katex .fontsize-ensurer.reset-size5.size2,.katex .sizing.reset-size5.size2{font-size:.66666667em}.katex .fontsize-ensurer.reset-size5.size3,.katex .sizing.reset-size5.size3{font-size:.77777778em}.katex .fontsize-ensurer.reset-size5.size4,.katex .sizing.reset-size5.size4{font-size:.88888889em}.katex .fontsize-ensurer.reset-size5.size5,.katex .sizing.reset-size5.size5{font-size:1em}.katex .fontsize-ensurer.reset-size5.size6,.katex .sizing.reset-size5.size6{font-size:1.11111111em}.katex .fontsize-ensurer.reset-size5.size7,.katex .sizing.reset-size5.size7{font-size:1.33333333em}.katex .fontsize-ensurer.reset-size5.size8,.katex .sizing.reset-size5.size8{font-size:1.6em}.katex .fontsize-ensurer.reset-size5.size9,.katex .sizing.reset-size5.size9{font-size:1.92em}.katex .fontsize-ensurer.reset-size5.size10,.katex .sizing.reset-size5.size10{font-size:2.30444444em}.katex .fontsize-ensurer.reset-size5.size11,.katex .sizing.reset-size5.size11{font-size:2.76444444em}.katex .fontsize-ensurer.reset-size6.size1,.katex .sizing.reset-size6.size1{font-size:.5em}.katex .fontsize-ensurer.reset-size6.size2,.katex .sizing.reset-size6.size2{font-size:.6em}.katex .fontsize-ensurer.reset-size6.size3,.katex .sizing.reset-size6.size3{font-size:.7em}.katex .fontsize-ensurer.reset-size6.size4,.katex .sizing.reset-size6.size4{font-size:.8em}.katex .fontsize-ensurer.reset-size6.size5,.katex .sizing.reset-size6.size5{font-size:.9em}.katex .fontsize-ensurer.reset-size6.size6,.katex .sizing.reset-size6.size6{font-size:1em}.katex .fontsize-ensurer.reset-size6.size7,.katex .sizing.reset-size6.size7{font-size:1.2em}.katex .fontsize-ensurer.reset-size6.size8,.katex .sizing.reset-size6.size8{font-size:1.44em}.katex .fontsize-ensurer.reset-size6.size9,.katex .sizing.reset-size6.size9{font-size:1.728em}.katex .fontsize-ensurer.reset-size6.size10,.katex .sizing.reset-size6.size10{font-size:2.074em}.katex .fontsize-ensurer.reset-size6.size11,.katex .sizing.reset-size6.size11{font-size:2.488em}.katex .fontsize-ensurer.reset-size7.size1,.katex .sizing.reset-size7.size1{font-size:.41666667em}.katex .fontsize-ensurer.reset-size7.size2,.katex .sizing.reset-size7.size2{font-size:.5em}.katex .fontsize-ensurer.reset-size7.size3,.katex .sizing.reset-size7.size3{font-size:.58333333em}.katex .fontsize-ensurer.reset-size7.size4,.katex .sizing.reset-size7.size4{font-size:.66666667em}.katex .fontsize-ensurer.reset-size7.size5,.katex .sizing.reset-size7.size5{font-size:.75em}.katex .fontsize-ensurer.reset-size7.size6,.katex .sizing.reset-size7.size6{font-size:.83333333em}.katex .fontsize-ensurer.reset-size7.size7,.katex .sizing.reset-size7.size7{font-size:1em}.katex .fontsize-ensurer.reset-size7.size8,.katex .sizing.reset-size7.size8{font-size:1.2em}.katex .fontsize-ensurer.reset-size7.size9,.katex .sizing.reset-size7.size9{font-size:1.44em}.katex .fontsize-ensurer.reset-size7.size10,.katex .sizing.reset-size7.size10{font-size:1.72833333em}.katex .fontsize-ensurer.reset-size7.size11,.katex .sizing.reset-size7.size11{font-size:2.07333333em}.katex .fontsize-ensurer.reset-size8.size1,.katex .sizing.reset-size8.size1{font-size:.34722222em}.katex .fontsize-ensurer.reset-size8.size2,.katex .sizing.reset-size8.size2{font-size:.41666667em}.katex .fontsize-ensurer.reset-size8.size3,.katex .sizing.reset-size8.size3{font-size:.48611111em}.katex .fontsize-ensurer.reset-size8.size4,.katex .sizing.reset-size8.size4{font-size:.55555556em}.katex .fontsize-ensurer.reset-size8.size5,.katex .sizing.reset-size8.size5{font-size:.625em}.katex .fontsize-ensurer.reset-size8.size6,.katex .sizing.reset-size8.size6{font-size:.69444444em}.katex .fontsize-ensurer.reset-size8.size7,.katex .sizing.reset-size8.size7{font-size:.83333333em}.katex .fontsize-ensurer.reset-size8.size8,.katex .sizing.reset-size8.size8{font-size:1em}.katex .fontsize-ensurer.reset-size8.size9,.katex .sizing.reset-size8.size9{font-size:1.2em}.katex .fontsize-ensurer.reset-size8.size10,.katex .sizing.reset-size8.size10{font-size:1.44027778em}.katex .fontsize-ensurer.reset-size8.size11,.katex .sizing.reset-size8.size11{font-size:1.72777778em}.katex .fontsize-ensurer.reset-size9.size1,.katex .sizing.reset-size9.size1{font-size:.28935185em}.katex .fontsize-ensurer.reset-size9.size2,.katex .sizing.reset-size9.size2{font-size:.34722222em}.katex .fontsize-ensurer.reset-size9.size3,.katex .sizing.reset-size9.size3{font-size:.40509259em}.katex .fontsize-ensurer.reset-size9.size4,.katex .sizing.reset-size9.size4{font-size:.46296296em}.katex .fontsize-ensurer.reset-size9.size5,.katex .sizing.reset-size9.size5{font-size:.52083333em}.katex .fontsize-ensurer.reset-size9.size6,.katex .sizing.reset-size9.size6{font-size:.5787037em}.katex .fontsize-ensurer.reset-size9.size7,.katex .sizing.reset-size9.size7{font-size:.69444444em}.katex .fontsize-ensurer.reset-size9.size8,.katex .sizing.reset-size9.size8{font-size:.83333333em}.katex .fontsize-ensurer.reset-size9.size9,.katex .sizing.reset-size9.size9{font-size:1em}.katex .fontsize-ensurer.reset-size9.size10,.katex .sizing.reset-size9.size10{font-size:1.20023148em}.katex .fontsize-ensurer.reset-size9.size11,.katex .sizing.reset-size9.size11{font-size:1.43981481em}.katex .fontsize-ensurer.reset-size10.size1,.katex .sizing.reset-size10.size1{font-size:.24108004em}.katex .fontsize-ensurer.reset-size10.size2,.katex .sizing.reset-size10.size2{font-size:.28929605em}.katex .fontsize-ensurer.reset-size10.size3,.katex .sizing.reset-size10.size3{font-size:.33751205em}.katex .fontsize-ensurer.reset-size10.size4,.katex .sizing.reset-size10.size4{font-size:.38572806em}.katex .fontsize-ensurer.reset-size10.size5,.katex .sizing.reset-size10.size5{font-size:.43394407em}.katex .fontsize-ensurer.reset-size10.size6,.katex .sizing.reset-size10.size6{font-size:.48216008em}.katex .fontsize-ensurer.reset-size10.size7,.katex .sizing.reset-size10.size7{font-size:.57859209em}.katex .fontsize-ensurer.reset-size10.size8,.katex .sizing.reset-size10.size8{font-size:.69431051em}.katex .fontsize-ensurer.reset-size10.size9,.katex .sizing.reset-size10.size9{font-size:.83317261em}.katex .fontsize-ensurer.reset-size10.size10,.katex .sizing.reset-size10.size10{font-size:1em}.katex .fontsize-ensurer.reset-size10.size11,.katex .sizing.reset-size10.size11{font-size:1.19961427em}.katex .fontsize-ensurer.reset-size11.size1,.katex .sizing.reset-size11.size1{font-size:.20096463em}.katex .fontsize-ensurer.reset-size11.size2,.katex .sizing.reset-size11.size2{font-size:.24115756em}.katex .fontsize-ensurer.reset-size11.size3,.katex .sizing.reset-size11.size3{font-size:.28135048em}.katex .fontsize-ensurer.reset-size11.size4,.katex .sizing.reset-size11.size4{font-size:.32154341em}.katex .fontsize-ensurer.reset-size11.size5,.katex .sizing.reset-size11.size5{font-size:.36173633em}.katex .fontsize-ensurer.reset-size11.size6,.katex .sizing.reset-size11.size6{font-size:.40192926em}.katex .fontsize-ensurer.reset-size11.size7,.katex .sizing.reset-size11.size7{font-size:.48231511em}.katex .fontsize-ensurer.reset-size11.size8,.katex .sizing.reset-size11.size8{font-size:.57877814em}.katex .fontsize-ensurer.reset-size11.size9,.katex .sizing.reset-size11.size9{font-size:.69453376em}.katex .fontsize-ensurer.reset-size11.size10,.katex .sizing.reset-size11.size10{font-size:.83360129em}.katex .fontsize-ensurer.reset-size11.size11,.katex .sizing.reset-size11.size11{font-size:1em}.katex .delimsizing.size1{font-family:KaTeX_Size1}.katex .delimsizing.size2{font-family:KaTeX_Size2}.katex .delimsizing.size3{font-family:KaTeX_Size3}.katex .delimsizing.size4{font-family:KaTeX_Size4}.katex .delimsizing.mult .delim-size1>span{font-family:KaTeX_Size1}.katex .delimsizing.mult .delim-size4>span{font-family:KaTeX_Size4}.katex .nulldelimiter{display:inline-block;width:.12em}.katex .delimcenter,.katex .op-symbol{position:relative}.katex .op-symbol.small-op{font-family:KaTeX_Size1}.katex .op-symbol.large-op{font-family:KaTeX_Size2}.katex .accent>.vlist-t,.katex .op-limits>.vlist-t{text-align:center}.katex .accent .accent-body{position:relative}.katex .accent .accent-body:not(.accent-full){width:0}.katex .overlay{display:block}.katex .mtable .vertical-separator{display:inline-block;min-width:1px}.katex .mtable .arraycolsep{display:inline-block}.katex .mtable .col-align-c>.vlist-t{text-align:center}.katex .mtable .col-align-l>.vlist-t{text-align:left}.katex .mtable .col-align-r>.vlist-t{text-align:right}.katex .svg-align{text-align:left}.katex svg{display:block;position:absolute;width:100%;height:inherit;fill:currentColor;stroke:currentColor;fill-rule:nonzero;fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1}.katex svg path{stroke:none}.katex img{border-style:none;min-width:0;min-height:0;max-width:none;max-height:none}.katex .stretchy{width:100%;display:block;position:relative;overflow:hidden}.katex .stretchy:after,.katex .stretchy:before{content:""}.katex .hide-tail{width:100%;position:relative;overflow:hidden}.katex .halfarrow-left{position:absolute;left:0;width:50.2%;overflow:hidden}.katex .halfarrow-right{position:absolute;right:0;width:50.2%;overflow:hidden}.katex .brace-left{position:absolute;left:0;width:25.1%;overflow:hidden}.katex .brace-center{position:absolute;left:25%;width:50%;overflow:hidden}.katex .brace-right{position:absolute;right:0;width:25.1%;overflow:hidden}.katex .x-arrow-pad{padding:0 .5em}.katex .cd-arrow-pad{padding:0 .55556em 0 .27778em}.katex .mover,.katex .munder,.katex .x-arrow{text-align:center}.katex .boxpad{padding:0 .3em}.katex .fbox,.katex .fcolorbox{box-sizing:border-box;border:.04em solid}.katex .cancel-pad{padding:0 .2em}.katex .cancel-lap{margin-left:-.2em;margin-right:-.2em}.katex .sout{border-bottom-style:solid;border-bottom-width:.08em}.katex .angl{box-sizing:border-content;border-top:.049em solid;border-right:.049em solid;margin-right:.03889em}.katex .anglpad{padding:0 .03889em}.katex .eqn-num:before{counter-increment:katexEqnNo;content:"(" counter(katexEqnNo) ")"}.katex .mml-eqn-num:before{counter-increment:mmlEqnNo;content:"(" counter(mmlEqnNo) ")"}.katex .mtr-glue{width:50%}.katex .cd-vert-arrow{display:inline-block;position:relative}.katex .cd-label-left{display:inline-block;position:absolute;right:calc(50% + .3em);text-align:left}.katex .cd-label-right{display:inline-block;position:absolute;left:calc(50% + .3em);text-align:right}.katex-display{display:block;margin:1em 0;text-align:center}.katex-display>.katex{display:block;text-align:center;white-space:nowrap}.katex-display>.katex>.katex-html{display:block;position:relative}.katex-display>.katex>.katex-html>.tag{position:absolute;right:0}.katex-display.leqno>.katex>.katex-html>.tag{left:0;right:auto}.katex-display.fleqn>.katex{text-align:left;padding-left:2em}body{counter-reset:katexEqnNo mmlEqnNo}
/*---------------------------------------------------------------------------------------------
* Copyright (c) Microsoft Corporation. All rights reserved.
* Licensed under the MIT License. See License.txt in the project root for license information.
*--------------------------------------------------------------------------------------------*/
.katex-error {
color: var(--vscode-editorError-foreground);
}
/* From extension goessner.mdmath */
@font-face{font-family:KaTeX_AMS;font-style:normal;font-weight:400;src:url(fonts/KaTeX_AMS-Regular.woff2) format("woff2"),url(fonts/KaTeX_AMS-Regular.woff) format("woff"),url(fonts/KaTeX_AMS-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Caligraphic;font-style:normal;font-weight:700;src:url(fonts/KaTeX_Caligraphic-Bold.woff2) format("woff2"),url(fonts/KaTeX_Caligraphic-Bold.woff) format("woff"),url(fonts/KaTeX_Caligraphic-Bold.ttf) format("truetype")}@font-face{font-family:KaTeX_Caligraphic;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Caligraphic-Regular.woff2) format("woff2"),url(fonts/KaTeX_Caligraphic-Regular.woff) format("woff"),url(fonts/KaTeX_Caligraphic-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Fraktur;font-style:normal;font-weight:700;src:url(fonts/KaTeX_Fraktur-Bold.woff2) format("woff2"),url(fonts/KaTeX_Fraktur-Bold.woff) format("woff"),url(fonts/KaTeX_Fraktur-Bold.ttf) format("truetype")}@font-face{font-family:KaTeX_Fraktur;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Fraktur-Regular.woff2) format("woff2"),url(fonts/KaTeX_Fraktur-Regular.woff) format("woff"),url(fonts/KaTeX_Fraktur-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Main;font-style:normal;font-weight:700;src:url(fonts/KaTeX_Main-Bold.woff2) format("woff2"),url(fonts/KaTeX_Main-Bold.woff) format("woff"),url(fonts/KaTeX_Main-Bold.ttf) format("truetype")}@font-face{font-family:KaTeX_Main;font-style:italic;font-weight:700;src:url(fonts/KaTeX_Main-BoldItalic.woff2) format("woff2"),url(fonts/KaTeX_Main-BoldItalic.woff) format("woff"),url(fonts/KaTeX_Main-BoldItalic.ttf) format("truetype")}@font-face{font-family:KaTeX_Main;font-style:italic;font-weight:400;src:url(fonts/KaTeX_Main-Italic.woff2) format("woff2"),url(fonts/KaTeX_Main-Italic.woff) format("woff"),url(fonts/KaTeX_Main-Italic.ttf) format("truetype")}@font-face{font-family:KaTeX_Main;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Main-Regular.woff2) format("woff2"),url(fonts/KaTeX_Main-Regular.woff) format("woff"),url(fonts/KaTeX_Main-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Math;font-style:italic;font-weight:700;src:url(fonts/KaTeX_Math-BoldItalic.woff2) format("woff2"),url(fonts/KaTeX_Math-BoldItalic.woff) format("woff"),url(fonts/KaTeX_Math-BoldItalic.ttf) format("truetype")}@font-face{font-family:KaTeX_Math;font-style:italic;font-weight:400;src:url(fonts/KaTeX_Math-Italic.woff2) format("woff2"),url(fonts/KaTeX_Math-Italic.woff) format("woff"),url(fonts/KaTeX_Math-Italic.ttf) format("truetype")}@font-face{font-family:"KaTeX_SansSerif";font-style:normal;font-weight:700;src:url(fonts/KaTeX_SansSerif-Bold.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Bold.woff) format("woff"),url(fonts/KaTeX_SansSerif-Bold.ttf) format("truetype")}@font-face{font-family:"KaTeX_SansSerif";font-style:italic;font-weight:400;src:url(fonts/KaTeX_SansSerif-Italic.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Italic.woff) format("woff"),url(fonts/KaTeX_SansSerif-Italic.ttf) format("truetype")}@font-face{font-family:"KaTeX_SansSerif";font-style:normal;font-weight:400;src:url(fonts/KaTeX_SansSerif-Regular.woff2) format("woff2"),url(fonts/KaTeX_SansSerif-Regular.woff) format("woff"),url(fonts/KaTeX_SansSerif-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Script;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Script-Regular.woff2) format("woff2"),url(fonts/KaTeX_Script-Regular.woff) format("woff"),url(fonts/KaTeX_Script-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Size1;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Size1-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size1-Regular.woff) format("woff"),url(fonts/KaTeX_Size1-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Size2;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Size2-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size2-Regular.woff) format("woff"),url(fonts/KaTeX_Size2-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Size3;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Size3-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size3-Regular.woff) format("woff"),url(fonts/KaTeX_Size3-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Size4;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Size4-Regular.woff2) format("woff2"),url(fonts/KaTeX_Size4-Regular.woff) format("woff"),url(fonts/KaTeX_Size4-Regular.ttf) format("truetype")}@font-face{font-family:KaTeX_Typewriter;font-style:normal;font-weight:400;src:url(fonts/KaTeX_Typewriter-Regular.woff2) format("woff2"),url(fonts/KaTeX_Typewriter-Regular.woff) format("woff"),url(fonts/KaTeX_Typewriter-Regular.ttf) format("truetype")}.katex{font:normal 1.21em KaTeX_Main,Times New Roman,serif;line-height:1.2;text-indent:0;text-rendering:auto}.katex *{-ms-high-contrast-adjust:none!important;border-color:currentColor}.katex .katex-version:after{content:"0.13.11"}.katex .katex-mathml{clip:rect(1px,1px,1px,1px);border:0;height:1px;overflow:hidden;padding:0;position:absolute;width:1px}.katex .katex-html>.newline{display:block}.katex .base{position:relative;white-space:nowrap;width:-webkit-min-content;width:-moz-min-content;width:min-content}.katex .base,.katex .strut{display:inline-block}.katex .textbf{font-weight:700}.katex .textit{font-style:italic}.katex .textrm{font-family:KaTeX_Main}.katex .textsf{font-family:KaTeX_SansSerif}.katex .texttt{font-family:KaTeX_Typewriter}.katex .mathnormal{font-family:KaTeX_Math;font-style:italic}.katex .mathit{font-family:KaTeX_Main;font-style:italic}.katex .mathrm{font-style:normal}.katex .mathbf{font-family:KaTeX_Main;font-weight:700}.katex .boldsymbol{font-family:KaTeX_Math;font-style:italic;font-weight:700}.katex .amsrm,.katex .mathbb,.katex .textbb{font-family:KaTeX_AMS}.katex .mathcal{font-family:KaTeX_Caligraphic}.katex .mathfrak,.katex .textfrak{font-family:KaTeX_Fraktur}.katex .mathtt{font-family:KaTeX_Typewriter}.katex .mathscr,.katex .textscr{font-family:KaTeX_Script}.katex .mathsf,.katex .textsf{font-family:KaTeX_SansSerif}.katex .mathboldsf,.katex .textboldsf{font-family:KaTeX_SansSerif;font-weight:700}.katex .mathitsf,.katex .textitsf{font-family:KaTeX_SansSerif;font-style:italic}.katex .mainrm{font-family:KaTeX_Main;font-style:normal}.katex .vlist-t{border-collapse:collapse;display:inline-table;table-layout:fixed}.katex .vlist-r{display:table-row}.katex .vlist{display:table-cell;position:relative;vertical-align:bottom}.katex .vlist>span{display:block;height:0;position:relative}.katex .vlist>span>span{display:inline-block}.katex .vlist>span>.pstrut{overflow:hidden;width:0}.katex .vlist-t2{margin-right:-2px}.katex .vlist-s{display:table-cell;font-size:1px;min-width:2px;vertical-align:bottom;width:2px}.katex .vbox{-webkit-box-orient:vertical;-webkit-box-direction:normal;-webkit-box-align:baseline;align-items:baseline;display:-webkit-inline-box;display:inline-flex;flex-direction:column}.katex .hbox{width:100%}.katex .hbox,.katex .thinbox{-webkit-box-orient:horizontal;-webkit-box-direction:normal;display:-webkit-inline-box;display:inline-flex;flex-direction:row}.katex .thinbox{max-width:0;width:0}.katex .msupsub{text-align:left}.katex .mfrac>span>span{text-align:center}.katex .mfrac .frac-line{border-bottom-style:solid;display:inline-block;width:100%}.katex .hdashline,.katex .hline,.katex .mfrac .frac-line,.katex .overline .overline-line,.katex .rule,.katex .underline .underline-line{min-height:1px}.katex .mspace{display:inline-block}.katex .clap,.katex .llap,.katex .rlap{position:relative;width:0}.katex .clap>.inner,.katex .llap>.inner,.katex .rlap>.inner{position:absolute}.katex .clap>.fix,.katex .llap>.fix,.katex .rlap>.fix{display:inline-block}.katex .llap>.inner{right:0}.katex .clap>.inner,.katex .rlap>.inner{left:0}.katex .clap>.inner>span{margin-left:-50%;margin-right:50%}.katex .rule{border:0 solid;display:inline-block;position:relative}.katex .hline,.katex .overline .overline-line,.katex .underline .underline-line{border-bottom-style:solid;display:inline-block;width:100%}.katex .hdashline{border-bottom-style:dashed;display:inline-block;width:100%}.katex .sqrt>.root{margin-left:.27777778em;margin-right:-.55555556em}.katex .fontsize-ensurer.reset-size1.size1,.katex .sizing.reset-size1.size1{font-size:1em}.katex .fontsize-ensurer.reset-size1.size2,.katex .sizing.reset-size1.size2{font-size:1.2em}.katex .fontsize-ensurer.reset-size1.size3,.katex .sizing.reset-size1.size3{font-size:1.4em}.katex .fontsize-ensurer.reset-size1.size4,.katex .sizing.reset-size1.size4{font-size:1.6em}.katex .fontsize-ensurer.reset-size1.size5,.katex .sizing.reset-size1.size5{font-size:1.8em}.katex .fontsize-ensurer.reset-size1.size6,.katex .sizing.reset-size1.size6{font-size:2em}.katex .fontsize-ensurer.reset-size1.size7,.katex .sizing.reset-size1.size7{font-size:2.4em}.katex .fontsize-ensurer.reset-size1.size8,.katex .sizing.reset-size1.size8{font-size:2.88em}.katex .fontsize-ensurer.reset-size1.size9,.katex .sizing.reset-size1.size9{font-size:3.456em}.katex .fontsize-ensurer.reset-size1.size10,.katex .sizing.reset-size1.size10{font-size:4.148em}.katex .fontsize-ensurer.reset-size1.size11,.katex .sizing.reset-size1.size11{font-size:4.976em}.katex .fontsize-ensurer.reset-size2.size1,.katex .sizing.reset-size2.size1{font-size:.83333333em}.katex .fontsize-ensurer.reset-size2.size2,.katex .sizing.reset-size2.size2{font-size:1em}.katex .fontsize-ensurer.reset-size2.size3,.katex .sizing.reset-size2.size3{font-size:1.16666667em}.katex .fontsize-ensurer.reset-size2.size4,.katex .sizing.reset-size2.size4{font-size:1.33333333em}.katex .fontsize-ensurer.reset-size2.size5,.katex .sizing.reset-size2.size5{font-size:1.5em}.katex .fontsize-ensurer.reset-size2.size6,.katex .sizing.reset-size2.size6{font-size:1.66666667em}.katex .fontsize-ensurer.reset-size2.size7,.katex .sizing.reset-size2.size7{font-size:2em}.katex .fontsize-ensurer.reset-size2.size8,.katex .sizing.reset-size2.size8{font-size:2.4em}.katex .fontsize-ensurer.reset-size2.size9,.katex .sizing.reset-size2.size9{font-size:2.88em}.katex .fontsize-ensurer.reset-size2.size10,.katex .sizing.reset-size2.size10{font-size:3.45666667em}.katex .fontsize-ensurer.reset-size2.size11,.katex .sizing.reset-size2.size11{font-size:4.14666667em}.katex .fontsize-ensurer.reset-size3.size1,.katex .sizing.reset-size3.size1{font-size:.71428571em}.katex .fontsize-ensurer.reset-size3.size2,.katex .sizing.reset-size3.size2{font-size:.85714286em}.katex .fontsize-ensurer.reset-size3.size3,.katex .sizing.reset-size3.size3{font-size:1em}.katex .fontsize-ensurer.reset-size3.size4,.katex .sizing.reset-size3.size4{font-size:1.14285714em}.katex .fontsize-ensurer.reset-size3.size5,.katex .sizing.reset-size3.size5{font-size:1.28571429em}.katex .fontsize-ensurer.reset-size3.size6,.katex .sizing.reset-size3.size6{font-size:1.42857143em}.katex .fontsize-ensurer.reset-size3.size7,.katex .sizing.reset-size3.size7{font-size:1.71428571em}.katex .fontsize-ensurer.reset-size3.size8,.katex .sizing.reset-size3.size8{font-size:2.05714286em}.katex .fontsize-ensurer.reset-size3.size9,.katex .sizing.reset-size3.size9{font-size:2.46857143em}.katex .fontsize-ensurer.reset-size3.size10,.katex .sizing.reset-size3.size10{font-size:2.96285714em}.katex .fontsize-ensurer.reset-size3.size11,.katex .sizing.reset-size3.size11{font-size:3.55428571em}.katex .fontsize-ensurer.reset-size4.size1,.katex .sizing.reset-size4.size1{font-size:.625em}.katex .fontsize-ensurer.reset-size4.size2,.katex .sizing.reset-size4.size2{font-size:.75em}.katex .fontsize-ensurer.reset-size4.size3,.katex .sizing.reset-size4.size3{font-size:.875em}.katex .fontsize-ensurer.reset-size4.size4,.katex .sizing.reset-size4.size4{font-size:1em}.katex .fontsize-ensurer.reset-size4.size5,.katex .sizing.reset-size4.size5{font-size:1.125em}.katex .fontsize-ensurer.reset-size4.size6,.katex .sizing.reset-size4.size6{font-size:1.25em}.katex .fontsize-ensurer.reset-size4.size7,.katex .sizing.reset-size4.size7{font-size:1.5em}.katex .fontsize-ensurer.reset-size4.size8,.katex .sizing.reset-size4.size8{font-size:1.8em}.katex .fontsize-ensurer.reset-size4.size9,.katex .sizing.reset-size4.size9{font-size:2.16em}.katex .fontsize-ensurer.reset-size4.size10,.katex .sizing.reset-size4.size10{font-size:2.5925em}.katex .fontsize-ensurer.reset-size4.size11,.katex .sizing.reset-size4.size11{font-size:3.11em}.katex .fontsize-ensurer.reset-size5.size1,.katex .sizing.reset-size5.size1{font-size:.55555556em}.katex .fontsize-ensurer.reset-size5.size2,.katex .sizing.reset-size5.size2{font-size:.66666667em}.katex .fontsize-ensurer.reset-size5.size3,.katex .sizing.reset-size5.size3{font-size:.77777778em}.katex .fontsize-ensurer.reset-size5.size4,.katex .sizing.reset-size5.size4{font-size:.88888889em}.katex .fontsize-ensurer.reset-size5.size5,.katex .sizing.reset-size5.size5{font-size:1em}.katex .fontsize-ensurer.reset-size5.size6,.katex .sizing.reset-size5.size6{font-size:1.11111111em}.katex .fontsize-ensurer.reset-size5.size7,.katex .sizing.reset-size5.size7{font-size:1.33333333em}.katex .fontsize-ensurer.reset-size5.size8,.katex .sizing.reset-size5.size8{font-size:1.6em}.katex .fontsize-ensurer.reset-size5.size9,.katex .sizing.reset-size5.size9{font-size:1.92em}.katex .fontsize-ensurer.reset-size5.size10,.katex .sizing.reset-size5.size10{font-size:2.30444444em}.katex .fontsize-ensurer.reset-size5.size11,.katex .sizing.reset-size5.size11{font-size:2.76444444em}.katex .fontsize-ensurer.reset-size6.size1,.katex .sizing.reset-size6.size1{font-size:.5em}.katex .fontsize-ensurer.reset-size6.size2,.katex .sizing.reset-size6.size2{font-size:.6em}.katex .fontsize-ensurer.reset-size6.size3,.katex .sizing.reset-size6.size3{font-size:.7em}.katex .fontsize-ensurer.reset-size6.size4,.katex .sizing.reset-size6.size4{font-size:.8em}.katex .fontsize-ensurer.reset-size6.size5,.katex .sizing.reset-size6.size5{font-size:.9em}.katex .fontsize-ensurer.reset-size6.size6,.katex .sizing.reset-size6.size6{font-size:1em}.katex .fontsize-ensurer.reset-size6.size7,.katex .sizing.reset-size6.size7{font-size:1.2em}.katex .fontsize-ensurer.reset-size6.size8,.katex .sizing.reset-size6.size8{font-size:1.44em}.katex .fontsize-ensurer.reset-size6.size9,.katex .sizing.reset-size6.size9{font-size:1.728em}.katex .fontsize-ensurer.reset-size6.size10,.katex .sizing.reset-size6.size10{font-size:2.074em}.katex .fontsize-ensurer.reset-size6.size11,.katex .sizing.reset-size6.size11{font-size:2.488em}.katex .fontsize-ensurer.reset-size7.size1,.katex .sizing.reset-size7.size1{font-size:.41666667em}.katex .fontsize-ensurer.reset-size7.size2,.katex .sizing.reset-size7.size2{font-size:.5em}.katex .fontsize-ensurer.reset-size7.size3,.katex .sizing.reset-size7.size3{font-size:.58333333em}.katex .fontsize-ensurer.reset-size7.size4,.katex .sizing.reset-size7.size4{font-size:.66666667em}.katex .fontsize-ensurer.reset-size7.size5,.katex .sizing.reset-size7.size5{font-size:.75em}.katex .fontsize-ensurer.reset-size7.size6,.katex .sizing.reset-size7.size6{font-size:.83333333em}.katex .fontsize-ensurer.reset-size7.size7,.katex .sizing.reset-size7.size7{font-size:1em}.katex .fontsize-ensurer.reset-size7.size8,.katex .sizing.reset-size7.size8{font-size:1.2em}.katex .fontsize-ensurer.reset-size7.size9,.katex .sizing.reset-size7.size9{font-size:1.44em}.katex .fontsize-ensurer.reset-size7.size10,.katex .sizing.reset-size7.size10{font-size:1.72833333em}.katex .fontsize-ensurer.reset-size7.size11,.katex .sizing.reset-size7.size11{font-size:2.07333333em}.katex .fontsize-ensurer.reset-size8.size1,.katex .sizing.reset-size8.size1{font-size:.34722222em}.katex .fontsize-ensurer.reset-size8.size2,.katex .sizing.reset-size8.size2{font-size:.41666667em}.katex .fontsize-ensurer.reset-size8.size3,.katex .sizing.reset-size8.size3{font-size:.48611111em}.katex .fontsize-ensurer.reset-size8.size4,.katex .sizing.reset-size8.size4{font-size:.55555556em}.katex .fontsize-ensurer.reset-size8.size5,.katex .sizing.reset-size8.size5{font-size:.625em}.katex .fontsize-ensurer.reset-size8.size6,.katex .sizing.reset-size8.size6{font-size:.69444444em}.katex .fontsize-ensurer.reset-size8.size7,.katex .sizing.reset-size8.size7{font-size:.83333333em}.katex .fontsize-ensurer.reset-size8.size8,.katex .sizing.reset-size8.size8{font-size:1em}.katex .fontsize-ensurer.reset-size8.size9,.katex .sizing.reset-size8.size9{font-size:1.2em}.katex .fontsize-ensurer.reset-size8.size10,.katex .sizing.reset-size8.size10{font-size:1.44027778em}.katex .fontsize-ensurer.reset-size8.size11,.katex .sizing.reset-size8.size11{font-size:1.72777778em}.katex .fontsize-ensurer.reset-size9.size1,.katex .sizing.reset-size9.size1{font-size:.28935185em}.katex .fontsize-ensurer.reset-size9.size2,.katex .sizing.reset-size9.size2{font-size:.34722222em}.katex .fontsize-ensurer.reset-size9.size3,.katex .sizing.reset-size9.size3{font-size:.40509259em}.katex .fontsize-ensurer.reset-size9.size4,.katex .sizing.reset-size9.size4{font-size:.46296296em}.katex .fontsize-ensurer.reset-size9.size5,.katex .sizing.reset-size9.size5{font-size:.52083333em}.katex .fontsize-ensurer.reset-size9.size6,.katex .sizing.reset-size9.size6{font-size:.5787037em}.katex .fontsize-ensurer.reset-size9.size7,.katex .sizing.reset-size9.size7{font-size:.69444444em}.katex .fontsize-ensurer.reset-size9.size8,.katex .sizing.reset-size9.size8{font-size:.83333333em}.katex .fontsize-ensurer.reset-size9.size9,.katex .sizing.reset-size9.size9{font-size:1em}.katex .fontsize-ensurer.reset-size9.size10,.katex .sizing.reset-size9.size10{font-size:1.20023148em}.katex .fontsize-ensurer.reset-size9.size11,.katex .sizing.reset-size9.size11{font-size:1.43981481em}.katex .fontsize-ensurer.reset-size10.size1,.katex .sizing.reset-size10.size1{font-size:.24108004em}.katex .fontsize-ensurer.reset-size10.size2,.katex .sizing.reset-size10.size2{font-size:.28929605em}.katex .fontsize-ensurer.reset-size10.size3,.katex .sizing.reset-size10.size3{font-size:.33751205em}.katex .fontsize-ensurer.reset-size10.size4,.katex .sizing.reset-size10.size4{font-size:.38572806em}.katex .fontsize-ensurer.reset-size10.size5,.katex .sizing.reset-size10.size5{font-size:.43394407em}.katex .fontsize-ensurer.reset-size10.size6,.katex .sizing.reset-size10.size6{font-size:.48216008em}.katex .fontsize-ensurer.reset-size10.size7,.katex .sizing.reset-size10.size7{font-size:.57859209em}.katex .fontsize-ensurer.reset-size10.size8,.katex .sizing.reset-size10.size8{font-size:.69431051em}.katex .fontsize-ensurer.reset-size10.size9,.katex .sizing.reset-size10.size9{font-size:.83317261em}.katex .fontsize-ensurer.reset-size10.size10,.katex .sizing.reset-size10.size10{font-size:1em}.katex .fontsize-ensurer.reset-size10.size11,.katex .sizing.reset-size10.size11{font-size:1.19961427em}.katex .fontsize-ensurer.reset-size11.size1,.katex .sizing.reset-size11.size1{font-size:.20096463em}.katex .fontsize-ensurer.reset-size11.size2,.katex .sizing.reset-size11.size2{font-size:.24115756em}.katex .fontsize-ensurer.reset-size11.size3,.katex .sizing.reset-size11.size3{font-size:.28135048em}.katex .fontsize-ensurer.reset-size11.size4,.katex .sizing.reset-size11.size4{font-size:.32154341em}.katex .fontsize-ensurer.reset-size11.size5,.katex .sizing.reset-size11.size5{font-size:.36173633em}.katex .fontsize-ensurer.reset-size11.size6,.katex .sizing.reset-size11.size6{font-size:.40192926em}.katex .fontsize-ensurer.reset-size11.size7,.katex .sizing.reset-size11.size7{font-size:.48231511em}.katex .fontsize-ensurer.reset-size11.size8,.katex .sizing.reset-size11.size8{font-size:.57877814em}.katex .fontsize-ensurer.reset-size11.size9,.katex .sizing.reset-size11.size9{font-size:.69453376em}.katex .fontsize-ensurer.reset-size11.size10,.katex .sizing.reset-size11.size10{font-size:.83360129em}.katex .fontsize-ensurer.reset-size11.size11,.katex .sizing.reset-size11.size11{font-size:1em}.katex .delimsizing.size1{font-family:KaTeX_Size1}.katex .delimsizing.size2{font-family:KaTeX_Size2}.katex .delimsizing.size3{font-family:KaTeX_Size3}.katex .delimsizing.size4{font-family:KaTeX_Size4}.katex .delimsizing.mult .delim-size1>span{font-family:KaTeX_Size1}.katex .delimsizing.mult .delim-size4>span{font-family:KaTeX_Size4}.katex .nulldelimiter{display:inline-block;width:.12em}.katex .delimcenter,.katex .op-symbol{position:relative}.katex .op-symbol.small-op{font-family:KaTeX_Size1}.katex .op-symbol.large-op{font-family:KaTeX_Size2}.katex .accent>.vlist-t,.katex .op-limits>.vlist-t{text-align:center}.katex .accent .accent-body{position:relative}.katex .accent .accent-body:not(.accent-full){width:0}.katex .overlay{display:block}.katex .mtable .vertical-separator{display:inline-block;min-width:1px}.katex .mtable .arraycolsep{display:inline-block}.katex .mtable .col-align-c>.vlist-t{text-align:center}.katex .mtable .col-align-l>.vlist-t{text-align:left}.katex .mtable .col-align-r>.vlist-t{text-align:right}.katex .svg-align{text-align:left}.katex svg{fill:currentColor;stroke:currentColor;fill-rule:nonzero;fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1;display:block;height:inherit;position:absolute;width:100%}.katex svg path{stroke:none}.katex img{border-style:none;max-height:none;max-width:none;min-height:0;min-width:0}.katex .stretchy{display:block;overflow:hidden;position:relative;width:100%}.katex .stretchy:after,.katex .stretchy:before{content:""}.katex .hide-tail{overflow:hidden;position:relative;width:100%}.katex .halfarrow-left{left:0;overflow:hidden;position:absolute;width:50.2%}.katex .halfarrow-right{overflow:hidden;position:absolute;right:0;width:50.2%}.katex .brace-left{left:0;overflow:hidden;position:absolute;width:25.1%}.katex .brace-center{left:25%;overflow:hidden;position:absolute;width:50%}.katex .brace-right{overflow:hidden;position:absolute;right:0;width:25.1%}.katex .x-arrow-pad{padding:0 .5em}.katex .cd-arrow-pad{padding:0 .55556em 0 .27778em}.katex .mover,.katex .munder,.katex .x-arrow{text-align:center}.katex .boxpad{padding:0 .3em}.katex .fbox,.katex .fcolorbox{border:.04em solid;box-sizing:border-box}.katex .cancel-pad{padding:0 .2em}.katex .cancel-lap{margin-left:-.2em;margin-right:-.2em}.katex .sout{border-bottom-style:solid;border-bottom-width:.08em}.katex .angl{border-right:.049em solid;border-top:.049em solid;box-sizing:border-content;margin-right:.03889em}.katex .anglpad{padding:0 .03889em}.katex .eqn-num:before{content:"(" counter(katexEqnNo) ")";counter-increment:katexEqnNo}.katex .mml-eqn-num:before{content:"(" counter(mmlEqnNo) ")";counter-increment:mmlEqnNo}.katex .mtr-glue{width:50%}.katex .cd-vert-arrow{display:inline-block;position:relative}.katex .cd-label-left{display:inline-block;position:absolute;right:-webkit-calc(50% + .3em);right:calc(50% + .3em);text-align:left}.katex .cd-label-right{display:inline-block;left:-webkit-calc(50% + .3em);left:calc(50% + .3em);position:absolute;text-align:right}.katex-display{display:block;margin:1em 0;text-align:center}.katex-display>.katex{display:block;text-align:center;white-space:nowrap}.katex-display>.katex>.katex-html{display:block;position:relative}.katex-display>.katex>.katex-html>.tag{position:absolute;right:0}.katex-display.leqno>.katex>.katex-html>.tag{left:0;right:auto}.katex-display.fleqn>.katex{padding-left:2em;text-align:left}body{counter-reset:katexEqnNo mmlEqnNo}
/* style for html inside of browsers */
.katex { font-size: 1em !important; } /* align KaTeX font-size to surrounding text */
eq { display: inline-block; }
eqn { display: block}
section.eqno {
display: flex;
flex-direction: row;
align-content: space-between;
align-items: center;
}
section.eqno > eqn {
width: 100%;
margin-left: 3em;
}
section.eqno > span {
width:3em;
text-align:right;
}
p {
text-align: justify;
hyphens: auto;
}
table {
display: table;
width: auto;
margin-left: auto;
margin-right: auto;
margin-bottom: 1em;
border-collapse: collapse;
}
table th, table td {
border-left: none;
border-right: none;
border-top: 1px solid #000;
border-bottom: 1px solid #000;
}
figure {
margin: 0.5em auto;
}
figure > img {
display: block;
margin: 0 auto;
page-break-inside: avoid;
text-align: center;
}
figcaption {
font-size: 0.9em;
margin-top: 0.5em;
text-align: center;
}
aside {
font-size: 0.9em;
max-width: 300px;
padding: 0 0 0 1em;
margin: 0 0 0 1em;
float: right;
}
aside > *:first-child {
margin-top: 0;
}
aside > *:last-child {
margin-bottom: 0;
}
</style>
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.10.2/dist/katex.min.css" integrity="sha384-yFRtMMDnQtDRO8rLpMIKrtPCD5jdktao2TV19YiZYWMDkUR5GQZR/NOVTdquEx1j" crossorigin="anonymous">
<link href="https://cdn.jsdelivr.net/npm/katex-copytex@latest/dist/katex-copytex.min.css" rel="stylesheet" type="text/css">
<link rel="stylesheet" href="https://cdn.jsdelivr.net/gh/Microsoft/vscode/extensions/markdown-language-features/media/markdown.css">
<link rel="stylesheet" href="https://cdn.jsdelivr.net/gh/Microsoft/vscode/extensions/markdown-language-features/media/highlight.css">
<style>
body {
font-family: -apple-system, BlinkMacSystemFont, 'Segoe WPC', 'Segoe UI', system-ui, 'Ubuntu', 'Droid Sans', sans-serif;
font-size: 14px;
line-height: 1.6;
}
</style>
<style>
.task-list-item { list-style-type: none; } .task-list-item-checkbox { margin-left: -20px; vertical-align: middle; }
</style>
<script src="https://cdn.jsdelivr.net/npm/katex-copytex@latest/dist/katex-copytex.min.js"></script>
</head>
<body class="vscode-body vscode-light">
<h1 id="fair-termination-of-binary-sessions---artifact">Fair Termination of Binary Sessions - Artifact</h1>
<p><code>FairCheck</code> is an implementation of the type system described in the paper
<a href="https://doi.org/10.1145/3498666"><em>Fair Termination of Binary Sessions</em></a> in the
proceedings of POPL 2022. A draft of the paper that also includes the
algorithmic version of the type system on which <code>FairCheck</code> is based is
<a href="paper/fair-termination.pdf">available here</a>. <code>FairCheck</code> parses a distributed
program modeled in a session-oriented variant of the π-calculus and verifies
that:</p>
<ol>
<li>There exists a <strong>typing derivation</strong> for each definition in the program using
the algorithmic version of the type system (Section 6 and Appendix F.1).</li>
<li>Each process definition is <strong>action bounded</strong>, namely there exists a finite
branch leading to termination (Section 5.1).</li>
<li>Each process definition is <strong>session bounded</strong>, namely the number of sessions
the process needs to create in order to terminate is bounded (Section 5.2).</li>
<li>Each process definition is <strong>cast bounded</strong>, namely the number of casts the
process needs to perform in order to terminate is bounded (Section 5.3).</li>
</ol>
<h2 id="list-of-claims-in-the-paper">List of claims in the paper</h2>
<p>Here is a list of claims made in the paper about the well- or ill-typing of the
key examples presented in the paper. Each claim will be discussed and checked
against the implementation of <code>FairCheck</code> in the corresponding section below.</p>
<ol>
<li><a href="#claim-1">The <em>acquirer-business-carrier</em> program in Example 4.1 is well typed
(Example 6.1)</a></li>
<li><a href="#claim-2">The <em>random bit generator</em> program is well typed (Example 6.3)</a></li>
<li><a href="#claim-3">In Eq. (3), the process <code>A</code> is action bounded and <code>B</code> is not (Section
5.1)</a></li>
<li><a href="#claim-4">At the end of Section 5.1, <code>A</code> is ill typed and <code>B</code> would be well typed if
action boundedness was not enforced</a></li>
<li><a href="#claim-5">In Eq. (4) and Eq. (5), <code>A</code> is session bounded whereas <code>B₁</code> and <code>B₂</code> are not
(Section 5.2)</a></li>
<li><a href="#claim-7">The process <code>C</code> in Eq. (6) is well typed (Section 5.2)</a></li>
<li><a href="#claim-7">The program in Eq. (7) would be well typed if action boundedness and cast
boundedness were not enforced (Section 5.3)</a></li>
<li><a href="#claim-8">The same program using the definitions in Eq. (8) would be well typed if cast
boundedness was not enforced (Section 5.3)</a></li>
<li><a href="#claim-9">The program in Eq. (9) is ill typed because it uses unfair subtyping
(Section 5.3)</a></li>
</ol>
<h2 id="download-installation-and-sanity-testing">Download, installation, and sanity-testing</h2>
<p>The artifact is <a href="https://github.com/boystrange/FairCheck">available on GitHub</a>
as well as on the ACM Digital Library as a source code archive associated with
the paper. The next sub-sections describe the steps to be taken to compile and
test the artifact in each case.</p>
<p>These instructions assume the use of MacOS with the <a href="https://brew.sh"><code>homebrew</code> package
manager</a> and a terminal running the <code>bash</code> shell. First of all,
make sure that the Haskell compiler and the Haskell Tool Stack are installed. If
not, issuing the commands</p>
<pre><code class="language-bash"><div>brew install haskell-stack
</div></code></pre>
<p>will install these tools. After cloning the GitHub repository or unpacking the
<code>.zip</code> archive downloaded from the ACM Digital Library, enter the directory of
the tool, for example with</p>
<pre><code class="language-bash"><div><span class="hljs-built_in">cd</span> FairCheck
</div></code></pre>
<p>At the time this document is being written, support for the Haskell compiler and
the Haskell Tool Stack on M1 Macs is not completely aligned with that of other
architectures. In particular, it may be necessary to use a different
configuration file for the Haskell Tool Stack to compile the artifact on an M1
Mac. To this aim, in addition to the installation instructions above, install
the Haskell compiler globally with the command</p>
<pre><code class="language-bash"><div>brew install ghc
</div></code></pre>
<p>then edit the <a href="Makefile"><code>Makefile</code></a> and change the topmost line</p>
<pre><code class="language-make"><code><div>YAML = stack.yaml
</div></code></code></pre>
<p>to</p>
<pre><code class="language-make"><code><div>YAML = stack_m1.yaml
</div></code></code></pre>
<p>To clean up all the auxiliary files produced by the compiler, to (re)generate
and install the <code>FairCheck</code> executable, issue the command</p>
<pre><code class="language-bash"><div>make clean && make && make install
</div></code></pre>
<p>The compilation should just take a few seconds to complete. To verify that the
<code>FairCheck</code> executable has been built and installed successfully, issue the
command</p>
<pre><code class="language-bash"><div>faircheck
</div></code></pre>
<p>to print the synopsis of <code>FairCheck</code> and a summary of the options it accepts. We
will illustrate the effect of some of these options in the next section. Note
that the executable is installed into a hidden local directory <code>~/.local/bin</code>
that is already included in the <code>PATH</code> variable for the terminal shell in the
virtual image. In case <code>FairCheck</code> is compiled from the <code>.zip</code> archive, it may
be necessary to add the installation directory of the <code>stack</code> tool to the <code>PATH</code>
environment variable (run <code>stack path --local-bin</code> to obtain the full path of
this directory).</p>
<p><code>FairCheck</code> includes a few examples of well- and ill-typed processes. To verify
that they are correctly classified as such, issue the command</p>
<pre><code class="language-bash"><div>make check
</div></code></pre>
<p>to print the list of programs being analyzed along with the result of the
analysis: a green <code>OK</code> followed by the time taken by type checking indicates
that the program is well typed; a red <code>NO</code> followed by an error message
indicates that the program is ill typed. Depending on the size of the terminal
window, it may be necessary to scroll the window up to see the whole list of
analyzed programs, divided into those that are well typed and those that are
not.</p>
<h2 id="evaluation-instructions">Evaluation instructions</h2>
<h3 id="claim-1">Claim 1</h3>
<p>The running example used throughout the paper models an
<em>acquirer-business-carrier</em> distributed program and is described in Example 4.1.
Its specification in the syntax accepted by <code>FairCheck</code> is contained in the
script <a href="artifact/acquirer_business_carrier.pi"><code>acquirer_business_carrier.pi</code></a>
and is shown below.</p>
<pre><code class="language-pi"><code><div>type T = !add.(!add.T ⊕ !pay.!end)
type S = ?add.S + ?pay.?end
type R = !add.R ⊕ !pay.!end
A(x : T) = x!add.x!{add: A⟨x⟩, pay: close x}
B(x : S, y : !ship.!end) = x?{add: B⟨x, y⟩, pay: wait x.y!ship.close y}
C(y : ?ship.?end) = y?ship.wait y.done
Main = new (y : !ship.!end)
new (x : R) ⌈x : T⌉ A⟨x⟩ in B⟨x, y⟩
in C⟨y⟩
</div></code></code></pre>
<p>The script begins with three <strong>session type declarations</strong> defining the acquirer
protocol <code>T</code>, the business protocol <code>S</code> and the dual of the business protocol
<code>R</code>. Next are the process definitions corresponding to those of Example 4.1.
Note that <code>FairCheck</code> implements a type checker, not a type reconstruction
algorithm. Hence, <strong>bound names</strong> and <strong>casts</strong> must be <strong>explicitly annotated</strong>
with session types. For example, the declarations <code>x : T</code> in the definition of
<code>A</code> and <code>y : !ship.!end</code> in the definition of <code>B</code> state that <code>x</code> and <code>y</code> have
type <code>T</code> and <code>!ship.!end</code> respectively, in agreement with the global type
assignments given in Example 6.1. Also, for the sake of readability, <strong>session
restrictions</strong> <code>(x)(P | Q)</code> are denoted by the form <code>new (x : S) P in Q</code>. Only
the type <code>S</code> of the session endpoint used by <code>P</code> must be provided, whereas the
endpoint used by <code>Q</code> is implicitly associated with the dual of <code>S</code>.</p>
<p>Example 6.1 claims that this program is well typed. To verify the claim we run
<code>FairCheck</code> specifying the file that contains the program to type check.
Hereafter, <code>$</code> represents the shell prompt and preceeds the command being
issued, whereas any text in the subsequent lines is the output produced by
<code>FairCheck</code>.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/acquirer_business_carrier.pi
OK
</div></code></pre>
<p>The <code>OK</code> output indicates that the program is well typed.</p>
<h3 id="claim-2">Claim 2</h3>
<p>The <em>random bit generator</em> program described in Example 6.3 is defined in the
script <a href="artifact/random_bit_generator.pi"><code>random_bit_generator.pi</code></a> and is
shown below (in the submitted version of the paper, the <code>B</code> process also uses a
session endpoint <code>y</code> which is omitted in the script so that the program is self
contained).</p>
<pre><code class="language-pi"><code><div>type S = ?more.(!0.S ⊕ !1.S) + ?stop.!end
type U = !more.(?0.U + ?1.!stop.?end)
type V = ?more.(!0.V ⊕ !1.?stop.!end)
A(x : S) = x?{more: x!{0: A⟨x⟩, 1: A⟨x⟩}, stop: close x}
B(x : U) = x!more.x?{0: B⟨x⟩, 1: x!stop.wait x.done}
Main = new (x : V) ⌈x : S⌉ A⟨x⟩ in B⟨x⟩
</div></code></code></pre>
<p>Example 6.3 claims that this program is well typed.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/random_bit_generator.pi
OK
</div></code></pre>
<h3 id="claim-3">Claim 3</h3>
<p>The purpose of the definitions in Eq. (3) is to illustrate the difference
between <strong>action-bounded</strong> processes, which have a finite branch leading to
termination, and <strong>action-unbounded</strong> processes, which have no such branch. The
process <code>A</code> in Eq. (3) is defined in the script
<a href="artifact/equation_3_A.pi"><code>equation_3_A.pi</code></a>.</p>
<pre><code class="language-pi"><code><div>A = A ⊕ done
</div></code></code></pre>
<p>This process may nondeterministically reduce to itself or to <code>done</code> and is
claimed to be action bounded thanks to the branch leading to <code>done</code>. In fact, it
is well typed.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/equation_3_A.pi
OK
</div></code></pre>
<p>The process <code>B</code> in the same Eq. (3) is defined in the script
<a href="artifact/equation_3_B.pi"><code>equation_3_B.pi</code></a>.</p>
<pre><code class="language-pi"><code><div>B = B ⊕ B
</div></code></code></pre>
<p>This process can only reduce to itself and is claimed to be action unbounded,
because it has no branch leading to termination.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/equation_3_B.pi
NO: action-unbounded process: B [line 1]
</div></code></pre>
<p>The <code>NO</code> output indicates that the program is ill typed and the subsequent
message provides details about (one of) the errors that have been found. In this
case, the error confirms that <code>B</code> is action unbounded.</p>
<h3 id="claim-4">Claim 4</h3>
<p>The purpose of the process definitions at the end of Section 5.1 is to
illustrate how action boundedness helps detecting programs that claim to use
certain session endpoints in a certain way, while in fact they never do so. To
illustrate this situation, consider the process <code>B</code> shown at the end of Section
5.1 and defined in the script
<a href="artifact/linearity_violation_B.pi"><code>linearity_violation_B.pi</code></a>.</p>
<pre><code class="language-pi"><code><div>type T = !a.T
B(x : T, y : !end) = x!a.B⟨x, y⟩
</div></code></code></pre>
<p>This process claims to use <code>x</code> according to <code>T</code> and <code>y</code> according to <code>!end</code>.
While <code>x</code> is indeed <strong>used</strong> as specified by <code>T</code>, <code>y</code> is only passed as an
argument in the recursive invocation of <code>B</code> so that the linearity of <code>y</code> is not
violated. As claimed in the paper, a process like <code>B</code> is not action bounded and
is therefore ruled out by the type system.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/linearity_violation_B.pi
NO: action-unbounded process: B [line 3]
</div></code></pre>
<p>A conventional session type system that does not enforce action boundedness may
be unable to realize that <code>y</code> is not actually used by <code>B</code>. We can verify this
claim by passing the <code>-a</code> option to <code>FairCheck</code>, which disables the enforcement
of action boundedness.</p>
<pre><code class="language-bash"><div>$ faircheck -a artifact/linearity_violation_B.pi
OK
</div></code></pre>
<p>In conclusion, without the requirement of action boundedness the process <code>B</code>
would be well typed, despite the fact that it never really uses <code>y</code>.</p>
<p>The process <code>A</code>, also defined at the end of Section 5.1 and contained in the
script <a href="artifact/linearity_violation_A.pi"><code>linearity_violation_A.pi</code></a>, is a
simple variation of <code>B</code> that is action bounded.</p>
<pre><code class="language-pi"><code><div>type S = !a.S ⊕ !b.!end
A(x : S, y : !end) = x!{a: A⟨x, y⟩, b: close x}
</div></code></code></pre>
<p>Just like <code>B</code>, also <code>A</code> declares that <code>y</code> is used according to the session type
<code>!end</code>. This process is claimed to be ill typed because the <code>b</code>-labeled branch
of the label output form does not actually use <code>y</code>.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/linearity_violation_A.pi
NO: linearity violation: y [line 3]
</div></code></pre>
<h3 id="claim-5">Claim 5</h3>
<p>The process definitions in Eq. (4) and Eq. (5) illustrate the difference between
<strong>session-bounded</strong> and <strong>session-unbounded</strong> processes. In a session-bounded
process, there is an upper bound to the number of sessions the process needs to
create in order to terminate.</p>
<p>The script <a href="artifact/equation_4_A.pi"><code>equation_4_A.pi</code></a> contains the process
<code>A</code> in Eq. (4).</p>
<pre><code class="language-pi"><code><div>A = (new (x : !end) close x in wait x.A) ⊕ done
</div></code></code></pre>
<p>The process is claimed to be session bounded, because it does not need to create
any new session in order to terminate despite the fact that it <em>may</em> create a
new session at each invocation. In fact, the program is well typed.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/equation_4_A.pi
OK
</div></code></pre>
<p>The file <a href="artifact/equation_4_B.pi"><code>equation_4_B.pi</code></a> contains the definition
of the process <code>B₁</code> in Eq. (4).</p>
<pre><code class="language-pi"><code><div>B₁ = new (x : !end) close x in wait x.B₁
</div></code></code></pre>
<p>This process is claimed to be session unbounded. Since this process is also
action unbounded and <code>FairCheck</code> verifies action boundedness <em>before</em> session
boundedness, we need to use the <code>-a</code> option to disable action boundedness
checking or else we would not be able to see the session unboundedness error.</p>
<pre><code class="language-bash"><div>$ faircheck -a artifact/equation_4_B.pi
NO: session-unbounded process: B₁ [line 1] creates x [line 1]
</div></code></pre>
<p><code>FairCheck</code> reports not only the name <code>B₁</code> of the process definition that has
been found to be session unbounded, but also the name <code>x</code> of the session that
contributes to its session unboundedness.</p>
<p>Finally, the script <a href="artifact/equation_5.pi"><code>equation_5.pi</code></a> contains the
definition of the process <code>B₂</code> in Eq. (5).</p>
<pre><code class="language-pi"><code><div>B₂ = new (x : !a.!end ⊕ !b.?end)
x!{a: close x, b: wait x.B₂}
in x?{a: wait x.B₂, b: close x}
</div></code></code></pre>
<p>This process is claimed to be action bounded (each of the two processes in
parallel has a non-recursive branch) but also session unbounded.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/equation_5.pi
NO: session-unbounded process: B₂ [line 1] creates x [line 1]
</div></code></pre>
<h3 id="claim-6">Claim 6</h3>
<p>The script <a href="artifact/equation_6.pi"><code>equation_6.pi</code></a> contains the definitions of
the program in Eq. (6), whose purpose is to show that a well-typed - hence
session-bounded - process may still create an <em>unbounded</em> number of sessions.
The process <code>A</code> discussed in <a href="#claim-5">the previous section</a> is already such an
example in which the created sessions are <em>chained</em> together, so that a new
session may be created only after the previous ones have terminated. In this
example we see that sessions may also be <em>nested</em>, so that a session terminates
only after those created after it have terminated as well.</p>
<pre><code class="language-pi"><code><div>C(x : !end) = (new (y : !end) C⟨y⟩ in wait y.close x) ⊕ close x
Main = new (x : !end) C⟨x⟩ in wait x.done
</div></code></code></pre>
<p>We can run <code>FairCheck</code> with the option <code>--verbose</code> to verify the claim that the
program is well typed and also to show the <strong>rank</strong> inferred by <code>FairCheck</code> of
the process definitions contained therein. The rank of a process is an upper
bound to the number of sessions the process needs to create and to the number of
casts it needs to perform in order to terminate.</p>
<pre><code class="language-bash"><div>$ faircheck --verbose artifact/equation_6.pi
OK
process C has rank 0
process Main has rank 1
</div></code></pre>
<p>We see that the rank of <code>C</code> is 0, since <code>C</code> may reduce to <code>close x</code> without
creating any new session. On the other hand, the rank of <code>Main</code> is 1, since
<code>Main</code> may terminate only after the session <code>x</code> it creates has been completed.</p>
<h3 id="claim-7">Claim 7</h3>
<p>The script <a href="artifact/equation_7.pi"><code>equation_7.pi</code></a> contains the definitions of
the program in Eq. (7), which illustrates one case where "infinitely many"
applications of fair subtyping may have the same overall effect of a single
application of unfair subtyping.</p>
<pre><code class="language-pi"><code><div>type S = !add.S ⊕ !pay.!end
type T = ?add.T + ?pay.?end
A(x : S) = ⌈x : !add.S⌉ x!add.A⟨x⟩
B(x : T) = x?{add: B⟨x⟩, pay: wait x.done}
Main = new (x : S) A⟨x⟩ in B⟨x⟩
</div></code></code></pre>
<p>The paper claims that this program would be well typed if action boundedness and
cast boundedness were not enforced. To verify this claim, we run <code>FairCheck</code>
with the options <code>-a</code> (to disable action boundedness checking) and <code>-b</code> (to
disable both session and cast boundedness checking).</p>
<pre><code class="language-bash"><div>$ faircheck -a -b artifact/equation_7.pi
OK
</div></code></pre>
<p>Note that the option <code>-b</code> disables <em>both</em> session boundedness and cast
boundedness checking. Nonetheless, <code>FairCheck</code> is able to distinguish the
violation of each property independently. For example, both <code>B₁</code> and <code>B₂</code>
discussed in <a href="#claim-5">Claim 5</a> are flagged as session unbounded, whereas <code>A</code>
discussed here is flagged as cast unbounded.</p>
<pre><code class="language-bash"><div>$ faircheck -a artifact/equation_7.pi
NO: cast-unbounded process: A [line 4] casts x [line 4]
</div></code></pre>
<p>The error message provides information about the location of the cast that makes
<code>A</code> cast unbounded.</p>
<h3 id="claim-8">Claim 8</h3>
<p>The purpose of Eq. (8) is to show that, if a program is allowed to perform an
unbounded number of casts, it may not terminate even if it is action bounded.
The script <a href="artifact/equation_8.pi"><code>equation_8.pi</code></a> contains the definitions of
the program in Eq. (8).</p>
<pre><code class="language-pi"><code><div>type S = !more.(?more.S + ?stop.?end) ⊕ !stop.!end
type T = ?more.(!more.T ⊕ !stop.!end) + ?stop.?end
type SA = !more.(?more.S + ?stop.?end)
A(x : S) = ⌈x : SA⌉ x!more.x?{more: A⟨x⟩, stop: wait x.done}
B(x : T) = x?{more: ⌈x : !more.T⌉ x!more.B⟨x⟩, stop: wait x.done}
Main = new (x : S) A⟨x⟩ in B⟨x⟩
</div></code></code></pre>
<p>The paper claims that this program is action bounded and cast unbounded. Indeed,
each recursive process contains a non-recursive branch and yet it may need to
perform an unbounded number of casts in order to terminate.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/equation_8.pi
NO: cast-unbounded process: A [line 5] casts x [line 5]
</div></code></pre>
<p>We can run <code>FairCheck</code> with the <code>-b</code> option to verify that the program is
otherwise well typed, and in particular that all the performed casts are valid
ones, in the sense that they use fair subtyping.</p>
<pre><code class="language-bash"><div>$ faircheck -b artifact/equation_8.pi
OK
</div></code></pre>
<h3 id="claim-9">Claim 9</h3>
<p>The script <a href="artifact/equation_9.pi"><code>equation_9.pi</code></a> contains the definitions of
the program shown in Eq. (9).</p>
<pre><code class="language-pi"><code><div>type S = !more.(?more.S + ?stop.?end) ⊕ !stop.!end
type T = ?more.(!more.T + !stop.!end) + ?stop.?end
type TA = !more.(?more.TA + ?stop.?end)
type TB = ?more.!more.TB + ?stop.?end
A(x : TA) = x!more.x?{more: A⟨x⟩, stop: wait x.done}
B(x : TB) = x?{more: x!more.B⟨x⟩, stop: wait x.done}
Main = new (x : S) ⌈x : TA⌉ A⟨x⟩ in ⌈x : TB⌉ B⟨x⟩
</div></code></code></pre>
<p>This program is claimed to be action bounded, session bounded and cast bounded,
but also ill typed because the two casts it performs are invalid.</p>
<pre><code class="language-bash"><div>$ faircheck artifact/equation_9.pi
NO: invalid cast <span class="hljs-keyword">for</span> x [line 8]: rec X₄.!{ more: ?{ more: X₄, stop: ?end }, stop: !end } is not a fair subtype of rec X₃.!more.?{ more: X₃, stop: ?end }
</div></code></pre>
<p>Since <code>FairCheck</code> internally represents session types as regular trees, the
session types printed in error messages may look different from those occurring
in the script. However, it is relatively easy to see that the recursive session
type</p>
<pre><code class="language-pi"><code><div>rec X₄.!{ more: ?{ more: X₄, stop: ?end }, stop: !end }
</div></code></code></pre>
<p>in the error message is isomorphic to <code>S</code> in the script and that</p>
<pre><code class="language-pi"><code><div>rec X₃.!more.?{ more: X₃, stop: ?end }
</div></code></code></pre>
<p>is isomorphic to <code>TA</code>. So, the error message indicates that <code>S</code> is not a fair
subtype of <code>TA</code>. We can verify that the program is well typed if <strong>unfair
subtyping</strong> is used instead of fair subtyping by passing the <code>-u</code> option to
<code>FairCheck</code>.</p>
<pre><code class="language-bash"><div>$ faircheck -u artifact/equation_9.pi
OK
</div></code></pre>
<h2 id="additional-artifact-description">Additional artifact description</h2>
<p>The <code>FairCheck</code> directory is structured in this way:</p>
<ul>
<li><a href="src"><code>src</code></a>: Haskell source code of <code>FairCheck</code></li>
<li><a href="examples"><code>examples</code></a>: some examples of well-typed programs, all of which
have also been discussed in the previous sections</li>
<li><a href="errors"><code>errors</code></a>: exhaustive set of ill-typed programs aimed at testing all
of the errors that can be detected by <code>FairCheck</code>. Some (but not all) of these
programs have been discussed in the previous sections.</li>
<li><a href="artifact"><code>artifact</code></a>: all of the programs discussed in the previous
sections. This is a mixed bag of well- and ill-typed programs.</li>
</ul>
<p>Within <a href="src"><code>src</code></a>, the source code of <code>FairCheck</code> is structured into the
following modules:</p>
<ul>
<li><a href="src/Common.hs"><code>Common</code></a>: general-purpose functions not found in Haskell
standard library</li>
<li><a href="src/Atoms.hs"><code>Atoms</code></a>: representation of <strong>identifiers</strong> and
<strong>polarities</strong></li>
<li><a href="src/Exceptions.hs"><code>Exceptions</code></a>: <code>FairCheck</code>-specific syntax and typing
<strong>errors</strong></li>
<li><a href="src/Type.hs"><code>Type</code></a>: representation of <strong>session types</strong></li>
<li><a href="src/Process.hs"><code>Process</code></a>: representation of <strong>processes</strong></li>
<li><a href="src/Lexer.x"><code>Lexer</code></a>: Alex specification of the <strong>lexical analyzer</strong></li>
<li><a href="src/Parser.y"><code>Parser</code></a>: Happy specification of the <strong>parser</strong></li>
<li><a href="src/Resolver.hs"><code>Resolver</code></a>: expansion of session types into closed
recursive terms</li>
<li><a href="src/Node.hs"><code>Node</code></a> and <a href="src/Tree.hs"><code>Tree</code></a>: <strong>regular tree
representation</strong> of session types</li>
<li><a href="src/Checker.hs"><code>Checker</code></a>: implementation of the <strong>type checker</strong></li>
<li><a href="src/Formula.hs"><code>Formula</code></a>: implementation of <strong>model checker</strong> for the
<strong>μ-calculus</strong></li>
<li><a href="src/Predicate.hs"><code>Predicate</code></a>: <strong>μ-calculus formulas</strong> used in the
algorithm for fair subtyping</li>
<li><a href="src/Relation.hs"><code>Relation</code></a>: implementation of <strong>session type equality</strong>,
<strong>unfair subtyping</strong> and <strong>fair subtyping</strong> decision algorithms</li>
<li><a href="src/Render.hs"><code>Render</code></a>: <strong>pretty printer</strong> for session types and error
messages</li>
<li><a href="src/Main.hs"><code>Main</code></a>: main module and handler of command-line options</li>
</ul>
<p>The <code>FairCheck</code> parser accepts a syntax that is close to, but not exactly the
same as, the one used in the paper. The table below shows the grammar of
scripts. Square brackets enclose optional parts of the syntax.</p>
<table>
<thead>
<tr>
<th style="text-align:right">Entity</th>
<th></th>
<th>Definition</th>
<th>Description</th>
</tr>
</thead>
<tbody>
<tr>
<td style="text-align:right">x, y</td>
<td></td>
<td>non-capitalized identifier (e.g. <code>x</code>, <code>y</code>, ...)</td>
<td>Channel name</td>
</tr>
<tr>
<td style="text-align:right">l</td>
<td></td>
<td>non-capitalized identifier or number (e.g. <code>a</code>, <code>add</code>, <code>0</code>, ...)</td>
<td>Label</td>
</tr>
<tr>
<td style="text-align:right">X</td>
<td></td>
<td>capitalized identifier (e.g. <code>S</code>, <code>T</code>, ...)</td>
<td>Type name</td>
</tr>
<tr>
<td style="text-align:right">A</td>
<td></td>
<td>capitalized identifier (e.g. <code>A</code>, <code>Main</code>, ...)</td>
<td>Process name</td>
</tr>
<tr>
<td style="text-align:right">π</td>
<td>::=</td>
<td><code>?</code></td>
<td>Input polarity</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td><code>!</code></td>
<td>Output polarity</td>
</tr>
<tr>
<td style="text-align:right">Script</td>
<td>::=</td>
<td>TypeDef₁ ... TypeDefₘ ProcessDef₁ ... ProcessDefₙ</td>
<td></td>
</tr>
<tr>
<td style="text-align:right">TypeDef</td>
<td>::=</td>
<td>X <code>=</code> Type</td>
<td>Type definition</td>
</tr>
<tr>
<td style="text-align:right">ProcessDef</td>
<td>::=</td>
<td>A [<code>(</code> x₁ <code>:</code> Type <code>,</code> ... <code>,</code> xₙ <code>:</code> Type <code>)</code>] <code>=</code> Process</td>
<td>Process definition</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>A [<code>(</code> x₁ <code>:</code> Type <code>,</code> ... <code>,</code> xₙ <code>:</code> Type <code>)</code>] <code>;</code></td>
<td>Undefined process declaration</td>
</tr>
<tr>
<td style="text-align:right">Process</td>
<td>::=</td>
<td><code>done</code></td>
<td>Terminated process</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td><code>close</code> x</td>
<td>Signal output</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td><code>wait</code> x <code>.</code> Process</td>
<td>Signal input</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>x π <code>(</code> y <code>)</code> <code>.</code> Process</td>
<td>Channel input/output</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>x π <code>{</code> l₁ <code>:</code> Process <code>,</code> ... <code>,</code> lₙ <code>:</code> Process <code>}</code></td>
<td>Label input/output</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>x <code>!</code> l <code>.</code> Process</td>
<td>Shortcut for label output</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td><code>new</code> <code>(</code> x <code>:</code> Type <code>)</code> Process <code>in</code> Process</td>
<td>New session</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>Process <code>⊕</code> Process</td>
<td>Non-deterministic choice</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td><code>⌈</code> x <code>:</code> Type <code>⌉</code> Process</td>
<td>Cast</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>A [<code>⟨</code> x₁ <code>,</code> ... <code>,</code> xₙ <code>⟩</code>]</td>
<td>Invocation</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td><code>(</code> Process <code>)</code></td>
<td>Bracketed process</td>
</tr>
<tr>
<td style="text-align:right">Type</td>
<td>::=</td>
<td>π <code>end</code></td>
<td>Terminated session</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>π Type <code>.</code> Type</td>
<td>Channel input/output</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>π <code>{</code> l₁ <code>:</code> Type <code>,</code> ... <code>,</code> lₙ <code>:</code> Type <code>}</code></td>
<td>Label input/output</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>π l <code>.</code> Type</td>
<td>Shortcur for label input/output</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>Type <code>+</code> Type</td>
<td>Shortcut for external choice (label input)</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>Type <code>⊕</code> Type</td>
<td>Shortcur for internal choice (label output)</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td>X</td>
<td>Type name</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td><code>rec</code> X <code>.</code> Type</td>
<td>Recursive type</td>
</tr>
<tr>
<td style="text-align:right"></td>
<td></td>
<td><code>(</code> Type <code>)</code></td>
<td>Bracketed type</td>
</tr>
</tbody>
</table>
</body>
</html>