Cardano Updates

Add the statement stub for issue #414 as a CHAIN-level claim in a new
module Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded:

- gaDepositInPot: a governance-action deposit is still held in a chain state
- CHAINStar: reflexive-transitive closure of CHAIN over a list of blocks
- GADepositsEventuallyRefunded: every held GA deposit is eventually removed
  from the deposit pot once the chain progresses past its expiry epoch

The proof is left as future work ("coming soon"). Wire the module into the
Chain.Properties aggregator, list the claim in the properties index, and note
it in the changelog.

Bumps [modernc.org/sqlite](https://gitlab.com/cznic/sqlite) from 1.51.0 to 1.52.0.
- [Changelog](https://gitlab.com/cznic/sqlite/blob/master/CHANGELOG.md)
- [Commits](https://gitlab.com/cznic/sqlite/compare/v1.51.0...v1.52.0)

---
updated-dependencies:
- dependency-name: modernc.org/sqlite
  dependency-version: 1.52.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>

Bumps [golang.org/x/crypto](https://github.com/golang/crypto) from 0.52.0 to 0.53.0.
- [Commits](https://github.com/golang/crypto/compare/v0.52.0...v0.53.0)

---
updated-dependencies:
- dependency-name: golang.org/x/crypto
  dependency-version: 0.53.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: Tripura Repalle <[email protected]>

Bumps [golang.org/x/crypto](https://github.com/golang/crypto) from 0.52.0 to 0.53.0.
- [Commits](https://github.com/golang/crypto/compare/v0.52.0...v0.53.0)

---
updated-dependencies:
- dependency-name: golang.org/x/crypto
  dependency-version: 0.53.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

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

  The init tx pre-funds the head output with enough ADA to cover the
  largest possible ClosedDatum (all parties having contested). The
  previous calculation used N-1 contesters, but the datum can grow
  to N entries when every party contests. For a single-party head,
  N-1=0 so the pre-funded amount was computed with an empty contesters
  list, leaving 103,440 lovelace short; the wallet's ensureMinUTxO
  then topped up the contest output, which the strict
  mustPreserveHeadValue (H4) check on-chain correctly rejected.

Signed-off-by: Sasha Bogicevic <[email protected]>

  getAccumulatorHash (which runs a BLS12-381 multi-scalar multiplication)
  was called three times per snapshot: once in `sign`, once in
  `mkSeenSnapshot`, and once in `toJSON`. All three operate on the same
  HydraAccumulator value.

  Change HydraAccumulator from a newtype to a data type with a lazy
  _cachedHash field. The thunk is computed at most once per value via
  normal Haskell sharing — subsequent callers return the already-evaluated
  ByteString immediately.

Signed-off-by: Sasha Bogicevic <[email protected]>

Signed-off-by: Sasha Bogicevic <[email protected]>

  deposit.ak checks the head redeemer constructor index via raw CBOR
  arithmetic; if Increment ever shifts from index 0, deposits are
  permanently locked. The test catches that at build time.

Signed-off-by: Sasha Bogicevic <[email protected]>

  mustNotChangeVersion (H13) fires before mustBeValidSnapshot (H28) in checkClose
  because && evaluates left-to-right; setting closedVersion != openVersion always
  triggers H13 first.

Signed-off-by: Sasha Bogicevic <[email protected]>

  The field was superseded by accumulatorHash (KZG-based) and was never
  read or validated by the on-chain head validator.

Signed-off-by: Sasha Bogicevic <[email protected]>

  Three coverage gaps in the contract test suite are filled:

  - CloseAny: new test module exercising the NoThing → CloseAny redeemer
    path, including the unique on-chain snapshotNumber > 0 check (21
    mutations; signature/number failures all map to FailedCloseAny because
    that path wraps both checks in a single traceIfFalse).

  - CloseInitial: expanded from 2 to 15 mutations, adding the three
    CloseInitial-specific checks (snapshotNumber == 0, version == 0,
    accumulatorCommitment == G1 generator → FailedCloseInitial) plus the
    ten shared close checks (parties, headId, contestation period, validity
    bounds, minting, contesters, value, required signer).

  - ContestInc: new test module contesting with a commit-type snapshot
    (utxoToCommit = Just depositedUTxO), exercising the ToCommit
    accumulator commitment path that ContestDec (decommit path) left
    uncovered.

Signed-off-by: Sasha Bogicevic <[email protected]>

Signed-off-by: Sasha Bogicevic <[email protected]>

  The geq → == change in mustPreserveHeadValue prevents stuck-head griefing
  but requires the head output ADA to never need a wallet bump at Close or
  Contest time. Since ClosedDatum with N-1 contesters is larger than
  OpenDatum, compute minUTxO(ClosedDatum_{N-1}, V_tokens) at initTx and
  set that as the head output ADA. This ADA is returned to participants at
  fanout and remains stable through Increments (headAdaOverhead = headADA -
  utxoADA stays constant as both sides grow by deposit_ADA).

  Move InitTx out of prepareTxToPost (STM) into postTx (IO) so getPParams
  — a new TinyWallet field — can be called to fetch live protocol params
  for the min-UTxO calculation.

Signed-off-by: Sasha Bogicevic <[email protected]>

  Add CloseCommitUnused and CloseCommitUsed contract tests to cover the
  (ToCommit, True) and (ToCommit, False) branches of headAdaOverhead
  computation in closeTx, which were previously untested. Both new test
  suites include a healthy-tx property and a full mutation generator.

Signed-off-by: Sasha Bogicevic <[email protected]>

  mustPreserveHeadValue used geq (≥) rather than == for the Close and
  Contest transitions. This allowed a malicious contester to add extra ADA
  to the head output — a griefing attack where the added value would cause
  the fanout's strict == conservation check to fail, permanently locking
  the head.

  The geq was a defensive measure for datum-growth min-UTxO scenarios, but
  neither closeTx nor contestTx ever changes the head value (both call
  modifyTxOutDatum only), and using geq to "top up" would break the fanout
  anyway. The correct invariant is ==, which matches the spec.

  Add ContestIncreaseHeadValue mutation test to document the property.

Signed-off-by: Sasha Bogicevic <[email protected]>

  withCRSLookup only checked txOutReferenceScript (script hash) but not
  txOutAddress. An attacker could create a UTxO at any address, attach the
  legitimate CRS script as a reference, and provide malicious G2 identity
  elements as datum — bypassing the KZG membership check and fanning out
  arbitrary outputs after the contestation deadline.

  Fix: add addressCredential (txOutAddress resolved) == ScriptCredential
  expectedHash check. Since expectedHash is already compiled into the head
  validator, no new parameters are needed. Move CRS UTxO publishing to the
  CRS script address (which already always-fails) so the on-chain check is
  self-consistent. Update the test generator to match.

  Add WrongAddressCRS mutation tests to FinalPartialFanout, PartialFanout,
  and FanOut (the full fanout path had no CRS mutation coverage at all).

Signed-off-by: Sasha Bogicevic <[email protected]>

  When a UTxO is settled on-chain via Increment or Decrement before Close,
  its scalar remains in the snapshot's KZG accumulator but its value has
  already left (or entered) the head. Fanning out only the remaining UTxOs
  produces a subset membership proof, but the old on-chain check required
  isG1Generator(proof) — only true when the subset equals the full
  accumulator. This caused H39 FanoutUTxOHashMismatch for any CloseUsed
  scenario.

  Fix (two inseparable halves):

  1. Remove `&& isG1Generator proof` from headIsFinalizedWith and
     checkFinalPartialFanout. Fanout and final-partial-fanout now accept
     any valid subset membership proof.

  2. Replace the `geq` conservation check with strict equality using a new
     `headAdaOverhead :: Integer` field in ClosedDatum and
     FanoutProgressDatum. This field holds the fixed lovelace overhead in
     the head UTxO not attributable to any L2 UTxO (the min-UTxO cost set
     at CollectCom). It closes the security hole that geq would leave: a
     valid subset proof + >= would let an attacker leave value unaccounted.

  Off-chain: fanoutTx receives a separate utxoForProof argument (the full
  snapshot UTxO set including pre-settled ones) to rebuild the accumulator
  matching the ClosedDatum commitment, while the fanned-out outputs cover
  only the UTxOs whose values are still in the head. closeTx computes
  headAdaOverhead as lovelace(headInputValue) - lovelace(UTxOs currently
  in head), with case analysis on incrementalAction × (version ==
  openVersion). contestTx propagates it unchanged; partialFanoutTx threads
  it through FanoutProgressDatum.

  checkContest preserves headAdaOverhead so it cannot be altered after the
  initial Close. checkPartialFanout also preserves it across intermediate
  steps.

Signed-off-by: Sasha Bogicevic <[email protected]>