omena-cascade 0.1.14

Cascade-formal substrate for Omena CSS
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

//! Modal proof-obligation aggregation for cascade transform witnesses.
//!
//! The V0 summary turns individual proof witnesses into a single conservative
//! surface that release gates can inspect without knowing each witness shape.

use crate::{ModalCheckWitnessSourceV0, ModalCheckWitnessV0, StaticSupportsEvalVerdictV0};

pub fn summarize_modal_check_witness_v0(
    witnesses: Vec<ModalCheckWitnessSourceV0>,
) -> ModalCheckWitnessV0 {
    let accepted_count = witnesses
        .iter()
        .filter(|witness| modal_witness_accepted(witness))
        .count();
    let source_products = witnesses
        .iter()
        .map(modal_witness_product)
        .collect::<Vec<_>>();
    let all_provenance_preserved = witnesses.iter().all(modal_witness_provenance_preserved);
    let obligation_count = witnesses.len();

    ModalCheckWitnessV0 {
        schema_version: "0",
        product: "omena-cascade.modal-check-witness",
        modal_family: "cascadeProofObligationStrictSuperset",
        substrate: "omena-cascade.proof-witnesses",
        obligation_count,
        accepted_count,
        blocked_count: obligation_count - accepted_count,
        all_provenance_preserved,
        source_products,
        witnesses,
    }
}

fn modal_witness_accepted(witness: &ModalCheckWitnessSourceV0) -> bool {
    match witness {
        ModalCheckWitnessSourceV0::ShorthandCombination(proof) => proof.accepted,
        ModalCheckWitnessSourceV0::StaticSupportsEval(witness) => {
            witness.verdict != StaticSupportsEvalVerdictV0::Unknown
        }
        ModalCheckWitnessSourceV0::ScopeFlatten(proof) => proof.accepted,
        ModalCheckWitnessSourceV0::LayerFlatten(proof) => proof.accepted,
    }
}

fn modal_witness_provenance_preserved(witness: &ModalCheckWitnessSourceV0) -> bool {
    match witness {
        ModalCheckWitnessSourceV0::ShorthandCombination(proof) => proof.provenance_preserved,
        ModalCheckWitnessSourceV0::StaticSupportsEval(witness) => witness.provenance_preserved,
        ModalCheckWitnessSourceV0::ScopeFlatten(proof) => proof.provenance_preserved,
        ModalCheckWitnessSourceV0::LayerFlatten(proof) => proof.provenance_preserved,
    }
}

fn modal_witness_product(witness: &ModalCheckWitnessSourceV0) -> &'static str {
    match witness {
        ModalCheckWitnessSourceV0::ShorthandCombination(proof) => proof.product,
        ModalCheckWitnessSourceV0::StaticSupportsEval(witness) => witness.product,
        ModalCheckWitnessSourceV0::ScopeFlatten(proof) => proof.product,
        ModalCheckWitnessSourceV0::LayerFlatten(proof) => proof.product,
    }
}