Skip to content

Commit

Permalink
Merge branch 'master' into i128
Browse files Browse the repository at this point in the history
  • Loading branch information
@bbyalcinkaya
bbyalcinkaya authored Nov 19, 2024
2 parents 8bd1335 + 50117c0 commit b67155a
Show file tree
Hide file tree
Showing 17 changed files with 604 additions and 137 deletions.
2 changes: 1 addition & 1 deletion deps/k_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
7.1.165
7.1.167
2 changes: 1 addition & 1 deletion deps/kwasm_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.112
0.1.113
30 changes: 15 additions & 15 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion flake.nix
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
description = "komet - K tooling for the Soroban platform";

inputs = {
wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.112";
wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.113";
k-framework.follows = "wasm-semantics/k-framework";
nixpkgs.follows = "k-framework/nixpkgs";
flake-utils.follows = "k-framework/flake-utils";
Expand Down
2 changes: 1 addition & 1 deletion package/version
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.39
0.1.41
157 changes: 99 additions & 58 deletions poetry.lock
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "komet"
version = "0.1.39"
version = "0.1.41"
description = "K tooling for the Soroban platform"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand All @@ -18,7 +18,7 @@ soroban-semantics = "komet.kdist.plugin"

[tool.poetry.dependencies]
python = "^3.10"
pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.112", subdirectory = "pykwasm" }
pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.113", subdirectory = "pykwasm" }

[tool.poetry.group.dev.dependencies]
autoflake = "*"
Expand Down
12 changes: 11 additions & 1 deletion src/komet/kdist/soroban-semantics/configuration.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ module CONFIG
Keys and values must be fully resolved `ScVal`s as in `<instanceStorage>`.

```k
<contractData> .Map </contractData> // Map of StorageKey to ScVal
<contractData> .Map </contractData> // Map of StorageKey to StorageVal
<contractCodes>
<contractCode multiplicity="*" type="Map">
<codeHash> .Bytes </codeHash>
Expand Down Expand Up @@ -99,6 +99,8 @@ module CONFIG
syntax StorageKey ::= #skey( ContractId , Durability , ScVal ) [symbol(StorageKey)]
syntax StorageVal ::= #sval( ScVal , Int ) [symbol(StorageVal)]
endmodule
```

Expand Down Expand Up @@ -470,6 +472,14 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
```

## Exception throwing

```k
syntax InternalInstr ::= #throw(ErrorType, Int) [symbol(throw)]
// ------------------------------------------------------------------
rule [throw]:
<instrs> #throw(ERRTYPE, CODE) ~> _REST => .K </instrs>
<hostStack> S => Error(ERRTYPE, CODE) : S </hostStack>
endmodule
```
4 changes: 2 additions & 2 deletions src/komet/kdist/soroban-semantics/data.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,8 +144,8 @@ module HOST-OBJECT
// https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#tag-values
syntax Int ::= getTag(ScVal) [function, total]
// -----------------------------------------------------
rule getTag(SCBool(true)) => 0
rule getTag(SCBool(false)) => 1
rule getTag(SCBool(false)) => 0
rule getTag(SCBool(true)) => 1
rule getTag(Void) => 2
rule getTag(Error(_,_)) => 3
rule getTag(U32(_)) => 4
Expand Down
112 changes: 108 additions & 4 deletions src/komet/kdist/soroban-semantics/host/ledger.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,14 +37,26 @@ module HOST-LEDGER
...
</contract>
rule [putContractData-other]:
rule [putContractData-other-existing]:
<instrs> putContractData(DUR:Durability) => toSmall(Void) ... </instrs>
<hostStack> KEY : VAL : S => S </hostStack>
<callee> CONTRACT </callee>
<contractData>
STORAGE => STORAGE [ #skey(CONTRACT, DUR, KEY) <- VAL ]
...
#skey(CONTRACT, DUR, KEY) |-> #sval(_ => VAL, _LIVE_UNTIL)
...
</contractData>
rule [putContractData-other-new]:
<instrs> putContractData(DUR:Durability) => toSmall(Void) ... </instrs>
<hostStack> KEY : VAL : S => S </hostStack>
<callee> CONTRACT </callee>
<contractData>
STORAGE => STORAGE [ #skey(CONTRACT, DUR, KEY) <- #sval(VAL, minLiveUntil(DUR, SEQ)) ]
</contractData>
<ledgerSequenceNumber> SEQ </ledgerSequenceNumber>
requires notBool( #skey(CONTRACT, DUR, KEY) in_keys(STORAGE) )
```

## has_contract_data
Expand Down Expand Up @@ -126,7 +138,7 @@ module HOST-LEDGER
</instrs>
<hostStack> KEY : S => S </hostStack>
<callee> CONTRACT </callee>
<contractData> ... #skey(CONTRACT, DUR, KEY) |-> VAL ... </contractData>
<contractData> ... #skey(CONTRACT, DUR, KEY) |-> #sval(VAL, _) ... </contractData>
```

Expand Down Expand Up @@ -165,6 +177,83 @@ module HOST-LEDGER
<contractData> MAP => MAP [#skey(CONTRACT, DUR, KEY) <- undef ] </contractData>
requires #skey(CONTRACT, DUR, KEY) in_keys(MAP)
```
## update_current_contract_wasm

```k
rule [hostfun-update-current-contract-wasm]:
<instrs> hostCall ( "l" , "6" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(HASH))
~> updateContractWasm(CALLEE)
~> toSmall(Void)
...
</instrs>
<locals>
0 |-> < i64 > HASH // Bytes
</locals>
<callee> CALLEE </callee>
syntax InternalInstr ::= updateContractWasm(ContractId) [symbol(updateContractWasm)]
// --------------------------------------------------------------------------------------
rule [updateContractWasm]:
<instrs> updateContractWasm(CONTRACT) => .K ... </instrs>
<hostStack> ScBytes(HASH) : S => S </hostStack>
<contract>
<contractId> CONTRACT </contractId>
<wasmHash> _ => HASH </wasmHash>
...
</contract>
<contractCode>
<codeHash> HASH </codeHash>
...
</contractCode>
```

## extend_contract_data_ttl

```k
rule [hostfun-extend-contract-data-ttl]:
<instrs> hostCall ( "l" , "7" , [ i64 i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(EXTEND_TO))
~> loadObject(HostVal(THRESHOLD))
~> loadObjectFull(HostVal(KEY))
~> extendContractDataTtl(CONTRACT, Int2StorageType(STORAGE_TYPE))
~> toSmall(Void)
...
</instrs>
<locals>
0 |-> < i64 > KEY // HostVal
1 |-> < i64 > STORAGE_TYPE // 0: temp, 1: persistent, 2: instance
2 |-> < i64 > THRESHOLD // U32
3 |-> < i64 > EXTEND_TO // U32
</locals>
<callee> CONTRACT </callee>
requires Int2StorageTypeValid(STORAGE_TYPE)
syntax InternalInstr ::= extendContractDataTtl(ContractId, StorageType) [symbol(extendContractDataTtl)]
// --------------------------------------------------------------------------------------------
rule [extendContractDataTtl]:
<instrs> extendContractDataTtl(CONTRACT, DUR:Durability) => .K ... </instrs>
<hostStack> KEY:ScVal : U32(THRESHOLD) : U32(EXTEND_TO) : S => S </hostStack>
<contractData>
...
#skey(CONTRACT, DUR, KEY)
|-> #sval(_VAL, LIVE_UNTIL => extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO))
...
</contractData>
<ledgerSequenceNumber> SEQ </ledgerSequenceNumber>
requires THRESHOLD <=Int EXTEND_TO // input is valid
andBool SEQ <=Int LIVE_UNTIL // entry is alive
andBool ( DUR =/=K #temporary
orBool extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) <=Int maxLiveUntil(SEQ)
) // #temporary TTLs has to be exact
rule [extendContractDataTtl-err]:
<instrs> extendContractDataTtl(_CONTRACT, _TYP) => #throw(ErrStorage, InvalidAction) ... </instrs>
<hostStack> _KEY:ScVal : U32(_THRESHOLD) : U32(_EXTEND_TO) : S => S </hostStack>
[owise]
```

## extend_current_contract_instance_and_code_ttl
Expand Down Expand Up @@ -207,7 +296,8 @@ module HOST-LEDGER
syntax Int ::= extendedLiveUntil(Int, Int, Int, Int) [function, total]
// -----------------------------------------------------------------------------------
rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) => SEQ +Int EXTEND_TO
rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO)
=> minInt( SEQ +Int EXTEND_TO , maxLiveUntil(SEQ) )
requires LIVE_UNTIL -Int SEQ <=Int THRESHOLD // CURRENT_TTL <= THRESHOLD
andBool LIVE_UNTIL <Int SEQ +Int EXTEND_TO // LIVE_UNTIL < NEW_LIVE_UNTIL
Expand Down Expand Up @@ -257,5 +347,19 @@ module HOST-LEDGER
// ------------------------------------------------------------
rule Int2StorageTypeValid(I) => 0 <=Int I andBool I <=Int 2
// make these values variable
syntax Int ::= minEntryTtl(Durability) [function, total]
| "#maxEntryTtl" [macro]
// -------------------------------------------------
rule minEntryTtl(#temporary) => 16
rule minEntryTtl(#persistent) => 4096
rule #maxEntryTtl => 6312000
syntax Int ::= minLiveUntil(Durability, Int) [function, total]
| maxLiveUntil(Int) [function, total]
// -----------------------------------------------------------------------
rule minLiveUntil(DUR, SEQ) => SEQ +Int minEntryTtl(DUR) -Int 1
rule maxLiveUntil(SEQ) => SEQ +Int #maxEntryTtl -Int 1
endmodule
```
42 changes: 0 additions & 42 deletions src/komet/kdist/soroban-semantics/host/map.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,47 +102,5 @@ The function returns a `HostVal` pointing to the new map object.
<relativeObjects> RELS </relativeObjects>
requires size(KEYS) ==Int lengthBytes(VALS_BS) /Int 8
```

## Helpers


```k
syntax List ::= Bytes2U32List(Bytes) [function, total, symbol(Bytes2U32List)]
// --------------------------------------------------------------------------------
rule Bytes2U32List(BS) => ListItem(Bytes2Int(substrBytes(BS, 0, 4), LE, Unsigned))
Bytes2U32List(substrBytes(BS, 4, lengthBytes(BS)))
requires lengthBytes(BS) >=Int 4
rule Bytes2U32List(BS) => .List
requires lengthBytes(BS) <Int 4
```

- `loadSlices`: Load symbols stored as byte slices in Wasm memory.

```k
syntax InternalInstr ::= "loadSlices" [symbol(loadSlices)]
| loadSlicesAux(List) [symbol(loadSlicesAux)]
// ---------------------------------------------------------------------------------
rule [loadSlices]:
<instrs> loadSlices
=> loadSlicesAux(Bytes2U32List(KEY_SLICES))
~> collectStackObjects(lengthBytes(KEY_SLICES) /Int 8)
...
</instrs>
<hostStack> KEY_SLICES : S => S </hostStack>
rule [loadSlicesAux-empty]:
<instrs> loadSlicesAux(.List) => .K ... </instrs>
rule [loadSlicesAux]:
<instrs> loadSlicesAux(REST ListItem(OFFSET) ListItem(LEN))
=> #memLoad(OFFSET, LEN)
~> mkSymbolFromStack
~> loadSlicesAux(REST)
...
</instrs>
endmodule
```
Loading

0 comments on commit b67155a

Please sign in to comment.