Fix Agda to Hs equality

Signed-off-by: Ana Pantilie <ana.pantilie95@gmail.com>
IntersectMBO · Jul 18, 2024 · 82bd47b · 82bd47b
1 parent 090f0f5
commit 82bd47b
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 3 deletions.
diff --git a/plutus-metatheory/src/Utils.lagda.md b/plutus-metatheory/src/Utils.lagda.md
@@ -171,6 +171,10 @@ postulate ByteString : Set
 {-# FOREIGN GHC import qualified Data.ByteString as BS #-}
 {-# COMPILE GHC ByteString = type BS.ByteString #-}
 
+postulate
+  eqByteString : ByteString → ByteString → Bool
+{-# COMPILE GHC eqByteString = (==) #-}
+
 ```
 ## Record Types
 ```
@@ -242,13 +246,25 @@ 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
+{-# 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
+{-# 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
+{-# COMPILE GHC eqBls12-381-MlResult = (==) #-}
 ```
 
 ## Kinds

diff --git a/plutus-metatheory/src/VerifiedCompilation/Equality.lagda.md b/plutus-metatheory/src/VerifiedCompilation/Equality.lagda.md
@@ -153,18 +153,32 @@ the underlying types, so this can leverage the standard library decision
 procedures. 
 
 ```
+record HsEq (A : Set) : Set where
+  field
+    hsEq : A → A → Agda.Builtin.Bool.Bool
+
+open HsEq {{...}} public
+
 postulate
   magicNeg : ∀ {A : Set} {a b : A} → ¬ a ≡ b
-  hsEq : {A : Set} → (a b : A) → Agda.Builtin.Bool.Bool
-{-# COMPILE GHC hsEq = (==) #-}
 
 magicBoolDec : {A : Set} → {a b : A} → Agda.Builtin.Bool.Bool → Dec (a ≡ b)
 magicBoolDec true = yes primTrustMe
 magicBoolDec false = no magicNeg
 
-builtinEq : {A : Set} → Binary.Decidable {A = A} _≡_
+builtinEq : {A : Set} {{_ : HsEq A}} → Binary.Decidable {A = A} _≡_
 builtinEq x y = magicBoolDec (hsEq x y)
 
+instance
+  HsEqBytestring : HsEq U.ByteString
+  HsEqBytestring = record { hsEq = U.eqByteString }
+  HsEqBlsG1 : HsEq U.Bls12-381-G1-Element
+  HsEqBlsG1 = record { hsEq = U.eqBls12-381-G1-Element }
+  HsEqBlsG2 : HsEq U.Bls12-381-G2-Element
+  HsEqBlsG2 = record { hsEq = U.eqBls12-381-G2-Element }
+  HsEqBlsMlResult : HsEq U.Bls12-381-MlResult
+  HsEqBlsMlResult = record { hsEq = U.eqBls12-381-MlResult }
+
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aInteger ⟧tag = Data.Integer.Properties._≟_
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aBytestring ⟧tag = builtinEq
 decEq-⟦ _⊢♯.atomic AtomicTyCon.aString ⟧tag = Data.String.Properties._≟_