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 Dec 2, 2024
2 parents ac3be21 + 5ccc0b2 commit 5ad3c9c
Show file tree
Hide file tree
Showing 5 changed files with 375 additions and 3 deletions.
9 changes: 9 additions & 0 deletions src/komet/kdist/soroban-semantics/configuration.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,15 @@ module CONFIG-OPERATIONS
<k> dropStack => .K ... </k>
<hostStack> _V : S => S </hostStack>
// Allows using `pushStack` and `dropStack` in the `<instrs>` cell
rule [pushStack-instr]:
<instrs> pushStack(V) => .K ... </instrs>
<hostStack> S => V : S </hostStack>
rule [dropStack-instr]:
<instrs> dropStack => .K ... </instrs>
<hostStack> _V : S => S </hostStack>
```

## Call State
Expand Down
10 changes: 8 additions & 2 deletions src/komet/kdist/soroban-semantics/data.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -196,12 +196,18 @@ module HOST-OBJECT
syntax HostVal ::= List "{{" Int "}}" "orDefault" HostVal
[function, total, symbol(HostVal:getOrDefault)]
// ---------------------------------------------------------
rule OBJS {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ], D)
rule OBJS:List {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ], D)
requires 0 <=Int I andBool I <Int size(OBJS)
rule _OBJS {{ _I }} orDefault (D:HostVal) => D
rule _OBJS:List {{ _I }} orDefault (D:HostVal) => D
[owise]
// typed version of builtin MAP [ K ] orDefault V
syntax HostVal ::= Map "{{" KItem "}}" "orDefault" HostVal
[function, total, symbol(HostVal:lookupOrDefault)]
// ---------------------------------------------------------
rule OBJS:Map {{ I }} orDefault (D:HostVal) => HostValOrDefault(OBJS [ I ] orDefault D, D)
```

## Conversion between `HostVal` and `ScVal`
Expand Down
130 changes: 130 additions & 0 deletions src/komet/kdist/soroban-semantics/host/map.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,136 @@ module HOST-MAP
imports SWITCH-SYNTAX
```

## map_new

```k
rule [hostfun-map-new]:
<instrs> hostCall ( "m" , "_" , [ .ValTypes ] -> [ i64 .ValTypes ] )
=> allocObject(ScMap(.Map))
~> returnHostVal
...
</instrs>
<locals> .Map </locals>
```

## map_put

```k
rule [hostfun-map-put]:
<instrs> hostCall ( "m" , "0" , [ i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> pushStack(HostVal(VAL))
~> loadObjectFull(HostVal(KEY))
~> loadObject(HostVal(M))
~> hostCallAux("m", "0")
...
</instrs>
<locals>
0 |-> < i64 > M
1 |-> < i64 > KEY
2 |-> < i64 > VAL
</locals>
rule [hostCallAux-map-put]:
<instrs> hostCallAux("m", "0")
=> allocObject(ScMap( M [ KEY <- VAL ] ))
~> returnHostVal
...
</instrs>
<hostStack> ScMap(M) : KEY:ScVal : VAL:HostVal : S => S </hostStack>
```

## map_get

```k
rule [hostfun-map-get]:
<instrs> hostCall ( "m" , "1" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObjectFull(HostVal(KEY))
~> loadObject(HostVal(M))
~> hostCallAux("m", "1")
...
</instrs>
<locals>
0 |-> < i64 > M
1 |-> < i64 > KEY
</locals>
rule [hostCallAux-map-get]:
<instrs> hostCallAux("m", "1")
=> pushStack( M {{ KEY }} orDefault HostVal(-1) )
~> returnHostVal
...
</instrs>
<hostStack> ScMap(M) : KEY:ScVal : S => S </hostStack>
requires KEY in_keys(M)
rule [hostCallAux-map-get-not-found]:
<instrs> hostCallAux("m", "1") => trap ... </instrs>
<hostStack> ScMap(M) : KEY:ScVal : S => S </hostStack>
requires notBool( KEY in_keys(M) )
```

## map_del

```k
rule [hostfun-map-del]:
<instrs> hostCall ( "m" , "2" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObjectFull(HostVal(KEY))
~> loadObject(HostVal(M))
~> hostCallAux("m", "2")
...
</instrs>
<locals>
0 |-> < i64 > M
1 |-> < i64 > KEY
</locals>
rule [hostCallAux-map-del]:
<instrs> hostCallAux("m", "2")
=> allocObject(ScMap( M [ KEY <- undef ] ))
~> returnHostVal
...
</instrs>
<hostStack> ScMap(M) : KEY:ScVal : S => S </hostStack>
requires KEY in_keys(M)
rule [hostCallAux-map-del-not-found]:
<instrs> hostCallAux("m", "2") => trap ... </instrs>
<hostStack> ScMap(M) : KEY:ScVal : S => S </hostStack>
requires notBool( KEY in_keys(M) )
```

## map_len

```k
rule [hostCallAux-map-len]:
<instrs> hostCallAux("m", "3") => toSmall(U32(size(M))) ... </instrs>
<hostStack> ScMap(M) : S => S </hostStack>
```

## map_has

```k
rule [hostfun-map-has]:
<instrs> hostCall ( "m" , "4" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObjectFull(HostVal(KEY))
~> loadObject(HostVal(M))
~> hostCallAux("m", "4")
...
</instrs>
<locals>
0 |-> < i64 > M
1 |-> < i64 > KEY
</locals>
rule [hostCallAux-map-has]:
<instrs> hostCallAux("m", "4") => toSmall(SCBool( KEY in_keys(M) )) ... </instrs>
<hostStack> ScMap(M) : KEY:ScVal : S => S </hostStack>
```

## map_unpack_to_linear_memory

Writes values from a map (`ScMap`) to a specified memory address.
Expand Down
38 changes: 37 additions & 1 deletion src/komet/kdist/soroban-semantics/wasm-ops.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,42 @@ module WASM-OPERATIONS
[owise]
```

## Host function operations

- `hostCallAux(MOD,FUNC)`: Helper instruction for implementing host functions with arguments already loaded onto the
host stack. Reduces the need to define custom `InternalInstr` productions for each host function.
The `hostCall-default` rule provides default behavior for host functions without complex argument handling, allowing
`hostCallAux` to streamline the process further.
- `loadArgs(N)`: Loads the first `N` arguments onto the host stack using `loadObject` starting from the last argument.
This positions the first argument at the top of the stack at the end.

```k
syntax InternalInstr ::= hostCallAux(String, String) [symbol(hostCallAux)]
| loadArgs(Int) [symbol(loadArgs)]
// Default implementation for `hostCall`. Loads the arguments to the host stack using `loadObject`
rule [hostCall-default]:
<instrs> hostCall(MOD, FUNC, [ _ARGS ] -> [ _RET ])
=> loadArgs(size(LOCALS))
~> hostCallAux(MOD, FUNC)
...
</instrs>
<locals> LOCALS </locals>
[owise]
rule [loadArgs-empty]:
<instrs> loadArgs(0) => .K ... </instrs>
rule [loadArgs]:
<instrs> loadArgs(I)
=> loadObject(HostVal(X))
~> loadArgs(I -Int 1)
...
</instrs>
<locals> ... (I -Int 1) |-> <i64> X ... </locals>
```

```k
endmodule
```
```
Loading

0 comments on commit 5ad3c9c

Please sign in to comment.