Cardano Updates

Signed-off-by: Akhil Repala <[email protected]>

After moving direct-deposit application from LEDGER-V into POST-CERT,
CERTS-pov now produces a symmetric "consumed = produced" equation:

  getCoin s₁ + getCoin (DirectDepositsOf Γ)
  ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)

Thread the direct-deposit term through the LEDGER-pov proof:

* SUBLEDGERS-certs-pov gains "+ sum (map ddwl stxs)" on the LHS,
  where ddwl = getCoin ∘ DirectDepositsOf is the per-sub-tx
  direct-deposit total (analogous to wdrwl).

* combined-certs gains "+ allDirectDeps" on the LHS, composing the
  per-sub CERTS-pov chain with the top-level call.

* The main LEDGER-V chain wraps the result in +-cancelʳ-≡ to
  discharge the asymmetric "+ allDirectDeps" combined-certs introduces.

Removed:

* The certStateFinal local definition (LEDGER-V no longer applies
  applyDirectDeposits).
* step-ii and the applyDirectDeposits-rewardsBalance module parameter
  (subsumed by indexedSumᵛ'-∪⁺ inside POST-CERT-pov).
* The DD-split module parameter (subsumed by per-tx CERTS-pov chain).
* Stale "Key Lemma" subsection and stale commented-out lines in bat'.
* Unused imports +-identityʳ and +-0-monoid.
* Redundant local aliases in bat's where-block.

Documentation: rewrote "Key Differences from Conway" point 2 and the
LEDGER-V Proof Outline to reflect the new architecture; clarified the
LEDGER-I outline.

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>

Two changes that unblock musl64 TH builds:

1. Set `LD_LIBRARY_PATH=<musl-gcc-libs>/lib` on `stdenv.hostPlatform.isMusl`
   so iserv-dyn can resolve `libgcc_s.so.1` from `libstdc++.so` at TH-eval
   time.  Same workaround `comp-builder.nix` has carried for v1; without
   it, `musl64.tests.th-dlls.build` fails with `Error loading shared
   library libgcc_s.so.1` because musl's `libstdc++.so` only carries
   `RUNPATH=<musl libc dir>` (not the gcc lib dir) and musl's dyld only
   consults the immediate library's RUNPATH when resolving its deps.

   That same `LD_LIBRARY_PATH` leaks into every subprocess we spawn,
   including patchelf — a glibc binary built against glibc's
   `libgcc_s.so.1`.  Letting patchelf dlopen the musl libgcc segfaults
   it (which was also the source of the `shrink-rpath` segfaults in
   fixupPhase we'd see on musl).  Prepend `unset LD_LIBRARY_PATH` to the
   rpath rewrite block on musl; nothing in the rest of installPhase or
   fixupPhase needs the iserv search path.

2. Restrict the rpath-walk's `find` to ELF / Mach-O candidates — `.so*`,
   `.dylib*`, and any file under `bin/` — so the rewrite functions
   don't have to defend against `.hi`, `.a`, `cabal-hash.txt`, etc.

The only remaining defence on the elf side is `|| return 0` on
`patchelf --print-rpath`, which the filter doesn't help with: musl exe
slices link statically (`executable-static: True`) and patchelf bails
with `cannot find section '.dynamic'` on those — comment notes it.

Confirmed:
  * x86_64-linux musl64 th-dlls.build (previously failing with both
    `libgcc_s.so.1` and the dep-resolution dyld error)
  * x86_64-linux native with-packages.run
  * x86_64-darwin native exe-lib-dlls.build-profiled

Signed-off-by: Akhil Repala <[email protected]>

Signed-off-by: Akhil Repala <[email protected]>