Skip to content

Commit

Permalink
Merge branch 'master' into maps
Browse files Browse the repository at this point in the history
  • Loading branch information
@bbyalcinkaya
bbyalcinkaya authored Nov 19, 2024
2 parents fb96725 + f689855 commit 28f4664
Show file tree
Hide file tree
Showing 22 changed files with 913 additions and 68 deletions.
2 changes: 1 addition & 1 deletion package/version
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.41
0.1.42
2 changes: 1 addition & 1 deletion 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.41"
version = "0.1.42"
description = "K tooling for the Soroban platform"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
7 changes: 4 additions & 3 deletions src/komet/kasmer.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -270,6 +270,7 @@ def deploy_and_prove(
self,
contract_wasm: Path,
child_wasms: tuple[Path, ...],
id: str | None = None,
proof_dir: Path | None = None,
bug_report: BugReport | None = None,
) -> None:
Expand All @@ -290,9 +291,9 @@ def deploy_and_prove(

conf, subst = self.deploy_test(contract_kast, child_kasts, has_init)

for binding in bindings:
if not binding.name.startswith('test_'):
continue
test_bindings = [b for b in bindings if b.name.startswith('test_') and (id is None or b.name == id)]

for binding in test_bindings:
proof = self.run_prove(conf, subst, binding, proof_dir, bug_report)
if proof.status == ProofStatus.FAILED:
raise KSorobanError(proof.summary)
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 @@ -479,6 +481,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
```
37 changes: 34 additions & 3 deletions src/komet/kdist/soroban-semantics/data.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ various contexts:
| U64(Int) [symbol(SCVal:U64)]
| I64(Int) [symbol(SCVal:I64)]
| U128(Int) [symbol(SCVal:U128)]
| I128(Int) [symbol(SCVal:I128)]
| ScVec(List) [symbol(SCVal:Vec)] // List<HostVal>
| ScMap(Map) [symbol(SCVal:Map)] // Map<ScVal, HostVal>
| ScAddress(Address) [symbol(SCVal:Address)]
Expand Down Expand Up @@ -143,17 +144,20 @@ 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
rule getTag(I32(_)) => 5
rule getTag(U64(I)) => 6 requires I <=Int #maxU64small
rule getTag(U64(I)) => 64 requires notBool( I <=Int #maxU64small )
rule getTag(I64(_)) => 65 // I64small is not implemented
rule getTag(I64(I)) => 7 requires #minI64small <=Int I andBool I <=Int #maxI64small
rule getTag(I64(I)) => 65 requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small )
rule getTag(U128(I)) => 10 requires I <=Int #maxU64small
rule getTag(U128(I)) => 68 requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width
rule getTag(I128(I)) => 11 requires #minI64small <=Int I andBool I <=Int #maxI64small
rule getTag(I128(I)) => 69 requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small )
rule getTag(ScVec(_)) => 75
rule getTag(ScMap(_)) => 76
rule getTag(ScAddress(_)) => 77
Expand Down Expand Up @@ -231,8 +235,16 @@ module HOST-OBJECT
rule fromSmall(VAL) => U64(getBody(VAL)) requires getTag(VAL) ==Int 6
rule fromSmall(VAL) => I64(#signed(i56, getBody(VAL)))
requires getTag(VAL) ==Int 7
andBool definedSigned(i56, getBody(VAL))
rule fromSmall(VAL) => U128(getBody(VAL)) requires getTag(VAL) ==Int 10
rule fromSmall(VAL) => I128(#signed(i56, getBody(VAL)))
requires getTag(VAL) ==Int 11
andBool definedSigned(i56, getBody(VAL))
rule fromSmall(VAL) => Symbol(decode6bit(getBody(VAL)))
requires getTag(VAL) ==Int 14
Expand All @@ -255,7 +267,13 @@ module HOST-OBJECT
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(I64(I)) => fromBodyAndTag(#unsigned(i56, I), 7)
requires #minI64small <=Int I andBool I <=Int #maxI64small
andBool definedUnsigned(i56, I)
rule toSmall(U128(I)) => fromBodyAndTag(I, 10) requires I <=Int #maxU64small
rule toSmall(I128(I)) => fromBodyAndTag(#unsigned(i56, I), 11)
requires #minI64small <=Int I andBool I <=Int #maxI64small
andBool definedUnsigned(i56, I)
rule toSmall(Symbol(S)) => fromBodyAndTag(encode6bit(S), 14) requires lengthString(S) <=Int 9
rule toSmall(_) => HostVal(-1) [owise]
Expand Down Expand Up @@ -313,5 +331,18 @@ module HOST-OBJECT
rule tail(S) => "" requires lengthString(S) <=Int 0
rule tail(S) => substrString(S, 1, lengthString(S)) requires lengthString(S) >Int 0
// 56-bit integers for small values
syntax IWidth ::= "i56"
// ------------------------------------
rule #width(i56) => 56
rule #pow(i56) => 72057594037927936
rule #pow1(i56) => 36028797018963968
syntax IWidth ::= "i128"
// ------------------------------------
rule #width(i128) => 128
rule #pow(i128) => 340282366920938463463374607431768211456
rule #pow1(i128) => 170141183460469231731687303715884105728
endmodule
```
57 changes: 57 additions & 0 deletions src/komet/kdist/soroban-semantics/host/integer.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,17 @@ module HOST-INTEGER
</locals>
<k> (.K => allocObject(U64(I))) ... </k>
rule [hostfun-obj-from-i64]:
<instrs> hostCall ( "i" , "1" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> allocObject(I64(#signed(i64, VAL)))
~> returnHostVal
...
</instrs>
<locals>
0 |-> < i64 > VAL
</locals>
requires definedSigned(i64, VAL)
rule [hostfun-obj-to-i64]:
<instrs> hostCall ( "i" , "2" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(VAL))
Expand Down Expand Up @@ -99,5 +110,51 @@ module HOST-INTEGER
<hostStack> U128(I) : S => S </hostStack>
[preserves-definedness] // 'X >>Int K' is defined for positive K
rule [hostfun-obj-from-i128-pieces]:
<instrs> hostCall ( "i" , "6" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> allocObject(I128(#signed(i128, (HIGH <<Int 64) |Int LOW )))
~> returnHostVal
...
</instrs>
<locals>
0 |-> < i64 > HIGH
1 |-> < i64 > LOW
</locals>
requires definedSigned(i128, (HIGH <<Int 64) |Int LOW )
rule [hostfun-obj-to-i128-lo64]:
<instrs> hostCall ( "i" , "7" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(VAL))
~> i128lo64
...
</instrs>
<locals>
0 |-> < i64 > VAL
</locals>
syntax InternalInstr ::= "i128lo64" [symbol(i128lo64)]
// --------------------------------------------------------
rule [i128lo64]:
<instrs> i128lo64 => i64.const (#unsigned(i128, I)) ... </instrs>
<hostStack> I128(I) : S => S </hostStack>
requires definedUnsigned(i128, I)
[preserves-definedness]
rule [hostfun-obj-to-i128-hi64]:
<instrs> hostCall ( "i" , "8" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(VAL))
~> i128hi64
...
</instrs>
<locals>
0 |-> < i64 > VAL
</locals>
syntax InternalInstr ::= "i128hi64" [symbol(i128hi64)]
// --------------------------------------------------------
rule [i128hi64]:
<instrs> i128hi64 => i64.const (I >>Int 64) ... </instrs>
<hostStack> I128(I) : S => S </hostStack>
endmodule
```
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
```
Loading

0 comments on commit 28f4664

Please sign in to comment.