Initial SAW Manual Reorganization

doc/conf.py

@@ -16,6 +16,7 @@
 
 myst_enable_extensions = [
     "amsmath",
+    "attrs_block",
     "colon_fence",
     "deflist",
     "dollarmath",

doc/saw-user-manual/appendices/command-reference.md

@@ -0,0 +1,5 @@
+# Command Reference
+
+:::{warning}
+This section is under construction!
+:::

doc/saw-user-manual/appendices/deprecated-items.md

@@ -0,0 +1,5 @@
+# Deprecated Items
+
+:::{warning}
+This section is under construction!
+:::

doc/saw-user-manual/appendices/glossary.md

@@ -0,0 +1,7 @@
+# Glossary
+
+:::{warning}
+This section is under construction!
+:::
+
+{.glossary}

doc/saw-user-manual/appendices/index.md

@@ -0,0 +1,11 @@
+# Appendices
+
+:::{toctree}
+:maxdepth: 1
+
+glossary
+command-reference
+repl-reference
+deprecated-items
+sawscript-language-reference/index
+:::

doc/saw-user-manual/appendices/repl-reference.md

@@ -0,0 +1,83 @@
+(repl-reference)=
+# REPL Reference
+
+The primary mechanism for interacting with SAW is through the `saw`
+executable included as part of the standard binary distribution. With no
+arguments, `saw` starts a read-evaluate-print loop (REPL) that allows
+the user to interactively evaluate commands in the SAWScript language.
+With one file name argument, it executes the specified file as a SAWScript
+program.
+
+In addition to a file name, the `saw` executable accepts several
+command-line options:
+
+`-h, -?, --help`
+: Print a help message.
+
+`-V, --version`
+: Show the version of the SAWScript interpreter.
+
+`-c path, --classpath=path`
+: Specify a colon-delimited list of paths to search for Java classes.
+
+`-i path, --import-path=path`
+: Specify a colon-delimited list of paths to search for imports.
+
+`-t, --extra-type-checking`
+: Perform extra type checking of intermediate values.
+
+`-I, --interactive`
+: Run interactively (with a REPL). This is the default if no other
+  arguments are specified.
+
+`-j path, --jars=path`
+: Specify a colon-delimited list of paths to `.jar` files to search
+  for Java classes.
+
+`-b path, --java-bin-dirs`
+: Specify a colon-delimited list of paths to search for a Java
+  executable.
+
+`-d num, --sim-verbose=num`
+: Set the verbosity level of the Java and LLVM simulators.
+
+`-v num, --verbose=num`
+: Set the verbosity level of the SAWScript interpreter.
+
+`--clean-mismatched-versions-solver-cache[=path]`
+: Run the `clean_mismatched_versions_solver_cache` command on the solver
+  cache at the given path, or if no path is given, the solver cache at the
+  value of the `SAW_SOLVER_CACHE_PATH` environment variable, then exit. See
+  the section **Caching Solver Results** for a description of the
+  `clean_mismatched_versions_solver_cache` command and the solver caching
+  feature in general.
+
+SAW also uses several environment variables for configuration:
+
+`CRYPTOLPATH`
+: Specify a colon-delimited list of directory paths to search for Cryptol
+  imports (including the Cryptol prelude).
+
+(path-definition)=
+`PATH`
+: If the `--java-bin-dirs` option is not set, then the `PATH` will be
+  searched to find a Java executable.
+
+`SAW_IMPORT_PATH`
+: Specify a colon-delimited list of directory paths to search for imports.
+
+`SAW_JDK_JAR`
+: Specify the path of the `.jar` file containing the core Java
+  libraries. Note that that is not necessary if the `--java-bin-dirs` option
+  or the `PATH` environment variable is used, as SAW can use this information
+  to determine the location of the core Java libraries' `.jar` file.
+
+(saw-solver-cache-path-definition)=
+`SAW_SOLVER_CACHE_PATH`
+: Specify a path at which to keep a cache of solver results obtained during
+  calls to certain tactics. A cache is not created at this path until it is
+  needed. See the section **Caching Solver Results** for more detail about this
+  feature.
+
+On Windows, semicolon-delimited lists are used instead of colon-delimited
+lists.

doc/saw-user-manual/appendices/sawscript-language-reference/index.md

@@ -0,0 +1,12 @@
+# SAWScript Language Reference
+
+:::{warning}
+This section is under construction!
+:::
+
+:::{toctree}
+:maxdepth: 2
+:caption: Contents
+
+
+:::

doc/saw-user-manual/creating-symbolic-variables.md

@@ -1,6 +1,6 @@
 # Creating Symbolic Variables
 
-The direct extraction process just discussed automatically introduces
+The direct extraction process discussed previously introduces
 symbolic variables and then abstracts over them, yielding a SAWScript
 `Term` that reflects the semantics of the original Java, LLVM, or MIR code.
 For simple functions, this is often the most convenient interface. For

doc/saw-user-manual/cryptol-and-its-role-in-saw.md

@@ -6,9 +6,10 @@ enough, however, to describe a wide variety of programs, and is
 particularly applicable to describing computations that operate on
 streams of data of some fixed size.
 
+<!-- N.b. Update the Cryptol repository to publish a canonical version of this. -->
 In addition to being integrated into SAW, Cryptol is a standalone
 language with [its own
-manual](http://cryptol.net/files/ProgrammingCryptol.pdf).
+manual](https://cdn.prod.website-files.com/673b407e535dbf3b547179dd/677c422f88a92701db5a834d_ProgrammingCryptol.pdf).
 
 SAW includes deep support for Cryptol, and in fact requires the use of
 Cryptol for most non-trivial tasks. To fully understand the rest of

doc/saw-user-manual/index.md

@@ -16,21 +16,21 @@ Thanks for helping to make SAW better for everyone!
 :maxdepth: 2
 :caption: Contents
 
-introduction
-invoking-saw
+overview
 structure-of-sawscript
-the-term-type
+invoking-saw
 cryptol-and-its-role-in-saw
-transforming-term-values
-proofs-about-terms
-symbolic-execution
-symbolic-termination
 loading-code
-direct-extraction
+analyzing-hardware-circuits-using-yosys
 creating-symbolic-variables
+symbolic-execution
+symbolic-termination
+the-term-type
 specification-based-verification
-extraction-to-the-coq-theorem-prover
-analyzing-hardware-circuits-using-yosys
 bisimulation-prover
+transforming-term-values
+proofs-about-terms
+extraction-to-the-coq-theorem-prover
 formal-deprecation-process
+appendices/index
 ```

doc/saw-user-manual/invoking-saw.md

@@ -1,96 +1,8 @@
 # Invoking SAW
 
-The primary mechanism for interacting with SAW is through the `saw`
-executable included as part of the standard binary distribution. With no
-arguments, `saw` starts a read-evaluate-print loop (REPL) that allows
-the user to interactively evaluate commands in the SAWScript language.
-With one file name argument, it executes the specified file as a SAWScript
-program.
+:::{warning}
+This section is under construction!
+:::
 
-In addition to a file name, the `saw` executable accepts several
-command-line options:
-
-`-h, -?, --help`
-
-  ~ Print a help message.
-
-`-V, --version`
-
-  ~ Show the version of the SAWScript interpreter.
-
-`-c path, --classpath=path`
-
-  ~ Specify a colon-delimited list of paths to search for Java classes.
-
-`-i path, --import-path=path`
-
-  ~ Specify a colon-delimited list of paths to search for imports.
-
-`-t, --extra-type-checking`
-
-  ~ Perform extra type checking of intermediate values.
-
-`-I, --interactive`
-
-  ~ Run interactively (with a REPL). This is the default if no other
-  arguments are specified.
-
-`-j path, --jars=path`
-
-  ~ Specify a colon-delimited list of paths to `.jar` files to search
-  for Java classes.
-
-`-b path, --java-bin-dirs`
-
-  ~ Specify a colon-delimited list of paths to search for a Java
-    executable.
-
-`-d num, --sim-verbose=num`
-
-  ~ Set the verbosity level of the Java and LLVM simulators.
-
-`-v num, --verbose=num`
-
-  ~ Set the verbosity level of the SAWScript interpreter.
-
-`--clean-mismatched-versions-solver-cache[=path]`
-
-  ~ Run the `clean_mismatched_versions_solver_cache` command on the solver
-  cache at the given path, or if no path is given, the solver cache at the
-  value of the `SAW_SOLVER_CACHE_PATH` environment variable, then exit. See
-  the section **Caching Solver Results** for a description of the
-  `clean_mismatched_versions_solver_cache` command and the solver caching
-  feature in general.
-
-SAW also uses several environment variables for configuration:
-
-`CRYPTOLPATH`
-
-  ~ Specify a colon-delimited list of directory paths to search for Cryptol
-  imports (including the Cryptol prelude).
-
-`PATH`
-
-  ~ If the `--java-bin-dirs` option is not set, then the `PATH` will be
-    searched to find a Java executable.
-
-`SAW_IMPORT_PATH`
-
-  ~ Specify a colon-delimited list of directory paths to search for imports.
-
-`SAW_JDK_JAR`
-
-  ~ Specify the path of the `.jar` file containing the core Java
-  libraries. Note that that is not necessary if the `--java-bin-dirs` option
-  or the `PATH` environment variable is used, as SAW can use this information
-  to determine the location of the core Java libraries' `.jar` file.
-
-`SAW_SOLVER_CACHE_PATH`
-
-  ~ Specify a path at which to keep a cache of solver results obtained during
-  calls to certain tactics. A cache is not created at this path until it is
-  needed. See the section **Caching Solver Results** for more detail about this
-  feature.
-
-On Windows, semicolon-delimited lists are used instead of colon-delimited
-lists.
+See [the REPL reference](./appendices/repl-reference) for additional details about
+the `saw` executable and its options.

doc/saw-user-manual/loading-code.md

@@ -28,7 +28,7 @@ control where to look for classes:
 - The `-b` flag takes the path where the `java` executable lives, which is used
   to locate the Java standard library classes and add them to the class
   database. Alternatively, one can put the directory where `java` lives on the
-  `PATH`, which SAW will search if `-b` is not set.
+ [`PATH`](path-definition), which SAW will search if `-b` is not set.
 
 - The `-j` flag takes the name of a JAR file as an argument and adds the
   contents of that file to the class database.
@@ -211,6 +211,43 @@ linking 11 mir files into <...>/example.linked-mir.json
 <snip>
 :::
 
+## Direct Extraction
+
+In many simple cases (such as the mathematical `max` function), the relevant
+inputs and outputs are immediately apparent. The function takes two integer
+arguments, always uses both of them, and returns a single integer value,
+making no other changes to the program state.
+
+In cases like this, a direct translation is possible, given only an
+identification of which code to execute. Two functions exist to handle
+such simple code. The first, for LLVM is the more stable of the two:
+
+- `llvm_extract : LLVMModule -> String -> TopLevel Term`
+
+A similar function exists for Java, but is more experimental.
+
+- `jvm_extract : JavaClass -> String -> TopLevel Term`
+
+Because of its lack of maturity, it (and later Java-related commands)
+must be enabled by running the `enable_experimental` command beforehand.
+
+- `enable_experimental : TopLevel ()`
+
+The structure of these two extraction functions is essentially
+identical. The first argument describes where to look for code (in
+either a Java class or an LLVM module, loaded as described in the
+previous section). The second argument is the name of the method or
+function to extract.
+
+When the extraction functions complete, they return a `Term`
+corresponding to the value returned by the function or method as a
+function of its arguments.
+
+These functions currently work only for code that takes some fixed
+number of integral parameters, returns an integral result, and does not
+access any dynamically-allocated memory (although temporary memory
+allocated during execution is allowed).
+
 ## Notes on C++ Analysis
 
 The distance between C++ code and LLVM is greater than between C and