karpal_verify/
session.rs

1use crate::{
2    ArtifactLayout, DryRunner, LeanConfig, LeanManifestReportFiles, LocalProcessRunner,
3    ObligationBundle, SmtConfig, VerificationReport, VerifierRunner, dry_run_bundle_artifacts,
4    dry_run_report, execute_report, write_bundle_artifacts,
5};
6#[cfg(feature = "amari")]
7use crate::{StatisticalVerification, ThreeTierVerificationReport, three_tier_report};
8use std::{fs, io, path::Path, string::String};
9
10/// Schema version for CI-oriented verification sidecar/report-file metadata.
11pub const VERIFICATION_SIDECAR_SCHEMA_VERSION: &str = "1";
12
13/// Default file stem used for CI-oriented verification summaries.
14pub const DEFAULT_REPORT_STEM: &str = "verification-report";
15
16/// Paths written for CI-oriented report summaries.
17#[derive(Debug, Clone, PartialEq, Eq)]
18pub struct ReportFiles {
19    pub json_path: String,
20    pub markdown_path: String,
21    pub lean_diagnostics_json_path: Option<String>,
22    pub lean_manifest_path: Option<String>,
23    pub three_tier_json_path: Option<String>,
24    pub three_tier_markdown_path: Option<String>,
25}
26
27/// End-to-end verification session configuration for a bundle.
28#[derive(Debug, Clone)]
29pub struct VerificationSession {
30    bundle: ObligationBundle,
31    layout: ArtifactLayout,
32    lean_module_name: String,
33    smt: SmtConfig,
34    lean: LeanConfig,
35    report_stem: String,
36    #[cfg(feature = "amari")]
37    statistical_verifications: Vec<StatisticalVerification>,
38}
39
40impl VerificationSession {
41    pub fn new(
42        bundle: ObligationBundle,
43        layout: ArtifactLayout,
44        lean_module_name: impl Into<String>,
45    ) -> Self {
46        Self {
47            bundle,
48            layout,
49            lean_module_name: lean_module_name.into(),
50            smt: SmtConfig::default(),
51            lean: LeanConfig::default(),
52            report_stem: DEFAULT_REPORT_STEM.into(),
53            #[cfg(feature = "amari")]
54            statistical_verifications: Vec::new(),
55        }
56    }
57
58    pub fn with_smt_config(mut self, smt: SmtConfig) -> Self {
59        self.smt = smt;
60        self
61    }
62
63    pub fn with_lean_config(mut self, lean: LeanConfig) -> Self {
64        self.lean = lean;
65        self
66    }
67
68    pub fn with_report_stem(mut self, report_stem: impl Into<String>) -> Self {
69        self.report_stem = report_stem.into();
70        self
71    }
72
73    #[cfg(feature = "amari")]
74    pub fn with_statistical_verification(mut self, verification: StatisticalVerification) -> Self {
75        self.statistical_verifications.push(verification);
76        self
77    }
78
79    #[cfg(feature = "amari")]
80    pub fn with_statistical_verifications(
81        mut self,
82        verifications: impl IntoIterator<Item = StatisticalVerification>,
83    ) -> Self {
84        self.statistical_verifications.extend(verifications);
85        self
86    }
87
88    pub fn bundle(&self) -> &ObligationBundle {
89        &self.bundle
90    }
91
92    pub fn layout(&self) -> &ArtifactLayout {
93        &self.layout
94    }
95
96    pub fn lean_module_name(&self) -> &str {
97        &self.lean_module_name
98    }
99
100    pub fn report_stem(&self) -> &str {
101        &self.report_stem
102    }
103
104    /// Build dry-run artifacts and return the attached verification report.
105    pub fn dry_run_report(&self) -> VerificationReport {
106        let artifacts = dry_run_bundle_artifacts(
107            &self.bundle,
108            &self.layout,
109            &self.lean_module_name,
110            &self.smt,
111            &self.lean,
112        );
113        dry_run_report(&self.bundle, &artifacts)
114    }
115
116    /// Build artifacts, execute plans, and return the resulting verification report.
117    pub fn verify_report(&self, runner: &impl VerifierRunner) -> io::Result<VerificationReport> {
118        let artifacts = write_bundle_artifacts(
119            &self.bundle,
120            &self.layout,
121            &self.lean_module_name,
122            &self.smt,
123            &self.lean,
124        )?;
125        Ok(execute_report(&self.bundle, &artifacts, runner))
126    }
127
128    /// Build artifacts, execute plans locally, and return the resulting verification report.
129    pub fn verify_local_report(&self) -> io::Result<VerificationReport> {
130        self.verify_report(&LocalProcessRunner)
131    }
132
133    /// Build artifacts, execute plans, and write JSON / Markdown summaries beside them.
134    pub fn verify_with_ci_outputs(
135        &self,
136        runner: &impl VerifierRunner,
137    ) -> io::Result<VerificationOutput> {
138        let artifacts = write_bundle_artifacts(
139            &self.bundle,
140            &self.layout,
141            &self.lean_module_name,
142            &self.smt,
143            &self.lean,
144        )?;
145        let report = execute_report(&self.bundle, &artifacts, runner);
146        let report_files = write_report_files(
147            &self.layout.root,
148            &self.report_stem,
149            &self.bundle,
150            &report,
151            artifacts.lean_manifest.as_ref(),
152            #[cfg(feature = "amari")]
153            &self.statistical_verifications,
154        )?;
155        Ok(VerificationOutput {
156            report,
157            report_files,
158        })
159    }
160
161    /// Build artifacts, execute plans locally, and write CI-oriented summaries.
162    pub fn verify_local_with_ci_outputs(&self) -> io::Result<VerificationOutput> {
163        self.verify_with_ci_outputs(&LocalProcessRunner)
164    }
165
166    /// Build artifacts via the real writer, then execute a dry-run runner.
167    pub fn verify_with_dry_runner(&self) -> io::Result<VerificationReport> {
168        self.verify_report(&DryRunner)
169    }
170}
171
172/// Report plus the CI-oriented files written beside generated artifacts.
173#[derive(Debug, Clone, PartialEq, Eq)]
174pub struct VerificationOutput {
175    pub report: VerificationReport,
176    pub report_files: ReportFiles,
177}
178
179/// One-shot orchestration helper.
180pub fn verify_bundle(
181    bundle: &ObligationBundle,
182    layout: &ArtifactLayout,
183    lean_module_name: &str,
184    smt: &SmtConfig,
185    lean: &LeanConfig,
186    runner: &impl VerifierRunner,
187) -> io::Result<VerificationReport> {
188    VerificationSession::new(bundle.clone(), layout.clone(), lean_module_name)
189        .with_smt_config(smt.clone())
190        .with_lean_config(lean.clone())
191        .verify_report(runner)
192}
193
194/// One-shot orchestration helper that also writes CI-oriented report files.
195pub fn verify_bundle_with_ci_outputs(
196    bundle: &ObligationBundle,
197    layout: &ArtifactLayout,
198    lean_module_name: &str,
199    smt: &SmtConfig,
200    lean: &LeanConfig,
201    runner: &impl VerifierRunner,
202) -> io::Result<VerificationOutput> {
203    VerificationSession::new(bundle.clone(), layout.clone(), lean_module_name)
204        .with_smt_config(smt.clone())
205        .with_lean_config(lean.clone())
206        .verify_with_ci_outputs(runner)
207}
208
209fn write_report_files(
210    root: impl AsRef<Path>,
211    report_stem: &str,
212    bundle: &ObligationBundle,
213    report: &VerificationReport,
214    lean_manifest: Option<&crate::artifact::LeanManifest>,
215    #[cfg(feature = "amari")] statistical_verifications: &[StatisticalVerification],
216) -> io::Result<ReportFiles> {
217    #[cfg(not(feature = "amari"))]
218    let _ = bundle;
219    let root = root.as_ref();
220    fs::create_dir_all(root)?;
221
222    let lean_manifest_path = report.lean_module.as_ref().map(|module| {
223        path_to_string(
224            &root
225                .join("lean")
226                .join(format!("{}.manifest.json", module.module_name)),
227        )
228    });
229
230    let lean_diagnostics_json_path = report
231        .lean_module
232        .as_ref()
233        .map(|_| -> io::Result<String> {
234            let path = root.join(format!("{report_stem}.lean-diagnostics.json"));
235            fs::write(&path, render_lean_diagnostics_json(report))?;
236            Ok(path_to_string(&path))
237        })
238        .transpose()?;
239
240    #[cfg(feature = "amari")]
241    let three_tier = (!statistical_verifications.is_empty())
242        .then(|| three_tier_report(bundle, statistical_verifications, Some(report)));
243    #[cfg(feature = "amari")]
244    let three_tier_json_path = if let Some(three_tier) = &three_tier {
245        let path = root.join(format!("{report_stem}.three-tier.json"));
246        fs::write(
247            &path,
248            render_three_tier_json_with_links(three_tier, report_stem, root),
249        )?;
250        Some(path_to_string(&path))
251    } else {
252        None
253    };
254    #[cfg(feature = "amari")]
255    let three_tier_markdown_path = if let Some(three_tier) = &three_tier {
256        let path = root.join(format!("{report_stem}.three-tier.md"));
257        fs::write(
258            &path,
259            render_three_tier_markdown_with_links(three_tier, report_stem, root),
260        )?;
261        Some(path_to_string(&path))
262    } else {
263        None
264    };
265    #[cfg(not(feature = "amari"))]
266    let three_tier_json_path = None;
267    #[cfg(not(feature = "amari"))]
268    let three_tier_markdown_path = None;
269
270    let json_path = root.join(format!("{report_stem}.json"));
271    let markdown_path = root.join(format!("{report_stem}.md"));
272    let report_files = ReportFiles {
273        json_path: path_to_string(&json_path),
274        markdown_path: path_to_string(&markdown_path),
275        lean_diagnostics_json_path,
276        lean_manifest_path,
277        three_tier_json_path,
278        three_tier_markdown_path,
279    };
280    fs::write(
281        &json_path,
282        render_report_json_with_links(report, &report_files),
283    )?;
284    fs::write(
285        &markdown_path,
286        render_report_markdown_with_links(report, &report_files),
287    )?;
288    if let (Some(path), Some(manifest)) = (&report_files.lean_manifest_path, lean_manifest) {
289        write_lean_manifest_with_report_links(path, manifest, &report_files)?;
290    }
291
292    Ok(report_files)
293}
294
295fn render_report_json_with_links(report: &VerificationReport, files: &ReportFiles) -> String {
296    let mut json = report.to_json();
297    if json.ends_with('}') {
298        json.pop();
299        json.push_str(",\"report_files\":{");
300        json.push_str(&format!(
301            "\"schema_version\":\"{}\",\"json_path\":\"{}\",\"markdown_path\":\"{}\"",
302            VERIFICATION_SIDECAR_SCHEMA_VERSION,
303            escape_json(&files.json_path),
304            escape_json(&files.markdown_path)
305        ));
306        if let Some(path) = &files.lean_diagnostics_json_path {
307            json.push_str(&format!(
308                ",\"lean_diagnostics_json_path\":\"{}\"",
309                escape_json(path)
310            ));
311        }
312        if let Some(path) = &files.lean_manifest_path {
313            json.push_str(&format!(
314                ",\"lean_manifest_path\":\"{}\"",
315                escape_json(path)
316            ));
317        }
318        if let Some(path) = &files.three_tier_json_path {
319            json.push_str(&format!(
320                ",\"three_tier_json_path\":\"{}\"",
321                escape_json(path)
322            ));
323        }
324        if let Some(path) = &files.three_tier_markdown_path {
325            json.push_str(&format!(
326                ",\"three_tier_markdown_path\":\"{}\"",
327                escape_json(path)
328            ));
329        }
330        json.push_str("}}");
331    }
332    json
333}
334
335fn render_report_markdown_with_links(report: &VerificationReport, files: &ReportFiles) -> String {
336    let mut markdown = report.to_markdown();
337    markdown.push_str("\nReport files:\n");
338    markdown.push_str(&format!(
339        "- Schema version: `{}`\n",
340        VERIFICATION_SIDECAR_SCHEMA_VERSION
341    ));
342    markdown.push_str(&format!("- JSON: `{}`\n", files.json_path));
343    markdown.push_str(&format!("- Markdown: `{}`\n", files.markdown_path));
344    if let Some(path) = &files.lean_diagnostics_json_path {
345        markdown.push_str(&format!("- Lean diagnostics JSON: `{}`\n", path));
346    }
347    if let Some(path) = &files.lean_manifest_path {
348        markdown.push_str(&format!("- Lean manifest: `{}`\n", path));
349    }
350    if let Some(path) = &files.three_tier_json_path {
351        markdown.push_str(&format!("- Three-tier JSON: `{}`\n", path));
352    }
353    if let Some(path) = &files.three_tier_markdown_path {
354        markdown.push_str(&format!("- Three-tier Markdown: `{}`\n", path));
355    }
356    markdown
357}
358
359#[cfg(feature = "amari")]
360fn render_three_tier_json_with_links(
361    report: &ThreeTierVerificationReport,
362    report_stem: &str,
363    root: &Path,
364) -> String {
365    let mut json = report.to_json();
366    if json.ends_with('}') {
367        json.pop();
368        json.push_str(",\"report_files\":{");
369        json.push_str(&format!(
370            "\"schema_version\":\"{}\",\"json_path\":\"{}\",\"markdown_path\":\"{}\"",
371            VERIFICATION_SIDECAR_SCHEMA_VERSION,
372            escape_json(&path_to_string(
373                &root.join(format!("{report_stem}.three-tier.json"))
374            )),
375            escape_json(&path_to_string(
376                &root.join(format!("{report_stem}.three-tier.md"))
377            ))
378        ));
379        json.push_str("}}");
380    }
381    json
382}
383
384#[cfg(feature = "amari")]
385fn render_three_tier_markdown_with_links(
386    report: &ThreeTierVerificationReport,
387    report_stem: &str,
388    root: &Path,
389) -> String {
390    let mut markdown = report.to_markdown();
391    markdown.push_str("\nReport files:\n");
392    markdown.push_str(&format!(
393        "- Schema version: `{}`\n",
394        VERIFICATION_SIDECAR_SCHEMA_VERSION
395    ));
396    markdown.push_str(&format!(
397        "- JSON: `{}`\n",
398        path_to_string(&root.join(format!("{report_stem}.three-tier.json")))
399    ));
400    markdown.push_str(&format!(
401        "- Markdown: `{}`\n",
402        path_to_string(&root.join(format!("{report_stem}.three-tier.md")))
403    ));
404    markdown
405}
406
407fn escape_json(s: &str) -> String {
408    s.replace('\\', "\\\\")
409        .replace('"', "\\\"")
410        .replace('\n', "\\n")
411}
412
413fn write_lean_manifest_with_report_links(
414    manifest_path: &str,
415    manifest: &crate::artifact::LeanManifest,
416    files: &ReportFiles,
417) -> io::Result<()> {
418    let manifest = manifest.clone().with_report_files({
419        let report_files =
420            LeanManifestReportFiles::new(files.json_path.clone(), files.markdown_path.clone());
421        match &files.lean_diagnostics_json_path {
422            Some(path) => report_files.with_lean_diagnostics_json_path(path.clone()),
423            None => report_files,
424        }
425    });
426    fs::write(manifest_path, manifest.to_json())
427}
428
429fn render_lean_diagnostics_json(report: &VerificationReport) -> String {
430    fn esc(s: &str) -> String {
431        s.replace('\\', "\\\\")
432            .replace('"', "\\\"")
433            .replace('\n', "\\n")
434    }
435
436    let module = match &report.lean_module {
437        Some(module) => module,
438        None => return "null".into(),
439    };
440
441    let obligation_entries = report
442        .obligations
443        .iter()
444        .filter(|obligation| {
445            obligation.lean_theorem_ref.is_some() || !obligation.lean_diagnostics.is_empty()
446        })
447        .map(|obligation| {
448            let diagnostics = obligation
449                .lean_diagnostics
450                .iter()
451                .map(|diagnostic| format!("\"{}\"", esc(diagnostic)))
452                .collect::<Vec<_>>()
453                .join(",");
454            format!(
455                "{{\"obligation_name\":\"{}\",\"theorem_ref\":{},\"diagnostics\":[{}]}}",
456                esc(&obligation.obligation_name),
457                obligation
458                    .lean_theorem_ref
459                    .as_ref()
460                    .map(|theorem_ref| format!("\"{}\"", esc(theorem_ref)))
461                    .unwrap_or_else(|| "null".into()),
462                diagnostics
463            )
464        })
465        .collect::<Vec<_>>()
466        .join(",");
467
468    let module_diagnostics = module
469        .diagnostics
470        .iter()
471        .map(|diagnostic| format!("\"{}\"", esc(diagnostic)))
472        .collect::<Vec<_>>()
473        .join(",");
474    let theorem_failures = module
475        .theorem_failures
476        .iter()
477        .map(|failure| format!("\"{}\"", esc(failure)))
478        .collect::<Vec<_>>()
479        .join(",");
480
481    format!(
482        "{{\"schema_version\":\"{}\",\"module_name\":\"{}\",\"module_diagnostics\":[{}],\"theorem_failures\":[{}],\"obligations\":[{}]}}",
483        VERIFICATION_SIDECAR_SCHEMA_VERSION,
484        esc(&module.module_name),
485        module_diagnostics,
486        theorem_failures,
487        obligation_entries
488    )
489}
490
491fn path_to_string(path: &Path) -> String {
492    path.to_string_lossy().into_owned()
493}
494
495#[cfg(test)]
496mod tests {
497    use super::*;
498    use crate::{
499        AlgebraicSignature, ExecutionResult, ExecutionStatus, LeanDiagnostic, LeanOutput, Origin,
500        SmtOutput, Sort,
501    };
502    #[cfg(feature = "amari")]
503    use crate::{StatisticalBound, verify_rare_event};
504
505    fn sample_session(root: &Path) -> VerificationSession {
506        let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
507        let bundle = ObligationBundle::monoid(
508            "sum_monoid",
509            Origin::new("karpal-core", "Monoid for Sum<i32>"),
510            &sig,
511        );
512
513        VerificationSession::new(bundle, ArtifactLayout::new(root), "KarpalVerify")
514    }
515
516    struct SuccessRunner;
517
518    impl VerifierRunner for SuccessRunner {
519        fn run(&self, plan: &crate::InvocationPlan) -> ExecutionResult {
520            ExecutionResult {
521                plan: plan.clone(),
522                status: match plan.kind {
523                    crate::CommandKind::Smt => ExecutionStatus::Unsat,
524                    crate::CommandKind::Lean | crate::CommandKind::Kani => ExecutionStatus::Success,
525                },
526                stdout: String::new(),
527                stderr: String::new(),
528                exit_code: Some(0),
529                backend_version: Some("tool 1.0".into()),
530                smt_output: Some(SmtOutput {
531                    status: Some(ExecutionStatus::Unsat),
532                    model: None,
533                    reason_unknown: None,
534                }),
535                lean_output: (plan.kind == crate::CommandKind::Lean).then(|| LeanOutput {
536                    diagnostics: vec![LeanDiagnostic {
537                        file: Some("lean/KarpalVerify.lean".into()),
538                        line: Some(4),
539                        column: Some(2),
540                        severity: "warning".into(),
541                        message: "declaration uses sorry: associativity".into(),
542                        theorem_hits: vec!["associativity".into()],
543                    }],
544                    theorem_hits: vec!["associativity".into()],
545                }),
546            }
547        }
548    }
549
550    #[test]
551    fn dry_run_report_orchestrates_artifacts_and_report() {
552        let session = sample_session(Path::new("target/karpal-verify-session-dry-run"));
553        let report = session.dry_run_report();
554
555        assert_eq!(report.obligation_count(), 3);
556        assert_eq!(report.root, "target/karpal-verify-session-dry-run");
557        assert!(
558            report
559                .obligations
560                .iter()
561                .all(|entry| entry.status() == Some(ExecutionStatus::DryRun))
562        );
563    }
564
565    #[test]
566    fn verify_report_builds_artifacts_runs_plans_and_returns_report() {
567        let temp = std::env::temp_dir().join("karpal_verify_session_report_test");
568        if temp.exists() {
569            let _ = fs::remove_dir_all(&temp);
570        }
571
572        let session = sample_session(&temp);
573        let report = session
574            .verify_report(&SuccessRunner)
575            .expect("session verification should succeed");
576        assert!(report.is_success());
577        assert!(temp.join("smt").exists());
578        assert!(temp.join("lean").exists());
579        assert_eq!(
580            report
581                .lean_module
582                .as_ref()
583                .map(|module| module.theorem_failures.clone()),
584            Some(vec!["KarpalVerify.associativity".into()])
585        );
586
587        let _ = fs::remove_dir_all(&temp);
588    }
589
590    #[test]
591    fn verify_with_ci_outputs_writes_reports_beside_artifacts() {
592        let temp = std::env::temp_dir().join("karpal_verify_session_ci_output_test");
593        if temp.exists() {
594            let _ = fs::remove_dir_all(&temp);
595        }
596
597        let output = sample_session(&temp)
598            .with_report_stem("summary")
599            .verify_with_ci_outputs(&SuccessRunner)
600            .expect("ci outputs should be written");
601
602        assert!(output.report.is_success());
603        assert!(Path::new(&output.report_files.json_path).exists());
604        assert!(Path::new(&output.report_files.markdown_path).exists());
605        assert!(
606            Path::new(
607                output
608                    .report_files
609                    .lean_diagnostics_json_path
610                    .as_deref()
611                    .expect("lean diagnostics sidecar should be written")
612            )
613            .exists()
614        );
615        assert!(
616            Path::new(
617                output
618                    .report_files
619                    .lean_manifest_path
620                    .as_deref()
621                    .expect("lean manifest path should be recorded")
622            )
623            .exists()
624        );
625        assert!(output.report_files.json_path.ends_with("summary.json"));
626        assert!(output.report_files.markdown_path.ends_with("summary.md"));
627        #[cfg(not(feature = "amari"))]
628        {
629            assert!(output.report_files.three_tier_json_path.is_none());
630            assert!(output.report_files.three_tier_markdown_path.is_none());
631        }
632        assert!(
633            output
634                .report_files
635                .lean_diagnostics_json_path
636                .as_deref()
637                .unwrap()
638                .ends_with("summary.lean-diagnostics.json")
639        );
640        assert!(
641            output
642                .report_files
643                .lean_manifest_path
644                .as_deref()
645                .unwrap()
646                .ends_with("lean/KarpalVerify.manifest.json")
647        );
648
649        let json = fs::read_to_string(&output.report_files.json_path)
650            .expect("summary json should be readable");
651        let markdown = fs::read_to_string(&output.report_files.markdown_path)
652            .expect("summary markdown should be readable");
653        let sidecar = fs::read_to_string(
654            output
655                .report_files
656                .lean_diagnostics_json_path
657                .as_deref()
658                .expect("lean diagnostics sidecar path should be present"),
659        )
660        .expect("lean diagnostics sidecar should be readable");
661        let manifest = fs::read_to_string(
662            output
663                .report_files
664                .lean_manifest_path
665                .as_deref()
666                .expect("lean manifest path should be present"),
667        )
668        .expect("lean manifest should be readable");
669        assert!(json.contains("\"schema_version\":\"1\""));
670        assert!(json.contains("\"report_files\""));
671        assert!(json.contains("\"lean_manifest_path\""));
672        assert!(json.contains("\"lean_diagnostics_json_path\""));
673        assert!(json.contains("\"schema_version\":\"1\",\"json_path\""));
674        assert!(markdown.contains("Report files:"));
675        assert!(markdown.contains("Schema version: `1`"));
676        assert!(markdown.contains("Lean diagnostics JSON"));
677        assert!(markdown.contains("Lean manifest"));
678        assert!(sidecar.contains("\"schema_version\":\"1\""));
679        assert!(manifest.contains("\"schema_version\":\"1\""));
680        assert!(manifest.contains("\"report_files\""));
681        assert!(manifest.contains("\"json_path\""));
682        assert!(manifest.contains("\"markdown_path\""));
683        assert!(manifest.contains("\"lean_diagnostics_json_path\""));
684
685        let _ = fs::remove_dir_all(&temp);
686    }
687
688    #[cfg(feature = "amari")]
689    #[test]
690    fn verify_with_ci_outputs_writes_three_tier_sidecars_when_statistical_evidence_exists() {
691        let temp = std::env::temp_dir().join("karpal_verify_session_three_tier_test");
692        if temp.exists() {
693            let _ = fs::remove_dir_all(&temp);
694        }
695
696        let bundle = sample_session(&temp).bundle().clone();
697        let statistical = verify_rare_event(
698            &bundle.obligations()[0],
699            &StatisticalBound::new(0.05).with_samples(128),
700            || false,
701        );
702
703        let output = sample_session(&temp)
704            .with_report_stem("summary")
705            .with_statistical_verification(statistical)
706            .verify_with_ci_outputs(&DryRunner)
707            .expect("ci outputs should be written");
708
709        let three_tier_json_path = output
710            .report_files
711            .three_tier_json_path
712            .as_deref()
713            .expect("three-tier json should be written");
714        let three_tier_markdown_path = output
715            .report_files
716            .three_tier_markdown_path
717            .as_deref()
718            .expect("three-tier markdown should be written");
719        assert!(Path::new(three_tier_json_path).exists());
720        assert!(Path::new(three_tier_markdown_path).exists());
721        assert!(three_tier_json_path.ends_with("summary.three-tier.json"));
722        assert!(three_tier_markdown_path.ends_with("summary.three-tier.md"));
723
724        let json = fs::read_to_string(three_tier_json_path).expect("three-tier json readable");
725        let markdown =
726            fs::read_to_string(three_tier_markdown_path).expect("three-tier markdown readable");
727        let main_json =
728            fs::read_to_string(&output.report_files.json_path).expect("main report json readable");
729        let main_markdown = fs::read_to_string(&output.report_files.markdown_path)
730            .expect("main report markdown readable");
731
732        assert!(json.contains("\"impossible_count\":1"));
733        assert!(json.contains("\"external_count\":2"));
734        assert!(json.contains("\"report_files\""));
735        assert!(markdown.contains("Three-Tier Verification Report"));
736        assert!(markdown.contains("Schema version: `1`"));
737        assert!(main_json.contains("\"three_tier_json_path\""));
738        assert!(main_json.contains("\"three_tier_markdown_path\""));
739        assert!(main_markdown.contains("Three-tier JSON"));
740        assert!(main_markdown.contains("Three-tier Markdown"));
741
742        let _ = fs::remove_dir_all(&temp);
743    }
744}
karpal_verify/session.rs

karpal_verify/
session.rs
