Skip to main content

start_command/
formal_ai_policy.rs

1//! Bounds and effect policy of the experimental `--use-formal-ai` mode
2//! (issue #255). Mirrors js/src/lib/formal-ai-policy.js.
3//!
4//! Formal AI owns the interpretation of a natural-language request and picks
5//! the tool calls; start owns the permission to run them. Every tool call is a
6//! POSIX command line that start tokenizes itself and runs as an argv vector,
7//! never through a shell, so a call that needs shell syntax (pipes, redirects,
8//! substitutions, globs, variables) is refused instead of being interpreted.
9
10use std::collections::{BTreeMap, BTreeSet, VecDeque};
11use std::fs;
12use std::path::{Component, Path, PathBuf};
13
14use regex::Regex;
15use serde_json::{json, Value};
16
17/// Request text or option combination rejected.
18pub const EXIT_USAGE: i32 = 64;
19/// Formal AI did not understand the task or reported a capability gap.
20pub const EXIT_UNSUPPORTED: i32 = 65;
21/// No qualified Formal AI runtime could be resolved.
22pub const EXIT_UNAVAILABLE: i32 = 69;
23/// Malformed or 5xx response, unknown tool or unverified effect.
24pub const EXIT_PROTOCOL: i32 = 70;
25/// A tool call was refused by the effect policy.
26pub const EXIT_REFUSED: i32 = 77;
27/// Invalid START_FORMAL_AI_* bound.
28pub const EXIT_CONFIG: i32 = 78;
29/// Step, tool, time or retry budget exhausted.
30pub const EXIT_BUDGET: i32 = 124;
31
32pub const EFFECT_MODES: [&str; 2] = ["read-only", "workspace-write"];
33
34/// One START_FORMAL_AI_* bound: environment variable, default and range.
35pub struct BoundSpec {
36    pub key: &'static str,
37    pub env: &'static str,
38    pub value: u64,
39    pub min: u64,
40    pub max: Option<u64>,
41}
42
43pub const BOUND_DEFAULTS: [BoundSpec; 10] = [
44    BoundSpec {
45        key: "maxSteps",
46        env: "START_FORMAL_AI_MAX_STEPS",
47        value: 8,
48        min: 1,
49        max: Some(64),
50    },
51    BoundSpec {
52        key: "maxRetries",
53        env: "START_FORMAL_AI_MAX_RETRIES",
54        value: 1,
55        min: 0,
56        max: Some(5),
57    },
58    BoundSpec {
59        key: "timeoutMs",
60        env: "START_FORMAL_AI_TIMEOUT_MS",
61        value: 120_000,
62        min: 1,
63        max: None,
64    },
65    BoundSpec {
66        key: "toolTimeoutMs",
67        env: "START_FORMAL_AI_TOOL_TIMEOUT_MS",
68        value: 30_000,
69        min: 1,
70        max: None,
71    },
72    BoundSpec {
73        key: "startupTimeoutMs",
74        env: "START_FORMAL_AI_STARTUP_TIMEOUT_MS",
75        value: 30_000,
76        min: 1,
77        max: None,
78    },
79    BoundSpec {
80        key: "maxOutputBytes",
81        env: "START_FORMAL_AI_MAX_OUTPUT_BYTES",
82        value: 64 * 1024,
83        min: 1,
84        max: Some(16 * 1024 * 1024),
85    },
86    BoundSpec {
87        key: "maxFileBytes",
88        env: "START_FORMAL_AI_MAX_FILE_BYTES",
89        value: 1024 * 1024,
90        min: 1,
91        max: Some(16 * 1024 * 1024),
92    },
93    BoundSpec {
94        key: "maxRequestChars",
95        env: "START_FORMAL_AI_MAX_REQUEST_CHARS",
96        value: 4096,
97        min: 1,
98        max: None,
99    },
100    BoundSpec {
101        key: "maxMemoryMb",
102        env: "START_FORMAL_AI_MAX_MEMORY_MB",
103        value: 1024,
104        min: 1,
105        max: None,
106    },
107    BoundSpec {
108        key: "maxFingerprintEntries",
109        env: "START_FORMAL_AI_MAX_FINGERPRINT_ENTRIES",
110        value: 5000,
111        min: 1,
112        max: None,
113    },
114];
115
116/// Resolved bounds of one run.
117#[derive(Debug, Clone, PartialEq)]
118pub struct Bounds {
119    pub max_steps: u64,
120    pub max_retries: u64,
121    pub timeout_ms: u64,
122    pub tool_timeout_ms: u64,
123    pub startup_timeout_ms: u64,
124    pub max_output_bytes: u64,
125    /// Largest file the read, edit and write tools handle (issue #258).
126    pub max_file_bytes: u64,
127    pub max_request_chars: u64,
128    pub max_memory_mb: u64,
129    pub max_fingerprint_entries: u64,
130    pub effects: String,
131}
132
133impl Default for Bounds {
134    fn default() -> Self {
135        resolve_bounds_with(|_| None).expect("defaults are valid")
136    }
137}
138
139impl Bounds {
140    /// The bounds as the evidence records them (same keys as JavaScript).
141    pub fn to_json(&self) -> Value {
142        json!({
143            "maxSteps": self.max_steps,
144            "maxRetries": self.max_retries,
145            "timeoutMs": self.timeout_ms,
146            "toolTimeoutMs": self.tool_timeout_ms,
147            "startupTimeoutMs": self.startup_timeout_ms,
148            "maxOutputBytes": self.max_output_bytes,
149            "maxFileBytes": self.max_file_bytes,
150            "maxRequestChars": self.max_request_chars,
151            "maxMemoryMb": self.max_memory_mb,
152            "maxFingerprintEntries": self.max_fingerprint_entries,
153            "effects": self.effects,
154        })
155    }
156}
157
158/// Resolve the bounds from the process environment.
159pub fn resolve_bounds() -> Result<Bounds, String> {
160    resolve_bounds_with(|name| std::env::var(name).ok())
161}
162
163/// Resolve the bounds of one run from START_FORMAL_AI_* variables read
164/// through `get`. An invalid value is an error (exit status EXIT_CONFIG).
165pub fn resolve_bounds_with(get: impl Fn(&str) -> Option<String>) -> Result<Bounds, String> {
166    let mut values = BTreeMap::new();
167    for spec in BOUND_DEFAULTS.iter() {
168        let raw = get(spec.env).unwrap_or_default();
169        if raw.is_empty() {
170            values.insert(spec.key, spec.value);
171            continue;
172        }
173        let trimmed = raw.trim();
174        let parsed = if !trimmed.is_empty() && trimmed.chars().all(|c| c.is_ascii_digit()) {
175            trimmed.parse::<u64>().ok()
176        } else {
177            None
178        };
179        match parsed {
180            Some(value) if value >= spec.min && spec.max.is_none_or(|max| value <= max) => {
181                values.insert(spec.key, value);
182            }
183            _ => {
184                let max = spec
185                    .max
186                    .map_or_else(|| "any".to_string(), |max| max.to_string());
187                return Err(format!(
188                    "{} must be an integer from {} to {}, got \"{}\"",
189                    spec.env, spec.min, max, raw
190                ));
191            }
192        }
193    }
194    let effects = get("START_FORMAL_AI_EFFECTS")
195        .filter(|value| !value.is_empty())
196        .unwrap_or_else(|| "read-only".to_string())
197        .trim()
198        .to_string();
199    if !EFFECT_MODES.contains(&effects.as_str()) {
200        return Err(format!(
201            "START_FORMAL_AI_EFFECTS must be one of {}, got \"{}\"",
202            EFFECT_MODES.join(", "),
203            effects
204        ));
205    }
206    Ok(Bounds {
207        max_steps: values["maxSteps"],
208        max_retries: values["maxRetries"],
209        timeout_ms: values["timeoutMs"],
210        tool_timeout_ms: values["toolTimeoutMs"],
211        startup_timeout_ms: values["startupTimeoutMs"],
212        max_output_bytes: values["maxOutputBytes"],
213        max_file_bytes: values["maxFileBytes"],
214        max_request_chars: values["maxRequestChars"],
215        max_memory_mb: values["maxMemoryMb"],
216        max_fingerprint_entries: values["maxFingerprintEntries"],
217        effects,
218    })
219}
220
221/// Words of a command line and the shell syntax it would have needed.
222#[derive(Debug, Clone, PartialEq, Default)]
223pub struct Tokenized {
224    pub tokens: Vec<String>,
225    pub problems: Vec<String>,
226}
227
228/// Split a command line with POSIX quoting rules. Characters that would make
229/// a shell do more than split words are reported instead of honoured.
230pub fn tokenize_command(line: &str) -> Tokenized {
231    let chars: Vec<char> = line.chars().collect();
232    let mut tokens = Vec::new();
233    let mut problems: Vec<String> = Vec::new();
234    let mut add = |problem: String| {
235        if !problems.contains(&problem) {
236            problems.push(problem);
237        }
238    };
239    let mut current: Option<String> = None;
240    let mut quote: Option<char> = None;
241    let mut i = 0;
242    while i < chars.len() {
243        let ch = chars[i];
244        if quote == Some('\'') {
245            if ch == '\'' {
246                quote = None;
247            } else {
248                current.get_or_insert_with(String::new).push(ch);
249            }
250            i += 1;
251            continue;
252        }
253        if quote == Some('"') {
254            if ch == '"' {
255                quote = None;
256            } else if ch == '\\' && i + 1 < chars.len() && "\"\\$`".contains(chars[i + 1]) {
257                i += 1;
258                current.get_or_insert_with(String::new).push(chars[i]);
259            } else {
260                if ch == '$' || ch == '`' {
261                    add(format!("expansion \"{}\"", ch));
262                }
263                current.get_or_insert_with(String::new).push(ch);
264            }
265            i += 1;
266            continue;
267        }
268        if ch == ' ' || ch == '\t' {
269            if let Some(token) = current.take() {
270                tokens.push(token);
271            }
272            i += 1;
273            continue;
274        }
275        if ch == '\'' || ch == '"' {
276            quote = Some(ch);
277            current.get_or_insert_with(String::new);
278            i += 1;
279            continue;
280        }
281        if ch == '\\' {
282            if i + 1 < chars.len() && chars[i + 1] != '\n' {
283                i += 1;
284                current.get_or_insert_with(String::new).push(chars[i]);
285                i += 1;
286                continue;
287            }
288            add("line continuation".to_string());
289            i += 1;
290            continue;
291        }
292        if "\n\r;&|<>()$`".contains(ch) {
293            let shown = if ch == '\n' {
294                "\\n".to_string()
295            } else {
296                ch.to_string()
297            };
298            add(format!("shell operator \"{}\"", shown));
299        } else if "*?[]{}".contains(ch) {
300            add(format!("unquoted pattern \"{}\"", ch));
301        } else if ch == '~' && current.is_none() {
302            add("home directory expansion \"~\"".to_string());
303        } else if ch == '#' && current.is_none() {
304            add("comment \"#\"".to_string());
305        }
306        current.get_or_insert_with(String::new).push(ch);
307        i += 1;
308    }
309    if quote.is_some() {
310        add("unterminated quote".to_string());
311    }
312    if let Some(token) = current {
313        tokens.push(token);
314    }
315    Tokenized { tokens, problems }
316}
317
318pub const READ_PROGRAMS: [&str; 24] = [
319    "basename",
320    "cat",
321    "cmp",
322    "diff",
323    "dirname",
324    "du",
325    "file",
326    "find",
327    "git",
328    "grep",
329    "head",
330    "ls",
331    "md5sum",
332    "pwd",
333    "readlink",
334    "realpath",
335    "sha256sum",
336    "sort",
337    "stat",
338    "tail",
339    "test",
340    "tree",
341    "uniq",
342    "wc",
343];
344pub const WRITE_PROGRAMS: [&str; 6] = ["cp", "mkdir", "mv", "rm", "rmdir", "touch"];
345const LISTING_PROGRAMS: [&str; 4] = ["ls", "find", "tree", "du"];
346const GIT_SUBCOMMANDS: [&str; 7] = [
347    "branch",
348    "diff",
349    "log",
350    "ls-files",
351    "rev-parse",
352    "show",
353    "status",
354];
355const GIT_BRANCH_FLAGS: [&str; 6] = ["-a", "-r", "-v", "-vv", "--list", "--show-current"];
356
357/// Flags that turn an otherwise read-only program into a writer or waiter.
358fn forbidden_flags(program: &str) -> Option<Regex> {
359    let pattern = match program {
360        "find" => r"^-(delete|exec|execdir|ok|okdir|fprint|fprint0|fprintf|fls)$",
361        "sort" | "tree" => r"^(-o.*|--output.*)$",
362        "file" => r"^(-C|--compile)$",
363        "tail" => r"^(-f|-F|--follow.*|--retry)$",
364        "git" => r"^(--output.*|--ext-diff|-c|--exec-path.*|--git-dir.*|--work-tree.*)$",
365        "rm" => r"^(-[a-zA-Z]*[rR][a-zA-Z]*|--recursive|--no-preserve-root)$",
366        "cp" => r"^(-[a-zA-Z]*[l][a-zA-Z]*|--link|-s|--symbolic-link)$",
367        _ => return None,
368    };
369    Regex::new(pattern).ok()
370}
371
372/// Lexically normalize a path (`.` and `..` resolved without the filesystem).
373fn normalize(path: &Path) -> PathBuf {
374    let mut result = PathBuf::new();
375    for component in path.components() {
376        match component {
377            Component::CurDir => {}
378            Component::ParentDir => {
379                result.pop();
380            }
381            other => result.push(other.as_os_str()),
382        }
383    }
384    result
385}
386
387/// Real path of `target`, resolving its nearest existing ancestor.
388fn real_target(target: &Path) -> PathBuf {
389    let mut existing = target.to_path_buf();
390    let mut rest = Vec::new();
391    while !existing.exists() {
392        match (existing.parent(), existing.file_name()) {
393            (Some(parent), Some(name)) => {
394                rest.push(name.to_os_string());
395                existing = parent.to_path_buf();
396            }
397            _ => return target.to_path_buf(),
398        }
399    }
400    let mut resolved = fs::canonicalize(&existing).unwrap_or(existing);
401    for name in rest.iter().rev() {
402        resolved.push(name);
403    }
404    resolved
405}
406
407/// Path-like operands of a call (values of `--opt=value` included).
408pub fn operands(tokens: &[String]) -> Vec<String> {
409    let mut values = Vec::new();
410    for token in tokens.iter().skip(1) {
411        if token.starts_with('-') {
412            if let Some(eq) = token.find('=') {
413                if eq > 0 && token.starts_with("--") {
414                    values.push(token[eq + 1..].to_string());
415                }
416            }
417            continue;
418        }
419        values.push(token.clone());
420    }
421    values
422}
423
424/// Normalized workspace-relative path of an operand, or None outside it.
425/// It uses `/` on every platform, like the fingerprint, so observations,
426/// messages and evidence are the same on Windows.
427pub fn workspace_path(cwd: &Path, operand: &str) -> Option<String> {
428    let root = fs::canonicalize(cwd).unwrap_or_else(|_| cwd.to_path_buf());
429    let resolved = real_target(&normalize(&cwd.join(operand)));
430    let relative = resolved.strip_prefix(&root).ok()?;
431    let text = relative
432        .components()
433        .map(|part| part.as_os_str().to_string_lossy())
434        .collect::<Vec<_>>()
435        .join("/");
436    Some(if text.is_empty() {
437        ".".to_string()
438    } else {
439        text
440    })
441}
442
443/// Directory of a workspace-relative path ("." at the top).
444pub fn parent_of(target: &str) -> String {
445    match Path::new(target).parent() {
446        Some(parent) if !parent.as_os_str().is_empty() => parent.to_string_lossy().to_string(),
447        _ => ".".to_string(),
448    }
449}
450
451/// What a read observed, so a later change may name it.
452#[derive(Debug, Clone, Default)]
453pub struct PolicyContext {
454    pub cwd: PathBuf,
455    pub effects: String,
456    pub observed: BTreeSet<String>,
457    pub observed_dirs: BTreeSet<String>,
458    /// SHA-256 of each file as start last read or wrote it (issue #258).
459    pub contents: BTreeMap<String, String>,
460}
461
462impl PolicyContext {
463    pub fn new(cwd: &Path, effects: &str) -> Self {
464        Self {
465            cwd: cwd.to_path_buf(),
466            effects: effects.to_string(),
467            ..Self::default()
468        }
469    }
470}
471
472/// Decision about one tool call.
473#[derive(Debug, Clone, PartialEq, Default)]
474pub struct Decision {
475    pub allowed: bool,
476    pub reason: Option<String>,
477    pub tokens: Vec<String>,
478    /// `read` or `write` when allowed
479    pub kind: Option<&'static str>,
480    pub targets: Vec<String>,
481}
482
483fn refuse(reason: String, tokens: &[String]) -> Decision {
484    Decision {
485        allowed: false,
486        reason: Some(reason),
487        tokens: tokens.to_vec(),
488        ..Decision::default()
489    }
490}
491
492/// Decide whether a tool call may run.
493pub fn evaluate_command(line: &str, context: &PolicyContext) -> Decision {
494    let Tokenized { tokens, problems } = tokenize_command(line);
495    if !problems.is_empty() {
496        return refuse(
497            format!(
498                "needs shell syntax start does not run: {}",
499                problems.join(", ")
500            ),
501            &tokens,
502        );
503    }
504    let Some(program) = tokens.first().cloned() else {
505        return refuse("empty command".to_string(), &tokens);
506    };
507    let is_write = WRITE_PROGRAMS.contains(&program.as_str());
508    if !READ_PROGRAMS.contains(&program.as_str()) && !is_write {
509        return refuse(
510            format!("program \"{}\" is not in the supported tool set", program),
511            &tokens,
512        );
513    }
514    if is_write && context.effects != "workspace-write" {
515        return refuse(
516            format!(
517                "\"{}\" changes files; the effect mode is read-only (set START_FORMAL_AI_EFFECTS=workspace-write to allow workspace changes)",
518                program
519            ),
520            &tokens,
521        );
522    }
523    if let Some(forbidden) = forbidden_flags(&program) {
524        if let Some(flag) = tokens.iter().skip(1).find(|t| forbidden.is_match(t)) {
525            return refuse(
526                format!("option \"{}\" of {} is not allowed", flag, program),
527                &tokens,
528            );
529        }
530    }
531    if program == "git" {
532        let sub = tokens.get(1).cloned().unwrap_or_default();
533        if !GIT_SUBCOMMANDS.contains(&sub.as_str()) {
534            return refuse(
535                format!("git subcommand \"{}\" is not read-only", sub),
536                &tokens,
537            );
538        }
539        if sub == "branch"
540            && tokens
541                .iter()
542                .skip(2)
543                .any(|t| !GIT_BRANCH_FLAGS.contains(&t.as_str()))
544        {
545            return refuse("git branch may only list branches".to_string(), &tokens);
546        }
547    }
548    let mut targets = Vec::new();
549    for operand in operands(&tokens) {
550        if operand.starts_with('~') {
551            return refuse(
552                format!("\"{}\" is outside the working directory", operand),
553                &tokens,
554            );
555        }
556        // Absolute, escaping and symlinked-out operands are refused: reads and
557        // changes stay inside the working directory.
558        match workspace_path(&context.cwd, &operand) {
559            Some(relative) => targets.push(relative),
560            None => {
561                return refuse(
562                    format!("\"{}\" is outside the working directory", operand),
563                    &tokens,
564                )
565            }
566        }
567    }
568    if is_write {
569        if targets.is_empty() {
570            return refuse(format!("{} needs an explicit target", program), &tokens);
571        }
572        let unobserved: Vec<String> = targets
573            .iter()
574            .filter(|t| {
575                t.as_str() == "."
576                    || !(context.observed.contains(*t)
577                        || context.observed_dirs.contains(&parent_of(t)))
578            })
579            .map(|t| format!("\"{}\"", t))
580            .collect();
581        if !unobserved.is_empty() {
582            return refuse(
583                format!(
584                    "target {} was not observed before the change",
585                    unobserved.join(", ")
586                ),
587                &tokens,
588            );
589        }
590    }
591    Decision {
592        allowed: true,
593        reason: None,
594        tokens,
595        kind: Some(if is_write { "write" } else { "read" }),
596        targets,
597    }
598}
599
600/// Remember what a read call observed, so a later change may name it.
601pub fn record_observation(decision: &Decision, context: &mut PolicyContext) {
602    for target in &decision.targets {
603        context.observed.insert(target.clone());
604    }
605    let listing = decision
606        .tokens
607        .first()
608        .is_some_and(|program| LISTING_PROGRAMS.contains(&program.as_str()));
609    if listing {
610        if decision.targets.is_empty() {
611            context.observed_dirs.insert(".".to_string());
612        }
613        for target in &decision.targets {
614            context.observed_dirs.insert(target.clone());
615        }
616    }
617}
618
619/// Bounded fingerprint of a directory tree (names, types, sizes, mtimes).
620#[derive(Debug, Clone, PartialEq, Default)]
621pub struct Fingerprint {
622    pub entries: BTreeMap<String, String>,
623    pub complete: bool,
624}
625
626/// Bounded breadth-first fingerprint of the working directory; `.git` is
627/// listed but not descended into.
628pub fn fingerprint(cwd: &Path, limit: u64) -> Fingerprint {
629    let mut entries = BTreeMap::new();
630    let mut queue = VecDeque::from([String::new()]);
631    while let Some(relative) = queue.pop_front() {
632        let dir = if relative.is_empty() {
633            cwd.to_path_buf()
634        } else {
635            cwd.join(&relative)
636        };
637        let Ok(read) = fs::read_dir(&dir) else {
638            continue;
639        };
640        let mut names: Vec<String> = read
641            .filter_map(|entry| entry.ok())
642            .map(|entry| entry.file_name().to_string_lossy().to_string())
643            .collect();
644        names.sort();
645        for name in names {
646            if entries.len() as u64 >= limit {
647                return Fingerprint {
648                    entries,
649                    complete: false,
650                };
651            }
652            let child = if relative.is_empty() {
653                name.clone()
654            } else {
655                format!("{}/{}", relative, name)
656            };
657            let Ok(meta) = fs::symlink_metadata(cwd.join(&child)) else {
658                continue;
659            };
660            let kind = if meta.is_dir() {
661                'd'
662            } else if meta.file_type().is_symlink() {
663                'l'
664            } else {
665                'f'
666            };
667            let mtime = meta
668                .modified()
669                .ok()
670                .and_then(|t| t.duration_since(std::time::UNIX_EPOCH).ok())
671                .map_or(0, |d| d.as_nanos());
672            entries.insert(child.clone(), format!("{}:{}:{}", kind, meta.len(), mtime));
673            if kind == 'd' && name != ".git" {
674                queue.push_back(child);
675            }
676        }
677    }
678    Fingerprint {
679        entries,
680        complete: true,
681    }
682}
683
684/// Differences between two fingerprints.
685#[derive(Debug, Clone, PartialEq)]
686pub struct EffectDiff {
687    pub added: Vec<String>,
688    pub removed: Vec<String>,
689    pub changed: Vec<String>,
690    pub complete: bool,
691}
692
693impl Default for EffectDiff {
694    fn default() -> Self {
695        Self {
696            added: Vec::new(),
697            removed: Vec::new(),
698            changed: Vec::new(),
699            complete: true,
700        }
701    }
702}
703
704impl EffectDiff {
705    pub fn has_effects(&self) -> bool {
706        !(self.added.is_empty() && self.removed.is_empty() && self.changed.is_empty())
707    }
708
709    pub fn to_json(&self) -> Value {
710        json!({
711            "added": self.added,
712            "removed": self.removed,
713            "changed": self.changed,
714            "complete": self.complete,
715        })
716    }
717}
718
719pub fn diff_fingerprints(before: &Fingerprint, after: &Fingerprint) -> EffectDiff {
720    let mut diff = EffectDiff {
721        complete: before.complete && after.complete,
722        ..EffectDiff::default()
723    };
724    for (name, value) in &after.entries {
725        match before.entries.get(name) {
726            None => diff.added.push(name.clone()),
727            Some(old) if old != value => diff.changed.push(name.clone()),
728            _ => {}
729        }
730    }
731    for name in before.entries.keys() {
732        if !after.entries.contains_key(name) {
733            diff.removed.push(name.clone());
734        }
735    }
736    diff
737}
738
739/// Result of reading a change back from the filesystem.
740#[derive(Debug, Clone, PartialEq)]
741pub struct Verification {
742    pub verified: bool,
743    pub detail: String,
744}
745
746impl Verification {
747    pub fn to_json(&self) -> Value {
748        json!({ "verified": self.verified, "detail": self.detail })
749    }
750}
751
752/// Read the result of a successful change back from the filesystem.
753pub fn verify_change(tokens: &[String], cwd: &Path) -> Verification {
754    let program = tokens.first().map(String::as_str).unwrap_or("");
755    let args = operands(tokens);
756    let exists = |p: &str| cwd.join(p).exists();
757    let is_dir = |p: &str| cwd.join(p).is_dir();
758    let mut missing: Vec<String> = Vec::new();
759    match program {
760        "mkdir" => missing = args.iter().filter(|p| !is_dir(p)).cloned().collect(),
761        "touch" => missing = args.iter().filter(|p| !exists(p)).cloned().collect(),
762        "rm" | "rmdir" => {
763            missing = args
764                .iter()
765                .filter(|p| exists(p))
766                .map(|p| format!("{} (still present)", p))
767                .collect()
768        }
769        "cp" | "mv" if !args.is_empty() => {
770            let dest = args[args.len() - 1].clone();
771            let sources = &args[..args.len() - 1];
772            let expected: Vec<String> = if is_dir(&dest) && !sources.is_empty() {
773                sources
774                    .iter()
775                    .map(|s| {
776                        let base = Path::new(s)
777                            .file_name()
778                            .map(|n| n.to_string_lossy().to_string())
779                            .unwrap_or_default();
780                        Path::new(&dest).join(base).to_string_lossy().to_string()
781                    })
782                    .collect()
783            } else {
784                vec![dest]
785            };
786            missing = expected.iter().filter(|p| !exists(p)).cloned().collect();
787            if program == "mv" {
788                missing.extend(
789                    sources
790                        .iter()
791                        .filter(|s| exists(s) && !expected.contains(s))
792                        .map(|s| format!("{} (still present)", s)),
793                );
794            }
795        }
796        _ => {}
797    }
798    if missing.is_empty() {
799        Verification {
800            verified: true,
801            detail: format!("readback confirmed {} {}", program, args.join(" ")),
802        }
803    } else {
804        Verification {
805            verified: false,
806            detail: format!("readback failed: {}", missing.join(", ")),
807        }
808    }
809}
810
811#[cfg(test)]
812#[path = "formal_ai_policy_cases.rs"]
813pub(crate) mod formal_ai_policy_cases;