### Initialize MIRAI Environment

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DeveloperGuide.md

Run the setup script to prepare the environment and install optional components.

```bash
./setup.sh
```

--------------------------------

### Install and Run MIRAI

Source: https://context7.com/endorlabs/mirai/llms.txt

Instructions for installing MIRAI and running analysis on a Rust project. Use flags to customize analysis behavior.

```bash
# Install MIRAI
git clone https://github.com/endorlabs/MIRAI.git
cd MIRAI
cargo install --locked --path ./checker

# Run analysis on your project
cd /path/to/your/project
cargo mirai

# Analyze test functions instead of main entry points
cargo mirai --tests

# Use MIRAI_FLAGS for additional options
MIRAI_FLAGS="--diag=verify" cargo mirai
MIRAI_FLAGS="--single_func my_function" cargo mirai
MIRAI_FLAGS="--body_analysis_timeout 120" cargo mirai
```

--------------------------------

### Install MIRAI into cargo

Source: https://github.com/endorlabs/mirai/blob/main/documentation/InstallationGuide.md

Build and install the MIRAI tool into the local cargo environment after navigating to the repository directory.

```bash
cargo install --locked --path ./checker
```

--------------------------------

### MIRAI Configuration JSON

Source: https://context7.com/endorlabs/mirai/llms.txt

Example configuration file for defining output paths, reductions, and Datalog settings.

```json
{
    "call_sites_output_path": "output/call_sites.json",
    "dot_output_path": "output/graph.dot",
    "reductions": [
        {"Slice": "target_function"},
        "Fold",
        "Clean",
        "Deduplicate"
    ],
    "included_crates": ["my_crate", "my_dependency"],
    "datalog_config": {
        "ddlog_output_path": "output/datalog/",
        "type_map_output_path": "output/types.json",
        "type_relations_path": "output/type_relations.json",
        "datalog_backend": "Souffle"
    }
}
```

--------------------------------

### Soufflé Datalog Proof Tree Example

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Illustrates a proof tree generated by Soufflé's explain command, showing the derivation of the Reachable(1, 3) relation through intermediate steps.

```text
              Edge(2, 2, 3)   
              -----------(R1) 
Edge(1, 1, 2) Reachable(2, 3) 
--------------------------(R2) 
       Reachable(1, 3)        
```

--------------------------------

### Soufflé Datalog Explain Command

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Command to initiate Soufflé's explain mode for analyzing proof trees of output relations. Requires Soufflé to be installed.

```bash
souffle -t explain reachable
```

--------------------------------

### Graphviz Dot Output Example

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

An example of a call graph represented in the Dot format, suitable for visualization with Graphviz tools. Nodes represent functions and edges represent calls.

```dot
digraph {
    0 [ label = "\"static[8787]::main\"" ]
    1 [ label = "\"static[8787]::fn1\"" ]
    2 [ label = "\"static[8787]::fn2\"" ]
    3 [ label = "\"static[8787]::fn3\"" ]
    0 -> 1 [ ]
    1 -> 2 [ ]
    2 -> 3 [ ]
}
```

--------------------------------

### Soufflé Datalog Explain Query

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Example of querying for the proof tree of a specific output relation in Soufflé Datalog. This helps understand how a result was derived.

```text
Enter command > explain Reachable(1,3)
```

--------------------------------

### Soufflé Datalog Reachability Analysis

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Defines input and output relations for a reachability analysis using Soufflé Datalog syntax. Requires Soufflé to be installed.

```datalog
.decl Edge(id: number, node1: number, node2: number)
.input Edge(io=file, delimiter=",")
.decl EdgeType(id: number, type_id: number)
.input EdgeType(io=file, delimiter=",")

.decl Reachable(node1: number, node2: number)
Reachable(node1, node2) :- Edge(_, node1, node2).
Reachable(node1, node3) :- Edge(_, node1, node2), Reachable(node2, node3).

.output Reachable(io=file, delimiter=",")
```

--------------------------------

### Differential Datalog Output Example

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Example of Differential Datalog output for a call graph, representing edges and their types. This format is used for logical analysis of the graph.

```datalog
start;
insert Edge(0,0,1);
insert Edge(1,1,2);
insert Edge(2,2,3);
insert EdgeType(0,0);
insert EdgeType(1,0);
insert EdgeType(2,0);
commit;
```

--------------------------------

### Running Differential Datalog Analysis

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Command to compile and run the Differential Datalog analysis. Ensure the Differential Datalog compiler and Cargo are installed.

```bash
ddlog -i reachable.dl &&
(cd base_ddlog && cargo build --release) &&
./reachable_ddlog/target/release/reachable_cli < ../graph.dat
```

--------------------------------

### Differential Datalog Reachability Output

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Example output from the Differential Datalog reachability analysis, showing pairs of nodes where the second node is reachable from the first.

```text
Reachable{.node1 = 0, .node2 = 1}
Reachable{.node1 = 0, .node2 = 2}
Reachable{.node1 = 0, .node2 = 3}
Reachable{.node1 = 1, .node2 = 2}
Reachable{.node1 = 1, .node2 = 3}
Reachable{.node1 = 2, .node2 = 3}
```

--------------------------------

### Example MIRAI Type Map

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

This map shows how type indexes in MIRAI relations correspond to actual Rust types. Use this to interpret type identifiers in graph relations.

```json
{
    "0": "u32",
    "1": "u8",
}
```

--------------------------------

### Build Mirai with Custom Rustc

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DebuggingRustc.md

After setting up the custom rustc, navigate to your Mirai project directory, override the toolchain, clean, and build Mirai.

```bash
# cd to your mirai directory
rustup override set custom
cargo clean
cargo build
```

--------------------------------

### Switch Back to Custom Build

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DebuggingRustc.md

After configuring the debugger, switch back to the custom rustc build to ensure Mirai loads correctly.

```bash
rustup override set custom
```

--------------------------------

### Build Custom Rustc

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DebuggingRustc.md

Clone rustc sources, configure build settings to true for debug options, and build the compiler. Link the built toolchain for use.

```bash
# cd to the directory where you want to keep the rust compiler sources
git clone https://github.com/rust-lang/rust/ rustc
cd rustc
cp config.toml.example config.toml
# Now edit config.toml and set debug, debug-assertions, debuginfo, and debuginfo-lines to true
./x.py build src/rustc
# You may have to change the architecture in the next command
rustup toolchain link custom build/nightly-x86_64-apple-darwin/stage2
```

--------------------------------

### Clone the MIRAI repository

Source: https://github.com/endorlabs/mirai/blob/main/documentation/InstallationGuide.md

Use these commands to download the source code from the official repository.

```bash
git clone https://github.com/endorlabs/MIRAI.git
cd MIRAI
```

--------------------------------

### Verify Conditions with verify!

Source: https://context7.com/endorlabs/mirai/llms.txt

Use the `verify!` macro to ask MIRAI to prove a condition at compile time. MIRAI emits a diagnostic if the condition cannot be proven.

```rust
use mirai_annotations::*

fn checked_operations(x: i32) {
    precondition!(x > 0 && x < 100);

    let doubled = x * 2;
    verify!(doubled > 0);      // MIRAI proves this
    verify!(doubled < 200);    // MIRAI proves this

    let squared = x * x;
    verify!(squared > 0);      // MIRAI proves this
}

pub fn main() {
    let mut sum = 0i32;
    for i in 0..10 {
        sum += i;
    }
    verify!(sum == 45); // MIRAI verifies loop result
}
```

--------------------------------

### VSCode Debug Configuration for Mirai

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DebuggingRustc.md

Configure VSCode's launch.json to use the custom rustc build for debugging Mirai. Ensure the DYLD_LIBRARY_PATH is set correctly.

```json
{
    "type": "lldb",
    "request": "launch",
    "name": "Debug executable 'mirai'",
    "cargo": {
        "args": [
            "build",
            "--bin=mirai",
            "--package=Mirai"
        ],
        "filter": {
            "kind": "bin"
        }
    },
    "env": {
       "DYLD_LIBRARY_PATH": "${env:HOME}/.rustup/toolchains/custom/lib",
    },
    "sourceLanguages": ["rust"],
    "args": [<what you'll give to rustc, split into an array of strings using space as the delimiter>],
    "cwd": "${workspaceFolder}/checker",
}
```

--------------------------------

### Alias MIRAI Binary

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DeveloperGuide.md

Create a shell alias to run the MIRAI binary with the correct dynamic library path.

```bash
alias mirai="DYLD_LIBRARY_PATH=$(rustc --print sysroot)/lib ~/mirai/target/debug/mirai"
```

--------------------------------

### CLion Command for Testing MIRAI Integration Tests

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DeveloperGuide.md

Use this command in CLion to run the integration tests for the MIRAI project.

```bash
test --package mirai --test integration_tests ""
```

--------------------------------

### Running Soufflé Datalog Analysis

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Command to run the Soufflé Datalog reachability analysis. The output will be saved to Reachable.csv.

```bash
souffle reachable.dl
```

--------------------------------

### Configure MIRAI Diagnostic Levels

Source: https://context7.com/endorlabs/mirai/llms.txt

Commands to set diagnostic sensitivity and logging levels via environment variables.

```bash
# Default mode: suppresses potential false positives
MIRAI_FLAGS="--diag=default" cargo mirai

# Verify mode: reports functions with potential incomplete analysis
MIRAI_FLAGS="--diag=verify" cargo mirai

# Library mode: requires explicit preconditions, flags any unguarded panic
MIRAI_FLAGS="--diag=library" cargo mirai

# Paranoid mode: flags any issue that may be an error
MIRAI_FLAGS="--diag=paranoid" cargo mirai

# Combine with other options
MIRAI_FLAGS="--diag=verify --body_analysis_timeout 60" cargo mirai

# Enable verbose logging for debugging
MIRAI_LOG=debug cargo mirai
MIRAI_LOG=trace cargo mirai
```

--------------------------------

### Generate Call Graphs

Source: https://context7.com/endorlabs/mirai/llms.txt

Configure and execute the MIRAI call graph generator to visualize program structure.

```bash
# Create call graph configuration file
cat > call_graph_config.json << 'EOF'
{
    "dot_output_path": "output/graph.dot",
    "call_sites_output_path": "output/call_sites.json",
    "reductions": ["Fold", "Clean", "Deduplicate"],
    "included_crates": ["my_crate"]
}
EOF

# Run MIRAI with call graph generation
MIRAI_FLAGS="--call_graph_config call_graph_config.json" cargo mirai
```

--------------------------------

### VSCode Debugging Configuration for MIRAI Executable

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DeveloperGuide.md

Add this to your launch.json to debug the MIRAI executable. Ensure DYLD_LIBRARY_PATH is correctly set for your environment.

```json
    {
        "type": "lldb",
        "request": "launch",
        "name": "Debug executable 'mirai'",
        "cargo": {
            "args": [
                "build",
                "--bin=mirai",
                "--package=mirai"
            ],
            "filter": {
                "kind": "bin"
            }
        },
        "env": {
           "DYLD_LIBRARY_PATH": "${env:HOME}/.rustup/toolchains/nightly-x86_64-apple-darwin/lib",
        },
        "sourceLanguages": ["rust"],
        "args": [<what you'll give to rustc, split into an array of strings using space as the delimiter,
        remember to append the --extern option described in the CLion section>],
        "cwd": "${workspaceFolder}/checker",
    },
```

--------------------------------

### Declare Function Postconditions with postcondition!

Source: https://context7.com/endorlabs/mirai/llms.txt

Use the `postcondition!` macro to specify conditions that must hold true after a function returns. MIRAI verifies these conditions.

```rust
use mirai_annotations::*

fn increment_positive(x: i32) -> i32 {
    precondition!(x > 0);
    let result = x + 1;
    postcondition!(result > x, "result must be greater than input");
    result
}

fn initialize_buffer(buffer: &mut [u8; 256]) {
    for i in 0..256 {
        buffer[i] = 0;
    }
    postcondition!(buffer[0] == 0, "buffer must be zeroed");
}

pub fn main() {
    let value = increment_positive(5);
    // MIRAI knows value > 5 after this call due to postcondition
    verify!(value > 5);
}
```

--------------------------------

### Configure CLion Debugging

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DeveloperGuide.md

Configuration settings for debugging a test case in CLion.

```text
run --package mirai --bin mirai -- tests/run-pass/assume.rs --edition=2021
  --extern mirai_annotations=/Users/hermanv/projects/mirai/target/debug/deps/libmirai_annotations-fceb8359d1c48f91.rlib
```

--------------------------------

### Assert Unreachable Code Paths

Source: https://context7.com/endorlabs/mirai/llms.txt

Use verify_unreachable! to prove a path is unreachable and assume_unreachable! to instruct MIRAI to treat a path as unreachable.

```rust
use mirai_annotations::*;

enum State {
    Ready,
    Running,
    Stopped,
}

fn handle_state(state: State) {
    match state {
        State::Ready => println!("Ready to start"),
        State::Running => println!("Currently running"),
        State::Stopped => println!("Has stopped"),
    }
}

fn handle_state_subset(state: State) {
    precondition!(matches!(state, State::Ready | State::Running));

    match state {
        State::Ready => println!("Ready"),
        State::Running => println!("Running"),
        State::Stopped => {
            // MIRAI verifies this branch cannot be reached given precondition
            verify_unreachable!("Stopped state should not occur");
        }
    }
}

fn external_guarantee(x: i32) {
    // External system guarantees x is positive
    if x <= 0 {
        assume_unreachable!("External system guarantees positive values");
    }

    // MIRAI assumes x > 0 from here
    verify!(x > 0);
}
```

--------------------------------

### MIRAI Call Graph Input for Datalog

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Provides sample input data for the Datalog reachability analysis, defining edges and edge types. This data is processed by MIRAI.

```shell
start;
insert Edge(0,0,1);
insert Edge(1,1,2);
insert Edge(2,2,3);
insert EdgeType(0,0);
insert EdgeType(1,0);
insert EdgeType(2,0);
commit;
dump Reachable;
```

--------------------------------

### Switch to Nightly Toolchain

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DebuggingRustc.md

Switch back to the nightly toolchain to prevent crashes with the Rust Language Service (RLS) in IDEs.

```bash
rustup override set nightly
```

--------------------------------

### Declare Function Preconditions with precondition!

Source: https://context7.com/endorlabs/mirai/llms.txt

Use the `precondition!` macro to enforce conditions that must be true before a function is called. MIRAI verifies callers satisfy these conditions.

```rust
use mirai_annotations::*

fn safe_divide(numerator: i32, denominator: i32) -> i32 {
    precondition!(denominator != 0, "denominator must not be zero");
    numerator / denominator
}

fn safe_array_access(arr: &mut [i32; 10], index: usize) {
    precondition!(index < 10, "index must be within bounds");
    arr[index] = 42;
}

pub fn main() {
    // Valid call - satisfies precondition
    let result = safe_divide(10, 2);

    // Invalid call - MIRAI reports: "unsatisfied precondition: denominator must not be zero"
    // let bad_result = safe_divide(10, 0);
}
```

--------------------------------

### Implement Design by Contracts

Source: https://context7.com/endorlabs/mirai/llms.txt

Integrate the contracts crate with MIRAI to define pre- and post-conditions for functions using attributes.

```rust
use contracts::*;
use mirai_annotations::*;

#[allow(dead_code)]
pub struct Item {
    name: String,
    price: u64,
}

impl Item {
    #[requires(!name.is_empty() && price > 0)]
    #[ensures(ret.price == price)]
    pub fn new(name: &str, price: u64) -> Item {
        Item {
            name: name.to_string(),
            price,
        }
    }
}

pub struct ShoppingCart {
    items: Vec<Item>,
    total: u64,
}

impl ShoppingCart {
    pub fn new() -> ShoppingCart {
        ShoppingCart {
            items: vec![],
            total: 0,
        }
    }

    #[requires(self.total <= u64::MAX - item.price)]
    #[requires(self.items.len() < usize::MAX)]
    #[ensures(self.total == old(self.total) + item.price)]
    pub fn add(&mut self, item: Item) {
        self.total += item.price;
        self.items.push(item);
    }

    #[ensures(ret == old(self.total))]
    #[ensures(self.total == 0)]
    pub fn checkout(&mut self) -> u64 {
        let bill = self.total;
        self.total = 0;
        self.items.clear();
        bill
    }
}

pub fn main() {
    let mut cart = ShoppingCart::new();
    cart.add(Item::new("iPad Pro", 899));
    cart.add(Item::new("iPad Folio", 169));
    assert_eq!(cart.checkout(), 899 + 169);
}
```

--------------------------------

### Generate Graphviz Visualization

Source: https://context7.com/endorlabs/mirai/llms.txt

Converts a DOT file into a PNG image using the Graphviz dot command.

```bash
dot -Tpng output/graph.dot -o output/graph.png
```

--------------------------------

### Set Debug Environment Variables

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DeveloperGuide.md

Required environment variables for debugging MIRAI in CLion.

```text
DYLD_LIBRARY_PATH=/Users/hermanv/.rustup/toolchains/nightly-YYYY-MM-DD-TA/lib;
MIRAI_LOG=debug
```

--------------------------------

### Runtime-Checked Assumptions and Verifications

Source: https://context7.com/endorlabs/mirai/llms.txt

Use checked_assume! and checked_verify! to provide runtime assertions that also serve as static analysis constraints for MIRAI.

```rust
use mirai_annotations::*;

fn safe_sqrt(x: f64) -> f64 {
    // Checked at runtime in debug/release, assumed by MIRAI
    checked_assume!(x >= 0.0, "sqrt requires non-negative input");
    x.sqrt()
}

fn validate_and_process(value: i32) -> i32 {
    // Runtime assert + MIRAI verification
    checked_verify!(value > 0, "value must be positive");
    checked_verify!(value < 1000, "value must be under 1000");

    value * 2
}

// Also available: checked_assume_eq!, checked_assume_ne!
// checked_verify_eq!, checked_verify_ne!
// debug_checked_* variants for debug-only runtime checks
```

--------------------------------

### VSCode Debugging Configuration for MIRAI Integration Tests

Source: https://github.com/endorlabs/mirai/blob/main/documentation/DeveloperGuide.md

Configure this launch setting in VSCode to debug integration tests. It requires manually specifying the program path and setting environment variables.

```json
    {
        "type": "lldb",
        "request": "launch",
        "name": "Launch",
        "program": "${workspaceFolder}/target/debug/deps/integration_tests-0ca00d8d322a6adc",
        "sourceLanguages": ["rust"],
        "args": [],
        "cwd": "${workspaceFolder}/checker",
        "env": {
            "DYLD_LIBRARY_PATH": "${env:HOME}/.rustup/toolchains/nightly-x86_64-apple-darwin/lib",
            "MIRAI_LOG": "debug",
        }
    },
```

--------------------------------

### Track Model Fields with set_model_field! and get_model_field!

Source: https://context7.com/endorlabs/mirai/llms.txt

Use these macros to define metadata fields on structs that exist only during MIRAI analysis, avoiding runtime overhead.

```rust
use mirai_annotations::*;

struct Connection {
    // Actual runtime fields
    host: String,
    port: u16,
}

impl Connection {
    fn new(host: &str, port: u16) -> Self {
        let conn = Connection {
            host: host.to_string(),
            port,
        };
        // Set model field to track authentication status (no runtime cost)
        set_model_field!(&conn, authenticated, false);
        conn
    }

    fn authenticate(&mut self, password: &str) -> bool {
        if password == "secret" {
            set_model_field!(self, authenticated, true);
            true
        } else {
            false
        }
    }

    fn send_secure_data(&self, data: &[u8]) {
        // Require authentication before sending
        precondition!(get_model_field!(self, authenticated, false) == true);
        // Send data...
    }
}

pub fn main() {
    let mut conn = Connection::new("example.com", 443);
    conn.authenticate("secret");

    // MIRAI verifies authentication status via model field
    verify!(get_model_field!(&conn, authenticated, false) == true);
    conn.send_secure_data(b"sensitive");
}
```

--------------------------------

### Soufflé Datalog Input Facts for Edge

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Input facts for the Edge relation in Soufflé Datalog, formatted as comma-separated values. Each relation should be in a separate file.

```text
0,0,1
1,1,2
2,2,3
```

--------------------------------

### Graphviz Dot Command

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Command to generate a PDF visualization of a call graph from a Dot file using the Graphviz 'dot' tool.

```bash
$ dot -Tpdf graph.dot -o graph.pdf
```

--------------------------------

### Create Abstract Values for Symbolic Analysis

Source: https://context7.com/endorlabs/mirai/llms.txt

Use abstract_value! to represent unknown inputs during symbolic analysis, allowing MIRAI to prove properties about ranges and conditional logic.

```rust
use mirai_annotations::*;

pub fn test_range_arithmetic() {
    let a = abstract_value!(6i32);
    let b = abstract_value!(7i32);

    assume!(4 < a && a < 8);  // a in [5,7]
    assume!(5 < b && b < 9);  // b in [6,8]

    // MIRAI proves the product is in range [30,56]
    verify!(30 <= a * b && a * b <= 56);
}

pub fn test_conditional_logic() {
    let input = abstract_value!(0i32);
    assume!(input >= 0 && input <= 100);

    let output = if input < 50 { input * 2 } else { input + 50 };

    verify!(output >= 0);
    verify!(output <= 150);
}
```

--------------------------------

### Soufflé Datalog Input Facts for EdgeType

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Input facts for the EdgeType relation in Soufflé Datalog, formatted as comma-separated values. Each relation should be in a separate file.

```text
0,0
1,0
2,0
```

--------------------------------

### Assume Conditions with assume!

Source: https://context7.com/endorlabs/mirai/llms.txt

Use the `assume!` macro to instruct MIRAI to treat a condition as true without runtime checking. Useful for facts difficult to express as preconditions or when interfacing with external code.

```rust
use mirai_annotations::*

fn process_external_data(data: &[u8]) {
    // Assume external data validation already occurred
    assume!(data.len() >= 4);

    let header = u32::from_le_bytes([data[0], data[1], data[2], data[3]]);
    verify!(header >= 0); // MIRAI can prove this
}

fn work_with_constraints(a: i32, b: i32) {
    assume!(4 < a && a < 8);  // a in [5,7]
    assume!(5 < b && b < 9);  // b in [6,8]
    verify!(30 <= a * b && a * b <= 56); // MIRAI proves a*b in [30,56]
}
```

--------------------------------

### Differential Datalog Reachability Analysis

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Defines input and output relations for a reachability analysis in Differential Datalog. Requires the Differential Datalog library.

```datalog
input relation Edge(id: u32, node1: u32, node2: u32)
input relation EdgeType(id: u32, type_id: u32)

output relation Reachable(node1: u32, node2: u32)
Reachable(node1, node2) :- Edge(_, node1, node2).
Reachable(node1, node3) :- Edge(_, node1, node2), Reachable(node2, node3).
```

--------------------------------

### Constant-Time Verification

Source: https://context7.com/endorlabs/mirai/llms.txt

Use tag analysis to verify that sensitive data does not influence program timing, preventing side-channel attacks.

```rust
#![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]

use mirai_annotations::*;

#[cfg(mirai)]
use mirai_annotations::{TagPropagation, TagPropagationSet};

#[cfg(mirai)]
struct SecretTaintKind<const MASK: TagPropagationSet> {}

// Only propagate through comparison operations
#[cfg(mirai)]
const SECRET_TAINT_MASK: TagPropagationSet = tag_propagation_set!(
    TagPropagation::Equals,
    TagPropagation::Ne,
    TagPropagation::GreaterThan,
    TagPropagation::LessThan
);

#[cfg(mirai)]
type SecretTaint = SecretTaintKind<SECRET_TAINT_MASK>;
#[cfg(not(mirai))]
type SecretTaint = ();

// NON-CONSTANT TIME - MIRAI flags this with --constant_time SecretTaintKind
fn compare_vulnerable(secret: &[i32; 32], input: &[i32; 32]) -> bool {
    precondition!(has_tag!(secret, SecretTaint));
    for i in 0..32 {
        if secret[i] != input[i] {
            return false;  // Early return leaks timing information
        }
    }
    true
}

// CONSTANT TIME - No timing side channel
fn compare_safe(secret: &[i32; 32], input: &[i32; 32]) -> bool {
    precondition!(has_tag!(secret, SecretTaint));
    let mut result = true;
    for i in 0..32 {
        result &= secret[i] == input[i];  // No early return
    }
    result
}

// Run with: MIRAI_FLAGS="--constant_time SecretTaintKind" cargo mirai
```

--------------------------------

### MIRAI Call Graph Configuration Schema

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

This JSON schema defines the structure for configuring MIRAI's call graph generator. It specifies paths for output files, reduction strategies, included crates, and Datalog backend settings.

```json
{
    "call_sites_output_path": "path/to/call_sites.json",
    "dot_output_path": "path/to/graph.dot",
    "reductions": [
        {"Slice": "function name"},
        "Fold",
        "Clean",
        "Deduplicate",
    ],
    "included_crates": ["crate_name"],
    "datalog_config": {
        "ddlog_output_path": "path/to/graph.dat" | "path/to/datalog/",
        "type_map_output_path": "path/to/types.json",
        "type_relations_path": "path/to/type_relations.json",
        "datalog_backend": "DifferentialDatalog" | "Souffle"
    },
}

```

--------------------------------

### Fold Reduction Configuration

Source: https://github.com/endorlabs/mirai/blob/main/documentation/CallGraph.md

Configures the Fold reduction to include only nodes within specified crates, preserving paths through excluded nodes. This helps in analyzing specific crate interactions.

```json
"Fold"
```

--------------------------------

### Taint Analysis with Tags

Source: https://context7.com/endorlabs/mirai/llms.txt

Attach tags to values using add_tag! and verify them with has_tag! to track data flow and enforce security policies.

```rust
#![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]

use mirai_annotations::*;

#[cfg(mirai)]
use mirai_annotations::{TagPropagation, TagPropagationSet};

#[cfg(mirai)]
struct TaintedKind<const MASK: TagPropagationSet> {}

#[cfg(mirai)]
const TAINTED_MASK: TagPropagationSet = tag_propagation_set!(TagPropagation::SubComponent);

#[cfg(mirai)]
type Tainted = TaintedKind<TAINTED_MASK>;
#[cfg(not(mirai))]
type Tainted = ();

#[cfg(mirai)]
struct SanitizedKind<const MASK: TagPropagationSet> {}

#[cfg(mirai)]
const SANITIZED_MASK: TagPropagationSet = tag_propagation_set!(TagPropagation::SubComponent);

#[cfg(mirai)]
type Sanitized = SanitizedKind<SANITIZED_MASK>;
#[cfg(not(mirai))]
type Sanitized = ();

fn read_user_input() -> String {
    let input = "user data".to_string();
    add_tag!(&input, Tainted);  // Mark as tainted
    input
}

fn sanitize(input: &str) -> String {
    // Perform validation/sanitization
    let clean = input.trim().to_string();
    add_tag!(&clean, Sanitized);  // Mark as sanitized
    clean
}

fn send_to_database(data: &str) {
    // Require data is either not tainted OR has been sanitized
    precondition!(does_not_have_tag!(data, Tainted) || has_tag!(data, Sanitized));
    // Safe to use data
}
```

--------------------------------

### Annotate Trait Methods with Postconditions

Source: https://github.com/endorlabs/mirai/blob/main/documentation/TagAnalysis.md

Define trait methods with postconditions to ensure all implementors satisfy the contract. The `postcondition!` macro checks the condition after the method execution.

```rust
trait TaintRemovable {
    fn remove_taint(&mut self) {
        self._impl_remove_taint();
        postcondition!(does_not_have_tag(self, SecretTaint));
    }

    fn _impl_remove_taint(&mut self);
}
```

--------------------------------

### Define tag propagation behavior

Source: https://github.com/endorlabs/mirai/blob/main/documentation/TagAnalysis.md

Configure which operations propagate a tag and define a type alias for the tag, ensuring compatibility with non-MIRAI builds.

```rust
#[cfg(mirai)]
const SECRET_TAINT_MASK = tag_propagation_set!(TagPropagation::Equals, TagPropagation::Ne);

#[cfg(mirai)]
type SecretTaint = SecretTaintKind<SECRET_TAINT_MASK>;
#[cfg(not(mirai))]
type SecretTaint = (); // Ensures code compiles in non-MIRAI builds
```