Skip to content

Commit

Permalink
corrections
Browse files Browse the repository at this point in the history
  • Loading branch information
PetarMax committed Aug 24, 2023
1 parent 25c1cc8 commit b8fe221
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion include/kframework/lemmas/lemmas.k
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ module LEMMAS [symbolic]
rule chop(_V) <Int pow256 => true [simplification]

rule X *Int Y <Int pow256 => true requires Y <=Int maxUInt256 /Int X [simplification]
rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification]jj
rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification]

// ########################
// Set Reasoning
Expand Down
2 changes: 1 addition & 1 deletion include/kframework/serialization.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ Address/Hash Helpers

```k
syntax Int ::= keccak ( Bytes ) [function, total, injective, smtlib(smt_keccak)]
// -------------------------------------------------------------------------
// --------------------------------------------------------------------------------
rule [keccak]: keccak(WS) => #parseHexWord(Keccak256(#unparseByteStack(WS))) [concrete]
```

Expand Down

0 comments on commit b8fe221

Please sign in to comment.