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

Jump to bottom

Fix documentation for #range and codeblocks #1153

Merged
merged 3 commits into from
Nov 3, 2021
Merged

Fix documentation for #range and codeblocks #1153

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
37b0b7a
Fix documentation for #rage and codeblocks
andreiburdusa Nov 3, 2021
4c20949
Merge branch 'master' into rage-codeblocks-documentation
andreiburdusa Nov 3, 2021
06b8fa2
Merge branch 'master' into rage-codeblocks-documentation
ehildenb Nov 3, 2021
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
24 changes: 12 additions & 12 deletions evm-types.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,7 @@ These can be used for pattern-matching on the LHS of rules as well (`macro` attr
rule #range ( LB <= X <= UB ) => LB <=Int X andBool X <=Int UB [macro]
```

- `chop` interprets an integer modulo $2^256$.
- `chop` interprets an integer modulo `2^256`.

```k
syntax Int ::= chop ( Int ) [function, functional, smtlib(chop)]
Expand Down Expand Up @@ -320,8 +320,8 @@ Bitwise logical operators are lifted from the integer versions.
rule W0 >>sWord W1 => chop( (abs(W0) *Int sgn(W0)) >>Int W1 )
```

- `bit` gets bit $N$ (0 being MSB).
- `byte` gets byte $N$ (0 being the MSB).
- `bit` gets bit `N` (0 being MSB).
- `byte` gets byte `N` (0 being the MSB).

```k
syntax Int ::= bit ( Int , Int ) [function]
Expand All @@ -334,8 +334,8 @@ Bitwise logical operators are lifted from the integer versions.
rule byte(N, W) => bitRangeInt(W , ( 31 -Int N) *Int 8 , 8) requires N >=Int 0 andBool N <Int 32
```

- `#nBits` shifts in $N$ ones from the right.
- `#nBytes` shifts in $N$ bytes of ones from the right.
- `#nBits` shifts in `N` ones from the right.
- `#nBytes` shifts in `N` bytes of ones from the right.
- `_<<Byte_` shifts an integer 8 bits to the left.
- `_>>Byte_` shifts an integer 8 bits to the right.

Expand All @@ -351,7 +351,7 @@ Bitwise logical operators are lifted from the integer versions.
rule N >>Byte M => N >>Int (8 *Int M)
```

- `signextend(N, W)` sign-extends from byte $N$ of $W$ (0 being MSB).
- `signextend(N, W)` sign-extends from byte `N` of `W` (0 being MSB).

```k
syntax Int ::= signextend( Int , Int ) [function, functional]
Expand Down Expand Up @@ -384,8 +384,8 @@ A cons-list is used for the EVM wordstack.
rule I : BS => Int2Bytes(1, I, BE) ++ BS requires I <Int 256
```

- `#take(N , WS)` keeps the first $N$ elements of a `WordStack` (passing with zeros as needed).
- `#drop(N , WS)` removes the first $N$ elements of a `WordStack`.
- `#take(N , WS)` keeps the first `N` elements of a `WordStack` (passing with zeros as needed).
- `#drop(N , WS)` removes the first `N` elements of a `WordStack`.

```k
syntax WordStack ::= #take ( Int , WordStack ) [klabel(takeWordStack), function, functional]
Expand Down Expand Up @@ -420,8 +420,8 @@ A cons-list is used for the EVM wordstack.

### Element Access

- `WS [ N ]` accesses element $N$ of $WS$.
- `WS [ N := W ]` sets element $N$ of $WS$ to $W$ (padding with zeros as needed).
- `WS [ N ]` accesses element `N` of `WS`.
- `WS [ N := W ]` sets element `N` of `WS` to `W` (padding with zeros as needed).

```k
syntax Int ::= WordStack "[" Int "]" [function, functional]
Expand Down Expand Up @@ -481,8 +481,8 @@ Local Memory

Most of EVM data is held in local memory.

- `WM [ N := WS ]` assigns a contiguous chunk of $WM$ to $WS$ starting at position $W$.
- `#range(M, START, WIDTH)` reads off $WIDTH$ elements from $WM$ beginning at position $START$ (padding with zeros as needed).
- `WM [ N := WS ]` assigns a contiguous chunk of `WM` to `WS` starting at position `W`.
- `#range(WM, START, WIDTH)` reads off `WIDTH` elements from `WM` beginning at position `START` (padding with zeros as needed).

```{.k .bytes}
syntax Memory = Bytes
Expand Down