bashrs 6.66.0

Rust-to-Shell transpiler for deterministic bootstrap scripts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

pub mod properties;

#[cfg(kani)]
pub mod kani_harnesses;

#[cfg(test)]
mod tests;

#[cfg(test)]
mod properties_tests;

use crate::ir::ShellIR;
use crate::models::{Result, VerificationLevel};

/// Verify that the given IR satisfies safety properties
pub fn verify(ir: &ShellIR, level: VerificationLevel) -> Result<()> {
    match level {
        VerificationLevel::None => Ok(()),
        VerificationLevel::Basic => verify_basic(ir),
        VerificationLevel::Strict => verify_strict(ir),
        VerificationLevel::Paranoid => verify_paranoid(ir),
    }
}

fn verify_basic(ir: &ShellIR) -> Result<()> {
    // Basic verification: check for obvious safety issues
    properties::verify_no_command_injection(ir)?;
    Ok(())
}

fn verify_strict(ir: &ShellIR) -> Result<()> {
    // Strict verification: all basic checks plus determinism
    verify_basic(ir)?;
    properties::verify_deterministic(ir)?;
    Ok(())
}

fn verify_paranoid(ir: &ShellIR) -> Result<()> {
    // Paranoid verification: all checks plus formal verification
    verify_strict(ir)?;
    properties::verify_idempotency(ir)?;
    properties::verify_resource_safety(ir)?;
    Ok(())
}