Bengt/specs consistency/base ledger

packages/docs/pages/ledger/env-vars.mdx

@@ -1,5 +1,5 @@
 import { Callout } from 'nextra-theme-docs'
-import Expandable from "../../components/Expandable"; // TODO: Use this component when properly css'd
+import Expandable from "../../components/Expandable";
 
 # Environment variables
 

packages/specs/pages/base-ledger.mdx

@@ -1,3 +1,12 @@
-## Base ledger
+# Base ledger
 
-The base ledger of Namada includes a [consensus system](./base-ledger/consensus.md), validity predicate-based [execution system](./base-ledger/execution.md), and signalling-based [governance mechanism](./base-ledger/governance.md). Namada's ledger also includes proof-of-stake, slashing, fees, and inflation funding for staking rewards, shielded pool incentives, and public goods — these are specified in the [economics section](./economics.md). This section also documents Namada's [multisignature VP](./base-ledger/multisignature.md), [fungible token VP](./base-ledger/fungible-token.md), [replay protection system](./base-ledger/replay-protection.md), and [block space allocator](./base-ledger/block-space-allocator.md).
+The base ledger of Namada includes a [consensus mechanism](./base-ledger/consensus.md) and a validity-predicate based [execution system](./base-ledger/execution.md). 
+
+## Consensus
+The consensus mechanism on Namada provides an algorithmic way for validators to communicate votes and collectively agree on a consistent state. The algorithim, coupled with a cryptoeconomic assurance called "proof of stake", ensures that non-colluding validators acting in their (economic) self interest will follow the consensus algorithm in a predictable manner.
+
+## Validity predicates
+The validity-predicate based execution mechanism is inherited from the architectural design philosophy of Anoma. The fundamental idea is that a "valid state" is defined as that which satisfies a set of boolean conditions. These boolean conditions are encoded by functional "validity predicates", which are invoked whenever a state is being proposed. If all validity predicates in the system return the boolean `true`, this defines a valid state which validators can vote on. The validity predicate based mechanism differs from the traditional "smart-contract" based execution model, where a valid state is instead defined as that which results from a series of pre-defined valid execution steps. These execution steps are defined within the smart contract, and verifying the validity of the new state requires *each* validator to run the series of execution steps.
+
+## Replay protection & block space allocator
+In addition to describing the execuction model and consensus, this section  also documents Namada's [replay protection system](./base-ledger/replay-protection.md), and [block space allocator](./base-ledger/block-space-allocator.md).

packages/specs/pages/base-ledger/block-space-allocator.mdx

@@ -1,42 +1,45 @@
+import { Callout } from 'nextra-theme-docs'
 import blockSpaceEx from './images/block-space-allocator-example.svg'
 import blockSpaceBins from './images/block-space-allocator-bins.svg'
 
 # Block space allocator
 
-Block space in Tendermint is a resource whose management is relinquished to the 
+<Callout type="info">
+Note that the DKG scheme for front-running prevention is not a feature included in the first release of Namada. 
+The block-space-allocator infrastructure still exists, but the decryption is hardcoded and does not require validator coordination.
+</Callout>
+
+Block space in CometBFT is a resource whose management is relinquished to the 
 running application. This section covers the design of an abstraction that 
 facilitates the process of transparently allocating space for transactions in a 
 block at some height $H$, whilst upholding the safety and liveness properties 
 of Namada.
 
-## On block sizes in Tendermint and Namada
+## On block sizes in CometBFT and Namada
 
-[Block sizes in Tendermint]
-(configured through the $MaxBytes$ consensus 
+[Block sizes in CometBFT](https://github.com/cometbft/cometbft/blob/main/spec/abci/abci%2B%2B_app_requirements.md#blockparamsmaxbytes) (configured through the `MaxBytes` consensus 
 parameter) have a minimum value of $1\ \text{byte}$, and a hard cap of $100\ 
-MiB$, reflecting the header, evidence of misbehavior (used to slash 
+\text{MiB}$, reflecting the header, evidence of misbehavior (used to slash 
 Byzantine validators) and transaction data, as well as any potential protobuf 
-serialization overhead. Some of these data are dynamic in nature (e.g. 
+serialization overhead. Some of this data is dynamic in nature (e.g. 
 evidence of misbehavior), so the total size reserved to transactions in a block 
 at some height $H_0$ might not be the same as another block's, say, at some 
-height $H_1 : H_1 \ne H_0$. During Tendermint's `PrepareProposal` ABCI phase, 
+height $H_1 : H_1 \ne H_0$. During CometBFT's `PrepareProposal` ABCI phase, 
 applications receive a $MaxTxBytes$ parameter whose value already accounts for 
 the total space available for transactions at some height $H$. Namada does not 
-rely on the $MaxTxBytes$ parameter of `RequestPrepareProposal`; instead, 
-app-side validators configure a $MaxProposalSize$ parameter at genesis (or
-through governance) and set Tendermint blocks' $MaxBytes$ parameter to its 
+rely on the `MaxTxBytes` parameter of `RequestPrepareProposal`; instead, 
+app-side validators configure a `MaxProposalSize` parameter at genesis (or
+through governance) and set CometBFT blocks' `MaxBytes` parameter to its 
 upper bound.
 
-[Block sizes in Tendermint](https://github.com/tendermint/tendermint/blob/v0.34.x/spec/abci/apps.md#blockparamsmaxbytes)
-
 ## Transaction batch construction
 
-During Tendermint's `PrepareProposal` ABCI phase, Namada (the ABCI server) is 
-fed a set of transactions $M = \{\ tx\ |\ tx\text{ in Tendermint's mempool}\ 
+During CometBFT's `PrepareProposal` ABCI phase, Namada (the ABCI server) is 
+fed a set of transactions $M := \{\ tx\ |\ tx\text{ in CometBFT's mempool}\ 
 \}$, whose total combined size (i.e. the sum of the bytes occupied by each $tx 
-: tx \in M$) may be greater than $MaxProposalBytes$. Therefore, consensus round 
+: tx \in M$) may be greater than `MaxProposalBytes`. Therefore, consensus round 
 leaders are responsible for selecting a batch of transactions $P$ whose total 
-combined bytes $P_{Len} \le MaxProposalBytes$.
+combined bytes $P_{Len} \le $ `MaxProposalBytes`.
 
 To stay within these bounds, block space is **allotted** to different kinds of 
 transactions: decrypted, protocol and encrypted transactions. Each kind of 
@@ -77,22 +80,23 @@ stops as soon as the respective `TxBin` runs out of space for some
 $tx_{Protocol} : tx_{Protocol} \in M$. The `TxBin` for protocol transactions is 
 allotted half of the remaining block space, after decrypted transactions have 
 been **allocated**.
+{/* TODO: The ordering of these steps is a bit unintuitive. Feels like we should begin with `BuildingEncryptedTx` */}
+{/* TODO: The WithoutEncryptedTxs is not clear. Are these special types of protocol txs? */}
 3. `BuildingEncryptedTxBatch` - This state behaves a lot like the previous 
 state, with one addition: it takes a parameter that guards the encrypted 
 transactions `TxBin`, which in effect splits the state into two sub-states. 
-When `WithEncryptedTxs` is active, we fill block space with encrypted 
-transactions (as the name implies); orthogonal to this mode of operation, there 
-is `WithoutEncryptedTxs`, which, as the name implies, does not allow encrypted 
+When `WithEncryptedTxs` is active, block space is filled with encrypted 
+transactions (as the name implies). Orthogonal to this mode of operation, there 
+exists `WithoutEncryptedTxs`, which, as the name implies, does not allow encrypted 
 transactions to be included in a block. The `TxBin` for encrypted transactions 
 is allotted $\min(R,\frac{1}{3} MaxProposalBytes)$ bytes, where $R$ is the 
 block space remaining after allocating space for decrypted and protocol 
 transactions.
 4. `FillingRemainingSpace` - The final state of the `BlockSpaceAllocator`. Due 
 to the short-circuit behavior of a `TxBin`, on allocation errors, some space 
 may be left unutilized at the end of the third state. At this state, the only 
-kinds of
-transactions that are left to fill the available block space are
-of type encrypted and protocol, but encrypted transactions are forbidden
+transaction types that are left to fill the available block space are
+encrypted and protocol transactions, but encrypted transactions are forbidden
 to be included, to avoid breaking their invariant regarding
 allotted block space (i.e. encrypted transactions can only occupy up to
 $\frac{1}{3}$ of the total block space for a given height $H$). As such,
@@ -123,16 +127,16 @@ Consider the following diagram:
 We denote `D`, `P` and `E` as decrypted, protocol and encrypted transactions, 
 respectively.
 
-* At height $H$, block space is evenly divided in three parts, one for each 
+* At height $H$, block space is evenly divided into three parts, one for each 
 kind of transaction type.
-* At height $H+1$, we do not include encrypted transactions in the proposal, 
+* At height $H+1$, no encrypted transactions are included in the proposal, 
 therefore protocol transactions are allowed to take up to $\frac{2}{3}$ of the 
 available block space.
 * At height $H+2$, no encrypted transactions are included either. Notice that 
 no decrypted transactions were included in the proposal, since at height $H+1$ 
-we did not decide on any encrypted transactions. In sum, only protocol 
+no encrypted transactions were committed. In sum, only protocol 
 transactions are included in the proposal for the block with height $H+2$.
-* At height $H+3$, we propose encrypted transactions once more. Just like in 
+* At height $H+3$, encrypted transactions are proposed once more. Just like in 
 the previous scenario, no decrypted transactions are available. Encrypted 
 transactions are capped at $\frac{1}{3}$ of the available block space, so the 
 remaining $\frac{1}{2} - \frac{1}{3} = \frac{1}{6}$ of the available block 
@@ -146,31 +150,33 @@ Batches of transactions proposed during ABCI's `PrepareProposal` phase are
 validated at the `ProcessProposal` phase. The validation conditions are 
 relaxed, compared to the rigid block structure imposed on blocks during 
 `PrepareProposal` (i.e. with decrypted, protocol and encrypted transactions 
-appearing in this order, as [examplified above](#example)). Let us fix $H$ as 
-the height of the block $B$ currently being decided through Tendermint's 
-consensus mechanism, $P$ as the batch of transactions proposed at $H$ as $B$'s 
-payload and $V$ as the current set of active validators. To vote on $P$, each 
-validator $v \in V$ checks:
-
-* If the length of $P$ in bytes, defined as $P_{Len} := \sum_{tx \in 
-P} \text{size\_of}(tx)$, is not greater than $MaxProposalBytes$.
-* If $P$ does not contain more than $\frac{1}{3} MaxProposalBytes$ worth of 
+appearing in this order, as [examplified above](#example)). 
+
+Define $H$ as the height of block $B$ currently being decided through Tendermint's 
+consensus mechanism. Define $P$ as the batch of transactions proposed at $H$ as $B$'s 
+payload and define $V$ as the current set of active validators. To vote on $P$, each 
+validator $v \in V$ checks that:
+
+* The length of $P$ in bytes, defined as $P_{Len} := \sum_{tx \in 
+P} \text{size\_of}(tx)$, is not greater than `MaxProposalBytes`.
+* $P$ does not contain more than $\frac{1}{3}$ `MaxProposalBytes` worth of 
 encrypted transactions.
-    - While not directly checked, our batch construction invariants guarantee 
-that we will constrain decrypted transactions to occupy up to $\frac{1}{3} 
-MaxProposalBytes$ bytes of the available block space at $H$ (or any block 
+    - While not directly checked, the batch construction invariants guarantee 
+that decrypted transactions are constrained to occupy up to $\frac{1}{3} $
+`MaxProposalBytes` bytes of the available block space at $H$ (or any block 
 height, in fact).
-* If all decrypted transactions from $H-1$ have been included in the proposal 
+* All decrypted transactions from $H-1$ have been included in the proposal 
 $P$, for height $H$.
-* That no encrypted transactions were included in the proposal $P$, if no
+* No encrypted transactions were included in the proposal $P$, if no
 encrypted transactions should be included at $H$.
-    - N.b. the conditions to reject encrypted transactions are still not clearly
-    specced out, therefore they will be left out of this section, for the
-    time being.
+
+<Callout type="info">
+N.b. the conditions to reject encrypted transactions are not specced out, and would be necessary should Namada incorporate the DKG scheme
+</Callout>
 
 Should any of these conditions not be met at some arbitrary round $R$ of $H$, 
 all honest validators $V_h : V_h \subseteq V$ will reject the proposal $P$. 
-Byzantine validators are permitted to re-order the layout of $P$ typically 
+Byzantine validators would be permitted to re-order the layout of $P$ typically 
 derived from the [`BlockSpaceAllocator`](#transaction-batch-construction) $A$, 
 under normal operation, however this should not be a compromising factor of the 
 safety and liveness properties of Namada. The rigid layout of $B$ is simply a 
@@ -180,25 +186,21 @@ consequence of $A$ allocating in different phases.
 
 Validator set updates, one type of protocol transactions decided through BFT 
 consensus in Namada, are fundamental to the liveness properties of the Ethereum 
-bridge, thus, ideally we would also check if these would be included once per 
-epoch at the `ProcessProposal` stage. Unfortunately, achieving a quorum of 
-signatures for a validator set update between two adjacent block heights 
+bridge. Unfortunately, achieving a quorum of signatures for a validator set update between two adjacent block heights 
 through ABCI alone is not feasible. Hence, the Ethereum bridge is not a live 
 distributed system, since there is the possibility to cross an epoch boundary 
 without constructing a valid proof for some validator set update. In practice, 
 however, it is nearly impossible for the bridge to get "stuck", as validator 
 set updates are eagerly issued at the start of an epoch, whose length should be 
 long enough for consensus(*) to be reached on a single validator set update.
 
-(*) Note that we loosely used consensus here to refer to the process of 
+(*) Note that consensus was used loosely here to refer to the process of 
 acquiring a quorum (e.g. more than $\frac{2}{3}$ of voting power, by stake) of 
 signatures on a single validator set update. "Chunks" of a proof (i.e. 
 individual votes) are decided and batched together, until a complete proof is 
 constructed.
 
-We cover validator set updates in detail in [the Ethereum bridge section].
-
-[the Ethereum bridge section](../interoperability/ethereum-bridge.md)
+Validator set updates are covered in more detail in [the Ethereum bridge section](../interoperability/ethereum-bridge.md).
 
 ## Governance
 

packages/specs/pages/base-ledger/consensus.mdx

@@ -1,3 +1,17 @@
 # Consensus
 
-Namada uses [CometBFT](https://github.com/cometbft/cometbft/) (nee Tendermint Go) through the [cometbft-rs](https://github.com/heliaxdev/tendermint-rs) (nee tendermint-rs) bindings in order to provide peer-to-peer transaction gossip, BFT consensus, and state machine replication for Namada's custom state machine. CometBFT implements the Tendermint consensus algorithm, which you can read more about [here](https://arxiv.org/abs/1807.04938).
+Namada uses [CometBFT](https://github.com/cometbft/cometbft/) (nee Tendermint Go) through the [cometbft-rs](https://github.com/heliaxdev/tendermint-rs) (nee tendermint-rs) bindings in order to provide peer-to-peer transaction gossip, Byzantine fault tolerant (BFT) consensus, and state machine replication for Namada's custom state machine. CometBFT implements the Tendermint consensus algorithm, which you can read more about [here](https://arxiv.org/abs/1807.04938).
+
+{/* Maybe we want to leave out the below section. I just felt we should give a brief summary of CometBFT */}
+## The benefits of using CometBFT
+
+Using the CometBFT consensus algorithm comes with a number of benefits including but not limited to:
+
+- Fast finality 
+    - Tendermint achieves fast and deterministic finality, meaning that once a block is committed to the blockchain, it is irreversible. This is crucial for applications rely on settled transactions that cannot be rolled back.
+- Inter-blockchain communication system (IBC)
+    - Composability with all other Tendermint based blockchains, such as Cosmos-ecosystem blockchains
+- Battle tested
+    - The entire cosmos-ecosystem have been using the Tendermint 
+- Customisable
+    - Allows the setting of various of parameters, including the ability to implement a custom proof of stake algorithm