Module formal 

Formal verification and proof generation Formal verification module for the rash emitter

This module implements formal verification of the emitter’s correctness for a tiny subset of the rash AST, proving semantic equivalence between rash AST nodes and their emitted POSIX shell commands.

Safety Note

Formal verification uses unwrap() on validated proofs and checked invariants.

Re-exports

pub use abstract_state::*;

pub use emitter::*;

pub use enhanced_state::*;

pub use inspector::*;

pub use semantics::*;

pub use tiny_ast::*;

Modules

abstract_state

Abstract state representation for formal verification

emitter

Formal emitter for the tiny AST subset

enhanced_state

Enhanced Abstract State with Permission Tracking

inspector

Proof inspection and intermediate artifact generation

semantics

Operational semantics for rash AST and POSIX shell

tiny_ast

Tiny subset of rash AST for formal verification