Skip to main content

asupersync/audit/
proof_traffic_blocked_loop_e2e.rs

1//! Deterministic blocked proof-loop e2e packet (PROOF-TRAFFIC A5).
2//!
3//! This module composes the A2 admission receipt, A3 clean-overlay handshake,
4//! and A4 parking lot into one replayable, deterministic scenario. It is not a
5//! live runner: callers provide fixtures, the module renders structured logs and
6//! handoff bodies, and no path starts Cargo, shells out, creates branches,
7//! creates worktrees, deletes files, or treats live RCH fleet state as proof.
8
9use super::clean_overlay_planner::{
10    CleanOverlayRequest, PathChange, ReservationLease, WorkingTreeEntry,
11};
12use super::proof_traffic_overlay_handshake::{
13    ProofTrafficOverlayCapability, ProofTrafficOverlayHandshake, ProofTrafficOverlayHandshakeInput,
14};
15use super::proof_traffic_parking_lot::{
16    ParkedProofAttempt, ProofTrafficParkingLot, ProofTrafficRetryPredicate,
17};
18use super::proof_traffic_receipt::{
19    ProofTrafficActiveBuild, ProofTrafficAdmissionInput, ProofTrafficAdmissionReceipt,
20    ProofTrafficBuildOwner, ProofTrafficCapabilityProbe, ProofTrafficDecision, ProofTrafficIntent,
21    ProofTrafficQueueSnapshot,
22};
23use serde::{Deserialize, Serialize};
24use std::collections::BTreeSet;
25
26/// Stable schema version for the A5 blocked-loop e2e packet.
27pub const PROOF_TRAFFIC_BLOCKED_LOOP_E2E_SCHEMA_VERSION: &str = "proof-traffic-blocked-loop-e2e-v1";
28
29/// Stable bead/scenario id for A5.
30pub const PROOF_TRAFFIC_BLOCKED_LOOP_E2E_ID: &str = "asupersync-proof-traffic-control-kuyx64.5";
31
32/// Deterministic fixture `HEAD` used by the A5 packet.
33pub const PROOF_TRAFFIC_BLOCKED_LOOP_HEAD: &str = "1f6e579fcafebabe0000000000000000000000";
34
35/// Deterministic focused proof command intent used by the A5 packet.
36pub const PROOF_TRAFFIC_BLOCKED_LOOP_COMMAND: &str =
37    "cargo test -p asupersync --test proof_traffic_blocked_loop_e2e_contract -- --nocapture";
38
39/// Deterministic target directory for the A5 packet.
40pub const PROOF_TRAFFIC_BLOCKED_LOOP_TARGET_DIR: &str =
41    "${TMPDIR:-/tmp}/rch_target_proof_traffic_blocked_loop_e2e";
42
43/// Owned dirty source path in the deterministic fixture.
44pub const PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY: &str =
45    "src/audit/proof_traffic_blocked_loop_e2e.rs";
46
47/// Owned untracked test path in the deterministic fixture.
48pub const PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_TEST: &str =
49    "tests/proof_traffic_blocked_loop_e2e_contract.rs";
50
51/// Peer poison path used to prove excluded dirt cannot enter admitted commands.
52pub const PROOF_TRAFFIC_BLOCKED_LOOP_PEER_POISON: &str = "src/peer_poison_would_not_compile.rs";
53
54const NO_CLAIM_BOUNDARIES: &[&str] = &[
55    "No release-readiness claim.",
56    "No broad workspace-health claim.",
57    "No runtime-correctness claim.",
58    "No performance-improvement claim.",
59    "No live RCH fleet-availability claim.",
60    "No local Cargo fallback approval.",
61    "No peer-owned build cancellation authority.",
62    "No permission to delete files, clean worktrees, create branches, or create worktrees.",
63    "Deterministic fixtures are the correctness source; live RCH fleet state is operator evidence only.",
64];
65
66const FORBIDDEN_ADMITTED_COMMAND_TOKENS: &[&str] = &[
67    "|| cargo",
68    "; cargo",
69    "\ncargo ",
70    "run cargo locally",
71    "local fallback allowed",
72    "cancel peer-owned build",
73    "cancel peer build",
74    "git branch",
75    "git checkout -b",
76    "git switch -c",
77    "git worktree",
78    "worktree add",
79    "git clone",
80    "scratch clone",
81    "git clean",
82    "git reset",
83    "rm -rf",
84    "rm -r ",
85    "rm -f ",
86];
87
88/// One structured decision log emitted by the A5 e2e packet.
89#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
90pub struct ProofTrafficBlockedLoopStep {
91    /// Stable fixture id.
92    pub step_id: String,
93    /// Input command intent. This is recorded, not executed.
94    pub input_command: String,
95    /// Selected paths for this proof attempt.
96    pub selected_paths: Vec<String>,
97    /// Reservation state summarized for handoff.
98    pub reservation_state: String,
99    /// Queue or planner snapshot summarized for handoff.
100    pub queue_snapshot: String,
101    /// A2/A3 decision produced by the composed receipt.
102    pub decision: ProofTrafficDecision,
103    /// Paste-ready handoff body for the relevant receipt.
104    pub rendered_handoff: String,
105    /// One explicit no-claim boundary tied to this step.
106    pub no_claim_boundary: String,
107    /// Proof command admitted by the receipt, if any.
108    pub admitted_command: Option<String>,
109    /// Replay or resume output for a future operator.
110    pub replay_or_resume_command: String,
111}
112
113/// Deterministic handoff bundle emitted by the A5 packet.
114#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
115pub struct ProofTrafficBlockedLoopArtifactBundle {
116    /// JSON-serializable parking receipt used as the replay ledger.
117    pub json_receipt: ProofTrafficParkingLot,
118    /// Deterministic Markdown report.
119    pub markdown_report: String,
120    /// Agent Mail handoff body.
121    pub agent_mail_body: String,
122    /// `br comment` handoff body.
123    pub br_comment_body: String,
124    /// Replay/resume command or parked marker.
125    pub replay_resume_command: String,
126}
127
128/// Deterministic A5 scenario packet.
129#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
130pub struct ProofTrafficBlockedLoopScenario {
131    /// Stable schema version.
132    pub schema_version: String,
133    /// Stable scenario id.
134    pub scenario_id: String,
135    /// Structured decision logs.
136    pub steps: Vec<ProofTrafficBlockedLoopStep>,
137    /// Parking lot for blocked/refused/stale attempts.
138    pub parking_lot: ProofTrafficParkingLot,
139    /// Operator-facing bundle: JSON receipt, Markdown, Agent Mail, `br`, resume.
140    pub artifact_bundle: ProofTrafficBlockedLoopArtifactBundle,
141    /// Peer poison paths that must never enter admitted proof commands.
142    pub peer_poison_paths: Vec<String>,
143    /// Rule for live RCH fleet state in this e2e.
144    pub live_fleet_state_rule: String,
145    /// Honest no-claim boundaries.
146    pub no_claim_boundaries: Vec<String>,
147}
148
149impl ProofTrafficBlockedLoopScenario {
150    /// Build the deterministic A5 fixture.
151    #[must_use]
152    pub fn fixture() -> Self {
153        let admitted = overlay_handshake(
154            "owned-dirty-admitted-control",
155            vec![
156                working_tree(PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY, PathChange::Modified),
157                working_tree(PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_TEST, PathChange::Untracked),
158            ],
159            vec![
160                PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY,
161                PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_TEST,
162            ],
163            vec![
164                lease(PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY),
165                lease("tests/*.rs"),
166            ],
167            supported_overlay_capability(),
168        );
169
170        let peer_poison = overlay_handshake(
171            "peer-poison-excluded",
172            vec![
173                working_tree(PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY, PathChange::Modified),
174                working_tree(PROOF_TRAFFIC_BLOCKED_LOOP_PEER_POISON, PathChange::Modified),
175            ],
176            vec![PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY],
177            vec![lease(PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY)],
178            supported_overlay_capability(),
179        );
180
181        let missing_capability = overlay_handshake(
182            "missing-overlay-capability",
183            vec![working_tree(
184                PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY,
185                PathChange::Modified,
186            )],
187            vec![PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY],
188            vec![lease(PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY)],
189            unsupported_overlay_capability(),
190        );
191
192        let active_project_refusal = admission_receipt(
193            "active-project-refusal",
194            ProofTrafficQueueSnapshot::new(true, false, false, Vec::new()),
195        );
196        let progress_stale_peer = admission_receipt(
197            "progress-stale-peer-build",
198            ProofTrafficQueueSnapshot::new(
199                false,
200                false,
201                false,
202                vec![ProofTrafficActiveBuild::new(
203                    "29887347701055984",
204                    ProofTrafficBuildOwner::PeerOwned,
205                    true,
206                    true,
207                    true,
208                    "cargo test -p asupersync --test peer_lane".to_string(),
209                )],
210            ),
211        );
212
213        let parking_lot = ProofTrafficParkingLot::new(
214            PROOF_TRAFFIC_BLOCKED_LOOP_E2E_ID,
215            vec![
216                parked_from_handshake(
217                    "peer-poison-excluded",
218                    "peer-poison-path",
219                    &peer_poison,
220                    "peer poison path clears or is selected by its owner",
221                ),
222                parked_from_handshake(
223                    "missing-overlay-capability",
224                    "capability-drift:clean-overlay",
225                    &missing_capability,
226                    "installed RCH exposes clean-overlay flags",
227                ),
228                parked_from_admission(
229                    "active-project-refusal",
230                    "active-project-exclusion",
231                    &active_project_refusal,
232                    "active_project_exclusion clears",
233                )
234                .with_exact_rch_command(remote_required_command()),
235                parked_from_admission(
236                    "progress-stale-peer-build",
237                    "peer-stale:29887347701055984",
238                    &progress_stale_peer,
239                    "peer owner reports terminal output",
240                )
241                .with_exact_rch_command(remote_required_command()),
242            ],
243        );
244
245        let steps = vec![
246            step_from_handshake(
247                "owned-dirty-admitted-control",
248                "exclusive self reservations cover owned dirty and test paths",
249                "empty overlay queue; no peer poison",
250                &admitted,
251                admitted.rendered_command.clone(),
252            ),
253            step_from_handshake(
254                "peer-poison-excluded",
255                "exclusive self reservation covers owned dirty path; peer poison is unselected",
256                "planner sees peer poison path and fails closed",
257                &peer_poison,
258                parking_lot
259                    .render_resume("peer-poison-excluded")
260                    .unwrap_or_else(|| peer_poison.rendered_command.clone()),
261            ),
262            step_from_handshake(
263                "missing-overlay-capability",
264                "exclusive self reservation covers owned dirty path",
265                "installed RCH clean-overlay capability missing",
266                &missing_capability,
267                parking_lot
268                    .render_resume("missing-overlay-capability")
269                    .unwrap_or_else(|| missing_capability.rendered_command.clone()),
270            ),
271            step_from_admission(
272                "active-project-refusal",
273                "selected paths are owned by this proof attempt",
274                "active_project_exclusion=true",
275                &active_project_refusal,
276                parking_lot
277                    .render_resume("active-project-refusal")
278                    .unwrap_or_else(|| active_project_refusal.br_comment_body()),
279            ),
280            step_from_admission(
281                "progress-stale-peer-build",
282                "selected paths are owned by this proof attempt",
283                "peer build 29887347701055984 heartbeat_fresh=true progress_stale=true",
284                &progress_stale_peer,
285                parking_lot
286                    .render_resume("progress-stale-peer-build")
287                    .unwrap_or_else(|| progress_stale_peer.br_comment_body()),
288            ),
289        ];
290
291        let mut scenario = Self {
292            schema_version: PROOF_TRAFFIC_BLOCKED_LOOP_E2E_SCHEMA_VERSION.to_string(),
293            scenario_id: PROOF_TRAFFIC_BLOCKED_LOOP_E2E_ID.to_string(),
294            steps,
295            artifact_bundle: ProofTrafficBlockedLoopArtifactBundle {
296                json_receipt: parking_lot.clone(),
297                markdown_report: String::new(),
298                agent_mail_body: String::new(),
299                br_comment_body: String::new(),
300                replay_resume_command: parking_lot
301                    .render_resume("active-project-refusal")
302                    .unwrap_or_else(|| "# PARKED: missing active-project-refusal".to_string()),
303            },
304            parking_lot,
305            peer_poison_paths: vec![PROOF_TRAFFIC_BLOCKED_LOOP_PEER_POISON.to_string()],
306            live_fleet_state_rule:
307                "operator evidence only; deterministic fixtures are the correctness source"
308                    .to_string(),
309            no_claim_boundaries: NO_CLAIM_BOUNDARIES
310                .iter()
311                .map(|boundary| (*boundary).to_string())
312                .collect(),
313        };
314
315        scenario.artifact_bundle.markdown_report = scenario.render_markdown();
316        scenario.artifact_bundle.agent_mail_body = scenario.agent_mail_body();
317        scenario.artifact_bundle.br_comment_body = scenario.br_comment_body();
318        scenario
319    }
320
321    /// Render deterministic Markdown for the whole scenario.
322    #[must_use]
323    pub fn render_markdown(&self) -> String {
324        let mut out = String::new();
325        out.push_str("## Proof-traffic blocked-loop e2e - ");
326        out.push_str(&self.scenario_id);
327        out.push_str("\n\n");
328        out.push_str(&format!(
329            "- schema_version: `{}`\n- step_count: `{}`\n- live_fleet_state_rule: {}\n\n",
330            self.schema_version,
331            self.steps.len(),
332            self.live_fleet_state_rule
333        ));
334
335        out.push_str("### steps\n");
336        for step in &self.steps {
337            out.push_str("- `");
338            out.push_str(&step.step_id);
339            out.push_str("` decision=`");
340            out.push_str(step.decision.label());
341            out.push_str("` selected=`");
342            out.push_str(&step.selected_paths.join(","));
343            out.push_str("` queue_snapshot=`");
344            out.push_str(&step.queue_snapshot);
345            out.push_str("`\n");
346        }
347        out.push('\n');
348
349        push_string_section(&mut out, "peer_poison_paths", &self.peer_poison_paths);
350        push_string_section(&mut out, "no_claim_boundaries", &self.no_claim_boundaries);
351        out
352    }
353
354    /// Render Agent Mail body with structured fields first.
355    #[must_use]
356    pub fn agent_mail_body(&self) -> String {
357        let mut out = String::new();
358        out.push_str("proof_traffic_blocked_loop_e2e:\n");
359        out.push_str(&format!(
360            "- scenario_id: `{}`\n- schema_version: `{}`\n- step_count: `{}`\n",
361            self.scenario_id,
362            self.schema_version,
363            self.steps.len()
364        ));
365        for step in &self.steps {
366            out.push_str("- step: `");
367            out.push_str(&step.step_id);
368            out.push_str("` decision: `");
369            out.push_str(step.decision.label());
370            out.push_str("`\n");
371        }
372        out.push_str("- local_cargo_fallback_allowed: `false`\n");
373        out.push_str("- branch_or_worktree_allowed: `false`\n");
374        out.push_str("- file_deletion_allowed: `false`\n");
375        out
376    }
377
378    /// Render `br comment` body with structured fields first.
379    #[must_use]
380    pub fn br_comment_body(&self) -> String {
381        let mut out = String::new();
382        out.push_str("Proof-traffic blocked-loop e2e\n\n");
383        out.push_str(&format!(
384            "- scenario_id: `{}`\n- step_count: `{}`\n- live_fleet_state_rule: {}\n",
385            self.scenario_id,
386            self.steps.len(),
387            self.live_fleet_state_rule
388        ));
389        out
390    }
391
392    /// Admitted proof commands in deterministic step order.
393    #[must_use]
394    pub fn admitted_commands(&self) -> Vec<&str> {
395        self.steps
396            .iter()
397            .filter_map(|step| step.admitted_command.as_deref())
398            .collect()
399    }
400
401    /// Forbidden tokens found in admitted proof commands.
402    #[must_use]
403    pub fn forbidden_admitted_command_tokens(&self) -> Vec<&'static str> {
404        let surface = self
405            .admitted_commands()
406            .into_iter()
407            .map(str::to_ascii_lowercase)
408            .collect::<Vec<_>>()
409            .join("\n");
410        FORBIDDEN_ADMITTED_COMMAND_TOKENS
411            .iter()
412            .copied()
413            .filter(|token| surface.contains(token))
414            .collect()
415    }
416
417    /// Whether any admitted command uses local Cargo fallback.
418    #[must_use]
419    pub fn uses_local_cargo_fallback(&self) -> bool {
420        self.admitted_commands().into_iter().any(|command| {
421            let lower = command.to_ascii_lowercase();
422            lower.contains("|| cargo")
423                || lower.contains("; cargo")
424                || lower.contains("\ncargo ")
425                || lower.contains("run cargo locally")
426                || lower.contains("local fallback allowed")
427                || (lower.contains("cargo") && !lower.contains("rch exec"))
428        })
429    }
430
431    /// Peer poison paths that leaked into admitted proof commands.
432    #[must_use]
433    pub fn peer_poison_paths_in_admitted_commands(&self) -> Vec<String> {
434        let admitted = self.admitted_commands();
435        let mut leaked = BTreeSet::new();
436        for path in &self.peer_poison_paths {
437            if admitted.iter().any(|command| command.contains(path)) {
438                leaked.insert(path.clone());
439            }
440        }
441        leaked.into_iter().collect()
442    }
443}
444
445/// Build the deterministic A5 fixture.
446#[must_use]
447pub fn proof_traffic_blocked_loop_fixture() -> ProofTrafficBlockedLoopScenario {
448    ProofTrafficBlockedLoopScenario::fixture()
449}
450
451fn overlay_handshake(
452    gate_id: &str,
453    working_tree: Vec<WorkingTreeEntry>,
454    selected_paths: Vec<&str>,
455    reservations: Vec<ReservationLease>,
456    capability: ProofTrafficOverlayCapability,
457) -> ProofTrafficOverlayHandshake {
458    let request = CleanOverlayRequest {
459        head_commit: PROOF_TRAFFIC_BLOCKED_LOOP_HEAD.to_string(),
460        working_tree,
461        selected_paths: selected_paths
462            .into_iter()
463            .map(std::string::ToString::to_string)
464            .collect(),
465        reservations,
466        command_intent: PROOF_TRAFFIC_BLOCKED_LOOP_COMMAND.to_string(),
467        report_only: false,
468    };
469    let input = ProofTrafficOverlayHandshakeInput::new(
470        gate_id,
471        request,
472        PROOF_TRAFFIC_BLOCKED_LOOP_TARGET_DIR,
473        capability,
474    );
475    ProofTrafficOverlayHandshake::from_input(&input)
476}
477
478fn admission_receipt(
479    gate_id: &str,
480    queue: ProofTrafficQueueSnapshot,
481) -> ProofTrafficAdmissionReceipt {
482    let intent = ProofTrafficIntent::new(
483        PROOF_TRAFFIC_BLOCKED_LOOP_HEAD,
484        PROOF_TRAFFIC_BLOCKED_LOOP_COMMAND,
485        PROOF_TRAFFIC_BLOCKED_LOOP_TARGET_DIR,
486        vec![
487            PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_DIRTY.to_string(),
488            PROOF_TRAFFIC_BLOCKED_LOOP_OWNED_TEST.to_string(),
489        ],
490    );
491    let input = ProofTrafficAdmissionInput::new(
492        gate_id,
493        intent,
494        ProofTrafficCapabilityProbe::new(
495            "rch-1.0.41-help",
496            true,
497            vec!["remote-required supported".to_string()],
498        ),
499        queue,
500        false,
501        false,
502    );
503    ProofTrafficAdmissionReceipt::decide(&input)
504}
505
506fn step_from_handshake(
507    step_id: &str,
508    reservation_state: &str,
509    queue_snapshot: &str,
510    receipt: &ProofTrafficOverlayHandshake,
511    replay_or_resume_command: String,
512) -> ProofTrafficBlockedLoopStep {
513    ProofTrafficBlockedLoopStep {
514        step_id: step_id.to_string(),
515        input_command: receipt.command_intent.clone(),
516        selected_paths: receipt.selected_paths.clone(),
517        reservation_state: reservation_state.to_string(),
518        queue_snapshot: queue_snapshot.to_string(),
519        decision: receipt.decision,
520        rendered_handoff: receipt.agent_mail_body(),
521        no_claim_boundary: receipt
522            .no_claim_boundaries
523            .iter()
524            .find(|boundary| boundary.contains("No local Cargo fallback"))
525            .cloned()
526            .unwrap_or_else(|| "No local Cargo fallback approval.".to_string()),
527        admitted_command: receipt.admitted.then(|| receipt.rendered_command.clone()),
528        replay_or_resume_command,
529    }
530}
531
532fn step_from_admission(
533    step_id: &str,
534    reservation_state: &str,
535    queue_snapshot: &str,
536    receipt: &ProofTrafficAdmissionReceipt,
537    replay_or_resume_command: String,
538) -> ProofTrafficBlockedLoopStep {
539    ProofTrafficBlockedLoopStep {
540        step_id: step_id.to_string(),
541        input_command: receipt.command_intent.clone(),
542        selected_paths: receipt.selected_paths.clone(),
543        reservation_state: reservation_state.to_string(),
544        queue_snapshot: queue_snapshot.to_string(),
545        decision: receipt.decision,
546        rendered_handoff: receipt.agent_mail_body(),
547        no_claim_boundary: receipt
548            .no_claim_boundaries
549            .iter()
550            .find(|boundary| boundary.contains("No local Cargo fallback"))
551            .cloned()
552            .unwrap_or_else(|| "No local Cargo fallback approval.".to_string()),
553        admitted_command: None,
554        replay_or_resume_command,
555    }
556}
557
558fn parked_from_handshake(
559    attempt_id: &str,
560    blocker_key: &str,
561    receipt: &ProofTrafficOverlayHandshake,
562    retry_condition: &str,
563) -> ParkedProofAttempt {
564    ParkedProofAttempt::new(
565        attempt_id,
566        blocker_key,
567        &receipt.head_commit,
568        &receipt.command_intent,
569        &receipt.target_dir,
570        receipt.decision,
571        ProofTrafficRetryPredicate::new(
572            format!("retry-{attempt_id}"),
573            retry_condition,
574            "fresh deterministic receipt plus terminal RCH output",
575            false,
576        ),
577    )
578    .with_blocker_marker(receipt.rendered_command.clone())
579    .with_paths(
580        receipt.included_paths.clone(),
581        receipt.reservation_evidence.clone(),
582    )
583}
584
585fn parked_from_admission(
586    attempt_id: &str,
587    blocker_key: &str,
588    receipt: &ProofTrafficAdmissionReceipt,
589    retry_condition: &str,
590) -> ParkedProofAttempt {
591    ParkedProofAttempt::new(
592        attempt_id,
593        blocker_key,
594        &receipt.head_commit,
595        &receipt.command_intent,
596        &receipt.target_dir,
597        receipt.decision,
598        ProofTrafficRetryPredicate::new(
599            format!("retry-{attempt_id}"),
600            retry_condition,
601            "fresh RCH terminal output",
602            false,
603        ),
604    )
605    .with_blocker_marker(format!(
606        "# PARKED: {}; no proof command emitted",
607        receipt.rch_worker_or_refusal
608    ))
609    .with_paths(
610        receipt.selected_paths.clone(),
611        receipt.selected_paths.clone(),
612    )
613}
614
615fn supported_overlay_capability() -> ProofTrafficOverlayCapability {
616    ProofTrafficOverlayCapability::from_rch_exec_help(
617        "rch-1.0.99-help",
618        r"Options:
619  -b, --base=<HEAD>
620      --clean-overlay
621  -o, --overlay-path=<PATH>
622      --no-overlay
623",
624    )
625}
626
627fn unsupported_overlay_capability() -> ProofTrafficOverlayCapability {
628    ProofTrafficOverlayCapability::from_rch_exec_help(
629        "rch-1.0.41-help",
630        r"Options:
631  -v, --verbose
632  Examples:
633  --base HEAD
634  --clean-overlay
635  --overlay-path PATH
636  --no-overlay
637",
638    )
639}
640
641fn remote_required_command() -> String {
642    format!(
643        "RCH_REQUIRE_REMOTE=1 rch exec -- env CARGO_TARGET_DIR=\"{}\" CARGO_INCREMENTAL=0 CARGO_PROFILE_TEST_DEBUG=0 RUSTFLAGS='-D warnings -C debuginfo=0' {}",
644        PROOF_TRAFFIC_BLOCKED_LOOP_TARGET_DIR, PROOF_TRAFFIC_BLOCKED_LOOP_COMMAND
645    )
646}
647
648fn working_tree(path: &str, change: PathChange) -> WorkingTreeEntry {
649    WorkingTreeEntry::new(path, change)
650}
651
652fn lease(pattern: &str) -> ReservationLease {
653    ReservationLease::new(pattern, true)
654}
655
656fn push_string_section(out: &mut String, title: &str, values: &[String]) {
657    out.push_str(&format!("### {title} ({})\n", values.len()));
658    if values.is_empty() {
659        out.push_str("- _none_\n");
660    } else {
661        for value in values {
662            out.push_str("- ");
663            out.push_str(value);
664            out.push('\n');
665        }
666    }
667    out.push('\n');
668}