use crate::properties::PropertyResult; use super::properties::GossipMetrics; // ── Public API ────────────────────────────────────────────────────────────── /// A named scenario with its metrics and property results. pub struct ScenarioReport { pub name: String, pub description: String, pub metrics: GossipMetrics, pub results: Vec, } /// A section groups related scenarios under a category heading. pub struct ReportSection { pub title: String, pub explanation: String, pub scenarios: Vec, } /// Data for the scalability scatter plot. pub struct ScalingPoint { pub n: usize, pub convergence_round: Option, pub total_pushes: usize, pub label: String, } /// Full report data. pub struct PropertyReportData { pub sections: Vec, pub scaling_points_st: Vec, pub scaling_points_mt: Vec, pub thread_comparison: Vec, /// All convergence curves keyed by scenario name, for the multi-line overlay. pub convergence_overlays: Vec<(String, Vec)>, } pub struct ThreadComparison { pub label: String, pub num_threads: usize, pub convergence_round: Option, pub total_pushes: usize, } /// Generate a self-contained HTML report from the collected data. pub fn generate_property_report(data: &PropertyReportData) -> String { let mut html = String::with_capacity(128_000); html.push_str("\n\n\n\n"); html.push_str("Gossip Protocol Property Verification Report\n"); html.push_str("\n\n\n"); html.push_str("

Gossip Protocol Property Verification Report

\n"); // Executive summary. render_executive_summary(&mut html, data); // Per-section content. for section in &data.sections { render_section(&mut html, section); } // Convergence overlay chart. if !data.convergence_overlays.is_empty() { render_convergence_overlay(&mut html, &data.convergence_overlays); } // Scalability charts. if !data.scaling_points_st.is_empty() { render_scalability_section(&mut html, data); } // Thread comparison. if !data.thread_comparison.is_empty() { render_thread_comparison(&mut html, &data.thread_comparison); } html.push_str("\n\n"); html } // ── CSS ───────────────────────────────────────────────────────────────────── const CSS: &str = r#" body { font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, sans-serif; max-width: 1400px; margin: 0 auto; padding: 20px; background: #fafafa; color: #222; } h1 { border-bottom: 3px solid #333; padding-bottom: 8px; } h2 { margin-top: 40px; color: #333; border-bottom: 2px solid #ddd; padding-bottom: 4px; } h3 { color: #555; margin-top: 24px; } .summary-grid { display: flex; flex-wrap: wrap; gap: 16px; margin: 16px 0; } .summary-card { background: #fff; border: 1px solid #ddd; border-radius: 8px; padding: 16px 24px; min-width: 160px; } .summary-card .label { font-size: 0.85em; color: #666; } .summary-card .value { font-size: 1.8em; font-weight: bold; } .badge-pass { display: inline-block; padding: 4px 12px; border-radius: 12px; background: #28a745; color: #fff; font-weight: bold; font-size: 0.9em; } .badge-fail { display: inline-block; padding: 4px 12px; border-radius: 12px; background: #dc3545; color: #fff; font-weight: bold; font-size: 0.9em; } .badge-partial { display: inline-block; padding: 4px 12px; border-radius: 12px; background: #ffc107; color: #333; font-weight: bold; font-size: 0.9em; } table { border-collapse: collapse; width: 100%; margin: 12px 0; } th, td { border: 1px solid #ddd; padding: 8px 12px; text-align: left; font-size: 0.9em; } th { background: #f0f0f0; } tr:nth-child(even) { background: #fafafa; } .pass { color: #28a745; font-weight: bold; } .fail { color: #dc3545; font-weight: bold; } svg { display: block; margin: 12px 0; } .explanation { color: #555; margin: 8px 0 16px 0; line-height: 1.5; } .scenario-desc { color: #777; font-style: italic; margin: 4px 0 8px 0; } "#; // ── Executive summary ─────────────────────────────────────────────────────── fn render_executive_summary(html: &mut String, data: &PropertyReportData) { html.push_str("

Executive Summary

\n"); let mut total_pass = 0usize; let mut total_fail = 0usize; for section in &data.sections { for scenario in §ion.scenarios { for r in &scenario.results { if r.passed { total_pass += 1; } else { total_fail += 1; } } } } let total = total_pass + total_fail; let badge = if total_fail == 0 { "ALL PASSED" } else if total_pass == 0 { "ALL FAILED" } else { "PARTIAL" }; html.push_str("

\n"); summary_card(html, "Total Checks", &total.to_string()); summary_card(html, "Passed", &total_pass.to_string()); summary_card(html, "Failed", &total_fail.to_string()); html.push_str(&format!( "

Verdict

{badge}

\n" )); html.push_str("

\n"); } fn summary_card(html: &mut String, label: &str, value: &str) { html.push_str(&format!( "

{label}

{value}

\n" )); } // ── Section rendering ─────────────────────────────────────────────────────── fn render_section(html: &mut String, section: &ReportSection) { html.push_str(&format!("

{}

\n", esc(§ion.title))); html.push_str(&format!( "

{}

\n", esc(§ion.explanation) )); for scenario in §ion.scenarios { html.push_str(&format!("

{}

\n", esc(&scenario.name))); html.push_str(&format!( "

{}

\n", esc(&scenario.description) )); // Results table. html.push_str("\n\n"); for r in &scenario.results { let status = if r.passed { "PASS" } else { "FAIL" }; html.push_str(&format!( "\n", esc(&r.name), esc(&r.expected), esc(&r.actual), esc(&r.description), )); } html.push_str("

Property	Status	Expected	Actual	Description
{}	{status}	{}	{}	{}

\n"); // Inline SVG graph for this scenario based on category. render_scenario_graph(html, section, scenario); } } // ── Per-scenario graphs ───────────────────────────────────────────────────── fn render_scenario_graph(html: &mut String, section: &ReportSection, scenario: &ScenarioReport) { let m = &scenario.metrics; match section.title.as_str() { "Convergence" | "Fault Tolerance" => { render_convergence_curve_svg(html, &scenario.name, &m.convergence_curve); } "Consistency" => { render_entropy_chart(html, &m.entropy_per_round); } "Practical" => { render_state_size_chart(html, &m.avg_state_size_per_round); } "Bandwidth/Load" => { render_load_bar_chart(html, m); } "Message Complexity" => { render_message_stacked_bar(html, m); } "Peer Selection" => { render_peer_histogram(html, m); } _ => {} } } // ── SVG chart helpers ─────────────────────────────────────────────────────── const CHART_W: f64 = 700.0; const CHART_H: f64 = 280.0; const ML: f64 = 60.0; // margin left const MR: f64 = 20.0; const MT: f64 = 20.0; const MB: f64 = 50.0; fn svg_open(html: &mut String, w: f64, h: f64) { html.push_str(&format!( "\n"); } fn draw_axes(html: &mut String) { let bx = ML; let by = MT + CHART_H; let rx = ML + CHART_W - ML; html.push_str(&format!( "\n" )); html.push_str(&format!( "\n" )); } fn y_for(val: f64, max_val: f64) -> f64 { if max_val < 1e-9 { return MT + CHART_H; } MT + CHART_H - (val / max_val) * CHART_H } fn x_for(idx: usize, total: usize) -> f64 { if total == 0 { return ML; } ML + (idx as f64 + 0.5) / total as f64 * (CHART_W - ML - MR) } // ── Convergence curve SVG ─────────────────────────────────────────────────── fn render_convergence_curve_svg(html: &mut String, _name: &str, curve: &[f64]) { if curve.is_empty() { return; } let total_w = CHART_W + MR; let total_h = CHART_H + MT + MB; svg_open(html, total_w, total_h); draw_axes(html); // Y-axis labels (0% to 100%). for pct in [0, 25, 50, 75, 100] { let y = y_for(pct as f64 / 100.0, 1.0); html.push_str(&format!( "{pct}%\n", ML - 6.0, y + 3.0, )); html.push_str(&format!( "\n", ML + CHART_W - ML - MR, )); } // X-axis labels. let step = (curve.len() / 10).max(1); for r in (0..curve.len()).step_by(step) { let x = x_for(r, curve.len()); html.push_str(&format!( "{}\n", MT + CHART_H + 16.0, r + 1, )); } // Line. let mut path = String::new(); for (i, &v) in curve.iter().enumerate() { let x = x_for(i, curve.len()); let y = y_for(v, 1.0); if i == 0 { path.push_str(&format!("M{x:.1},{y:.1}")); } else { path.push_str(&format!(" L{x:.1},{y:.1}")); } } html.push_str(&format!( "\n" )); // Dots. let dot_step = (curve.len() / 30).max(1); for (i, &v) in curve.iter().enumerate() { if i % dot_step == 0 { let x = x_for(i, curve.len()); let y = y_for(v, 1.0); html.push_str(&format!( "\n" )); } } svg_close(html); } // ── Multi-line convergence overlay ────────────────────────────────────────── fn render_convergence_overlay(html: &mut String, curves: &[(String, Vec)]) { html.push_str("

Convergence Comparison (All Topologies)

\n"); html.push_str("

Overlay of convergence curves across different topologies at scale.

\n"); let max_len = curves.iter().map(|(_, c)| c.len()).max().unwrap_or(0); if max_len == 0 { return; } let total_w = CHART_W + MR; let total_h = CHART_H + MT + MB + 40.0; // extra for legend svg_open(html, total_w, total_h); draw_axes(html); let colors = ["#4a90d9", "#d94a4a", "#4ad94a", "#d9a64a", "#9a4ad9", "#4ad9d9"]; for pct in [0, 25, 50, 75, 100] { let y = y_for(pct as f64 / 100.0, 1.0); html.push_str(&format!( "{pct}%\n", ML - 6.0, y + 3.0, )); } for (ci, (name, curve)) in curves.iter().enumerate() { let color = colors[ci % colors.len()]; let mut path = String::new(); for (i, &v) in curve.iter().enumerate() { let x = x_for(i, max_len); let y = y_for(v, 1.0); if i == 0 { path.push_str(&format!("M{x:.1},{y:.1}")); } else { path.push_str(&format!(" L{x:.1},{y:.1}")); } } html.push_str(&format!( "\n" )); // Legend entry. let lx = ML + ci as f64 * 140.0; let ly = MT + CHART_H + 36.0; html.push_str(&format!( "\n" )); html.push_str(&format!( "{name}\n", lx + 18.0, ly + 9.0, )); } svg_close(html); } // ── Entropy chart ─────────────────────────────────────────────────────────── fn render_entropy_chart(html: &mut String, entropy: &[usize]) { if entropy.is_empty() { return; } let max_e = *entropy.iter().max().unwrap_or(&1) as f64; let total_w = CHART_W + MR; let total_h = CHART_H + MT + MB; svg_open(html, total_w, total_h); draw_axes(html); html.push_str(&format!( "{}\n", ML - 6.0, MT + 3.0, max_e as usize, )); html.push_str(&format!( "0\n", ML - 6.0, MT + CHART_H + 3.0, )); let mut path = String::new(); for (i, &e) in entropy.iter().enumerate() { let x = x_for(i, entropy.len()); let y = y_for(e as f64, max_e); if i == 0 { path.push_str(&format!("M{x:.1},{y:.1}")); } else { path.push_str(&format!(" L{x:.1},{y:.1}")); } } html.push_str(&format!( "\n" )); svg_close(html); } // ── State size chart ──────────────────────────────────────────────────────── fn render_state_size_chart(html: &mut String, sizes: &[f64]) { if sizes.is_empty() { return; } let max_s = sizes.iter().cloned().fold(0.0f64, f64::max).max(1.0); let total_w = CHART_W + MR; let total_h = CHART_H + MT + MB; svg_open(html, total_w, total_h); draw_axes(html); html.push_str(&format!( "{:.1}\n", ML - 6.0, MT + 3.0, max_s, )); let mut path = String::new(); for (i, &s) in sizes.iter().enumerate() { let x = x_for(i, sizes.len()); let y = y_for(s, max_s); if i == 0 { path.push_str(&format!("M{x:.1},{y:.1}")); } else { path.push_str(&format!(" L{x:.1},{y:.1}")); } } html.push_str(&format!( "\n" )); svg_close(html); } // ── Load bar chart ────────────────────────────────────────────────────────── fn render_load_bar_chart(html: &mut String, metrics: &GossipMetrics) { let mut nodes: Vec<(&String, usize)> = metrics .pushes_received_per_node .iter() .map(|(n, &c)| (n, c)) .collect(); nodes.sort_by(|a, b| b.1.cmp(&a.1)); // Show top 20 nodes. nodes.truncate(20); if nodes.is_empty() { return; } let max_v = nodes[0].1 as f64; let bar_h = 18.0; let gap = 4.0; let total_h = MT + (bar_h + gap) * nodes.len() as f64 + MB; let total_w = CHART_W + MR; svg_open(html, total_w, total_h); for (i, (name, count)) in nodes.iter().enumerate() { let y = MT + i as f64 * (bar_h + gap); let w = if max_v > 0.0 { (*count as f64 / max_v) * (CHART_W - ML - MR - 40.0) } else { 0.0 }; html.push_str(&format!( "{name}\n", ML - 4.0, y + bar_h - 4.0, )); html.push_str(&format!( "\n" )); html.push_str(&format!( "{count}\n", ML + w + 4.0, y + bar_h - 4.0, )); } svg_close(html); } // ── Message stacked bar ───────────────────────────────────────────────────── fn render_message_stacked_bar(html: &mut String, metrics: &GossipMetrics) { let useful = metrics.total_pushes - metrics.redundant_pushes; let redundant = metrics.redundant_pushes; let total = metrics.total_pushes.max(1) as f64; let total_w = 400.0; let total_h = 80.0; svg_open(html, total_w, total_h); let bar_w = 300.0; let bar_h = 30.0; let y = 20.0; let x = 60.0; let useful_w = (useful as f64 / total) * bar_w; let redundant_w = (redundant as f64 / total) * bar_w; html.push_str(&format!( "\n" )); html.push_str(&format!( "\n", x + useful_w, )); // Legend. let ly = y + bar_h + 16.0; html.push_str(&format!( "\n" )); html.push_str(&format!( "Useful ({useful})\n", x + 16.0, ly + 9.0, )); html.push_str(&format!( "\n", x + 140.0, )); html.push_str(&format!( "Redundant ({redundant})\n", x + 156.0, ly + 9.0, )); svg_close(html); } // ── Peer selection histogram ──────────────────────────────────────────────── fn render_peer_histogram(html: &mut String, metrics: &GossipMetrics) { // Aggregate: for each target, total selection count across all nodes. let mut target_totals: std::collections::HashMap = std::collections::HashMap::new(); for targets in metrics.peer_selection_distribution.values() { for (target, &count) in targets { *target_totals.entry(target.clone()).or_default() += count; } } let mut sorted: Vec<(String, usize)> = target_totals.into_iter().collect(); sorted.sort_by(|a, b| a.0.cmp(&b.0)); if sorted.is_empty() { return; } let max_v = sorted.iter().map(|(_, c)| *c).max().unwrap_or(1) as f64; let bar_w = 30.0; let gap = 4.0; let total_w = ML + (bar_w + gap) * sorted.len() as f64 + MR; let total_h = CHART_H + MT + MB; svg_open(html, total_w, total_h); // Axes. let base_y = MT + CHART_H; html.push_str(&format!( "\n" )); html.push_str(&format!( "\n", total_w - MR, )); for (i, (name, count)) in sorted.iter().enumerate() { let x = ML + i as f64 * (bar_w + gap); let h = (*count as f64 / max_v) * CHART_H; let y = base_y - h; html.push_str(&format!( "\n" )); // Label. html.push_str(&format!( "{name}\n", x + bar_w / 2.0, base_y + 14.0, x + bar_w / 2.0, base_y + 14.0, )); // Count on top. html.push_str(&format!( "{count}\n", x + bar_w / 2.0, y - 3.0, )); } svg_close(html); } // ── Scalability section ───────────────────────────────────────────────────── fn render_scalability_section(html: &mut String, data: &PropertyReportData) { html.push_str("

Scalability

\n"); html.push_str("

How convergence time and message count scale with network size.

\n"); // Convergence round vs N (with O(log N) reference). html.push_str("

Convergence Time vs Network Size

\n"); render_scaling_scatter( html, &data.scaling_points_st, &data.scaling_points_mt, true, ); // Total messages vs N (with O(N) reference). html.push_str("

Total Messages vs Network Size

\n"); render_scaling_scatter( html, &data.scaling_points_st, &data.scaling_points_mt, false, ); } fn render_scaling_scatter( html: &mut String, st_points: &[ScalingPoint], mt_points: &[ScalingPoint], is_convergence: bool, ) { let all_n: Vec = st_points .iter() .chain(mt_points.iter()) .map(|p| p.n) .collect(); let all_y: Vec = st_points .iter() .chain(mt_points.iter()) .map(|p| { if is_convergence { p.convergence_round.unwrap_or(0) as f64 } else { p.total_pushes as f64 } }) .collect(); if all_n.is_empty() { return; } let max_n = *all_n.iter().max().unwrap() as f64; let max_y = all_y.iter().cloned().fold(0.0f64, f64::max).max(1.0); let total_w = CHART_W + MR; let total_h = CHART_H + MT + MB + 30.0; svg_open(html, total_w, total_h); draw_axes(html); // Reference line. let ref_color = "#ccc"; let ref_points = 50; let mut ref_path = String::new(); for i in 0..=ref_points { let n = (i as f64 / ref_points as f64) * max_n; let ref_y_val = if is_convergence { // O(log N) reference scaled to fit. if n > 1.0 { (n.ln() / max_n.ln()) * max_y } else { 0.0 } } else { // O(N) reference. (n / max_n) * max_y }; let x = ML + (n / max_n) * (CHART_W - ML - MR); let y = y_for(ref_y_val, max_y); if i == 0 { ref_path.push_str(&format!("M{x:.1},{y:.1}")); } else { ref_path.push_str(&format!(" L{x:.1},{y:.1}")); } } html.push_str(&format!( "\n" )); let ref_label = if is_convergence { "O(log N)" } else { "O(N)" }; html.push_str(&format!( "{ref_label}\n", ML + CHART_W - ML - MR - 50.0, MT + 14.0, )); // Single-threaded points. for p in st_points { let x = ML + (p.n as f64 / max_n) * (CHART_W - ML - MR); let yv = if is_convergence { p.convergence_round.unwrap_or(0) as f64 } else { p.total_pushes as f64 }; let y = y_for(yv, max_y); html.push_str(&format!( "\n" )); } // Multi-threaded points. for p in mt_points { let x = ML + (p.n as f64 / max_n) * (CHART_W - ML - MR); let yv = if is_convergence { p.convergence_round.unwrap_or(0) as f64 } else { p.total_pushes as f64 }; let y = y_for(yv, max_y); html.push_str(&format!( "\n" )); } // Legend. let ly = MT + CHART_H + 30.0; html.push_str(&format!( "\n" )); html.push_str(&format!( "Single-threaded\n", ML + 10.0, ly + 4.0, )); html.push_str(&format!( "\n", ML + 130.0, )); html.push_str(&format!( "Multi-threaded\n", ML + 140.0, ly + 4.0, )); svg_close(html); } // ── Thread comparison ─────────────────────────────────────────────────────── fn render_thread_comparison(html: &mut String, comparisons: &[ThreadComparison]) { html.push_str("

Thread-Mode Comparison

\n"); html.push_str("

Comparing convergence time and message counts across different thread configurations.

\n"); html.push_str("\n\n"); for tc in comparisons { html.push_str(&format!( "\n", esc(&tc.label), tc.num_threads, tc.convergence_round .map(|r| r.to_string()) .unwrap_or("never".into()), tc.total_pushes, )); } html.push_str("

Configuration	Threads	Convergence Round	Total Pushes
{}	{}	{}	{}

\n"); } // ── HTML escape ───────────────────────────────────────────────────────────── fn esc(s: &str) -> String { s.replace('&', "&") .replace('<', "<") .replace('>', ">") .replace('"', """) }