add safety docs

In principle this can be checked by the
clippy::undocumented_unsafe_blocks lint, and I used the lint to find
the issues. In practice the lint is buggy and so cannot safely be
enabled in CI. Hopefully it will be fixed within a few stable version
releases; keep your eyes on
rust-lang/rust-clippy#8449 .

mm0-rs/components/mm0_util/src/lib.rs

@@ -30,6 +30,7 @@
   clippy::rc_buffer,
   clippy::rest_pat_in_fully_bound_structs,
   clippy::string_add,
+  clippy::undocumented_unsafe_blocks,
   clippy::unwrap_used
 )]
 // all the clippy lints we don't want
@@ -384,10 +385,11 @@ pub struct SliceUninit<T>(Box<[MaybeUninit<T>]>);
 
 impl<T> SliceUninit<T> {
   /// Create a new uninitialized slice of length `size`.
+  #[inline]
   #[must_use]
   pub fn new(size: usize) -> Self {
     let mut res = Vec::with_capacity(size);
-    // safety: the newly constructed elements have type MaybeUninit<T>
+    // Safety: the newly constructed elements have type MaybeUninit<T>
     // so it's fine to not initialize them
     unsafe { res.set_len(size) };
     Self(res.into_boxed_slice())
@@ -396,13 +398,15 @@ impl<T> SliceUninit<T> {
   /// Assign the value `val` to location `i` of the slice. Warning: this does not
   /// call the destructor for `T` on the previous value, so this should be used only
   /// once per location unless `T` has no `Drop` impl.
+  #[inline]
   pub fn set(&mut self, i: usize, val: T) { self.0[i] = MaybeUninit::new(val) }
 
   /// Finalizes the construction, returning an initialized `Box<[T]>`.
   ///
   /// # Safety
   ///
   /// This causes undefined behavior if the content is not fully initialized.
+  #[inline]
   #[must_use]
   pub unsafe fn assume_init(self) -> Box<[T]> { unsafe { mem::transmute(self.0) } }
 }

mm0-rs/components/mm0_util/src/lined_string.rs

@@ -70,16 +70,26 @@ impl LinedString {
     lines
   }
 
+  /// Returns the index of the start of the line, and the line number.
+  #[must_use]
+  pub fn get_line(&self, line: usize) -> Option<usize> { self.lines.get(line).copied() }
+
+  /// Returns the index of the start of the line, and the line number.
+  #[must_use]
+  pub fn line_start(&self, idx: usize) -> (usize, usize) {
+    match self.lines.binary_search(&idx) {
+      Ok(n) => (idx, n + 1),
+      Err(n) => (n.checked_sub(1).map_or(0, |i| self.lines[i]), n),
+    }
+  }
+
   /// Turn a byte index into an LSP [`Position`]
   ///
   /// # Safety
   /// `idx` must be a valid index in the string.
   #[must_use]
   pub fn to_pos(&self, idx: usize) -> Position {
-    let (pos, line) = match self.lines.binary_search(&idx) {
-      Ok(n) => (idx, n + 1),
-      Err(n) => (n.checked_sub(1).map_or(0, |i| self.lines[i]), n),
-    };
+    let (pos, line) = self.line_start(idx);
     Position {
       line: line.try_into().expect("too many lines"),
       character: if self.unicode {

mm0-rs/components/mm0b_parser/src/lib.rs

@@ -31,6 +31,7 @@
   clippy::rc_buffer,
   clippy::rest_pat_in_fully_bound_structs,
   clippy::string_add,
+  clippy::undocumented_unsafe_blocks,
   clippy::unwrap_used
 )]
 // all the clippy lints we don't want

mm0-rs/components/mm1_parser/src/lib.rs

@@ -34,6 +34,7 @@
   clippy::rc_buffer,
   clippy::rest_pat_in_fully_bound_structs,
   clippy::string_add,
+  clippy::undocumented_unsafe_blocks,
   clippy::unwrap_used,
   clippy::wrong_pub_self_convention
 )]

mm0-rs/components/mmcc/src/lib.rs

@@ -33,6 +33,7 @@
   clippy::rc_buffer,
   clippy::rest_pat_in_fully_bound_structs,
   clippy::string_add,
+  clippy::undocumented_unsafe_blocks,
   clippy::unwrap_used,
 )]
 // all the clippy lints we don't want

mm0-rs/src/compiler.rs

@@ -84,6 +84,10 @@ impl FileContents {
   pub(crate) fn new_bin_from_file(path: &std::path::Path) -> io::Result<Self> {
     #[cfg(not(target_arch = "wasm32"))] {
       let file = fs::File::open(path)?;
+      // Safety: Well, memory mapping files is never totally safe, but we're assuming
+      // some reasonableness assumptions on the part of the user here.
+      // If they delete the file from under us then interesting things will happen.
+      // (I blame linux for not having a sensible locking model.)
       Ok(Self::new_mmap(unsafe { memmap::MmapOptions::new().map(&file)? }))
     }
     #[cfg(target_arch = "wasm32")] {
@@ -223,23 +227,29 @@ impl ElabErrorKind {
 fn make_snippet<'a>(path: &'a FileRef, file: &'a LinedString, pos: Span,
     msg: &'a str, level: ErrorLevel, footer: Vec<Annotation<'a>>) -> Snippet<'a> {
   let annotation_type = level.to_annotation_type();
-  let Range {start, end} = file.to_range(pos);
-  let start2 = pos.start - start.character as usize;
+  let (start, start_line) = file.line_start(pos.start);
+  let (_, end_line) = file.line_start(pos.end);
   #[allow(clippy::or_fun_call)]
-  let end2 = file.to_idx(Position {line: end.line + 1, character: 0}).unwrap_or(file.len());
+  let end = file.to_idx(Position {
+    line: u32::try_from(end_line).expect("too many lines") + 1,
+    character: 0
+  }).unwrap_or(file.len());
   Snippet {
     title: Some(Annotation {
       id: None,
       label: Some(msg),
       annotation_type,
     }),
     slices: vec![Slice {
-      source: unsafe {std::str::from_utf8_unchecked(&file[(start2..end2).into()])},
-      line_start: start.line as usize + 1,
+      source: {
+        // Safety: We assume `Span` is coming from the correct file,
+        unsafe { std::str::from_utf8_unchecked(&file[(start..end).into()]) }
+      },
+      line_start: start_line + 1,
       origin: Some(path.rel()),
-      fold: end.line - start.line >= 5,
+      fold: end_line - start_line >= 5,
       annotations: vec![SourceAnnotation {
-        range: (pos.start - start2, pos.end - start2),
+        range: (pos.start - start, pos.end - start),
         label: "",
         annotation_type,
       }],

mm0-rs/src/doc/mod.rs

@@ -289,6 +289,7 @@ impl<'a> LayoutProof<'a> {
       ProofNode::Thm {thm, ref args, ref res} => {
         let td = &self.env.thms[thm];
         let mut hyps = SliceUninit::new(td.hyps.len());
+        assert!(td.args.len() + td.hyps.len() == args.len());
         if self.rev {
           for (i, e) in args[td.args.len()..].iter().enumerate().rev() {
             hyps.set(i, self.layout(e).into_proof())
@@ -299,7 +300,9 @@ impl<'a> LayoutProof<'a> {
           }
         }
         let res = self.layout(res).into_expr();
-        LayoutResult::Proof(self.push_line(unsafe {hyps.assume_init()}, LineKind::Thm(thm), res))
+        // Safety: We checked that the length matches, and we initialize
+        // every element exactly once in forward or reverse order.
+        LayoutResult::Proof(self.push_line(unsafe { hyps.assume_init() }, LineKind::Thm(thm), res))
       }
       ProofNode::Conv(ref p) => {
         let n = self.layout(&p.2).into_proof();
@@ -405,7 +408,10 @@ struct CaseInsensitiveName(ArcString);
 
 impl<'a> From<&'a ArcString> for &'a CaseInsensitiveName {
   #[allow(clippy::transmute_ptr_to_ptr)]
-  fn from(s: &'a ArcString) -> Self { unsafe { mem::transmute(s) } }
+  fn from(s: &'a ArcString) -> Self {
+    // Safety: CaseInsensitiveName is repr(transparent)
+    unsafe { mem::transmute(s) }
+  }
 }
 impl Hash for CaseInsensitiveName {
   fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
@@ -531,6 +537,9 @@ impl<'a, W: Write> BuildDoc<'a, W> {
   ) -> io::Result<std::path::PathBuf> {
     let mut path = self.thm_folder.clone();
     #[allow(clippy::useless_transmute)]
+    // Safety: This is a lifetime hack. We need to pass a mutable Environment to render_proof
+    // because LayoutProof::layout calls Environment::get_atom which mutates the env.data field.
+    // This is disjoint from the reference to env.thms that we retain here, so it's okay.
     let td: &Thm = unsafe { mem::transmute(&self.env.thms[tid]) };
     self.mangler.mangle(&self.env, tid, |_, s| path.push(&format!("{}.html", s)));
     let mut file = BufWriter::new(File::create(&path)?);
@@ -545,7 +554,9 @@ impl<'a, W: Write> BuildDoc<'a, W> {
           .expect("writing to a string"));
     }
     nav.push_str("<a href=\"../index.html#");
-    disambiguated_anchor(unsafe {nav.as_mut_vec()}, ad, true)?;
+    // Safety: disambiguated_anchor writes a theorem name,
+    // which is ASCII and so can safely be written to a String.
+    disambiguated_anchor(unsafe { nav.as_mut_vec() }, ad, true)?;
     nav.push_str("\">index</a>");
     if let Some(base) = &self.base_url {
       use std::fmt::Write;
@@ -579,6 +590,7 @@ impl<'a, W: Write> BuildDoc<'a, W> {
         \n        <tr class=\"proof-head\">\
                     <th>Step</th><th>Hyp</th><th>Ref</th><th>Expression</th>\
                   </tr>")?;
+      // double borrow here, see safety comment
       render_proof(self.source, &mut self.env, &mut self.mangler,
         &mut file, self.order, &td.args, &td.hyps, pf)?;
       writeln!(file, "      </tbody>\n    </table>")?;

mm0-rs/src/elab.rs

@@ -696,6 +696,7 @@ where F: FnMut(FileRef) -> Result<Receiver<ElabResult<T>>, BoxError> {
     impl<T> Future for ElabFuture<T> {
       type Output = (Option<ArcList<FileRef>>, Vec<T>, Vec<ElabError>, FrozenEnv);
       fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll<Self::Output> {
+        // Safety: We don't move `this` out of the pin
         let this = &mut unsafe { self.get_unchecked_mut() }.0;
         let ElabFutureInner {
           elab: FrozenElaborator(elab),
@@ -706,6 +707,8 @@ where F: FnMut(FileRef) -> Result<Receiver<ElabResult<T>>, BoxError> {
           match progress {
             UnfinishedStmt::None => {},
             UnfinishedStmt::Import(sp, p, other) => {
+              // Safety: `other` is pinned because it is projected from
+              // `this.progress` which is pinned
               match ready!(unsafe { Pin::new_unchecked(other) }.poll(cx)) {
                 Ok(ElabResult::Ok(t, errors, env)) => {
                   toks.push(t);

mm0-rs/src/elab/environment.rs

@@ -539,14 +539,16 @@ impl ObjectKind {
   /// Because this function calls [`FrozenLispVal::new`],
   /// the resulting object must not be examined before the elaborator is frozen.
   #[must_use] pub fn expr(e: LispVal) -> ObjectKind {
-    ObjectKind::Expr(unsafe {FrozenLispVal::new(e)})
+    // Safety: ObjectKind objects are write-only during the construction phase
+    ObjectKind::Expr(unsafe { FrozenLispVal::new(e) })
   }
   /// Create an [`ObjectKind`] for a [`Proof`].
   /// # Safety
   /// Because this function calls [`FrozenLispVal::new`],
   /// the resulting object must not be examined before the elaborator is frozen.
   #[must_use] pub fn proof(e: LispVal) -> ObjectKind {
-    ObjectKind::Proof(unsafe {FrozenLispVal::new(e)})
+    // Safety: ObjectKind objects are write-only during the construction phase
+    ObjectKind::Proof(unsafe { FrozenLispVal::new(e) })
   }
 }
 
@@ -678,6 +680,7 @@ impl<A: Remap, const N: usize> Remap for [A; N] {
   type Target = [A::Target; N];
   fn remap(&self, r: &mut Remapper) -> Self::Target {
     let arr = self.iter().map(|e| e.remap(r)).collect::<arrayvec::ArrayVec<_, N>>();
+    // Safety: We are collecting an iterator with exactly N elements, so it is initialized
     unsafe { arr.into_inner_unchecked() }
   }
 }