Skip to content

Commit af95052

Browse files
committed
fix: merged main
2 parents 12b22d1 + 7aec979 commit af95052

File tree

703 files changed

+158417
-1181
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

703 files changed

+158417
-1181
lines changed

.github/workflows/conformance.yaml

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
name: "conformance"
2+
3+
env:
4+
ALLOWED_URIS: "https://github.com https://api.github.com"
5+
TRUSTED_PUBLIC_KEYS: "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ="
6+
SUBSTITUTERS: "https://cache.nixos.org/ https://cache.iog.io"
7+
REGISTRY: ghcr.io
8+
IMAGE_NAME: ${{ github.repository }}
9+
10+
on:
11+
pull_request:
12+
paths:
13+
- "leios-trace-hs/**"
14+
- "leios-trace-verifier/**"
15+
push:
16+
branches:
17+
- main
18+
paths:
19+
- "leios-trace-hs/**"
20+
- "leios-trace-verifier/**"
21+
22+
jobs:
23+
24+
trace-verifier:
25+
name: Leios trace verifier
26+
runs-on: ubuntu-latest
27+
steps:
28+
- name: 📥 Checkout repository
29+
uses: actions/checkout@v4
30+
- name: 🛠️ Install Nix
31+
uses: cachix/install-nix-action@v21
32+
with:
33+
nix_path: nixpkgs=channel:nixos-24.05
34+
install_url: https://releases.nixos.org/nix/nix-2.28.3/install
35+
extra_nix_config: |
36+
allowed-uris = ${{ env.ALLOWED_URIS }}
37+
trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }}
38+
substituters = ${{ env.SUBSTITUTERS }}
39+
experimental-features = nix-command flakes
40+
accept-flake-config = true
41+
- name: 🏗️ Build trace verifier
42+
run: |
43+
nix build --show-trace .#leios-trace-verifier
44+
- name: 🧪 Test trace verifier
45+
run: |
46+
nix run --show-trace .#test-trace-verifier
47+
- name: 🔬 Check example trace
48+
run: |
49+
nix run .#ols -- \
50+
sim leios \
51+
--leios-config-file data/simulation/config.default.yaml \
52+
--topology-file data/simulation/topo-default-100.yaml \
53+
--conformance-events \
54+
--shared-log-format JSON \
55+
--output-seconds 30 \
56+
--output-file sim.log
57+
nix run .#leios-trace-verifier -- \
58+
--config-file data/simulation/config.default.yaml \
59+
--topology-file data/simulation/topo-default-100.yaml \
60+
--trace-file sim.log \
61+
--idSut 0 \
62+
|| true # FIXME: Remove when simulations conform to spec.

.github/workflows/formal-spec-integration.yaml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,12 +46,15 @@ jobs:
4646
# Copy the HTML files
4747
cp -r formal-spec-html/* site/static/formal-spec/
4848
49+
<<<<<<< HEAD
4950
- name: 🔄 Enhance Agda documentation
5051
working-directory: site
5152
run: |
5253
# Process HTML files using the agda-web-docs-lib
5354
NODE_OPTIONS="--max-old-space-size=16384" npx agda-web-docs-lib process ./static/formal-spec ./agda-docs.config.json
5455
56+
=======
57+
>>>>>>> main
5558
- name: 🏗️ Build Docusaurus site
5659
working-directory: site
5760
run: |
Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
name: "simulation-docs"
2+
3+
env:
4+
ALLOWED_URIS: "https://github.com https://api.github.com"
5+
TRUSTED_PUBLIC_KEYS: "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ="
6+
SUBSTITUTERS: "https://cache.nixos.org/ https://cache.iog.io"
7+
REGISTRY: ghcr.io
8+
IMAGE_NAME: ${{ github.repository }}
9+
10+
on:
11+
pull_request:
12+
paths:
13+
- "simulation/docs/**"
14+
push:
15+
branches:
16+
- main
17+
paths:
18+
- "simulation/docs/**"
19+
20+
jobs:
21+
22+
sim-docs:
23+
name: Build documents via Ubuntu
24+
if: true
25+
runs-on: ubuntu-latest
26+
steps:
27+
- name: 📥 Checkout repository
28+
uses: actions/checkout@v4
29+
- name: 🛠️ Install system dependencies
30+
run: sudo apt-get install -y texlive-full gnuplot python3-pygments
31+
- name: 🏗️ network-spec.pdf
32+
run: |
33+
cd simulation/docs/network-spec/
34+
make
35+
- name: 🏗️ sim-realism.pdf
36+
run: |
37+
cd simulation/docs/
38+
make
39+
40+
sim-docs-via-nix:
41+
if: false
42+
name: Build documents via Nix
43+
runs-on: ubuntu-latest
44+
steps:
45+
- name: 📥 Checkout repository
46+
uses: actions/checkout@v4
47+
- name: 🛠️ Install Nix
48+
uses: cachix/install-nix-action@v21
49+
with:
50+
nix_path: nixpkgs=channel:nixos-unstable
51+
install_url: https://releases.nixos.org/nix/nix-2.18.8/install
52+
extra_nix_config: |
53+
allowed-uris = ${{ env.ALLOWED_URIS }}
54+
trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }}
55+
substituters = ${{ env.SUBSTITUTERS }}
56+
experimental-features = nix-command flakes
57+
accept-flake-config = true
58+
- name: 🏗️ network-spec.pdf
59+
run: |
60+
nix build --show-trace .#networkSpec
61+
- name: 🏗️ sim-realism.pdf
62+
run: |
63+
nix build --show-trace .#simRealism

Logbook.md

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,127 @@
11
# Leios logbook
22

3+
## 2025-05-16
4+
5+
### Trace verifier improvements
6+
7+
- Error handling, initial error reporting
8+
- Trace verification starting from other than initial state
9+
10+
### Informal review of Haskell simulator for Leios
11+
12+
We reviewed existing code and documents related to the Haskell simulator, and assessed its state of completeness. See also the discussion in [PR#353](https://github.com/input-output-hk/ouroboros-leios/pull/353).
13+
14+
- Statistics
15+
- ELOC: 17,035 lines
16+
- TODO: 51 lines
17+
- Comments 1437 lines
18+
- Organization
19+
- Some intertwining of concerns
20+
- Simulation
21+
- Data analysis
22+
- Visualization
23+
- Examples
24+
- Praos cleanly separated from Leios.
25+
- Leios specifics are concentrated in just three modules.
26+
- Code quality
27+
- Generally readable and well organized code.
28+
- Especially understandable by those already familiar with the Cardano codebase.
29+
- Most types and functions are not documented.
30+
- The best documentation is for the typed protocols.
31+
- Networking code is most mature, with few changes for many months.
32+
- Block management is also mature.
33+
- Only three tests in the test suite, and these do not relate to the protocol
34+
- `test_benchTopologyIsConnected`
35+
- `test_defaultConfigOnDiskMatchesDef`
36+
- `test_canParseConstantDistribution`
37+
- Design
38+
- Leios variants handled via pattern matching on sum types.
39+
- Moderately high fidelity treatment of TCP.
40+
- Faithful to Leios specification regarding input blocks, endorser blocks, votes, Praos blocks, CPU resources, and networking behavior.
41+
- Uses typed mini-protocols for blocks and votes in a unified manner
42+
- Some node operations are modeled as parallel threads.
43+
- The network is static, so the input topology needs to reflect a snapshot of a typical p2p network.
44+
- The fidelity of the network representation is greater than needed for SRL4 analyses.
45+
- No representation or modeling of transactions.
46+
- Essentially no representation of adversarial behavior, though there is one placeholder.
47+
- There is no provision for modeling network dynamism such as coming/going of nodes or communication disruptions.
48+
- "Full Short" Leios implementation is slightly out of sync with the recent v0.2 changes.
49+
- Implementation
50+
- Single threaded execution because of its reliance of `IOSim`.
51+
- Runs 40x slower than Rust simulator.
52+
- Simulations of 3000 nodes for one hour takes ~24 hours for high TPS.
53+
- Dependencies our the production Ouroboros packages and a few Cardano packages.
54+
- Does not account for CPU resources needed for ledger updates.
55+
- Documentation
56+
- The readme files (`README.md` and `simulation/README.md`) are slightly out of date.
57+
- The "Network Specification" document is terse but complete enough to be useful in comparing against the implementation. It is unclear how closely the implementation matches or if there are major gaps (aside from the to-do list in its header) in the documentation.
58+
- The "Simulation Realism" document mostly consists of figures, with some brief text introducing them and pointing out interesting features. The document is not complete enough to make a sound case for the realism of the simulation.
59+
- Evidently, the simulations were compared to graph-theory models of idealized behavior, but there does not seem to be documentation of this.
60+
- There is no high-level design documentation for the simulation itself.
61+
- Assessment
62+
- The trace logs currently fail the conformance tests in the Leios trace verifier.
63+
- Changes to the networking model would require great care and understanding.
64+
- Most prospective changes to the Leios protocol would only involve a small fraction of the codebase and would likely be straightforward.
65+
- Addition of memory pool and transactions is feasible but would likely take ~100-200 hours of labor.
66+
- Many aspects of transactions could leverage the existing network code and protocol patterns.
67+
- Understanding the details of the existing Praos memory pool and transaction diffusion would be critical to implementing Leios transactions in the simulation.
68+
- Major speedup or parallelization of execution might require a lot of effort, but the code should be profiled to identify easily mitigated hotspots.
69+
- QA on the network implementation would require detailed understanding of TCP and reverse-engineering requirements documents.
70+
71+
### Documentation housekeeping
72+
73+
We relocated the ancient report on Leios from `report/` to [docs/obsolete-report/](docs/obsolete-report/) in order to avoid confusing that the report still represents the Leios design. It does contain useful background information and design principles, however.
74+
75+
### Higher excess-capacity simulations
76+
77+
The transaction lifecycle simulations earlier this week and last week raised the question of whether the duplication of transactions in IBs was starving other transactions from ever being included in an IB, and hence never making it to the ledger. Those earlier simulations had at total IB capacity that was only modestly larger than the size of all of the transactions submitted during the course of the simulation.
78+
79+
To evaluate this hypothesis, we re-ran the experiment with IBs being produced at three times a higher rate, which leaves plenty of space in IBs for transaction duplication. The loss of transactions persists, indicating that the hypothesis was incorrect and that some other factor is preventing transactions from making it to the ledger.
80+
81+
- [Read-me file](analysis/sims/2025w20/)
82+
- [Results at 1x IB capacity](analysis/sims/2025w20/analysis1x.ipynb)
83+
- [Results at 3x IB capacity](analysis/sims/2025w20/analysis3x.ipynb)
84+
85+
| | |
86+
|---|---|
87+
| ![Temporal efficiency of Leios](analysis/sims/2025w20/plots3x/temporal-efficiency-bar.svg) | ![Temporal efficiency of Leios](analysis/sims/2025w20/plots3x/temporal-efficiency-timeseries.svg) |
88+
89+
90+
### Rust simulation
91+
92+
- Added `tx-start-time` and `tx-stop-time` parameters, to avoid effect of Leios's slow start or sudden termination on TX analysis
93+
- Added a new leios variant `full-without-ibs`. In this variant, there are no IBs; instead, EBs contain references to TXs directly.
94+
95+
## 2025-05-15
96+
97+
### Manually curated test cases for Leios trace verifier
98+
99+
We manually created test cases for checking the Leios trace verifier. These are indented to scrutinize the correct operation of `leios-trace-verifier`. Over time, this database of scenarios will be expanded.
100+
101+
- [Valid traces](/leios-trace-verifier/examples/valid/)
102+
- [Invalid traces](leios-trace-verifier/examples/invalid/)
103+
104+
These have been integrated into a new test suite, `test-trace-verifier`, and the CI.
105+
106+
## 2025-05-14
107+
108+
### Removed deterministic conformance testing
109+
110+
The non-deterministic, trace-based conformance testing in [leios-trace-verifier/](leios-trace-verifier/) has replaced the deterministic approach based on an executable specification. The folder [conformance-testing/](https://github.com/input-output-hk/ouroboros-leios/tree/47d9128219af214cec8dae17ee4fb461a8a52a87/conformance-testing) has been deleted after being archived via permalink.
111+
112+
## 2025-05-13
113+
114+
### Nix derivations and CI for trace verifier
115+
116+
The [Leios trace verifier](leios-trace-verifier/) has been added to the Nix infrastructure and the CI builds. Currently, the CI runs a short simulation and then checks its trace.
117+
118+
### Partial documentation of Haskell simulations
119+
120+
Two partially-drafted technical reports related to the Haskell simulations have been added to the Nix and CI builds:
121+
122+
- [Ouroboros Leios Network Specification](simulation/docs/network-spec/ReadMe.md)
123+
- [Ouroboros Leios simulation: building confidence in the performance results](simulation/docs/ReadMe.md)
124+
3125
## 2025-05-09
4126

5127
### Lifecycle and resource analysis of Rust simulations

analysis/sims/2025w20/.gitignore

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
plots1x/
2+
plots3x/

0 commit comments

Comments
 (0)