SAW User Manual

Warning

The SAW User Manual is currently being restructured/rewritten in large chunks.

It is likely that you will encounter typos, omissions, and otherwise incorrect or incomplete information about SAW and SAWScript’s features and operation.

Your help identifying these documentation issues is deeply appreciated, as it helps us prioritize and resolve them more quickly. Thanks for helping to make SAW better for everyone!

Contents

• Introduction
  • Notation
  • Outline
• Installing SAW
  • Binary Distributions
  • Building from Source
  • Installing Solvers
  • Installing the Python Bindings
  • Using the Docker Images
• Getting Started
  • Proofs In Files
  • Proofs About Code
• Getting Started with the Python Bindings
• Overview of SAW and SAW’s Structure
  • Key Subsystems
  • Typical / Common Use Cases
  • Terminology
  • Running Example
• Running SAW
  • Invoking saw
  • Invoking saw-remote-api
• Quick Introduction to the SAWScript Language
  • Types
  • Looking up Builtins
  • Monads
  • return
  • do Blocks
  • Expressions
  • Common Pitfalls
  • The REPL
  • Experimental and Deprecated Builtins
  • Haskell-Relative Notes
• Proofs about Cryptol Models
  • Importing Cryptol
  • Writing Cryptol Inline in SAWScript
  • Semantics of Imports
  • Semantics of Quasiquotation Blocks
  • Stating Proof Goals
  • Proving Things
  • Using Solvers
  • Uninterpreted Functions
  • Satisfiability
• Introduction to Symbolic Execution
  • Path Satisfiability
  • Symbolic Termination
  • Setting up Symbolic Execution
• Verifying Code Using Symbolic Execution
  • Simple Example for Getting Started
  • Languages for Specifications
  • Specifications
  • The LLVM Backend and LLVM Specifications
  • The JVM Backend and JVM Specifications
  • The MIR backend and Rust/MIR Specifications
  • Compositional Verification
  • Using Ghost State
  • Extracting Code
  • A Heap-Based Example
  • An Extended Example
  • Verifying Cryptol FFI functions
  • Multi-Step Proofs and Loop Invariants with Cuts
• Verifying Hardware Using Yosys
  • Processing VHDL With Yosys
  • Example: Ripple-Carry Adder
  • API Reference
• The SAWScript Language
  • Lexical Structure and Basic Syntax
  • Types
  • Statements
  • Expressions
  • The SAWScript REPL
• The Python Bindings
• Interactive Proofs
  • Transforming Term Values
  • Proofs about Terms
• Extraction to Rocq
  • Support Library
  • Cryptol module extraction
  • Proofs involving uninterpreted functions
  • Translation limitations and caveats
• Bisimulation Prover
  • Bisimulation Example
  • Understanding the proof goals
  • Limitations
• Command Line Reference
  • saw Command Line
  • saw Environment Variables
  • saw-remote-api Command Line
  • saw-remote-api Environment Variables
• SAWScript Language Reference
  • Using Cryptol in SAWScript
• SAWScript Commands Reference
• SAW REPL Reference
  • REPL Commands
• Python API Reference
• SAWCore Language Reference
• Mapping Cryptol to SAWCore
• Appendices
  • Formal Deprecation Process
  • Deprecated Items
  • Glossary