SAW User Manual Issues and Recommendations

[smithdtyler]

Overview

The SAW User Manual has a couple of significant issues:

• The flow and intent of the manual is inconsistent--sometimes it reads like a tutorial, other times like a reference
• Terminology is frequently used before it is defined
• Style and level of detail is inconsistent between supported input types (Java vs MIR vs LLVM)
• Comprehension aids like running examples and graphical representations of concepts are missing

In this issue I outline a suggestion for a new SAW manual organization and provide recommendations for new content and fixes for specific issues

---

Current Structure

The SAW manual today flows as follows:

• Overview
• Invoking SAW
• Structure of SAWScript
  • Syntax
  • Basic Types and Values
  • Basic Expression Forms
  • Other Basic Functions
• The Term Type
• Cryptol and its Role in SAW
• Transforming Term Values
  • Rewriting
  • Folding and Unfolding
  • Other Built-in Transformation and Inspection Functions
  • Loading and Storing Terms
• Proofs about Terms
  • Automated Tactics
  • Proof Script Diagnostics
  • Rewriting in Proof Scripts
  • Other Transformations
  • Caching Solver Results
  • Other External Provers
  • Offline Provers
  • Finishing Proofs without External Solvers. Move all deprecated content into the appendix.depricated section.
  • Multiple Goals
  • Proof Failure and Satisfying Assignments
  • AIG Values and Proofs
• Symbolic Execution
• Symbolic Termination
• Loading Code
  • Loading LLVM
  • Loading Java
  • Loading MIR
  • Notes on Compiling Code for SAW
  • Notes on C++ Analysis
• Direct Extraction
• Creating Symbolic Variables
• 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
  • Compositional Verification
  • Specifying Heap Layout
  • Specifying Heap Values
  • Working with Compound Types
  • Global variables
  • Preconditions and Postconditions
  • Assuming specifications
  • A Heap-Based Example
  • Verifying Cryptol FFI functions
• Extraction to the Coq theorem prover
  • Support Library
  • Cryptol module extraction
  • Proofs involving uninterpreted functions
  • Translation limitations and caveats
• Analyzing Hardware Circuits using Yosys
  • Processing VHDL With Yosys
  • Example: Ripple-Carry Adder
  • API Reference
• Bisimulation Prover
  • Bisimulation Example
  • Understanding the proof goals
  • Limitiations (note spelling error)

Recommended Structure and Per-Section Changes

• Overview

  • (new) SAW Use Cases. Discuss who is the intended audience for this manual. Introduce the types of equivalence checking or property exploration with which SAW can help.
  • (new) SAW Terminology. Introduce 8-12 most important SAW concepts (e.g., cryptol, sawscript, symbolic execution, term, goal, tactic, etc). Pick terminology that applies across llvm, jvm, mir. Include a link to the (new!) glossary section.
  • (new) Running example. Introduce a running example to reference throughout the manual. I suggest using a C and LLVM example.

• Structure of SAWScript

  • (new) parts of a SAW Script. Describe the common components of a SAW Script (e.g., load modules, set up symbolic execution, verify)
  • A first simple example (bring forward from its old location)
  • Syntax
  • Basic Types and Values
  • Basic Expression Forms
  • Other Basic Functions

• Invoking SAW. Move all of the old content for this section to appendix.repl reference. Replace it with a description (and running example) of how most users execute saw (e.g. saw script.saw). Note that windows users will need --no-color. Discuss basics of the SAW REPL and when you might use it (again, with running example). Refer users to appendix.command reference for more details.

• Cryptol and its Role in SAW

• Loading Code.

  • Loading LLVM
  • Loading Java
  • Loading MIR
  • Notes on Compiling Code for SAW
  • Direct Extraction (demoted from top-level)
  • Notes on C++ Analysis

• 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
  • Verifying Cryptol FFI functions

• Proofs about Terms

  • Automated Tactics
  • Proof Script Diagnostics
  • Rewriting in Proof Scripts
  • Other Transformations
  • Caching Solver Results
  • Other External Provers
  • Offline Provers
  • Finishing Proofs without External Solvers
  • Multiple Goals
  • Proof Failure and Satisfying Assignments
  • AIG Values and Proofs

• Transforming Term Values

  • Rewriting
  • Folding and Unfolding
  • Other Built-in Transformation and Inspection Functions
  • Loading and Storing Terms

• Extraction to the Coq theorem prover

  • Support Library
  • Cryptol module extraction
  • Proofs involving uninterpreted functions
  • Translation limitations and caveats

• Analyzing Hardware Circuits using Yosys

  • Processing VHDL With Yosys
  • Example: Ripple-Carry Adder
  • API Reference

• Bisimulation Prover

  • Bisimulation Example
  • Understanding the proof goals
  • Limitiations (note spelling error)

• (new) Appendices

  • (new) Glossary
    • Command
    • Controlled binding
    • Fold (and unfold)
    • Function
    • Goal
    • JVMTerm
    • JVMValue
    • Hypothesis
    • LLVMTerm
    • MIRTerm
    • MIRValue
    • Post Conditions
    • Pre Conditions
    • ProofResult
    • ReWrite Rule
    • SatResult
    • Simpset
    • SetupValue. (why isn't this LLVMValue?)
    • Symbolic Execution
    • Tactic
    • Term
    • Theorem
    • TopLevel
  • (new) Command Reference
    • admit
    • jvm_fresh_var
    • llvm_alloc
    • llvm_fresh_var
    • llvm_global
    • llvm_points_to_
    • llvm_verify
    • mir_fresh_var
    • ...
  • (new) Shell/REPL Reference
  • (deprecated item reference)
    • crucible*
      • ...

[sauclovian-g]

I have the following immediate thoughts:

• The yosys section should probably be moved up and go either in or after "Loading Code"; it's the same kind of topic. Also, the sections about proofs will want to (and probably already do) talk about hardware-related frobs, e.g. there's a heading "AIG Values and Proofs", and these should come after the introduction of the hardware bits.
• Bisimulation should be moved after Specification-Based Verification, since those are also the same kind of topic, and both are ways to generate terms to do proofs about.
• There should be a section about using the Python bindings and the remote API server. (That or there should be a section on the structure of the Python bindings right after the section on the structure of SAWScript, and intersperse discussions of the different control interfaces throughout the rest of the manual; this would probably be better but I don't think we're ready to write it just yet.)
• There should be a "SAWScript Language Reference" appendix with the saw-script language specification. This both makes it possible to look up language details without wading through expository text, and also creates a place to put exotica and details that don't belong in the expository text and otherwise have a way of hanging around awkwardly.
• There should also be a "SAW-Core Language Reference" appendix but I don't think we're in a position to be able to write it right now.

also:

• The SetupValue and JVMValue Types -> The SetupValue, MIRValue, and JVMValue Types

Also, the reference for the saw-script standard library (such as it is) belongs in the SAWScript reference, not the Command Reference -- we should restrict the latter to "real" operations that exist regardless of which control interface you're using.

[ChrisEPhifer]

Thanks for writing this up @smithdtyler! I was going to make an outline of the current manual until I saw you had already done so :)

I think that, long-term, we really need to get away from the gigantic one-page manual/tutorials and chop them up / re-organize with something like mdBook, which is used by many projects in the Rust community, or Sphinx, which would match some other Galois projects / the SAW verification intro.

Since I think we can do this reasonably quickly (especially with mdBook -- Sphinx would require porting all the Markdown formatting to reStructured Text), I'm planning to tackle this early in the new year, so we can then more easily address all the serious 'bugs', particularly in the manual.