Skip to content

Commit

Permalink
Implement U128
Browse files Browse the repository at this point in the history
  • Loading branch information
@bbyalcinkaya
bbyalcinkaya committed Jul 16, 2024
1 parent 25b33c3 commit 7c2c2ac
Show file tree
Hide file tree
Showing 3 changed files with 276 additions and 1 deletion.
6 changes: 6 additions & 0 deletions src/ksoroban/kdist/soroban-semantics/data.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ storing data on the host side.
| I32(Int) [symbol(SCVal:I32)]
| U64(Int) [symbol(SCVal:U64)]
| I64(Int) [symbol(SCVal:I64)]
| U128(Int) [symbol(SCVal:U128)]
| ScVec(List) [symbol(SCVal:Vec)]
| ScMap(Map) [symbol(SCVal:Map)]
| ScAddress(Address) [symbol(SCVal:Address)]
Expand Down Expand Up @@ -115,6 +116,8 @@ module HOST-OBJECT
rule getTag(U64(I)) => 6 requires I <=Int #maxU64small
rule getTag(U64(I)) => 64 requires notBool( I <=Int #maxU64small )
rule getTag(I64(_)) => 65 // I64small is not implemented
rule getTag(U128(I)) => 10 requires I <=Int #maxU64small
rule getTag(U128(I)) => 68 requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width
rule getTag(ScVec(_)) => 75
rule getTag(ScMap(_)) => 76
rule getTag(ScAddress(_)) => 77
Expand Down Expand Up @@ -179,6 +182,8 @@ module HOST-OBJECT
rule fromSmall(VAL) => U64(getBody(VAL)) requires getTag(VAL) ==Int 6
rule fromSmall(VAL) => U128(getBody(VAL)) requires getTag(VAL) ==Int 10
// return `Void` for invalid values
rule fromSmall(_) => Void [owise]
Expand All @@ -197,6 +202,7 @@ module HOST-OBJECT
rule toSmall(I32(I)) => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5)
requires definedUnsigned(i32, I)
rule toSmall(U64(I)) => fromBodyAndTag(I, 6) requires I <=Int #maxU64small
rule toSmall(U128(I)) => fromBodyAndTag(I, 10) requires I <=Int #maxU64small
rule toSmall(_) => HostVal(-1) [owise]
syntax Bool ::= toSmallValid(ScVal)
Expand Down
48 changes: 47 additions & 1 deletion src/ksoroban/kdist/soroban-semantics/host/integer.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ module HOST-INTEGER
<instrs> returnI64 => i64.const #unsigned(i64, I) ... </instrs>
<hostStack> I64(I) : S => S </hostStack>
requires definedUnsigned(i64, I)
[preserves-definedness]
[preserves-definedness] // definedness of '#unsigned(,)' is checked
rule [returnHostVal]:
<instrs> returnHostVal => i64.const I ... </instrs>
Expand Down Expand Up @@ -53,5 +53,51 @@ module HOST-INTEGER
<locals>
0 |-> < i64 > VAL
</locals>
rule [hostfun-obj-from-u128-pieces]:
<instrs> hostCall ( "i" , "3" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> #waitCommands
~> returnHostVal
...
</instrs>
<locals>
0 |-> < i64 > HIGH
1 |-> < i64 > LOW
</locals>
<k> (.K => allocObject( U128((HIGH <<Int 64) |Int LOW)) ) ... </k>
rule [hostfun-obj-to-u128-lo64]:
<instrs> hostCall ( "i" , "4" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(VAL))
~> u128low64
...
</instrs>
<locals>
0 |-> < i64 > VAL
</locals>
syntax InternalInstr ::= "u128low64" [symbol(u128low64)]
// ---------------------------------------------------------------
rule [u128-low64]:
<instrs> u128low64 => i64.const I ... </instrs> // 'i64.const N' chops N to 64 bits
<hostStack> U128(I) : S => S </hostStack>
rule [hostfun-obj-to-u128-hi64]:
<instrs> hostCall ( "i" , "5" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(VAL))
~> u128high64
...
</instrs>
<locals>
0 |-> < i64 > VAL
</locals>
syntax InternalInstr ::= "u128high64" [symbol(u128high64)]
// ---------------------------------------------------------------
rule [u128-high64]:
<instrs> u128high64 => i64.const (I >>Int 64) ... </instrs>
<hostStack> U128(I) : S => S </hostStack>
[preserves-definedness] // 'X >>Int K' is defined for positive K
endmodule
```
223 changes: 223 additions & 0 deletions src/tests/integration/data/add_u128.wast
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,223 @@

setExitCode(1)

uploadWasm( b"arith",
(module $add_u128.wasm
(type (;0;) (func (param i64) (result i64)))
(type (;1;) (func (param i64 i64) (result i64)))
(type (;2;) (func (param i32 i64)))
(type (;3;) (func))
(import "i" "5" (func $_ZN17soroban_env_guest5guest3int16obj_to_u128_hi6417h645b49e080dcfdf6E (type 0)))
(import "i" "4" (func $_ZN17soroban_env_guest5guest3int16obj_to_u128_lo6417h0c596faaeffbf363E (type 0)))
(import "i" "3" (func $_ZN17soroban_env_guest5guest3int20obj_from_u128_pieces17h5d7cf2ad07a3899bE (type 1)))
(func $_ZN104_$LT$u128$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17h6b320ddacd75d7c2E (type 2) (param i32 i64)
(local i32 i64)
block ;; label = @1
block ;; label = @2
block ;; label = @3
local.get 1
i32.wrap_i64
i32.const 255
i32.and
local.tee 2
i32.const 68
i32.eq
br_if 0 (;@3;)
local.get 2
i32.const 10
i32.ne
br_if 1 (;@2;)
i64.const 0
local.set 3
local.get 0
i32.const 16
i32.add
i64.const 0
i64.store
local.get 0
local.get 1
i64.const 8
i64.shr_u
i64.store offset=8
br 2 (;@1;)
end
local.get 1
call $_ZN17soroban_env_guest5guest3int16obj_to_u128_hi6417h645b49e080dcfdf6E
local.set 3
local.get 1
call $_ZN17soroban_env_guest5guest3int16obj_to_u128_lo6417h0c596faaeffbf363E
local.set 1
local.get 0
i32.const 16
i32.add
local.get 3
i64.store
local.get 0
local.get 1
i64.store offset=8
i64.const 0
local.set 3
br 1 (;@1;)
end
local.get 0
i64.const 34359740419
i64.store offset=8
i64.const 1
local.set 3
end
local.get 0
local.get 3
i64.store)
(func $add (type 1) (param i64 i64) (result i64)
(local i32 i32 i64 i32)
global.get $__stack_pointer
i32.const 32
i32.sub
local.tee 2
global.set $__stack_pointer
local.get 2
i32.const 8
i32.add
local.get 0
call $_ZN104_$LT$u128$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17h6b320ddacd75d7c2E
block ;; label = @1
block ;; label = @2
local.get 2
i64.load offset=8
i64.eqz
i32.eqz
br_if 0 (;@2;)
local.get 2
i32.const 24
i32.add
local.tee 3
i64.load
local.set 4
local.get 2
i64.load offset=16
local.set 0
local.get 2
i32.const 8
i32.add
local.get 1
call $_ZN104_$LT$u128$u20$as$u20$soroban_env_common..convert..TryFromVal$LT$E$C$soroban_env_common..val..Val$GT$$GT$12try_from_val17h6b320ddacd75d7c2E
local.get 2
i64.load offset=8
i64.eqz
i32.eqz
br_if 0 (;@2;)
local.get 0
local.get 2
i64.load offset=16
i64.add
local.tee 1
local.get 0
i64.lt_u
local.tee 5
local.get 4
local.get 3
i64.load
i64.add
local.get 5
i64.extend_i32_u
i64.add
local.tee 0
local.get 4
i64.lt_u
local.get 0
local.get 4
i64.eq
select
i32.const 1
i32.eq
br_if 1 (;@1;)
block ;; label = @3
block ;; label = @4
local.get 1
i64.const 72057594037927935
i64.gt_u
local.get 0
i64.const 0
i64.ne
local.get 0
i64.eqz
select
br_if 0 (;@4;)
local.get 1
i64.const 8
i64.shl
i64.const 10
i64.or
local.set 0
br 1 (;@3;)
end
local.get 0
local.get 1
call $_ZN17soroban_env_guest5guest3int20obj_from_u128_pieces17h5d7cf2ad07a3899bE
local.set 0
end
local.get 2
i32.const 32
i32.add
global.set $__stack_pointer
local.get 0
return
end
unreachable
unreachable
end
call $_ZN4core9panicking5panic17hb157b525de3fe68dE
unreachable)
(func $_ZN4core9panicking5panic17hb157b525de3fe68dE (type 3)
call $_ZN4core9panicking9panic_fmt17hc7427f902a13f1a9E
unreachable)
(func $_ZN4core9panicking9panic_fmt17hc7427f902a13f1a9E (type 3)
unreachable
unreachable)
(func $_ (type 3))
(memory (;0;) 16)
(global $__stack_pointer (mut i32) (i32.const 1048576))
(global (;1;) i32 (i32.const 1048576))
(global (;2;) i32 (i32.const 1048576))
(export "memory" (memory 0))
(export "add" (func $add))
(export "_" (func $_))
(export "__data_end" (global 1))
(export "__heap_base" (global 2)))

)

setAccount(Account(b"test-account"), 9876543210)

deployContract(
Account(b"test-account"),
Contract(b"calculator"),
b"arith",
.List
)

callTx(
Account(b"test-caller"),
Contract(b"calculator"),
"add",
ListItem(U128(3)) ListItem(U128(5)),
U128(8)
)

callTx(
Account(b"test-caller"),
Contract(b"calculator"),
"add",
ListItem(U128(1329227995784915872903807060280344576)) ListItem(U128(1152921504606846976)),
U128(1329227995784915874056728564887191552)
)

callTx(
Account(b"test-caller"),
Contract(b"calculator"),
"add",
ListItem(U128(1329227995784915872903807060280344576)) ListItem(U128(1329227995784915872903807060280344576)),
U128(2658455991569831745807614120560689152)
)

setExitCode(0)

0 comments on commit 7c2c2ac

Please sign in to comment.