Skip to content

Commit

Permalink
Merge branch 'master' into _update-deps/runtimeverification/wasm-sema…
Browse files Browse the repository at this point in the history 
…ntics
  • Loading branch information
@bbyalcinkaya
bbyalcinkaya authored Jul 29, 2024
2 parents 8ec4ebd + d02f5f7 commit a7bade8
Show file tree
Hide file tree
Showing 7 changed files with 704 additions and 47 deletions.
104 changes: 76 additions & 28 deletions src/ksoroban/kdist/soroban-semantics/configuration.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ module CONFIG
<hostObjects> .List </hostObjects> // List of ScVals
<callStack> .List </callStack>
<interimStates> .List </interimStates>
</host>
</host>
<contracts>
<contract multiplicity="*" type="Map">
Expand All @@ -46,7 +46,7 @@ module CONFIG
</soroban>
syntax HostStack ::= List{HostStackVal, ":"} [symbol(hostStackList)]
syntax HostStackVal ::= ScVal | HostVal | Bytes
syntax HostStackVal ::= ScVal | HostVal | Bytes | List
syntax InternalCmd ::= #callResult(ValStack, List) [symbol(#callResult)]
Expand Down Expand Up @@ -81,7 +81,7 @@ module CONFIG-OPERATIONS

## Call State

The `<callStack>` cell stores a list of previous contract execution states.
The `<callStack>` cell stores a list of previous contract execution states.
These internal commands manages the call stack when calling and returning from a contract.

```k
Expand Down Expand Up @@ -156,13 +156,13 @@ These internal commands manages the call stack when calling and returning from a

### Creating host objects

If `SCV` is an object (i.e., not a small value), `allocObject(SCV)` creates a new host object
and pushes a `HostVal` onto the `<hostStack>` that points to the newly created object.
If `SCV` is a container such as a Vector or Map, `allocObject` recursively allocates host objects for its content
If `SCV` is an object (i.e., not a small value), `allocObject(SCV)` creates a new host object
and pushes a `HostVal` onto the `<hostStack>` that points to the newly created object.
If `SCV` is a container such as a Vector or Map, `allocObject` recursively allocates host objects for its content
but only pushes a single `HostVal` for the entire container onto the stack.
If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly equivalent to `SCV`.
```k

```k
syntax InternalCmd ::= allocObject(ScVal) [symbol(allocObject)]
// ---------------------------------------------------------------------------
rule [allocObject-small]:
Expand All @@ -177,12 +177,40 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
~> allocObjectVecAux
...
</k>
syntax InternalCmd ::= "allocObjectVecAux"
// ------------------------------------------
// recursively allocate map values.
rule [allocObject-map]:
<k> allocObject(ScMap(ITEMS))
// Using `lookupMany` with `keys_list` instead of `values`
// to ensure the order of values matches the order of keys.
=> allocObjects(lookupMany(ITEMS, keys_list(ITEMS), 0))
~> allocObjectMapAux(keys_list(ITEMS))
...
</k>
syntax Map ::= mapFromLists(List, List) [function, total, symbol(mapFromLists)]
// --------------------------------------------------------------------------------
rule mapFromLists(ListItem(KEY) KEYS, ListItem(VAL) VALS)
=> mapFromLists(KEYS, VALS) [ KEY <- VAL]
rule mapFromLists(_, _) => .Map
[owise]
syntax InternalCmd ::= "allocObjectVecAux" [symbol(allocObjectVecAux)]
// -------------------------------------------------------------------------
rule [allocObjectVecAux]:
<k> allocObjectVecAux => addObject(ScVec(V)) ... </k>
<hostStack> ScVec(V) : S => S </hostStack>
<hostStack> V : S => S </hostStack>
syntax InternalCmd ::= allocObjectMapAux(List) [symbol(allocObjectMapAux)]
// -------------------------------------------------------------------------
rule [allocObjectMapAux]:
<k> allocObjectMapAux(KEYS)
=> addObject(ScMap(mapFromLists(KEYS, VALS)))
...
</k>
<hostStack> VALS : S => S </hostStack>
requires size(KEYS) ==Int size(VALS)
rule [allocObject]:
<k> allocObject(SCV) => addObject(SCV) ... </k>
Expand All @@ -204,31 +232,37 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
syntax InternalCmd ::= allocObjects (List) [symbol(allocObjects)]
| allocObjectsAux (List) [symbol(allocObjectsAux)]
| allocObjectsCollect(Int) [symbol(allocObjectsCollect)]
// ---------------------------------------------------------------------------
rule [allocObjects]:
<k> allocObjects(L) => allocObjectsAux(L) ~> allocObjectsCollect(size(L)) ... </k>
<k> allocObjects(L) => allocObjectsAux(L) ~> collectStackObjects(size(L)) ... </k>
rule [allocObjectsAux-empty]:
<k> allocObjectsAux(.List) => .K ... </k>
rule [allocObjectsAux]:
<k> allocObjectsAux(ListItem(SCV:ScVal) L)
<k> allocObjectsAux(ListItem(SCV:ScVal) L)
=> allocObjectsAux(L)
~> allocObject(SCV)
...
</k>
rule [allocObjectsAux-HostVal]:
<k> allocObjectsAux(ListItem(HV:HostVal) L)
<k> allocObjectsAux(ListItem(HV:HostVal) L)
=> allocObjectsAux(L)
~> pushStack(HV)
...
</k>
rule [allocObjectsCollect]:
<k> allocObjectsCollect(LENGTH) => .K ... </k>
<hostStack> STACK => ScVec(take(LENGTH, STACK)) : drop(LENGTH, STACK) </hostStack>
// Collect stack values into a List
syntax InternalCmd ::= collectStackObjects(Int) [symbol(collectStackObjects)]
// ---------------------------------------------------------------------------------------
rule [collectStackObjects]:
<k> collectStackObjects(LENGTH) => .K ... </k>
<hostStack> STACK => take(LENGTH, STACK) : drop(LENGTH, STACK) </hostStack>
rule [collectStackObjects-instr]:
<instrs> collectStackObjects(LENGTH) => .K ... </instrs>
<hostStack> STACK => take(LENGTH, STACK) : drop(LENGTH, STACK) </hostStack>
```

Expand All @@ -248,7 +282,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
andBool getIndex(VAL) <Int size(OBJS)
rule [loadObject-rel]:
<instrs> loadObject(VAL)
<instrs> loadObject(VAL)
=> loadObject(RELS {{ getIndex(VAL) }} orDefault HostVal(0))
...
</instrs>
Expand All @@ -264,7 +298,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
requires notBool isObject(VAL)
andBool fromSmallValid(VAL)
```

### Auxiliary functions
Expand All @@ -274,27 +308,37 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
// -------------------------------------------------------------------------------------
rule drop(N, _ : S) => drop(N -Int 1, S) requires N >Int 0
rule drop(_, S) => S [owise]
syntax List ::= take(Int, HostStack) [function, total, symbol(HostStack:take)]
// -------------------------------------------------------------------------------------
rule take(N, X : S) => ListItem(X) take(N -Int 1, S) requires N >Int 0
rule take(_, _) => .List [owise]
```

- `lookupMany`: Retrieve values for multiple keys from a map. Return the specified default value for missing keys.

```k
syntax List ::= lookupMany(Map, List, KItem) [function, total]
// ----------------------------------------------------------------
rule lookupMany(M, ListItem(A) REST, D) => ListItem(M [ A ] orDefault D) lookupMany(M, REST, D)
rule lookupMany(_, _, _) => .List
[owise]
```

## Call result handling

```k
rule [callResult-empty]:
<k> #callResult(.ValStack, _RELS) => .K ... </k>
rule [callResult]:
<k> #callResult(<i64> I : SS, RELS)
=> #callResult(SS, RELS)
~> pushStack(HostVal2ScVal(HostVal(I), OBJS, RELS))
...
</k>
<hostObjects> OBJS </hostObjects>
// Convert HostVals to ScVal recursively
syntax ScVal ::= HostVal2ScVal(HostVal, objs: List, rels: List) [function, total, symbol(HostVal2ScVal)]
// -------------------------------------------------------------------------------------------------------------------
Expand All @@ -318,19 +362,23 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
syntax ScVal ::= HostVal2ScValRec(ScVal, objs: List, rels: List) [function, total, symbol(HostVal2ScValRec)]
// -------------------------------------------------------------------------------------------------------------------
rule HostVal2ScValRec(ScVec(VEC), OBJS, RELS) => ScVec(HostVal2ScValMany(VEC, OBJS, RELS))
rule HostVal2ScValRec(ScMap(M), OBJS, RELS)
=> ScMap(mapFromLists( keys_list(M), HostVal2ScValMany(values(M), OBJS, RELS)) )
rule HostVal2ScValRec(SCV, _OBJS, _RELS) => SCV [owise]
syntax List ::= HostVal2ScValMany(List, objs: List, rels: List) [function, total, symbol(HostVal2ScValMany)]
// -------------------------------------------------------------------------------------------------------------------
rule HostVal2ScValMany(ListItem(V:HostVal) REST, OBJS, RELS)
=> ListItem(HostVal2ScVal(V, OBJS, RELS)) HostVal2ScValMany(REST, OBJS, RELS)
rule HostVal2ScValMany(ListItem(V:ScVal) REST, OBJS, RELS)
=> ListItem(HostVal2ScValRec(V, OBJS, RELS)) HostVal2ScValMany(REST, OBJS, RELS)
rule HostVal2ScValMany(_, _, _)
=> .List [owise]
```

```k
Expand Down
59 changes: 43 additions & 16 deletions src/ksoroban/kdist/soroban-semantics/data.md
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
# Host Data Types

[Documentation - Host Value Type](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#host-value-type)

Expand All @@ -15,21 +16,47 @@ module HOST-OBJECT-SYNTAX

[Documentation: ScVal](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#scval)

`ScVal` is a union of various datatypes used in the context of smart contracts for passing values to and from contracts and
storing data on the host side.
`ScVal` is a union of various datatypes used in the context of smart contracts for passing values to and from contracts
and storing data on the host side.
It combines elements from Stellar XDR’s `ScVal` and the Soroban Rust environment’s `HostObject` type (_Stellar XDR_ is
the data format storing and communicating blockchain data).

* [Stellar XDR - `ScVal`](https://github.com/stellar/stellar-xdr/blob/78ef9860777bd53e75a8ce8b978131cade26b321/Stellar-contract.x#L214)
* [Soroban Environment - `HostObject`](https://github.com/stellar/rs-soroban-env/blob/00ddd2714e757d0005bfc98798f05aa209f283bf/soroban-env-host/src/host_object.rs#L22)

There are notable differences between XDR’s `ScVal` and Rust’s `HostObject`:

* Data Representation: XDR `ScVal` and Rust `HostObject` differ in their data representation and storage.
XDR’s `ScVal` is recursive on container types such as map and vector, meaning it stores `ScVal`s as both keys and
values within vectors and maps, allowing for nested data structures. In contrast, `HostObject` uses `HostVal` in
container types, which requires resolving the corresponding host objects when accessing these values.
* Containers: XDR uses sorted vectors of key-value pairs for maps with binary search for lookups. The Rust environment
also uses a sorted vector but stores `HostVal` within these containers. Our semantics, however, use `Map` instead for
efficient lookup and simpler implementation.

In our semantic implementation, `ScVal` is utilized to represent both XDR `ScVal` and Rust `HostObject`, adapting to
various contexts:

* Inside the Host:
* `ScVec`: Represented as a `List` of `HostVal`
* `ScMap`: Represented as a `Map` from `ScVal` to `HostVal`.
Using `ScVal` as keys allows for more efficient lookups because it avoids the additional layer of indirection that
would be required if `HostVal` were used.
* Outside the Host:
* `ScVec`: Represented as a `List` of `ScVal`.
* `ScVec`: Represented as a `Map` from `ScVal` to `ScVal`.

```k
syntax ScVal
syntax ScVal
::= SCBool(Bool) [symbol(SCVal:Bool)]
| "Void" [symbol(SCVal:Void)]
| U32(Int) [symbol(SCVal:U32)]
| 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)]
| ScVec(List) [symbol(SCVal:Vec)] // List<HostVal>
| ScMap(Map) [symbol(SCVal:Map)] // Map<ScVal, HostVal>
| ScAddress(Address) [symbol(SCVal:Address)]
| Symbol(String) [symbol(SCVal:Symbol)]
Expand Down Expand Up @@ -78,11 +105,11 @@ module HOST-OBJECT
rule getBody(HostVal(I)) => I >>Int 8
syntax Bool ::= isObject(HostVal) [function, total, symbol(isObject)]
| isObjectTag(Int) [function, total, symbol(isObjectTag)]
| isObjectTag(Int) [function, total, symbol(isObjectTag)]
| isRelativeObjectHandle(HostVal) [function, total, symbol(isRelativeObjectHandle)]
// --------------------------------------------------------------------------------
rule isObject(V) => isObjectTag(getTag(V))
rule isObjectTag(TAG) => 64 <=Int TAG andBool TAG <=Int 77
rule isObjectTag(TAG) => 64 <=Int TAG andBool TAG <=Int 77
rule isRelativeObjectHandle(V) => getMajor(V) &Int 1 ==Int 0
syntax Int ::= indexToHandle(Int, Bool) [function, total, symbol(indexToHandle)]
Expand All @@ -93,7 +120,7 @@ module HOST-OBJECT
syntax Int ::= getIndex(HostVal) [function, total, symbol(getIndex)]
// ----------------------------------------------------------------------------
rule getIndex(V) => getMajor(V) >>Int 1
syntax HostVal ::= fromHandleAndTag(Int, Int) [function, total, symbol(fromHandleAndTag)]
| fromMajorMinorAndTag(Int, Int, Int) [function, total, symbol(fromMajorMinorAndTag)]
| fromBodyAndTag(Int, Int) [function, total, symbol(fromBodyAndTag)]
Expand All @@ -112,7 +139,7 @@ module HOST-OBJECT
rule getTag(SCBool(true)) => 0
rule getTag(SCBool(false)) => 1
rule getTag(Void) => 2
rule getTag(U32(_)) => 4
rule getTag(U32(_)) => 4
rule getTag(I32(_)) => 5
rule getTag(U64(I)) => 6 requires I <=Int #maxU64small
rule getTag(U64(I)) => 64 requires notBool( I <=Int #maxU64small )
Expand Down Expand Up @@ -145,7 +172,7 @@ module HOST-OBJECT
rule HostValOrDefault(X:HostVal, _:HostVal) => X
rule HostValOrDefault(_, D:HostVal) => D [owise]
syntax ScVal ::= List "{{" Int "}}" "orDefault" ScVal
syntax ScVal ::= List "{{" Int "}}" "orDefault" ScVal
[function, total, symbol(List:getOrDefault)]
// ---------------------------------------------------------
rule OBJS {{ I }} orDefault (D:ScVal) => ScValOrDefault(OBJS [ I ], D)
Expand All @@ -154,7 +181,7 @@ module HOST-OBJECT
rule _OBJS {{ _I }} orDefault (D:ScVal) => D
[owise]
syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal
syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal
[function, total, symbol(HostVal:getOrDefault)]
// ---------------------------------------------------------
rule OBJS {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ], D)
Expand Down Expand Up @@ -222,7 +249,7 @@ module HOST-OBJECT
syntax String ::= decode6bit(Int) [function, total, symbol(decode6bit)]
// --------------------------------------------------------------------------------
rule decode6bit(I) => decode6bit(I >>Int 6) +String decode6bitChar(I &Int 63) requires 0 <Int I
rule decode6bit(_) => "" [owise]
rule decode6bit(_) => "" [owise]
syntax String ::= "sixBitStringTable" [macro]
// -------------------------------------------------------------------------------------------
Expand All @@ -241,7 +268,7 @@ module HOST-OBJECT
=> encode6bitAux((A <<Int 6) |Int encode6bitChar(head(S)), tail(S))
requires 0 <Int lengthString(S)
rule encode6bitAux(A, _) => A
[owise]
[owise]
syntax Int ::= encode6bitChar(String) [function, total, symbol(encode6bitChar)]
// ---------------------------------------------------------------------------------
Expand All @@ -253,9 +280,9 @@ module HOST-OBJECT
rule validSymbol(S) => true
requires lengthString(S) ==Int 0
rule validSymbol(S) => validSymbolChar(head(S)) andBool validSymbol(tail(S))
requires 0 <Int lengthString(S) andBool lengthString(S) <=Int 32
requires 0 <Int lengthString(S) andBool lengthString(S) <=Int 32
rule validSymbol(S) => false
requires 32 <Int lengthString(S)
requires 32 <Int lengthString(S)
rule validSymbolChar(I) => findChar(sixBitStringTable, I, 0) =/=Int -1
Expand All @@ -266,6 +293,6 @@ module HOST-OBJECT
rule head(S) => substrString(S, 0, 1) requires lengthString(S) >Int 0
rule tail(S) => "" requires lengthString(S) <=Int 0
rule tail(S) => substrString(S, 1, lengthString(S)) requires lengthString(S) >Int 0
endmodule
```
2 changes: 2 additions & 0 deletions src/ksoroban/kdist/soroban-semantics/host/hostfuns.md
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@

```k
requires "integer.md"
requires "map.md"
requires "symbol.md"
requires "vector.md"
module HOSTFUNS
imports HOST-INTEGER
imports HOST-MAP
imports HOST-SYMBOL
imports HOST-VECTOR
endmodule
Expand Down
Loading

0 comments on commit a7bade8

Please sign in to comment.