Publish site (#184)

Author: Arnaud Bailly

.github/workflows/ci.yaml

@@ -126,6 +126,7 @@ jobs:
     - name: 🏗️ Agda-to-HTML
       run: |
         nix develop --command bash -c ".github/workflows/scripts/agda-2-html.sh"
+
     - name: Publish Docusaurus build
       uses: actions/upload-artifact@v4
       with:
@@ -134,8 +135,50 @@ jobs:
         path: |
           html/*
 
+  build-pdf-report:
+    runs-on: ubuntu-22.04
+    steps:
+      - name: 📥 Checkout repository
+        uses: actions/checkout@v4
+
+      - name: 🔧 Massage markdown
+        run: |
+          cat site/docs/reports/tech-report-1.md|  sed -e 's/\/img/site\/static\/img/g' | sed -e 's/#scale50)/){ width=50% }/g' | sed -e 's/^#//g' > tech-report-1.md
+          cat site/docs/reports/tech-report-2.md|  sed -e 's/\/img/site\/static\/img/g' | sed -e 's/#scale50)/){ width=50% }/g' | sed -e 's/^#//g' > tech-report-2.md
+
+      - name: 📓 Build PDF
+        uses: docker://pandoc/latex:3.2.0
+        with:
+          args: >-  # allows you to break string into multiple lines
+            --pdf-engine=xelatex
+            -N
+            --standalone
+            --output=tech-report-1.pdf
+            tech-report-1.md
+
+      - name: 📓 Build PDF
+        uses: docker://pandoc/latex:3.2.0
+        with:
+          args: >-  # allows you to break string into multiple lines
+            --pdf-engine=xelatex
+            -N
+            --standalone
+            --output=tech-report-2.pdf
+            tech-report-2.md
+
+      - name: 📤 Upload PDF
+        uses: actions/upload-artifact@v4
+        with:
+          name: tech-reports
+          if-no-files-found: error
+          path: |
+            tech-report-*.pdf
+
   build-docusaurus:
     runs-on: ubuntu-22.04
+    needs:
+      - build-specification
+      - build-pdf-report
     steps:
       - name: 📥 Checkout repository
         uses: actions/checkout@v4
@@ -151,6 +194,18 @@ jobs:
         working-directory: site
         run: npm ci
 
+      - name: 📥 Download Agda specification
+        uses: actions/download-artifact@v4
+        with:
+          name: agda-specification
+          path: ./site/static/agda_html/
+
+      - name: 📥 Download PDF
+        uses: actions/download-artifact@v4
+        with:
+          name: tech-reports
+          path: ./site/static/
+
       - name: 🏗️ Build Docusaurus site
         working-directory: site
         run: |
@@ -164,6 +219,37 @@ jobs:
           path: |
             site/build/*
 
+  # FIXME: remove once merged
+  publish-staging-docs:
+    environment: 'staging'
+    runs-on: ubuntu-latest
+    needs:
+      - build-docusaurus
+    steps:
+      - name: 📥 Download Docusaurus build
+        uses: actions/download-artifact@v4
+        with:
+          name: docusaurus-build
+          path: ./site
+
+      - name: 🔑 Install SSH Key
+        uses: shimataro/ssh-key-action@v2
+        with:
+          key: ${{ secrets.SSH_KEY }}
+          known_hosts: 'just-a-placeholder-so-we-dont-get-errors'
+      - name: 🔍 Adding Known Hosts
+        run: ssh-keyscan -H ${{ secrets.STAGING_HOST }} >> ~/.ssh/known_hosts
+
+      - name: 🚅 Deploy with rsync
+        uses: burnett01/rsync-deployments@7.0.1
+        with:
+          switches: -avzr
+          path: site/
+          remote_path: /var/www/${{ secrets.STAGING_HOST }}/public_html
+          remote_host: ${{ secrets.STAGING_HOST }}
+          remote_user: ${{ secrets.SSH_USER }}
+          remote_key: ${{ secrets.SSH_KEY }}
+
   publish-docs:
     if: github.event_name == 'push' && github.ref == 'refs/heads/main'
     runs-on: ubuntu-22.04

.github/workflows/scripts/agda-2-html.sh

@@ -1,5 +1,8 @@
 #!/bin/bash
 rm -f html/*.md html/*.html
 agda --html --html-highlight=auto --css=Agda.css src/Peras/SmallStep.lagda.md
-for f in html/*.md; do pandoc $f -o ${f%.md}.html -s --css=Agda.css; done
+for f in html/*.md; do
+    pandoc $f -o ${f%.md}.html -s --css=Agda.css;
+    rm $f;
+done
 

README.md

@@ -6,6 +6,49 @@
 
 This repository is intended to host more or less formal specifications, experiments, models for the Ouroboros Peras protocol.
 
+## Roadmap
+
+- Complete proofs.
+    - Voting strings.
+    - Liveness of the protocol.
+    - Soundness of the executable specification.
+    - Synchronize with Praos formalization.
+    - Prepare a publication or online supplement.
+- Complete conformance suite.
+    - Tests for non-voting parts of the protocol.
+    - Serialization format and inter-process communication for testing third-party implementations.
+    - Package for easy installation and use.
+- Recommend parameter values.
+    - Seek and analyze stakeholder requirements, especially from partner chains.
+    - Develop a parameter-evaluation tool (based on the Markov-chain simulator) that provides a full set of impact metrics for a given set of parameters.
+- Reach out to stakeholders.
+    - Populate website with latest results.
+    - Online versions of all analysis, simulation, and visualization tools.
+    - Organize a stakeholder workshop and/or a Intersect Consensus Technical WG.
+        - Feedback on specification format.
+        - Feedback on conformance suite.
+        - Feedback on and refinement of the draft CIP.
+- Tooling fixes and enhancements
+    - Improve the usability, efficiency, and testing of the ΔQ software.
+        - Provide out-of-the-box and possibly interactive visualization.
+        - Provide faster numeric computations (e.g. using discretized CDFs and fast vector operations, possibly offloaded to GPU).
+        - Provide additional combinators (e.g., quantile-arrival time) for the DSL.
+    - Improve the protocol visualizer.
+        - Allow users to inject adversarial behavior or network disruptions (e.g., "split brain" scenarios).
+        - Make visualization scalable in the browser to long chains (i.e., hours of simulated block production) and large networks.
+    - Improve the prototype simulator.
+        - Add an efficient implementation suitable for large networks and long simulations.
+        - Create a simple DSL for inputting simulation scenarios for both honest and adversarial behavior.
+    - Improve the Markov-chain analyzer.
+        - Add a DSL for defining scenarios.
+        - Add visualization and analysis tools.
+    - Collaborate with higher-resolution network simulation efforts, potentially implementing Peras on them.
+        - PeerNet
+        - ce-netsim
+- Move from the "pre-alpha" to the "alpha" version of the protocol.
+    - Requires completion of the Peras paper.
+    - Formalize and implement the preagreement YOSO abstraction.
+
 ## Documentation
 
 * [Weekly updates](docs/weekly) provide regular "heartbeat" about the

infra/cloud-run.tf

@@ -39,6 +39,12 @@ resource "google_cloud_run_v2_service" "peras_server" {
       "managed-by" = "github-actions"
     }
   }
+
+  lifecycle {
+    ignore_changes = [
+      template, client, client_version
+    ]
+  }
 }
 
 resource "google_cloud_run_v2_service_iam_member" "noauth" {
@@ -59,4 +65,10 @@ resource "google_cloud_run_domain_mapping" "peras_server_domain_mapping" {
   spec {
     route_name = google_cloud_run_v2_service.peras_server.name
   }
+  lifecycle {
+    ignore_changes = [
+      metadata,
+      spec
+    ]
+  }
 }

infra/ssh_keys

@@ -0,0 +1,2 @@
+curry:ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIC8aDeQyneOJA8KJegRWsJyf7qWbyKet5j0GACCDw7KS
+root:ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIC8aDeQyneOJA8KJegRWsJyf7qWbyKet5j0GACCDw7KS

infra/staging.tf

@@ -0,0 +1,46 @@
+resource "google_compute_firewall" "allow-http-https" {
+  name    = "allow-http-https"
+  network = "default"
+
+  allow {
+    protocol = "tcp"
+    ports    = ["80", "443", "22"]
+  }
+
+  // Allow traffic from everywhere to instances with an http-server tag
+  source_ranges = ["0.0.0.0/0"]
+  target_tags   = ["staging"]
+}
+
+resource "google_compute_address" "staging-external-address" {
+  name = "staging-ip"
+}
+
+resource "google_compute_instance" "staging-vm" {
+  name         = "staging-vm"
+  machine_type = "n1-standard-1"
+  tags         = ["staging"]
+
+  allow_stopping_for_update = true
+
+  metadata = {
+    sshKeys = file("./ssh_keys")
+  }
+
+  boot_disk {
+    initialize_params {
+      image = "debian-cloud/debian-11"
+    }
+  }
+
+  network_interface {
+    network = "default"
+    access_config {
+      nat_ip = google_compute_address.staging-external-address.address
+    }
+  }
+}
+
+output "external-ip" {
+  value = google_compute_address.staging-external-address.address
+}

site/docs/intro.md

@@ -1,9 +1,106 @@
+---
+sidebar_label: 'Introduction'
+sidebar_position: 1
+---
+
 # What is Peras?
 
-Peras, or more precisely Ouroboros Peras, is an extension of [Ouroboros Praos](https://iohk.io/en/research/library/papers/ouroboros-praos-an-adaptively-secure-semi-synchronous-proof-of-stake-protocol/) that addresses one of the known issues of blockchains based on Nakamoto-style consensus, namely _settlement time_.
+Peras, or more precisely Ouroboros Peras, is an extension of [Ouroboros Praos](https://iohk.io/en/research/library/papers/ouroboros-praos-an-adaptively-secure-semi-synchronous-proof-of-stake-protocol/) that addresses one of the known issues of blockchains based on Nakamoto-style consensus, namely _settlement time_. Peras achieves that goal while being _self-healing_, preserving the security of Praos, and being light on resources.
+
+:::important
 
-:::warning
+This site documents the **pre-alpha** version of the protocol, which already provides strong guarantees of settlement bounds, adapts to fluctuating participation, and can recover from failures.
 
-Coming soon! We are working on providing documentation at various levels of details for Peras. Stay tuned.
+Research work is still ongoing to refine the protocol and provide even better guarantees in the face of high adversarial stake.
 
 :::
+
+## What is settlement?
+
+Recall that in Cardano, like in all Nakamoto-style consensus blockchains, new blocks are added to the chain in a probabilistic way. The protocol gives each _Stake-Pool Operator_ (SPO) the right to _forge_ a new block every slot depending on the amount of stake they represent, and the protocol parameters are defined in such a way that one new block is created every 20 slots. A newly forged block is then propagated across the network and adopted by other nodes following the _longest chain_ principle: when a given node receives a new chain, i.e. a chain extended with a new block, it adopts it as its own if and only if the new chain is longer than any other previously known chain.
+
+Because of the distributed, decentralized and probabilistic nature of the protocol, it's perfectly possible that two or more chains coexist simultaneously across the network:
+
+* More than one SPO can be elected to create a new block at approximately the same time,
+* Blocks take some time to reach all network nodes giving rise to the possibility of different nodes having different views of the best chain,
+* Nodes come and go,
+* Transactions included in blocks also need to travel across the network before reaching the SPO that will forge a block including them,
+* ...
+
+This phenomenon is known as _forking_: a node's current best chain can be superseded by a new best chain which is very similar but for the last few blocks. Short (eg. a couple of blocks long) forks happen all the time, and they are usually non-problematic: rolled back blocks will be mostly identical, including the same transactions perhaps distributed differently among blocks, or with minor differences. But they can be harmful: if an end-user takes a decision, for example to ship some goods to another user, based on some transaction that's later rolled back and never appears again because it was actually invalid, double-spending some UTxO, this opens up the possibility of fraud.
+
+Therefore, from the point of view of an end-user submitting to or depending on a specific transaction, the important question is: _When can they consider their transaction will never be rolled back_? In other words, when can they consider the transaction to be _settled_?
+
+In the context of this work, settlement is henceforth defined from an _observability_ perspective:
+
+> Settlement time is the duration after which a block (or transaction) added to node's best chain has a negligible probability of being rolled back because of a fork
+
+## What's current settlement value?
+
+It turns out giving a precise answer to this question is convoluted, and depends on various characteristics of the protocol, most notably the expected diffusion time (Δ) across the network, and assumptions about the fraction of _adversarial stake_. When reasoning about blockchain properties, the relative power between _honest_ nodes, i.e. the nodes that respect the protocol, and _adversarial_ nodes, i.e. the ones that can do whatever they want, is extremely important.
+
+Ouroboros Praos has been [proven to be safe](https://iohk.io/en/research/library/papers/ouroboros-praos-an-adaptively-secure-semi-synchronous-proof-of-stake-protocol/) up to 50% adversarial stake: as long as the adversary does not control majority of the stake, it guarantees various key properties of the chain which we can summarize informally by saying all honest nodes will ultimately agree on the same, honest, chain. However, this robustness comes at a price which is the time nodes have to wait to consider a block (therefore a chain) _settled_.
+
+In Cardano a node considers a block definitely _settled_, or _immutable_, once it is $k$ blocks behind the current tip of its best chain, where $k=2160$. Assuming average interblock arrival rate of 20 seconds, this means a block is settled after about 12 hours.
+
+### How is $k$ determined?
+
+The question of settlement time has been given a mathematically rigorous treatment in the paper [Practical Settlement Bounds for Longest-Chain consensus](https://iohk.io/en/research/library/papers/practical-settlement-bounds-for-longest-chain-consensus/), whose main findings can be summarized in the following picture.
+
+![Fork probability for 10% adversarial stake](/img/settlement-failure-probability.png#scale50)
+
+This graph reads as follows: assuming an adversarial stake of at most 10%, and a diffusion bound Δ of 5 seconds, the probability of a block being rolled back after a node has observed 20 blocks is 0.001%.
+
+If Δ drops to 2s, e.g. if we consider the network to be faster and more reliable, then this probability also drops to 0.0001%.
+
+On Cardano's mainnet, because of the much more stringent security requirements, we'll require a much lower failure rate of $2^60$. Assuming the adversary has at most 35% stake and huge _grinding power_, and network propagation delay $Δ=5s$, the same computation yields roughly the current value of $k$, i.e. a bit over 2000 blocks.
+
+### What happens in practice?
+
+In practice we know that _core nodes_, e.g.. block producing nodes or relays, seldom observe forks longer than 2 blocks. And most wallets, explorers, DApps, and other end-user facing systems provide feedback about transaction settlement under the name _number of confirmations_ which is exactly the same thing: the number of blocks past current best chain's tip of the block containing the transaction. A _number of confirmations_ higher than 10 is considered _high_.
+
+However, it's quite possible an adversary is "lurking in the shadows", building a _private chain_ and awaiting the best time to take over the network and roll back transactions which would have normally be considered safe. This idea of private chains or "selfish mining" has been detailed in the classical paper [Majority is not enough](https://arxiv.org/abs/1311.0243), and it is critical to address this problem to ensure the security of any decentralised blockchain. This explains why we observe such a difference between the theoretical settlement bound provided by the protocol, and the practically observed one.
+
+## How does Peras work?
+
+Peras exists to bridge that gap and make settlement bounds closer to practical values, e.g. to dramatically decrease the probability of a fork even after only a few blocks.
+
+The key idea of Peras is to use stake-based voting to _boost_ the weight of blocks on which a majority  of SPOs agree. The chain selection rule is then modified to select the _heaviest_ chain instead of the _longest_ one.
+
+### How does the protocol work?
+
+From a high-level perspective, the protocol works as follows:
+
+* At the beginning of each _round_, a randomly selected _committee_ of SPOs _vote_ for the block at a fixed depth from their current best chain tip, with each vote having a weight correlated to the SPO's stake,
+* Time is divided in fixed-length _rounds_ with a duration in the order of a few tens of slots,
+* The votes are broadcast to all nodes across the network,
+* If a node sees a _quorum_ of vote for the same block, it can issue a _certificate_ which _boosts_ the weight of this block,
+* Certificates are also diffused across the network on demand, to those nodes which don't have equivalent votes,
+* If a node does not receive a quorum for a round, either from votes or a certificate, it enters a _cooldown_ period during which any vote or certificate are _ignored_,
+  * A node exits cooldown after a fixed number of rounds, and starts voting again.
+  * When it enters cooldown, a block producer also appends the latest certificate to the block it forges.
+
+### What are the benefits?
+
+The exact effect of Peras depends on the values of various protocol parameters which are detailed in the [Technical Report](/docs/reports/tech-report-2). Based on the [recommendations](/docs/reports/tech-report-2#recommendations-for-peras-parameters) provided in the report
+
+> anyone seeing a transaction appearing in a block need wait no more
+> than two minutes to be certain whether the transaction is on the
+> preferred chain (effectively permanently, less than a one in a
+> trillion probability even at 45% adversarial stake) versus having
+> been discarded because of a roll back
+
+Importantly, Peras does not change the underlying security guarantees of Ouroboros Praos, and reverts to it in the event of a cooldown. Moreover, it adapts to fluctuating participation of SPOs and can recover from temporary "failures", e.g. if an adversary manages to temporarily reach a _quorum_, they only will be able to takeover the chain if they manage to maintain that superiority over time, otherwise the honest parties will take over.
+
+## Where to go from here?
+
+A lot more details about Peras protocol can be found in various places:
+
+* For detailed analysis of the protocol, please refer to [Technical Report #2](/docs/reports/tech-report-2)
+* For a formal description, refer to the [Agda Specification](pathname:///agda_html/Peras.SmallStep.html)
+* Conformance tests are available in the [Peras repository](https://github.com/input-output-hk/peras-design)
+* A live simulation of the protocol is available https://peras-simulation.cardano-scaling.org
+
+
+<!--  Localwords:  Peras Ouroboros Praos Nakamoto SPO observability
+ -->

site/docs/reports/index.md

@@ -0,0 +1,13 @@
+---
+sidebar_label: 'Reports'
+sidebar_position: 2
+---
+
+# Reports
+
+This page groups "reports" on the project's results.
+
+For convenience we provide PDF versions of technical reports:
+
+* [Technical report #1](/tech-report-1.pdf)
+* [Technical report #2](/tech-report-2.pdf)