Skip to content

Commit 87c71f0

Browse files
committed
Fix Mathematical Foundation section in TECHNICAL_DOCUMENTATION.md
- Add removeFromList definition with all 4 prev/next cases - Expand moveToEnd formula and document 'only node' edge case - Fix TTL validity invariant to handle expiry=0 when ttl=0
1 parent d125a12 commit 87c71f0

1 file changed

Lines changed: 10 additions & 2 deletions

File tree

docs/TECHNICAL_DOCUMENTATION.md

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -217,6 +217,12 @@ $$\begin{align}
217217
delete(k) &= \begin{cases}
218218
removeFromList(H[k]) \land H \setminus \{k\} \land size \leftarrow size - 1 & \text{if } k \in H \\
219219
\text{no-op} & \text{otherwise}
220+
\end{cases} \\
221+
removeFromList(item) &= \begin{cases}
222+
item.prev.next \leftarrow item.next \land item.next.prev \leftarrow item.prev \land first \leftarrow item.next \land last \leftarrow item.prev & \text{if } item.prev \neq null \land item.next \neq null \\
223+
item.prev.next \leftarrow item.next \land first \leftarrow item.next \land last \leftarrow null & \text{if } item.prev \neq null \land item.next = null \\
224+
item.next.prev \leftarrow item.prev \land first \leftarrow item.next \land last \leftarrow null & \text{if } item.prev = null \land item.next \neq null \\
225+
first \leftarrow null \land last \leftarrow null & \text{if } item.prev = null \land item.next = null
220226
\end{cases}
221227
\end{align}$$
222228

@@ -226,10 +232,12 @@ removeFromList(H[k]) \land H \setminus \{k\} \land size \leftarrow size - 1 & \t
226232
$$\begin{align}
227233
moveToEnd(item) &= \begin{cases}
228234
\text{no-op} & \text{if } item = last \\
229-
removeFromList(item) \land appendToList(item) & \text{otherwise}
235+
item.prev.next \leftarrow item.next \land item.next.prev \leftarrow item.prev \land first \leftarrow item.next \land item.prev \leftarrow last \land last.next \leftarrow item \land last \leftarrow item \land first \leftarrow item \lor first & \text{if } item \neq last
230236
\end{cases}
231237
\end{align}$$
232238

239+
**Edge Case:** When item is the only node in the list ($item.prev = null \land item.next = null$), the condition $item = last$ is true since $first = last = item$, so the operation is a no-op.
240+
233241
**Time Complexity:** $O(1)$
234242

235243
### Eviction Policy
@@ -272,7 +280,7 @@ delete(k) & \text{if } isExpired(k) \\
272280
2. **List Consistency:** $first \neq null \iff last \neq null \iff size > 0$
273281
3. **Hash Consistency:** $|H| = size$
274282
4. **LRU Order:** Items in list are ordered from least to most recently used
275-
5. **TTL Validity:** $ttl = 0 \lor \forall k \in H: H[k].expiry > t_{now}$
283+
5. **TTL Validity:** $(ttl = 0 \Rightarrow \forall k \in H: H[k].expiry = 0) \land (ttl > 0 \Rightarrow \forall k \in H: H[k].expiry > t_{now})$
276284
6. **TTL Reset Invariant:** TTL is only reset during `set()` operations when `bypass = false`, never during `get()` or `setWithEvicted()` operations
277285

278286
## TypeScript Support

0 commit comments

Comments
 (0)