aver-cert 0.1.0

Independent artifact certificate engine and verifier for Aver WebAssembly
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

fn render_certificate(
    analysis: &Analysis,
    model_roots: &[String],
    model_info: &ModelInfo,
) -> String {
    let mut s = String::new();
    s.push_str(
        "import CertPrelude\nimport Module\nimport Schema\nimport Manifest\nimport IntDispatchSoundness\nimport DischargeComposition\nimport DischargeExprFragment\nimport DischargeRecursion\n",
    );
    for r in model_roots {
        s.push_str(&format!("import {r}\n"));
    }
    s.push_str(
        "\nset_option linter.unusedSimpArgs false\n\
         set_option linter.unusedVariables false\n\
         set_option maxRecDepth 1000000\n\n\
         namespace CertProofs\nopen CertPrelude CertModule AverCert AverCert.Schema\n\n",
    );
    let struct_table_lean = emit_frag_struct_table_lean(analysis)
        .expect("certified fragment struct table remains consistent");
    // Mutual option-(b) bridges share one concrete SCC/acceptance package.
    // Emit those packages first so source/export order cannot create a forward
    // reference when a non-primary member appears before its primary.
    for c in &analysis.certs {
        if matches!(c.inner(), Cert::MutualRecursion { .. }) {
            s.push_str(&render_mutual_shared_bridge_data(c));
        }
    }
    for c in &analysis.certs {
        match c.inner() {
            Cert::Recursive { .. } | Cert::AccumulatorRecursive { .. }
                if recursion_uses_audited_generic(c) =>
            {
                s.push_str(&render_recursion_semantic_bridge(c))
            }
            Cert::Recursive { .. } | Cert::AccumulatorRecursive { .. } => {
                s.push_str(&render_fueled_recursion_cert(c))
            }
            Cert::AdtConstructor { .. } if adt_constructor_uses_model(c, model_info) => {
                s.push_str(&render_adt_constructor_semantic_bridge(c, model_info))
            }
            // Verbatim constructor packs are option-(c) leaves discharged in
            // `Final.cert`; model-bearing constructors emit only their option-(b)
            // source-model bridge above.
            Cert::AdtConstructor { .. } => {}
            // The field-projection family is discharged in `Final.cert` by the
            // audited generic theorem plus its canonical option-(c) leaf bridge.
            // Its plan, obligation and claim data remain emitted unchanged.
            Cert::FieldProjection { .. } => {}
            Cert::WidenedIntMatch { .. } | Cert::VariantDispatch { .. } => {
                s.push_str(&render_int_dispatch_semantic_bridge(
                    c,
                    model_info,
                    analysis.frag_host_table,
                ))
            }
            Cert::ExprFragment { .. } if expr_fragment_uses_audited_generic(c) => {
                s.push_str(&render_expr_fragment_semantic_bridge(
                    c,
                    analysis.frag_host_table,
                    &struct_table_lean,
                ))
            }
            Cert::ExprFragment { .. } => s.push_str(&render_expr_fragment_cert(c)),
            // Verbatim and String families are discharged by their audited
            // canonical leaf bridges. Their plans/claims/data remain emitted.
            Cert::VerbatimWidenedMatch { .. }
            | Cert::VerbatimVariantDispatch { .. }
            | Cert::StringEqVerbatimMatch { .. }
            | Cert::StringConcatVerbatimMatch { .. } => {}
            Cert::Composition { .. } => {
                s.push_str(&render_composition_semantic_bridge(c, analysis))
            }
            Cert::MutualRecursion { .. } => s.push_str(&render_mutual_semantic_bridge(c)),
            Cert::NonRecursive { .. } => unreachable!(),
        }
        s.push('\n');
    }
    s.push_str("end CertProofs\n");
    s
}