Add a spec for fixupMaxVersion

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;