rapidchain.ml

(* RapidChain: Scaling Blockchain via Full Sharding *)
(* OmniLedger: A Secure, Scale-Out, Decentralized Ledger via Sharding https://eprint.iacr.org/2017/406.pdf *)

(* ida, kademlia, cross-verify, reshard, bootstrap *)
(* opt: batch, pipeline, sparsify *)

type state                                                                       (* utxo state: transaction id, row *)

type signature                                                                  (* public-key signature *)

(* each transaction in RapidChain has a unique identity, a list of inputs (depicted by their identities), and a list of outputs that is shown by the transaction ID and their row number  *)
(* a transaction consists of a set of inputs and outputs that reference other transactions, and a signature generated by their issuer to certify its validity *)
(* https://bitcoin.org/bitcoin.pdf *)
(* Chimeric Ledgers: Translating and Unifying UTXO-based and Account-based Cryptocurrencies https://eprint.iacr.org/2018/262.pdf *)
type tx = {
  (* Each committee only stores transactions that have the committee ID as their prefix in their IDs...  Committee C0 wants to locate committee C7 (via C4 and C6) responsible for transactions with prefix 0x111. *)
  (* Since transactions are assigned to committees based on their randomly-generated IDs, transactions are expected to be distributed uniformly among committees. *)
  id: int;
  inputs: txs;
  (* because the inputs and outputs of each transaction might reside in multiple committees *)
  (* the committee that stores tx and its possible UTXOs as the output committee, *)
  (*  the leader requires to requests a verication proof from a constant number of committees assuming tx has constant number of inputs and outputs. *)
  (* [C_out] a committee responsible for storing tx. We refer to this committee as the output committee for tx and denote it by Cout *)
  outputs: txs;
  signature: signature }                                                                         (* [tx], Let x[i,j] represent the j-th transaction in the i-th block. *)
and txs = tx list

(* we assume 512 B/tx, one-day long epochs, 100 ms network latency for all links, and 20 Mbps bandwidth for all nodes in all three protocols. *)
(* "each block of transaction consist of 4,096 transactions, where each transaction consists of 512 bytes resulting in a block size of 2 MB." *)
let tx_size = 512                                                               (* 512 B/tx *)
let block_txs = 4096                                                            (* each block of transaction consist of 4,096 transactions *)
let epoch_time = 24 * 60 * 60                                                   (* 1-day long epoch *)
let network_latency = 0.1                                                       (* 100-ms network latency for all links *)
let network_bandwidth = 20                                                      (* 20 Mbps bandwidth for all nodes *)

(* "each block of transaction consist of 4,096 transactions, where each transaction consists of 512 bytes resulting in a block size of 2 MB." *)
let block_size = 2 * 1024 * 1024                                                (* 2MB [b] *)

(* todo: reconfiguration block *)
type block = tx list                                                            (* [B_i] *)

type hash
type tag = Propose | Echo | Pending | Accept
type step = int                                                                       (* [i] block iteration, consensus iteration [[should use timestamp + nonce]] *)
type random = float

type chunk
type chunks = chunk list

type key
type keys = key list
type id = {
  public: key;
  secret: key }

type header = {                                                                 (* block header [H_i] digest, proposal, safe value *)
  step: step;                                                                    (* iteration number *)
  root: hash }                                                                  (* the root of the Merkle tree from IDA-Gossip *)
type headers = header list                                                      (* The m f + 1 echoes serve as the proof of why the node accepts Hi *)


(* any set of m = o(n) nodes as a committee if at least an f < 1/2 fraction of its members belongs to honest nodes 

[C] the reference committee creates k committees {C1, ...,Ck } each of size O(logn) 

Let node P be a member of a group [C]
*)
type shard = {                                                                  (* [X_i] shard, committee, group. a set X containing k disjoint subsets or shards *)
  nodes: keys;
  random: random;
  mutable leader: key; }                                                       
and shards = shard list

(* 
Consider a peer-to-peer network with n nodes who establish identities (i.e., public/private keys)
through a Sybil-resistant identity generation mechanism such as that of [7], which requires every node to solve
a computationally-hard puzzle on their locally-generated identities (i.e., public keys) veried by all other (honest)
nodes without the assumption of a trusted randomness beacon.

Let node P be a member of a group [C]. We refer to other members of C as the neighbors of P in C.

When a user wants to submit a transaction, it sends the transaction to any arbitrary RapidChain node who will
forward it to the corresponding committee via the Kademlia routing mechanism.

When a node wants to send a message to another node in
the system it identifies the node among its neighbors (which it stores locally) that is closest to the destination node’s
Kademlia ID (or KID) and it asks it to run recursively the discovery mechanism.
*)
and node = {                                                                    (* [P] "Let node P be a member of a group C" *)
  id: id;  
  mutable txs: txs;
  mutable shard: shard;
  mutable step: step;                                                           (* current iteration, block height *)
  mutable headers: headers;                                                             (* a valid accept message with a proof certificate on H_0 *)
  (* Let d denote the degree of every committee member, i.e., the number of neighbors that are chosen uniformly at random *)
  (* Kademlia bucket parameter k = 10 or 20?? *)
  peers: nodes }                                                                (* [d] neighbors; "other members of C as the neighbors of P in C" *)
and nodes = node list

(* during our bootstrapping phase: each node in the global P2P network can accept up to 8 outgoing connections and up to 125 incoming connections *)
let bootstrap_out_peer_size = 8

(* during consensus epoch, nodes communicate through much smaller P2P overlays created within every committee, where
each node accepts up to 16 outgoing connections and up to 125 incoming connections. *) 
let out_peer_size = 16 
let in_peer_size = 125


type chain                                                                      (* ledger, blockchain *)

(* 
a set of transactions are sent to our protocol by a set of users that are external to the protocol. 

the client-perceived latency is roughly 8 times more than the confirmation latency 

user-perceived latency measures the delay between the time that a user sends a transaction, tx, to the network until the time that tx can be confirmed by any (honest) node in the system

Each user sends its transactions to a subset of nodes (found via a P2P discovery protocol) who batch and forward the transactions to the corresponding committee responsible for processing them.

Each transaction tx is submitted by a user of the system to a small number of arbitrary RapidChain nodes who route tx, via an inter-committee routing protocol, to a committee responsible for storing tx.
*)
type user = {
  portals: nodes }                                                              (* gateway *)

(* up to 80 bytes size including signatures and control bits *)
type msg = {                                                                    (* consensus protocol *)
  signature: signature;                                                         (* sender's signature *)
  header: header;
  tag: tag }

type msg2 = {                                                                   (* block propagation *)
  signature: signature;                                                         (* sender's signature *)
  chunk: chunk }

let get_portals () : nodes = []                                                 (* P2P discovery *)
let get_peers () : nodes = []                                                   (* Peer discovery of the same sharding committee *)
let get_shards () : shards = []                                                 (* Committee discovery *)
let get_nodes () : nodes = []                                                   (* Kademlia node discovery *)
let get_group () : nodes = []                                                   (* Subgroup Peer Discovery. *)

let list_size = List.length

(* Inter-committee routing, Routing Overlay Network
Node discovery & messaging routing in logarithmic steps

each node in the system is assigned an identier and there is a metric
of distance between identiers (for example, the Hamming distance of the identiers)

"each node stores information about all members of its committee as well as about log log(n) nodes in each of the logn closest committees to its own committee. 

Each committee-to-committee message is implemented by having all nodes in the sender committee send the message to all nodes they know in the receiver committee. Each node who receives a message invokes the IDA-gossip protocol to sent the message to all other members of its committee."

"When we say a committee runs a protocol, we mean all honest members of the committee participate in an execution of the protocol. Let C1,C2 be two committees. When we say C1 sends a message M to C2, we mean every honest member of C1 sends M to every member of C2 who he knows. Since each member of C2 may receive different messages due to malicious behavior, it chooses the message with a frequency of at least 1/2 + 1"

[Maymounkov2002] Kademlia: A peer-to-peer information system based on the xor metric *)
let route = 2
  (* node_corrupt_probability *)

(* Cross-shard verification *)
let cross_shard_check (tx:tx) : bool = 
(*
  The members of Cout batch several transactions into a large block (about 2 MB), and then,
  append it to their own ledger. Before the block can be appended, the committee has to verify the validity of every
  transaction in the block. 
  
  "To verify cross-shard transactions, RapidChain’s committees discover each other via an efficient routing mechanism
  inspired by Kademlia [48] that incurs only a logarithmic (in number of committees) latency and storage"
  
  Another challenge in using a synchronous consensus protocol happens in the cross-shard transaction scenario,
  where a malicious leader can deceive the input committee with a transaction that has been accepted by some but not
  all honest members in the output committee.
  
  Let tx denote the transaction sent by the user. In the verification process, multiple committees may be involved
  to ensure all the input UTXOs to tx are valid. We refer to the committee that stores tx and its possible UTXOs as the
  output committee, and denote it by Cout. We refer to the committees that store the input UTXOs to tx as the input
  committees, and denoted them by C (1) in , . . . ,C (N ) in .
  
  If I1, I2 belong to different committees other than Cout, then the leader of Cout, creates three new transactions: For i
  ∈ {1, 2}, txi with input Ii and output I 0 i , where |I 0 i | = |Ii | (i.e., the same amounts) and I 0 i belongs to
  Cout. tx3 with inputs I 0 1 and I 0 2 and output O. The leader sends txi to C i in via the inter-committee routing
  protocol, and C i in adds txi to its ledger. If txi is successful, C i in sends I 0 i to Cout. Finally, Cout adds tx3 to
  its ledger.
  
  Security of Cross-Shard Verification. Without loss of generality, we assume tx has two inputsI1, I2 and one output O. If
  the user provides valid inputs, both input committees successfully verify their transactions and send the new UTXOs to
  the output committee. Thus, tx3 will be successful. If both inputs are invalid, both input committees will not send I 0
  i , and as a result tx3 will not be accepted. If I1 is valid but I2 is invalid, then C 1 in successfully transfers I 0 1
  but C 2 in will not send I 0 2 . Thus, tx3 will not be accepted in Cout. However, I 0 1 is a valid UTXO in the output
  committee and the user can spend it later. The output committee can send the resulting UTXO to the user.
  
  Moreover, with probability 96.3% (see Section 6.7) tx is a cross-shard transaction, and the leader requires to requests
  a verification proof from a constant number of committees assuming tx has constant number of inputs and outputs. The
  cost of routing the requests and their responses is O(m logn), and the cost of consensus on the request and response is
  O(m2 /b) (amortized on the block size due to batching) which happens in every input and output committee.

  Before the block can be appended, the committee has to verify the validity of every transaction in the block. 

  [rapidchain’s utxo splitting is very similar to eth 2.0's contract yanking.]
  https://notes.ethereum.org/s/H1PGqDhpm#Cross-shard-communication
    https://ethresear.ch/t/cross-shard-contract-yanking/1450
    https://ethresear.ch/t/simple-synchronous-cross-shard-transaction-protocol/3097/12
  https://github.com/ethereum/wiki/wiki/Sharding-FAQs#how-can-we-facilitate-cross-shard-communication
  
  let txs = tx.input
  new_tx 

*)
  assert (list_size tx.outputs = 1);                                             (* todo?? *)  
  (* If I1, I2 belong to different committees other than Cout, then the leader of Cout, creates three new transactions: For i ∈ {1, 2}, txi with input Ii and output I 0 i , where |I 0 i | = |Ii | (i.e., the same amounts) and I 0 i belongs to Cout. tx3 with inputs I 0 1 and I 0 2 and output O. The leader sends txi to C i in via the inter-committee routing protocol, and C i in adds txi to its ledger. If txi is successful, C i in sends I 0 i to Cout. Finally, Cout adds tx3 to its ledger. *)
  true
  

  
let check_block () = ()                                                         (* verify, validate *)
let add_block () = ()

let node_init (id:id) (shard:shard) : node = {
  id = id;
  txs = [];
  shard = shard;
  step = -1;
  headers = [];
  peers = get_peers () }

(* 
"RapidChain can process (and confirm) more than 7,300 tx/sec with an expected
confirmation latency of roughly 8.7 seconds in a network of 4,000 nodes with an overwhelming time-to-failure of
more than 4,500 years"

"We simulate networks of up to 4,000 nodes by oversubscribing a set of 32 machines each running up to 125 RapidChain instances. Each machine has a 64-core Intel Xeon Phi 7210 @ 1.3GHz processor and a 10-Gbps communication link. To simulate geographically-distributed nodes, we consider a latency of 100 ms for every message and a bandwidth of 20 Mbps for each node. Similar to Bitcoin Core, we assume each node in the global P2P network can accept up to 8 outgoing connections and up to 125 incoming connections. The global P2P overlay is only used during our bootstrapping phase. During consensus epoch, nodes communicate through much smaller P2P overlays created within every committee, where each node accepts up to 16 outgoing connections and up to 125 incoming connections."

doubling the network size increases the capacity of RapidChain by 1.5-1.7 times *)
let network_nodes = 4000                                                        (* the total number of nodes [n] *)
let network_security = 20                                                       (* [λ] lambda, the security parameter *)

(* 
Overhead of Bootstrapping. We measure the overheads of our bootstrapping protocol to setup committees for
the rst time in two dierent experiments with 500 and 4,000 nodes. The measured latencies are 2.7 hours and 18.5
hours for each experiment respectively. Each participant in these two experiments consumes a bandwidth of roughly
29.8 GB and 86.5 GB respectively.

 *)
let bootstrap = ()
  (* a hard-coded seed and the initial network size which
is known to all nodes since we assume the initial set of nodes have already established identities. *)

(* t < n/3 denote the total number of corrupt nodes 

"The corrupt nodes not only may collude with each other
but also can deviate from the protocol in any arbitrary manner, e.g., by sending invalid or inconsistent messages, or
remaining silent."

"At the end of each epoch, the adversary is allowed to corrupt a constant (and small) number of uncorrupted nodes while maintaining their identities. In addition, the adversary can run a join-leave attack [25, 8], where it rejoins a constant (and small) number of corrupt nodes using fresh identities in order to compromise one or more committees. However, at any moment, at least a 2/3 fraction of the computational resources belong to uncorrupted participants that are online (i.e., respond within the network time bound)."

*)

(* at least an f < 1/2 fraction of its members belongs to honest nodes *)
let network_resiliency = 3                                                      (* [t] total faulty resiliency, [f] the probability of each node being corrupt is f = t/n *)
let shard_resiliency = 2                                                        (* (synchronous) committee resiliency *)
let network_corrupt_nodes = network_nodes / network_resiliency

(* each epoch consists of multiple iterations of consensus 
  "For a network of 1,800 nodes, epoch transition in OmniLedger [42] takes more than 1,000 seconds while it takes
less than 380 second for RapidChain. In practice, OmniLegder’s epoch transition takes more than 3 hours since the
distributed random generation protocol used has to be repeated at least 10 times to succeed with high probability." 

we store a reference block at the start of each epoch that contains the list of all of the nodes and their corresponding committees.
*)
let new_epoch () =
 ()

let listen (node:key) : txs = []

let new_block (txs:txs) : block = []

(* "all the messages that the leader or other nodes send during the consensus is signed by their public key and thus the sender of the message and its integrity is verified" *)
let check_msg (msg:msg) : unit = ()

let add_block (leader:node) = 
  check_block ();
  (* agree (); *)
  ()

(*  "run among only a small number of nodes (about 250 nodes), and the size of the message to agree is small (roughly 80
bytes), the latency of each round of communication is also small in practice (about 500 ms – see Figure 4–left)
resulting in a small ∆ (about 600 ms) and a small epoch latency"

"The source gossips Mi and its Merkle proof, for all 1 ≤ i ≤ κ, by sending a unique set of κ/d chunks (assuming κ is divisible by d) to each of its neighbors.
Then, they gossip the chunks to their neighbors and so on."

RapidChain creates a well-connected random graph for gossiping between nodes on a committee.

[Karp2000] Randomized Rumor Spreading *)
let multicast (src:key) (all:keys) (msg:msg) : unit = ()

exception Undef
let sign (src:key) (header:header) (tag:tag) : signature = raise Undef

let sign_multicast (src:key) (all:keys) (header:header) (tag:tag) : unit =
  multicast src all { signature = sign src header tag; header = header; tag = tag }

let chunk (block:block) : chunks = []

(* Information Dispersal Algorithms, IDA, IDA-Gossip, Gossiping large messages, multicast

"reduce the communication overhead and latency of P2P consensus on large blocks gossiped in each committee by roughly
3-10 times"

"Once an ECC-encoded message is dispersed in the network via IDA, honest nodes agree on the root of the Merkle tree
using the intra-committee consensus protocol to ensure consistency. Using the corresponding authentication path in the
Merkle tree sent by the sender, recipients can verify the integrity of all chunks and use a decoding mechanism to
recover the message"

"Each node who receives a message invokes the IDA-gossip protocol to sent the message to all other members of its committee."

"To implement our IDA-based gossiping protocol to gossip 2-MB blocks within committees, we split each block into 128
chunks and use the Jerasure library [3] to encode messages using erasure codes based on Reed-Solomon codes [59] with the
decoding algorithm of Berlekamp and Welch [10]."

"The probability that a message is not delivered to all honest nodes after it is gossiped using IDA-Gossip without sparsification is at most 0.1."

[Alon2004] Addendum to scalable secure storage when half the system is faulty *)
let chunk_counts = 128                                                          (* κ denote the number of chunks of the large message *)
let signature_size = 160 / 8                                                   (* ECDSA? 160 bits = 20 bytes *)
let chunk_size = block_size / chunk_counts                                      (* 1024*2/128 = 16KB ?? *)
let message_size = signature_size + chunk_size

let multicast_large (block:block) (nodes:keys) : unit =
  let chunks = chunk block in
  ignore chunks

let new_hash (block:block) : hash = raise Undef

let each = List.iter

let each_sign_multicast (all:keys) (header:header) (tag:tag) : unit =
  each (fun node -> sign_multicast node all header tag) all

(*  For our target network size of 4,000, we consider a committee size of 250 which results in an epoch failure
probability of less than 6 · 10−7
(i.e., time-to-failure of more than 4,580 years). *)
let hash_length = -1                                                            (* [h] is the length of a hash that depends only on the security parameter *)
let shard_constant = 20                                                         (* [c] is a constant depending only on the security parameter (in practice, c is roughly 20) *)
let shard_nodes = 250                                                           (* [m] shard size, committee size, m = c log n = O(log n) *)
let shard_count = network_nodes / shard_nodes                                   (* [k] 4000/250 = 16, k = n/m *)

(* Intra-committee consensus 

"synchronous consensus can be solved with t < n/2 using digital signatures."

"This protocol allows RapidChain to obtain an
intra-committee consensus with the optimal resiliency of 1/2, and thus, achieve a total resiliency of 1/3 with small
committees."

Since each member of C2 may receive different messages due to malicious behavior, it chooses the message with a frequency of at least 1/2 + 1.

a leader in C drives an intra-committee consensus, which requiresO(m^2 b) communication amortized on the block size, b

the leader sends the block to all the members of Cout using a fast gossiping protocol that we build based on the information dispersal algorithm (IDA) of Alon et al. [6, 5] for large blocks

"Since less than m/2 of the committee members are corrupt, the leader will be corrupt with a probability less than 1/2."

"Theorem 2. The protocol achieves safety if the committee has no more than f < 1/2 fraction of corrupt nodes.

Definition 3 (Honesty). A committee satisifies the honesty condition if the fraction of corrupt nodes in the committee
is strictly less than 1/2."

[Ren2017] Practical Synchronous Byzantine Consensus. https://allquantor.at/blockchainbib/pdf/ren2017practical.pdf *)
let peer_corrupt_ratio = 0.5                                                    (* [ϕ] denote the fraction of corrupt neighbors *)
let shard_corrupt_nodes = shard_nodes / shard_resiliency                        (* 250 / 2 = 125 *)
let leader_corrupt_probability = 0.49                                           (* the leader gossips two different messages in the same iteration with probability 0.49 *)

(* in our inter-committee routing protocol, 49% of the nodes do not participate in the gossip protocol (i.e., remain silent) *)
let node_corrupt_probability = 0.49

(* [ζ] a threshold ζ such that the probability of having more than ζ fraction corrupt neighbors is at most 0.1. For example, for m = 200 and f < 1/2, we set ζ = 0.63. *)
(* [δ] the distribution of corrupt nodes in the majority of the groups is within a δ fraction of the number of corrupt nodes in the initial set. *)
(* [α] fraction of all its bad parties to the groups such that the assignment corrupts maximum number of groups *)
(* [β] the fraction of strategies that the adversary ignores due to the step three rule *)
(* [ϵ] let nodes join and leave one-by-one in each round. Moreover, we assume that at any time during the protocol, the fraction of corrupt nodes to honest nodes is ϵ *)
let peer_corrupt = 0.63                                                         (* [ζ] *)
let peer_corrupt_probability = 0.1                                             (* probability of having more than ζ fraction corrupt neighbors is at most 0.1 *)

type event =
  | New                                                                         (* initialization *)
  | Msg of key * msg                                                            (* sender, consensus vote *)
  | Cross of key * tx                                                           (* cross-shard transaction *)
  | Tx of key * tx                                                              (* user, transaction *)
  | Chunk of key * chunk                                                        (* sender, block chunk *)

let same_headers_count (headers:headers) (header:header) : int = raise Undef

let headers_step (headers:headers) (step:step) : hash = raise Undef

let headers_safe (headers:headers) (step:step) : header = raise Undef

(*
all honest nodes who terminate in that iteration will output the same value, called the safe value. 

some honest nodes may terminate before others with a “safe value” that yet needs to be accepted by all honest nodes in future iterations before a transaction can be considered as committed.

A new proposal is safe if it does not conflict with any accepted value with a correct proof, if there is any. Thus, at iteration i, for all pending block headers, the leader proposes a safe value. For a new block, any value is considered safe while for a pending block of previous iterations, the value is safe if and only if it has a correct proof of at least m f + 1 votes (permanent or temporary from iteration i − 1). If there is no value with enough votes, then any value is safe. In Section 6.3, we prove that our consensus protocol achieves safety and liveness in a committee with honest majority.

We first show that all the honest nodes will accept all the pending blocks, or they have accepted them with the safe value before, as soon as the leader for the current block height is honest.

in all the rounds of iteration i or all iterations after i, no leader can construct a safe proposal for a different header other than Hi since he cannot obtain enough votes from honest nodes on a value that is not safe and thus create a m f +1 proof.

The m f + 1 echoes serve as the proof of why the node accepts Hi *)
let header_safe (header:header) : bool = raise Undef

let msg_check (msg:msg) (sender:key) : bool = raise Undef

(* the members of Cout choose a local leader using the current epoch randomness 

Assuming a random leader-election protocol exists,

At each iteration i, each committee picks a leader randomly using the epoch randomness.

[Bracha1985] An o(logn) expected rounds randomized byzantine generals protocol
[Ostrovsky1994] Simple and efficient leader election in the full information model
[Russell1998] Perfect information leader election in log∗ N + o(1) rounds
[King2006] Scalable leader election
[King2010] Breaking the o(n^2) bit barrier: Scalable byzantine agreement with an adaptive adversary
*)
let new_leader (shard:shard) : key = raise Undef               (* pick a member of `shards` indexed by `random` *)

(* the leader gathers all the transactions it has received (from users or other committees) in a block Bi *)
(* propose a safe value *)
let leader_do (node:node) : unit =
  assert (node.id.public = node.shard.leader)
  (* a new leader to propose a new block while re-proposing the headers of the pending blocks *)

  (* each committee will have an honest leader every two rounds in expectation *)

  (* The honest leader will send valid proposals for all the pending blocks to all nodes that is safe to propose and has a valid proof. *)

  (* the members of each committee in RapidChain record the hash of the current UTXO set in every block added to the committee’s blockchain {only leader??} *)

let check_tx (tx:tx) : bool = raise Undef
  (* After receiving a transaction, the nodes verify if a transaction is valid by checking (1) if the input is unspent; and (2) if the sum of outputs is less than the sum of the inputs. *)

(* 
Our consensus protocol consists of four synchronous rounds. 

First, the leader gossips a messages containing Hi and a tag in the header of the message that the leader sets it to
propose.

Second, all other nodes in the network echo the headers they received from the leader, i.e., they gossip Hi again with
the tag echo. This step ensures that all the honest nodes will see all versions of the header that other honest nodes
received in the first round. Thus, if the leader equivocates and gossips more than one version of the message, it will
be noticed by the honest nodes.

In the third round, if an honest node receives more than one version of the header for iteration i, it knows that the
leader is corrupt and will gossip H 0 i with the tag pending, where H 0 i contains a null Merkle root and iteration
number i.

Finally, in the last round, if an honest node receivesm f+1 echoes of the same and the only header Hi for iteration i,
it accepts Hi and gossips Hi with the tag accept along with all the m f + 1 echoes of Hi . The m f + 1 echoes serve as
the proof of why the node accepts Hi . 

Clearly, it is impossible for any node to create this proof if the leader has not gossiped Hi to at least one honest
node. If an honest node accepts a header, then all other honest nodes either accept the same header or they reject any
header from the leader. In the above scenario, if the leader is corrupt, then some honest nodes reject the header and
tag it as pending. 

... some honest nodes may terminate before others with a “safe value” that yet needs to be accepted by all honest nodes in future iterations before a transaction can be considered as committed. 10 4.2.3 Protocol Details At each iteration i, each committee picks a leader randomly using the epoch randomness.

If a node accepts a header, it will not gossip more headers since all nodes already know its vote. This will protect honest nodes against denial-ofservice attacks by corrupt leaders attempting to force them echo a large number of non-pending blocks. It is left to describe how the leader proposes a header for a pending block even if some honest nodes might have already accepted a value for it. 

A new proposal is safe if it does not conflict with any accepted value with a correct proof, if there is any. Thus, at iteration i, for all pending block headers, the leader proposes a safe value. For a new block, any value is considered safe while for a pending block of previous iterations, the value is safe if and only if it has a correct proof of at least m f + 1 votes (permanent or temporary from iteration i − 1). If there is no value with enough votes, then any value is safe. In Section 6.3, we prove that our consensus protocol achieves safety and liveness in a committee with honest majority.

We first show that all the honest nodes will accept all the pending blocks, or they have accepted them with the safe value before, as soon as the leader for the current block height is honest.
*)
let node_do (node:node) : event -> unit = function
  Msg (sender, msg) ->
    (* all honest nodes will vote for the proposed header for all the pending blocks, subsequently the will
  receive m f + 1 votes for them since we have m f + 1 honest nodes. Therefore, all honest nodes have finalized the
  block at the end of this iteration. *)
  
    if msg_check msg sender then (
      (* TODO: If the node sends two accepts for two different headers Hj and H'j, then the honest nodes will ignore the vote. *)
      node.headers <- msg.header :: node.headers;
      if sender = node.shard.leader then (      
        if headers_step node.headers msg.header.step = msg.header.root then (
          each_sign_multicast node.shard.nodes msg.header Echo
  
        ) else (                
          (* "if the leader equivocates and gossips more than one version of the message" *)
          (* "if an honest node receives more than one version of the header for iteration i, it knows that the leader is corrupt" *)
          node.shard.leader <- new_leader node.shard;
          if node.id.public = node.shard.leader then (
            let header = headers_safe node.headers msg.header.step in                    (* safe value; TODO: if no safe value *)
            sign_multicast node.id.public node.shard.nodes header Propose;
            leader_do node;
  
          ) else each_sign_multicast node.shard.nodes msg.header Pending
  
      )) else if same_headers_count node.headers msg.header > shard_corrupt_nodes then 
          (* Finally, in the last round, if an honest node receivesm f+1 echoes of the same and the only header Hi for
             iteration i, it accepts Hi and gossips Hi with the tag accept along with all the m f + 1 echoes of Hi . The m f + 1
             echoes serve as the proof of why the node accepts Hi .  *)
  
        (* If an honest node accepts a header, then all other honest nodes either accept the same header or they reject
          any header from the leader. In the above scenario, if the leader is corrupt, then some honest nodes reject the
          header and tag it as pending. *)
        each_sign_multicast node.shard.nodes msg.header Accept)

     (* TODO: runs in iterations with a new unique leader in every iteration *)

   else raise Undef
  
  | Tx (user, tx) -> 
    (* "wait for external users to submit their transactions" *)
    (* "batch and forward the transactions to the corresponding committee responsible for processing them" *)
    (* The nodes add the valid transaction to the next block they are accepting. *)
    (* RapidChain partitions the transactions based on their transaction ID among the committees which will be responsible for storing the transaction outputs in their UTXO databases. Each committee only stores transactions that have the committee ID as their prefix in their IDs *)
    (* TODO: check sender? *)
    if check_tx tx then (
      (* the total per-transaction communication and complexity of a consensus iteration is equal to O(m^2/b + m log n) *)
      (* consensus iteration *)      
      node.txs <- tx :: node.txs;
      if node.id.public = node.shard.leader && list_size node.txs >= block_txs then (
        let block = new_block node.txs in
        node.txs <- [];                                                         (* [[reset]] *)
        multicast_large block node.shard.nodes;
        let header = { step = node.step + 1; root = new_hash block } in
        sign_multicast node.id.public node.shard.nodes header Propose
     
    )) else raise Undef

  | Chunk (sender, chunk) -> raise Undef
    (* "The source gossips Mi and its Merkle proof, for all 1 ≤ i ≤ κ, by sending a unique set of κ/d chunks (assuming κ is divisible by d) to each of its neighbors.
    Then, they gossip the chunks to their neighbors and so on." *)

    (* a node may receive a message from the source that does not contain all of the digests needed to verify the validity of the gossiped message. *)

    (* Using the corresponding authentication path in the Merkle tree sent by the sender, recipients can verify the integrity of all chunks and use a decoding mechanism to recover the message *)    

  | Cross _ ->
    (* The leader sends txi to C i in via the inter-committee routing protocol, and C i in adds txi to its ledger. *)
    ()

  | New -> raise Undef
    (* The nodes belonging to the same sharding committee discover each other via a peer-discovery algorithm. *)
    (* a new RapidChain node initially downloads only the set of unspent transactions (i.e., UTXOs) from a sufficient
  number of committee members in order to verify future transactions. *)  

(* When we say a committee runs a protocol, we mean all honest members of the committee participate in an execution of the protocol. *)
let shard_do () : unit = ()
  (* To better alleviate the responsiveness issue of synchronous consensus, RapidChain runs a pre-scheduled consensus
among committee members about every week to agree on a new ∆ so that the system adjusts its consensus speed
with the latest average delay of the network. *)

  (* To maintain the desired failure probability, each committee in RapidChain runs a consensus in predetermined
intervals, e.g., once a week, to agree on a new committee size, based on which, the committee will accept
more nodes to join the committee in future epochs. *)

  (* RapidChain partitions the transactions based on their transaction ID among the committees which will be responsible for storing the transaction outputs in their UTXO databases. Each committee only stores transactions that have the committee ID as their prefix in their IDs *)

  (* both input committees successfully verify their transactions and send the new UTXOs to the output committee. *)
  
  (* The leader sends txi to C i in via the inter-committee routing protocol, and C i in adds txi to its ledger. *)

(* in our target network size of 4,000 nodes with 16 committees, roughly 99.98% of all transactions are expected to be cross-shard *)
let cross_shard_probability = 99.98 /. 100.

(* Improvement via Sparsification. 

"the source chooses a random subset of size d/(1−ϕ) of its neighbors and only sends the digest to
the node in that subset. We refer to this process as sparsification. As a result, a node may receive a message from the
source that does not contain all of the digests needed to verify the validity of the gossiped message."

the process of sparsification is not going to change the correctness and security of the
gossiping protocol and it increases the probability of failure slightly.

"by sparsification, the gossiper decrease his
chance of a successful gossip slightly but in return puts less communication burden on the nodes and network. Since
the gossip of the blocks are crucial to the system, we do not use sparsification for them"

However, users can use sparsification for their large transactions if the transaction is not time-sensitive. In case the
transaction fails to be gossiped correctly due to sparsification, the user can re-send the Merkle tree nodes later which
will happen with small probability.

[why blocks are more crucial than headers??]
*)
let sparsify = 3

(*  Improving Performance via Pipelining 
the throughput with pipelining (i.e., 7,384 tx/sec) with the throughput without pipelining
(i.e., 5,287 tx/sec) for n = 4, 000, showing an improvement of about 1.4x.
*)
let pipeline _ = raise Undef

(* Reconfiguration, bounded Cuckoo rule
[Awerbuch2006] Towards a scalable and robust DHT.
[Sen2012] Commensal cuckoo: secure group partitioning for large-scale services. *)
let reshard _ = raise Undef
  (* the range [0, 1) is partitioned into k regions of size k/n *)
  (* We define the age of a k-region as the amount of time that has passed after a new node is placed in that k-region.
     We define the age of a committee as the sum of the ages of its k-regions. *)

(* the user sends tx to a constant number of RapidChain nodes who route it to C.  *)
let user_submit (user:user) (tx:tx) : hash = raise Undef

let user_init () : user = {
  portals = get_portals () }

(* the size of a batch of cross-shard transactions for each committee for processing every block of size 2 MB is expected to be equal to 2 MB/16 = 128 KB *)
let batch_size = 128 * 1024

(* 
Cross-Shard Batching.
"the size of a batch of cross-shard
transactions for each committee for processing every block of size 2 MB is expected to be equal to 2 MB/16 = 128 KB"
 *)
let batch () : unit = ()
 (* batch_size *)

(* Let |B| denote the size of the blockchain. 
Storage Overhead. We measure the amount of data stored by each node after 1,250 blocks (about 5 million transactions)
are processed by RapidChain.
 *)

(* Assumption

total resiliency of ⅓??

However, at any moment, at least a 2/3 fraction of the computational resources belong to uncorrupted participants
that are online (i.e., respond within the network time bound).

Finally, we do not rely on any public-key infrastructure or any secure broadcast channel.

 *)

IMHO, this should be incorporated into a tech talk.

<3!!!