Cardano Updates

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

The cancel() method previously used .catch() with a re-throw for non-AbortError rejections. Since the promise returned by .catch() was never consumed, this caused unhandled promise rejections.

Fixed by aborting the controller first, then attaching a no-op .catch() handler to silence the rejection. Any errors from the task remain accessible via the callback() method.

Signed-off-by: A-Chronicle <[email protected]>

Move six closed-form cert-deposit helpers from
src/Ledger/Dijkstra/Specification/Utxo.lagda.md to
src/Ledger/Dijkstra/Specification/Certs.lagda.md:

  + updateCertDeposit
  + updateCertDepositsStep  (new named extraction of the fold body)
  + updateCertDeposits
  + coinFromDeposits
  + depositsChange
  + newCertDeposits
  + refundCertDeposits

These helpers depend only on Certs-level definitions, so their natural
home is Certs.lagda.md.  Their placement in Utxo.lagda.md forced any
proof referencing them to take the larger TransactionStructure /
AbstractFunctions parameter set, blocking proofs in
Certs.Properties.PoV(Lemmas) (parameterised only by GovStructure) from
referring to them.

govProposalsDeposits stays in Utxo.lagda.md — it depends on GovProposal
from Gov.Actions, not on a Certs-level type.

Bundled bug fixes to updateCertDeposits:

  + Typo: DState.deposits was being set from the GState delta instead
    of the DState delta.

  + Fold direction: was foldr (right-to-left).  CERTS processes certs
    left-to-right via BS-ind's head-first decomposition.  Changed to
    foldl, matching Conway's left-to-right recursion and Dijkstra's
    own applyToRewards.  Counterexample under foldr:
    [delegate c d, dereg c (just d)] on a fresh credential should
    leave c ∉ deposits per CERTS, but foldr processes dereg first
    (a no-op) then delegate, ending with c ∈ deposits.

updateCertDepositsStep is the inner fold body extracted as a named
function so downstream proofs in Certs.Properties.PoV can state and
use a per-step pots equation about it.

Also: add HasCoin-UTxOState (Utxo.lagda.md) and HasCoin-LedgerState
(Ledger.lagda.md).  HasCoin-LedgerState sums UTxO state total, DState
rewards balance, and the three deposit pots via the hoisted
coinFromDeposits — the form needed to balance against the UTXO
batch-balance equation.

Closes #1208.

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

The Haskell code allows scaling an empty value, regardless of scalar size. We would return an error here, which is not correct. Every error case gets caught in the loop, so we can simply remove the extra check.

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

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

Explorer will only show its main UI when the store is fully loaded, this avoids timing issues such as loading the aggregator from the URL which may be overriden by init logic.

Add fallback loaders for `Provider` and `Suspense` to improve user experience during the loading phase.

streamline store initialization and state preloading logic

Consolidate state preloading with `getPreloadedStateFromLocalStorage` and introduce `getEmptyPreloadedState` for default states.

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

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

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

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