Fix headAdaOverhead and partial fanout proof UTxO handling
closeTx now reads headAdaOverhead directly from the OpenDatum rather than recomputing it from the difference between head lovelace and snapshot UTxO lovelace. The old computation was vulnerable to griefing (anyone could bump the head value) and broke strict equality in the on-chain mustPreserveHeadAdaOverhead check. The value is already locked at init time, so propagating it unchanged is both simpler and correct. FinalPartialFanoutTx gains a separate utxoForProof field so the accumulator membership proof can include pre-settled UTxOs (e.g. decommit outputs already removed from the head by a DecrementTx before close), while utxoToDistribute covers only what is actually fanned out in the final step. finalPartialFanoutTx / finalPartialFanout are updated to accept the full accumulator explicitly rather than rebuilding it from utxoToDistribute alone. Test generators (genClosedStateForFanout, genClosedStateWithAppliedDecommit, genClosedStateForFanoutWithComplexUTxO) were setting head ADA to headAdaOverhead + genStOpen_u0Value + snapshot_u0Value, leaving surplus lovelace unaccounted for in the FinalPartialFanout conservation check. They now net out genStOpen's inflation so head ADA equals exactly headAdaOverhead + snapshot_u0Value as the invariant requires. Signed-off-by: Sasha Bogicevic <[email protected]>
