meerkat-machine-schema 0.5.0

Formal machine schemas and transition definitions for Meerkat
Documentation
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
use indexmap::IndexMap;

use crate::{
    EffectDisposition, EffectDispositionRule, EffectEmit, EnumSchema, Expr, FieldSchema, Guard,
    HelperSchema, InitSchema, InputMatch, InvariantSchema, MachineSchema, Quantifier, RustBinding,
    StateSchema, TransitionSchema, TypeRef, Update, VariantSchema,
};

pub fn peer_comms_machine() -> MachineSchema {
    MachineSchema {
        machine: "PeerCommsMachine".into(),
        version: 1,
        rust: RustBinding {
            crate_name: "meerkat-comms".into(),
            module: "generated::peer_comms".into(),
        },
        state: StateSchema {
            phase: EnumSchema {
                name: "PeerIngressState".into(),
                variants: vec![
                    variant("Absent"),
                    variant("Received"),
                    variant("Dropped"),
                    variant("Delivered"),
                ],
            },
            fields: vec![
                field(
                    "trusted_peers",
                    TypeRef::Set(Box::new(TypeRef::Named("PeerId".into()))),
                ),
                field(
                    "raw_item_peer",
                    TypeRef::Map(
                        Box::new(TypeRef::Named("RawItemId".into())),
                        Box::new(TypeRef::Named("PeerId".into())),
                    ),
                ),
                field(
                    "raw_item_kind",
                    TypeRef::Map(
                        Box::new(TypeRef::Named("RawItemId".into())),
                        Box::new(TypeRef::Named("RawPeerKind".into())),
                    ),
                ),
                field(
                    "classified_as",
                    TypeRef::Map(
                        Box::new(TypeRef::Named("RawItemId".into())),
                        Box::new(TypeRef::Named("PeerInputClass".into())),
                    ),
                ),
                field(
                    "text_projection",
                    TypeRef::Map(
                        Box::new(TypeRef::Named("RawItemId".into())),
                        Box::new(TypeRef::String),
                    ),
                ),
                field(
                    "content_shape",
                    TypeRef::Map(
                        Box::new(TypeRef::Named("RawItemId".into())),
                        Box::new(TypeRef::Named("ContentShape".into())),
                    ),
                ),
                field(
                    "request_id",
                    TypeRef::Map(
                        Box::new(TypeRef::Named("RawItemId".into())),
                        Box::new(TypeRef::Option(Box::new(TypeRef::Named(
                            "RequestId".into(),
                        )))),
                    ),
                ),
                field(
                    "reservation_key",
                    TypeRef::Map(
                        Box::new(TypeRef::Named("RawItemId".into())),
                        Box::new(TypeRef::Option(Box::new(TypeRef::Named(
                            "ReservationKey".into(),
                        )))),
                    ),
                ),
                field(
                    "trusted_snapshot",
                    TypeRef::Map(
                        Box::new(TypeRef::Named("RawItemId".into())),
                        Box::new(TypeRef::Bool),
                    ),
                ),
                field(
                    "submission_queue",
                    TypeRef::Seq(Box::new(TypeRef::Named("RawItemId".into()))),
                ),
            ],
            init: InitSchema {
                phase: "Absent".into(),
                fields: vec![],
            },
            terminal_phases: vec!["Dropped".into(), "Delivered".into()],
        },
        inputs: EnumSchema {
            name: "PeerCommsInput".into(),
            variants: vec![
                VariantSchema {
                    name: "TrustPeer".into(),
                    fields: vec![field("peer_id", TypeRef::Named("PeerId".into()))],
                },
                VariantSchema {
                    name: "ReceivePeerEnvelope".into(),
                    fields: vec![
                        field("raw_item_id", TypeRef::Named("RawItemId".into())),
                        field("peer_id", TypeRef::Named("PeerId".into())),
                        field("raw_kind", TypeRef::Named("RawPeerKind".into())),
                        field("text_projection", TypeRef::String),
                        field("content_shape", TypeRef::Named("ContentShape".into())),
                        field(
                            "request_id",
                            TypeRef::Option(Box::new(TypeRef::Named("RequestId".into()))),
                        ),
                        field(
                            "reservation_key",
                            TypeRef::Option(Box::new(TypeRef::Named("ReservationKey".into()))),
                        ),
                    ],
                },
                VariantSchema {
                    name: "SubmitTypedPeerInput".into(),
                    fields: vec![field("raw_item_id", TypeRef::Named("RawItemId".into()))],
                },
            ],
        },
        effects: EnumSchema {
            name: "PeerCommsEffect".into(),
            variants: vec![VariantSchema {
                name: "SubmitPeerInputCandidate".into(),
                fields: vec![
                    field("raw_item_id", TypeRef::Named("RawItemId".into())),
                    field("peer_input_class", TypeRef::Named("PeerInputClass".into())),
                    field("text_projection", TypeRef::String),
                    field("content_shape", TypeRef::Named("ContentShape".into())),
                    field(
                        "request_id",
                        TypeRef::Option(Box::new(TypeRef::Named("RequestId".into()))),
                    ),
                    field(
                        "reservation_key",
                        TypeRef::Option(Box::new(TypeRef::Named("ReservationKey".into()))),
                    ),
                ],
            }],
        },
        helpers: vec![HelperSchema {
            name: "ClassFor".into(),
            params: vec![field("raw_kind", TypeRef::Named("RawPeerKind".into()))],
            returns: TypeRef::Named("PeerInputClass".into()),
            body: Expr::IfElse {
                condition: Box::new(Expr::Eq(
                    Box::new(Expr::Binding("raw_kind".into())),
                    Box::new(Expr::String("request".into())),
                )),
                then_expr: Box::new(Expr::String("ActionableRequest".into())),
                else_expr: Box::new(Expr::IfElse {
                    condition: Box::new(Expr::Eq(
                        Box::new(Expr::Binding("raw_kind".into())),
                        Box::new(Expr::String("response_terminal".into())),
                    )),
                    then_expr: Box::new(Expr::String("Response".into())),
                    else_expr: Box::new(Expr::IfElse {
                        condition: Box::new(Expr::Eq(
                            Box::new(Expr::Binding("raw_kind".into())),
                            Box::new(Expr::String("response_progress".into())),
                        )),
                        then_expr: Box::new(Expr::String("Response".into())),
                        else_expr: Box::new(Expr::IfElse {
                            condition: Box::new(Expr::Eq(
                                Box::new(Expr::Binding("raw_kind".into())),
                                Box::new(Expr::String("plain_event".into())),
                            )),
                            then_expr: Box::new(Expr::String("PlainEvent".into())),
                            else_expr: Box::new(Expr::IfElse {
                                condition: Box::new(Expr::Eq(
                                    Box::new(Expr::Binding("raw_kind".into())),
                                    Box::new(Expr::String("silent_request".into())),
                                )),
                                then_expr: Box::new(Expr::String("SilentRequest".into())),
                                else_expr: Box::new(Expr::String("ActionableMessage".into())),
                            }),
                        }),
                    }),
                }),
            },
        }],
        derived: vec![],
        invariants: vec![
            InvariantSchema {
                name: "queued_items_are_classified".into(),
                expr: Expr::Quantified {
                    quantifier: Quantifier::All,
                    binding: "raw_item_id".into(),
                    over: Box::new(Expr::Field("submission_queue".into())),
                    body: Box::new(Expr::Contains {
                        collection: Box::new(Expr::MapKeys(Box::new(Expr::Field(
                            "classified_as".into(),
                        )))),
                        value: Box::new(Expr::Binding("raw_item_id".into())),
                    }),
                },
            },
            InvariantSchema {
                name: "queued_items_preserve_content_shape".into(),
                expr: Expr::Quantified {
                    quantifier: Quantifier::All,
                    binding: "raw_item_id".into(),
                    over: Box::new(Expr::Field("submission_queue".into())),
                    body: Box::new(Expr::Contains {
                        collection: Box::new(Expr::MapKeys(Box::new(Expr::Field(
                            "content_shape".into(),
                        )))),
                        value: Box::new(Expr::Binding("raw_item_id".into())),
                    }),
                },
            },
            InvariantSchema {
                name: "queued_items_preserve_text_projection".into(),
                expr: Expr::Quantified {
                    quantifier: Quantifier::All,
                    binding: "raw_item_id".into(),
                    over: Box::new(Expr::Field("submission_queue".into())),
                    body: Box::new(Expr::Contains {
                        collection: Box::new(Expr::MapKeys(Box::new(Expr::Field(
                            "text_projection".into(),
                        )))),
                        value: Box::new(Expr::Binding("raw_item_id".into())),
                    }),
                },
            },
            InvariantSchema {
                name: "queued_items_preserve_correlation_slots".into(),
                expr: Expr::Quantified {
                    quantifier: Quantifier::All,
                    binding: "raw_item_id".into(),
                    over: Box::new(Expr::Field("submission_queue".into())),
                    body: Box::new(Expr::And(vec![
                        Expr::Contains {
                            collection: Box::new(Expr::MapKeys(Box::new(Expr::Field(
                                "request_id".into(),
                            )))),
                            value: Box::new(Expr::Binding("raw_item_id".into())),
                        },
                        Expr::Contains {
                            collection: Box::new(Expr::MapKeys(Box::new(Expr::Field(
                                "reservation_key".into(),
                            )))),
                            value: Box::new(Expr::Binding("raw_item_id".into())),
                        },
                    ])),
                },
            },
        ],
        transitions: vec![
            TransitionSchema {
                name: "TrustPeer".into(),
                from: vec!["Absent".into(), "Received".into()],
                on: InputMatch {
                    variant: "TrustPeer".into(),
                    bindings: vec!["peer_id".into()],
                },
                guards: vec![],
                updates: vec![Update::SetInsert {
                    field: "trusted_peers".into(),
                    value: Expr::Binding("peer_id".into()),
                }],
                to: "Absent".into(),
                emit: vec![],
            },
            TransitionSchema {
                name: "ReceiveTrustedPeerEnvelope".into(),
                from: vec!["Absent".into(), "Received".into()],
                on: InputMatch {
                    variant: "ReceivePeerEnvelope".into(),
                    bindings: vec![
                        "raw_item_id".into(),
                        "peer_id".into(),
                        "raw_kind".into(),
                        "text_projection".into(),
                        "content_shape".into(),
                        "request_id".into(),
                        "reservation_key".into(),
                    ],
                },
                guards: vec![Guard {
                    name: "peer_is_trusted".into(),
                    expr: Expr::Contains {
                        collection: Box::new(Expr::Field("trusted_peers".into())),
                        value: Box::new(Expr::Binding("peer_id".into())),
                    },
                }],
                updates: vec![
                    Update::MapInsert {
                        field: "raw_item_peer".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("peer_id".into()),
                    },
                    Update::MapInsert {
                        field: "raw_item_kind".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("raw_kind".into()),
                    },
                    Update::MapInsert {
                        field: "classified_as".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Call {
                            helper: "ClassFor".into(),
                            args: vec![Expr::Binding("raw_kind".into())],
                        },
                    },
                    Update::MapInsert {
                        field: "text_projection".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("text_projection".into()),
                    },
                    Update::MapInsert {
                        field: "content_shape".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("content_shape".into()),
                    },
                    Update::MapInsert {
                        field: "request_id".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("request_id".into()),
                    },
                    Update::MapInsert {
                        field: "reservation_key".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("reservation_key".into()),
                    },
                    Update::MapInsert {
                        field: "trusted_snapshot".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Bool(true),
                    },
                    Update::SeqAppend {
                        field: "submission_queue".into(),
                        value: Expr::Binding("raw_item_id".into()),
                    },
                ],
                to: "Received".into(),
                emit: vec![],
            },
            TransitionSchema {
                name: "DropUntrustedPeerEnvelope".into(),
                from: vec!["Absent".into(), "Received".into()],
                on: InputMatch {
                    variant: "ReceivePeerEnvelope".into(),
                    bindings: vec![
                        "raw_item_id".into(),
                        "peer_id".into(),
                        "raw_kind".into(),
                        "text_projection".into(),
                        "content_shape".into(),
                        "request_id".into(),
                        "reservation_key".into(),
                    ],
                },
                guards: vec![Guard {
                    name: "peer_is_not_trusted".into(),
                    expr: Expr::Not(Box::new(Expr::Contains {
                        collection: Box::new(Expr::Field("trusted_peers".into())),
                        value: Box::new(Expr::Binding("peer_id".into())),
                    })),
                }],
                updates: vec![
                    Update::MapInsert {
                        field: "raw_item_peer".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("peer_id".into()),
                    },
                    Update::MapInsert {
                        field: "raw_item_kind".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("raw_kind".into()),
                    },
                    Update::MapInsert {
                        field: "text_projection".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("text_projection".into()),
                    },
                    Update::MapInsert {
                        field: "content_shape".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("content_shape".into()),
                    },
                    Update::MapInsert {
                        field: "request_id".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("request_id".into()),
                    },
                    Update::MapInsert {
                        field: "reservation_key".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Binding("reservation_key".into()),
                    },
                    Update::MapInsert {
                        field: "trusted_snapshot".into(),
                        key: Expr::Binding("raw_item_id".into()),
                        value: Expr::Bool(false),
                    },
                ],
                to: "Dropped".into(),
                emit: vec![],
            },
            TransitionSchema {
                name: "SubmitTypedPeerInputDelivered".into(),
                from: vec!["Received".into()],
                on: InputMatch {
                    variant: "SubmitTypedPeerInput".into(),
                    bindings: vec!["raw_item_id".into()],
                },
                guards: vec![
                    Guard {
                        name: "item_was_queued".into(),
                        expr: Expr::Contains {
                            collection: Box::new(Expr::Field("submission_queue".into())),
                            value: Box::new(Expr::Binding("raw_item_id".into())),
                        },
                    },
                    Guard {
                        name: "item_was_classified".into(),
                        expr: Expr::Contains {
                            collection: Box::new(Expr::MapKeys(Box::new(Expr::Field(
                                "classified_as".into(),
                            )))),
                            value: Box::new(Expr::Binding("raw_item_id".into())),
                        },
                    },
                    Guard {
                        name: "delivery_drains_queue".into(),
                        expr: Expr::Eq(
                            Box::new(Expr::Len(Box::new(Expr::Field("submission_queue".into())))),
                            Box::new(Expr::U64(1)),
                        ),
                    },
                ],
                updates: vec![Update::SeqRemoveValue {
                    field: "submission_queue".into(),
                    value: Expr::Binding("raw_item_id".into()),
                }],
                to: "Delivered".into(),
                emit: vec![emit_submit_candidate()],
            },
            TransitionSchema {
                name: "SubmitTypedPeerInputContinue".into(),
                from: vec!["Received".into()],
                on: InputMatch {
                    variant: "SubmitTypedPeerInput".into(),
                    bindings: vec!["raw_item_id".into()],
                },
                guards: vec![
                    Guard {
                        name: "item_was_queued".into(),
                        expr: Expr::Contains {
                            collection: Box::new(Expr::Field("submission_queue".into())),
                            value: Box::new(Expr::Binding("raw_item_id".into())),
                        },
                    },
                    Guard {
                        name: "item_was_classified".into(),
                        expr: Expr::Contains {
                            collection: Box::new(Expr::MapKeys(Box::new(Expr::Field(
                                "classified_as".into(),
                            )))),
                            value: Box::new(Expr::Binding("raw_item_id".into())),
                        },
                    },
                    Guard {
                        name: "delivery_leaves_more_work".into(),
                        expr: Expr::Gt(
                            Box::new(Expr::Len(Box::new(Expr::Field("submission_queue".into())))),
                            Box::new(Expr::U64(1)),
                        ),
                    },
                ],
                updates: vec![Update::SeqRemoveValue {
                    field: "submission_queue".into(),
                    value: Expr::Binding("raw_item_id".into()),
                }],
                to: "Received".into(),
                emit: vec![emit_submit_candidate()],
            },
        ],
        effect_dispositions: vec![disposition(
            "SubmitPeerInputCandidate",
            EffectDisposition::Routed {
                consumer_machines: vec!["RuntimeControlMachine".into()],
            },
        )],
    }
}

fn disposition(name: &str, d: EffectDisposition) -> EffectDispositionRule {
    EffectDispositionRule {
        effect_variant: name.into(),
        disposition: d,
        handoff_protocol: None,
    }
}

fn emit_submit_candidate() -> EffectEmit {
    EffectEmit {
        variant: "SubmitPeerInputCandidate".into(),
        fields: IndexMap::from([
            ("raw_item_id".into(), Expr::Binding("raw_item_id".into())),
            (
                "peer_input_class".into(),
                Expr::MapGet {
                    map: Box::new(Expr::Field("classified_as".into())),
                    key: Box::new(Expr::Binding("raw_item_id".into())),
                },
            ),
            (
                "text_projection".into(),
                Expr::MapGet {
                    map: Box::new(Expr::Field("text_projection".into())),
                    key: Box::new(Expr::Binding("raw_item_id".into())),
                },
            ),
            (
                "content_shape".into(),
                Expr::MapGet {
                    map: Box::new(Expr::Field("content_shape".into())),
                    key: Box::new(Expr::Binding("raw_item_id".into())),
                },
            ),
            (
                "request_id".into(),
                Expr::MapGet {
                    map: Box::new(Expr::Field("request_id".into())),
                    key: Box::new(Expr::Binding("raw_item_id".into())),
                },
            ),
            (
                "reservation_key".into(),
                Expr::MapGet {
                    map: Box::new(Expr::Field("reservation_key".into())),
                    key: Box::new(Expr::Binding("raw_item_id".into())),
                },
            ),
        ]),
    }
}

fn variant(name: &str) -> VariantSchema {
    VariantSchema {
        name: name.into(),
        fields: vec![],
    }
}

fn field(name: &str, ty: TypeRef) -> FieldSchema {
    FieldSchema {
        name: name.into(),
        ty,
    }
}