Skip to content

Handled additional Range constructor in toSigners side condition.#944

Draft
mariaKt wants to merge 1 commit intofeature/p-tokenfrom
mk/all-keys-range
Draft

Handled additional Range constructor in toSigners side condition.#944
mariaKt wants to merge 1 commit intofeature/p-tokenfrom
mk/all-keys-range

Conversation

@mariaKt
Copy link
Collaborator

@mariaKt mariaKt commented Feb 19, 2026

This PR replaces the allKeys condition in the requires clause of toSigners with another function, allRangeWrappedKeys, that works in exactly the same way except is unwraps an additional Range constructor from the provided ListItem. This Range is generated from fromKey, and the existing allKeys implementation was not sufficient to handle it, as it was expecting just a List.

The issue came up when investigating the failure of the proof for test_process_initialize_multisig2. I attach a file that contains a part of the stuck configuration, where I isolated a term that shows the issue. The relevant term is SignersError(...). With this change, the proof was able to pass.
signers-error.txt

Note: I chose to use a new function rather than extend the functionality of allKeys beyond its (apparent) intend to handle Lists, but I believe that the issue could be solved with just another rule in allKeys, if that is what you prefer.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

Comments