Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix kompile warnings. #1001

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Fix kompile warnings. #1001

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
efa8a89
fix build warnings
anvacaru Mar 24, 2025
96eba6b
Merge branch 'master' into warnings_fix
palinatolmach Mar 24, 2025
cba22b0
Merge branch 'master' into warnings_fix
anvacaru Mar 27, 2025
6cf7db4
Merge branch 'master' into warnings_fix
anvacaru Apr 1, 2025
ab198fa
Merge branch 'master' into warnings_fix
anvacaru Apr 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/kontrol/kdist/keccak.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,8 @@ module KECCAK-LEMMAS
4. The result of a `keccak` is assumed not to fall too close to the edges of its official range. This accounts for the shifts added to the result of a `keccak` when accessing storage slots, and is a hypothesis made by the ecosystem.

```k
rule BOUND:Int <Int keccak(B:Bytes) => true requires BOUND <=Int 32 [simplification, concrete(BOUND)]
rule keccak(B:Bytes) <Int BOUND:Int => true requires BOUND >=Int pow256 -Int 32 [simplification, concrete(BOUND)]
rule BOUND:Int <Int keccak(_B:Bytes) => true requires BOUND <=Int 32 [simplification, concrete(BOUND)]
rule keccak(_B:Bytes) <Int BOUND:Int => true requires BOUND >=Int pow256 -Int 32 [simplification, concrete(BOUND)]
```

5. `keccak` is injective: that is, if `keccak(A)` equals `keccak(B)`, then `A` equals `B`.
Expand Down
8 changes: 4 additions & 4 deletions src/kontrol/kdist/kontrol_lemmas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ module KONTROL-AUX-LEMMAS
requires C +Int D ==Int 0 [simplification, preserves-definedness]

// modInt
rule (X *Int Y) modInt Z => 0 requires X modInt Z ==Int 0 [simplification, concrete(X, Z), preserves-definedness]
rule (X *Int _Y) modInt Z => 0 requires X modInt Z ==Int 0 [simplification, concrete(X, Z), preserves-definedness]

// >>Int
rule [shift-to-div]: X >>Int N => X /Int (2 ^Int N)
Expand Down Expand Up @@ -197,9 +197,9 @@ module KONTROL-AUX-LEMMAS
rule KI:KItem in ListItem(KJ:KItem) => KI ==K KJ [simplification]

// Recursive list membership check for lists with multiple elements
rule KI:KItem in (ListItem(KI) Rest) => true [simplification]
rule KI:KItem in (ListItem(KJ) Rest) => KI in Rest [simplification]
rule KI:KItem in .List => false [simplification]
rule KI:KItem in (ListItem(KI) _REST) => true [simplification]
rule KI:KItem in (ListItem(_KJ) REST) => KI in REST [simplification]
rule _KI:KItem in .List => false [simplification]

endmodule
```
Loading