Add some missing documentation

For updr I made fewer things public and then didn't document the private
items (I don't understand the code well enough to add that documentation
in any case).

Signed-off-by: Tej Chajed <[email protected]>

inference/src/fixpoint.rs

@@ -51,12 +51,17 @@ fn invariant_cover(
     (covered, proof.invariants.len())
 }
 
+/// An inductive fixpoint
 pub struct FoundFixpoint {
+    /// The fixpoint term (the conjunction of these lemmas)
     pub proof: Vec<Term>,
+    /// Whether the discovered fixpoint implies the safety predicates
     pub safe: bool,
+    /// Total time for fixpoint calculation
     pub time_taken: Duration,
-    // How much of fixpoint covers handwritten invariant
+    /// Number of terms of handwritten invariant covered
     pub covered_handwritten: usize,
+    /// Total number of terms in the handwritten invariant
     pub size_handwritten: usize,
 }
 

inference/src/hashmap.rs

@@ -1,15 +1,20 @@
 // Copyright 2022-2023 VMware, Inc.
 // SPDX-License-Identifier: BSD-2-Clause
 
+//! Aliases for HashMap and HashSet with deterministic iteration order.
+
 use fxhash::FxBuildHasher;
 use std::hash::Hash;
 
+/// HashMap with deterministic iteration order
 pub type HashMap<K, V> = indexmap::IndexMap<K, V, FxBuildHasher>;
+/// HashSet with deterministic iteration order
 pub type HashSet<K> = indexmap::IndexSet<K, FxBuildHasher>;
 
 // pub type HashMap<K, V> = std::collections::HashMap<K, V>;
 // pub type HashSet<K> = std::collections::HashSet<K>;
 
+/// Construct a deterministic HashSet from a `std::collections::HashSet`.
 pub fn set_from_std<K: Eq + Hash>(s: std::collections::HashSet<K>) -> HashSet<K> {
     s.into_iter().collect()
 }

inference/src/lib.rs

@@ -6,13 +6,13 @@
 //! Mostly consists of an implementation of the "q-alpha" algorithm, but also
 //! provides an implementation of Houdini.
 
+#![allow(missing_docs)] // TODO: remove
 // configure clippy
 #![allow(clippy::needless_return)]
 #![allow(clippy::large_enum_variant)]
 #![allow(clippy::upper_case_acronyms)]
 #![allow(clippy::type_complexity)]
 // documentation-related lints (only checked when running rustdoc)
-// #![warn(missing_docs)]
 #![allow(rustdoc::private_intra_doc_links)]
 #![deny(rustdoc::broken_intra_doc_links)]
 

inference/src/updr.rs

@@ -1,6 +1,8 @@
 // Copyright 2022-2023 VMware, Inc.
 // SPDX-License-Identifier: BSD-2-Clause
 
+//! Implementation of UPDR. See https://www.tau.ac.il/~sharonshoham/papers/jacm17.pdf.
+
 use im::{hashset, HashSet};
 use itertools::Itertools;
 use std::sync::Arc;
@@ -12,31 +14,33 @@ use fly::term::cnf::term_to_cnf_clauses;
 use solver::conf::SolverConf;
 
 #[derive(Debug, Clone)]
-pub struct Frame {
+struct Frame {
     terms: Vec<Term>,
 }
 
 impl Frame {
-    pub fn strengthen(&mut self, term: Term) {
+    fn strengthen(&mut self, term: Term) {
         self.terms.push(term);
     }
 }
 
-pub struct BackwardsReachableState {
-    pub id: usize,
-    pub term_or_model: TermOrModel,
-    pub num_steps_to_bad: usize,
-    pub known_absent_until_frame: usize,
+struct BackwardsReachableState {
+    id: usize,
+    term_or_model: TermOrModel,
+    num_steps_to_bad: usize,
+    known_absent_until_frame: usize,
 }
 
+/// State for a UPDR invariant search
 pub struct Updr {
-    pub solver_conf: Arc<SolverConf>,
+    solver_conf: Arc<SolverConf>,
     frames: Vec<Frame>,
     backwards_reachable_states: Vec<BackwardsReachableState>,
     currently_blocking_id: Option<usize>,
 }
 
 impl Updr {
+    /// Initialize a UPDR search
     pub fn new(solver_conf: Arc<SolverConf>) -> Updr {
         Updr {
             solver_conf,
@@ -46,7 +50,7 @@ impl Updr {
         }
     }
 
-    pub fn find_state_to_block(&mut self, module: &FOModule) -> Option<usize> {
+    fn find_state_to_block(&mut self, module: &FOModule) -> Option<usize> {
         // println!("start");
         loop {
             // println!("loop");
@@ -323,7 +327,7 @@ impl Updr {
         out
     }
 
-    pub fn search(&mut self, m: &Module) -> Option<Frame> {
+    fn find_frame(&mut self, m: &Module) -> Option<Frame> {
         let module = FOModule::new(m, false, false, false);
         self.backwards_reachable_states = Vec::new();
         for safety in &module.safeties {
@@ -374,6 +378,12 @@ impl Updr {
         }
     }
 
+    /// Search for an inductive invariant.
+    pub fn search(&mut self, m: &Module) -> Option<Term> {
+        // TODO: is the and of the terms correct?
+        self.find_frame(m).map(|t| Term::and(t.terms))
+    }
+
     fn simplify(&mut self, module: &FOModule) {
         for frame in self.frames.iter_mut() {
             let mut terms: Vec<Term> = vec![];

temporal-verifier/src/command.rs

@@ -1,6 +1,8 @@
 // Copyright 2022-2023 VMware, Inc.
 // SPDX-License-Identifier: BSD-2-Clause
 
+//! The temporal-verifier binary's command-line interface.
+
 use codespan_reporting::diagnostic::{Diagnostic, Label};
 use path_slash::PathExt;
 use std::collections::HashMap;

temporal-verifier/src/lib.rs

@@ -6,13 +6,13 @@
 //! The API is currently primarily available for testing purposes and not really
 //! intended as a general-purpose library.
 
+#![deny(missing_docs)]
 // configure clippy
 #![allow(clippy::needless_return)]
 #![allow(clippy::large_enum_variant)]
 #![allow(clippy::upper_case_acronyms)]
 #![allow(clippy::type_complexity)]
 // documentation-related lints (only checked when running rustdoc)
-// #![warn(missing_docs)]
 #![allow(rustdoc::private_intra_doc_links)]
 #![deny(rustdoc::broken_intra_doc_links)]