A sophisticated Python tool that converts ARM CCA's Realm Management Monitor (RMM) specification documents into Verus verification code for formal analysis.
The scope is a shorthand for spectroscope. The name reflects the way a spectroscope takes incoming light (spec) and shines it through a prism.
- Multi-Specification Support: Supports EAC5, REL0, and ALP11-ALP14 specifications
- Flexible Input Processing: Handles both PDF and text input files
- Multiple Processing Modes: Reasoning, rule-based checking, and raw parsing modes
- Formal Verification: Generates Verus code for verification
1. Install pdftotext
sudo apt-get install libpoppler-dev2. Install Verus
Currently, version 0.2025.01.11 should be used. Please follow its installation instructions.
git clone https://github.com/verus-lang/verus.git
cd verus
git reset --hard bec74a67d9281a4f51a7e1855760c5d16d8f63ff
cd ./source
./tools/get-z3.sh
source ../tools/activate
vargo build --release3. Prepare the RMM specification
Download the PDF files using the following links (1.0-eac5,
1.0-rel0).
Download the zip files using the following links (1.1-alp11,
1.1-alp12)
and extract the PDF files from them.
Ensure that the PDF files are placed in the same directory as the scope script.
# Run with default settings (EAC5 text file, reasoning mode)
./scope
# Process a PDF file directly
./scope --input-type pdf --target eac5
# Use rule-based checking mode
./scope --mode rule --target alp14
# Process with custom settings
./scope --target rel0 --mode reason --input-type pdf--target: Specify target specification (eac5, rel0, alp11, alp12, alp13, alp14)--mode: Processing mode (reason, rule, raw)--input-type: Input file type (pdf, txt)
- Reasoning Mode (
--mode reason): Full conversion to Verus verification code - Rule-based check Mode (
--mode rule): Analysis and validation without conversion - Raw Mode (
--mode raw): Document parsing without processing
- Text Input (
--input-type txt): Process pre-converted text files - PDF Input (
--input-type pdf): Automatically convert PDF to text
# Process EAC5 specification (default)
./scope
# Process ALP14 specification with text input
./scope --target alp14 --input-type txt
# Process REL0 specification with PDF input
./scope --target rel0 --input-type pdf
# Generate only RMM model without processing dependency tables
./scope --target eac5 --no-dependency# Full conversion to Verus code
./scope --target eac5 --mode reason
# Rule-based checking for analysis
./scope --target alp13 --mode rule
# Raw document parsing
./scope --target alp12 --mode raw# Direct PDF processing
./scope --input-type pdf --target eac5
# PDF processing with rule-based analysis
./scope --input-type pdf --target alp14 --mode rule| Target | Specification version |
|---|---|
| eac5 | 1.0-eac5 |
| rel0 | 1.0-rel0 |
| alp11 | 1.1-alp11 |
| alp12 | 1.1-alp12 |
| alp13 | 1.1-alp13 |
| alp14 | 1.1-alp14 |
The scope generates different outputs based on the processing mode:
- Reasoning Mode: Generate Verus verification code
- Rule-based checks Mode: Analysis reports and validation results
- Raw Mode: Parsed specification data and dependencies
# Check if pdftotext is installed
pdftotext -v
# Install if missing
sudo apt-get install poppler-utils
# Verify PDF file exists
ls -la DEN0137_1.0-eac5_rmm-arch_external.pdf- "PDF file does not exist": Ensure the PDF file is present
- "pdftotext is not available": Install poppler-utils
- "Target version not supported": Use a supported specification
The scope consists of several key components:
- Document Preprocessor: Cleans and normalizes specification text
- Type Parser: Extracts enums, structs, and type definitions
- Interface Parser: Processes command interfaces and conditions
- Code Generator: Converts specifications to Verus code
Apache-2.0 license
For issues and questions:
- Check the troubleshooting section
- Review the USAGE.md for detailed examples
- Upload issues in Issues page