Make costmdls a map as in the Alonzo spec

[facundominguez]

Addresses part of #723

[facundominguez]

I'm puzzled that adding these two instances here is necessary.

Moreover, I don't understand why Show-× isn't enough and I need to replace it with Show-L×C. The meta program fails to produce the Show instance of PParams otherwise.

[facundominguez]

Imitating how Show-ProtVer is defined, I implemented a shorter solution in a later commit. I guess my questions stand as concerns of an Agda user. Show-List and Show-× are not defined as instances in standard-library-classes:Class.Show.Instances.

[williamdemeo]

key issue/possible bug

Using lookupᵐ? and mapPartial in collectP2ScriptsWithContext might result in silently skipping required scripts.

We define collectP2ScriptsWithContext with a helper,

toScriptInput : ScriptPurpose → ScriptHash → Maybe (P2Script × List Data × ExUnits × CostModel)

which (in this PR) uses costModel ← lookupᵐ? (PParams.costmdls pp) (language p2s), and collectP2ScriptsWithContext builds a list via:

setToList
    $ mapPartial (λ (sp , c) → if isScriptObj c
                                then (λ {sh} → toScriptInput sp sh)
                                else nothing)
    $ credsNeeded utxo (tx .Tx.body)

So, if a cost model is missing for some language, then lookupᵐ? returns nothing, which makes toScriptInput return nothing, which makes mapPartial drop that script from the list, which makes evalP2Scripts run all over a list that is missing a required script. I think this means the transaction could incorrectly pass because a script never ran. This seems like a real risk, unless we ensure that a missing cost model is impossible.

Suggested Fix

I suggest (for now) just adding the following to the list of premises of the UTXOW rule:

    ∙  languages tx utxo ⊆ dom (PParams.costmdls (PParamsOf Γ))

and wherever collectP2ScriptsWithContext is called, treat a nothing in the list a Phase 1 failure.

[williamdemeo]

In the Alonzo spec, collectTwoPhaseScriptInputs explicitly includes the membership condition language script ↦ cm ∈ costmdls pp. So the input list is defined only when the cost model exists. (Missing cost models are a Phase 1 failure, before script evaluation.) This means "don't silently skip; fail earlier" is actually part of the Alonzo design.

I think the "right" (faithful to Alonzo) way would be to refactor collectP2ScriptsWithContext so that the helper function toScriptInput can use the total map lookup (i.e., let costModel = lookupᵐ (PParams.costmdls pp) (language p2s)), but this is a bit tricky because we would then need to somehow prove, or make it a hypothesis of collectP2ScriptsWithContext, that the language of every script is in the domain of the PParams.costmdls map.

Alternatively, probably much easier (but maybe not as safe), keep the current toScriptInput helper, but don't let a missing cost model just cause a dropped script and then continue as if nothing's wrong. Instead, make collectP2ScriptsWithContext return Maybe List (P2Script x List Data x ...)) and then, wherever collectP2ScriptsWithContext is used, treat a nothing as a Phase 1 failure.

[facundominguez]

It is true that in both the Agda spec and the Alonzo spec, scripts are dropped in the collect... functions if they don't have a cost model.

However, Alonzo also requires that all scripts have a cost model. This is done in the UTXOW rule, exactly with the suggested premise, in Figure 13.

The Agda implementation did not include this premise yet. Thus the concern is entirely justified!

treat a nothing in the list a Phase 1 failure.

I don't know what this means. After adding the missing premise, are there other missing bits from Alonzo related to cost models?

[facundominguez]

It is looking to me like the same trouble would come if indexedRdrms returned nothing. The Alonzo spec has a premise to prevent that in the same Figure 13, which is missing in the Agda spec. This deserves a separate PR though.

[facundominguez]

@williamdemeo, perhaps this is ready for another review. I rebased master and added the suggested premise relating the domain of costmdls and the script languages.

[facundominguez]

I rebased master, and reverted a small modification to the Dijkstra spec now that we agreed to let Dijkstra alone when porting Alonzo features.