diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/bracha-broadcast-from-cb.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/bracha-broadcast-from-cb.png new file mode 100644 index 0000000..21b2453 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/bracha-broadcast-from-cb.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/bracha-broadcast.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/bracha-broadcast.png new file mode 100644 index 0000000..148dcb5 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/bracha-broadcast.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/buses.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/buses.png new file mode 100644 index 0000000..1ec31e3 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/buses.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cb.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cb.png new file mode 100644 index 0000000..586c012 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cb.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cover-image.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cover-image.png new file mode 100644 index 0000000..ee1baee Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cover-image.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-alt.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-alt.png new file mode 100644 index 0000000..3acce04 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-alt.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-unspec-ctrl-abbrev.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-unspec-ctrl-abbrev.png new file mode 100644 index 0000000..2c1a82e Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-unspec-ctrl-abbrev.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-unspec-ctrl.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-unspec-ctrl.png new file mode 100644 index 0000000..e3a3324 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap-unspec-ctrl.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap.png new file mode 100644 index 0000000..a7d122d Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/cswap.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/def-abbrev.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/def-abbrev.png new file mode 100644 index 0000000..c2b050d Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/def-abbrev.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/def.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/def.png new file mode 100644 index 0000000..78bb217 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/def.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/delay-alt.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/delay-alt.png new file mode 100644 index 0000000..14e078c Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/delay-alt.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/delay.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/delay.png new file mode 100644 index 0000000..a16d7b5 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/delay.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/gossip.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/gossip.png new file mode 100644 index 0000000..4cce79d Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/gossip.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/index.mdx b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/index.mdx new file mode 100644 index 0000000..05958c5 --- /dev/null +++ b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/index.mdx @@ -0,0 +1,372 @@ +--- +title: A Sketch of Reversible Deterministic Concurrency for Distributed Protocols +description: A post sharing first result of elaborating the idea of reversible deterministic concurrency +authors: sergefdrv +toc_max_heading_level: 4 +image: "./cover-image.png" +tags: ["technical", "long", "notes"] +--- + +import styles from './styles.css'; + +This post presents preliminary results of elaborating the idea that was [introduced on project's GitHub](https://github.com/orgs/replica-io/discussions/49#discussioncomment-12436415) and which can be referred to as _reversible deterministic concurrency_. We try to make those ideas a little more concrete and apply them to modelling some well-known distributed protocols. + + + + +Designing, verifying, correctly implementing and later improving core mechanisms of complex distributed, decentralized systems, such as Byzantine fault tolerant consensus, is notoriously difficult and error-prone. One of the biggest challenges here is dealing with the inherently concurrent nature of distributed systems. So there is an underlying problem of structuring the inherently concurrent logic of distributed protocols that we don’t really know how to solve in a simple, flexible, and reliable way. Embarrassingly often, we approach this rather awkwardly and unsurprisingly end up with awfully complicated, obscure, and fragile code. + +[Considering what modelling approach to initially adopt in the Replica_IO framework](https://github.com/replica-io/replica-io/issues/47), an approach that would allow _both specifying and implementing_ complex distributed protocols in a _natural_ way, I decided to challenge the status quo and try to rethink the conventional approaches to modeling distributed systems and the ways of expressing distributed protocols. So came up the idea of reversible deterministic concurrency. The idea was inspired by a number of [explored models of computation and programming models](https://github.com/replica-io/replica-io/issues/7), as well as some principles from information theory, modern physics, reversible and quantum computing, such as conservation of information. + +The long-term goal is to develop this idea further into an approach for _specifying_ core mechanisms of concurrent, distributed systems, _implementing_ them in Rust code, as well as _verifying_ their correctness. The approach will be used as the foundation for the Replica_IO framework. Following this approach, it should be safe and easy to express concurrency and communication within the framework in a structured and composable way. + +In order to get some intuition about the idea, we'll begin by discussing some basic principles behind it. Then we'll try modelling some well-known distributed protocols following those principles, namely the Bracha's reliable broadcast and the Tendermint consensus protocols. + +Please bear in mind that this write-up is an early sketch and that many details of the approach presented here, including terminology, will likely undergo significant changes in the future. + +## Approach + +We conceptually think of concurrent systems as consisting of _deterministic_ components that can be connected with each other and interact _concurrently_. The only means of interaction with the components are through their _inputs_ and _outputs_. Each input and output can convey a certain type of data, and they are typed accordingly. Inputs and outputs matching in type can be connected _pairwise_, so that data can flow through the connection. Connecting inputs and outputs of different components enables data flow between those components. + +### Base and composite components, extrinsic inputs and outputs + +Components can be _composite_, i.e. consist of lower-level sub-components connected together. The remaining unconnected inputs and outputs become the inputs and outputs of the composite component. The process of decomposition bottoms out at _base components_ that are considered primitive and not decomposed further. Apart from base components, there can be _extrinsic inputs and outputs_ for exchanging information with the environment. The extrinsic inputs and outputs can represent interfaces for interacting with entities that are considered external to the modeled system, or they can be _sources_ of auxiliary data items and _sinks_ to dispose of excessive data. + +### Input-output pairs, interaction lines, and two kinds of interaction + +Inputs and outputs can only appear in complementary pairs. This applies to inputs and outputs of base components, and therefore of composite components, as well as to extrinsic inputs and outputs. Moreover, in a complete system, every input must be connected to exactly one output matching in type. So the input-output pairs connected one to another form a kind of chains or _interaction lines_. Data items flowing along different interaction lines can interact with each other by redistributing the information contained within those data items when they arrive at the same base component. So there are _two kinds of interaction_ within the system: passing data items from one component to another along interaction lines and exchange of information between data items on different interaction lines within base components. + +### Determinism and reversibility + +All components are conceptually _deterministic_: provided all the component's assumptions hold true, the output values must be completely determined by the input values and nothing else. Although the availability of output values can depend both on the availability of the input values and on the input values themselves, neither the output values nor their availability may per se depend on the relative order in which the input values become available. (It is worth noting here that this determinism is only conceptual: later we'll see how some input values may be left unspecified and, in normal operation, get chosen on spot, possibly depending on the availability and values of other inputs.) Moreover, the components must also be _reversible_, so that the original input values can always be recovered from the resulting output values. + +One can view the determinism and reversibility requirements as a consequence of making all information flow within the system explicit. If all information that is used to determine the output values is contained in the input values then the inputs uniquely determine the outputs and the computation is deterministic. Similarly, if the output values collectively contain all the information that was contained in the original input values then the inputs can be recovered from the outputs and the computation is reversible. Determinism and reversibility are dual to each other: if a computation carried out in one direction is reversible then the same computation carried out in the opposite direction is deterministic. + +Requiring that components are conceptually deterministic we make non-determinism explicit, structurally evident rather than emergent or accidental, while treating concurrency implicitly as emerging naturally from data availability and the system’s structure rather than from control flow. This should improve modularity and facilitate _compositional reasoning_. Together with the reversibility requirement this ensures that there is no hidden data flow, enables backward reasoning, backtracking mechanisms, _reverse debugging_ and would facilitate _management of resources_, such as memory. + +### Simple components + +#### Sum + +We can represent components graphically. For example, the following figure depicts a component that simply adds one integer value to another: + +![](sum.png) + +The component is represented by a rectangle divided into horizontal sections, one section for each input-output pair, i.e. interaction line. The component is labeled above by its name, `Sum`; its interaction lines are labeled as `x: Int` and `y: Int` , where `x` and `y` denote the names of the interaction lines and `Int` is the type of data items conveyed by them. The inputs are on the left side of the component whereas the outputs are on the right side. The component takes two integers as input values, denoted as `a` and `b`, along lines `x` and `y` and returns two integers as output values; the first input value goes through unchanged, whereas the second one becomes the sum of the two input values. The first input is required to determine both outputs, and the second input is required to determine the second output. Since this component has just two interaction lines, one of which leaves the value unchanged, we can alternatively depict it as follows: + +![](sum-alt.png) + +It is easy to see that this component is deterministic, i.e. the output values are completely determined by the input values, no matter in which order the inputs become available. It is also not hard to see that this component is reversible, i.e. the original input values can always be recovered from the resulting output values. We can depict the inverse of the component as follows: + +![](sum-inv.png) + +#### Generalized controlled swap + +Let's consider another example. The following component represents a kind of generalized controlled swap operation[^fredkin-gate]: + +![](cswap.png) + +or depicted alternatively: + +![](cswap-alt.png) + +[^fredkin-gate]: Controlled swap of individual bits is known as [Fredkin gate](https://en.wikipedia.org/wiki/Fredkin_gate) in [reversible](https://en.wikipedia.org/wiki/Reversible_computing) and [quantum](https://en.wikipedia.org/wiki/Quantum_computing) computing; here we generalize it to operate on target values of arbitrary type. + +It has three interaction lines: one control line, `c`, and two target lines, `t1` and `t2`. The value of the control line goes through unchanged, but it determines the output values of the target lines: If the control value is true then the values of the target lines get swapped, otherwise they simply go through unchanged. The controlled swap component is an inverse of itself. + +### Concurrency of interaction lines + +Interaction lines are highly _concurrent_: an output value becomes available as soon as it can be obtained from the input values that are available for the interaction. For example, in the `CSwap` component, once the value on the control line is available, each of the target outputs remains dependent only on one of the target inputs and becomes available as soon as that input value is available, concurrently and independently of each other. + +### Demand-driven nature of interactions + +Interactions are _demand-driven_: certain extrinsic inputs and some inputs of base components may demand a value from the connected output, and this demand propagates further along the inputs required to determine the demanded output value until it eventually reaches available values and triggers the interactions required to satisfy the demand. Sinks are never demanding, but they will consume the value when it becomes available. + +### Unspecified values + +Certain inputs of base components may be connected to special sources of _unspecified_ values. Those unspecified values are not real; they are just placeholders that stand for concrete values. During normal operation, the component will choose appropriate concrete values for such unspecified values and act as if they were guessed correctly and provided by the environment. When debugging the system or during verification, the sources of unspecified values can be forced to provide specific values; in that case, the component has no choice but to take the forced value as is. One can think of an unspecified value as a "superposition" of all possible values of the corresponding type that will "collapse" to a concrete value when going through the base component. + +#### The `Def` component + +The following component is meant to be used with such sources of unspecified values: + +![](def.png) + +Both interaction lines of this component conceptually go through unchanged; however, if the value of the second input is unspecified, as denoted in the picture by the special source labeled with `?`, then the component chooses it to be equal to the value of the first input. This is effectively a way to copy the value of the first input in normal operation, but the second line can be forced to an arbitrary value, e.g. to model a Byzantine failure during verification. To avoid cluttering, we will often abbreviate the `Def` component in diagrams as follows: + +![](def-abbrev.png) + +#### `CSwap` with unspecified control + +The control line of the controlled swap component can also be left unspecified, e.g. as follows: + +![](cswap-unspec-ctrl.png) + +or in an abbreviated form: + +![](cswap-unspec-ctrl-abbrev.png) + +In the diagram above, the control line is connected to a source of unspecified values, and the second target output is connected to a sink (which is never demanding). When there is a demand for the first target output value, `w`, both of the target inputs will be demanded, and the demand for `w` will be satisfied by taking either `u` or `v`, whichever becomes available earlier, and the value of the control line will be chosen accordingly. If both target inputs are available when the target output is demanded then the value of the control line is chosen to be false, i.e. the component is biased towards passing the values of target lines through without swapping them. + +### Synchronization + +In some cases, we need to make sure that a certain value only becomes available if some other value also becomes available, without changing the values themselves. This can be achieved with the following synchronization primitive: + +![](sync.png) + +Values `u` and `v` go through the bar unchanged, but only once they both become available. Thus values `u` and `v` on the right side mean something more than those on the left side: a value becoming available on any line on the right side implies the existence and availability of some value on the other line as well. + +### Signals + +For similar reasons, it may also be useful to have a kind of _signalling_ interaction lines of unit type, which convey data items that can take only a single possible value. Such signal values themselves have no meaning other than their existence, i.e. availability. Signalling lines work naturally with synchronization bars: + +![](sync-with-signal-line.png) + +or in an abbreviated form: + +![](sync-with-signal-line-abbrev.png) + +In the diagram above, values `u` and `v` go through unchanged, but `v` becomes available on the right side only when `u` becomes available. However, because there are separate synchronization bars and an additional signal line, the availability of `v` has no effect on the availability of `u`. + +### Delays and timers + +In order to represent time-dependent behavior of the system, we introduce the _delay_ component: + +![](delay.png) + +or alternatively: + +![](delay-alt.png) + +Values `d` and `v` go through the delay component unchanged, but, in normal operation, value `v` becomes available on the second output with a delay of at least time duration `d`. + +Using the delay component, we can construct a timer component that passes an arbitrary value through the `trigger` line, and then, after a given amount of time provided on the `duration` line, lets a unit value to pass through the `signal` line (which would normally be connected to a source of an immediately available unit value): + +![](timer.png) + +### One-shot and composite lines + +Individual inputs and outputs, and therefore interaction lines composed thereof, are conceptually _one-shot_, i.e. they can convey only a single data item. However, we can bundle multiple inputs/outputs together and thus construct _composite inputs/outputs and interaction lines_. There is _no synchronization_ imposed by composing interaction lines together, i.e. each individual line remains _concurrent in composition_. + +We can compose two interaction lines together and decompose them back by constructing and deconstructing a pair, graphically represented as follows: + +![](pair.png) + +We can also uniformly bundle an arbitrary number of lines together as follows: + +![](mux.png) + +In the diagram above, the source labeled with the bang symbol `!` denotes an empty source. (With just two lines being multiplexed uniformly, the notation above appears the same as the one for constructing a pure pair; in such cases, the ambiguity will be resolved by the context.) + +Using this notation, we can also bundle a virtually indefinite number of lines together: + +![](mux-inf.png) + +Note that the line composition primitives are not components: there is neither interaction nor synchronization between individual interaction lines caused by the composition; this is just notational convenience for dealing with multiple interaction lines. + +### Transposition + +It may be useful to rearrange the elements within a composition. We can transpose the last two levels of a composition as follows: + +![](transpose.png) + +The transposer connects line $x_{i,j}$ from composite line $x^{mn}$ on the left to line $y_{j,i}$ of composite line $y^{nm}$ on the right. For example, it will rearrange + +``` +[ [u, v, w], [x, y, z] ] +``` + +into + +``` +[ [u, x], [v, y], [w, z] ] +``` + +### The `Select` component + +Using composite interaction lines we can define a component representing a choice from an arbitrary number of options: + +![](select.png) + +In the `Select` component, the first input, `choice`, determines the value of which element from the second, composite input, `options`, should become available on the third output, `chosen`. The `chosen` input is supposed to be connected to a source of unspecified values. The `choice` input can also be left unspecified; in that case, the component chooses it to select the element of `options` that becomes available earlier. + +### Uncluttering diagrams + +To unclutter diagrams, we may depict several connections in one stroke and omit sources of unspecified values and sinks like this: + +![](buses.png) + +### Repetitive patterns + +#### Replication box + +We would often need to connect one or many components in a repetitive pattern. To represent such patterns in a diagram, we can depict a single instance of the repeating part of the diagram enclosed in a _replication box_: + +![](replication-box.png) + +In the diagram above, component `G` enclosed in a replication box is virtually repeated for each element of the composite lines entering and exiting the replication box. + +#### Recursive loops + +We can use the replication box to represent recursive patterns of connections as follows: + +![](recursion.png) + +### Domains and projections + +Each interaction line belongs to a certain _domain_, which characterizes its location. For example, we can define a separate domain for each node of a distributed system. Interaction lines cannot cross domain boundaries, but _some components may span multiple domains_ and thus enable _cross-domain interaction_. + +We can then derive a _projection_ of a system model onto a subset of its domains. Connections with base components that span the projection boundary will be represented as extrinsic inputs and outputs. So we can project a model of the whole distributed system separately onto each node and derive the local logic of individual nodes. The base components that represent means of communication between nodes, which are necessarily cross-domain, will be replaced by extrinsic inputs and outputs standing for gateways to the networking layer. + +### Assume-guarantee reasoning and modelling of faults + +The behavior of individual components could be specified in terms of the assumptions about their inputs and the guarantees about their outputs. This would enable _assume-guarantee reasoning_ about correctness of the system and _compositional verification_. In the context of distributed systems, benign node faults can be modeled by suppressing some extrinsic sources belonging to the corresponding domains, whereas Byzantine faults can be modeled by forcing some of the extrinsic sources with arbitrary values ("garbage in — garbage out"). + +### Confining interaction lines + +The total number of interaction lines in complex components can quickly become too large. Therefore, components should only expose a subset of input-output pairs that is enough to guarantee determinism and reversibility under the component's assumptions, _confining_ the remaining interaction lines by connecting them to sources and sinks inside the component. For example, in distributed protocols, the exact set of votes forming a valid quorum for certain decisions of the protocol logic often does not affect the outcomes, given the assumptions about the maximal fraction of faulty nodes hold true; so the corresponding interaction lines can be confined within a component representing the protocol. + +## Modelling Distributed Protocols + +### Bracha's Reliable Broadcast + +Now we'll try to apply the approach to modelling a relatively simple distributed protocol, namely Bracha's broadcast[^bracha-broadcast]. Bracha's broadcast is a foundational distributed protocol implementing a Byzantine fault-tolerant reliable broadcast mechanism in the asynchronous model. The protocol allows one party to broadcast a message such that all correct parties eventually deliver the message and agree on the delivered message, given that less than a third of the parties may be corrupt. The protocol adopts the asynchronous model, i.e. it makes no timing assumptions but requires that every message sent by a correct process is eventually received. + +[^bracha-broadcast]: To learn about Bracha's broadcast in detail, please refer to the [original paper](https://ecommons.cornell.edu/bitstream/handle/1813/6430/84-590.pdf), where it was introduced as a key building block of an asynchronous consensus protocol. The following post may also be helpful: [Living with Asynchrony: Bracha's Reliable Broadcast](https://decentralizedthoughts.github.io/2020-09-19-living-with-asynchrony-brachas-reliable-broadcast/), as well as [these lecture notes](https://dcl.epfl.ch/site/_media/education/sdc_byzconsensus.pdf). + +For the sake of simplicity, we will model a one-shot version of the protocol that only allows broadcasting a single value from a designated sender party. The protocol can be expressed in traditional event-oriented pseudo-code as follows: + +``` +upon broadcast(m): // only sender + send message to all + +upon receiving a message from the sender: + send message to all + +upon receiving n-f messages and not having sent a READY message: + send message to all + +upon receiving f+1 messages and not having sent a READY message: + send message to all + +upon receiving n-f messages : + deliver(m) +``` + +#### Peer-to-peer links + +We will start by modelling communication between individual nodes in the system. Each party in the protocol is represented by a node, and each node is modeled as a separate domain. For the nodes to communicate, those domains need to be able to interact through some kind of cross-domain component. So we define the following component for that purpose: + +![](link.png) + +The `Link` component allows sending an authenticated value from one node to another. If the `rcv` input is left unspecified, as supposed, the component chooses the value from the `snd` input as the value of the `rcv` output. The `snd` line belongs to the message sender's domain, whereas the `rcv` line belongs to the destination node's domain. If we treat `Link` as a composite component, we can model it as shown on the right side of the diagram above, where the internal interaction line in the middle belongs to a separate domain and represents the communication medium. + +#### Weak broadcast + +Although the underlying communication mechanism is point-to-point message exchange, if we look closer, the basic communication pattern used in the reliable broadcast protocol is sending the same message to all nodes. Let's refer to this pattern as weak broadcast and represent it as the following component: + +![](wb.png) + +The `bc` line belongs to the sending node's domain, whereas the elements of the composite `dlvr` line belong to the corresponding receiving nodes' domains. We can model a corrupt sender committing the failure of message equivocation (sending different messages to some receivers) by forcing some of the sources in its domain with arbitrary values. The component is mainly composed of `Link` and `Def` components replicated for each receiving node. The `Def` components are meant to create an individual copy of the `bc` value for each instance of `Link`. Note the recursive pattern, used together with the replication box, that forms a kind of forward loop in order to thread the value from the `bc` input through the replicated components. + +#### Quorums + +Another kind of component that we will need is for collecting quorums of values received from peer nodes: + +![](rb-quorums.png) + +The `WeakQuroum` and `StrongQuorum` components are identical except the number of votes required to reach the quorum: `f+1` and `n-f`, respectively. `WeakQuorum` ensures that there is at least one vote from a correct node, whereas `StrongQuorum` ensures that any two of such quorums must intersect in at least one correct node. Moreover, `StrongQuorum` ensures that any of its quorums contains at least as many votes from correct nodes as the total number of votes required by `WeakQuorum`. The `votes` line represents the values received from peer nodes, whereas the `value` line represents the value supported by a sufficient quorum of votes. If the `value` input is left unspecified then the component will choose the value corresponding to the earliest quorum of votes becoming available; if the `value` input is forced then the component will make the complementary output available only once a quorum becomes available on the `votes` input. + +#### Overall protocol model + +Now we can model the Bracha's reliable broadcast protocol as a cross-domain component with an interface identical to `WB` but providing the guarantees of reliable broadcast: + +![](bracha-broadcast.png) + +In this diagram, we omit sources of unspecified values and sinks. We also omit types, but indicate the dimentionality of composite lines. We label the instances of the `WB` component with names: `send`, `echo`, and `ready`, indicating the kind of protocol message being communicated through those components. + +The `send` component is used to send a value from the designated sender node to all nodes, whereas the `echo` and `ready` components are replicated for each node and represent all-to-all communication. Note that the composite `dlvr` outputs of the `WB` components replicated for each node sending `ECHO` and `READY` messages go through transposers outside of replication boxes. Remember that individual lines of the `dlvr` output belong to the corresponding receiving nodes' domains, but we need to connect the `votes` inputs of the quorum components so that they all belong to the same node's domain. The trasnposers rearrange the composite lines to achieve that. + +The `Select` component, replicated for each node, represents a choice between two alternative causes for sending a `READY` message: either upon receiving a strong quorum of `ECHO` messages or upon receiving a weak quorum of `READY` message from other nodes. + +#### Consistent broadcast and modularized protocol model + +We should recognize that a part of this reliable broadcast protocol actually represents a consistent broadcast protocol. Consistent broadcast guarantees that receivers agree on the delivered values, but it does not guarantee that all correct receivers eventually deliver the value even if some correct receivers deliver. We can represent this sub-protocol as a cross-domain component: + +![](cb.png) + +and then restructure the reliable broadcast protocol as follows: + +![](bracha-broadcast-from-cb.png) + +### Tendermint Consensus + +Now we'll try to apply the approach to a more complicated protocol and sketch a model of the Tendermint consensus protocol[^tendermint]. Tendermint is a Byzantine fault-tolerant sequence consensus protocol (a.k.a. total order broadcast or atomic broadcast), which allows nodes to agree on a single growing sequence of values where values can be proposed by different nodes. The protocol adopts the partially synchronous model, i.e. it assumes that eventually all messages are delivered within certain time bound, although there might be periods of asynchrony in the system. The timing assumptions complicate modelling by adding more non-determinism and appear in the protocol in a form of timeouts. + +[^tendermint]: For a more precise and detailed description of the Tendermint protocol please refer to the [original paper](https://arxiv.org/pdf/1807.04938). + +#### Gossip communication + +The Tendermint protocol relies upon a gossip-based mechanism for communication between nodes: a node can broadcast a message through the gossip mechanism and it will be delivered at all correct nodes. Moreover, if a correct node delivers a message from the gossip mechanism then the same message is guaranteed to be delivered at all other correct nodes. We will model this communication mechanism as the following cross-domain component: + +![](gossip.png) + +The `bc` line belongs to the sending node and represents the set of values broadcast through this instance of the gossip mechanism; each element of the `dlvr` line belongs to the corresponding receiving node and represents the set of values delivered from that instance of the gossip mechanism. + +Individual elements in the `Set` type are concurrent and can become available independently of each other. We can think of the `Set` type as a composition of single-bit lines, each representing the presence or absence of a particular value of `T` in the set. + +If the `bc` line belongs to a correct node then the same set of values becomes available on all elements of the `dlvr` output that belong to correct nodes as the set of values on the `bc` input. Moreover, if any value becomes available on one element of `dlvr` of a correct node then the same value also becomes available on all correct nodes' elements of `dlvr`. + +Correct nodes in the Tendermint protocol only ever broadcast a single value through each instance of the `Gossip` component; however, Byzantine nodes may broadcast multiple values and all correct nodes would eventually deliver all of those values from that instance of the `Gossip` component. + +#### Overall protocol model + +Nodes in the Tendermint protocol decide on a single value at each _height_ in the growing sequence of values. At each height, the protocol may need one or multiple _rounds_ in order to reach agreement between nodes and determine the decision value to _commit_ at that height. Each round consists of the _proposal_, _prevote_, and _precommit_ stages. So we can model the overall protocol as the following cross-domain component: + +![](tendermint.png) + +Here, again, we omit sources of unspecified values and sinks, omit most of the types, but indicate the dimentionality of composite lines with superscript indeces. + +The `Tendermint` component represents the overall protocol. Its composite `value` input represents the values that would be proposed by each node (index `n`) in each round (index `r`) at each height (index `h`); the `proposer` input represent the designated proposer for each round at each height; the `decision` output represents the decision value by each node at each height. Finally, the composite `aux` line represents the auxiliary lines added for each height in order to satisfy the determinism and reversibility requirements. + +The `Height` component represents the protocol logic for each height. Its interaction lines are mostly identical to those of the `Tendermint` component, without the last level of composition, except that the auxiliary line is represented more explicitly. Namely, the `aux` line of `Tendermint` is composed of the following lines of `Height`: `decisionRound` representing the round number in which each nodes commits the decision value, `timeouts` and `aborts` representing timeouts and aborts happened at each node in each round. + +#### `Height` component + +We model the `Height` component as follows: + +![](tendermint-height.png) + +The `Round` component represents a single instance of the repetitive part of the protocol that includes the proposal, prevote, and precommit stages, in which a designated proposer broadcasts a proposal proposing a decision value to all nodes who can then broadcast prevote and precommit votes for the proposed value. At each node, instead of voting for the proposal, the prevote and precommit stages may timeout, in which case the node broadcasts a special `nil` vote, or abort, in which case the node does not broadcast any vote in that stage of the round; the propose stage can also abort. As we'll see later, the rounds and stages are coordinated by the signals from the `pmSignals` input. Those signals are required for the round stages to broadcast a proposal or vote, to timeout, or to abort. The actual timeout and abort decisions are represented by the `timeouts` and `aborts` lines. + +The Tendermint protocol defines certain conditions that a proposal must satisfy in order to be voted for. Those conditions depend on the outcomes of the previous round, so there is a forward loop, represented by the `loopFwd` line, that connects successive instances of the replicated `Round` component and conveys the required values from the previous to the next round. + +The `Commit` component represents the decision logic of the protocol that is replicated for each node. Given the proposal and precommit votes from each round, it determines the single decision by selecting the value proposed in one of the rounds, the decision round, for which there exists a strong quorum of matching precommit votes. + +The `Pacemaker` component coordinates the rounds and stages of the protocol by making the corresponding signals available according to the required dynamics of the protocol. We'll see those signals connected to the corresponding components in the next diagram. + +#### `Round` component + +We model the `Round` component as follows: + +![](tendermint-round.png) + +The `Propose`, `Prevote`, and `Precommit` components represent the stages of the protocol logic and determine the values of the corresponding messages to broadcast through the gossip mechanism. `Prevote` and `Precommit` are replicated so that there are individual instances for each node. Note that there are separate instances of the `Gossip` component for each node and stage, except for the proposal that is broadcast only by the designated proposer node, and those instances are replicated in the overall protocol component for each round and height. This way, there is no need to include the message tag, height and round numbers in the values that are broadcast through the `Gossip` component instances. The composite lines representing all-to-all communication go through transposers outside of the replication boxes in order to rearrange their components appropriately. + +The `validVR` and `lockedVR` are composite lines representing `(validValue, validRound)` and `(lockedValue, lockedRound)`, respectively, with the values corresponding to the variables of the same name from the protocol pseudo-code as it is described in the original paper[^tendermint]. Basically, `validVR` is used to determine whether the proposer should propose a new value or re-propose a value proposed in one of the previous rounds, `lockedVR` determines which proposals are safe to cast a prevote for. As we can see from the diagram, the values in those lines are updated in the `Precommit` component. The `prevoteQVals` line is a composite line each element of which corresponds to the prevote, if any, supported by a strong quorum in the previous rounds. Note how the `prevoteQVals` and `round` lines are updated for each node in a replication box: the composite `prevoteQVals` line is extended with an additional line connected to the corresponding output of the `Precommit` component, whereas `round` is simply incremented by the component labeled with `+1`. + +We will not decompose the components further since the main point was to make a sketch of how we can model the overall structure of the Tendermint protocol, namely the heights, rounds, stages, the interconnection between them, and represent the dynamics of the protocol. + +## Conclusion + +We explored a possible way of applying the ideas of reversible deterministic concurrency to modelling distributed protocols. We tried to make the vague ideas a little more concrete and give a better intuition of how an approach based on those ideas may look like by considering some guiding principles, spelling out some details, introducing some primitives and patterns, expressing this in a graphical notation. We considered modelling distributed systems as a whole and then deriving local projections for individual nodes. We also considered how we can model node failures, both benign and Byzantine. Finally, we saw how some concrete, well-known distributed protocols may look like when modeled following this approach. + +We also anticipated some potential benefits of the approach, such as modularity, composability, compositional reasoning and verification, absence of hidden data flows, enhanced debugging and verification methods, resource management, representing a distributed system as a whole and then deriving the logic and implementation for its local nodes. + +This is just the beginning of developing those ideas into a practical solution. We'll need to see what this approach means for different aspects of designing and implementing distributed protocols. We'll need to invent some kind of textual notation and develop a clear, consistent concept codifying the core principles. We'll need to find a way of implementing those ideas in real code and examine its expressivity and limitations, better understand the benefits and drawbacks. In other words, we need to find a good way of turning this into a solid foundation for our framework. + +import Admonition from '@theme/Admonition'; + + +If you like the project and find it valuable, please support its further development! 🙏 + diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/link.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/link.png new file mode 100644 index 0000000..690ef8b Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/link.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/merge-signal.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/merge-signal.png new file mode 100644 index 0000000..a938b62 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/merge-signal.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/mux-inf.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/mux-inf.png new file mode 100644 index 0000000..65305d7 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/mux-inf.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/mux.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/mux.png new file mode 100644 index 0000000..395f3f0 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/mux.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/pair.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/pair.png new file mode 100644 index 0000000..3a7b355 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/pair.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/rb-quorums.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/rb-quorums.png new file mode 100644 index 0000000..5b0e013 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/rb-quorums.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/recursion.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/recursion.png new file mode 100644 index 0000000..3e26463 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/recursion.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/replication-box.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/replication-box.png new file mode 100644 index 0000000..69e2694 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/replication-box.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/select.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/select.png new file mode 100644 index 0000000..6d68950 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/select.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/styles.css b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/styles.css new file mode 100644 index 0000000..7e6a894 --- /dev/null +++ b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/styles.css @@ -0,0 +1,5 @@ +/* Center images */ +img { + display: block; + margin: auto; +} diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum-alt.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum-alt.png new file mode 100644 index 0000000..06f564b Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum-alt.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum-inv.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum-inv.png new file mode 100644 index 0000000..e5ead84 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum-inv.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum.png new file mode 100644 index 0000000..418e568 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sum.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync-with-signal-line-abbrev.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync-with-signal-line-abbrev.png new file mode 100644 index 0000000..e36aa68 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync-with-signal-line-abbrev.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync-with-signal-line.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync-with-signal-line.png new file mode 100644 index 0000000..ddff44c Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync-with-signal-line.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync.png new file mode 100644 index 0000000..fcefc7e Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/sync.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint-height.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint-height.png new file mode 100644 index 0000000..6629573 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint-height.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint-round.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint-round.png new file mode 100644 index 0000000..9ee1fd6 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint-round.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint.png new file mode 100644 index 0000000..1d6a46a Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/tendermint.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/timer.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/timer.png new file mode 100644 index 0000000..628633d Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/timer.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/transpose.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/transpose.png new file mode 100644 index 0000000..897a581 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/transpose.png differ diff --git a/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/wb.png b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/wb.png new file mode 100644 index 0000000..d611a58 Binary files /dev/null and b/blog/2025-05-30-a-sketch-of-reversible-deterministic-concurrency-for-distributed-protocols/wb.png differ diff --git a/docusaurus.config.js b/docusaurus.config.js index 7e31b55..ddf3a14 100644 --- a/docusaurus.config.js +++ b/docusaurus.config.js @@ -3,6 +3,9 @@ import { themes as prismThemes } from 'prism-react-renderer'; +import remarkMath from 'remark-math'; +import rehypeKatex from 'rehype-katex'; + const lightCodeTheme = prismThemes.github; const darkCodeTheme = prismThemes.dracula; @@ -74,8 +77,11 @@ const config = { onInlineAuthors: 'throw', // Remove this to remove the "edit this page" links. editUrl: `${siteGitHubUrl}/edit/main/`, + remarkPlugins: [remarkMath], + rehypePlugins: [rehypeKatex], }, - ] + ], + 'image-zoom', ], presets: [ @@ -102,6 +108,16 @@ const config = { ], ], + stylesheets: [ + { + href: 'https://cdn.jsdelivr.net/npm/katex@0.13.24/dist/katex.min.css', + type: 'text/css', + integrity: + 'sha384-odtC+0UGzzFL/6PNoE8rX/SPcQDXBJ+uRepguP4QkPCm2LBxH3FA3y+fKSiJ+AmM', + crossorigin: 'anonymous', + }, + ], + themeConfig: /** @type {import('@docusaurus/preset-classic').ThemeConfig} */ ({ @@ -228,6 +244,14 @@ const config = { darkTheme: darkCodeTheme, additionalLanguages: ['bash'], }, + zoom: { + selector: '.markdown img', + background: { + // Using `--ifm-color-white` in light theme because `--ifm-background-color` makes background transparent + light: 'var(--ifm-color-white)', + dark: 'var(--ifm-background-color)', + } + } }), }; diff --git a/package-lock.json b/package-lock.json index 24a3434..f80fcdb 100644 --- a/package-lock.json +++ b/package-lock.json @@ -15,10 +15,13 @@ "@mdx-js/react": "^3.0.1", "botex": "^1.0.0", "clsx": "^2.1.1", + "docusaurus-plugin-image-zoom": "^3.0.1", "prism-react-renderer": "^2.3.1", "react": "^18.3.1", "react-dom": "^18.3.1", - "react-lite-youtube-embed": "^2.4.0" + "react-lite-youtube-embed": "^2.4.0", + "rehype-katex": "^7.0.1", + "remark-math": "^6.0.0" }, "devDependencies": { "@docusaurus/module-type-aliases": "^3.8.0", @@ -4582,6 +4585,12 @@ "resolved": "https://registry.npmjs.org/@types/json-schema/-/json-schema-7.0.15.tgz", "integrity": "sha512-5+fP8P8MFNC+AyZCDxrB2pkZFPGzqQWUzpSeuuVLvm8VMcorNYavBqoFcxK8bQz4Qsbn4oUEEem4wDLfcysGHA==" }, + "node_modules/@types/katex": { + "version": "0.16.7", + "resolved": "https://registry.npmjs.org/@types/katex/-/katex-0.16.7.tgz", + "integrity": "sha512-HMwFiRujE5PjrgwHQ25+bsLJgowjGjm5Z8FVSf0N6PwgJrwxH0QxzHYDcKsTfV3wva0vzrpqMTJS2jXPr5BMEQ==", + "license": "MIT" + }, "node_modules/@types/mdast": { "version": "4.0.4", "resolved": "https://registry.npmjs.org/@types/mdast/-/mdast-4.0.4.tgz", @@ -6944,6 +6953,19 @@ "node": ">=6" } }, + "node_modules/docusaurus-plugin-image-zoom": { + "version": "3.0.1", + "resolved": "https://registry.npmjs.org/docusaurus-plugin-image-zoom/-/docusaurus-plugin-image-zoom-3.0.1.tgz", + "integrity": "sha512-mQrqA99VpoMQJNbi02qkWAMVNC4+kwc6zLLMNzraHAJlwn+HrlUmZSEDcTwgn+H4herYNxHKxveE2WsYy73eGw==", + "license": "MIT", + "dependencies": { + "medium-zoom": "^1.1.0", + "validate-peer-dependencies": "^2.2.0" + }, + "peerDependencies": { + "@docusaurus/theme-classic": ">=3.0.0" + } + }, "node_modules/dom-converter": { "version": "0.2.0", "resolved": "https://registry.npmjs.org/dom-converter/-/dom-converter-0.2.0.tgz", @@ -8270,6 +8292,55 @@ "node": ">= 0.4" } }, + "node_modules/hast-util-from-dom": { + "version": "5.0.1", + "resolved": "https://registry.npmjs.org/hast-util-from-dom/-/hast-util-from-dom-5.0.1.tgz", + "integrity": "sha512-N+LqofjR2zuzTjCPzyDUdSshy4Ma6li7p/c3pA78uTwzFgENbgbUrm2ugwsOdcjI1muO+o6Dgzp9p8WHtn/39Q==", + "license": "ISC", + "dependencies": { + "@types/hast": "^3.0.0", + "hastscript": "^9.0.0", + "web-namespaces": "^2.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/hast-util-from-html": { + "version": "2.0.3", + "resolved": "https://registry.npmjs.org/hast-util-from-html/-/hast-util-from-html-2.0.3.tgz", + "integrity": "sha512-CUSRHXyKjzHov8yKsQjGOElXy/3EKpyX56ELnkHH34vDVw1N1XSQ1ZcAvTyAPtGqLTuKP/uxM+aLkSPqF/EtMw==", + "license": "MIT", + "dependencies": { + "@types/hast": "^3.0.0", + "devlop": "^1.1.0", + "hast-util-from-parse5": "^8.0.0", + "parse5": "^7.0.0", + "vfile": "^6.0.0", + "vfile-message": "^4.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/hast-util-from-html-isomorphic": { + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/hast-util-from-html-isomorphic/-/hast-util-from-html-isomorphic-2.0.0.tgz", + "integrity": "sha512-zJfpXq44yff2hmE0XmwEOzdWin5xwH+QIhMLOScpX91e/NSGPsAzNCvLQDIEPyO2TXi+lBmU6hjLIhV8MwP2kw==", + "license": "MIT", + "dependencies": { + "@types/hast": "^3.0.0", + "hast-util-from-dom": "^5.0.0", + "hast-util-from-html": "^2.0.0", + "unist-util-remove-position": "^5.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/hast-util-from-parse5": { "version": "8.0.3", "resolved": "https://registry.npmjs.org/hast-util-from-parse5/-/hast-util-from-parse5-8.0.3.tgz", @@ -8290,6 +8361,19 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/hast-util-is-element": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/hast-util-is-element/-/hast-util-is-element-3.0.0.tgz", + "integrity": "sha512-Val9mnv2IWpLbNPqc/pUem+a7Ipj2aHacCwgNfTiK0vJKl0LF+4Ba4+v1oPHFpf3bLYmreq0/l3Gud9S5OH42g==", + "license": "MIT", + "dependencies": { + "@types/hast": "^3.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/hast-util-parse-selector": { "version": "4.0.0", "resolved": "https://registry.npmjs.org/hast-util-parse-selector/-/hast-util-parse-selector-4.0.0.tgz", @@ -8412,6 +8496,22 @@ "url": "https://github.com/sponsors/wooorm" } }, + "node_modules/hast-util-to-text": { + "version": "4.0.2", + "resolved": "https://registry.npmjs.org/hast-util-to-text/-/hast-util-to-text-4.0.2.tgz", + "integrity": "sha512-KK6y/BN8lbaq654j7JgBydev7wuNMcID54lkRav1P0CaE1e47P72AWWPiGKXTJU271ooYzcvTAn/Zt0REnvc7A==", + "license": "MIT", + "dependencies": { + "@types/hast": "^3.0.0", + "@types/unist": "^3.0.0", + "hast-util-is-element": "^3.0.0", + "unist-util-find-after": "^5.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/hast-util-whitespace": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/hast-util-whitespace/-/hast-util-whitespace-3.0.0.tgz", @@ -9310,6 +9410,31 @@ "graceful-fs": "^4.1.6" } }, + "node_modules/katex": { + "version": "0.16.22", + "resolved": "https://registry.npmjs.org/katex/-/katex-0.16.22.tgz", + "integrity": "sha512-XCHRdUw4lf3SKBaJe4EvgqIuWwkPSo9XoeO8GjQW94Bp7TWv9hNhzZjZ+OH9yf1UmLygb7DIT5GSFQiyt16zYg==", + "funding": [ + "https://opencollective.com/katex", + "https://github.com/sponsors/katex" + ], + "license": "MIT", + "dependencies": { + "commander": "^8.3.0" + }, + "bin": { + "katex": "cli.js" + } + }, + "node_modules/katex/node_modules/commander": { + "version": "8.3.0", + "resolved": "https://registry.npmjs.org/commander/-/commander-8.3.0.tgz", + "integrity": "sha512-OkTL9umf+He2DZkUq8f8J9of7yL6RJKI24dVITBmNfZBmri9zYZQrKkuXiKhyfPSu8tUhnVBB1iKXevvnlR4Ww==", + "license": "MIT", + "engines": { + "node": ">= 12" + } + }, "node_modules/keyv": { "version": "4.5.4", "resolved": "https://registry.npmjs.org/keyv/-/keyv-4.5.4.tgz", @@ -9811,6 +9936,25 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/mdast-util-math": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/mdast-util-math/-/mdast-util-math-3.0.0.tgz", + "integrity": "sha512-Tl9GBNeG/AhJnQM221bJR2HPvLOSnLE/T9cJI9tlc6zwQk2nPk/4f0cHkOdEixQPC/j8UtKDdITswvLAy1OZ1w==", + "license": "MIT", + "dependencies": { + "@types/hast": "^3.0.0", + "@types/mdast": "^4.0.0", + "devlop": "^1.0.0", + "longest-streak": "^3.0.0", + "mdast-util-from-markdown": "^2.0.0", + "mdast-util-to-markdown": "^2.1.0", + "unist-util-remove-position": "^5.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/mdast-util-mdx": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/mdast-util-mdx/-/mdast-util-mdx-3.0.0.tgz", @@ -9972,6 +10116,12 @@ "node": ">= 0.6" } }, + "node_modules/medium-zoom": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/medium-zoom/-/medium-zoom-1.1.0.tgz", + "integrity": "sha512-ewyDsp7k4InCUp3jRmwHBRFGyjBimKps/AJLjRSox+2q/2H4p/PNpQf+pwONWlJiOudkBXtbdmVbFjqyybfTmQ==", + "license": "MIT" + }, "node_modules/memfs": { "version": "3.5.3", "resolved": "https://registry.npmjs.org/memfs/-/memfs-3.5.3.tgz", @@ -10607,6 +10757,81 @@ ], "license": "MIT" }, + "node_modules/micromark-extension-math": { + "version": "3.1.0", + "resolved": "https://registry.npmjs.org/micromark-extension-math/-/micromark-extension-math-3.1.0.tgz", + "integrity": "sha512-lvEqd+fHjATVs+2v/8kg9i5Q0AP2k85H0WUOwpIVvUML8BapsMvh1XAogmQjOCsLpoKRCVQqEkQBB3NhVBcsOg==", + "license": "MIT", + "dependencies": { + "@types/katex": "^0.16.0", + "devlop": "^1.0.0", + "katex": "^0.16.0", + "micromark-factory-space": "^2.0.0", + "micromark-util-character": "^2.0.0", + "micromark-util-symbol": "^2.0.0", + "micromark-util-types": "^2.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/micromark-extension-math/node_modules/micromark-factory-space": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/micromark-factory-space/-/micromark-factory-space-2.0.1.tgz", + "integrity": "sha512-zRkxjtBxxLd2Sc0d+fbnEunsTj46SWXgXciZmHq0kDYGnck/ZSGj9/wULTV95uoeYiK5hRXP2mJ98Uo4cq/LQg==", + "funding": [ + { + "type": "GitHub Sponsors", + "url": "https://github.com/sponsors/unifiedjs" + }, + { + "type": "OpenCollective", + "url": "https://opencollective.com/unified" + } + ], + "license": "MIT", + "dependencies": { + "micromark-util-character": "^2.0.0", + "micromark-util-types": "^2.0.0" + } + }, + "node_modules/micromark-extension-math/node_modules/micromark-util-character": { + "version": "2.1.1", + "resolved": "https://registry.npmjs.org/micromark-util-character/-/micromark-util-character-2.1.1.tgz", + "integrity": "sha512-wv8tdUTJ3thSFFFJKtpYKOYiGP2+v96Hvk4Tu8KpCAsTMs6yi+nVmGh1syvSCsaxz45J6Jbw+9DD6g97+NV67Q==", + "funding": [ + { + "type": "GitHub Sponsors", + "url": "https://github.com/sponsors/unifiedjs" + }, + { + "type": "OpenCollective", + "url": "https://opencollective.com/unified" + } + ], + "license": "MIT", + "dependencies": { + "micromark-util-symbol": "^2.0.0", + "micromark-util-types": "^2.0.0" + } + }, + "node_modules/micromark-extension-math/node_modules/micromark-util-symbol": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/micromark-util-symbol/-/micromark-util-symbol-2.0.1.tgz", + "integrity": "sha512-vs5t8Apaud9N28kgCrRUdEed4UJ+wWNvicHLPxCa9ENlYuAY31M0ETy5y1vA33YoNPDFTghEbnh6efaE8h4x0Q==", + "funding": [ + { + "type": "GitHub Sponsors", + "url": "https://github.com/sponsors/unifiedjs" + }, + { + "type": "OpenCollective", + "url": "https://opencollective.com/unified" + } + ], + "license": "MIT" + }, "node_modules/micromark-extension-mdx-expression": { "version": "3.0.1", "resolved": "https://registry.npmjs.org/micromark-extension-mdx-expression/-/micromark-extension-mdx-expression-3.0.1.tgz", @@ -12523,6 +12748,27 @@ "integrity": "sha512-LDJzPVEEEPR+y48z93A0Ed0yXb8pAByGWo/k5YYdYgpY2/2EsOsksJrq7lOHxryrVOn1ejG6oAp8ahvOIQD8sw==", "license": "MIT" }, + "node_modules/path-root": { + "version": "0.1.1", + "resolved": "https://registry.npmjs.org/path-root/-/path-root-0.1.1.tgz", + "integrity": "sha512-QLcPegTHF11axjfojBIoDygmS2E3Lf+8+jI6wOVmNVenrKSo3mFdSGiIgdSHenczw3wPtlVMQaFVwGmM7BJdtg==", + "license": "MIT", + "dependencies": { + "path-root-regex": "^0.1.0" + }, + "engines": { + "node": ">=0.10.0" + } + }, + "node_modules/path-root-regex": { + "version": "0.1.2", + "resolved": "https://registry.npmjs.org/path-root-regex/-/path-root-regex-0.1.2.tgz", + "integrity": "sha512-4GlJ6rZDhQZFE0DPVKh0e9jmZ5egZfxTkp7bcRDuPlJXbAwhxcl2dINPUAsjLdejqaLsCeg8axcLjIbvBjN4pQ==", + "license": "MIT", + "engines": { + "node": ">=0.10.0" + } + }, "node_modules/path-to-regexp": { "version": "1.9.0", "resolved": "https://registry.npmjs.org/path-to-regexp/-/path-to-regexp-1.9.0.tgz", @@ -14585,6 +14831,25 @@ "node": ">=6" } }, + "node_modules/rehype-katex": { + "version": "7.0.1", + "resolved": "https://registry.npmjs.org/rehype-katex/-/rehype-katex-7.0.1.tgz", + "integrity": "sha512-OiM2wrZ/wuhKkigASodFoo8wimG3H12LWQaH8qSPVJn9apWKFSH3YOCtbKpBorTVw/eI7cuT21XBbvwEswbIOA==", + "license": "MIT", + "dependencies": { + "@types/hast": "^3.0.0", + "@types/katex": "^0.16.0", + "hast-util-from-html-isomorphic": "^2.0.0", + "hast-util-to-text": "^4.0.0", + "katex": "^0.16.0", + "unist-util-visit-parents": "^6.0.0", + "vfile": "^6.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/rehype-raw": { "version": "7.0.0", "resolved": "https://registry.npmjs.org/rehype-raw/-/rehype-raw-7.0.0.tgz", @@ -14689,6 +14954,22 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/remark-math": { + "version": "6.0.0", + "resolved": "https://registry.npmjs.org/remark-math/-/remark-math-6.0.0.tgz", + "integrity": "sha512-MMqgnP74Igy+S3WwnhQ7kqGlEerTETXMvJhrUzDikVZ2/uogJCb+WHUg97hK9/jcfc0dkD73s3LN8zU49cTEtA==", + "license": "MIT", + "dependencies": { + "@types/mdast": "^4.0.0", + "mdast-util-math": "^3.0.0", + "micromark-extension-math": "^3.0.0", + "unified": "^11.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/remark-mdx": { "version": "3.1.0", "resolved": "https://registry.npmjs.org/remark-mdx/-/remark-mdx-3.1.0.tgz", @@ -14908,6 +15189,18 @@ "node": ">=4" } }, + "node_modules/resolve-package-path": { + "version": "4.0.3", + "resolved": "https://registry.npmjs.org/resolve-package-path/-/resolve-package-path-4.0.3.tgz", + "integrity": "sha512-SRpNAPW4kewOaNUt8VPqhJ0UMxawMwzJD8V7m1cJfdSTK9ieZwS6K7Dabsm4bmLFM96Z5Y/UznrpG5kt1im8yA==", + "license": "MIT", + "dependencies": { + "path-root": "^0.1.1" + }, + "engines": { + "node": ">= 12" + } + }, "node_modules/resolve-pathname": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/resolve-pathname/-/resolve-pathname-3.0.0.tgz", @@ -16168,6 +16461,20 @@ "url": "https://github.com/sponsors/sindresorhus" } }, + "node_modules/unist-util-find-after": { + "version": "5.0.0", + "resolved": "https://registry.npmjs.org/unist-util-find-after/-/unist-util-find-after-5.0.0.tgz", + "integrity": "sha512-amQa0Ep2m6hE2g72AugUItjbuM8X8cGQnFoHk0pGfrFeT9GZhzN5SW8nRsiGKK7Aif4CrACPENkA6P/Lw6fHGQ==", + "license": "MIT", + "dependencies": { + "@types/unist": "^3.0.0", + "unist-util-is": "^6.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/unist-util-is": { "version": "6.0.0", "resolved": "https://registry.npmjs.org/unist-util-is/-/unist-util-is-6.0.0.tgz", @@ -16207,6 +16514,20 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/unist-util-remove-position": { + "version": "5.0.0", + "resolved": "https://registry.npmjs.org/unist-util-remove-position/-/unist-util-remove-position-5.0.0.tgz", + "integrity": "sha512-Hp5Kh3wLxv0PHj9m2yZhhLt58KzPtEYKQQ4yxfYFEO7EvHwzyDYnduhHnY1mDxoqr7VUwVuHXk9RXKIiYS1N8Q==", + "license": "MIT", + "dependencies": { + "@types/unist": "^3.0.0", + "unist-util-visit": "^5.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/unist-util-stringify-position": { "version": "4.0.0", "resolved": "https://registry.npmjs.org/unist-util-stringify-position/-/unist-util-stringify-position-4.0.0.tgz", @@ -16507,6 +16828,19 @@ "uuid": "dist/bin/uuid" } }, + "node_modules/validate-peer-dependencies": { + "version": "2.2.0", + "resolved": "https://registry.npmjs.org/validate-peer-dependencies/-/validate-peer-dependencies-2.2.0.tgz", + "integrity": "sha512-8X1OWlERjiUY6P6tdeU9E0EwO8RA3bahoOVG7ulOZT5MqgNDUO/BQoVjYiHPcNe+v8glsboZRIw9iToMAA2zAA==", + "license": "MIT", + "dependencies": { + "resolve-package-path": "^4.0.3", + "semver": "^7.3.8" + }, + "engines": { + "node": ">= 12" + } + }, "node_modules/value-equal": { "version": "1.0.1", "resolved": "https://registry.npmjs.org/value-equal/-/value-equal-1.0.1.tgz", diff --git a/package.json b/package.json index 72ea8d1..361dfcb 100644 --- a/package.json +++ b/package.json @@ -21,10 +21,13 @@ "@mdx-js/react": "^3.0.1", "botex": "^1.0.0", "clsx": "^2.1.1", + "docusaurus-plugin-image-zoom": "^3.0.1", "prism-react-renderer": "^2.3.1", "react": "^18.3.1", "react-dom": "^18.3.1", - "react-lite-youtube-embed": "^2.4.0" + "react-lite-youtube-embed": "^2.4.0", + "rehype-katex": "^7.0.1", + "remark-math": "^6.0.0" }, "devDependencies": { "@docusaurus/module-type-aliases": "^3.8.0",