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
- Overview
- Structure of SAWScript
- Invoking SAW
- Cryptol and its Role in SAW
- Loading Code
- Analyzing Hardware Circuits using Yosys
- Creating Symbolic Variables
- Symbolic Execution
- Symbolic Termination
- The Term Type
- Specification-Based Verification
- Running a Verification
- Structure of a Specification
- Creating Fresh Variables
- The SetupValue and JVMValue Types
- Executing
- Return Values
- A First Simple Example (Revisited)
- Compositional Verification
- Specifying Heap Layout
- Specifying Heap Values
- Working with Compound Types
- Global variables
- Preconditions and Postconditions
- Assuming specifications
- A Heap-Based Example
- Using Ghost State
- An Extended Example
- Verifying Cryptol FFI functions
- Bisimulation Prover
- Transforming Term Values
- Proofs about Terms
- Extraction to the Coq theorem prover
- Formal Deprecation Process
- Appendices