/benchmark plutus-benchmark:validation

Comparing benchmark results of 'plutus-benchmark:validation' on '17e096548' (base) and '5581c30bf' (PR)

Ready for review.

Wait, what.

Seems like a glitch to me. Removing some constraints hardly can make the code slower. Core is much better. Everything else got a speedup.

/benchmark plutus-benchmark:validation

Comparing benchmark results of 'plutus-benchmark:validation' on 'afe6dcd54' (base) and 'f9ccac2e7' (PR)

Oops, merged instead of rebasing, fixing.

@michaelpj what's wrong with CI?

/benchmark plutus-benchmark:validation

Comparing benchmark results of 'plutus-benchmark:validation' on 'afe6dcd54' (base) and '03a216ed0' (PR)

I don't know why benchmarks are being

after I rebased on master, but it's still a speedup (albeit a tiny one) and the generated Core is definitely better, so I believe it's still worth merging.

The escrow ones got slower after the skew binary change. These are the only 3 that are underperforming when using skewbinary instead of intmap as the env. I have not investigated why.

/benchmark plutus-benchmark:nofib

Comparing benchmark results of 'plutus-benchmark:nofib' on 'afe6dcd54' (base) and 'fe3ee8c70' (PR)

/benchmark plutus-benchmark:nofib

Comparing benchmark results of 'plutus-benchmark:nofib' on 'afe6dcd54' (base) and 'fe3ee8c70' (PR)

/benchmark plutus-benchmark:nofib

Comparing benchmark results of 'plutus-benchmark:nofib' on 'afe6dcd54' (base) and 'fe3ee8c70' (PR)

I guess if you think the Core is clearly better I'm okay with it, but I think the speedup is below our noise threshold so shrug

I think a 2% change is above our noise threshold. In any case, this PR is essential. Here's how readKnown used to compile:

-- RHS size: {terms: 76, types: 249, coercions: 41, joins: 0/0}
$fKnownTypeInDefaultUnitermInteger_$creadKnown
  = \ @ term_ag9l $d(%,,,%)_ag9m @ cause_ag9N eta_B2 eta1_B1 ->
      case eq_sel ($p1(%,%) ($p1(%,,,%) $d(%,,,%)_ag9m)) of co_agQ7
      { __DEFAULT ->
      case $d(%,,,%)_ag9m of
      { (ww1_sFbW, ww2_sFc6, ww3_sFc7, ww4_sFc8) ->
      case ww1_sFbW of { (ww6_sFbZ, ww7_sFc4) ->
      case ww6_sFbZ of { Eq# ww9_sFc2 ->
      case (($p1(%,%) ww7_sFc4) `cast` <Co:2>)
             $fAsUnliftingErrorReadKnownError eta_B2 eta1_B1
      of {
        Left l_iv28 -> Left l_iv28;
        Right r_iv2a ->
          case r_iv2a `cast` <Co:5> of { ValueOf uniAct_iv2d x_iv2e ->
          case (ww3_sFc7 `cast` <Co:4>) uniAct_iv2d (ww4_sFc8 `cast` <Co:6>)
          of {
            Nothing ->
              Left <...>
            Just ds_iv2l ->
              case ds_iv2l of { Refl co1_iv2o -> (Right x_iv2e) `cast` <Co:8> }
          }
          }
      }
      }
      }
      }
      }

Here's how it compiles now:

-- RHS size: {terms: 61, types: 182, coercions: 37, joins: 0/0}
$fKnownTypeInDefaultUnitermInteger_$creadKnown
  = \ @ term_a2ffv $d(%,%)_a2ffw @ cause_a2ffX eta_B2 eta1_B1 ->
      case eq_sel ($p1(%,%) $d(%,%)_a2ffw) of co_a2fBV { __DEFAULT ->
      case $p1(%,%) $d(%,%)_a2ffw of { Eq# ww1_s2DsX ->
      case (($p1(%,%) ($p2(%,%) ($d(%,%)_a2ffw `cast` <Co:15>)))
            `cast` <Co:2>)
             $fAsUnliftingErrorReadKnownError eta_B2 eta1_B1
      of {
        Left l_i1W2s -> Left l_i1W2s;
        Right r_i1W2u ->
          case r_i1W2u `cast` <Co:5> of { ValueOf uniAct_a1UPO x_a1UPP ->
          case uniAct_a1UPO `cast` <Co:6> of wild2_XR {
            __DEFAULT ->
              Left <...>
            DefaultUniInteger co1_a2eQY -> (Right x_a1UPP) `cast` <Co:7>
          }
          }
      }
      }
      }

Note how in the latter we directly match on DefaultUniInteger instead of checking two things for equality at runtime and manually extracting the proof.

I'm not sure where the occasional slowdown is coming from (I did look at the whole Core output closely), maybe those $p1(%,%) and $p2(%,%) are slow and we have more of them now, but I think the changes are worth merging and I have a branch where all of HasConstant stuff is inlined and we don't have as many selectors there.