Implement reference inputs and inline datums

[WhatisRT]

Since we have a few things in Conway that depend on Babbage, it makes sense to work on Babbage some time soon. This ticket is concerned with new Babbage transaction features, which almost entirely consist of modifying existing definitions.

There are a few additional subtleties which can be handled later as separate tasks (i.e. not as part of this ticket):

• Modifying Scripts-No to include collOuts and collateralFees means adjusting the preservation of Value proof. Without this, it also makes sense to add the two new collateral features from the transaction body some other time.
• We don't have a notion of well-formedness for Scripts & Datums (I believe), so we can either not include that check in UTXOW or add it into AbstractFunctions.
• We don't have the check for languages in Alonzo yet, so that can be omitted.

Specifically, the tasks for this ticket are implementing:

• [x] Figure 1 (without collRet and txcoll)
• [x] Figure 2 (only isTwoPhaseScriptAddress)
• [x] Figure 3 (except allOuts, languages and allowedLanguages)
• [x] Figure 5 (not using allOuts)
• [x] Figure 6 (without the isWellFormed check at the bottom)

Note that of those figures, only those changes that are either highlighted in yellow or required by something that is highlighted in yellow should be implemented.

[jmchapman]

Adding additional new properties is out of scope of this task.

[williamdemeo]

I unchecked the first two items because, although I made the required changes to the type definitions, these changes break things which I will need to fix before the items can be rightfully checked off.

[williamdemeo]

Status of Item 1.

I am able to change TxOut = Addr × Value × Maybe DataHash to TxOut = Addr × Value × Maybe (Datum ⊎ DataHash), and Everything type-checks, once I change the definition of TxOut in Ledger.Foreign.LedgerTypes to TxOut = Pair Addr $ Pair Coin $ Maybe (Either Datum DataHash).

However, when I try to expand the definition of TxOut to TxOut = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script, I get an error in HSLedger indicating that there's no F.Script type.

I took a stab at defining a Convertible-Script type in Foreign.HSLedger like this:

  Convertible-Script : Convertible Script F.Script
  Convertible-Script = λ where
    .to → λ where (inj₁ p1s) → p1s
                  (inj₂ p2s) → p2s
    .from s → inj₂ s

(just a guess, based on the definition of Script in Ledger.Script, Script = P1Script ⊎ P2Script)

but I must also define Script in Ledger.Foreign.LedgerTypes and I'm not sure how to do that. From type-checking error messages I'm getting, I suppose Script should have type Ledger.Script.Timelock crypto epochStructure. Does this mean we need an Haskell translation for the Timelock type?

[WhatisRT]

At the moment we don't have scripts in the Haskell interface and I wouldn't worry about that now. Just use ⊥.

[williamdemeo]

@WhatisRT I'm not sure how to use ⊥ for Script.

If I define Script = ⊥ in Ledger.Foreign.LedgerTypes, then, inside {-# FOREIGN GHC ... #-}, do I write type Script = ()? That seems like a contradiction. Haskell has no empty or "bottom" type, correct?

Perhaps you meant, "just use Script = ⊤" (and type Script = ())?

If, in LedgerTypes, I define Script that way, and change the definition of TxOut to

TxOut = Pair Addr $ Pair Coin $ Pair (Maybe (Either Datum DataHash)) $ Maybe Script

and, inside {-# FOREIGN GHC ... #-},

  type TxOut = (Addr, (Coin, (Maybe (Datum | DataHash), Maybe Script)))

then LedgerTypes type-checks, but I get the following error when I try to type-check Evertying:

./src/Ledger/Foreign/HSLedger.agda:281,18-20
No instance of type Convertible Script F.Script was found in scope.
when checking that txouts is a valid argument to a function of type
{A B : Set} ⦃ r : Convertible A B ⦄ → A → B

[williamdemeo]

For the record, I'll re-post here some questions I asked on slack about issues that are blocking understanding/completion of the last task in this issue.

1. I'm trying to understand the inputHashes definition in the UTXOW-inductive rule (Fig. 6 in the Babbage spec pdf). The definition is as follows:

   inputHashes := {h | (a, _ , h, _) ∈ range(utxo|spendInputs tx ) ∧ isTwoPhaseScriptAddress tx utxo a } − Datum

   Since utxo : UTxO is a map from TxIn to TxOut, the range of utxo|spendInputs tx ought to be a set of TxOut values, that is, a set of quadruples which inhabit the type

   TxOut = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script

   (note the third coordinate of the quadruple, h : Maybe (Datum ⊎ DataHash)).

   What is not clear is the "subtraction" of Datum in the definition of inputHashes. In discussing this with James earlier today, we decided it's most likely a shorthand indicating that we only keep hs of the form just (inj₂ d), where d : DataHash; otherwise (when h has the form nohting or just (inj₁ d), with d : Datum), we leave such h out of inputHashes.

2. inputHashes seems to be defined in the UTxO-witG rule in Alonzo in order to provide/check the condition inputHashes ⊆ dom(txdats), whereas in Babbage the analogous subset condition appears with a subscript on the ⊆ symbol---specifically, the subscript is {h | (_ , _ , h , _) ∈ allOuts tx ∪ utxo (refInputs tx)} (see the screen grab below). What is meant by a subscript on the subset relation symbol?

3. For the script type conversion for the Haskell foreign language interface, I tried the following

   Convertible-Script : Convertible Script F.Script
   Convertible-Script = λ where
   .to _ → tt
   .from tt → inj₁ tt

   but Agda complains that ⊤ !=< Timelock when checking that the expression tt has type P1Script... This is because, inside the ScriptStructure record type are the lines

   p1s : P1ScriptStructure
   p1s = P1ScriptStructure-TL
   open P1ScriptStructure p1s public

   and P1ScriptSctructure-TL is defined as follows:

   P1ScriptStructure-TL : ⦃ Hashable Timelock ScriptHash ⦄ → P1ScriptStructure
   P1ScriptStructure-TL = record
    { P1Script = Timelock
    ; validP1Script = evalTimelock }

   so opening p1s inside the ScriptStructure record type has the effect of redefining P1Script as an alias for Timelock.

   Question: what is Timelock and why is P1Script redefined as an alias for it?

[WhatisRT]

I didn't know that we already partially instantiated scripts, so you'll need to match Timelock to a Haskell type. I think you can do a dummy implementation for now, where you make it correspond to a unit type and map it to a dummy script such at RequireAllOf [].

I'm not really sure if you can actually use Script = ⊤ which is why I suggested ⊥. You can define a type that's equivalent to ⊥ in Haskell, it just has inhabitants anyway. But I wouldn't worry about that too much right now, just get the Agda side to work.

Timelock scripts are an alternative to Plutus scripts that are evaluated by the ledger itself. They are evaluated during 'phase 1' of transaction processing, which is why they are also called P1Script (and Plutus P2Script).