Implement granular Automerge sync with before state

disconcision · claude · disconcision · commit db0e2ec530cd · 2026-02-01T15:22:13.000-05:00
- Add 'before' field to EditorState message for granular CRDT ops
- Track changed_before in delta computation (PatchworkComm.re)
- Add SegmentValidator module for post-sync invariant checking
- Validate shards/children, segment shape, and UUID uniqueness

See docs/automerge-granular-sync.md for design rationale.

Co-Authored-By: Claude Opus 4.5 &lt;noreply@anthropic.com&gt;
diff --git a/embed/src/types/patchworkmessages.d.ts b/embed/src/types/patchworkmessages.d.ts
@@ -46,7 +46,8 @@ export interface Pong {
 /**
  * The main sync message - contains document state delta.
  *
- * - `state`: Changed/added pieces (partial HazelDoc with only affected pieces)
+ * - `state`: Changed/added pieces (partial HazelDoc with only affected pieces, after state)
+ * - `before`: Before state of changed pieces (for granular CRDT operations)
  * - `deleted`: IDs of pieces to remove from Automerge
  *
  * Why explicit deletion? Hazel uses a tree structure where deleted pieces
@@ -56,11 +57,19 @@ export interface Pong {
  * a piece, it's already in Automerge (unchanged), so it's not forwarded to
  * other clients, who then crash when the parent references a missing piece.
  *
+ * Why `before` state? To enable granular CRDT operations in tool.tsx.
+ * By comparing before/after for each piece, we can detect shard changes
+ * (which require atomic replacement) vs. content changes (which can use
+ * granular RGA operations on children arrays). The before state is used
+ * solely to compute what operations Hazel intended to perform.
+ *
  * See docs/patchwork-integration.md "Explicit Deletion Sync" for details.
+ * See docs/automerge-granular-sync.md for the granular sync design.
  */
 export interface EditorState {
   t: "state";
   state: HazelDoc;
+  before?: HazelDoc;
   deleted?: string[];
 }
 
diff --git a/src/haz3lcore/patchwork/PatchworkComm.re b/src/haz3lcore/patchwork/PatchworkComm.re
@@ -292,14 +292,11 @@ module JsConvert = {
     };
   };
 
-  let js_of_flatdoc =
-      (~deleted: list(Id.t)=[], map: FlatConvert.Doc.t): Ojs.t => {
-    // Create empty JS object for pieces map
+  /* Convert a flat doc to a JS HazelDoc object */
+  let hazeldoc_of_flatdoc = (map: FlatConvert.Doc.t): HazelDoc.t_0 => {
     let pieces_obj = Ojs.empty_obj();
     let pieces =
       FlatDoc.HazelDoc.AnonymousInterface2.Pieces4.t_of_js(pieces_obj);
-
-    // Add each piece to the map using UUID as key
     map
     |> Id.Map.iter((id, piece) => {
          let id_str = Id.to_string(id);
@@ -310,15 +307,37 @@ module JsConvert = {
            js_piece,
          );
        });
+    FlatDoc.HazelDoc.AnonymousInterface2.create(~title="", ~pieces, ());
+  };
 
-    let state =
-      FlatDoc.HazelDoc.AnonymousInterface2.create(~title="", ~pieces, ());
+  let js_of_flatdoc =
+      (
+        ~deleted: list(Id.t)=[],
+        ~before: option(FlatConvert.Doc.t)=?,
+        map: FlatConvert.Doc.t,
+      )
+      : Ojs.t => {
+    // Create JS HazelDoc for the after state
+    let state = hazeldoc_of_flatdoc(map);
 
     // Convert deleted IDs to string list for JS
     let deleted_strs = List.map(Id.to_string, deleted);
 
+    // Convert before state if provided
+    let before_js =
+      switch (before) {
+      | Some(before_doc) => Some(hazeldoc_of_flatdoc(before_doc))
+      | None => None
+      };
+
     EditorState.t_to_js(
-      EditorState.create(~t=`L_s8_state, ~state, ~deleted=deleted_strs, ()),
+      EditorState.create(
+        ~t=`L_s8_state,
+        ~state,
+        ~before=?before_js,
+        ~deleted=deleted_strs,
+        (),
+      ),
     );
   };
 
@@ -327,16 +346,23 @@ module JsConvert = {
      The deleted list is critical: Hazel's tree structure means deleted pieces
      simply disappear, but Automerge's flat map keeps pieces until explicitly
      removed. Without explicit deletion, deleted pieces become "orphans" in
-     Automerge, breaking undo/redo sync. See docs/patchwork-integration.md. */
+     Automerge, breaking undo/redo sync. See docs/patchwork-integration.md.
+
+     The changed_before field enables granular CRDT operations: by comparing
+     before/after for each changed piece, tool.tsx can detect shard changes
+     (requiring atomic replacement) vs. content changes (allowing granular
+     RGA ops). See docs/automerge-granular-sync.md. */
   type delta = {
     changed: Id.Map.t(FlatConvert.Flat.piece),
+    changed_before: Id.Map.t(FlatConvert.Flat.piece),
     added: Id.Map.t(FlatConvert.Flat.piece),
     deleted: list(Id.t),
   };
 
   let compute_delta =
       (old_doc: FlatConvert.Doc.t, new_doc: FlatConvert.Doc.t): delta => {
     let changed = ref(Id.Map.empty);
+    let changed_before = ref(Id.Map.empty);
     let added = ref(Id.Map.empty);
     let deleted = ref([]);
 
@@ -425,6 +451,7 @@ module JsConvert = {
            // Piece exists, check if changed using structural inequality
            if (old_piece != new_piece) {
              changed := Id.Map.add(id, new_piece, changed^);
+             changed_before := Id.Map.add(id, old_piece, changed_before^);
            };
          }
        });
@@ -440,6 +467,7 @@ module JsConvert = {
 
     {
       changed: changed^,
+      changed_before: changed_before^,
       added: added^,
       deleted: deleted^,
     };
@@ -796,10 +824,22 @@ let send_state =
   let affected_pieces =
     Id.Map.union((_, _, b) => Some(b), delta.changed, delta.added);
 
-  // Convert to JS with deleted IDs included
+  // Only include before state if there are changed pieces (not just added)
+  let before =
+    if (Id.Map.is_empty(delta.changed_before)) {
+      None;
+    } else {
+      Some(delta.changed_before);
+    };
+
+  // Convert to JS with deleted IDs and before state included
   let js_obj =
     PerfLog.measure("js_of_state", () =>
-      JsConvert.js_of_flatdoc(~deleted=delta.deleted, affected_pieces)
+      JsConvert.js_of_flatdoc(
+        ~deleted=delta.deleted,
+        ~before?,
+        affected_pieces,
+      )
     );
 
   // Measure payload size
diff --git a/src/haz3lcore/patchwork/PatchworkMessages.mli b/src/haz3lcore/patchwork/PatchworkMessages.mli
@@ -236,7 +236,9 @@ end
 
 (** The main sync message - contains document state delta.
 
-    - `state`: Changed/added pieces (partial HazelDoc with only affected pieces)
+    - `state`: Changed/added pieces (partial HazelDoc with only affected pieces,
+      after state)
+    - `before`: Before state of changed pieces (for granular CRDT operations)
     - `deleted`: IDs of pieces to remove from Automerge
 
     Why explicit deletion? Hazel uses a tree structure where deleted pieces
@@ -246,7 +248,14 @@ end
     piece, it's already in Automerge (unchanged), so it's not forwarded to other
     clients, who then crash when the parent references a missing piece.
 
-    See docs/patchwork-integration.md "Explicit Deletion Sync" for details. *)
+    Why `before` state? To enable granular CRDT operations in tool.tsx. By
+    comparing before/after for each piece, we can detect shard changes (which
+    require atomic replacement) vs. content changes (which can use granular RGA
+    operations on children arrays). The before state is used solely to compute
+    what operations Hazel intended to perform.
+
+    See docs/patchwork-integration.md "Explicit Deletion Sync" for details. See
+    docs/automerge-granular-sync.md for the granular sync design. *)
 module EditorState : sig
   type t = [ `EditorState ] intf
   [@@js.custom { of_js = Obj.magic; to_js = Obj.magic }]
@@ -279,12 +288,15 @@ module EditorState : sig
 
   val get_state : 'tags this -> HazelDoc.t_0 [@@js.get "state"]
   val set_state : 'tags this -> HazelDoc.t_0 -> unit [@@js.set "state"]
+  val get_before : 'tags this -> HazelDoc.t_0 option [@@js.get "before"]
+  val set_before : 'tags this -> HazelDoc.t_0 -> unit [@@js.set "before"]
   val get_deleted : 'tags this -> string list option [@@js.get "deleted"]
   val set_deleted : 'tags this -> string list -> unit [@@js.set "deleted"]
 
   val create :
     t:([ `L_s8_state [@js "state"] ][@js.enum]) ->
     state:HazelDoc.t_0 ->
+    ?before:HazelDoc.t_0 ->
     ?deleted:string list ->
     unit ->
     t
diff --git a/src/haz3lcore/patchwork/SegmentValidator.re b/src/haz3lcore/patchwork/SegmentValidator.re
@@ -0,0 +1,117 @@
+/* SegmentValidator.re - Validation predicates for sync invariants.
+
+   This module provides development-time checks to detect invariant violations
+   after sync operations. These checks are O(n) in segment size and should be
+   disabled in production builds.
+
+   See docs/automerge-granular-sync.md "Invariants and Validation Framework". */
+
+open Util;
+
+/* Check shards/children relationship for all tiles.
+   Invariant: length(shards) == length(children) + 1 */
+let validate_shards_children = (seg: Segment.t): list(string) => {
+  let errors = ref([]);
+  let rec check = (seg: Segment.t, path: string) => {
+    seg
+    |> List.iteri((i, p) =>
+         switch (p) {
+         | Piece.Tile(t) =>
+           let expected = List.length(t.children) + 1;
+           let actual = List.length(t.shards);
+           if (actual != expected && actual > 0) {
+             errors :=
+               [
+                 path
+                 ++ "/tile"
+                 ++ string_of_int(i)
+                 ++ ": shards="
+                 ++ string_of_int(actual)
+                 ++ " but children="
+                 ++ string_of_int(List.length(t.children)),
+                 ...errors^,
+               ];
+           };
+           t.children
+           |> List.iteri((j, child) =>
+                check(
+                  child,
+                  path
+                  ++ "/tile"
+                  ++ string_of_int(i)
+                  ++ "/child"
+                  ++ string_of_int(j),
+                )
+              );
+         | _ => ()
+         }
+       );
+  };
+  check(seg, "root");
+  errors^;
+};
+
+/* Check segment shape consistency via skeleton generation.
+   Invariant: Segment.skel(seg) doesn't throw Skel.Nonconvex_segment */
+let validate_shape = (seg: Segment.t): list(string) => {
+  let errors = ref([]);
+  let rec check = (seg: Segment.t, path: string) => {
+    switch (Segment.skel(seg)) {
+    | exception Skel.Nonconvex_segment =>
+      errors := [path ++ ": Nonconvex segment (shape conflict)", ...errors^]
+    | exception Skel.Input_contains_secondary => () /* Shouldn't happen - skel filters secondary */
+    | _ => ()
+    };
+    /* Recursively check tile children */
+    seg
+    |> List.iter(p =>
+         switch (p) {
+         | Piece.Tile(t) =>
+           t.children
+           |> List.iteri((j, child) =>
+                check(child, path ++ "/child" ++ string_of_int(j))
+              )
+         | _ => ()
+         }
+       );
+  };
+  check(seg, "root");
+  errors^;
+};
+
+/* Check UUID uniqueness across segment.
+   Invariant: All piece IDs are unique across the entire edit state */
+let validate_unique_ids = (seg: Segment.t): list(string) => {
+  let ids = Segment.ids(seg);
+  let unique_ids = List.sort_uniq(Id.compare, ids);
+  if (List.length(ids) != List.length(unique_ids)) {
+    ["Duplicate piece IDs detected in segment"];
+  } else {
+    [];
+  };
+};
+
+/* Run all validations, log any errors.
+   Call this after sync operations to detect invariant violations.
+   Disable in production for performance. */
+let validate_all = (seg: Segment.t): unit => {
+  let errors =
+    validate_shards_children(seg)
+    @ validate_shape(seg)
+    @ validate_unique_ids(seg);
+  errors
+  |> List.iter(e =>
+       Js_of_ocaml.Firebug.console##warn(
+         Js_of_ocaml.Js.string("[SYNC VALIDATION] " ++ e),
+       )
+     );
+};
+
+/* Validate and return whether any errors were found */
+let has_errors = (seg: Segment.t): bool => {
+  let errors =
+    validate_shards_children(seg)
+    @ validate_shape(seg)
+    @ validate_unique_ids(seg);
+  List.length(errors) > 0;
+};
diff --git a/src/haz3lcore/patchwork/SyncReplace.re b/src/haz3lcore/patchwork/SyncReplace.re
@@ -361,6 +361,10 @@ let sync_replace = (z: Zipper.t, delta_doc: FlatConvert.Doc.t): Zipper.t => {
       FlatConvert.doc_to_seg(merged_doc)
     );
 
+  // Validate invariants after sync - disable in production for performance
+  // This helps detect any CRDT merge issues that violate Hazel's invariants
+  SegmentValidator.validate_all(new_seg);
+
   //let num_pieces = PerfLog.Count.pieces_in_segment_deep(new_seg);
   let num_pieces = (-1);
   let context = string_of_int(num_pieces) ++ " pieces";
