Cardano Updates

After direct-deposit application moved from LEDGER-V/SUBLEDGER-V into the
POST-CERT rule, the Certs preservation-of-value proofs needed to account for
the `getCoin (DirectDepositsOf Γ)` increase that POST-CERT now produces via
`rewards ∪⁺ directDeposits`.

Statement changes:
- POST-CERT-pov:  getCoin s ≡ getCoin s'
              →  getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s'
- sts-pov:        gains a `+ getCoin (DirectDepositsOf Γ)` term on the LHS
- CERTS-pov:      becomes the symmetric "consumed = produced" form
                  getCoin s₁ + getCoin (DirectDepositsOf Γ)
                  ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)

Structural changes:
- POST-CERT-pov and sts-pov move into the parameterized `Certs-Pov-lemmas`
  sub-module (alongside PRE-CERT-pov), since they now require a fourth
  module parameter:
    indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m'
  This is the natural ∪⁺ analogue of the existing `indexedSumᵛ'-∪` lemma for
  `∪ˡ` on disjoint domains, but unconditional because `∪⁺` adds (rather than
  drops) values at shared keys.  TODO: upstream to agda-sets.
- `Certs-PoV` (in PoV.lagda.md) gains the same parameter and forwards it.

CERT-pov and PRE-CERT-pov are unchanged: the CERT and PRE-CERT rules did
not change in this refactor.

Closes part of #1185.

Co-authored-by: Copilot Autofix powered by AI <[email protected]>

Now that the file lives at
`src-lib-exts/abstract-set-theory/Axiom/Set/Map/Extra.lagda.md`:

+ Update the top-level module declaration to
  `module abstract-set-theory.Axiom.Set.Map.Extra (th : Theory) where`,
  matching the rest of the abstract-set-theory subtree.
+ Replace `open import Ledger.Prelude` with explicit imports from
  `abstract-set-theory.Prelude` and stdlib modules. `src-lib-exts/`
  cannot depend on `Ledger.Prelude` (upward dependency).
+ Inline the five-line `_≢ᵐ_` definition that previously lived in
  the standalone `Extra.agda`, and delete `Extra.agda`.
+ Convert the file to literate-markdown formatting with brief
  section prose; the module body is otherwise unchanged.
+ Update the single downstream caller
  (`Ledger.Conway.Conformance.Equivalence.Deposits`) to import from
  the new location.

Closes #1194

A deep-link wire protocol so native mobile dApps can ask an installed
Cardano wallet to perform CIP-30 operations (signTx, signData, ...)
over the OS URL-handling mechanism: no relay server, no embedded
WebView, no QR, no WebSocket. Addresses CPS-0010 for the
mobile-native dApp shape.

Reference implementations: Aegis (dApp) + Yuti (wallet), both from
Flux Point Studios.

Discussions:
  - https://forum.cardano.org/t/cip-proposal-mobile-deep-link-signing-for-native-dapps-cip-30-extension/154561
  - https://github.com/cardano-foundation/CIPs/pull/1189

Four internal ByteString allocations held the raw 128-byte extended
private key (ed25519 scalar || public key || chain code) in memory
without guaranteed zeroing on GC.  Switch them to ScrubbedBytes so
the memory package zeroes the pages when they are collected.

  - keyMaterialFromLegacyBytes: avoids an intermediate full :: ByteString
    carrying all 128 bytes; slices secret/pub/cc directly from ScrubbedBytes
  - legacyMaterialFromSecret / legacyMaterialFromMasterKey / legacyDerivePrivate:
    type annotations changed from ByteString to ScrubbedBytes so B.allocRet
    allocates scrubbed pages from the start

No public API or serialisation changes.

Two fixes for the dummy-ghc-info still-failing matrix at eval 1507:

* lib/dummy-ghc.nix — wasm (wasi32 / wasm32) gained an interpreter and
  dynamic RTS ways in GHC 9.12+.  Real cross GHC for 9.12+ wasm now
  reports `Tables next to code: NO`, `Have / Use interpreter: YES`,
  and `RTS ways: v debug debug_dyn dyn`.  Branch the existing
  ghcjs/wasm case on `versionAtLeast ghc.version "9.12" &&
  targetPlatform.isWasm`; older wasm and all ghcjs keep the legacy
  stage-1-without-interpreter values.

* test/dummy-ghc-info/default.nix — `mktemp` the diff-output file
  rather than hard-coding `/tmp/dummy-vs-real.diff`.  The darwin
  sandbox refuses writes to `/tmp/`, so the previous code errored on
  permission-denied before printing the actual "diverges from real"
  block, making darwin failures look mysterious in CI.  All the
  ghc9124/ghc984 ghcjs and ghc967/9124/9141 native darwin failures
  were just this — they pass once the diff write target is writable.

Verified on linux-0 against eval 1507's still-failing matrix:

  PASS aarch64-darwin ghc9124 ghcjs / native
  PASS aarch64-darwin ghc9141 native / wasi32
  PASS aarch64-darwin ghc967  native
  PASS aarch64-darwin ghc984  ghcjs / native
  PASS x86_64-darwin  ghc9124 ghcjs / native
  PASS x86_64-linux   ghc9124 wasi32
  PASS x86_64-linux   ghc9141 wasi32

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

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

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

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