{
 "type": "excalidraw",
 "version": 2,
 "source": "https://excalidraw.com",
 "elements": [
  {
   "type": "rectangle",
   "id": "canvas_margin",
   "x": 10,
   "y": 10,
   "width": 1177.512,
   "height": 730,
   "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": 599.76,
   "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": "Two roads to one fence: the Seal frame,\nor a forced seal after 5 ms",
   "originalText": "Two roads to one fence: the Seal frame,\nor a forced seal after 5 ms",
   "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": 841.12,
   "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": "Each old replica of R_e runs this machine. Both roads end at the same S, fenced by Q signatures.",
   "originalText": "Each old replica of R_e runs this machine. Both roads end at the same S, fenced by Q signatures.",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "rectangle",
   "id": "voting",
   "x": 40,
   "y": 190,
   "width": 150,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F4B7C2",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 230535765,
   "version": 1,
   "versionNonce": 230535772,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "voting_t",
     "type": "text"
    },
    {
     "id": "a1",
     "type": "arrow"
    },
    {
     "id": "a5",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "voting_t",
   "x": 67.53399999999999,
   "y": 208.75,
   "width": 94.932,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 321057970,
   "version": 1,
   "versionNonce": 321057977,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Voting(e)",
   "originalText": "Voting(e)",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "voting",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "wait",
   "x": 330,
   "y": 190,
   "width": 150,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F4B7C2",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 112783333,
   "version": 1,
   "versionNonce": 112783340,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "wait_t",
     "type": "text"
    },
    {
     "id": "a1",
     "type": "arrow"
    },
    {
     "id": "a2",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "wait_t",
   "x": 357.534,
   "y": 208.75,
   "width": 94.932,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 83147420,
   "version": 1,
   "versionNonce": 83147427,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "WaitFinal",
   "originalText": "WaitFinal",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "wait",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "replay",
   "x": 640,
   "y": 190,
   "width": 160,
   "height": 60,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F4B7C2",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1644323058,
   "version": 1,
   "versionNonce": 1644323065,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "replay_t",
     "type": "text"
    },
    {
     "id": "a2",
     "type": "arrow"
    },
    {
     "id": "a3",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "replay_t",
   "x": 663.48,
   "y": 208.75,
   "width": 113.03999999999999,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1083373132,
   "version": 1,
   "versionNonce": 1083373139,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Replay to S",
   "originalText": "Replay to S",
   "fontSize": 18,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "replay",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "rectangle",
   "id": "signed",
   "x": 955,
   "y": 190,
   "width": 150,
   "height": 60,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "#EDE5F6",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 515627203,
   "version": 1,
   "versionNonce": 515627210,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "signed_t",
     "type": "text"
    },
    {
     "id": "a3",
     "type": "arrow"
    },
    {
     "id": "a4",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "signed_t",
   "x": 998.356,
   "y": 208.75,
   "width": 63.288,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1129129617,
   "version": 1,
   "versionNonce": 1129129624,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Signed",
   "originalText": "Signed",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "signed",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a1",
   "x": 194,
   "y": 220,
   "width": 132,
   "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
    ],
    [
     132,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "voting",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "wait",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l1",
   "x": 214.0,
   "y": 192,
   "width": 92.0,
   "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": "Seal frame",
   "originalText": "Seal frame",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "arrow",
   "id": "a2",
   "x": 484,
   "y": 220,
   "width": 152,
   "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
    ],
    [
     152,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "wait",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "replay",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l2",
   "x": 515.36,
   "y": 172,
   "width": 89.28,
   "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": "block with\nS final",
   "originalText": "block with\nS final",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "arrow",
   "id": "a3",
   "x": 804,
   "y": 220,
   "width": 147,
   "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
    ],
    [
     147,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "replay",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "signed",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l3",
   "x": 833.36,
   "y": 192,
   "width": 89.28,
   "height": 20.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": "root ready",
   "originalText": "root ready",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "text",
   "id": "happy",
   "x": 560,
   "y": 274,
   "width": 412.544,
   "height": 40.0,
   "angle": 0,
   "strokeColor": "#565A6B",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1203236809,
   "version": 1,
   "versionNonce": 1203236816,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "at S: state_root + log_hash → HandoffRecord,\nsigned and sent as HandoffSig",
   "originalText": "at S: state_root + log_hash → HandoffRecord,\nsigned and sent as HandoffSig",
   "fontSize": 16,
   "fontFamily": 3,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "rectangle",
   "id": "fenced",
   "x": 930,
   "y": 440,
   "width": 200,
   "height": 64,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "#EDE5F6",
   "fillStyle": "solid",
   "strokeWidth": 3,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 253055539,
   "version": 1,
   "versionNonce": 253055546,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "fenced_t",
     "type": "text"
    },
    {
     "id": "a4",
     "type": "arrow"
    },
    {
     "id": "a6",
     "type": "arrow"
    },
    {
     "id": "a7",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "fenced_t",
   "x": 965.54,
   "y": 459.5,
   "width": 128.92,
   "height": 25.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1865017043,
   "version": 1,
   "versionNonce": 1865017050,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Fenced(e,S)",
   "originalText": "Fenced(e,S)",
   "fontSize": 20,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "fenced",
   "autoResize": true,
   "baseline": 18
  },
  {
   "type": "arrow",
   "id": "a4",
   "x": 1030,
   "y": 254,
   "width": 0,
   "height": 182,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "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,
     182
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "signed",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "fenced",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l4",
   "x": 1045,
   "y": 330,
   "width": 54.879999999999995,
   "height": 40.0,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 837824225,
   "version": 1,
   "versionNonce": 837824232,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "Q sigs\nseen",
   "originalText": "Q sigs\nseen",
   "fontSize": 16,
   "fontFamily": 5,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "rectangle",
   "id": "force",
   "x": 40,
   "y": 440,
   "width": 330,
   "height": 64,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "#F4B7C2",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 540208936,
   "version": 1,
   "versionNonce": 540208943,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": [
    {
     "id": "force_t",
     "type": "text"
    },
    {
     "id": "a5",
     "type": "arrow"
    },
    {
     "id": "a6",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "force_t",
   "x": 87.28000000000002,
   "y": 449.5,
   "width": 235.43999999999997,
   "height": 45.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 41815321,
   "version": 1,
   "versionNonce": 41815328,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "ForceSeal\n07 failover in seal mode",
   "originalText": "ForceSeal\n07 failover in seal mode",
   "fontSize": 18,
   "fontFamily": 5,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "force",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a5",
   "x": 115,
   "y": 254,
   "width": 0,
   "height": 182,
   "angle": 0,
   "strokeColor": "#191B26",
   "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
    ],
    [
     0,
     182
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "voting",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "force",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l5",
   "x": 132,
   "y": 290,
   "width": 281.28,
   "height": 40.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "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": "clock ≥ T + EPO_SEAL_GRACE_MS,\nno Seal frame",
   "originalText": "clock ≥ T + EPO_SEAL_GRACE_MS,\nno Seal frame",
   "fontSize": 16,
   "fontFamily": 3,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "arrow",
   "id": "a6",
   "x": 374,
   "y": 472,
   "width": 552,
   "height": 0,
   "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
    ],
    [
     552,
     0
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "force",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "fenced",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l6",
   "x": 489.856,
   "y": 444,
   "width": 356.28799999999995,
   "height": 20.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 := last step of the finalized prefix",
   "originalText": "S := last step of the finalized prefix",
   "fontSize": 16,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "text",
   "id": "force_sub",
   "x": 40,
   "y": 516,
   "width": 365.664,
   "height": 20.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1356029542,
   "version": 1,
   "versionNonce": 1356029549,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "sends EpoForceSeal{e, last_height_held}",
   "originalText": "sends EpoForceSeal{e, last_height_held}",
   "fontSize": 16,
   "fontFamily": 3,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "rectangle",
   "id": "follower",
   "x": 930,
   "y": 650,
   "width": 200,
   "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": "a7",
     "type": "arrow"
    }
   ],
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 3
   }
  },
  {
   "type": "text",
   "id": "follower_t",
   "x": 961.438,
   "y": 668.75,
   "width": 137.124,
   "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+1)",
   "originalText": "Follower(e+1)",
   "fontSize": 18,
   "fontFamily": 3,
   "textAlign": "center",
   "verticalAlign": "middle",
   "lineHeight": 1.25,
   "containerId": "follower",
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a7",
   "x": 1030,
   "y": 508,
   "width": 0,
   "height": 138,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 239950102,
   "version": 1,
   "versionNonce": 239950109,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "points": [
    [
     0,
     0
    ],
    [
     0,
     138
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": {
    "elementId": "fenced",
    "focus": 0,
    "gap": 4
   },
   "endBinding": {
    "elementId": "follower",
    "focus": 0,
    "gap": 4
   },
   "elbowed": false
  },
  {
   "type": "text",
   "id": "l7",
   "x": 1045,
   "y": 560,
   "width": 112.512,
   "height": 20.0,
   "angle": 0,
   "strokeColor": "#191B26",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 808227675,
   "version": 1,
   "versionNonce": 808227682,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "EpoActivated",
   "originalText": "EpoActivated",
   "fontSize": 16,
   "fontFamily": 3,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 14
  },
  {
   "type": "text",
   "id": "n_grace",
   "x": 230,
   "y": 372,
   "width": 113.75999999999999,
   "height": 22.5,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1795464458,
   "version": 1,
   "versionNonce": 1795464465,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "grace = 5 ms",
   "originalText": "grace = 5 ms",
   "fontSize": 18,
   "fontFamily": 5,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a_grace",
   "x": 340,
   "y": 380,
   "width": 52,
   "height": 46,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 639064547,
   "version": 1,
   "versionNonce": 639064554,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 2
   },
   "points": [
    [
     0,
     0
    ],
    [
     40,
     -18
    ],
    [
     52,
     -46
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": null,
   "endBinding": null,
   "elbowed": false
  },
  {
   "type": "text",
   "id": "n_fence",
   "x": 520,
   "y": 560,
   "width": 410.58,
   "height": 45.0,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 1,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 432081057,
   "version": 1,
   "versionNonce": 432081064,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": null,
   "text": "INV-FENCE: from Q valid HandoffSig on,\nreject every epoch-e frame above S",
   "originalText": "INV-FENCE: from Q valid HandoffSig on,\nreject every epoch-e frame above S",
   "fontSize": 18,
   "fontFamily": 5,
   "textAlign": "left",
   "verticalAlign": "top",
   "lineHeight": 1.25,
   "containerId": null,
   "autoResize": true,
   "baseline": 16
  },
  {
   "type": "arrow",
   "id": "a_fence",
   "x": 880,
   "y": 566,
   "width": 42,
   "height": 56,
   "angle": 0,
   "strokeColor": "#5A2D91",
   "backgroundColor": "transparent",
   "fillStyle": "solid",
   "strokeWidth": 2,
   "strokeStyle": "solid",
   "roughness": 1,
   "opacity": 100,
   "seed": 1723788360,
   "version": 1,
   "versionNonce": 1723788367,
   "isDeleted": false,
   "groupIds": [],
   "frameId": null,
   "boundElements": null,
   "link": null,
   "locked": false,
   "updated": 1,
   "roundness": {
    "type": 2
   },
   "points": [
    [
     0,
     0
    ],
    [
     25,
     -21
    ],
    [
     42,
     -56
    ]
   ],
   "lastCommittedPoint": null,
   "startArrowhead": null,
   "endArrowhead": "arrow",
   "startBinding": null,
   "endBinding": null,
   "elbowed": false
  }
 ],
 "appState": {
  "viewBackgroundColor": "#FFFFFF",
  "gridSize": 20
 },
 "files": {}
}