test: add key assignment to model and driver

[p-offtermatt]

Description

Closes: #1529

• Adds key assignment to the Quint model
• Adds key assignment to the MBT driver

---

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

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

[mpoke]

Great work @p-offtermatt. Partial review without ccv_model.qnt. See my comments below. In general, try to either comment large blocks of quint or split the blocks -- it's very hard for me (Quint beginner) to read it.

[insumity]

Great work!

I focused my review on the Quint code.
I concur with Mariu's comment in regards to introducing more comments in general.

Two last comments:

1. I'm not sure if it would simplify the model in not considering 0 powers. If I understood correctly from our discussion, this stems from ABCI which might be too implementation specific. If it doesn't simplify, then it's fine to leave as is.
2. Now addr and key seem to be used interchangeably in names. Would it make sense to stick with one for consistency?

[p-offtermatt]

Great work!

I focused my review on the Quint code. I concur with Mariu's comment in regards to introducing more comments in general.

Two last comments:

1. I'm not sure if it would simplify the model in not considering `0` powers. If I understood correctly from our discussion, this stems from ABCI which might be too implementation specific. If it doesn't simplify, then it's fine to leave as is.

2. Now `addr` and `key` seem to be used interchangeably in names. Would it make sense to stick with one for consistency?

1. Yes, I think this would simplify a lot. Let me do that - it will be some bigger changes, e.g. I can get rid of keyAssignmentReplacements afaict.
2. I think both are sort-of needed: The feature is called key assignment, but in the model I think I don't want to talk about keys, but rather addresses, but maybe this is confusing. Let me think about this a bit, but feel free to chime in if you have an opinion @mpoke @sainoe

[mpoke]

Great work @p-offtermatt.