Skip to content

Commit

Permalink
Improved hashing in conformance testing
Browse files Browse the repository at this point in the history
  • Loading branch information
Soupstraw committed Oct 4, 2024
1 parent 4189bdc commit 91d8d95
Show file tree
Hide file tree
Showing 3 changed files with 28 additions and 20 deletions.
4 changes: 2 additions & 2 deletions cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@ source-repository-package
-- !WARNING!:
-- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
subdir: generated
tag: 0b0b1f4eddb718b704824dcdc86abb8ce815deb2
--sha256: sha256-+bpsxn1hPGZqJ0rwZmUaPlOJuRj0RzLj1rulldUqk/E=
tag: d5c32e238236e6e2a3941551b4512e117e399271
--sha256: sha256-bi4+bXqi8n2BQM4+9uwwaDsm3nblg15Cj+9IvNGTkPI=
-- NOTE: If you would like to update the above, look for the `MAlonzo-code`
-- branch in the `formal-ledger-specifications` repo and copy the SHA of
-- the commit you need. The `MAlonzo-code` branch functions like an alternative
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,8 @@ instance NFData BootstrapAddr

instance NFData Timelock

instance NFData HashedTimelock

instance NFData UTxOState

instance NFData Vote
Expand Down Expand Up @@ -186,6 +188,8 @@ instance ToExpr BootstrapAddr

instance ToExpr Timelock

instance ToExpr HashedTimelock

instance ToExpr TxBody

instance ToExpr Tag
Expand Down Expand Up @@ -277,6 +281,8 @@ instance FixupSpecRep BootstrapAddr

instance FixupSpecRep Timelock

instance FixupSpecRep HashedTimelock

instance FixupSpecRep UTxOState

instance FixupSpecRep Credential
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -217,23 +217,25 @@ instance
) =>
SpecTranslate ctx (Timelock era)
where
type SpecRep (Timelock era) = Agda.Timelock

toSpecRep =
\case
RequireSignature kh ->
Agda.RequireSig <$> toSpecRep kh
RequireAllOf ss -> do
tls <- traverse toSpecRep ss
pure . Agda.RequireAllOf $ toList tls
RequireAnyOf ss -> do
tls <- traverse toSpecRep ss
pure . Agda.RequireAnyOf $ toList tls
RequireMOf m ss -> do
tls <- traverse toSpecRep ss
pure . Agda.RequireMOf (toInteger m) $ toList tls
RequireTimeExpire slot -> Agda.RequireTimeExpire <$> toSpecRep slot
RequireTimeStart slot -> Agda.RequireTimeStart <$> toSpecRep slot
type SpecRep (Timelock era) = Agda.HashedTimelock

toSpecRep tl = Agda.HashedTimelock <$> timelockToSpecRep tl <*> undefined
where
timelockToSpecRep x =
case x of
RequireSignature kh ->
Agda.RequireSig <$> toSpecRep kh
RequireAllOf ss -> do
tls <- traverse timelockToSpecRep ss
pure . Agda.RequireAllOf $ toList tls
RequireAnyOf ss -> do
tls <- traverse timelockToSpecRep ss
pure . Agda.RequireAnyOf $ toList tls
RequireMOf m ss -> do
tls <- traverse timelockToSpecRep ss
pure . Agda.RequireMOf (toInteger m) $ toList tls
RequireTimeExpire slot -> Agda.RequireTimeExpire <$> toSpecRep slot
RequireTimeStart slot -> Agda.RequireTimeStart <$> toSpecRep slot

instance
( AlonzoEraScript era
Expand Down Expand Up @@ -261,7 +263,7 @@ instance
instance
( EraTxOut era
, SpecRep (Value era) ~ Agda.Coin
, SpecRep (Script era) ~ Either Agda.Timelock ()
, Script era ~ AlonzoScript era
, SpecTranslate ctx (Value era)
, SpecTranslate ctx (Script era)
) =>
Expand Down

0 comments on commit 91d8d95

Please sign in to comment.