Cardano Updates

mkdocs .md files weren't being generated even when .lagda.md files changed.

* Add utxo0 binding in UTXOW

For consistency with SUBUTXOW

* Add missing premises

* Improve tc time of Utxo.Computational

mkdocs .md files weren't being generated even when .lagda.md files changed.

For consistency with SUBUTXOW

* Remove DepositsChange

Calculate deposit changes from CertState and certificates in the tx

---------

Co-authored-by: William DeMeo <[email protected]>

UTxOEnv now carries the pre-batch CertState directly rather than a
precomputed DepositsChange, so the LEDGER computational instance no
longer needs separate environments for the valid and invalid cases.
The two old builders (utxoΓ-valid : CertState → CertState → UTxOEnv,
utxoΓ-invalid : UTxOEnv) collapse into a single

   utxoΓ : UTxOEnv
   utxoΓ = ⟦ slot , pparams , treasury , utxo₀ , certState
           , allScripts , RewardsOf certState ⟧

with certState (= the pre-batch state) used in both the LEDGER-V and
LEDGER-I cases.  This resolves the [NotInScope] error from
calculateDepositsChange (which no longer exists) and removes the
vestigial CertState → CertState arguments to utxoΓ-valid that were
unused after the refactor.

The completeness side gets one small additional change: the implicit
argument order in the LEDGER-V destructuring is reorganised to match
the constructor's declared order
   {utxoState₁ , govSt₁ , certSt₁ , certSt₂ , govSt₂ , utxoSt₂}
so the subsequent computeSubledgers / computeEntities / computeGov /
computeUtxow pattern matches against the right intermediate states.

Also adds a "Design Note: Cert-State Threading and Deposit Accounting"
subsection to Utxo.lagda.md explaining the rationale for the
refactor.  Key points:

+  The UTXO rule has been promoted from a consumer of CertState data
   to a secondary executor of certificate accounting:
   updateCertDeposit recomputes the deposit evolution that the
   CERT/ENTITIES rules also produce as part of their operational
   semantics.
+  The same certificate-deposit logic now exists in two places --
   inside the DELEG/POOL/GOVCERT sub-rules of CERT, and inside
   updateCertDeposit in Utxo.lagda.md.
+  Any drift between the two is a soundness problem, since it would
   admit transactions whose UTxO-side balance equation accepts but
   whose actual CertState evolution doesn't balance.  The note states
   the consistency obligation as a lemma to be discharged alongside
   LEDGER-pov.

UTxOEnv now carries the pre-batch CertState directly rather than a
precomputed DepositsChange, so the LEDGER computational instance no
longer needs separate environments for the valid and invalid cases.
The two old builders (utxoΓ-valid : CertState → CertState → UTxOEnv,
utxoΓ-invalid : UTxOEnv) collapse into a single

   utxoΓ : UTxOEnv
   utxoΓ = ⟦ slot , pparams , treasury , utxo₀ , certState
           , allScripts , RewardsOf certState ⟧

with certState (= the pre-batch state) used in both the LEDGER-V and
LEDGER-I cases.  This resolves the [NotInScope] error from
calculateDepositsChange (which no longer exists) and removes the
vestigial CertState → CertState arguments to utxoΓ-valid that were
unused after the refactor.

The completeness side gets one small additional change: the implicit
argument order in the LEDGER-V destructuring is reorganised to match
the constructor's declared order
   {utxoState₁ , govSt₁ , certSt₁ , certSt₂ , govSt₂ , utxoSt₂}
so the subsequent computeSubledgers / computeEntities / computeGov /
computeUtxow pattern matches against the right intermediate states.

Also adds a "Design Note: Cert-State Threading and Deposit Accounting"
subsection to Utxo.lagda.md explaining the rationale for the
refactor.  Key points:

+  The UTXO rule has been promoted from a consumer of CertState data
   to a secondary executor of certificate accounting:
   updateCertDeposit recomputes the deposit evolution that the
   CERT/ENTITIES rules also produce as part of their operational
   semantics.
+  The same certificate-deposit logic now exists in two places --
   inside the DELEG/POOL/GOVCERT sub-rules of CERT, and inside
   updateCertDeposit in Utxo.lagda.md.
+  Any drift between the two is a soundness problem, since it would
   admit transactions whose UTxO-side balance equation accepts but
   whose actual CertState evolution doesn't balance.  The note states
   the consistency obligation as a lemma to be discharged alongside
   LEDGER-pov.

Calculate deposit changes from CertState and certificates in the tx

Calculate deposit changes from CertState and certificates in the tx