Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into _update-deps/runtim…
Browse files Browse the repository at this point in the history 
…everification/wasm-semantics
  • Loading branch information
devops committed Jul 23, 2024
2 parents bed9f8b + 9942796 commit aca440e
Show file tree
Hide file tree
Showing 10 changed files with 822 additions and 33 deletions.
128 changes: 99 additions & 29 deletions src/ksoroban/kdist/soroban-semantics/configuration.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ module CONFIG
</soroban>
syntax HostStack ::= List{HostStackVal, ":"} [symbol(hostStackList)]
syntax HostStackVal ::= ScVal | HostVal
syntax HostStackVal ::= ScVal | HostVal | Bytes
syntax InternalCmd ::= #callResult(ValStack, List) [symbol(#callResult)]
Expand Down Expand Up @@ -154,20 +154,54 @@ These internal commands manages the call stack when calling and returning from a

## `ScVal` Operations

```k
### 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
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
syntax InternalCmd ::= allocObject(ScVal) [symbol(allocObject)]
// ---------------------------------------------------------------------------
rule [allocObject-small]:
<k> allocObject(SCV) => .K ... </k>
<hostStack> STACK => toSmall(SCV) : STACK </hostStack>
requires toSmallValid(SCV)
// recursively allocate vector items
rule [allocObject-vec]:
<k> allocObject(ScVec(ITEMS))
=> allocObjects(ITEMS)
~> allocObjectVecAux
...
</k>
syntax InternalCmd ::= "allocObjectVecAux"
// ------------------------------------------
rule [allocObjectVecAux]:
<k> allocObjectVecAux => addObject(ScVec(V)) ... </k>
<hostStack> ScVec(V) : S => S </hostStack>
rule [allocObject]:
<k> allocObject(SCV) => .K ... </k>
<hostObjects> OBJS => OBJS ListItem(SCV) </hostObjects>
<hostStack> STACK => fromHandleAndTag(indexToHandle(size(OBJS), false), getTag(SCV)) : STACK </hostStack>
<k> allocObject(SCV) => addObject(SCV) ... </k>
[owise]
// Allows using `allocObject` in the `<instrs>` cell
rule [allocObject-instr]:
<instrs> allocObject(SCV) => #waitCommands ... </instrs>
<k> (.K => allocObject(SCV)) ... </k>
syntax InternalCmd ::= addObject(ScVal) [symbol(addObject)]
// --------------------------------------------------------------------------------------------
rule [addObject]:
<k> addObject(SCV) => .K ... </k>
<hostObjects> OBJS => OBJS ListItem(SCV) </hostObjects>
<hostStack> STACK
=> fromHandleAndTag(indexToHandle(size(OBJS), false), getTag(SCV)) : STACK
</hostStack>
syntax InternalCmd ::= allocObjects (List) [symbol(allocObjects)]
| allocObjectsAux (List) [symbol(allocObjectsAux)]
| allocObjectsCollect(Int) [symbol(allocObjectsCollect)]
Expand All @@ -185,20 +219,23 @@ These internal commands manages the call stack when calling and returning from a
...
</k>
rule [allocObjectsAux-HostVal]:
<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>
syntax HostStack ::= drop(Int, HostStack) [function, total, symbol(HostStack:drop)]
// -------------------------------------------------------------------------------------
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]
```

### Accessing host objects


```k
syntax InternalInstr ::= loadObject(HostVal) [symbol(loadObject)]
// --------------------------------------------------------------------
rule [loadObject-abs]:
Expand All @@ -220,6 +257,28 @@ These internal commands manages the call stack when calling and returning from a
andBool isRelativeObjectHandle(VAL)
andBool 0 <=Int getIndex(VAL)
andBool getIndex(VAL) <Int size(RELS)
rule [loadObject-small]:
<instrs> loadObject(VAL) => .K ... </instrs>
<hostStack> S => fromSmall(VAL) : S </hostStack>
requires notBool isObject(VAL)
andBool fromSmallValid(VAL)
```

### Auxiliary functions

```k
syntax HostStack ::= drop(Int, HostStack) [function, total, symbol(HostStack:drop)]
// -------------------------------------------------------------------------------------
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]
```

## Call result handling
Expand All @@ -231,36 +290,47 @@ These internal commands manages the call stack when calling and returning from a
rule [callResult]:
<k> #callResult(<i64> I : SS, RELS)
=> #callResult(SS, RELS)
~> HostVal2ScVal(HostVal(I), RELS)
~> pushStack(HostVal2ScVal(HostVal(I), OBJS, RELS))
...
</k>
syntax InternalCmd ::= HostVal2ScVal(HostVal, List) [symbol(HostVal2ScVal)]
// --------------------------------------------------------------------------
rule [HostVal2ScVal-obj-abs]:
<k> HostVal2ScVal(VAL, _RELS) => .K ... </k>
<hostObjects> OBJS </hostObjects>
<hostStack> S => OBJS {{ getIndex(VAL) }} orDefault Void : S </hostStack>
// Convert HostVals to ScVal recursively
syntax ScVal ::= HostVal2ScVal(HostVal, objs: List, rels: List) [function, total, symbol(HostVal2ScVal)]
// -------------------------------------------------------------------------------------------------------------------
rule HostVal2ScVal(VAL, OBJS, RELS) => HostVal2ScValRec(OBJS {{ getIndex(VAL) }} orDefault Void, OBJS, RELS)
requires isObject(VAL)
andBool notBool(isRelativeObjectHandle(VAL))
andBool getIndex(VAL) <Int size(OBJS)
rule [HostVal2ScVal-obj-rel]:
<k> HostVal2ScVal(VAL, RELS)
=> HostVal2ScVal(RELS {{ getIndex(VAL) }} orDefault HostVal(0), RELS)
...
</k>
rule HostVal2ScVal(VAL, OBJS, RELS) => HostVal2ScVal(RELS {{ getIndex(VAL) }} orDefault HostVal(0), OBJS, RELS)
requires isObject(VAL)
andBool isRelativeObjectHandle(VAL)
andBool getIndex(VAL) <Int size(RELS)
[preserves-definedness]
rule [HostVal2ScVal-small]:
<k> HostVal2ScVal(VAL, _RELS) => .K ... </k>
<hostStack> S => fromSmall(VAL) : S </hostStack>
rule HostVal2ScVal(VAL, _OBJS, _RELS) => fromSmall(VAL)
requires notBool isObject(VAL)
andBool fromSmallValid(VAL)
rule HostVal2ScVal(_, _, _) => Void [owise]
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(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
64 changes: 60 additions & 4 deletions src/ksoroban/kdist/soroban-semantics/data.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ storing data on the host side.
| ScVec(List) [symbol(SCVal:Vec)]
| ScMap(Map) [symbol(SCVal:Map)]
| ScAddress(Address) [symbol(SCVal:Address)]
| Symbol(String) [symbol(SCVal:Symbol)]
syntax Address ::= AccountId | ContractId
syntax AccountId ::= Account(Bytes) [symbol(AccountId)]
Expand Down Expand Up @@ -121,6 +122,9 @@ module HOST-OBJECT
rule getTag(ScVec(_)) => 75
rule getTag(ScMap(_)) => 76
rule getTag(ScAddress(_)) => 77
rule getTag(Symbol(BS)) => 14 requires lengthString(BS) <=Int 9
rule getTag(Symbol(BS)) => 74 requires lengthString(BS) >Int 9
// 64-bit integers that fit in 56 bits
syntax Int ::= "#maxU64small" [macro]
Expand Down Expand Up @@ -184,6 +188,9 @@ module HOST-OBJECT
rule fromSmall(VAL) => U128(getBody(VAL)) requires getTag(VAL) ==Int 10
rule fromSmall(VAL) => Symbol(decode6bit(getBody(VAL)))
requires getTag(VAL) ==Int 14
// return `Void` for invalid values
rule fromSmall(_) => Void [owise]
Expand All @@ -201,15 +208,64 @@ module HOST-OBJECT
rule toSmall(U32(I)) => fromMajorMinorAndTag(I, 0, 4)
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]
rule toSmall(U64(I)) => fromBodyAndTag(I, 6) requires I <=Int #maxU64small
rule toSmall(U128(I)) => fromBodyAndTag(I, 10) requires I <=Int #maxU64small
rule toSmall(Symbol(S)) => fromBodyAndTag(encode6bit(S), 14) requires lengthString(S) <=Int 9
rule toSmall(_) => HostVal(-1) [owise]
syntax Bool ::= toSmallValid(ScVal)
[function, total, symbol(toSmallValid)]
// ---------------------------------------------------------------------------------
rule toSmallValid(VAL) => toSmall(VAL) =/=K HostVal(-1)
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]
syntax String ::= "sixBitStringTable" [macro]
// -------------------------------------------------------------------------------------------
rule sixBitStringTable => "_0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefgyahijklmnopqrstuvwxyz"
syntax String ::= decode6bitChar(Int) [function, total, symbol(decode6bitChar)]
// ---------------------------------------------------------------------------------
rule decode6bitChar(I) => substrString(sixBitStringTable, I -Int 1, I)
syntax Int ::= encode6bit ( String) [function, total, symbol(encode6bit)]
| encode6bitAux(Int, String) [function, total, symbol(encode6bitAux)]
// --------------------------------------------------------------------------------
rule encode6bit(S) => encode6bitAux(0, S)
rule encode6bitAux(A, S)
=> encode6bitAux((A <<Int 6) |Int encode6bitChar(head(S)), tail(S))
requires 0 <Int lengthString(S)
rule encode6bitAux(A, _) => A
[owise]
syntax Int ::= encode6bitChar(String) [function, total, symbol(encode6bitChar)]
// ---------------------------------------------------------------------------------
rule encode6bitChar(I) => findChar(sixBitStringTable, I, 0) +Int 1
syntax Bool ::= validSymbol(String) [function, total, symbol(validSymbol)]
| validSymbolChar(String) [function, total, symbol(validSymbolChar)]
// --------------------------------------------------------------------------------
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
rule validSymbol(S) => false
requires 32 <Int lengthString(S)
rule validSymbolChar(I) => findChar(sixBitStringTable, I, 0) =/=Int -1
syntax String ::= head(String) [function, total, symbol(headString)]
| tail(String) [function, total, symbol(tailString)]
// -----------------------------------------------------------------------
rule head(S) => "" requires lengthString(S) <=Int 0
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
```
```
4 changes: 4 additions & 0 deletions src/ksoroban/kdist/soroban-semantics/host/hostfuns.md
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,12 @@

```k
requires "integer.md"
requires "symbol.md"
requires "vector.md"
module HOSTFUNS
imports HOST-INTEGER
imports HOST-SYMBOL
imports HOST-VECTOR
endmodule
```
40 changes: 40 additions & 0 deletions src/ksoroban/kdist/soroban-semantics/host/symbol.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
# Symbol

```k
requires "../configuration.md"
requires "../switch.md"
requires "../wasm-ops.md"
requires "integer.md"
module HOST-SYMBOL
imports CONFIG-OPERATIONS
imports WASM-OPERATIONS
imports HOST-INTEGER
imports SWITCH-SYNTAX
// symbol_new_from_linear_memory
rule [hostfun-symbol-new-from-linear-memory]:
<instrs> hostCall ( "b" , "j" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> #memLoad(getMajor(HostVal(LM_POS)), getMajor(HostVal(LEN)))
~> symbolNewFromLinearMemory
...
</instrs>
<locals>
0 |-> < i64 > LM_POS // U32
1 |-> < i64 > LEN // U32
</locals>
requires fromSmallValid(HostVal(LM_POS))
andBool fromSmallValid(HostVal(LEN))
syntax InternalInstr ::= "symbolNewFromLinearMemory" [symbol(symbolNewFromLinearMemory)]
rule [symbolNewFromLinearMemory]:
<instrs> symbolNewFromLinearMemory
=> allocObject(Symbol(Bytes2String(BS)))
~> returnHostVal
...
</instrs>
<hostStack> BS:Bytes : S => S </hostStack>
requires validSymbol(Bytes2String(BS))
endmodule
```
Loading

0 comments on commit aca440e

Please sign in to comment.