{
 "type": "excalidraw",
 "version": 2,
 "source": "https://excalidraw.com",
 "elements": [
  {
   "type": "rectangle",
   "id": "canvas_margin",
   "x": 10,
   "y": 10,
   "width": 1180,
   "height": 812.5,
   "angle": 0,
   "strokeColor": "transparent",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1367397668,
   "version": 1,
   "versionNonce": 1367397675,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null
  },
  {
   "type": "text",
   "id": "title",
   "x": 40,
   "y": 40,
   "width": 691.04,
   "height": 70.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 724990059,
   "version": 1,
   "versionNonce": 724990066,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "The new sequencer works ahead on S′ and keeps\nthe work only if the certificate agrees",
   "originalText": "The new sequencer works ahead on S′ and keeps\nthe work only if the certificate agrees",
   "fontSize": 28,
   "fontFamily": 5,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 25
  },
  {
   "type": "text",
   "id": "sub",
   "x": 40,
   "y": 120,
   "width": 840.8,
   "height": 20.0,
   "angle": 0,
   "strokeColor": "#565A6B",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1476559580,
   "version": 1,
   "versionNonce": 1476559587,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "The new home's primary vyrn-seq. The standby (F2) runs the same machine without client traffic.",
   "originalText": "The new home's primary vyrn-seq. The standby (F2) runs the same machine without client traffic.",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "rectangle",
   "id": "follower",
   "x": 40,
   "y": 230,
   "width": 160,
   "height": 60,
   "angle": 0,
   "strokeColor": "#565A6B",
   "backgroundColor": "#FFFFFF",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "dashed",
   "roughness": 1,
   "opacity": 100,
   "seed": 1117812038,
   "version": 1,
   "versionNonce": 1117812045,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "follower_t",
     "type": "text"
    },
    {
     "id": "a1",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "follower_t",
   "x": 61.986000000000004,
   "y": 248.75,
   "width": 116.02799999999999,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 100788144,
   "version": 1,
   "versionNonce": 100788151,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Follower(e)",
   "originalText": "Follower(e)",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "follower",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "prep",
   "x": 280,
   "y": 230,
   "width": 160,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F2D447",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1434529120,
   "version": 1,
   "versionNonce": 1434529127,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "prep_t",
     "type": "text"
    },
    {
     "id": "a1",
     "type": "arrow"
    },
    {
     "id": "a2",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "prep_t",
   "x": 312.534,
   "y": 248.75,
   "width": 94.932,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 196117522,
   "version": 1,
   "versionNonce": 196117529,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Preparing",
   "originalText": "Preparing",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "prep",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "collect",
   "x": 540,
   "y": 230,
   "width": 140,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F2D447",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 751881972,
   "version": 1,
   "versionNonce": 751881979,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "collect_t",
     "type": "text"
    },
    {
     "id": "a2",
     "type": "arrow"
    },
    {
     "id": "a3",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "collect_t",
   "x": 573.082,
   "y": 248.75,
   "width": 73.83599999999998,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 177421962,
   "version": 1,
   "versionNonce": 177421969,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Collect",
   "originalText": "Collect",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "collect",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "apply",
   "x": 920,
   "y": 230,
   "width": 170,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F2D447",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1174009887,
   "version": 1,
   "versionNonce": 1174009894,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "apply_t",
     "type": "text"
    },
    {
     "id": "a3",
     "type": "arrow"
    },
    {
     "id": "a4",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "apply_t",
   "x": 957.534,
   "y": 248.75,
   "width": 94.932,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 46570235,
   "version": 1,
   "versionNonce": 46570242,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Apply(S′)",
   "originalText": "Apply(S′)",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "apply",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a1",
   "x": 204,
   "y": 260,
   "width": 72,
   "height": 0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1826703395,
   "version": 1,
   "versionNonce": 1826703402,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     72,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "follower",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "prep",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l1",
   "x": 211.872,
   "y": 228,
   "width": 56.256,
   "height": 20.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1645847150,
   "version": 1,
   "versionNonce": 1645847157,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "T−60 s",
   "originalText": "T−60 s",
   "fontSize": 16,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "arrow",
   "id": "a2",
   "x": 444,
   "y": 260,
   "width": 92,
   "height": 0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 125628825,
   "version": 1,
   "versionNonce": 125628832,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     92,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "prep",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "collect",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l2",
   "x": 445.92,
   "y": 206,
   "width": 88.16,
   "height": 40.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1078355924,
   "version": 1,
   "versionNonce": 1078355931,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "T\n(own PTP)",
   "originalText": "T\n(own PTP)",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "arrow",
   "id": "a3",
   "x": 684,
   "y": 260,
   "width": 232,
   "height": 0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 196711695,
   "version": 1,
   "versionNonce": 196711702,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     232,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "collect",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "apply",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l3",
   "x": 736.8,
   "y": 206,
   "width": 126.39999999999999,
   "height": 40.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 927029058,
   "version": 1,
   "versionNonce": 927029065,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "replay reaches\nSeal step S′",
   "originalText": "replay reaches\nSeal step S′",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "text",
   "id": "prep_sub",
   "x": 296.8,
   "y": 300,
   "width": 126.39999999999999,
   "height": 40.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 658748903,
   "version": 1,
   "versionNonce": 658748910,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "derive keys\nwarm retention",
   "originalText": "derive keys\nwarm retention",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "text",
   "id": "col_sub",
   "x": 511.6,
   "y": 300,
   "width": 196.79999999999998,
   "height": 60.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1061836543,
   "version": 1,
   "versionNonce": 1061836550,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "lanes queue-ack,\nstream PacketRecords,\npropose window blocks",
   "originalText": "lanes queue-ack,\nstream PacketRecords,\npropose window blocks",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "text",
   "id": "app_sub",
   "x": 787.9200000000001,
   "y": 300,
   "width": 202.07999999999998,
   "height": 40.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1987064091,
   "version": 1,
   "versionNonce": 1987064098,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "lanes apply window ops\nagainst the state at S′",
   "originalText": "lanes apply window ops\nagainst the state at S′",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "right",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "text",
   "id": "app_sub2",
   "x": 738.48,
   "y": 344,
   "width": 251.51999999999998,
   "height": 20.0,
   "angle": 0,
   "strokeColor": "#565A6B",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 428897232,
   "version": 1,
   "versionNonce": 428897239,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "no response depends on it yet",
   "originalText": "no response depends on it yet",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "right",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "diamond",
   "id": "cert",
   "x": 885,
   "y": 420,
   "width": 240,
   "height": 120,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "#EDE5F6",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 212476011,
   "version": 1,
   "versionNonce": 212476018,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "cert_t",
     "type": "text"
    },
    {
     "id": "a4",
     "type": "arrow"
    },
    {
     "id": "a5",
     "type": "arrow"
    },
    {
     "id": "a6",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 2
   }
  },
  {
   "type": "text",
   "id": "cert_t",
   "x": 957.534,
   "y": 457.5,
   "width": 94.932,
   "height": 45.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 532669519,
   "version": 1,
   "versionNonce": 532669526,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "cert(e,S)\narrives",
   "originalText": "cert(e,S)\narrives",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "cert",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a4",
   "x": 1005,
   "y": 294,
   "width": 0,
   "height": 122,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 478919852,
   "version": 1,
   "versionNonce": 478919859,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     0,
     122
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "apply",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "cert",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "rectangle",
   "id": "close",
   "x": 40,
   "y": 630,
   "width": 170,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F2D447",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 318865860,
   "version": 1,
   "versionNonce": 318865867,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "close_t",
     "type": "text"
    },
    {
     "id": "b1",
     "type": "arrow"
    },
    {
     "id": "a5",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "close_t",
   "x": 62.81000000000001,
   "y": 648.75,
   "width": 124.37999999999998,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 515593404,
   "version": 1,
   "versionNonce": 515593411,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Close window",
   "originalText": "Close window",
   "fontSize": 18,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "close",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "unx",
   "x": 280,
   "y": 630,
   "width": 150,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#191B26",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 148622478,
   "version": 1,
   "versionNonce": 148622485,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "unx_t",
     "type": "text"
    },
    {
     "id": "b1",
     "type": "arrow"
    },
    {
     "id": "b2",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "unx_t",
   "x": 318.082,
   "y": 648.75,
   "width": 73.83599999999998,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#F2D447",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 474011076,
   "version": 1,
   "versionNonce": 474011083,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Uncross",
   "originalText": "Uncross",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "unx",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "catch",
   "x": 500,
   "y": 630,
   "width": 150,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F2D447",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1312155492,
   "version": 1,
   "versionNonce": 1312155499,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "catch_t",
     "type": "text"
    },
    {
     "id": "b2",
     "type": "arrow"
    },
    {
     "id": "b3",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "catch_t",
   "x": 533.24,
   "y": 648.75,
   "width": 83.52,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1990103357,
   "version": 1,
   "versionNonce": 1990103364,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "catch-up",
   "originalText": "catch-up",
   "fontSize": 18,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "catch",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "live",
   "x": 720,
   "y": 630,
   "width": 170,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F2D447",
   "fillStyle": "solid",
   "strokeWidth": 3,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1393503407,
   "version": 1,
   "versionNonce": 1393503414,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "live_t",
     "type": "text"
    },
    {
     "id": "b3",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "live_t",
   "x": 752.26,
   "y": 647.5,
   "width": 105.48,
   "height": 25.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 819296651,
   "version": 1,
   "versionNonce": 819296658,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Live(e+1)",
   "originalText": "Live(e+1)",
   "fontSize": 20,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "live",
   "autoResize": true,
   "baseline": 18
  },
  {
   "type": "arrow",
   "id": "b1",
   "x": 214,
   "y": 660,
   "width": 62,
   "height": 0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1204558816,
   "version": 1,
   "versionNonce": 1204558823,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     62,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "close",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "unx",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "arrow",
   "id": "b2",
   "x": 434,
   "y": 660,
   "width": 62,
   "height": 0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1737471578,
   "version": 1,
   "versionNonce": 1737471585,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     62,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "unx",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "catch",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "arrow",
   "id": "b3",
   "x": 654,
   "y": 660,
   "width": 62,
   "height": 0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 848094924,
   "version": 1,
   "versionNonce": 848094931,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     62,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "catch",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "live",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "arrow",
   "id": "a5",
   "x": 881,
   "y": 480,
   "width": 756,
   "height": 146,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1804373050,
   "version": 1,
   "versionNonce": 1804373057,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     -756,
     0
    ],
    [
     -756,
     146
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "cert",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "close",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l5",
   "x": 406.24,
   "y": 450,
   "width": 187.51999999999998,
   "height": 20.0,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1726832247,
   "version": 1,
   "versionNonce": 1726832254,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "S == S′, roots equal",
   "originalText": "S == S′, roots equal",
   "fontSize": 16,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "rectangle",
   "id": "undo",
   "x": 945,
   "y": 624,
   "width": 215,
   "height": 90,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#FFFFFF",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1815816178,
   "version": 1,
   "versionNonce": 1815816185,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "undo_t",
     "type": "text"
    },
    {
     "id": "a6",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "undo_t",
   "x": 967.86,
   "y": 639.0,
   "width": 169.28,
   "height": 60.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1370221578,
   "version": 1,
   "versionNonce": 1370221585,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Undo to the last\nfinal block, replay\nto S, Apply(S)",
   "originalText": "Undo to the last\nfinal block, replay\nto S, Apply(S)",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "undo",
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "arrow",
   "id": "a6",
   "x": 1005,
   "y": 544,
   "width": 35,
   "height": 76,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 68859264,
   "version": 1,
   "versionNonce": 68859271,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     35,
     76
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "cert",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "undo",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l6",
   "x": 1046,
   "y": 548,
   "width": 112.512,
   "height": 40.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1194042317,
   "version": 1,
   "versionNonce": 1194042324,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "S ≠ S′ or\nroot differs",
   "originalText": "S ≠ S′ or\nroot differs",
   "fontSize": 16,
   "fontFamily": 3,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "text",
   "id": "n_armed",
   "x": 140,
   "y": 746,
   "width": 372.59999999999997,
   "height": 45.0,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1422750430,
   "version": 1,
   "versionNonce": 1422750437,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "first auction fill waits for EpoArmed\nfrom Q members of R_{e+1}",
   "originalText": "first auction fill waits for EpoArmed\nfrom Q members of R_{e+1}",
   "fontSize": 18,
   "fontFamily": 5,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a_armed",
   "x": 300,
   "y": 742,
   "width": 52,
   "height": 46,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 978023991,
   "version": 1,
   "versionNonce": 978023998,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 2
   },
   "points": [
    [
     0,
     0
    ],
    [
     40,
     -20
    ],
    [
     52,
     -46
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": null,
   "endBinding": null,
   "elbowed": false
  },
  {
   "type": "text",
   "id": "n_respec",
   "x": 880,
   "y": 770,
   "width": 208.07999999999998,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 209114219,
   "version": 1,
   "versionNonce": 209114226,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "re-spec budget: 15 ms",
   "originalText": "re-spec budget: 15 ms",
   "fontSize": 18,
   "fontFamily": 5,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a_respec",
   "x": 1000,
   "y": 766,
   "width": 40,
   "height": 44,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1519155911,
   "version": 1,
   "versionNonce": 1519155918,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 2
   },
   "points": [
    [
     0,
     0
    ],
    [
     30,
     -20
    ],
    [
     40,
     -44
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": null,
   "endBinding": null,
   "elbowed": false
  }
 ],
 "appState": {
  "viewBackgroundColor": "#FFFFFF",
  "gridSize": 20
 },
 "files": {}
}