Skip to content

Commit 5ba0798

Browse files
bbyalcinkayarv-auditor
bbyalcinkaya
and
rv-auditor
authored
Add U256 arithmetic functions (#73)
* refactor integer.md using hostCallAux * implement u256 arithmetic * implement noop `authorize_as_curr_contract` * Set Version: 0.1.62 * Set Version: 0.1.63 * add comments for max/min int helpers --------- Co-authored-by: devops <[email protected]>
1 parent 0827449 commit 5ba0798

File tree

7 files changed

+316
-70
lines changed

7 files changed

+316
-70
lines changed

‎package/version‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.62
1+
0.1.63

‎pyproject.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "komet"
7-
version = "0.1.62"
7+
version = "0.1.63"
88
description = "K tooling for the Soroban platform"
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

‎src/komet/kdist/soroban-semantics/data.md‎

Lines changed: 41 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ various contexts:
6060
| I64(Int) [symbol(SCVal:I64)]
6161
| U128(Int) [symbol(SCVal:U128)]
6262
| I128(Int) [symbol(SCVal:I128)]
63+
| U256(Int) [symbol(SCVal:U256)]
6364
| ScVec(List) [symbol(SCVal:Vec)] // List<HostVal> or List<ScVal>
6465
| ScMap(Map) [symbol(SCVal:Map)] // Map<ScVal, HostVal> or Map<ScVal, ScVal>
6566
| ScAddress(Address) [symbol(SCVal:Address)]
@@ -159,6 +160,8 @@ module HOST-OBJECT
159160
rule getTag(U128(I)) => 68 requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width
160161
rule getTag(I128(I)) => 11 requires #minI64small <=Int I andBool I <=Int #maxI64small
161162
rule getTag(I128(I)) => 69 requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small )
163+
rule getTag(U256(I)) => 12 requires I <=Int #maxU64small
164+
rule getTag(U256(I)) => 70 requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width
162165
rule getTag(ScVec(_)) => 75
163166
rule getTag(ScMap(_)) => 76
164167
rule getTag(ScAddress(_)) => 77
@@ -176,14 +179,33 @@ module HOST-OBJECT
176179
rule getTagWithFlag(true, Symbol(_)) => 74
177180
rule getTagWithFlag(_, SCV) => getTag(SCV) [owise]
178181
179-
// 64-bit integers that fit in 56 bits
180-
syntax Int ::= "#maxU64small" [macro]
181-
| "#maxI64small" [macro]
182-
| "#minI64small" [macro]
183-
// -----------------------------------------
184-
rule #maxU64small => 72057594037927935
185-
rule #maxI64small => 36028797018963967
186-
rule #minI64small => -36028797018963968
182+
// Define the max/min values of small 64-bit integers that fit in 56 bits.
183+
// These are used to check whether an i64 can be embedded directly as a "small" HostVal
184+
// based on the small integer definition in [CAP-046-01](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01).md#tag-values)
185+
syntax Int ::= "#maxU64small" [macro] // Maximum unsigned small int: 2^56 - 1
186+
| "#maxI64small" [macro] // Maximum signed small int: 2^55 - 1
187+
| "#minI64small" [macro] // Minimum signed small int: -2^55
188+
// -----------------------------------------------------------------------------------------
189+
rule #maxU64small => maxInt(i56, Unsigned)
190+
rule #maxI64small => maxInt(i56, Signed)
191+
rule #minI64small => minInt(i56, Signed)
192+
193+
// Helpers for computing max/min values given a bit width and signedness.
194+
syntax Int ::= maxInt(IWidth, Signedness) [function, total]
195+
| minInt(IWidth, Signedness) [function, total]
196+
// ----------------------------------------------------------------
197+
// For unsigned: max = 2^W - 1, min = 0
198+
rule maxInt(W, Unsigned) => #pow(W) -Int 1
199+
rule minInt(_, Unsigned) => 0
200+
201+
// For signed: max = 2^(W - 1) - 1, min = -2^(W - 1)
202+
rule maxInt(W, Signed) => #pow1(W) -Int 1
203+
rule minInt(W, Signed) => 0 -Int #pow1(W)
204+
205+
// refactor small int checks using this
206+
syntax Bool ::= inRangeInt(IWidth, Signedness, Int) [function, total, symbol(inRangeInt)]
207+
// ------------------------------------------------------------------------------------------
208+
rule inRangeInt(W, SG, I) => minInt(W, SG) <=Int I andBool I <=Int maxInt(W, SG)
187209
188210
syntax ScVal ::= ScValOrDefault(KItem, ScVal) [function, total, symbol(ScValOrDefault)]
189211
// ---------------------------------------------------------
@@ -261,6 +283,8 @@ module HOST-OBJECT
261283
requires getTag(VAL) ==Int 11
262284
andBool definedSigned(i56, getBody(VAL))
263285
286+
rule fromSmall(VAL) => U256(getBody(VAL)) requires getTag(VAL) ==Int 12
287+
264288
rule fromSmall(VAL) => Symbol(decode6bit(getBody(VAL)))
265289
requires getTag(VAL) ==Int 14
266290
@@ -290,6 +314,7 @@ module HOST-OBJECT
290314
rule toSmall(I128(I)) => fromBodyAndTag(#unsigned(i56, I), 11)
291315
requires #minI64small <=Int I andBool I <=Int #maxI64small
292316
andBool definedUnsigned(i56, I)
317+
rule toSmall(U256(I)) => fromBodyAndTag(I, 12) requires I <=Int #maxU64small
293318
rule toSmall(Symbol(S)) => fromBodyAndTag(encode6bit(S), 14) requires lengthString(S) <=Int 9
294319
rule toSmall(_) => HostVal(-1) [owise]
295320
@@ -363,11 +388,15 @@ module HOST-OBJECT
363388
rule #pow(i56) => 72057594037927936
364389
rule #pow1(i56) => 36028797018963968
365390
366-
syntax IWidth ::= "i128"
367-
// ------------------------------------
391+
syntax IWidth ::= "i128" [symbol(i128)]
392+
| "i256" [symbol(i256)]
393+
// -------------------------------------------
368394
rule #width(i128) => 128
369395
rule #pow(i128) => 340282366920938463463374607431768211456
370396
rule #pow1(i128) => 170141183460469231731687303715884105728
397+
rule #width(i256) => 256
398+
rule #pow(i256) => 115792089237316195423570985008687907853269984665640564039457584007913129639936
399+
rule #pow1(i256) => 57896044618658097711785492504343953926634992332820282019728792003956564819968
371400
372401
```
373402

@@ -419,6 +448,7 @@ For scalar types the comparison is straightforward.
419448
rule compare(I64(A), I64(B)) => compareInt(A, B)
420449
rule compare(U128(A), U128(B)) => compareInt(A, B)
421450
rule compare(I128(A), I128(B)) => compareInt(A, B)
451+
rule compare(U256(A), U256(B)) => compareInt(A, B)
422452
rule compare(ScAddress(A), ScAddress(B)) => compareAddress(A, B)
423453
rule compare(Symbol(A), Symbol(B)) => compareString(A, B)
424454
rule compare(ScBytes(A), ScBytes(B)) => compareBytes(A, B)
@@ -539,8 +569,7 @@ corresponding values.
539569
// Duration => 8
540570
rule ScValTypeOrd(U128(_)) => 9
541571
rule ScValTypeOrd(I128(_)) => 10
542-
// U256 => 11
543-
// I256 => 12
572+
rule ScValTypeOrd(U256(_)) => 11
544573
rule ScValTypeOrd(ScBytes(_)) => 13
545574
rule ScValTypeOrd(ScString(_)) => 14
546575
rule ScValTypeOrd(Symbol(_)) => 15

‎src/komet/kdist/soroban-semantics/host/address.md‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,19 @@ module HOST-ADDRESS
2727
<locals>
2828
0 |-> < i64 > _ // Address
2929
</locals>
30+
```
31+
32+
## authorize_as_curr_contract
33+
34+
```k
35+
rule [hostfun-authorize-as-curr-contract]:
36+
<instrs> hostCall ( "a" , "3" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
37+
=> toSmall(Void)
38+
...
39+
</instrs>
40+
<locals>
41+
0 |-> < i64 > _
42+
</locals>
3043
3144
endmodule
3245
```

‎src/komet/kdist/soroban-semantics/host/integer.md‎

Lines changed: 141 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ requires "../configuration.md"
44
55
module HOST-INTEGER
66
imports CONFIG-OPERATIONS
7+
imports WASM-OPERATIONS
78
89
syntax InternalInstr ::= "returnU64" [symbol(returnU64)]
910
| "returnI64" [symbol(returnI64)]
@@ -35,14 +36,13 @@ module HOST-INTEGER
3536
3637
rule [hostfun-obj-from-u64]:
3738
<instrs> hostCall ( "i" , "_" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
38-
=> #waitCommands
39+
=> allocObject(U64(I))
3940
~> returnHostVal
4041
...
4142
</instrs>
4243
<locals>
4344
0 |-> < i64 > I
4445
</locals>
45-
<k> (.K => allocObject(U64(I))) ... </k>
4646
4747
rule [hostfun-obj-from-i64]:
4848
<instrs> hostCall ( "i" , "1" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
@@ -77,36 +77,12 @@ module HOST-INTEGER
7777
</locals>
7878
<k> (.K => allocObject( U128((HIGH <<Int 64) |Int LOW)) ) ... </k>
7979
80-
rule [hostfun-obj-to-u128-lo64]:
81-
<instrs> hostCall ( "i" , "4" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
82-
=> loadObject(HostVal(VAL))
83-
~> u128low64
84-
...
85-
</instrs>
86-
<locals>
87-
0 |-> < i64 > VAL
88-
</locals>
89-
90-
syntax InternalInstr ::= "u128low64" [symbol(u128low64)]
91-
// ---------------------------------------------------------------
92-
rule [u128-low64]:
93-
<instrs> u128low64 => i64.const I ... </instrs> // 'i64.const N' chops N to 64 bits
80+
rule [hostCallAux-obj-to-u128-lo64]:
81+
<instrs> hostCallAux ( "i" , "4" ) => i64.const I ... </instrs> // 'i64.const N' chops N to 64 bits
9482
<hostStack> U128(I) : S => S </hostStack>
9583
96-
rule [hostfun-obj-to-u128-hi64]:
97-
<instrs> hostCall ( "i" , "5" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
98-
=> loadObject(HostVal(VAL))
99-
~> u128high64
100-
...
101-
</instrs>
102-
<locals>
103-
0 |-> < i64 > VAL
104-
</locals>
105-
106-
syntax InternalInstr ::= "u128high64" [symbol(u128high64)]
107-
// ---------------------------------------------------------------
108-
rule [u128-high64]:
109-
<instrs> u128high64 => i64.const (I >>Int 64) ... </instrs>
84+
rule [hostCallAux-obj-to-u128-hi64]:
85+
<instrs> hostCallAux ( "i" , "5" ) => i64.const (I >>Int 64) ... </instrs>
11086
<hostStack> U128(I) : S => S </hostStack>
11187
[preserves-definedness] // 'X >>Int K' is defined for positive K
11288
@@ -122,39 +98,150 @@ module HOST-INTEGER
12298
</locals>
12399
requires definedSigned(i128, (HIGH <<Int 64) |Int LOW )
124100
125-
rule [hostfun-obj-to-i128-lo64]:
126-
<instrs> hostCall ( "i" , "7" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
127-
=> loadObject(HostVal(VAL))
128-
~> i128lo64
129-
...
130-
</instrs>
131-
<locals>
132-
0 |-> < i64 > VAL
133-
</locals>
134-
135-
syntax InternalInstr ::= "i128lo64" [symbol(i128lo64)]
136-
// --------------------------------------------------------
137-
rule [i128lo64]:
138-
<instrs> i128lo64 => i64.const (#unsigned(i128, I)) ... </instrs>
101+
rule [hostCallAux-obj-to-i128-lo64]:
102+
<instrs> hostCallAux ( "i" , "7" ) => i64.const (#unsigned(i128, I)) ... </instrs>
139103
<hostStack> I128(I) : S => S </hostStack>
140104
requires definedUnsigned(i128, I)
141105
[preserves-definedness]
142106
143-
rule [hostfun-obj-to-i128-hi64]:
144-
<instrs> hostCall ( "i" , "8" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
145-
=> loadObject(HostVal(VAL))
146-
~> i128hi64
107+
rule [hostCallAux-obj-to-i128-hi64]:
108+
<instrs> hostCallAux ( "i" , "8" ) => i64.const (I >>Int 64) ... </instrs>
109+
<hostStack> I128(I) : S => S </hostStack>
110+
```
111+
112+
## obj_from_u256_pieces
113+
114+
```k
115+
rule [hostfun-obj-from-u256-pieces]:
116+
<instrs> hostCall ( "i" , "9" , [ i64 i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
117+
=> allocObject( U256(
118+
(HI_HI <<Int 192)
119+
|Int (HI_LO <<Int 128)
120+
|Int (LO_HI <<Int 64)
121+
|Int LO_LO
122+
))
123+
~> returnHostVal
147124
...
148125
</instrs>
149126
<locals>
150-
0 |-> < i64 > VAL
127+
0 |-> < i64 > HI_HI
128+
1 |-> < i64 > HI_LO
129+
2 |-> < i64 > LO_HI
130+
3 |-> < i64 > LO_LO
151131
</locals>
132+
```
152133

153-
syntax InternalInstr ::= "i128hi64" [symbol(i128hi64)]
154-
// --------------------------------------------------------
155-
rule [i128hi64]:
156-
<instrs> i128hi64 => i64.const (I >>Int 64) ... </instrs>
157-
<hostStack> I128(I) : S => S </hostStack>
134+
## u256_val_from_be_bytes
158135

136+
Convert a 32-byte `Bytes` object to `U256`.
137+
138+
```k
139+
rule [hostCallAux-u256-val-from-be-bytes]:
140+
<instrs> hostCallAux ( "i" , "a" )
141+
=> allocObject( U256( Bytes2Int(BS, BE, Unsigned) ) )
142+
~> returnHostVal
143+
...
144+
</instrs>
145+
<hostStack> ScBytes(BS) : S => S </hostStack>
146+
requires lengthBytes(BS) ==Int 32
147+
```
148+
149+
## u256_val_to_be_bytes
150+
151+
```k
152+
rule [hostCallAux-u256-val-to-be-bytes]:
153+
<instrs> hostCallAux ( "i" , "b" )
154+
=> allocObject( ScBytes( Int2Bytes(32, I, BE) ) )
155+
~> returnHostVal
156+
...
157+
</instrs>
158+
<hostStack> U256(I) : S => S </hostStack>
159+
```
160+
161+
## obj_to_u256_hi_hi
162+
163+
```k
164+
rule [hostCallAux-obj-to-u256-hi-hi]:
165+
<instrs> hostCallAux ( "i" , "c" ) => i64.const (I >>Int 192) ... </instrs>
166+
<hostStack> U256(I) : S => S </hostStack>
167+
```
168+
169+
## obj_to_u256_hi_lo
170+
171+
```k
172+
rule [hostCallAux-obj-to-u256-hi-lo]:
173+
<instrs> hostCallAux ( "i" , "d" ) => i64.const (I >>Int 128) ... </instrs>
174+
<hostStack> U256(I) : S => S </hostStack>
175+
```
176+
177+
## obj_to_u256_lo_hi
178+
179+
```k
180+
rule [hostCallAux-obj-to-u256-lo-hi]:
181+
<instrs> hostCallAux ( "i" , "e" ) => i64.const (I >>Int 64) ... </instrs>
182+
<hostStack> U256(I) : S => S </hostStack>
183+
```
184+
185+
## obj_to_u256_lo_lo
186+
187+
```k
188+
rule [hostCallAux-obj-to-u256-lo-lo]:
189+
<instrs> hostCallAux ( "i" , "f" ) => i64.const I ... </instrs>
190+
<hostStack> U256(I) : S => S </hostStack>
191+
```
192+
193+
## u256_add
194+
195+
```k
196+
rule [hostCallAux-u256-add]:
197+
<instrs> hostCallAux ( "i" , "n" )
198+
=> allocObject( U256( A +Int B ) )
199+
~> returnHostVal
200+
...
201+
</instrs>
202+
<hostStack> U256(A) : U256(B) : S => S </hostStack>
203+
requires inRangeInt(i256, Unsigned, A +Int B)
204+
```
205+
206+
## u256_sub
207+
208+
```k
209+
rule [hostCallAux-u256-sub]:
210+
<instrs> hostCallAux ( "i" , "o" )
211+
=> allocObject( U256( A -Int B ) )
212+
~> returnHostVal
213+
...
214+
</instrs>
215+
<hostStack> U256(A) : U256(B) : S => S </hostStack>
216+
requires inRangeInt(i256, Unsigned, A -Int B)
217+
```
218+
219+
## u256_mul
220+
221+
```k
222+
rule [hostCallAux-u256-mul]:
223+
<instrs> hostCallAux ( "i" , "p" )
224+
=> allocObject( U256( A *Int B ) )
225+
~> returnHostVal
226+
...
227+
</instrs>
228+
<hostStack> U256(A) : U256(B) : S => S </hostStack>
229+
requires inRangeInt(i256, Unsigned, A *Int B)
230+
```
231+
232+
## u256_div
233+
234+
```k
235+
rule [hostCallAux-u256-div]:
236+
<instrs> hostCallAux ( "i" , "q" )
237+
=> allocObject( U256( A /Int B ) )
238+
~> returnHostVal
239+
...
240+
</instrs>
241+
<hostStack> U256(A) : U256(B) : S => S </hostStack>
242+
requires 0 =/=Int B
243+
```
244+
245+
```k
159246
endmodule
160247
```

0 commit comments

Comments
 (0)