Cardano Updates

Bumps [docker/metadata-action](https://github.com/docker/metadata-action) from 6.0.0 to 6.1.0.
- [Release notes](https://github.com/docker/metadata-action/releases)
- [Commits](https://github.com/docker/metadata-action/compare/030e881283bb7a6894de51c315a6bfe6a94e05cf...80c7e94dd9b9319bd5eb7a0e0fe9291e23a2a2e9)

---
updated-dependencies:
- dependency-name: docker/metadata-action
  dependency-version: 6.1.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <[email protected]>

Bumps [docker/login-action](https://github.com/docker/login-action) from 4.1.0 to 4.2.0.
- [Release notes](https://github.com/docker/login-action/releases)
- [Commits](https://github.com/docker/login-action/compare/4907a6ddec9925e35a0a9e82d7399ccc52663121...650006c6eb7dba73a995cc03b0b2d7f5ca915bee)

---
updated-dependencies:
- dependency-name: docker/login-action
  dependency-version: 4.2.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <[email protected]>

Signed-off-by: jeluard <[email protected]>

Signed-off-by: Chris Gianelloni <[email protected]>

Signed-off-by: Hyperledger Bot <[email protected]>

Bumps [docker/setup-buildx-action](https://github.com/docker/setup-buildx-action) from 4.0.0 to 4.1.0.
- [Release notes](https://github.com/docker/setup-buildx-action/releases)
- [Commits](https://github.com/docker/setup-buildx-action/compare/4d04d5d9486b7bd6fa91e7baf45bbb4f8b9deedd...d7f5e7f509e45cec5c76c4d5afdd7de93d0b3df5)

---
updated-dependencies:
- dependency-name: docker/setup-buildx-action
  dependency-version: 4.1.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

Signed-off-by: Matthieu Pizenberg <[email protected]>

Adds the per-step and RTC-induction bridging lemmas that prove the actual `CertState` produced by a `CERTS` chain has the same three deposit pots (and hence the same `coinFromDeposits`) as the closed-form `updateCertDeposits` applied to the initial state and the cert list.  This is the cert-deposit half of the `LEDGER-pov` chain; combined with the `posNeg-deposits` cancellation identity, it closes the deposit-accounting equation against the UTXO batch-balance equation.

New proofs (PR branch):

+  `CERT-deposits-updateCertDeposit` in `Certs.Properties.PoVLemmas`.  Per-step, case-split on the `CERT` rule's eight `DCert` constructors; `refl` in seven cases, `POOL-rereg` discharged via the pool-deposit alignment invariant.

+  `CERTS-deposits-updateCertDeposits` in `Certs.Properties.PoV`.  RTC induction mirroring `CERTS-pov`.  Factored through `updateCertDeposit-list`, a pure pot-only `foldl` that is the rule-intrinsic counterpart of `updateCertDeposits`; the bridge `pots-updateCertDeposits` handles the inheritance of non-deposit `CertState` fields.

+  `CERTS-coinFromDeposits-updateCertDeposits`.  Coin projection of the main lemma, immediately usable by `LEDGER-pov`.

Both bridging lemmas are parameterised over (a) two deferred set/map facts (`∪ˡ-singleton-mem-≡`, `Is-just-isPoolRegistered⇒∈-dom`) to be discharged from the standard library; and (b) the pool-deposit alignment invariant `PoolDepositsAligned` plus, for the RTC sibling, its `CERT`-step preservation lemma — both follow by inspection of the `POOL` sub-rules.

Master-touching changes

+  **Bug fix in `updateCertDeposits`**.  Was setting `DState.deposits` to `depositsᵍ` (the `GState` delta) instead of `depositsᵈ`.  The `depositsᵈ` name was bound by destructuring but otherwise unused — almost certainly an unintended typo.

+  **Bug fix in `updateCertDeposits`**.  Was using `foldr`, processing certs right-to-left.  The `CERTS` rule processes certs left-to-right (via `BS-ind`'s head-first decomposition).  For non-commutative cert sequences this is unsound: e.g. `[delegate c keyDeposit, dereg c (just keyDeposit)]` for a fresh credential should end with `c ∉ deposits` per `CERTS`, but `foldr` (which processes the `dereg` on the fresh state first as a no-op, then the `delegate`) ends with `c ∈ deposits`.  Switched to `foldl`.  Conway's `updateCertDeposits` is recursive left-to-right (equivalent to `foldl`); Dijkstra's own `applyToRewards` uses `foldl`.

+  **Refactor**.  Extracted `updateCertDepositsStep` as a named function from `updateCertDeposits`' inner lambda, so that downstream proofs can state and use its per-step pots equation.

+  **Hoist**.  Moved `updateCertDeposit`, `updateCertDeposits`, `coinFromDeposits`, `depositsChange`, `newCertDeposits`, `refundCertDeposits` from `Utxo.lagda.md` to `Certs.lagda.md`.  These depend only on `Certs`-level definitions (`PParams`, `DCert`, `CertState`); the previous location forced any proof referencing them to take the larger `TransactionStructure` / `AbstractFunctions` parameter set, blocking placement of the bridging lemmas in `Certs.Properties.PoV{,Lemmas}`.  `govProposalsDeposits` remains in `Utxo.lagda.md` (depends on `GovProposal`).

PR-branch-only changes:

+  `Ledger.lagda.md`. Replaced the local `coinFromDeposit` (singular) with the hoisted `coinFromDeposits` (plural).  `HasCoin-LedgerState` has three summands: `getCoin(UTxOState) + rewardsBalance(DState) + coinFromDeposits(CertState)`.  Gov-action deposits are stored in `GState.deposits` (keyed by `returnAddr`'s stake credential) and are therefore already counted by the third summand.

Signed-off-by: akrepala <[email protected]>

* Enable filecoin storage via Blockfrost

Signed-off-by: Matthieu Pizenberg <[email protected]>

* Format server python code

Signed-off-by: Matthieu Pizenberg <[email protected]>

---------

Signed-off-by: Matthieu Pizenberg <[email protected]>

Signed-off-by: akrepala <[email protected]>

Signed-off-by: Matthieu Pizenberg <[email protected]>

Signed-off-by: Eric Torreborre <[email protected]>

feat: add an environment variable to control the metric export interval

Signed-off-by: Eric Torreborre <[email protected]>

Signed-off-by: akrepala <[email protected]>

Signed-off-by: Matthieu Pizenberg <[email protected]>

Signed-off-by: Chris Guiney <[email protected]>

Signed-off-by: akrepala <[email protected]>

- tray/wizard: implemented setup wizard framework and navigation
- tray/wizard: added notification permission verification flow
- tray: renamed application to AdderTray and updated bundle identity
- tray: implemented bulletproof tray icon synchronization and cache-busting
- tray: expanded recent events menu to 10 entries with explorer links
- output: implemented 'Log to File' functionality and added webhook tests
- macos: fixed native notification icons and Script Editor bug via bundle ID cycling
- ci: optimized workflows with caching and fixed cross-platform build dependencies
- hardening: resolved 30+ lint issues and 28+ architectural verification findings

Signed-off-by: Ales Verbic <[email protected]>