Refactor some inconsistent field names

[williamdemeo]

Specifically, the field names in TxBody should be more consistent. Either all should begin with tx, or none should, and we should stick to either all lower case or all camel case. This will make name choices for type classes and lenses more natural/obvious.

[WhatisRT]

Way back, there was a decision to not have a prefix. This is for example why it's body instead of txbody in the current spec. But I think what happened is that I forgot about enforcing it, and so new fields still have that prefix sometimes.

[williamdemeo]

I think the field names txins and txouts (of TxBody record type) seem more natural than ins and outs, maybe only because that's what I'm used to. @WhatisRT @lehins @carlostome what do you guys think? Should we really change all the field names in TxBody in the spec so that none of them has a tx prefix?

[williamdemeo]

Also, keeping the tx prefix is more "backward compatible" for readers of pdfs of previous eras. For example, below is a screenshot from the Shelley spec. Interestingly, txins (and others) are actually "accessor functions" in the Shelley spec, which gives me an idea: we could call the field ins in the record and then define an accessor function (or type class instance of a new HasIns class) called txins that returns the value of the ins field of the given TxBody (or, vice-versa, keep the field name txins and call the accessor ins or insOf or txinsOf, or...). Thoughts?

[williamdemeo]

I just did a search for each field name in the Agda code base and noticed that three fields are hardly used at all. Specifically,txup, reqSigHash, and scriptIntHash:

txup : Maybe Update

Occurrences in Agda code

• 5 matches in 3 files

File: Ledger/Conway/Specification/Transaction.lagda
152:7:      txup           : Maybe Update

File: Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda
88:28:                         ; txup = nothing
124:28:                         ; txup = nothing

File: Ledger/Conway/Specification/Test/Examples/HelloWorld.agda
66:28:                         ; txup = nothing
98:28:                         ; txup = nothing

---

reqSigHash : ℙ KeyHash

Occurrences in Agda code

• 6 matches in 4 files

File: Ledger/Conway/Specification/Transaction.lagda
158:7:      reqSigHash     : ℙ KeyHash

File: Ledger/Conway/Specification/Test/Examples/HelloWorld.agda
72:28:                         ; reqSigHash = ∅
104:28:                         ; reqSigHash = ∅

File: Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda
94:28:                         ; reqSigHash = ∅
130:28:                         ; reqSigHash = ∅

File: Ledger/Conway/Specification/Script/Validation.agda
70:13:  ; vkKey = reqSigHash

---

scriptIntHash : Maybe ScriptHash

Occurrences in Agda code

• 5 matches in 3 files

File: Ledger/Conway/Specification/Transaction.lagda
159:7:      scriptIntHash  : Maybe ScriptHash

File: Ledger/Conway/Specification/Test/Examples/HelloWorld.agda
73:28:                         ; scriptIntHash = nothing
105:28:                         ; scriptIntHash = nothing

File: Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda
95:28:                         ; scriptIntHash = nothing
131:28:                         ; scriptIntHash = nothing

[williamdemeo]

My preference would be to change the TxBody field names so it's more immediately obvious what they are for. @WhatisRT, what do you think about possibly changing the record definition from

  record TxBody : Type where
    field
      txins          : ℙ TxIn
      refInputs      : ℙ TxIn
      txouts         : Ix ⇀ TxOut
      txfee          : Coin
      mint           : Value
      txvldt         : Maybe Slot × Maybe Slot
      txcerts        : List DCert
      txwdrls        : Wdrl
      txvote         : List GovVote
      txprop         : List GovProposal
      txdonation     : Coin
      txup           : Maybe Update
      txADhash       : Maybe ADHash
      txNetworkId    : Maybe Network
      curTreasury    : Maybe Coin
      txid           : TxId
      collateral     : ℙ TxIn
      reqSigHash     : ℙ KeyHash
      scriptIntHash  : Maybe ScriptHash

to

  record TxBody : Type where
    field
      txInputs             : ℙ TxIn
      txRefInputs          : ℙ TxIn
      txOutputs            : Ix ⇀ TxOut
      txFee                : Coin
      txMint               : Value
      txValidSlotInterval  : Maybe Slot × Maybe Slot
      txDCerts             : List DCert
      txWithdrawals        : Wdrl
      txGovVote            : List GovVote
      txGovProposal        : List GovProposal
      txDonation           : Coin
      txADhash             : Maybe ADHash
      txNetworkId          : Maybe Network
      txCurrentTreasury    : Maybe Coin
      txId                 : TxId
      txCollateral         : ℙ TxIn

So, give all fields the tx prefix for consistency, lengthen their names for clarity, and eliminate the currently unused fields reqSigHash, scriptIntHash, txup.

Btw, elsewhere in the Transaction module we have

  adHashingScheme : isHashableSet AuxiliaryData
  open isHashableSet adHashingScheme renaming (THash to ADHash) public

I'm not sure what the "AD" in ADHash and txADhash stands for.

[facundominguez]

Given the work I'm doing at the moment, my biased preference is that names are kept the same as used in the PDF documents for older eras.