bashrs 6.66.3

//! Kani proof harnesses for formal verification
//!
//! This module contains Kani harnesses that formally verify
//! properties of the tiny AST emitter using bounded model checking.

#[cfg(kani)]
mod kani_proofs {
    use crate::formal::semantics::{posix_semantics, rash_semantics};
    use crate::formal::{AbstractState, FormalEmitter, TinyAst};
    // GH-212: `let s: String = kani::any()` is an E0277 — String is not (and
    // cannot be) kani::Arbitrary. These harnesses had never been compiled.
    use crate::kani_bounded::{any_bounded_identifier, any_bounded_string};

    /// Verify that echo commands preserve their output exactly
    #[kani::proof]
    #[kani::unwind(7)]
    fn verify_echo_semantic_equivalence() {
        // Bounded at 6, not the original's 10: the state space is 62^N, and the
        // bound must be justified by a measured runtime rather than a wish.
        let arg = any_bounded_string::<6>();

        let ast = TinyAst::ExecuteCommand {
            command_name: "echo".to_string(),
            args: vec![arg.clone()],
        };

        // Verify the AST is valid
        assert!(ast.is_valid());

        // Create initial state
        let initial_state = AbstractState::new();

        // Evaluate rash AST
        if let Ok(rash_state) = rash_semantics::eval_rash(&ast, initial_state.clone()) {
            // Emit POSIX code
            let posix_code = FormalEmitter::emit(&ast);

            // Evaluate POSIX code
            if let Ok(posix_state) = posix_semantics::eval_posix(&posix_code, initial_state) {
                // Verify semantic equivalence
                assert!(rash_state.is_equivalent(&posix_state));

                // Specifically check stdout
                assert_eq!(rash_state.stdout.len(), 1);
                assert_eq!(posix_state.stdout.len(), 1);
                assert_eq!(rash_state.stdout[0], arg);
                assert_eq!(posix_state.stdout[0], arg);
            }
        }
    }

    /// Verify that environment variable assignments are preserved
    #[kani::proof]
    #[kani::unwind(6)]
    fn verify_assignment_semantic_equivalence() {
        // any_bounded_identifier encodes the leading-char rule the original
        // spelled out with two assumes (and an `.unwrap()` on `next()` that
        // would have been reachable had len == 0 slipped through).
        let name = any_bounded_identifier::<4>();
        let value = any_bounded_string::<5>();

        let ast = TinyAst::SetEnvironmentVariable {
            name: name.clone(),
            value: value.clone(),
        };

        // Verify the AST is valid
        assert!(ast.is_valid());

        // Create initial state
        let initial_state = AbstractState::new();

        // Evaluate rash AST
        if let Ok(rash_state) = rash_semantics::eval_rash(&ast, initial_state.clone()) {
            // Emit POSIX code
            let posix_code = FormalEmitter::emit(&ast);

            // Evaluate POSIX code
            if let Ok(posix_state) = posix_semantics::eval_posix(&posix_code, initial_state) {
                // Verify semantic equivalence
                assert!(rash_state.is_equivalent(&posix_state));

                // Specifically check the environment variable
                assert_eq!(rash_state.get_env(&name), Some(&value));
                assert_eq!(posix_state.get_env(&name), Some(&value));
            }
        }
    }

    /// Verify that mkdir commands create directories correctly
    #[kani::proof]
    fn verify_mkdir_semantic_equivalence() {
        // Use a fixed simple path for bounded verification
        let path = "/tmp/test".to_string();

        let ast = TinyAst::ExecuteCommand {
            command_name: "mkdir".to_string(),
            args: vec!["-p".to_string(), path.clone()],
        };

        // Create initial state with /tmp directory
        let mut initial_state = AbstractState::new();
        initial_state.filesystem.insert(
            std::path::PathBuf::from("/tmp"),
            crate::formal::FileSystemEntry::Directory,
        );

        // Evaluate rash AST
        if let Ok(rash_state) = rash_semantics::eval_rash(&ast, initial_state.clone()) {
            // Emit POSIX code
            let posix_code = FormalEmitter::emit(&ast);

            // Evaluate POSIX code
            if let Ok(posix_state) = posix_semantics::eval_posix(&posix_code, initial_state) {
                // Verify semantic equivalence
                assert!(rash_state.is_equivalent(&posix_state));

                // Verify directory was created
                let path_buf = std::path::PathBuf::from(&path);
                assert!(rash_state.filesystem.contains_key(&path_buf));
                assert!(posix_state.filesystem.contains_key(&path_buf));
            }
        }
    }

    /// Verify that change directory commands work correctly
    #[kani::proof]
    fn verify_cd_semantic_equivalence() {
        // Use a fixed path
        let path = "/tmp".to_string();

        let ast = TinyAst::ChangeDirectory { path: path.clone() };

        // Create initial state with the target directory
        let mut initial_state = AbstractState::new();
        initial_state.filesystem.insert(
            std::path::PathBuf::from(&path),
            crate::formal::FileSystemEntry::Directory,
        );

        // Evaluate rash AST
        if let Ok(rash_state) = rash_semantics::eval_rash(&ast, initial_state.clone()) {
            // Emit POSIX code
            let posix_code = FormalEmitter::emit(&ast);

            // Evaluate POSIX code
            if let Ok(posix_state) = posix_semantics::eval_posix(&posix_code, initial_state) {
                // Verify semantic equivalence
                assert!(rash_state.is_equivalent(&posix_state));

                // Verify current directory changed
                assert_eq!(rash_state.cwd, std::path::PathBuf::from(&path));
                assert_eq!(posix_state.cwd, std::path::PathBuf::from(&path));
            }
        }
    }

    /// Verify that sequences preserve order and state changes
    #[kani::proof]
    fn verify_sequence_semantic_equivalence() {
        // Create a simple two-command sequence
        let ast = TinyAst::Sequence {
            commands: vec![
                TinyAst::SetEnvironmentVariable {
                    name: "VAR".to_string(),
                    value: "test".to_string(),
                },
                TinyAst::ExecuteCommand {
                    command_name: "echo".to_string(),
                    args: vec!["done".to_string()],
                },
            ],
        };

        // Create initial state
        let initial_state = AbstractState::new();

        // Evaluate rash AST
        if let Ok(rash_state) = rash_semantics::eval_rash(&ast, initial_state.clone()) {
            // Emit POSIX code
            let posix_code = FormalEmitter::emit(&ast);

            // Evaluate POSIX code
            if let Ok(posix_state) = posix_semantics::eval_posix(&posix_code, initial_state) {
                // Verify semantic equivalence
                assert!(rash_state.is_equivalent(&posix_state));

                // Verify both effects happened
                assert_eq!(rash_state.get_env("VAR"), Some(&"test".to_string()));
                assert_eq!(posix_state.get_env("VAR"), Some(&"test".to_string()));
                assert_eq!(rash_state.stdout.len(), 1);
                assert_eq!(posix_state.stdout.len(), 1);
                assert_eq!(rash_state.stdout[0], "done");
            }
        }
    }

    /// Verify emitter produces valid shell code for all valid ASTs
    #[kani::proof]
    fn verify_emitter_totality() {
        // This would ideally check all possible ASTs, but we'll check a representative sample
        let ast_examples = vec![
            TinyAst::ExecuteCommand {
                command_name: "echo".to_string(),
                args: vec!["test".to_string()],
            },
            TinyAst::SetEnvironmentVariable {
                name: "VAR".to_string(),
                value: "val".to_string(),
            },
            TinyAst::ChangeDirectory {
                path: "/tmp".to_string(),
            },
            TinyAst::Sequence {
                commands: vec![TinyAst::ExecuteCommand {
                    command_name: "echo".to_string(),
                    args: vec![],
                }],
            },
        ];

        for ast in ast_examples {
            if ast.is_valid() {
                let posix_code = FormalEmitter::emit(&ast);

                // Emitter should always produce non-empty output for valid ASTs
                assert!(!posix_code.is_empty());

                // The output should be parseable (no panics)
                let initial_state = AbstractState::new();
                let _ = posix_semantics::eval_posix(&posix_code, initial_state);
            }
        }
    }
}

#[cfg(test)]
mod tests {
    use crate::formal::semantics::{posix_semantics, rash_semantics};
    use crate::formal::{AbstractState, FormalEmitter, TinyAst};

    #[test]
    fn test_echo_emitter_output() {
        let ast = TinyAst::ExecuteCommand {
            command_name: "echo".to_string(),
            args: vec!["hello".to_string()],
        };
        assert!(ast.is_valid());
        let posix_code = FormalEmitter::emit(&ast);
        assert!(!posix_code.is_empty());
        assert!(posix_code.contains("echo"));
    }

    #[test]
    fn test_assignment_emitter_output() {
        let ast = TinyAst::SetEnvironmentVariable {
            name: "MY_VAR".to_string(),
            value: "test_value".to_string(),
        };
        assert!(ast.is_valid());
        let posix_code = FormalEmitter::emit(&ast);
        assert!(!posix_code.is_empty());
    }

    #[test]
    fn test_cd_emitter_output() {
        let ast = TinyAst::ChangeDirectory {
            path: "/tmp".to_string(),
        };
        assert!(ast.is_valid());
        let posix_code = FormalEmitter::emit(&ast);
        assert!(!posix_code.is_empty());
    }

    #[test]
    fn test_sequence_emitter_output() {
        let ast = TinyAst::Sequence {
            commands: vec![
                TinyAst::ExecuteCommand {
                    command_name: "echo".to_string(),
                    args: vec!["first".to_string()],
                },
                TinyAst::ExecuteCommand {
                    command_name: "echo".to_string(),
                    args: vec!["second".to_string()],
                },
            ],
        };
        assert!(ast.is_valid());
        let posix_code = FormalEmitter::emit(&ast);
        assert!(!posix_code.is_empty());
    }

    #[test]
    fn test_echo_semantic_equivalence() {
        let ast = TinyAst::ExecuteCommand {
            command_name: "echo".to_string(),
            args: vec!["hello".to_string()],
        };
        let initial_state = AbstractState::new();
        if let Ok(rash_state) = rash_semantics::eval_rash(&ast, initial_state.clone()) {
            let posix_code = FormalEmitter::emit(&ast);
            if let Ok(posix_state) = posix_semantics::eval_posix(&posix_code, initial_state) {
                assert!(rash_state.is_equivalent(&posix_state));
            }
        }
    }

    #[test]
    fn test_assignment_semantic_equivalence() {
        let ast = TinyAst::SetEnvironmentVariable {
            name: "VAR".to_string(),
            value: "test".to_string(),
        };
        let initial_state = AbstractState::new();
        if let Ok(rash_state) = rash_semantics::eval_rash(&ast, initial_state.clone()) {
            let posix_code = FormalEmitter::emit(&ast);
            if let Ok(posix_state) = posix_semantics::eval_posix(&posix_code, initial_state) {
                assert!(rash_state.is_equivalent(&posix_state));
                assert_eq!(rash_state.get_env("VAR"), Some(&"test".to_string()));
            }
        }
    }
}