Skip to content

Commit 1661b80

Browse files
authored
Handled additional Range constructor in toSigners side condition. (#944)
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](https://github.com/user-attachments/files/25424362/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.
1 parent 133e94d commit 1661b80

1 file changed

Lines changed: 7 additions & 1 deletion

File tree

  • kmir/src/kmir/kdist/mir-semantics/symbolic

kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ This ensures that branches on the key value are not duplicated.
130130
131131
syntax Signers ::= toSigners ( Value ) [function, total]
132132
// -----------------------------------------------------
133-
rule toSigners(Range(ELEMS)) => Signers( toKeys(ELEMS) ) requires size(ELEMS) ==Int 11 andBool allKeys(ELEMS)
133+
rule toSigners(Range(ELEMS)) => Signers( toKeys(ELEMS) ) requires size(ELEMS) ==Int 11 andBool allRangeWrappedKeys(ELEMS)
134134
rule toSigners(VAL) => SignersError(VAL) [owise]
135135
136136
syntax Value ::= fromSigners ( Signers ) [function, total]
@@ -155,6 +155,12 @@ This ensures that branches on the key value are not duplicated.
155155
rule allKeys( .List ) => true
156156
rule allKeys( ListItem(ELEMS) REST:List ) => allKeys(REST) requires size(ELEMS) ==Int 32 andBool allBytes(ELEMS)
157157
rule allKeys( ListItem(_OTHER) _:List ) => false [owise]
158+
159+
syntax Bool ::= allRangeWrappedKeys ( List ) [function, total]
160+
// -----------------------------------------------------------
161+
rule allRangeWrappedKeys( .List ) => true
162+
rule allRangeWrappedKeys( ListItem(Range(ELEMS)) REST:List ) => allRangeWrappedKeys(REST) requires size(ELEMS) ==Int 32 andBool allBytes(ELEMS)
163+
rule allRangeWrappedKeys( ListItem(_OTHER) _:List ) => false [owise]
158164
```
159165

160166
### SPL Token Interface Account

0 commit comments

Comments
 (0)