affidavit 26.6.22

Provenance Layer — receipt assembly and certification (verify a witness against a format standard; never decide honesty).
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

// Reference witness: the process-artifact shape taxonomy, conformance/receipt
// verdicts, and BPMN gateway kinds are constructed as exhaustive censuses
// (COVERAGE.md §2 — shape taxonomy + verdict vocabulary).
//
//   • ProcessShapeKind  — the 22-shape taxonomy of every process artifact the
//     court models (logs, nets, trees, POWL, DECLARE, OCPQ, alignment, …).
//   • ConformanceVerdict — token-replay verdict vocabulary.
//   • ReceiptVerdict     — the admitted/refused receipt outcome.
//   • BpmnGateway        — the BPMN gateway kinds.

use wasm4pm_compat::bpmn::BpmnGateway;
use wasm4pm_compat::law::ProcessShapeKind as Shape;
use wasm4pm_compat::receipt::{ConformanceVerdict, ReceiptRefusal, ReceiptVerdict};

#[test]
fn the_process_shape_taxonomy_is_constructed() {
    let all = [
        Shape::Event,
        Shape::Trace,
        Shape::EventLog,
        Shape::EventStream,
        Shape::XesLog,
        Shape::OcelLog,
        Shape::DirectlyFollowsGraph,
        Shape::ObjectCentricDfg,
        Shape::PetriNet,
        Shape::WorkflowNet,
        Shape::ObjectCentricPetriNet,
        Shape::ProcessTree,
        Shape::Powl,
        Shape::DeclareModel,
        Shape::ObjectCentricDeclareModel,
        Shape::LogSkeleton,
        Shape::OcpqQuery,
        Shape::Alignment,
        Shape::TokenReplay,
        Shape::ConformanceVerdict,
        Shape::PredictionProblem,
        Shape::Receipt,
    ];
    assert_eq!(
        all.len(),
        22,
        "the taxonomy enumerates 22 process-artifact shapes"
    );
    // Distinctness via Debug (each is a materialised, distinct shape label).
    let s: std::collections::BTreeSet<String> = all.iter().map(|x| format!("{x:?}")).collect();
    assert_eq!(s.len(), 22, "all 22 shapes are distinct constructions");

    // COMPILE-ENFORCED exhaustiveness (van der Aalst panel B1 fix): a no-wildcard
    // match makes the census total. If wasm4pm-compat adds a 23rd ProcessShapeKind,
    // THIS fails to compile — the hand-listed array above can drift silently, but
    // the match cannot. Every shape is classified by its modelling family, so the
    // arm is a real touch of the variant, not a throwaway `_ => ()`.
    fn family(s: Shape) -> &'static str {
        match s {
            Shape::Event
            | Shape::Trace
            | Shape::EventLog
            | Shape::EventStream
            | Shape::XesLog
            | Shape::OcelLog => "log",
            Shape::DirectlyFollowsGraph
            | Shape::ObjectCentricDfg
            | Shape::PetriNet
            | Shape::WorkflowNet
            | Shape::ObjectCentricPetriNet
            | Shape::ProcessTree
            | Shape::Powl => "model",
            Shape::DeclareModel
            | Shape::ObjectCentricDeclareModel
            | Shape::LogSkeleton
            | Shape::OcpqQuery => "declarative/query",
            Shape::Alignment | Shape::TokenReplay | Shape::ConformanceVerdict => "conformance",
            Shape::PredictionProblem => "prediction",
            Shape::Receipt => "provenance",
        }
    }
    // Every listed shape resolves to a family — and the match's exhaustiveness is
    // the real guarantee (drift → compile error).
    assert!(all.iter().copied().all(|s| !family(s).is_empty()));
}

#[test]
fn conformance_and_receipt_verdicts_are_constructed() {
    // Conformance verdict vocabulary (token replay outcomes).
    let cv = [
        ConformanceVerdict::PerfectAlignment,
        ConformanceVerdict::FitnessDeficit,
        ConformanceVerdict::DeadlockEncountered,
    ];
    fn cv_label(v: ConformanceVerdict) -> &'static str {
        match v {
            ConformanceVerdict::PerfectAlignment => "perfect",
            ConformanceVerdict::FitnessDeficit => "deficit",
            ConformanceVerdict::DeadlockEncountered => "deadlock",
        }
    }
    let s: std::collections::BTreeSet<&str> = cv.iter().copied().map(cv_label).collect();
    assert_eq!(s.len(), 3, "three conformance verdicts");

    // Receipt verdict: the admitted/refused outcome (the court's binary verdict).
    // Refused carries the named refusal law — constructed with a real one.
    fn rv_label(v: &ReceiptVerdict) -> &'static str {
        match v {
            ReceiptVerdict::Admitted => "admitted",
            ReceiptVerdict::Refused(_) => "refused",
        }
    }
    let admitted = ReceiptVerdict::Admitted;
    let refused = ReceiptVerdict::Refused(ReceiptRefusal::EmptyChain);
    assert_ne!(rv_label(&admitted), rv_label(&refused));
    assert_eq!(rv_label(&refused), "refused");
}

#[test]
fn bpmn_gateway_kinds_are_constructed() {
    let all = [
        BpmnGateway::Exclusive,
        BpmnGateway::Parallel,
        BpmnGateway::Inclusive,
        BpmnGateway::EventBased,
        BpmnGateway::Complex,
    ];
    fn ok(g: BpmnGateway) -> bool {
        matches!(
            g,
            BpmnGateway::Exclusive
                | BpmnGateway::Parallel
                | BpmnGateway::Inclusive
                | BpmnGateway::EventBased
                | BpmnGateway::Complex
        )
    }
    assert!(all.iter().copied().all(ok));
    assert_eq!(all.len(), 5, "five BPMN gateway kinds");
}