Cardano Updates

* Overhaul SPO and operator docs — restructure, rewrite, and consolidate

- Move all cardano-cli reference docs from get-started/infrastructure/cardano-cli/ to learn/cardano-cli/ with redirects
- Add secure transaction workflow page covering build/sign/submit pattern, mnemonic key derivation (cardano-signer, cardano-addresses), CIP-8 signing, CIP-100 governance metadata, and Calidus registration
- Rewrite security hardening page: nftables (replacing UFW), WireGuard for cross-datacenter relay/BP, fail2ban, systemd unit hardening
- Add SPO governance page: voting on hard forks and no-confidence actions, alwaysAbstain DRep delegation via reward account stake key, Calidus key identity
- Consolidate air-gap docs (cardano-airgap ISO + manual Ubuntu) into single page under learn/educational-resources/
- Move frankenwallet to learn/educational-resources/; add security tag to builder-tools
- Add monitoring section with overview (gLiveView) and Prometheus/Grafana pages moved out of relay-configuration/
- Add Docker security warning and nix build command to installing-cardano-node
- Fix broken redirects for deleted grafana-dashboard-tutorial and monitoring-gLiveView pages
- Fix relative links in monitoring-prometheus-grafana and stake-address-delegation

* Fix redirect targets to match actual doc id slugs

Redirect to paths must match the URL slug derived from frontmatter id,
not the filename. Also point deleted dynamic-block-forging and
rts-options-node redirects at running-cardano.

* Overhaul SPO and operator docs — restructure, rewrite, and consolidate

- Move all cardano-cli reference docs from get-started/infrastructure/cardano-cli/ to learn/cardano-cli/ with redirects
- Add secure transaction workflow page covering build/sign/submit pattern, mnemonic key derivation (cardano-signer, cardano-addresses), CIP-8 signing, CIP-100 governance metadata, and Calidus registration
- Rewrite security hardening page: nftables (replacing UFW), WireGuard for cross-datacenter relay/BP, fail2ban, systemd unit hardening
- Add SPO governance page: voting on hard forks and no-confidence actions, alwaysAbstain DRep delegation via reward account stake key, Calidus key identity
- Consolidate air-gap docs (cardano-airgap ISO + manual Ubuntu) into single page under learn/educational-resources/
- Move frankenwallet to learn/educational-resources/; add security tag to builder-tools
- Add monitoring section with overview (gLiveView) and Prometheus/Grafana pages moved out of relay-configuration/
- Add Docker security warning and nix build command to installing-cardano-node
- Fix broken redirects for deleted grafana-dashboard-tutorial and monitoring-gLiveView pages
- Fix relative links in monitoring-prometheus-grafana and stake-address-delegation

* additions

- replace all "current" mentions by a reference to a date and node version
- add openBlockPerf to monitoring section
- minor text additions

* more minor additions

* back out navbar changes

* update docs per TSC recommendations

---------

Co-authored-by: gufmar <[email protected]>
Co-authored-by: Tommy 🐙 <[email protected]>

Snapshot-merge: parents are (old leios-prototype tip, origin/master tip)
but tree equals origin/master byte-for-byte. The leios-prototype branch
ref moves forward without losing the historic prototype commits — they
remain reachable as ancestors via the merge's first parent.

The chunks of the recreation land as ordinary commits on top of this
one.

Mirrors the existing Maybe PerasCert pattern: a StrictMaybe LeiosCert
field on DijkstraBlockBodyRaw, a placeholder LeiosCert newtype
(ByteArray with derived EncCBOR/DecCBOR + NoThunks + NFData), a
lensMemoRawType-based leiosCertBlockBodyL accessor, the pattern
synonym extended with a third StrictMaybe LeiosCert argument, and the
CBOR codecs lengthened by one optional element each (EncCBOR raw list
3→4, DecCBOR record (const 3)→(const 4), EncCBORGroup inner list 2→3).
Test-side: ToExpr LeiosCert, Arbitrary LeiosCert, and the constraints
on the DijkstraBlockBody instances updated.

Only the Dijkstra era is Leios-enabled — earlier eras are untouched.
The original leios-prototype branch explored a richer shape on Conway
(Body with BodyInline / BodyCertificate plus EB-announcement and
certification flags on the Ledger Block) and then walked the flags
back in its final commit; this commit lands the simpler end state
directly on Dijkstra.

Refs: snapshot-merge first-parent ancestry preserves the originals;
the substantive ones were 0f9818960 (introduce Body type), 0c0368ea7
(remove EB-announcement / certification flags), 53517f2a7
(blockMayAnnouncedEb / blockCertifiesEb on Block).

Co-Authored-By: Claude Opus 4.7 <[email protected]>

Fix haddock urls

improve hardware wallet logging

  1. In-place dylib bundle — after the usb bundle step, do the same for
  node-hid/build/Release/HID.node so its Nix store paths resolve outside the
  sandbox.
  2. Exclude from deletion — added -not -path '*/node-hid/build/Release/*.node'
   so the cleanup loop doesn't wipe out the .node file that
  pkg-prebuilds/bindings needs.

remove existing app before installing new one on OSX

Initial attempt at the full adapt revealed that the original 670-line
@Test.ThreadNet.Leios@ test is tightly coupled to design choices that
were retired in the new prototype:

- @blockTxSizeSum@ pattern-matches on @SL.BodyInline@ and
  @SL.BodyCertificate@ — types replaced by the single
  @Maybe LeiosCert@ on @DijkstraBlockBody@ (L1 decision).
- It threads @resolveLeiosBlock@ before block application, relying
  on @ResolveLeiosBlock@ — the user's memory note flags this as
  "a hint, not a model"; the new design has no pre-application
  resolution step.
- It depends on @TraceThreadNet@ / @TraceThreadNetNode@ / @LeiosState@
  in @Test.ThreadNet.Network@ plus runtime tracer plumbing through
  the threadnet driver, mempool, and Leios kernel that were
  prototype-only additions.

Adapting the test isn't a compile-fix exercise — it's writing a new
test against the post-rebase design surface (header
@hbLeiosEbAnnouncement@ + body @Maybe LeiosCert@ + existing
@AddedToCurrentChain@ / @SwitchedToAFork@ trace events). That work
belongs in a follow-up chunk on its own. The stub keeps the
@cardano-test@ target compiling; the original is reachable through
@pre-rebase-orig@.

Refs: #1883 (Leios ThreadNet), #1906 (Leios: ThreadNet test suite),
#1971 (Test EB inclusion).

Co-Authored-By: Claude Opus 4.7 <[email protected]>

Carries C5's shelleyCumulativeTxBytes addition through to the
remaining record-construct sites that build the cardano-test target:

- ShelleyLedgerState construction in Test/Consensus/Shelley/Examples.hs
  (two example ledger states for the Praos vs TPraos protocol).
- The `Arbitrary (LedgerState (ShelleyBlock proto era) EmptyMK/ValuesMK)`
  generators in Test/Consensus/Shelley/Generators.hs.

Wires `Test.ThreadNet.Leios` into the cardano-test driver:
- Cabal: add to `other-modules` of `test-suite cardano-test`.
- Main.hs: import + `tests` reference.
- Add `bytestring`, `vector`, `directory`, `temporary` to
  `test-suite consensus-test` build-depends (needed by the new
  Test.LeiosDemo* test modules from C1).

The Leios test file itself is a placeholder for now; the full
threadnet adaptation is the next sub-chunk, which needs to bring
back the prototype's TraceThreadNet/TraceThreadNetNode/LeiosState
additions to unstable-diffusion-testlib first.

Co-Authored-By: Claude Opus 4.7 <[email protected]>

Snapshot-merge: parents are (old leios-prototype tip, origin/main tip)
but tree equals origin/main byte-for-byte. The leios-prototype branch
now sits on top of current upstream main while keeping all historic
commits reachable via the first-parent ancestry.

Original tip tagged locally as pre-rebase-orig.
See /home/ch1bo/.claude/plans/1-leios-should-not-transient-hummingbird.md.

Note: a plain 'git rebase origin/main' was tried first per a suggestion;
it hit immediate conflicts on files upstream-deleted-leios-modified, so
we fall back to the snapshot-merge approach. The 57 demo-tuning commits
remain reachable via the merge's first parent for manual cherry-pick or
direct-upstream-PR later.

Brings the leios-demo scripts back from pre-rebase-orig — pure
shell/Python/notebook content, no Haskell compile path:

- scripts/leios-demo/leios-november-demo.sh — end-to-end smoke run
- scripts/leios-demo/log_parser.py — analysis of node logs
- scripts/leios-demo/demo_analysis.ipynb, jupyter_utils.py — Jupyter
  notebook analysis flow
- scripts/leios-demo/build.nix, .envrc — local nix environment
- scripts/leios-demo/BUFFERBLOAT.md — TBF/netem tuning notes
- scripts/leios-demo/data/*.log* — recorded reference runs

The Haskell-side Test.ThreadNet.Leios bring-up (the other part of
chunk C7) is a separate commit; that file references many testlib
APIs that have evolved upstream and will need adaptation.

Refs: #1718 (NixOS setup), #1724 (Nixify demo), #1883, #1906
(ThreadNet); leiosdemo202510 / leiosdemo202511 direct-commit series.

Co-Authored-By: Claude Opus 4.7 <[email protected]>

Adds `shelleyCumulativeTxBytes :: !Word64` to `ShelleyLedgerState` (and
its ticked variant `tickedShelleyCumulativeTxBytes`), parallel to the
existing `shelleyLedgerLatestPerasCertRound`. Era-abstract — applies
to every Shelley-onwards ledger state. This is orthogonal to Leios
itself; Leios EB-sizing on Dijkstra is one user, but the accumulator
is generic.

Update protocol:
- Tick: preserve through, `tickedShelleyCumulativeTxBytes = shelleyCumulativeTxBytes`.
- Apply: `shelleyCumulativeTxBytes = tickedShelleyCumulativeTxBytes stBefore
    + sum (fromIntegral . (^. sizeTxF) <$> txs of block body)`, monotonically
    increasing across all blocks.
- Initial state and Byron→Shelley translation: 0.
- Era translation (Shelley→Allegra→...→Dijkstra): preserved.
- CBOR codec: encodeListLen 4→5, append `toCBOR shelleyCumulativeTxBytes`.
- Many record-construct/destructure sites (HasLedgerTables / CanStowLedgerTables /
  HFC era translations / SupportsProtocol forecast) updated in lock-step.

Tx-byte extraction uses the era-generic `Core.bbody (shelleyBlockRaw blk)
^. Core.txSeqBlockBodyL` + `^. Core.sizeTxF` — works uniformly across
all Shelley-onwards eras including Dijkstra's `Maybe LeiosCert` body.

Refs: #1988 (Add cumulative tx bytes to ledger state); the original
prototype put it on a `ShelleyLedgerLeiosState` extension type — this
version lifts it onto the existing `ShelleyLedgerState` directly since
the field is era-abstract and not Leios-specific.

Co-Authored-By: Claude Opus 4.7 <[email protected]>

Following the merge of CIP-159 PR #1197 (DirectDeposits keyed by
RewardAddress; applyDirectDeposits and applyWithdrawals refactored
through a shared applyToRewards fold) and the agda-sets cleanup
PR #1196 (Conway Equivalence.Map utilities moved into Ledger.Prelude),
this commit updates the Dijkstra CERTS preservation-of-value proofs
to compile against the new APIs.

Main changes:

+  Rename `ApplyWithdrawals-PoV` sub-module to `ApplyToRewards-PoV`,
   since it now houses lemmas for both withdrawals and direct deposits.

+  Add `getCoin-∪ˡ-overwrite` bridge lemma: `getCoin (❴ c , v ❵ ∪ˡ acc)
   ≡ v + getCoin (acc ∣ ❴ c ❵ ᶜ)`.  Encapsulates the
   listing-vs-replacement reconciliation between the new `❴ k , v ❵ ∪ˡ
   acc` form (used by `applyToRewards`) and the equivalent
   complement-restricted form used by the existing decomposition
   reasoning.

+  Factor `split-by-lookup` as a top-level lemma decomposing
   `getCoin acc` along a known lookup result.  Used by both
   `applyOne-pov` (subtraction) and the new `applyOne-pov-add`
   (addition).

+  Add the additive parallel: `applyOne-pov-add`,
   `foldl-applyOne-pov-add`, and `applyDirectDeposits-pov`.  Mirrors
   the existing withdrawal chain, sharing `getCoin-∪ˡ-overwrite` and
   `split-by-lookup`.

+  Strengthen the `setToList-Unique` module parameter with a
   `NetworkId` premise on the map's domain (the assumption no longer
   conflates withdrawals-specifically with general
   `RewardAddress ⇀ Coin` maps).

+  Replace the `∪ˡ-res-lookup-preserve` module parameter (which
   carried a no-longer-needed complement restriction on the right
   operand) with `∪ˡ-lookup-preserve`, stated against the new
   `❴ c , v ❵ ∪ˡ m` form.

+  Add a small top-level helper `∈-dom⇒¬lookup-nothing` to discharge
   the defensive `nothing` case of `foldl-applyOne-pov-add`.

+  Update `POST-CERT-pov` to use the new
   `applyDirectDeposits-pov`; the proof is `sym
   (applyDirectDeposits-pov ...)`.  The CERT-post step's own
   `mapˢ stake (dom dd) ⊆ dom rewards` premise is extracted from the
   pattern rather than threaded as a separate parameter, since the
   pre-CERT* state's `dom rewards` is not preserved across `CERT`
   trace steps (in particular by `DELEG-dereg`).

+  Update `sts-pov` and `CERTS-pov` signatures accordingly: add the
   `DirectDeposits`-`NetworkId` premise, drop the
   membership-of-deposits premise.

The proofs now typecheck on top of master.

Add `-with-rtsopts=--optimistic-linking` to iserv-proxy's cabalProjectLocal so the RTS option is embedded in `main.c` at link time and processed with `RtsOptsAll` — bypassing the OPTION_UNSAFE gate that command-line `+RTS --optimistic-linking -RTS` is subject to. The wrapper scripts under `overlays/{linux-cross,mingw_w64}.nix` no longer need to pass it at invocation. Gated on `impl(ghc >=9.14)` since earlier RTS versions don't recognise the flag.

Minimal-shape C4 per resolved design: the forge loop is *unchanged*.
No new arg to ForgeBlockArgs, no LeiosDb threading, no signature
change to forgeBlock. The new fields just need a default value at the
header/body construction sites:

- Praos.mkHeader::mkBhBodyBytes (the per-forge HeaderBody site):
  hbLeiosEbAnnouncement = SNothing. Dijkstra-era forging that wants
  to populate it will do so out-of-band by post-processing the
  forged block (TODO; not part of this chunk).
- Test generators that construct HeaderBody directly: same default.
- DijkstraBody side needs nothing here — mkBasicBlockBody already
  initialises dbbrLeiosCert = SNothing via the L1 changes.

Adds cardano-strict-containers to the unstable-protocol-testlib
build-depends so the generator can use SNothing.

Storage of forged EBs themselves lives in the concrete Shelley
implementation (planned, not in this chunk) — keeping the era-abstract
forge loop free of Leios.

Refs: #1832, #1888 (originals threaded LeiosDb through forging;
that shape is intentionally not adopted here).

Co-Authored-By: Claude Opus 4.7 <[email protected]>

The original leios-prototype kept Leios CDDLs in the cardano-blueprint
submodule rather than under ouroboros-consensus-cardano/cddl/. The
snapshot-merge to upstream main dropped the submodule pointer (main
has CDDLs in-repo). This commit re-adds the submodule pointer at
ebabbf18 (the prototype's pinned tip; current contents reachable via
git's `submodule.cardano-blueprint.url` config).

Upstream main's in-repo CDDLs at ouroboros-consensus-cardano/cddl/
are left intact for now; Leios CDDLs (LeiosNotify, LeiosFetch) live
in the submodule per the resolved design.

Voting wiring is mostly already in place from C1 (LeiosVoteState type
and LeiosNotify mini-protocol carry the vote payloads). Further
voting integration into the consensus voting flow is bundled into
later chunks where the voter logic actually runs.

Refs: #1963 (Leios: Prototype voting); leiosdemo202510 direct-commit
series for the CDDL drafts (reachable via the snapshot-merge ancestry).

Co-Authored-By: Claude Opus 4.7 <[email protected]>

- Extract shared TxBody fields into encodeSharedTxBody
- Add encodeSubTx and encodeSubTxBody for Tx SubTx DijkstraEra
- Encode requiredTopLevelGuards in sub-transaction bodies
- Pass MetadataFormat through encodeTxBody for sub-tx metadata

Co-Authored-By: Claude <[email protected]>