From 9b6dd51b85762dc50bf55873d69692c9d3666b21 Mon Sep 17 00:00:00 2001
From: Andrew Noyes <andrew@weaselab.dev>
Date: Fri, 9 Oct 2026 16:28:36 -0400
Subject: [PATCH] Add a spec for fixupMaxVersion

---
 ConflictSet.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/ConflictSet.cpp b/ConflictSet.cpp
index a02446f..e298ae3 100644
--- a/ConflictSet.cpp
+++ b/ConflictSet.cpp
@@ -2902,7 +2902,11 @@ horizontalMax16(InternalVersionT *vs, InternalVersionT) {
   return max;
 }
 
-// Precondition: `node->entryPresent`, and node is not the root
+/** @pre `node` is not the root, `node->entryPresent`, and `writeContext !=
+ * nullptr`.
+ * @post `maxVersion(node)` is the max of `writeContext->zero` and the max
+ * version of all logical keys starting with the search path of `node`.
+ */
 void fixupMaxVersion(Node *node, WriteContext *writeContext) {
   assert(node->parent);
   InternalVersionT max;