diff --git a/doc/rust-tutorial/rust-tutorial.md b/doc/rust-tutorial/rust-tutorial.md index 81d54fbb02..865e4ff602 100644 --- a/doc/rust-tutorial/rust-tutorial.md +++ b/doc/rust-tutorial/rust-tutorial.md @@ -1685,7 +1685,7 @@ so use it with caution. ## Static items Sometimes, Rust code makes use of [_static -items_](https://doc.rust-lang.org/std/intrinsics/fn.ctpop.html), which are +items_](https://doc.rust-lang.org/reference/items/static-items.html), which are definitions that are defined in a precise memory location for the entire duration of the program. As such, static items can be thought of as a form of global variables. @@ -1974,7 +1974,7 @@ transcribing an English-language specification to executable Cryptol code is interesting in its own right, but it is not the primary focus of this tutorial. As such, we will save you some time by providing a pre-baked Cryptol implementation of the Salsa20 spec -[here](https://github.com/GaloisInc/saw-script/tree/master/doc/rust-tutorial/code/salsa20/src/Salsa20.cry). +[here](https://github.com/GaloisInc/saw-script/blob/master/doc/rust-tutorial/code/salsa20/Salsa20.cry). (This implementation is [adapted](https://github.com/GaloisInc/cryptol-specs/blob/1366ccf71db9dca58b16ff04ca7d960a4fe20e34/Primitive/Symmetric/Cipher/Stream/Salsa20.cry) from the [`cryptol-specs`](https://github.com/GaloisInc/cryptol-specs) repo.) diff --git a/doc/tutorial/sawScriptTutorial.pdf b/doc/tutorial/sawScriptTutorial.pdf index bb5f420e58..263092dca4 100644 Binary files a/doc/tutorial/sawScriptTutorial.pdf and b/doc/tutorial/sawScriptTutorial.pdf differ diff --git a/doc/tutorial/tutorial.md b/doc/tutorial/tutorial.md index 62412f7ee2..801b4806f6 100644 --- a/doc/tutorial/tutorial.md +++ b/doc/tutorial/tutorial.md @@ -67,7 +67,7 @@ $include 19-26 code/ffs.c Another optimized version, in the following rather mysterious program (also in `ffs.c`), based on the `ffs` implementation in [musl -libc](http://www.musl-libc.org/). +libc](http://musl.libc.org/). ``` {.c} $include 69-76 code/ffs.c @@ -307,7 +307,7 @@ In addition to the `abc`, `z3`, and `yices` proof tactics used above, SAWScript can also invoke arbitrary external SAT solvers that read CNF files and produce results according to the SAT competition -[input and output conventions](http://www.satcompetition.org/2009/format-solvers2009.html), +[input and output conventions](https://jix.github.io/varisat/manual/0.2.0/formats/dimacs.html), using the `external_cnf_solver` tactic. For example, you can use [PicoSAT](http://fmv.jku.at/picosat/) to prove the theorem `thm` from the last example, with the following commands: