add general documentation on the polonius module

this describes the rough algorithm using the localized constraint graph

compiler/rustc_borrowck/src/polonius/mod.rs

@@ -1,3 +1,38 @@
+//! Polonius analysis and support code:
+//! - dedicated constraints
+//! - conversion from NLL constraints
+//! - debugging utilities
+//! - etc.
+//!
+//! The current implementation models the flow-sensitive borrow-checking concerns as a graph
+//! containing both information about regions and information about the control flow.
+//!
+//! Loan propagation is seen as a reachability problem (with some subtleties) between where the loan
+//! is introduced and a given point.
+//!
+//! Constraints arising from type-checking allow loans to flow from region to region at the same CFG
+//! point. Constraints arising from liveness allow loans to flow within from point to point, between
+//! live regions at these points.
+//!
+//! Edges can be bidirectional to encode invariant relationships, and loans can flow "back in time"
+//! to traverse these constraints arising earlier in the CFG.
+//!
+//! When incorporating kills in the traversal, the loans reaching a given point are considered live.
+//!
+//! After this, the usual NLL process happens. These live loans are fed into a dataflow analysis
+//! combining them with the points where loans go out of NLL scope (the frontier where they stop
+//! propagating to a live region), to yield the "loans in scope" or "active loans", at a given
+//! point.
+//!
+//! Illegal accesses are still computed by checking whether one of these resulting loans is
+//! invalidated.
+//!
+//! More information on this simple approach can be found in the following links, and in the future
+//! in the rustc dev guide:
+//! - <https://smallcultfollowing.com/babysteps/blog/2023/09/22/polonius-part-1/>
+//! - <https://smallcultfollowing.com/babysteps/blog/2023/09/29/polonius-part-2/>
+//!
+
 mod constraints;
 pub(crate) use constraints::*;