feat(spec): Blocksync witnesses and invariants (#594)

* startin with witnesses and invariants * more invariants * feat(code): Start consensus at `H+1` where `H` is the height of the latest committed block (#587) * feat(code): Start consensus at `H+1` where `H` is the height of the latest committed block * Update spawn.bash * chore(code/part_stream): Deduplicate received proposal parts by sequence number (#584) * chore(code/part_stream): Use random `StreamId` (#583) * chore(code/part_stream): Use random StreamId to ensure a stream is not re-used when a node crashes and restarts quickly * Start with random StreamId and increment from there * spec/quint: some renaming and comments * spec/quint: undoing new line changes * spec/quint: witness renamed, comments added * spec/quint: invariant renamed, comments adapted * spec/quint: invariant renamed, comments adapted * more invariants * spec/quint: re-tabbing blocksync.qnt * spec/quint: fix comments, types, identation --------- Co-authored-by: Romain Ruetschi <[email protected]> Co-authored-by: Daniel Cason <[email protected]>
informalsystems · Nov 22, 2024 · 710924f · 710924f
1 parent 12b51e4
commit 710924f
Show file tree

Hide file tree

Showing 6 changed files with 315 additions and 169 deletions.
diff --git a/specs/quint/specs/blocksync/blocksync.qnt b/specs/quint/specs/blocksync/blocksync.qnt
@@ -6,89 +6,104 @@
 
 module blocksync {
 
-	import types.* from "../types"
-	export types.*
-
-	type Option[a] =
-	    | Some(a)
-	    | None
-
-	type StatusMsg = {
-	    peer: Address,
-	    base: Height,
-	    top: Height
-	}
-
-	type BlockRange = {
-	    base: Height,
-	    top: Height
-	}
-
-	type ReqType =
-	    | SyncCertificate
-	    | SyncBlock
-	    | SyncBlockStoreEntry
-
-	type RequestMsg = {
-	    client: Address,
-	    server: Address,
-	    rtype: ReqType,
-	    height: Height
-	}
-
-	pure def emptyReqMsg = {
-	    client: "",
-	    server: "",
-	    rtype: SyncCertificate,
-	    height: -1
-	}
-
-	type Response =
-	    | RespBlock(Proposal)
-	    | RespCertificate(Set[Vote])
-	    | RespBlockStoreEntry(BlockStoreEntry)
-
-	type ResponseMsg = {
-	    client: Address,
-	    server: Address,
-	    height: Height,
-	    response: Response,
-	}
-
-	pure def emptyResponseMsg = {
-	    client: "",
-	    server: "",
-	    height: -1,
-	    response: RespBlock(emptyProposal),
-	}
-
-	// *************
-	// State machine
-	// *************
-
-	// Messages exchanged by nodes (clients and servers)
-	var statusBuffer : Address -> Set[StatusMsg]
-	var requestsBuffer : Address -> Set[RequestMsg]
-	var responsesBuffer : Address -> Set[ResponseMsg]
-
-	// Auxiliary functions for sending messages
-
-	pure def broadcastStatusMsg(buffer: Address -> Set[StatusMsg], sm: StatusMsg): Address -> Set[StatusMsg] =
-	    buffer.keys().mapBy(x => { ...buffer.get(x).union(Set(sm)) })
-
-	// put the response message in the buffer of the client
-	pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] =
-	    buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) })
-
-	action initBsync(nodes) = all {
-	    statusBuffer' = nodes.mapBy(v => Set()),
-	    requestsBuffer' = nodes.mapBy(v => Set()),
-	    responsesBuffer' = nodes.mapBy (v => Set()),
-	}
-
-	action unchangedBsync = all {
-	    statusBuffer' = statusBuffer,
-	    requestsBuffer' = requestsBuffer,
-	    responsesBuffer' = responsesBuffer,
-	}
+  import types.* from "../types"
+  export types.*
+
+  type Option[a] =
+    | Some(a)
+    | None
+
+  type StatusMsg = {
+    peer: Address,
+    base: Height,
+    top: Height
+  }
+
+  type BlockRange = {
+    base: Height,
+    top: Height
+  }
+
+  type ReqType =
+    | SyncCertificate
+    | SyncBlock
+    | SyncBlockStoreEntry
+
+  type RequestMsg = {
+    client: Address,
+    server: Address,
+    rtype: ReqType,
+    height: Height
+  }
+
+  pure def emptyReqMsg = {
+    client: "",
+    server: "",
+    rtype: SyncCertificate,
+    height: -1
+  }
+
+  type Response =
+    | RespBlock(Proposal)
+    | RespCertificate(Set[Vote])
+    | RespBlockStoreEntry(BlockStoreEntry)
+
+  type ResponseMsg = {
+    client: Address,
+    server: Address,
+    height: Height,
+    response: Response,
+  }
+
+  pure def matchingMessages(req: RequestMsg, resp: ResponseMsg): bool =
+    and {
+      req.client == resp.client,
+      req.server == resp.server,
+      req.height == resp.height,
+    }
+
+
+  pure val emptyResponseMsg = {
+    client: "",
+    server: "",
+    height: -1,
+    response: RespBlock(emptyProposal),
+  }
+
+  // *************
+  // State machine
+  // *************
+
+  /// Messages exchanged by nodes (clients and servers)
+  var statusBuffer : Address -> Set[StatusMsg]
+  var requestsBuffer : Address -> Set[RequestMsg]
+  var responsesBuffer : Address -> Set[ResponseMsg]
+
+  // Auxiliary functions for sending messages
+
+  /// Put the status message in the buffer of every client.
+  pure def broadcastStatusMsg(buffer: Address -> Set[StatusMsg], sm: StatusMsg): Address -> Set[StatusMsg] =
+    buffer.keys().mapBy(x =>
+      if (x == sm.peer) // don't send to yourself
+        buffer.get(x)
+      else
+        { ...buffer.get(x).union(Set(sm)) }
+    )
+
+  /// Put the response message in the buffer of the requesting client.
+  pure def sendResponse(buffer: Address -> Set[ResponseMsg], m: ResponseMsg): Address -> Set[ResponseMsg] =
+    buffer.put(m.client, { ...buffer.get(m.client).union(Set(m)) })
+
+  action initBsync(nodes) = all {
+    statusBuffer' = nodes.mapBy(v => Set()),
+    requestsBuffer' = nodes.mapBy(v => Set()),
+    responsesBuffer' = nodes.mapBy (v => Set()),
+  }
+
+  action unchangedBsync = all {
+    statusBuffer' = statusBuffer,
+    requestsBuffer' = requestsBuffer,
+    responsesBuffer' = responsesBuffer,
+  }
+
 }