Skip to content

Certifier: Add decision procedure for hoist-builtins pass #7822

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
basetunnel wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Certifier: Add decision procedure for hoist-builtins pass #7822

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ data CertifiedOptStage
| ApplyToCase
| CaseReduce
| LetFloatOut
| PolyBuiltin
deriving stock (Show, Generic)
deriving anyclass (NFData)

Expand All @@ -44,7 +45,6 @@ at https://github.com/IntersectMBO/plutus/issues. -}
data UncertifiedOptStage
= CaseOfCase
| ConstantFolding
| PolyBuiltin
deriving stock (Show, Generic)
deriving anyclass (NFData)

Expand Down Expand Up @@ -81,7 +81,7 @@ pattern ConstantFoldingStage :: OptStage
pattern ConstantFoldingStage = Left ConstantFolding

pattern PolyBuiltinStage :: OptStage
pattern PolyBuiltinStage = Left PolyBuiltin
pattern PolyBuiltinStage = Right PolyBuiltin

{-# COMPLETE
FloatDelayStage
Expand Down
4 changes: 3 additions & 1 deletion plutus-metatheory/src/CertifierReport.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ open import VerifiedCompilation.UntypedTranslation
open import VerifiedCompilation.UInline
open import VerifiedCompilation.UCaseReduce as CR
import VerifiedCompilation.FloatOut as FloatOut
open import VerifiedCompilation.UCSE as CSE
open import Untyped.Relation.Binary.Modular
open import Untyped.Relation.Binary.Core renaming (Pointwise to PW)
open import Untyped
Expand Down Expand Up @@ -48,11 +49,11 @@ showCertifiedOptTag cseT = "Common Subexpression Elimination"
showCertifiedOptTag applyToCaseT = "Transform multi-argument applications into case-constr form"
showCertifiedOptTag caseReduceT = "Case-Constr and Case-Constant Cancellation"
showCertifiedOptTag letFloatOutT = "Float bindings outwards"
showCertifiedOptTag polyBuiltinT = "Hoist Polymorphic Builtins"

showUncertifiedOptTag : UncertifiedOptTag → String
showUncertifiedOptTag caseOfCaseT = "Case-of-Case"
showUncertifiedOptTag constantFoldingT = "Constant Folding"
showUncertifiedOptTag polyBuiltinT = "Hoist Polymorphic Builtins"

showTag : OptTag → String
showTag (inj₁ tag) = showUncertifiedOptTag tag ++ " ⚠ (certifier unavailable)"
Expand Down Expand Up @@ -129,6 +130,7 @@ numSites forceCaseDelayT p = numSites′ p
numSites applyToCaseT p = numSites′ p
numSites {M = M} caseReduceT p = numSitesCaseReduce (CR.sound {M = M} p)
numSites letFloatOutT p = FloatOut.numSites p
numSites polyBuiltinT p = CSE.polyNumSites p

showSites : {M N : 0 ⊢} → (tag : OptTag) → RelationOf tag M N → String
showSites (inj₁ _) _ = ""
Expand Down
2 changes: 1 addition & 1 deletion plutus-metatheory/src/FFI/AgdaUnparse.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,11 +74,11 @@ instance AgdaUnparse CertifiedOptStage where
agdaUnparse ApplyToCase = "applyToCaseT"
agdaUnparse CaseReduce = "caseReduceT"
agdaUnparse LetFloatOut = "letFloatOutT"
agdaUnparse PolyBuiltin = "polyBuiltinT"

instance AgdaUnparse UncertifiedOptStage where
agdaUnparse CaseOfCase = "caseOfCaseT"
agdaUnparse ConstantFolding = "constantFoldingT"
agdaUnparse PolyBuiltin = "polyBuiltinT"

instance AgdaUnparse Hints.Hints where
agdaUnparse = \case
Expand Down
12 changes: 6 additions & 6 deletions plutus-metatheory/src/MAlonzo/Code/Certifier.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ d_runCertifier_2 ::
(MAlonzo.Code.Utils.T__'215'__436
(MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10)
MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
MAlonzo.Code.RawU.T_Untyped_210 ->
MAlonzo.Code.Utils.T_Either_6
Expand Down Expand Up @@ -65,7 +65,7 @@ runCertifierMain ::
(MAlonzo.Code.Utils.T__'215'__436
(MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10)
MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
MAlonzo.Code.RawU.T_Untyped_210 ->
MAlonzo.Code.Agda.Builtin.List.T_List_10
Expand All @@ -80,7 +80,7 @@ d_runCertifierMain_10 ::
(MAlonzo.Code.Utils.T__'215'__436
(MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10)
MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
MAlonzo.Code.RawU.T_Untyped_210 ->
[MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122] ->
Expand All @@ -104,15 +104,15 @@ d_runCertifierMain_10 v0 v1
MAlonzo.Code.Utils.C__'44'__450
(coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(coe
MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1)))
MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1)))
MAlonzo.Code.VerifiedCompilation.C_abort_10 v4
-> coe
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(coe
MAlonzo.Code.Utils.C__'44'__450
(coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(coe
MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1)))
MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1)))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Utils.C_inj'8322'_14 v3
-> coe
Expand All @@ -123,5 +123,5 @@ d_runCertifierMain_10 v0 v1
MAlonzo.Code.Utils.C__'44'__450
(coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
(coe
MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1))))
MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1))))
_ -> MAlonzo.RTE.mazUnreachableError)
Loading
Loading