Cardano Updates

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

net-rs: added voting tracking for UI, added t22 threat emulation implementation

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

Implements Value builtins and Value type

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]>

Bundled patches per PR #1189 comment 4566013539. Each is minimal and
surgical; no semantic re-litigation of decisions outside the listed
ambiguities.

1. Appendix C.1 nonce example: 36-char value (decodes to 27 bytes) ->
   32-char value `AgICAgICAgICAgICAgICAgICAgICAgIC` (24 bytes, matching
   the spec-mandated nonce length). Fix applied to both the constant
   listing and the request-URL example.
2. URI format ABNF: split `key` into `request-key` and `response-key`
   productions. Adds `aead` to request side (referenced in §Methods
   AEAD envelope, was missing from grammar). Adds `response`,
   `walletKey`, `nonce`, `payload`, `signature`, `errorCode`,
   `errorMessage` to response side (every response URL produced under
   §Response signing or §Methods rejection uses these, previously
   unenumerated).
3. §Unknown-key policy: updated to reference both ABNF productions so
   the strict-reject rule applies symmetrically to wallets (rejecting
   request URLs with unknown `request-key`) and dApps (rejecting
   response URLs with unknown `response-key`).
4. §Callback host binding: `errorCode=-4 RedirectHostMismatch` envelope
   MUST be delivered to the `connect`-time persisted `redirect`, NOT to
   the offending request's `redirect`. Closes the cross-host phishing
   defeat where -4 would otherwise sink into the attacker's domain.
5. §signTx response: dApp MUST verify `result-json.commit` echoes the
   request `commit`; mismatch is `errorCode=-2`. Promotes the echo from
   advisory to load-bearing (defence-in-depth complement to the
   wallet's pre-render commit check).
6. §signTx response: `partialSign=true` witness-set merge semantics.
   dApp concatenates returned `vkey_witnesses` array to existing array
   under map key 0 of `transaction_witness_set`; non-vkey keys (1, 3,
   4, 5, 6, 7) follow array-append. Replace-semantics silently drops
   prior co-signer witnesses.
7. §Conway transaction body extraction: literal-bytes rule. Wallet MUST
   slice the source CBOR's element-index-0 byte range; MUST NOT
   re-encode. The chain's `tx_id` is BLAKE2b-256 over the source
   bytes; any wallet re-canonicaliser that differs from the dApp's
   source encoder breaks every downstream hash-pin. dApp supplies
   canonical Conway-era CBOR; wallets MAY reject non-canonical input.
8. §Conway tx body: reference encoders pinned. cardano-ledger
   (Haskell), pallas-codec (Rust), cardano-multiplatform-lib (JS/Rust)
   are the three named reference implementations. Conformance against
   any is sufficient.
9. §Response signing canonical form: port inclusion explicit. Include
   port iff it appears literally in URL authority; default ports MUST
   NOT be emitted. Keeps the canonical subject byte-deterministic
   across libraries that disagree on RFC 3986 §3.2.3 default-port
   omission.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

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]>