From 967bbfd78bbea5f7a7fbeff4b7ad0d576010fb80 Mon Sep 17 00:00:00 2001
From: Karl Ostmo <kostmo@gmail.com>
Date: Tue, 5 Sep 2023 23:50:45 -0700
Subject: [PATCH] docs elaboration

---
 src/Swarm/TUI/View.hs             |  4 ++++
 src/Swarm/Util/WindowedCounter.hs | 28 ++++++++++++++++++++++++----
 2 files changed, 28 insertions(+), 4 deletions(-)

diff --git a/src/Swarm/TUI/View.hs b/src/Swarm/TUI/View.hs
index f6d2913ee..66ac0d678 100644
--- a/src/Swarm/TUI/View.hs
+++ b/src/Swarm/TUI/View.hs
@@ -648,6 +648,10 @@ robotsListWidget s = hCenter table
       ]
 
     dutyCycleAttrIdx = floor $ dutyCycleRatio * fromIntegral (length meterAttributeNames - 1)
+    -- Since (!!) is partial, here is "proof" that it is safe:
+    -- * 'dutyCycleRatio' lies within the unit interval
+    -- * If 'dutyCycleRatio' is 1, then the maximum value of 'dutyCycleAttrIdx' is
+    --   one less than the length of 'meterAttributeNames' (i.e., a valid index).
     dutyCycleAttr = meterAttributeNames !! dutyCycleAttrIdx
     dutyCycleDisplay = withAttr dutyCycleAttr . str . flip (showFFloat (Just 1)) "%" $ dutyCyclePercentage
 
diff --git a/src/Swarm/Util/WindowedCounter.hs b/src/Swarm/Util/WindowedCounter.hs
index 5ecb36184..832ac56fe 100644
--- a/src/Swarm/Util/WindowedCounter.hs
+++ b/src/Swarm/Util/WindowedCounter.hs
@@ -73,7 +73,7 @@ data WindowedCounter a = WindowedCounter
   , _lastLargest :: Maybe a
   -- ^ NOTE: It is possible that '_lastLargest' may not exist in the 'Set'.
   , _nominalSpan :: Int
-  -- ^ Data retention window
+  -- ^ Data retention window. This value is guaranteed positive by the smart constructor.
   }
   deriving (Eq, Show)
 
@@ -92,19 +92,28 @@ instance FromJSON (WindowedCounter a) where
     s <- v .: "span"
     return $ mkWindow s
 
+-- | NOTE: We take the absolute value of the "window span" argument
+-- so that we can make guarantees about the output of 'getOccupancy'.
 mkWindow ::
-  -- | Window span
+  -- | window span
   Int ->
   WindowedCounter a
-mkWindow = WindowedCounter Set.empty Nothing
+mkWindow = WindowedCounter Set.empty Nothing . abs
 
 -- | Return the ratio of {members in the window} to the {integral span
 -- represented by the window}.
 --
--- The "current time" must be at least as large as the largest
+-- The "current time" should be at least as large as the largest
 -- element of the window.
 --
 -- A fully-contiguous collection of ticks would have an occupancy ratio of @1@.
+--
+-- == Unit interval guarantee
+-- The returned ratio is /guaranteed/ to lie on the unit interval, because:
+--
+-- * Both the numerator and denominator of the ratio are guaranteed positive, and
+-- * 'discardGarbage' guarantees that the set size is less than or equal to
+--   the nominal span.
 getOccupancy ::
   (Ord a, Offsettable a) =>
   -- | current time
@@ -142,8 +151,19 @@ insert x (WindowedCounter s lastLargest nominalSpan) =
 -- However, there may
 -- be opportunity to call this even more often, i.e. in code paths where the
 -- robot is visited but the condition for insertion is not met.
+--
+-- == Invariant
+-- If the largest member of the set is the current time,
+-- then after calling this function, the difference between smallest and largest
+-- value in the set is strictly less than the "nominal span", and the size of the
+-- set is less than or equal to the nominal span.
+--
+-- For example, if the nominal span is @3@, the current time is @7@, and the
+-- set entails a contiguous sequence @{2, 3, 4, 5, 6, 7}@, then the pivot for 'Set.split' will be
+-- @7 - 3 = 4@. The set becomes @{5, 6, 7}@, with cardinality equal to the nominal span.
 discardGarbage :: (Ord a, Offsettable a) => a -> WindowedCounter a -> WindowedCounter a
 discardGarbage currentTime (WindowedCounter s lastLargest nominalSpan) =
   WindowedCounter larger lastLargest nominalSpan
  where
+  -- NOTE: Neither output set of 'split' includes the "pivot" value.
   (_smaller, larger) = Set.split (offsetBy (negate nominalSpan) currentTime) s