Skip to content

Conversation

@morganthomas
Copy link
Contributor

@morganthomas morganthomas commented Oct 23, 2025

Closes #76 .

These changes save exactly 1,000 cycles for the 500 XMSS aggregation test, while reducing bytecode size by 1 and leaving memory usage the same.

These changes make it the XMSS aggregation verifier's responsibility to ensure that the bitield values in the public input are in fact bits.

Unfortunately, the most frequent usage of the if X == 1 idiom in the XMSS aggregation test were not apparently in a context where X can be assumed to be boolean. This is in the condition if merkle_are_left[h] == 1. Changing this to if merkle_are_left[h] resulted in an increased cycle count. Changing this to if !!assume_bool(merkle_are_left[h]) resulted in a more substantially decreased cycle count, but I expect it also would give up soundness.

These changes increase the cycle count by 12 for the WHIR recursion test, while leaving bytecode size and memory usage the same.

I don't know why these changes increase the cycle count by 12 for the WHIR recursion test. I did find usages of the if X == 1 idiom in the WHIR recursion test where X could safely be assumed to be boolean, but for whatever reason, replacing these instances with if !!assume_bool(X) resulted in an increased cycle count.

@morganthomas morganthomas changed the title Morgan/76 Issue #76: Boolean expressions in conditional statements Oct 23, 2025
@morganthomas morganthomas force-pushed the morgan/76 branch 2 times, most recently from 8a011d2 to 5db6fab Compare October 23, 2025 18:55
@morganthomas morganthomas marked this pull request as ready for review October 23, 2025 19:07
@TomWambsgans TomWambsgans merged commit 7330d74 into leanEthereum:main Oct 23, 2025
3 checks passed
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.

Use arbitrary expressions as conditions in if statements

2 participants