Skip to content

Conversation

lucasmt
Copy link
Contributor

@lucasmt lucasmt commented Sep 17, 2025

This PR removes lemma 6 from keccak.md. Unlike other keccak lemmas, which are technically unsound but safe under keccak's cryptographic properties, this lemma can cause tests to miss certain valid edge cases and pass when they should fail. This PR also introduces a new test SlotsDisjointTest.testReceiver as an example (found by @lisandrasilva). With lemma 6, the test passes, but it should fail now that the lemma has been removed.

If a situation arises that requires this lemma, there are a few alternatives:

  • You can add this lemma to a lemmas.k file in the project, but make extra sure that there aren't edge cases that might be missed like in the provided example. This decision must be made intentionally in a project-by-project basis, rather than having this lemma upstreamed into Kontrol where it will be included by default, possibly without the user's knowledge.
  • Add assumptions to the test for the specific cases that trigger the lemma. This is preferable because it makes the assumptions explicit and they only apply in the scope of the test (rather than a lemma that applies to the whole project). On the other hand, it might be more tedious and increase verbosity, especially if multiple such assumptions are needed.
  • In the future, allowing the keccak function to remain unevaluated even for concrete inputs would allow many such cases to be covered by the other keccak lemmas (such as lemma 5).

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