Skip to content

Commit 0ab98ac

Browse files
committed
Add smtlib markers to Word operations
1 parent 893fa46 commit 0ab98ac

File tree

1 file changed

+8
-8
lines changed

1 file changed

+8
-8
lines changed

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -160,14 +160,14 @@ The `<op>Word` comparisons similarly lift K operators to EVM ones:
160160
Bitwise logical operators are lifted from the integer versions.
161161

162162
```k
163-
syntax Int ::= "~Word" Int [function, total]
164-
| Int "|Word" Int [function, total]
165-
| Int "&Word" Int [function, total]
166-
| Int "xorWord" Int [function, total]
167-
| Int "<<Word" Int [function, total]
168-
| Int ">>Word" Int [function, total]
169-
| Int ">>sWord" Int [function, total]
170-
// --------------------------------------------------
163+
syntax Int ::= "~Word" Int [function, total, smtlib(notWord)]
164+
| Int "|Word" Int [function, total, smtlib(orWord)]
165+
| Int "&Word" Int [function, total, smtlib(andWord)]
166+
| Int "xorWord" Int [function, total, smtlib(xorWord)]
167+
| Int "<<Word" Int [function, total, smtlib(shlWord)]
168+
| Int ">>Word" Int [function, total, smtlib(shrWord)]
169+
| Int ">>sWord" Int [function, total, smtlib(shrsWord)]
170+
// --------------------------------------------------------------------
171171
rule ~Word W => W xorInt maxUInt256
172172
rule W0 |Word W1 => W0 |Int W1
173173
rule W0 &Word W1 => W0 &Int W1

0 commit comments

Comments
 (0)