Fix Haskell version of certifier builtinEq

plutus-executables/test/certifier/Test/Certifier/AST.hs

@@ -7,6 +7,7 @@ import UntypedPlutusCore
 import AgdaTrace (mkAgdaTrace)
 import MAlonzo.Code.VerifiedCompilation (runCertifierMain)
 
+import Data.Text.Encoding qualified as Text
 import Test.Tasty
 import Test.Tasty.HUnit
 
@@ -80,9 +81,27 @@ testTrivialFailure1 =
     (mkConstant () (1 :: Integer))
     (mkConstant () (2 :: Integer))
 
+testByteStringEqSuccess :: TestTree
+testByteStringEqSuccess =
+  testFailure
+    "bytestrings expected to not be equal"
+    FloatDelay
+    (mkConstant () (Text.encodeUtf8 "foo"))
+    (mkConstant () (Text.encodeUtf8 "bar"))
+
+testByteStringEqFailure :: TestTree
+testByteStringEqFailure =
+  testSuccess
+    "bytestrings expected to be equal"
+    FloatDelay
+    (mkConstant () (Text.encodeUtf8 "foo"))
+    (mkConstant () (Text.encodeUtf8 "foo"))
+
 astTests :: TestTree
 astTests =
   testGroup "certifier ast tests"
     [ testTrivialSuccess1
     , testTrivialFailure1
+    , testByteStringEqSuccess
+    , testByteStringEqFailure
     ]

plutus-metatheory/changelog.d/20250428_130712_ana.pantilie95_haskell_builtinEq.rst

@@ -0,0 +1,5 @@
+Fixed
+-----
+
+- Fixed the runtime representation of `VerifiedCompilation.Equality.builtinEq`.
+- `DATA` equality now depends on `builtinEq` as well.

plutus-metatheory/src/Utils.lagda.md

@@ -176,8 +176,12 @@ postulate ByteString : Set
 {-# COMPILE GHC ByteString = type BS.ByteString #-}
 
 postulate
-  eqByteString : ByteString → ByteString → Bool
   mkByteString : String → ByteString
+
+-- Agda implementation should only be used as part of deciding builtin equality.
+-- See "Decidable Equality of Builtins" in "VerifiedCompilation.Equality".
+eqByteString : ByteString → ByteString → Bool
+eqByteString _ _ = Bool.true
 {-# COMPILE GHC eqByteString = (==) #-}
 
 ```
@@ -253,31 +257,76 @@ data DATA : Set where
 {-# FOREIGN GHC import PlutusCore.Data as D #-}
 {-# COMPILE GHC DATA = data Data (D.Constr | D.Map | D.List | D.I | D.B)   #-}
 
-postulate eqDATA : DATA → DATA → Bool
+-- Agda implementation should only be used as part of deciding builtin equality.
+-- See "Decidable Equality of Builtins" in "VerifiedCompilation.Equality".
+{-# TERMINATING #-}
+eqDATA : DATA → DATA → Bool
+eqDATA (ConstrDATA i₁ l₁) (ConstrDATA i₂ l₂) =
+    (Relation.Nullary.isYes (i₁ Data.Integer.≟ i₂))
+  Data.Bool.∧
+    L.and (L.zipWith eqDATA (toList l₁) (toList l₂))  
+eqDATA (ConstrDATA x x₁) (MapDATA x₂) = Bool.false
+eqDATA (ConstrDATA x x₁) (ListDATA x₂) = Bool.false
+eqDATA (ConstrDATA x x₁) (iDATA x₂) = Bool.false
+eqDATA (ConstrDATA x x₁) (bDATA x₂) = Bool.false
+eqDATA (MapDATA x) (ConstrDATA x₁ x₂) = Bool.false
+eqDATA (MapDATA m₁) (MapDATA m₂) =
+  L.and
+    (L.zipWith
+      (λ (x₁ , y₁) (x₂ , y₂) → eqDATA x₁ x₂ Data.Bool.∧ eqDATA y₁ y₂)
+      (toList m₁)
+      (toList m₂)
+    )
+eqDATA (MapDATA x) (ListDATA x₁) = Bool.false 
+eqDATA (MapDATA x) (iDATA x₁) = Bool.false
+eqDATA (MapDATA x) (bDATA x₁) = Bool.false
+eqDATA (ListDATA x) (ConstrDATA x₁ x₂) = Bool.false
+eqDATA (ListDATA x) (MapDATA x₁) = Bool.false
+eqDATA (ListDATA x) (ListDATA x₁) = L.and (L.zipWith eqDATA (toList x) (toList x₁))
+eqDATA (ListDATA x) (iDATA x₁) = Bool.false
+eqDATA (ListDATA x) (bDATA x₁) = Bool.false
+eqDATA (iDATA x) (ConstrDATA x₁ x₂) = Bool.false
+eqDATA (iDATA x) (MapDATA x₁) = Bool.false
+eqDATA (iDATA x) (ListDATA x₁) = Bool.false
+eqDATA (iDATA i₁) (iDATA i₂) = Relation.Nullary.isYes (i₁ Data.Integer.≟ i₂)
+eqDATA (iDATA x) (bDATA x₁) = Bool.false
+eqDATA (bDATA x) (ConstrDATA x₁ x₂) = Bool.false
+eqDATA (bDATA x) (MapDATA x₁) = Bool.false
+eqDATA (bDATA x) (ListDATA x₁) = Bool.false
+eqDATA (bDATA x) (iDATA x₁) = Bool.false
+-- Warning: eqByteString is always trivially true at the Agda level.
+-- See "Decidable Equality of Builtins" in "VerifiedCompilation.Equality".
+eqDATA (bDATA b₁) (bDATA b₂) = eqByteString b₁ b₂
 {-# COMPILE GHC eqDATA = (==) #-}
 
 postulate Bls12-381-G1-Element : Set
 {-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.G1 as G1 #-}
 {-# COMPILE GHC Bls12-381-G1-Element = type G1.Element #-}
 
-postulate
-  eqBls12-381-G1-Element : Bls12-381-G1-Element → Bls12-381-G1-Element → Bool
+-- Agda implementation should only be used as part of deciding builtin equality.
+-- See "Decidable Equality of Builtins" in "VerifiedCompilation.Equality".
+eqBls12-381-G1-Element : Bls12-381-G1-Element → Bls12-381-G1-Element → Bool
+eqBls12-381-G1-Element _ _ = Bool.true
 {-# COMPILE GHC eqBls12-381-G1-Element = (==) #-}
 
 postulate Bls12-381-G2-Element : Set
 {-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.G2 as G2 #-}
 {-# COMPILE GHC Bls12-381-G2-Element = type G2.Element #-}
 
-postulate
-  eqBls12-381-G2-Element : Bls12-381-G2-Element → Bls12-381-G2-Element → Bool
+-- Agda implementation should only be used as part of deciding builtin equality.
+-- See "Decidable Equality of Builtins" in "VerifiedCompilation.Equality".
+eqBls12-381-G2-Element : Bls12-381-G2-Element → Bls12-381-G2-Element → Bool
+eqBls12-381-G2-Element _ _ = Bool.true
 {-# COMPILE GHC eqBls12-381-G2-Element = (==) #-}
 
 postulate Bls12-381-MlResult : Set
 {-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.Pairing as Pairing #-}
 {-# COMPILE GHC Bls12-381-MlResult = type Pairing.MlResult #-}
 
-postulate
-  eqBls12-381-MlResult : Bls12-381-MlResult → Bls12-381-MlResult → Bool
+-- Agda implementation should only be used as part of deciding builtin equality.
+-- See "Decidable Equality of Builtins" in "VerifiedCompilation.Equality".
+eqBls12-381-MlResult : Bls12-381-MlResult → Bls12-381-MlResult → Bool
+eqBls12-381-MlResult _ _ = Bool.true
 {-# COMPILE GHC eqBls12-381-MlResult = (==) #-}
 ```
 

plutus-metatheory/src/VerifiedCompilation/Equality.lagda.md

@@ -148,40 +148,51 @@ decEq-TyTag (_⊢♯.pair t t₁) (_⊢♯.pair t' t'') with (t ≟ t') ×-dec (
 ... | no ¬pq = no λ { refl → ¬pq (refl , refl) }
 
 ```
-The equality of the semantics of constants will depend on the equality of
-the underlying types, so this can leverage the standard library decision
-procedures. 
+# Decidable Equality of Builtins
 
-```
-record HsEq (A : Set) : Set where
-  field
-    hsEq : A → A → Agda.Builtin.Bool.Bool
+We need to decide equality between our builtin types. This is tricky because
+this needs to be done at both the Agda type-checking time and at runtime, while
+each stage has a completely different representation of the types.
 
-open HsEq {{...}} public
+## Type-checking time vs runtime
 
-postulate
-  magicNeg : ∀ {A : Set} {a b : A} → ¬ a ≡ b
+In Agda, the types are postulated, which means that at type-checking time we
+may only rely on Agda's unification algorithm to decide equality. This can be
+done by matching on `refl`, which checks whether the left hand side and the
+right hand side of `≡` are definitionally equal. However, this does not translate
+to the runtime stage, since at runtime the values which the `≡` type depends on
+are erased. Therefore, we need to somehow "inject" a Haskell equality function which
+triggers only at the runtime stage. 
 
-magicBoolDec : {A : Set} → {a b : A} → Agda.Builtin.Bool.Bool → Dec (a ≡ b)
-magicBoolDec true = yes primTrustMe
-magicBoolDec false = no magicNeg
-```
+## Why not just implement the builtin types in Agda?
+
+The problem is that Agda's FFI only allows non-postulated Agda types which are
+representationally equivalent to the Haskell types they compile to. If we were to
+implement the types in Agda, they would need to be equivalent to the highly optimized
+and complicated Haskell types, and this is not feasible.
+
+We also cannot de-couple the Agda types from the Haskell types because the Agda
+specification of UPLC is also used in conformance testing.
+
+## Using the quirks of the FFI to our advantage
 
-Our builtins types and functions are postulated. In order to decide equality
-we rely on Agda's notion of definitional equality.
+Agda's FFI machinery allows us to define functions with different runtime
+and type-checking definitions (see the warning at https://agda.readthedocs.io/en/v2.7.0.1/language/foreign-function-interface.html#using-haskell-functions-from-agda).
+We are still constrained by the type, which needs to agree between the two
+stages, so we can't just define the two implementations arbitrarily. 
 
-The definition of `builtinEq` might seem strange, but what happens is that
-matching on `refl` triggers Agda's unification algorithm, which checks whether
-the two terms are definitionally equal.
+The simplest solution is to provide separate type-checking time and runtime definitions
+for the instances of `HsEq`. During type-checking, the functions are essentially no-ops
+by always returning `true`, while at runtime they defer to the Haskell implementation of
+equality for each type. At type-checking time, we rely on matching on `refl` to defer to
+Agda's unification algorithm, while at runtime, the matching on `refl` becomes a no-op.
 
-For example: for `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.
 ```
-builtinEq : {A : Set} → Binary.Decidable {A = A} _≡_
-builtinEq {A} x y with primTrustMe {Agda.Primitive.lzero} {A} {x} {y}
-... | refl = yes refl
+record HsEq (A : Set) : Set where
+  field
+    hsEq : A → A → Agda.Builtin.Bool.Bool
+
+open HsEq {{...}} public
 
 instance
   HsEqBytestring : HsEq U.ByteString
@@ -192,14 +203,43 @@ instance
   HsEqBlsG2 = record { hsEq = U.eqBls12-381-G2-Element }
   HsEqBlsMlResult : HsEq U.Bls12-381-MlResult
   HsEqBlsMlResult = record { hsEq = U.eqBls12-381-MlResult }
+  HsEqDATA : HsEq U.DATA
+  HsEqDATA = record { hsEq = U.eqDATA }
+
+```
+
+## An example
+
+Let's look at the behavior of `builtinEq (mkByteString "foo") (mkByteString "foo")` vs
+`builtinEq (mkByteString "foo") (mkByteString "bar")`. 
+
+At type-checking time, if the two bytestrings are definitionally equal unification will succeed,
+and the function will return `yes refl`. There is no way to return `no` because there is
+no way to prove that the two terms are not equal without extra information about the
+`ByteString` type. But this is enough to make Agda not succesfully type-check the program,
+since it gets stuck while trying to normalize `primTrustMe`.
+
+At runtime, `hsEq` will defer to the Haskell implementation of bytestring equality, and return
+the correct result based on that. In the `yes` case, matching on `refl` will be a no-op,
+while in the `no` case, we return a phony negative proof. This is safe to do because we're
+at runtime and the proof gets erased anyway.
+
+```
+postulate
+  magicNeg : ∀ {A : Set} {a b : A} → ¬ a ≡ b
+
+builtinEq : {A : Set} {{_ : HsEq A}} → Binary.Decidable {A = A} _≡_
+builtinEq {A} x y with hsEq x y
+... | false = no magicNeg
+... | true with primTrustMe {Agda.Primitive.lzero} {A} {x} {y}
+...             | refl = yes refl
 
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aInteger ⟧tag = Data.Integer.Properties._≟_
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aBytestring ⟧tag = builtinEq
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aString ⟧tag = Data.String.Properties._≟_
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aUnit ⟧tag = Data.Unit.Properties._≟_
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aBool ⟧tag = Data.Bool.Properties._≟_
--- TODO(https://github.com/IntersectMBO/plutus-private/issues/1528): why does this use magicBoolDec? surely it can be implemented correctly
-decEq-⟦ _⊢♯.atomic AtomicTyCon.aData ⟧tag v v₁ = magicBoolDec (U.eqDATA v v₁)
+decEq-⟦ _⊢♯.atomic AtomicTyCon.aData ⟧tag = builtinEq
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-g1-element ⟧tag = builtinEq
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-g2-element ⟧tag = builtinEq
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-mlresult ⟧tag = builtinEq