Fix bug in builtin decidable equality

[ana-pantilie]

Fixes https://github.com/IntersectMBO/plutus-private/issues/1505

[ana-pantilie]

Unrelated to this issue, this golden file was not checked in but it should be.

[ramsay-t]

Thanks - I think this should have been in the Pure PR? It wasn't checked in because it was broken before we decided how to resolve that.

[ramsay-t]

Doesn't this now always return true? primTrustMe just builds an equality proof out of thin air, so will always produce refl? magicBoolDec is about summoning the magical proof from a legitimate boolean answer of true or false, hence it only uses primTrustMe in the true branch. Or am I missing something?

[ramsay-t]

Ok, the docs suggest this is how you are supposed to use primTrusMe - I think it works on the basis that when Agda sees refl it tries to unify a bunch of stuff, which will then fail if they are incompatible? It looks scary though :)

[ana-pantilie]

Doesn't this now always return true? primTrustMe just builds an equality proof out of thin air, so will always produce refl? magicBoolDec is about summoning the magical proof from a legitimate boolean answer of true or false, hence it only uses primTrustMe in the true branch. Or am I missing something?

magicBoolDec is where the proofs were getting stuck. Why? Because it matches on true and false, which it should get from the hsEq functions. But the hsEq functions cannot ever evaluate to true and false because they're all postulated!

Ok, the docs suggest this is how you are supposed to use primTrusMe - I think it works on the basis that when Agda sees refl it tries to unify a bunch of stuff, which will then fail if they are incompatible? It looks scary though :)

Yes, that's right. primTrustMe will evaluate to refl if it can unify the two terms, if it can't, it will get stuck.

[zliu41]

If it always returns yes refl, you may want to reflect in the name of this function that this is a bogus equality check.

Is there no use at all for the original builtEq, which can at least return no?

[ana-pantilie]

@zliu41

If it always returns yes refl

It doesn't always return yes refl. Matching on refl triggers Agda's unification algorithm, which checks whether the two terms are definitionally equal. For example: in builtinEq (mkByteString "foo") (mkByteString "foo") the two terms are structurally equal so unification will succeed, and the function will return yes refl, while builtinEq (mkByteString "foo") (mkByteString "bar") will get stuck because unification does not succeed.

Is there no use at all for the original builtEq, which can at least return no?

The original builtinEq could never return no, it could never return yes either, which was the root of this bug!

I will add some documentation making all of the above more clear.

There is one thing I have realized now: we have only been discussing the behavior of this code at compile time, and we need to also know what happens at runtime. We currently don't have any tests for that, or a way to construct such tests, but I'll add some very soon since this is what I'm working on at the moment.

[ramsay-t]

This is what I was wanting to test - if it unifies then it makes refl and returns yes. If it doesn't, it "gets stuck" but I'm not sure what that will look like - it won't make a nice no response I don't think?

[ramsay-t]

It just refuses to typecheck - although it produces quite a nice, helpful error! We can probably use this fine in Certificates if we want to certify that the things are equal; we might want to keep the other version for the decision procedures that run in Haskell? They can then do something with the negative response, since hsEq will run there?

[zliu41]

Matching on refl triggers Agda's unification algorithm, which checks whether the two terms are definitionally equal.

Ah, that's nice.

we might want to keep the other version for the decision procedures that run in Haskell?

It's probably sufficient to keep hsEq (rather than the previous version of builtinEq)?

[ana-pantilie]

I'll need to look into that, I don't think it will be that easy. It's possible to give a different runtime definition to Agda functions (see the warning at https://agda.readthedocs.io/en/stable/language/foreign-function-interface.html#using-haskell-functions-from-agda), but the types need to match. So I would need to implement builtinEq : {A : Set} → Binary.Decidable {A = A} _≡_ in Haskell. In order to do that the types need to have certain pragmas to be identifiable from Haskell, and unfortunately the Agda stdlib does not provide these. I will try to see if some workaround exists. Opened an issue for this: https://github.com/IntersectMBO/plutus-private/issues/1534

[zliu41]

If it always returns yes refl, you may want to reflect in the name of this function that this is a bogus equality check.

Is there no use at all for the original builtEq, which can at least return no?

[zliu41]

do you need a COMPILE pragma?

[ana-pantilie]

I don't think so. mkByteString is only used for generating the certificates which are only meant to be type-checked, and not compiled down to Haskell.