Skip to content

[WIP] #129

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

Closed
bbyalcinkaya wants to merge 1 commit into from
Closed

[WIP] #129

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 2 additions & 0 deletions src/komet/kdist/soroban-semantics/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,8 @@ module HOST-OBJECT
rule getTagWithFlag(true, I64(_)) => 65
rule getTagWithFlag(true, U128(_)) => 68
rule getTagWithFlag(true, I128(_)) => 69
rule getTagWithFlag(true, U256(_)) => 70
rule getTagWithFlag(true, I256(_)) => 71
rule getTagWithFlag(true, Symbol(_)) => 74
rule getTagWithFlag(_, SCV) => getTag(SCV) [owise]

Expand Down
24 changes: 13 additions & 11 deletions src/komet/kdist/soroban-semantics/host/integer.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -351,7 +351,7 @@ negative value is converted to its unsigned form before shifting.

The i256 arithmetic host functions are *checked*: the result must be
representable, and the divisor must be non-zero. Otherwise the host fails the
call with `(ErrValue, ArithDomain)` rather than wrapping around.
call with `(ErrObject, ArithDomain)` rather than wrapping around.

The first Wasm argument is on top of the host stack (`loadArgs` pushes the
arguments in reverse), so `A` is the left-hand side.
Expand All @@ -367,7 +367,7 @@ arguments in reverse), so `A` is the left-hand side.
requires inRangeInt(i256, Signed, A +Int B)

rule [hostCallAux-i256-add-overflow]:
<instrs> hostCallAux ( "i" , "v" ) => #throw(ErrValue, ArithDomain) ... </instrs>
<instrs> hostCallAux ( "i" , "v" ) => #throw(ErrObject, ArithDomain) ... </instrs>
<hostStack> I256(A) : I256(B) : S => S </hostStack>
requires notBool inRangeInt(i256, Signed, A +Int B)
```
Expand All @@ -385,7 +385,7 @@ arguments in reverse), so `A` is the left-hand side.
requires inRangeInt(i256, Signed, A -Int B)

rule [hostCallAux-i256-sub-overflow]:
<instrs> hostCallAux ( "i" , "w" ) => #throw(ErrValue, ArithDomain) ... </instrs>
<instrs> hostCallAux ( "i" , "w" ) => #throw(ErrObject, ArithDomain) ... </instrs>
<hostStack> I256(A) : I256(B) : S => S </hostStack>
requires notBool inRangeInt(i256, Signed, A -Int B)
```
Expand All @@ -403,7 +403,7 @@ arguments in reverse), so `A` is the left-hand side.
requires inRangeInt(i256, Signed, A *Int B)

rule [hostCallAux-i256-mul-overflow]:
<instrs> hostCallAux ( "i" , "x" ) => #throw(ErrValue, ArithDomain) ... </instrs>
<instrs> hostCallAux ( "i" , "x" ) => #throw(ErrObject, ArithDomain) ... </instrs>
<hostStack> I256(A) : I256(B) : S => S </hostStack>
requires notBool inRangeInt(i256, Signed, A *Int B)
```
Expand All @@ -427,22 +427,22 @@ rather than range-checking `A /Int B`, so no side condition divides.
[preserves-definedness] // 'A /Int B' is defined for non-zero B

rule [hostCallAux-i256-div-by-zero]:
<instrs> hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... </instrs>
<instrs> hostCallAux ( "i" , "y" ) => #throw(ErrObject, ArithDomain) ... </instrs>
<hostStack> I256(_A) : I256(B) : S => S </hostStack>
requires B ==Int 0

rule [hostCallAux-i256-div-overflow]:
<instrs> hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... </instrs>
<instrs> hostCallAux ( "i" , "y" ) => #throw(ErrObject, ArithDomain) ... </instrs>
<hostStack> I256(A) : I256(B) : S => S </hostStack>
requires A ==Int minInt(i256, Signed) andBool B ==Int -1
```

## i256_rem_euclid

Euclidean modulo: the result is always non-negative, whatever the signs of the
operands. K's `modInt` takes the sign of its divisor, so dividing by `absInt(B)`
gives exactly Rust's `rem_euclid`. The quotient never leaves the range, so a
zero divisor is the only failure.
operands. K's `modInt` is e-division, so it already lands in `[0, absInt(B))`
and agrees with Rust's `rem_euclid`. `checked_rem_euclid` rejects the same two
operand pairs as `checked_div`: a zero divisor, and `i256::MIN` by `-1`.

```k
rule [hostCallAux-i256-rem-euclid]:
Expand All @@ -453,12 +453,14 @@ zero divisor is the only failure.
</instrs>
<hostStack> I256(A) : I256(B) : S => S </hostStack>
requires B =/=Int 0
andBool notBool (A ==Int minInt(i256, Signed) andBool B ==Int -1)
[preserves-definedness] // 'A modInt absInt(B)' is defined for non-zero B

rule [hostCallAux-i256-rem-euclid-error]:
<instrs> hostCallAux ( "i" , "z" ) => #throw(ErrValue, ArithDomain) ... </instrs>
<hostStack> I256(_A) : I256(B) : S => S </hostStack>
<instrs> hostCallAux ( "i" , "z" ) => #throw(ErrObject, ArithDomain) ... </instrs>
<hostStack> I256(A) : I256(B) : S => S </hostStack>
requires B ==Int 0
orBool (A ==Int minInt(i256, Signed) andBool B ==Int -1)
```

```k
Expand Down
22 changes: 16 additions & 6 deletions src/tests/integration/data/i256.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -268,7 +268,7 @@ callTx(
Contract(b"test-sc"),
"add",
ListItem(I256(2 ^Int 255 -Int 1)) ListItem(I256(1)),
Error(ErrValue, ArithDomain)
Error(ErrObject, ArithDomain)
)

callTx(
Expand All @@ -292,7 +292,7 @@ callTx(
Contract(b"test-sc"),
"sub",
ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(1)),
Error(ErrValue, ArithDomain)
Error(ErrObject, ArithDomain)
)

callTx(
Expand All @@ -317,7 +317,7 @@ callTx(
Contract(b"test-sc"),
"mul",
ListItem(I256(2 ^Int 200)) ListItem(I256(2 ^Int 200)),
Error(ErrValue, ArithDomain)
Error(ErrObject, ArithDomain)
)

;; Division truncates toward zero.
Expand Down Expand Up @@ -358,7 +358,7 @@ callTx(
Contract(b"test-sc"),
"div",
ListItem(I256(1)) ListItem(I256(0)),
Error(ErrValue, ArithDomain)
Error(ErrObject, ArithDomain)
)

;; i256::MIN / -1 is the one division that overflows.
Expand All @@ -367,7 +367,7 @@ callTx(
Contract(b"test-sc"),
"div",
ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(0 -Int 1)),
Error(ErrValue, ArithDomain)
Error(ErrObject, ArithDomain)
)

;; Euclidean modulo is never negative, whatever the signs of the operands.
Expand Down Expand Up @@ -408,7 +408,17 @@ callTx(
Contract(b"test-sc"),
"rem",
ListItem(I256(1)) ListItem(I256(0)),
Error(ErrValue, ArithDomain)
Error(ErrObject, ArithDomain)
)

;; `checked_rem_euclid` rejects i256::MIN % -1 as well, even though the
;; mathematical remainder (0) is representable.
callTx(
Account(b"test-caller"),
Contract(b"test-sc"),
"rem",
ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(0 -Int 1)),
Error(ErrObject, ArithDomain)
)

setExitCode(0)
Loading