Cardano Updates

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

* feat: add a way to call a stage from outside the stage graph

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

* feat: integrate the mempool as a stage

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

* test: check the result of a rejected tx submission.

And fix: remove that tx id from the ack window. 

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

* refactor: remove the type parameter on CanValidateTxs 

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

* test: use traces to test the behavior of the mempool stage

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

* refactor: remove an incepted module

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

* refactor: remove an unnecessary method

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

* feat: wait for available transactions inside the tx submission initiator stage

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

* test: remove the sized mempool

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

* fix: implement the call of an input in the simulation builder

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

* refactor: use a specific message type for the mempool stage

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

* refactor: extract validation traits to the same module

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

* fix: prevent a memory leak with contramapped stage inside the txsubmission initiator

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

---------

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

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

Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module
parameters of `Utxo/Properties/PoV` with direct proofs.  The proofs are
organised as three layers:

+  Layer 1 — single-transaction coin equations

   `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)`

   `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)`

   Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin`
   across `+`, followed by `coin∘inject≗id` to strip each `inject`.  The
   consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel
   the mint term (from UTXO premise p₆ / SUBUTXO premise).

+  Layer 2 — sum-over-sub-transactions coin equations

   `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over
   `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from
   `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction.

   `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx`
   hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`)
   through the induction so each element's Layer-1 application has its
   `noMint` premise available.

+  Layer 3 — the two batch-level coin equations

   `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer
   `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by
   repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1
   top-level equation for the top-level summand, and substitute the Layer-2
   equation for the sub-transaction sum.

   The produced-side proof ends with a small associative-commutative shuffle
   (`reshape-top`) that reorders the top-level fields from
   `(outs + Donations + DirectDeposits) + TxFees` to the stated
   `outs + TxFees + Donations + DirectDeposits`.  The shuffle uses the same
   `swap-right` helper already used in `UTXO-V-mechanical`.

+  Supporting change

   Adds a small helper alias `noMintingSubTxs` at the top of the file to keep
   the sub-level mint-conservation hypothesis readable in the theorem
   statements.

All proofs typecheck under `--safe`.  The `UTXO-pov` placeholder remains;
this commit delivers the coin-balance infrastructure that the eventual
full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will
depend on.

From https://github.com/IntersectMBO/cardano-ledger at 226b002d5b5e83e24355f8a28ab214f3259eabda

Upgrade cardano-node from 10.6.2 to 10.7.1 and configure the V2LSM
ledger backend to reduce memory usage by storing UTxO data on disk
rather than in-heap. Also updates the cardano-playground config pin
and switches the config path to environments-pre/.

Detect Apple Silicon via sysctl hw.optional.arm64 (returns 1 even when
running the x86_64 build under Rosetta 2) and expose isAppleSilicon on
the environment object.

In AppUpdateStore.getUpdateInfo, look up the 'darwin-arm' key first on
Apple Silicon hardware, falling back to 'darwin' if absent (e.g. when
only one macOS variant is present in the feed).

In News.ts, expand the platform filter to match both 'darwin' and
'darwin-arm' target entries on Apple Silicon, so update news items are
not incorrectly hidden.

Replace hardcoded newsfeed.daedalus.io and newsfeed.daedaluswallet.io
with NEWS_URL / NEWS_HASH_URL webpack EnvironmentPlugin variables so
installers can be built pointing at a test server. Supports both http://
and https:// schemes; hostname, protocol, and port are parsed from the
full URL and forwarded to externalRequest.

fix(newsfeed): log error.message instead of raw Error object

fix(updater): log news fetch url on getNews error

fix(updater): respect pathname prefix in NEWS_URL and NEWS_HASH_URL

Extracting only hostname/protocol/port from NEWS_URL discarded any
path prefix (e.g. /daedalus/7.4). Export NEWS_PATH_PREFIX and
NEWS_HASH_PATH_PREFIX from urlsConfig and prepend them in getNews and
getNewsHash so URLs like https://cdn.example.com/daedalus/7.4 resolve
correctly to /daedalus/7.4/newsfeed/… and /daedalus/7.4/newsfeed-verification/….

feat(updater): add detailed debug logging to news fetch and update check flow

fix(updater): remove debug logging from news fetch and update store

Adds the drt (Daedalus Release Tool) Rust CLI, replacing the old
proposal-ui Haskell tool.

Commands:
  drt fetch-installers  — download unsigned installers from a Hydra eval
  drt sign              — GPG + macOS/Windows code signing via SSH hosts
  drt release           — hash, sign, upload to S3, push version JSON
  drt serve             — local HTTP mirror for end-to-end tester workflows
                          (generates newsfeed + verification files on the fly)

Nix:
  - Add crane + fenix flake inputs for Rust builds
  - Add perSystem/release-cli.nix (drt package + devShell + checks)
  - Add ops/ direnv environment for signing credentials

fix(drt/serve): bind IPv6 loopback alongside IPv4

Also bind [::1]:<port> so that `localhost` resolving to ::1 (common on
modern Linux/macOS) works without changing NEWS_URL to 127.0.0.1.
IPv6 bind is best-effort — silently skipped if unavailable.

refactor(drt): remove signing from release, add next-step hints

drt release no longer runs GPG signing — signing is a separate step
done via drt sign. Existing .asc files are still picked up and uploaded.

drt fetch-installers now hints: run drt sign
drt sign now hints: run drt release --bucket <bucket> --bucket-url <url>

fix(drt): skip -unsigned. installer files in all commands

fix(drt): split Darwin platform into DarwinArm/DarwinX86

Platform::Darwin was used for all .pkg files, causing aarch64-darwin
and x86_64-darwin installers to collide in HashMaps (last writer wins).

Split into DarwinArm (aarch64) and DarwinX86 (x86_64), with keys
darwin-arm and darwin in both version JSON and newsfeed output.
Platform detection now parses the full filename rather than just the
extension.

fix(drt/release): split bucket arg into bucket name + key prefix

Passing --bucket dripdropz-production/daedalus/7.4 used the full string
as the S3 bucket name, which contains slashes that are invalid in bucket
names. The AWS SDK then built a malformed canonical request, causing
SignatureDoesNotMatch errors.

Split --bucket on the first '/' into the actual bucket name and an
optional key prefix. All object keys (hash, filename, version JSON,
signatures) are stored under the prefix when one is present.

--bucket my-bucket              → bucket=my-bucket, prefix=
--bucket my-bucket/path/to/dir → bucket=my-bucket, prefix=path/to/dir

feat(drt/release): add --test flag to upload newsfeed stub to S3

Production newsfeeds are managed via GitHub; drt release should not
touch them. Add --test to opt in to uploading a generated newsfeed
stub and its SHA-256 verification file alongside the installers:

  newsfeed/newsfeed_<env>.json
  newsfeed-verification/<env>/<timestamp>.txt

Refactor serve::generate_local_newsfeed into a pub build_newsfeed
function that returns bytes + sha256 without touching the filesystem,
shared by both drt serve and drt release --test.

Add s3::upload_bytes for generic public-read byte uploads.

feat(drt/s3): skip upload if object already exists

Before uploading each installer (hash key + filename copy) or signature,
issue a HeadObject to check if the key is already present. If so, skip
the upload silently.

For hash-keyed objects the key IS the content hash, so existence implies
correct content — no re-download needed to verify.

This makes drt release idempotent: safe to re-run after a partial failure
without re-uploading multi-hundred-MB installer files.

feat(drt/fetch): retry downloads and skip already-verified files

Two improvements for unreliable Hydra connections:

- Retry: wraps each download in up to 5 attempts with exponential
  backoff (3 s, 6 s, 12 s, 24 s). Prints the error and delay before
  each retry so progress is visible.

- Resume: before downloading, checks if the destination file already
  exists and its SHA-256 matches the expected hash. If so, skips the
  download entirely. Re-running after a partial failure continues from
  where it left off rather than restarting from the beginning.

Also removes the unused human_size placeholder.

fix(drt/sign): skip already-signed files and resume partial signing

Add `unsigned_path()` and `is_already_code_signed()` to `Installer`.
In the signing loop, if the -unsigned companion exists and the signed
file is also present, skip (idempotent re-run). If the companion exists
but the signed file is missing (network error mid-SCP/pipe), fall
through and retry — macOS already skips the rename conditionally;
Windows now does the same.

fix(drt/release): simplify done output to version, json url, and installer urls

feat(drt/release): show newsfeed urls in done summary when --test is passed

fix(drt/release): remove duplicate path prefix in newsfeed summary urls

fix(drt/release): use exact timestamp and no-store cache-control for newsfeed uploads

Rounding updatedAt to the nearest hour meant re-runs within the same
hour overwrote the same verification file key in S3, but CloudFront
served the cached old hash causing a mismatch. Using actual milliseconds
gives each run a unique key. Add Cache-Control: no-store to both newsfeed
and verification uploads so CDN never serves stale copies.

Extract NEWS_PATH_PREFIX and NEWS_HASH_PATH_PREFIX from URL pathnames so
that a NEWS_URL like https://cdn.example.com/daedalus/7.3 resolves to the
correct newsfeed and verification paths instead of dropping the prefix.

Also export newsUrl from getNews for richer error logging, and log the
url, updatedAt, and hash values on fetch/verification failures.

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

Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module
parameters of `Utxo/Properties/PoV` with direct proofs.  The proofs are
organised as three layers:

+  Layer 1 — single-transaction coin equations

   `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)`

   `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)`

   Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin`
   across `+`, followed by `coin∘inject≗id` to strip each `inject`.  The
   consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel
   the mint term (from UTXO premise p₆ / SUBUTXO premise).

+  Layer 2 — sum-over-sub-transactions coin equations

   `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over
   `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from
   `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction.

   `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx`
   hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`)
   through the induction so each element's Layer-1 application has its
   `noMint` premise available.

+  Layer 3 — the two batch-level coin equations

   `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer
   `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by
   repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1
   top-level equation for the top-level summand, and substitute the Layer-2
   equation for the sub-transaction sum.

   The produced-side proof ends with a small associative-commutative shuffle
   (`reshape-top`) that reorders the top-level fields from
   `(outs + Donations + DirectDeposits) + TxFees` to the stated
   `outs + TxFees + Donations + DirectDeposits`.  The shuffle uses the same
   `swap-right` helper already used in `UTXO-V-mechanical`.

+  Supporting change

   Adds a small helper alias `noMintingSubTxs` at the top of the file to keep
   the sub-level mint-conservation hypothesis readable in the theorem
   statements.

All proofs typecheck under `--safe`.  The `UTXO-pov` placeholder remains;
this commit delivers the coin-balance infrastructure that the eventual
full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will
depend on.

Signed-off-by: Roland Kuhn <[email protected]>

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

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

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

From https://github.com/IntersectMBO/cardano-ledger at 226b002d5b5e83e24355f8a28ab214f3259eabda

Bumps [dompurify](https://github.com/cure53/DOMPurify) from 3.3.3 to 3.4.1.
- [Release notes](https://github.com/cure53/DOMPurify/releases)
- [Commits](https://github.com/cure53/DOMPurify/compare/3.3.3...3.4.1)

---
updated-dependencies:
- dependency-name: dompurify
  dependency-version: 3.4.1
  dependency-type: indirect
...

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