test: MBT: Add partial set security to model #1614

p-offtermatt · 2024-01-31T13:58:17Z

Description

Closes: #1574

Adds partial set security to the Quint model.

This PR only contains logic, tests, and sanity checks, but no invariants yet.
The invariants are becoming more subtle and harder to define, so I want to see whether to prioritise MBT or defining the invariants first.

Highlights:

ccv_pss contains the logic for calculating the top N set. Notice it can be much simpler because I don't need synthetic updates, I just send the whole set
in ccv.qnt, some things changed to accomodate sending the partial validator sets

Author Checklist

All items are required. Please add a note to the item if the item is not applicable and
please add links to any relevant follow up issues.

I have...

Included the correct type prefix in the PR title
Targeted the correct branch (see PR Targeting)
Provided a link to the relevant issue or specification
Reviewed "Files changed" and left comments if necessary
Confirmed all CI checks have passed (test failure for MBT is expected)

Reviewers Checklist

All items are required. Please add a note if the item is not applicable and please add
your handle next to the items reviewed if you only reviewed selected items.

I have...

Confirmed the correct type prefix in the PR title
Confirmed all author checklist items have been addressed
Confirmed that this PR does not change production code

Co-authored-by: insumity <insumity@users.noreply.github.com>

tests/mbt/model/libraries/extraSpells.qnt

insumity · 2024-02-06T10:00:04Z

tests/mbt/model/libraries/extraSpells.qnt

@@ -139,6 +139,71 @@ module extraSpells {
        __set.fold(List(), (__l, __e) => __l.append(__e))
    }

+  /// The type of orderings between comparable things


Why the /// here and later instead of //?

Good question, this is copy-pasted from the Quint "standard library" (there is no actual standard library yet, so copy-pasting what you need is atm the canonical way of using it) and their style differs sometimes

I see. I guess in this case we could adhere to our own standard with just //.

Co-authored-by: insumity <insumity@users.noreply.github.com>

…urity into ph/mbt-pss

insumity · 2024-02-06T10:49:00Z

tests/mbt/model/ccv_pss.qnt

+    import extraSpells.* from "./libraries/extraSpells"
+    import ccv_utils.* from "./ccv_utils"
+
+    // Given a base validator set, an N for a top N chain, and a set of validators that have opted in to the chain,


The way I read this, I would expect that an N parameter to this function which is not the case.

insumity · 2024-02-06T10:49:41Z

tests/mbt/model/ccv_pss.qnt

+    // Given a base validator set, an N for a top N chain, and a set of validators that have opted in to the chain,
+    // returns the validator set that should be sent to the chain.
+    // Assumes that the value for N is valid.
+    pure def GetPSSValidatorSet(providerState: ProviderState, origValSet: ValidatorSet, consumer: Chain): ValidatorSet = {


Why do we need to take the origValSet as a parameter here? Isn't this something we can extract from the providerState?

tests/mbt/model/ccv_pss.qnt

insumity · 2024-02-06T11:37:51Z

tests/mbt/model/ccv_pss.qnt

+        res._1
+    }
+
+    // Opts a validator in for a consumer chain the provider.


Suggested change

// Opts a validator in for a consumer chain the provider.

// Opts a validator in for a consumer chain of the provider.

insumity · 2024-02-06T11:41:08Z

tests/mbt/model/ccv_pss.qnt

+        val topNVals = GetTopNVals(proviValSet, providerState.topNByConsumer.get(consumer))
+        val prevOptedInVals = providerState.optedInVals.getOrElse(consumer, Set())
+        // opt in all the top N validators, i.e. union the top N vals with the previous opted in vals
+        val newOptedInVals = providerState.optedInVals.put(consumer, prevOptedInVals.union(topNVals))


I guess because we have sets here, we're guaranteed that a validator that IsTopN and has opted in only appears once at the optedInVals, right?

Yup, exactly!

insumity · 2024-02-06T11:43:15Z

tests/mbt/model/ccv_pss.qnt

+        currentState.providerState.optedInVals.getOrElse(consumer, Set()).contains(validator)
+    }
+
+    // Opts a validator out. Safe to call before the consumer chain even runs.


Safe to call before the consumer chain even runs.

Regarding the implementation of this (although we do not have the code yet), I was thinking that we should not allow validators to opt out before the chain has started running. This is because, we assume validator that voted Yes on a ConsumerAdditionProposal are opted in by default, so it would be weird to give them the right to opt out before the chain starts. What do you think?

Good point. My thought was to use this, at the time the consumer starts, to determine who voted yes on the proposal (and is thus opted in), but maybe I am cutting too many corners here and it is not as clear.
But essentially I think this is an implementation detail and maybe abstracting away like I did is ok, but I would love to know if you disagree

at the time the consumer starts, to determine who voted yes on the proposal (and is thus opted in) [...]

Thanks for your answer. This makes sense. We can leave as is :)

tests/mbt/model/ccv_pss_model.qnt

insumity · 2024-02-06T11:52:54Z

tests/mbt/model/ccv_pss_test.qnt

+
+    run TopNTest = 
+        val valSet =
+            Map("a" -> 5, "a1" -> 5, "a2" -> 5, "b" -> 10, "b1" -> 10, "b2" -> 10, "c" -> 15, "c1" -> 15, "e" -> 25)


nit: Why e is the last one and not d?

Might make sense to have the map written in descending order so it would be slightly clearer that e would be the first validator to be returned, then e, c1 and c, etc.

d was rationalized away at some point and I didn't change this :D
yeah, sorting the map the other way around is also a great point

insumity · 2024-02-06T11:53:30Z

tests/mbt/model/ccv_pss_test.qnt

+            assert(GetTopNVals(valSet, 85) == Set("e", "c1", "c", "b2", "b1", "b")),
+            assert(GetTopNVals(valSet, 86) == Set("e", "c1", "c", "b2", "b1", "b", "a2", "a1", "a")),
+            assert(GetTopNVals(valSet, 95) == Set("e", "c1", "c", "b2", "b1", "b", "a2", "a1", "a")),
+            assert(GetTopNVals(valSet, 100) == Set("e", "c1", "c", "b2", "b1", "b", "a2", "a1", "a")),


nit: Why not GetTopNVals(valSet, 100) == valSet?

Sure. need to be valSet.keys(), because valSets are actually maps.. but still more descriptive :)

insumity

Great work! Thanks @p-offtermatt.

Would it make sense to merge this under the feat/partial-set-security branch? I'm suggesting this because it might take quite some time until we merge feat/partial-set-security back to main so it might complicate your upcoming MBT work.

p-offtermatt · 2024-02-06T12:47:42Z

Great work! Thanks @p-offtermatt.

Would it make sense to merge this under the feat/partial-set-security branch? I'm suggesting this because it might take quite some time until we merge feat/partial-set-security back to main so it might complicate your upcoming MBT work.

Great point - let me retarget this.

p-offtermatt · 2024-02-06T13:11:57Z

Great work! Thanks @p-offtermatt.
Would it make sense to merge this under the feat/partial-set-security branch? I'm suggesting this because it might take quite some time until we merge feat/partial-set-security back to main so it might complicate your upcoming MBT work.

Great point - let me retarget this.

That gave a lot of modified files, I think I will rather just make a new branch with the correct branch and cherry-pick.

p-offtermatt · 2024-02-06T13:29:34Z

Closed in favor of #1627

p-offtermatt and others added 30 commits January 9, 2024 11:05

Start implementing key assignment in Quint

214f6e5

Update model

79e8044

Update model

e52e0ce

Update model

ed0901e

Add key assignment to functional layer

c4423ff

Start writing test for key assignment

e9a7699

Continue adding key assignment to model

05feedb

Fix some behaviours in key assignment logic

dba46b5

Pull key assignment into its own module

ba6e684

Split key assignment into extra module

c9ae38c

Start updating invariants for key assignment

b9914a2

Update key assignment spec

7b23574

Merge key assignment into main model

9c21742

Update spec, fix bug

6a0eb29

Fix map building for key assignment

db78b88

Fix key assignment invariants

2869fac

Update driver to include key assignment

1f368de

Fix key assignment in bounded steps

ff0489e

Finish key assignment integration in driver

35e5d6c

Update clients every block

147569d

Add key assignment to invariant check

6c110f7

Use key assignment in its step

7cf2855

Fix merge

bb722a4

Revert changes to extraSpells

36a7041

Add check to avoid empty set of running consumers

36b5d92

Update tests/mbt/model/ccv.qnt

a90e79d

Co-authored-by: insumity <insumity@users.noreply.github.com>

Update tests/mbt/model/ccv.qnt

dc62877

Co-authored-by: insumity <insumity@users.noreply.github.com>

Start adapting spec to pss

ec67531

Continue modelling partial set security

33ace67

Incorporate review comments

e7c220d

p-offtermatt marked this pull request as ready for review February 5, 2024 13:31

p-offtermatt requested a review from a team as a code owner February 5, 2024 13:31

insumity reviewed Feb 6, 2024

View reviewed changes

tests/mbt/model/libraries/extraSpells.qnt Show resolved Hide resolved

insumity reviewed Feb 6, 2024

View reviewed changes

tests/mbt/model/libraries/extraSpells.qnt Outdated Show resolved Hide resolved

insumity reviewed Feb 6, 2024

View reviewed changes

tests/mbt/model/libraries/extraSpells.qnt Outdated Show resolved Hide resolved

insumity reviewed Feb 6, 2024

View reviewed changes

p-offtermatt and others added 3 commits February 6, 2024 11:22

Update tests/mbt/model/libraries/extraSpells.qnt

7f57098

Co-authored-by: insumity <insumity@users.noreply.github.com>

Add another test for sortedListInsert

f91b909

Merge branch 'ph/mbt-pss' of https://github.com/cosmos/interchain-sec…

9da2959

…urity into ph/mbt-pss

github-actions bot added the C:Build Assigned automatically by the PR labeler label Feb 6, 2024

Unify comments for __cmp

ad1b555

insumity reviewed Feb 6, 2024

View reviewed changes

tests/mbt/model/ccv_pss.qnt Outdated Show resolved Hide resolved

insumity reviewed Feb 6, 2024

View reviewed changes

tests/mbt/model/ccv_pss_model.qnt Outdated Show resolved Hide resolved

insumity reviewed Feb 6, 2024

View reviewed changes

insumity approved these changes Feb 6, 2024

View reviewed changes

p-offtermatt added 3 commits February 6, 2024 13:08

Reformulate top N comment

8d65f07

Revert map order, better naming for possible values

cf3cb18

Rename e -> d

5f0fb0e

p-offtermatt changed the base branch from main to feat/partial-set-security February 6, 2024 12:47

p-offtermatt changed the base branch from feat/partial-set-security to main February 6, 2024 13:11

p-offtermatt closed this Feb 6, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

test: MBT: Add partial set security to model #1614

test: MBT: Add partial set security to model #1614

p-offtermatt commented Jan 31, 2024 •

edited

Loading

insumity Feb 6, 2024

p-offtermatt Feb 6, 2024

insumity Feb 6, 2024

insumity Feb 6, 2024

insumity Feb 6, 2024

insumity Feb 6, 2024

insumity Feb 6, 2024

p-offtermatt Feb 6, 2024

insumity Feb 6, 2024

p-offtermatt Feb 6, 2024

insumity Feb 6, 2024 •

edited

Loading

insumity Feb 6, 2024

insumity Feb 6, 2024

p-offtermatt Feb 6, 2024

insumity Feb 6, 2024

p-offtermatt Feb 6, 2024

insumity left a comment

p-offtermatt commented Feb 6, 2024

p-offtermatt commented Feb 6, 2024

p-offtermatt commented Feb 6, 2024

	// Opts a validator in for a consumer chain the provider.
	// Opts a validator in for a consumer chain of the provider.

test: MBT: Add partial set security to model #1614

test: MBT: Add partial set security to model #1614

Conversation

p-offtermatt commented Jan 31, 2024 • edited Loading

Description

Author Checklist

Reviewers Checklist

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

insumity Feb 6, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

insumity left a comment

Choose a reason for hiding this comment

p-offtermatt commented Feb 6, 2024

p-offtermatt commented Feb 6, 2024

p-offtermatt commented Feb 6, 2024

p-offtermatt commented Jan 31, 2024 •

edited

Loading

insumity Feb 6, 2024 •

edited

Loading