Merge pull request #2170 from GaloisInc/fix/dead-doc-links

Fix the dead links in the tutorials

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.)

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: