v5.0.0

scip-callgraph v5.0.0

What's New in v4.0.0

BREAKING CHANGE: Restructured to Cargo workspace. Commands now require -p metrics-cli flag when using cargo run.

New Features

• Metrics Pipeline: Complete toolchain for computing code, spec, and proof metrics
• Halstead Metrics for Verus Specs: First-of-kind metrics for requires/ensures clauses
• Transitive Proof Metrics: Aggregate metrics across lemma dependencies
• One-Command Pipeline: run_full_pipeline orchestrates all metrics computation
• Visualization Support: Python script for correlation analysis plots

Key Findings

• Code complexity does NOT predict proof difficulty (r ≈ 0)
• Spec complexity does NOT predict proof difficulty (r = -0.27)
• Proof effort is highly concentrated in foundational functions

Installation

Download the appropriate archive for your platform and extract it:

Linux

tar -xzf scip-callgraph-v5.0.0-x86_64-unknown-linux-gnu.tar.gz
cd scip-callgraph-v5.0.0-x86_64-unknown-linux-gnu
sudo cp * /usr/local/bin/

macOS

tar -xzf scip-callgraph-v5.0.0-x86_64-apple-darwin.tar.gz
cd scip-callgraph-v5.0.0-x86_64-apple-darwin
sudo cp * /usr/local/bin/

Windows

Extract the zip file and add the directory to your PATH.

Tools Included

Core Tools

• detect_unused_specs - Detect potentially unused Verus specifications
• generate_index_scip_json - Generate SCIP JSON index files
• generate_call_graph_dot - Generate call graph visualizations
• generate_function_subgraph_dot - Generate function-level subgraphs
• generate_file_subgraph_dot - Generate file-level subgraphs
• generate_files_subgraph_dot - Generate multi-file subgraphs
• write_atoms - Convert call graphs to atoms JSON format

Metrics Pipeline Tools (NEW)

• run_full_pipeline - One-command metrics computation (~17s)
• compute_metrics - Compute Halstead metrics for Verus specs
• compute_proof_metrics - Compute metrics for proof blocks with lemma traversal
• enrich_csv_with_metrics - Add RCA code metrics to CSV
• enrich_csv_complete - Combine all metrics into final CSV

Quick Start

# Full metrics pipeline
run_full_pipeline \
  --scip index.json \
  --csv functions.csv \
  --rca-dir rca_output/ \
  --proof-csv proofs.csv \
  --output-dir metrics/

# Or individual steps
write_atoms index.json atoms.json
compute_metrics atoms.json with_specs.json
compute_proof_metrics with_specs.json with_proofs.json

Documentation

• README
• Metrics Pipeline Guide
• Correlation Analysis Findings

Requirements

• verus-analyzer must be installed
• scip CLI tool must be installed
• For visualization: Python 3 with pandas, matplotlib, seaborn

v3.2.1

scip-callgraph v3.2.1

Installation

Download the appropriate archive for your platform and extract it:

Linux

tar -xzf scip-callgraph-v3.2.1-x86_64-unknown-linux-gnu.tar.gz
cd scip-callgraph-v3.2.1-x86_64-unknown-linux-gnu
sudo cp detect_unused_specs /usr/local/bin/

macOS

tar -xzf scip-callgraph-v3.2.1-x86_64-apple-darwin.tar.gz
cd scip-callgraph-v3.2.1-x86_64-apple-darwin
sudo cp detect_unused_specs /usr/local/bin/

Windows

Extract the zip file and add the directory to your PATH.

Tools Included

• detect_unused_specs - Detect potentially unused Verus specifications
• generate_index_scip_json - Generate SCIP JSON index files
• generate_call_graph_dot - Generate call graph visualizations
• generate_function_subgraph_dot - Generate function-level subgraphs
• generate_file_subgraph_dot - Generate file-level subgraphs
• generate_files_subgraph_dot - Generate multi-file subgraphs
• write_atoms - Convert call graphs to atoms JSON format

Quick Start

# Detect unused specs in your project
detect_unused_specs /path/to/verus/project

# Generate SCIP index
generate_index_scip_json /path/to/project

Documentation

See the repository README for full documentation.

Requirements

• verus-analyzer must be installed
• scip CLI tool must be installed

v3.2.0

scip-callgraph v3.2.0

Installation

Download the appropriate archive for your platform and extract it:

Linux

tar -xzf scip-callgraph-v3.2.0-x86_64-unknown-linux-gnu.tar.gz
cd scip-callgraph-v3.2.0-x86_64-unknown-linux-gnu
sudo cp detect_unused_specs /usr/local/bin/

macOS

tar -xzf scip-callgraph-v3.2.0-x86_64-apple-darwin.tar.gz
cd scip-callgraph-v3.2.0-x86_64-apple-darwin
sudo cp detect_unused_specs /usr/local/bin/

Windows

Extract the zip file and add the directory to your PATH.

Tools Included

• detect_unused_specs - Detect potentially unused Verus specifications
• generate_index_scip_json - Generate SCIP JSON index files
• generate_call_graph_dot - Generate call graph visualizations
• generate_function_subgraph_dot - Generate function-level subgraphs
• generate_file_subgraph_dot - Generate file-level subgraphs
• generate_files_subgraph_dot - Generate multi-file subgraphs
• write_atoms - Convert call graphs to atoms JSON format

Quick Start

# Detect unused specs in your project
detect_unused_specs /path/to/verus/project

# Generate SCIP index
generate_index_scip_json /path/to/project

Documentation

See the repository README for full documentation.

Requirements

• verus-analyzer must be installed
• scip CLI tool must be installed

v3.1.1

scip-callgraph v3.1.1

Installation

Download the appropriate archive for your platform and extract it:

Linux

tar -xzf scip-callgraph-v3.1.1-x86_64-unknown-linux-gnu.tar.gz
cd scip-callgraph-v3.1.1-x86_64-unknown-linux-gnu
sudo cp detect_unused_specs /usr/local/bin/

macOS

tar -xzf scip-callgraph-v3.1.1-x86_64-apple-darwin.tar.gz
cd scip-callgraph-v3.1.1-x86_64-apple-darwin
sudo cp detect_unused_specs /usr/local/bin/

Windows

Extract the zip file and add the directory to your PATH.

Tools Included

• detect_unused_specs - Detect potentially unused Verus specifications
• generate_index_scip_json - Generate SCIP JSON index files
• generate_call_graph_dot - Generate call graph visualizations
• generate_function_subgraph_dot - Generate function-level subgraphs
• generate_file_subgraph_dot - Generate file-level subgraphs
• generate_files_subgraph_dot - Generate multi-file subgraphs
• write_atoms - Convert call graphs to atoms JSON format

Quick Start

# Detect unused specs in your project
detect_unused_specs /path/to/verus/project

# Generate SCIP index
generate_index_scip_json /path/to/project

Documentation

See the repository README for full documentation.

Requirements

• verus-analyzer must be installed
• scip CLI tool must be installed

v2.0.0

Function Subgraph Analyzer Release

This release contains the generate_function_subgraph_dot binary for multiple platforms.

Available Binaries:

• Linux x86_64: generate_function_subgraph_dot-linux-x86_64.tar.gz
• Windows x86_64: generate_function_subgraph_dot-windows-x86_64.exe.zip
• macOS x86_64: generate_function_subgraph_dot-macos-x86_64.tar.gz
• macOS ARM64: generate_function_subgraph_dot-macos-arm64.tar.gz

Usage:

./generate_function_subgraph_dot <input-scip-json> <output-dot-file> <function-name1> [flags...]

Flags:

• --include-callees: Include functions called by the specified functions
• --include-callers: Include functions that call the specified functions
• --depth <n>: Limit the caller/callee expansion to depth n
• --filter-non-libsignal-sources: Filter out non-libsignal sources

See the README files included in each archive for detailed usage instructions.

v1.0.1

Function Subgraph Analyzer Release

This release contains the generate_function_subgraph_dot binary for multiple platforms.

Available Binaries:

• Linux x86_64: generate_function_subgraph_dot-linux-x86_64.tar.gz
• Windows x86_64: generate_function_subgraph_dot-windows-x86_64.exe.zip
• macOS x86_64: generate_function_subgraph_dot-macos-x86_64.tar.gz
• macOS ARM64: generate_function_subgraph_dot-macos-arm64.tar.gz

Usage:

./generate_function_subgraph_dot <input-scip-json> <output-dot-file> <function-name1> [flags...]

Flags:

• --include-callees: Include functions called by the specified functions
• --include-callers: Include functions that call the specified functions
• --depth <n>: Limit the caller/callee expansion to depth n
• --filter-non-libsignal-sources: Filter out non-libsignal sources

See the README files included in each archive for detailed usage instructions.