Skip to content
Permalink
Browse files

data.md: Remove excess chops for monotonically decreasing word ops (#387

)

* data.md: Remove excess chops for monotonically decreasing word ops

* Update data.md

* formatting; edit comment
  • Loading branch information...
MrChico authored and ehildenb committed Jul 11, 2019
1 parent 15d98f3 commit 8b73f8efb25711ef3faca9fe1540cc1df969cd85
Showing with 11 additions and 10 deletions.
  1. +11 −10 data.md
21 data.md
@@ -234,6 +234,7 @@ You could alternatively calculate `I1 modInt I2`, then add one to the normal int
```

The corresponding `<op>Word` operations automatically perform the correct modulus for EVM words.
Warning: operands are assumed to be within the range of a 256 bit EVM word. Unbound integers may not return the correct result.

```k
syntax Int ::= Int "+Word" Int [function]
@@ -243,13 +244,13 @@ The corresponding `<op>Word` operations automatically perform the correct modulu
| Int "%Word" Int [function]
// -----------------------------------------
rule W0 +Word W1 => chop( W0 +Int W1 )
rule W0 -Word W1 => chop( W0 -Int W1 ) requires W0 >=Int W1
rule W0 -Word W1 => W0 -Int W1 requires W0 >=Int W1
rule W0 -Word W1 => chop( (W0 +Int pow256) -Int W1 ) requires W0 <Int W1
rule W0 *Word W1 => chop( W0 *Int W1 )
rule W0 /Word W1 => 0 requires W1 ==Int 0
rule W0 /Word W1 => chop( W0 /Int W1 ) requires W1 =/=Int 0
rule W0 %Word W1 => 0 requires W1 ==Int 0
rule W0 %Word W1 => chop( W0 modInt W1 ) requires W1 =/=Int 0
rule W0 /Word W1 => 0 requires W1 ==Int 0
rule W0 /Word W1 => W0 /Int W1 requires W1 =/=Int 0
rule W0 %Word W1 => 0 requires W1 ==Int 0
rule W0 %Word W1 => W0 modInt W1 requires W1 =/=Int 0
```

Care is needed for `^Word` to avoid big exponentiation.
@@ -324,13 +325,13 @@ Bitwise logical operators are lifted from the integer versions.
| Int ">>Word" Int [function]
| Int ">>sWord" Int [function]
// -------------------------------------------
rule ~Word W => chop( W xorInt (pow256 -Int 1) )
rule W0 |Word W1 => chop( W0 |Int W1 )
rule W0 &Word W1 => chop( W0 &Int W1 )
rule W0 xorWord W1 => chop( W0 xorInt W1 )
rule ~Word W => W xorInt maxUInt256
rule W0 |Word W1 => W0 |Int W1
rule W0 &Word W1 => W0 &Int W1
rule W0 xorWord W1 => W0 xorInt W1
rule W0 <<Word W1 => chop( W0 <<Int W1 ) requires W1 <Int 256
rule W0 <<Word W1 => 0 requires W1 >=Int 256
rule W0 >>Word W1 => chop( W0 >>Int W1 )
rule W0 >>Word W1 => W0 >>Int W1
rule W0 >>sWord W1 => chop( (abs(W0) *Int sgn(W0)) >>Int W1 )
```

0 comments on commit 8b73f8e

Please sign in to comment.
You can’t perform that action at this time.