Cardano Updates

Step 4 of the LEDGER preservation-of-value plan (#1187).  Chains the
three lemmas already proved in steps 2-3 over the single ENTITIES
constructor:

  applyWithdrawals-pov  on (wdrls, r₀)
  CERTS-pov             on the inner ⟦ ... ,CERTS⦈ premise
  applyDirectDeposits-pov on (dd, r₁)

The resulting equation is the value-flow statement for the whole rule:

  getCoin s + getCoin (DirectDepositsOf Γ)
    ≡ getCoin s' + getCoin (WithdrawalsOf Γ)

ENTITIES-pov takes the two per-batch NetworkId witnesses as separate
arguments, mirroring extract-netId's output in the old #1190 LEDGER-pov
proof.  These witnesses are produced at the call site by the
SUBUTXOW/UTXOW step and threaded into ENTITIES-pov from there.

The module ENTITIES-PoV inherits and re-exports the three set/map
parameters of ApplyToRewards-PoV (∪ˡ-lookup-preserve,
sum-map-proj₂≡getCoin, setToList-Unique), to be discharged in a
follow-up.

Also adds a top-level Entities.Properties module that re-exports the
two property submodules, matching the existing Certs.Properties
convention.

- Refactored imports to streamline the usage of `completeTxWithFreshCostModels` across the codebase.
- Updated unit tests to reflect changes in cost model handling, including support for raw arrays and ordering of indexed cost model objects.
- Added new test cases to validate the rejection of improperly ordered cost model objects, ensuring robustness in transaction processing.

Cross from x86_64 to aarch64-linux currently breaks the
`useLocalGhcLib = true` slicing path.  Disable the cabal flavour of
the reinstallable-ghc-lib test on both the glibc and musl aarch64
multiplatform targets; native and other cross targets remain
enabled.

`qemu-arm` segfaults running `iserv-proxy-interpreter` when ghc
spawns iserv for the annotations TH eval, so the build can't
proceed past `Compiling Lib`.  The same chain works on
`aarch64-android-prebuilt` (qemu-aarch64), so the issue is specific
to the 32-bit ARM qemu / iserv interaction rather than something
haskell.nix can sidestep.

Disable on `isAndroid && isAarch32` — same shape as the existing
`th-dlls` guard.

Runs both applyTx (phase 1) and evaluateTransactionExecutionUnits (phase 2)
independently in a single LocalStateQueryExpr session, returning both results
via TxValidationResult.

cabal hashes per-package `extra-lib-dirs:` and `extra-include-dirs:`
into `pkgHashExtraLibDirs` / `pkgHashExtraIncludeDirs`.  If the user
puts them in `cabalProjectLocal` to point cabal at a C library that
lives outside the standard `lib/` layout (e.g. mingw-w64 import libs
under `bin/`), plan-nix records the corresponding `--extra-lib-dirs=`
/ `--extra-include-dirs=` flags in plan.json's `configure-args` — but
v2 wasn't pulling those flags through to the slice's own
`cabal.project`, so the slice's cabal recomputed the package's
unit-id without them, diverged from plan-nix, and downstream
consumers couldn't reuse the slice.

Three pieces:

1. `modules/package-options.nix`: new per-package `extraLibDirs` and
   `extraIncludeDirs` options.
2. `modules/install-plan/configure-args.nix`: extract
   `--extra-lib-dirs=PATH` and `--extra-include-dirs=PATH` from
   plan.json's `configure-args` into the new options.
3. `builder/comp-v2-builder.nix`: emit a `package <pkg>\n
   extra-lib-dirs: ...\n  extra-include-dirs: ...\n` block per
   sliced package in the slice's `cabal.project`.

Also update `test/th-dlls-minimal/default.nix` to demonstrate the
pattern: spell test-clib's lib dirs out in `cabalProjectLocal` so
plan-nix's `extra-lib-dirs:` matches the slice's, AND keep
`components.library.libs = [test-clib]` so haskell.nix's module
system can resolve the `extra-libraries: test-clib` entry in
test-lib.cabal (without it, eval fails with
"The Nixpkgs package set does not contain the package: test-clib").

Confirmed:
  * x86_64-linux ucrt64 th-dlls-minimal.build (was failing with
    `Cabal-4345 Missing (or bad) C library: test-clib`)
  * x86_64-linux musl64 githash.run, th-dlls.build
  * x86_64-linux native with-packages.run
  * x86_64-linux armv7a-android cabal-22.run, c-ffi.run

Addresses review feedback on #566: the mediator may answer a
keylist-update either inline in the same HTTP reply or asynchronously
as a separate inbound message, and the SDK should handle both.

updateKeyListWithDID now registers a MESSAGE listener before sending.
When Send resolves with a matching inline response that response is
used directly (path A); otherwise the method waits for the response to
arrive on the MESSAGE event (path B), racing against the existing 60 s
timeout. The response is matched by piuri and by a thread id equal to
either the outgoing message id or the registered peer DID.

Tests cover the async success path, a response threaded on the peer
DID, an async failure result, and a non-matching thid timing out.

Signed-off-by: Seydi Charyyev <[email protected]>

Step 3 of the LEDGER preservation-of-value plan (#1187).

These two lemmas describe the value flow through the per-transaction
withdrawal and direct-deposit handling that bracket the inner CERTS
step inside the new ENTITIES rule (#1201):

+  applyWithdrawals-pov: getCoin rwds ≡ getCoin (applyWithdrawals w r) + getCoin w
+  applyDirectDeposits-pov: getCoin (applyDirectDeposits d r) ≡ getCoin r + getCoin d

Both are proved by induction over setToList of the underlying
RewardAddress ⇀ Coin map, with a per-step lemma about applyOne (the
lambda body of applyToRewards) at each inductive step.

The withdrawal version requires the per-batch NetworkId witness and a
Unique-on-stake-projection invariant on the remaining fold list,
because truncating subtraction (_∸_) means an already-reduced balance
must never be revisited.  The direct-deposit version drops both --
addition is total and commutative, so a re-visit is harmless -- and
the resulting signature is correspondingly leaner.

The module ApplyToRewards-PoV is parameterised over three set/map
identities to be discharged in a follow-up:

+  ∪ˡ-lookup-preserve
+  sum-map-proj₂≡getCoin
+  setToList-Unique  (used only by applyWithdrawals-pov)

File location reflects the post-#1201 home of applyWithdrawals and
applyDirectDeposits: Entities.Specification.<...>, not
Certs.Specification.<...>.

Extract required claim keys from the presentation request's
input_descriptors.constraints.fields and forward them to
SDJWT.verify() during presentation verification. Previously
hardcoded to [], which meant @sd-jwt/core never enforced that
required claims were actually disclosed by the holder.

Fixes #366

Signed-off-by: Abhigyan Singh <[email protected]>

Adds a new local state query that runs applyTx against the current
ledger state and returns the raw result. The provisional implementation
queries the full EpochState and runs applyTx client-side; this will be
replaced by a dedicated node-side consensus query.

Exposed from Cardano.Api.Query alongside other queries.

From https://github.com/IntersectMBO/cardano-base at 9a18592565cf15b900329095d699997b763b6bd3

The previous flow assumed Send.run would resolve to the mediator's
keylist-update-response. In practice it always resolved to undefined:
DIDCommConnection.send returned the registered handler's result rather
than the parsed message, and the SDK never asked the mediator for an
inline reply. Per coordinate-mediation 2.0 the mediator only answers
synchronously when the request carries `return_route: "all"`, and
Mercury auto-attaches that header for the piuris in ReturnRouteProtocols
(packages/wasm/didcomm/src/Wrapper.ts) -- but keylist-update was never
on that list. So every keylist-update went out without return_route, the
mediator dispatched the response asynchronously, and the client never
observed it.

Add keylist-update to ReturnRouteProtocols, make DIDCommConnection.send
return the inline response, and rewrite updateKeyListWithDID to send the
message, race the call against a 60 s timeout, assert the response is a
Message with the expected piuri and a thid matching the outgoing id, and
validate the body via MediationKeysUpdateResponse (throws on any
non-success / non-no_change result).

Tests cover success, no_change, client_error, server_error, malformed
body, timeout, wrong piuri, wrong thid and a missing response. A guard
on ReturnRouteProtocols prevents the same kind of regression that
originally introduced this bug (PR #85).

Closes #391

Signed-off-by: Seydi Charyyev <[email protected]>

The plaintext 64-byte ed25519 scalar is now held in sodium_malloc'd
memory (MLockedSizedBytes 64) throughout its lifetime:
- locked against swapping (mlock)
- never moved by the GC
- zeroed on release via mlsbFinalize

ScrubbedBytes (GC-heap, moveable, swappable) is no longer used for
any secret key material.  The wrapping key (Argon2id output) remains
in ScrubbedBytes for now.

All public crypto operations are now IO (Either XPrvError X).  The
unsafePerformIO facade is gone except for:
- the two global IORef initialisations (runtimeKdfParamsRef, randomModeRef)
- encryptedDerivePublic (pure EC math, no secret key involved)

Callers of encryptedKeyMaterial receive a MLockedSizedBytes 64 and
are responsible for calling mlsbFinalize when done with it.

Adds cardano-crypto-class to library build-depends.

+  Add singleton/union/sum lemmas to Ledger.Prelude

   Foundational identities used by the Dijkstra preservation-of-value
   proofs (#1187) and likely useful elsewhere.  All are stated at the
   generic `A ⇀ Coin` (or `List A`) level and are independent of any
   ledger-era rule.

   Added definitions:

   +  ≡ᵉ-getCoin, getCoin-cong, indexedSumᵛ'-∪, res-decomp: lift the
      abstract-set-theory equational machinery (≡ᵉ, indexedSum-cong,
      indexedSumᵐ-∪) to the `getCoin` interface.
   +  getCoin-singleton, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom, ∪ˡsingleton0≡:
      left-biased union with a single-entry map, with the zero-valued
      specialisation that arises in DELEG-delegate / DELEG-dereg.
   +  sumConstZero, indexedSumL-proj₂-zero, setToList-∈: small list/set
      bookkeeping used by sumConstZero.
   +  sum-map-+, +-interleave: list-of-ℕ algebra that the eventual
      LEDGER-pov chain will use to interleave summands.
   +  dec-de-morgan: de Morgan rewrite for a decidable conjunction.

   No semantic change to any ledger rule.

+  Add Certs preservation-of-value lemmas for Dijkstra

   Step 2 of the LEDGER preservation-of-value plan (#1187).  In Dijkstra
   (post-#1201), CERTS is the plain reflexive-transitive closure of CERT,
   with withdrawal and direct-deposit handling having migrated to the
   surrounding ENTITIES rule.  Consequently the value-preservation
   statement for CERTS reduces to

      getCoin s ≡ getCoin s'

   This commit adds two new modules:

   +  Certs.Properties.PoVLemmas: the per-step lemma CERT-pov, with all
      four sub-rule cases (CERT-deleg DELEG-delegate, CERT-deleg
      DELEG-dereg, CERT-pool, CERT-gov).  The proofs use the
      singleton/union helpers now in Ledger.Prelude.
   +  Certs.Properties.PoV: the closure-level CERTS-pov, by induction on
      the reflexive-transitive closure using CERT-pov at each step.

   A one-line addition to Certs/Properties.lagda.md re-exports both new
   modules from the top-level Properties namespace.

   No parameterised wrapper modules.  Both lemmas are top-level
   definitions and threading-free for consumers.

Preliminary infrastructure for the LEDGER preservation-of-value proof (#1187).

LedgerState contains three coin-bearing components: the UTxO state (fees
and donations counted via the existing HasCoin-UTxOState instance), the
rewards balance in DState.rewards, and the three deposit pots (stake-key,
pool, DRep). The existing HasCoin-CertState instance only counts the
rewards balance; the deposit pots have to be added at the LedgerState
level for the LEDGER-pov equation to balance.

This commit:

+  Promotes coinFromDeposit from a where-bound helper inside
   calculateDepositsChange to a top-level definition, so the PoV proof
   (and any future consumer) can reference it directly.
+  Adds a HasCoin-LedgerState instance summing UTxO state coin, the
   rewards balance, and coinFromDeposit applied to the CertState.

No semantic change to LEDGER or any other rule.