Comments

collect/src/main/kotlin/com/certora/collect/AbstractKeySet.kt

@@ -1,7 +1,28 @@
 package com.certora.collect
 
+/**
+    Presents the keys of a [TreapMap] as a [TreapSet].
+
+    The idea here is that a `TreapMap<K, *>` is stored with the same Treap structure as a `TreapSet<K>`, so we can very
+    quickly create the corresponding `TreapSet<K>` when needed, in O(1) time.
+
+    We lazily initialize the set, so that we don't create it until we need it.  For many operations, we can avoid
+    creating the set entirely, and just use the map directly.  However, many operations, e.g. [addAll]/[union] and
+    [retainAll/intersect], are much more efficient when we have a [TreapSet], so we create it when needed.
+
+    Note: It would be really nice if we could just treat the [TreapMap] objects themselves as [TreapSet] objects, but
+    this presents some problems.  The most fundamental problem is that the [TreapMap] and [TreapSet] interfaces have
+    methods that are not compatible; for example, they both implement [Iterable], but with different element types.
+ */
 internal abstract class AbstractKeySet<@Treapable K, S : TreapSet<K>> : TreapSet<K> {
+    /**
+        The map whose keys we are presenting as a set.  We prefer to use the map directly when possible, so we don't
+        need to create the set.
+     */
     abstract val map: AbstractTreapMap<K, *, *>
+    /**
+        The set of keys.  This is a lazy property so that we don't create the set until we need it.
+     */
     abstract val keys: Lazy<S>
 
     @Suppress("Treapability")