tokitai-operator 0.1.0

Verified DL kernel compiler: formally-checked GEMM, p-adic, sheaf, contract-carrying ops. Paper-artifact grade.
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

//! Proof-replay report section that lists witness types and runs
//! cover-glue inference (P357).
//!
//! The base `proof_replay_report` only lists replayed proofs and
//! warnings. This module adds a complementary section that surfaces
//! the P347 valuation witness types and the P348 cover-glue
//! inference result, so the proof-replay report can answer "what
//! witness types and inference passes are available for this plan?".
//!
//! P357 keeps the new section additive: it does not modify the
//! existing proof-replay report. The new section is generated by
//! `proof_replay_witnesses_section` (static listing) and
//! `proof_replay_witnesses_section_with_inference` (with cover
//! glue inference run).

use crate::object::sheaf::{Cover, SectionTable};
use crate::verify::{CoverGlueInferenceReport, InferenceAttempt, cover_glue_inference_report};

/// Format a "proof-replay witnesses" section. The section is a static
/// listing of the P347 witness types and their purpose. It does
/// not run any inference; for cover-glue inference use
/// `proof_replay_witnesses_section_with_inference`.
pub fn proof_replay_witnesses_section() -> String {
    let mut lines: Vec<String> = Vec::new();
    lines.push("witnesses:".to_string());
    lines.push(
        "  witness: kind=ValuationAdditivityWitness, purpose=observed samples of v(x*y) == v(x) + v(y)"
            .to_string(),
    );
    lines.push(
        "  witness: kind=UltrametricWitness, purpose=observed samples of v(x+y) >= min(v(x), v(y))"
            .to_string(),
    );
    lines.push(
        "  witness: kind=PrecisionPreservationWitness, purpose=observed samples of precision labels preserved"
            .to_string(),
    );
    lines.push("  source: src/verify/witnesses.rs (P347)".to_string());
    lines.join("\n")
}

/// Format a "proof-replay cover-glue inference" section. Runs
/// the P348 inference report and summarizes passed/failed counts.
pub fn proof_replay_cover_glue_section<T: Clone + PartialEq>(
    cover: &Cover,
    sections: &SectionTable<T>,
) -> String {
    let report: CoverGlueInferenceReport = cover_glue_inference_report(cover, sections);
    let total = report.attempts.len();
    let inferred = report
        .attempts
        .iter()
        .filter(|a| matches!(a, InferenceAttempt::InferredMissingSection { .. }))
        .count();
    let resolved = report
        .attempts
        .iter()
        .filter(|a| matches!(a, InferenceAttempt::ResolvedOverlap { .. }))
        .count();
    let failed = report
        .attempts
        .iter()
        .filter(|a| matches!(a, InferenceAttempt::FailedRecovery { .. }))
        .count();
    let mut lines: Vec<String> = Vec::new();
    lines.push("cover_glue_inference:".to_string());
    lines.push(format!(
        "  cover_glue_inference_attempts: total={}, inferred={}, resolved={}, failed={}",
        total, inferred, resolved, failed
    ));
    lines.push(format!(
        "  cover_glue_inference_succeeded: {}",
        report.all_succeeded()
    ));
    lines.push("  source: src/verify/cover_glue_inference.rs (P348)".to_string());
    lines.join("\n")
}