Skip to content

Commit ea55a76

Browse files
virgil-serbanutaehildenb
authored andcommitted
Fix the SIGNEXTEND kore/haskell backend test. (#434)
* Fix the SIGNEXTEND kore/haskell backend test. * data: formatting
1 parent b31f51b commit ea55a76

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

data.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -373,9 +373,9 @@ Bitwise logical operators are lifted from the integer versions.
373373
```k
374374
syntax Int ::= signextend( Int , Int ) [function]
375375
// -------------------------------------------------
376-
rule signextend(N, W) => W requires N >=Int 32 orBool N <Int 0
377-
rule signextend(N, W) => chop( (#nBytes(31 -Int N) <<Byte (N +Int 1)) |Int W ) requires N <Int 32 andBool N >=Int 0 andBool word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W))
378-
rule signextend(N, W) => chop( #nBytes(N +Int 1) &Int W ) requires N <Int 32 andBool N >=Int 0 andBool notBool word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W))
376+
rule signextend(N, W) => W requires N >=Int 32 orBool N <Int 0 [concrete]
377+
rule signextend(N, W) => chop( (#nBytes(31 -Int N) <<Byte (N +Int 1)) |Int W ) requires N <Int 32 andBool N >=Int 0 andBool word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W)) [concrete]
378+
rule signextend(N, W) => chop( #nBytes(N +Int 1) &Int W ) requires N <Int 32 andBool N >=Int 0 andBool notBool word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W)) [concrete]
379379
```
380380

381381
- `keccak` serves as a wrapper around the `Keccak256` in `KRYPTO`.

0 commit comments

Comments
 (0)