Merge branch 'main' into javierdiaz/trace-translator

Author: javierdiaz72

.github/workflows/leios-design.yaml

@@ -0,0 +1,99 @@
+name: "Build Leios Design PDF"
+
+on:
+  pull_request:
+    paths:
+      - "docs/leios-design/**"
+      - "nix/artifacts.nix"
+      - ".github/workflows/leios-design.yaml"
+  push:
+    branches:
+      - main
+    paths:
+      - "docs/leios-design/**"
+      - "nix/artifacts.nix"
+  workflow_dispatch: # Allow manual triggering
+
+permissions:
+  contents: read
+  actions: read
+
+# Prevent redundant workflow runs
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build-pdf:
+    name: "Build Leios Design PDF"
+    runs-on: ubuntu-latest
+    steps:
+      - name: 📥 Checkout repository
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 1
+
+      - name: 🛠️ Install Nix
+        uses: cachix/install-nix-action@v27
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+            accept-flake-config = true
+            extra-substituters = https://cache.iog.io
+            extra-trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+
+      - name: 🗂️ Setup Cachix for IOG cache
+        uses: cachix/cachix-action@v15
+        with:
+          name: iog
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+          skipPush: true
+
+      - name: 🏗️ Build PDF using Nix
+        run: |
+          echo "Building Leios Design PDF..."
+          nix build .#leiosDesignPdf -L
+          
+          # Verify the PDF was created
+          if [ ! -f result/leios-design.pdf ]; then
+            echo "Error: PDF file was not created"
+            exit 1
+          fi
+          
+          # Show file size and info
+          ls -lh result/leios-design.pdf
+          file result/leios-design.pdf
+
+      - name: 📊 Get PDF metadata
+        run: |
+          # Get basic file info
+          echo "PDF file size: $(stat -c%s result/leios-design.pdf) bytes"
+          echo "PDF creation date: $(stat -c%y result/leios-design.pdf)"
+          
+          # If pdfinfo is available, show more details
+          if command -v pdfinfo &> /dev/null; then
+            echo "PDF metadata:"
+            pdfinfo result/leios-design.pdf || true
+          fi
+
+      - name: 🚀 Upload PDF artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: leios-design-pdf-${{ github.sha }}
+          path: result/leios-design.pdf
+          if-no-files-found: error
+          retention-days: 30
+
+      - name: 📄 Add PDF info to job summary
+        run: |
+          echo "## 📄 Leios Design PDF Generated" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "✅ Successfully built PDF from markdown source" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "**File details:**" >> $GITHUB_STEP_SUMMARY
+          echo "- Size: $(stat -c%s result/leios-design.pdf) bytes" >> $GITHUB_STEP_SUMMARY
+          echo "- Generated: $(date -u '+%Y-%m-%d %H:%M:%S UTC')" >> $GITHUB_STEP_SUMMARY
+          echo "- Commit: \`${{ github.sha }}\`" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "The PDF is available as a workflow artifact named \`leios-design-pdf-${{ github.sha }}\`" >> $GITHUB_STEP_SUMMARY

analysis/markov/Linleios.lean

@@ -1 +1,5 @@
 import Linleios.Evolve
+
+/-!
+# Linleios: a Markovian model of Linear Leios
+-/

analysis/markov/Linleios/Evolve.lean

@@ -11,6 +11,9 @@ open Lean.ToJson (toJson)
 open Std (HashMap)
 
 
+/--
+Try to forge an RB in this substep, given the state and environment.
+-/
 def forgeRb {env : Environment} (state : State) : Outcomes :=
   let state' :=
     {
@@ -23,6 +26,9 @@ def forgeRb {env : Environment} (state : State) : Outcomes :=
   , ({state' with hasRb := false, canCertify := false}, 1 - p)
   ]
 
+/--
+Try to include a certificate in the latest RB being forged in this substep, given the state and environment.
+-/
 def certify {env : Environment} (state : State) : Outcomes :=
   if state.hasRb && state.canCertify
     then let p := env.pSpacingOkay
@@ -32,6 +38,9 @@ def certify {env : Environment} (state : State) : Outcomes :=
          ]
     else [(state, 1)]
 
+/--
+Try to forge an EB in this substep, given the state and environment.
+-/
 def forgeEb {env : Environment} (state : State) : Outcomes :=
   if state.hasRb
     then let p := 1 - env.pLate
@@ -41,6 +50,9 @@ def forgeEb {env : Environment} (state : State) : Outcomes :=
          ]
     else [(state, 1)]
 
+/--
+Try to vote for an EB in this substep, given the state and environment.
+-/
 def vote {env : Environment} (state : State) : Outcomes :=
   if state.hasRb
     then let p := env.pQuorum
@@ -50,13 +62,22 @@ def vote {env : Environment} (state : State) : Outcomes :=
          ]
     else [(state, 1)]
 
+/--
+Step forward to the next potential block.
+-/
 def step {env : Environment} : List (State → Outcomes) :=
   [@forgeRb env, @certify env, @forgeEb env, @vote env]
 
 
+/--
+Discard probabilities below the specified threshold.
+-/
 def prune (ε : Float) : Probabilities → Probabilities :=
   HashMap.filter (fun _ p => p > ε)
 
+/--
+Evolve state probabilities on step forward according the a transition function.
+-/
 def evolve (transition : State → Outcomes) : Probabilities → Probabilities :=
   HashMap.fold
     (
@@ -68,19 +89,32 @@ def evolve (transition : State → Outcomes) : Probabilities → Probabilities :
     )
     ∅
 
+/--
+Chain a sequence of transitions sequentially, evolving probabilities.
+-/
 def chain (transitions : List (State → Outcomes)) : Probabilities → Probabilities :=
   match transitions with
   | [] => id
   | (t :: ts) => chain ts ∘ evolve t
 
+/--
+Simulate the specified number of potential blocks, given a starting set of probabilities.
+-/
 def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat → Probabilities
 | 0     => start
 | n + 1 => let state' := prune ε $ chain (@step env) start
            simulate env state' ε n
 
+
+/--
+Compute the total probabilities of a set of states.
+-/
 def totalProbability (states : Probabilities) : Probability :=
   states.values.sum
 
+/--
+Compute the distribution of EB counts.
+-/
 def ebDistribution : Probabilities → HashMap Nat Probability :=
   HashMap.fold
     (
@@ -90,13 +124,19 @@ def ebDistribution : Probabilities → HashMap Nat Probability :=
     )
     ∅
 
+/--
+Format the distribution of EB counts as JSON.
+-/
 def ebDistributionJson : Probabilities → Json :=
   Json.mkObj
     ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩)
     ∘ (fun z => z.mergeSort (by exact fun x y => x.fst ≤ y.fst))
     ∘ HashMap.toList
     ∘ ebDistribution
 
+/--
+Compute the RB efficiency, given a set of states.
+-/
 def rbEfficiency (states : Probabilities) : Float :=
   let clock := states.keys.head!.clock
   let rbCount :=
@@ -106,6 +146,9 @@ def rbEfficiency (states : Probabilities) : Float :=
       states
   rbCount / clock.toFloat
 
+/--
+Compute the EB efficiency, given a set of states.
+-/
 def ebEfficiency (states : Probabilities) : Float :=
   let clock := states.keys.head!.clock
   let ebCount :=
@@ -115,6 +158,9 @@ def ebEfficiency (states : Probabilities) : Float :=
       states
   ebCount / (clock.toFloat - 1)
 
+/--
+Compute the overall efficiency, give a set of states.
+-/
 def efficiency (states : Probabilities) : Float :=
   let rb := rbEfficiency states
   let eb := ebEfficiency states

analysis/markov/Linleios/Probability.lean

@@ -2,18 +2,30 @@
 import Linleios.Util
 
 
+/--
+Number of stake pools.
+-/
 def nPools : Nat := 2500
 
+/--
+Compute a realistic stake distribution for the specified number of pools.
+-/
 def stakeDistribution (nPools : Nat) : List Float :=
   (List.range nPools).map (fun k => ((k + 1).toFloat / nPools.toFloat)^10 - (k.toFloat / nPools.toFloat)^10)
 
+/--
+Determine the distribution parameter that achieves the specified committee size.
+-/
 private def calibrateCommittee(committeeSize : Float) : Float :=
   let stakes : List Float := stakeDistribution nPools
   let f (m : Float) : Float :=
     let ps : List Float := stakes.map (fun s => 1 - Float.exp (- m * s))
     ps.sum - committeeSize
   bisectionSearch f committeeSize nPools.toFloat 0.5 10
 
+/--
+Compute the mean and standard deviation of the committee size, given the probability of a successful vote and a target committee size.
+-/
 private def committeeDistribution (pSuccessfulVote committeeSize : Float) : Float × Float :=
   let stakes : List Float := stakeDistribution nPools
   let m := calibrateCommittee committeeSize
@@ -22,6 +34,9 @@ private def committeeDistribution (pSuccessfulVote committeeSize : Float) : Floa
   let σ := (ps.map (fun p => p * (1 - p))).sum.sqrt
   ⟨ μ , σ ⟩
 
+/--
+Compute the probability of a quorum, given the probability of a successful vote, the target committee size, and the quorum fraction.
+-/
 def pQuorum (pSuccessfulVote committeeSize τ : Float) : Float :=
   let ⟨ μ , σ ⟩ := committeeDistribution pSuccessfulVote committeeSize
   1 - cdfGaussian (τ * committeeSize) μ σ

analysis/markov/Linleios/Types.lean

@@ -7,20 +7,44 @@ import Linleios.Probability
 open Std (HashMap)
 
 
+/--
+Represent probabilities as floating-point numbers.
+-/
 abbrev Probability := Float
 
-
+/--
+The constant parameters used for computing transitions.
+-/
 structure Environment where
+  /-- The active slot coefficient. -/
   activeSlotCoefficient : Probability
+  /-- The $L_\text{hdr}$ protocol parameter. -/
   Lheader : Nat
+  /-- The $L_\text{vote}$ protocol parameter. -/
   Lvote : Nat
+  /-- The $L_\text{diff}$ protocol parameter. -/
   Ldiff : Nat
+  /-- The probability that an RB occurs long enough after the previous RB so that an EB can be certified. -/
   pSpacingOkay : Probability
+  /-- The per-step quorum probability. -/
   pQuorum : Probability
+  /-- The probability that the EB and transaction data arrives too late to compute the ledger. -/
   pLate : Probability
+  /-- The fraction of adversarial stake. -/
   fAdversary : Float
 deriving Repr
 
+/--
+Create an environment.
+
+- `activeSlotCoefficient`: the active slot coefficient
+- `committeeSize`: the mean committee size
+- `τ`: the quorum fraction
+- `pRbHeaderArrives`: the probability that an RB header arrives before $L_\text{hdr}$ slots
+- `pEBValidates`: the probability that an EB is validated before $3 L_\text{hdr} + L_\text{vote} + L_\text{diff}$ slots
+- `pEbUnvalidated`: the probability that the EB and transaction data arrives too late to compute the ledger
+- `fAdversary`: the fraction of adversarial stake
+-/
 def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committeeSize τ pRbHeaderArrives pEbValidates pEbUnvalidated fAdversary : Float) : Environment :=
   {
     activeSlotCoefficient := activeSlotCoefficient
@@ -34,14 +58,25 @@ def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committee
   }
 
 
+/--
+The state of the chain's evolution.
+-/
 structure State where
+  /-- The number of potential RB oppurtunities. -/
   clock : Nat
+  /-- The number of RBs actually forged. -/
   rbCount : Nat
+  /-- The number of EBs certified. -/
   ebCount : Nat
+  /-- Whether an RB was forged in the current step. -/
   hasRb : Bool
+  /-- Whether an EB could be certified in the current step. -/
   canCertify : Bool
 deriving Repr, BEq, Hashable, Inhabited
 
+/--
+The genesis state starts when zero counts.
+-/
 theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
   constructor
   rfl
@@ -50,11 +85,16 @@ theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0
   rfl
 
 
+/--
+The active states and their probabilities.
+-/
 def Probabilities := HashMap State Probability
 deriving Repr, EmptyCollection
 
 instance : Inhabited Probabilities where
   default := (∅ : Probabilities).insert Inhabited.default 1
 
 
+/--
+An outcome is a list of new states and their probabilities. -/
 abbrev Outcomes := List (State × Probability)

analysis/markov/Linleios/Util.lean

@@ -1,4 +1,7 @@
 
+/--
+The error function.
+-/
 partial def erf (x : Float) : Float :=
   if x < 0
     then - erf (- x)
@@ -12,9 +15,15 @@ partial def erf (x : Float) : Float :=
       let t := 1 / (1 + p * x)
       1 - (a₁ * t + a₂ * t^2 + a₃ * t^3 + a₄ * t^4 + a₅ * t^5) * Float.exp (- x^2)
 
+/--
+The CDF for a normal distribution.
+-/
 def cdfGaussian (x μ σ : Float) : Float :=
   (1 + erf ((x - μ) / σ / Float.sqrt 2)) / 2
 
+/--
+A bisection search.
+-/
 def bisectionSearch (f : Float → Float) (low high : Float) (ε : Float) (maxIter : Nat) : Float :=
   match maxIter with
   | 0 => (low + high) / 2

analysis/markov/docbuild/.gitignore

@@ -0,0 +1 @@
+.lake