-
Notifications
You must be signed in to change notification settings - Fork 11
LTL helper functions #501
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.
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
base: main
Are you sure you want to change the base?
LTL helper functions #501
Conversation
0814b7c to
6529694
Compare
src/Cooked/MockChain/Staged.hs
Outdated
| -- | Apply an Ltl modification somewhere in the given Trace. The modification | ||
| -- must apply at least once. | ||
| somewhere' :: (MonadModal m) => Ltl (Modification m) -> m a -> m a | ||
| somewhere' ltl = modifyLtl (LtlUntil LtlTruth ltl) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Having modifyLtl hinders composability. This is also true for the current version in origin/master.
It may be better to have smart constructors for data Ltl, eg:
atom :: C.Tweak m a -> C.Ltl (C.UntypedTweak m)
atom = C.LtlAtom . C.UntypedTweak
somewhere :: C.Ltl a -> C.Ltl a
somewhere = C.LtlUntil C.LtlTruth
fork :: C.Ltl a -> C.Ltl a -> C.Ltl a
fork = C.LtlOr
everywhere = ...
Then we could do something like:
tryHijack :: C.Ltl (C.UntypedTweak C.InterpMockChain)
tryHijack =
fork
(atom $ C.datumHijackingAttack $ C.scriptsDatumHijackingParams carrie)
(atom $ C.datumHijackingAttack $ C.scriptsDatumHijackingParams $ Script.trueSpendingMPScript @())
tryAddToken :: C.Ltl (C.UntypedTweak C.InterpMockChain)
tryAddToken = atom $ C.addTokenAttack f bob
where
f vs
| vs == oracleVScript = [(Api.tokenName "Dummy", 10)]
| otherwise = []
tryDupToken :: C.Ltl (C.UntypedTweak C.InterpMockChain)
tryDupToken = atom $ C.dupTokenAttack f alice
where
f _ _ i = i + 1
Essentially, have composable combinators to build the Ltl expressions and use modifyLtl at the end.
Eg:
C.modifyLtl (somewhere tryHijack) T.closeOracle
C.modifyLtl (somewhere (fork tryAddToken tryDupToken)) T.closeOracle
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah I like this, it'd be a pretty big change to the interface of the library though, so something I'd want @mmontin to decide on.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I really like this work, and believe this is a good first PR.
I made a few in line comments, and questioned some of the additions within the code.
Additionally, I would like to see some small test cases added in relevant places.
src/Cooked/MockChain/Staged.hs
Outdated
| -- > } | ||
| -- > | ||
| -- > someTest = someEndpoint & labled @Text "InitialMinting" someTweak | ||
| labeled :: (LabelConstrs lbl, MonadModalBlockChain m) => lbl -> Tweak InterpMockChain b -> m a -> m a |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
While I like the idea behind labeled I don't like the current implementation. This forces the tweak to be applied everywhere by default, while we already have all the machinery to selectively apply it where we please. There are two options:
- It should instead only be made a tweak (in
Tweak.Labelfor instance?) but that would not technically work on the labels and thus would not entirely fit our file structure. - Not have any tweak at all, since
hasLabelTweak >> tweakis extremely straightforward. I would lean towards that option.
As a summary: the value in your proposal is to use labels as a means of selecting transactions on which we apply tweaks, which is very interesting and which we have not yet done, for some reason. However, I believe we already have all the necessary machinery to have this working out of the box, without the need of additional helpers, so I would be in favor of removing this one.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
While I agree the functionality already exists, I think there is still some value in having a combinator which helps with readability - somewhere, everywhere and there can also already be written with just tweaks/modifyLtl, but being able to write
...
( "We can't redirect a script output before close",
T.updateOracle & C.somewhere do
datumHijackingAttack $ scriptsDatumHijackingParams carrie
),
( "We can't redirect a script output with close",
T.closeOracle2 & C.labeled "OracleFlow" do
x <- datumHijackingAttack $ scriptsDatumHijackingParams john
someOtherAttack x
),
( "We do another thing",
T.closeOracle2 & C.labeled "NFTFlow" do
x <- datumHijackingAttack $ scriptsDatumHijackingParams paul
yetAnotherattack x
),
...keeps the same pattern as those other combinators, and makes the intent clear - I only want these attacks to be applied to transactions in a specific flow/group. Redundancy is not necessarily a bad thing, and it seems like this is a very common thing to want to be able to do, from the discussions of using there. I think having named helpers for common patterns is really useful in a library like this - the alternative feels more clunky to me with the other combinators already provided:
( "We can't redirect a script output with close",
T.closeOracle2 & everywhere do
hadLabelTweak SomeLabel
x <- datumHijackingAttack $ scriptsDatumHijackingParams john
someOtherAttack x
),
...Separating the "when" from the "what" feels cleaner. Here we've got two conflicting statements, "Apply this everywhere", "but only when it has this label" (writing this I'm not sure this example makes sense, but I'm not sure now how to write the "apply this tweak to every transaction with a given label" - I guess it would be
( "We can't redirect a script output with close",
T.closeOracle2 & everywhere ((do
hadLabelTweak SomeLabel
x <- datumHijackingAttack $ scriptsDatumHijackingParams john
someOtherAttack x) <|> doNothingTweak)
),
...? I'm sure there's something cleaner)
Having thought about the interface over the weekend, I think it would be worthwhile having two versions of labelled (I need to fix the name...), to remove the need for the type application:
labeled :: (MonadModalBlockChain m) => Text -> Tweak InterpMockChain b -> m a -> m a
labelled = labelled'
labeled' :: (LabelConstrs lbl, MonadModalBlockChain m) => lbl -> Tweak InterpMockChain b -> m a -> m a
labelled lbl = ...with helpers in the Labels module to make adding Text labels to transactions easy.
504ded2 to
e1580f6
Compare
Adds functions for making writing LTL expressions easier. In
Cooked.MockChain.Stagedit adds various prime versions of combinators for applying LTL expressionseverywhere,somewhereorthere` at a specific transaction (and then implements the original function using these helpers).the new
Cooked.Ltl.Combinatorsjust adds functions for taking lists of actions or Ltl values, and combining them disjunctively or conjunctively usinganyOf[']andallOf[']respectively.