{
  "environment": {
    "platform": "Linux-5.10.134-013.16.kangaroo.al8.x86_64-x86_64-with-glibc2.39",
    "python": "3.12.3"
  },
  "gates": {
    "assignment_requires_separate_recovery_evidence": true,
    "minority_cannot_commit_metadata_change": true,
    "resource_side_epoch_rejects_stale_executor": true
  },
  "model": "finite product-neutral control/data boundary model",
  "not_proved": [
    "the behavior of Kafka, Kubernetes, etcd, HBase, ZooKeeper, or HDFS",
    "service availability after control-quorum loss",
    "network, disk, crash-recovery, timing, or performance properties",
    "that one generic receipt or epoch scheme fits all three product families"
  ],
  "results": {
    "data-recovery": {
      "mutant_path": {
        "metadata_assignment_committed_without_data_gate": true,
        "missing_bytes_detected": true,
        "read_after_assignment": null
      },
      "safe_path": {
        "assignment_after_recovery_receipt": true,
        "assignment_before_recovery_receipt": false,
        "copy_installed": true,
        "read_after_assignment": "v1"
      }
    },
    "fencing": {
      "committed_assignment": {
        "epoch": 2,
        "item": "orders",
        "owner": "worker-b"
      },
      "with_resource_fence": {
        "accepted": [
          {
            "effect": "charge-new",
            "epoch": 2,
            "executor": "worker-b",
            "item": "orders"
          }
        ],
        "new_executor_accepted": true,
        "old_executor_accepted": false,
        "rejected": [
          {
            "effect": "charge-old",
            "epoch": 1,
            "executor": "worker-a",
            "item": "orders"
          }
        ],
        "resource_high_water": 2
      },
      "without_resource_fence": {
        "effects": [
          {
            "effect": "charge-old",
            "epoch": 1,
            "executor": "worker-a",
            "item": "orders"
          },
          {
            "effect": "charge-new",
            "epoch": 2,
            "executor": "worker-b",
            "item": "orders"
          }
        ],
        "new_executor_accepted": true,
        "old_executor_accepted": true
      }
    },
    "quorum-loss": {
      "alive_control_voters": [
        "c1"
      ],
      "data_nodes_still_holding_bytes": [
        "d1",
        "d2"
      ],
      "last_committed_assignment": {
        "epoch": 1,
        "item": "orders",
        "owner": "d1"
      },
      "metadata_change_committed": false,
      "quorum_required": 2,
      "reason": "byte survival and request serviceability are separate predicates",
      "service_availability_inferred": false
    }
  },
  "schema_version": 1
}