From a8a0d5d54c2cdc1de4df3f2f2aaf8e3fb9bb141c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Mon, 17 Jun 2024 09:28:24 +0300 Subject: [PATCH] Booster improvements (#288) * `startPrank` match: `getbuffer` => `#getBuffer` * `memLoad-zero-length` match * `appendToOutAccount` definedness of `_Map_` * add `preserves-definedness` * Set Version: 0.1.80 --------- Co-authored-by: devops --- kmultiversx/pyproject.toml | 2 +- .../kdist/mx-semantics/elrond-config.md | 3 ++- .../kdist/mx-semantics/elrond-node.md | 21 +++++++++---------- .../kmultiversx/kdist/mx-semantics/kasmer.md | 17 +++++++-------- .../kdist/mx-semantics/vmhooks/manBufOps.md | 2 ++ .../kdist/mx-semantics/vmhooks/smallIntOps.md | 7 +++++++ package/version | 2 +- 7 files changed, 30 insertions(+), 24 deletions(-) diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index 8a5a5e89..d400f91e 100644 --- a/kmultiversx/pyproject.toml +++ b/kmultiversx/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmultiversx" -version = "0.1.79" +version = "0.1.80" description = "Python tools for Elrond semantics" authors = [ "Runtime Verification, Inc. ", diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md index 805d9a52..bf74790e 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md @@ -117,8 +117,9 @@ module ELROND-CONFIG requires #signed(i32 , LENGTH) #memLoad(_, 0) => .K ... + #memLoad(_, LENGTH) => .K ... STACK => .Bytes : STACK + requires LENGTH ==Int 0 rule [memLoad-bad-bounds]: #memLoad(OFFSET, LENGTH) => #throwException(ExecutionFailed, "mem load: bad bounds") ... diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md index f25eff5f..28016d4f 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md @@ -156,23 +156,22 @@ Storage maps byte arrays to byte arrays. rule [appendToOutAccount]: appendToOutAccount(ACC, T) => .K ... - ... - ACC |-> (OA => appendToOutTransfers(OA, T)) - ... + OAs => OAs [ ACC <- appendToOutTransfers( + { OAs [ ACC ] orDefault OutputAccount(ACC, .List) }:>OutputAccount, + T + ) ] requires nonZeroOutputTransfer(T) - [priority(60)] - - rule [appendToOutAccount-new-item]: - appendToOutAccount(ACC, T) => .K ... - OAs => OAs [ ACC <- OutputAccount(ACC, ListItem(T))] - requires nonZeroOutputTransfer(T) - [priority(61)] + andBool isOutputAccount( OAs [ ACC ] orDefault OutputAccount(ACC, .List) ) + [priority(60), preserves-definedness] + // Preserving definedness + // - Map[_<-_], Map[_]orDefault_ and appendToOutTransfers are total + // - {_}:>OutputAccount is checked rule [appendToOutAccount-zero]: appendToOutAccount(_, T) => .K ... requires notBool nonZeroOutputTransfer(T) - [priority(61)] + [priority(60)] syntax TransferValue ::= Int // EGLD transfer | List diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md index ff11c9c3..d8956fff 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md @@ -588,36 +588,33 @@ Only the `#kasmerRunner` account can execute these commands/host functions. ```k rule [testapi-startPrank]: hostCall ( "env" , "startPrank" , [ i32 .ValTypes ] -> [ .ValTypes ] ) - => #startPrank(getBuffer(ADDR_HANDLE)) ... + => #getBuffer(ADDR_HANDLE) + ~> #startPrank ... 0 |-> ADDR_HANDLE #kasmerRunner - syntax InternalInstr ::= #startPrank(BytesResult) + syntax InternalInstr ::= "#startPrank" // ------------------------------------------------- rule [startPrank]: - #startPrank(ADDR:Bytes) => .K ... + #startPrank => .K ... + ADDR:Bytes : S => S #kasmerRunner => ADDR false => true rule [startPrank-not-allowed]: - #startPrank(_:Bytes) + #startPrank => #throwException(ExecutionFailed, "Only the test contract can start a prank and the test contract can't start a prank while already pranking") ... + _:Bytes : S => S ADDR PRANK requires ADDR =/=K #kasmerRunner orBool PRANK - rule [startPrank-err]: - #startPrank(Err(MSG)) - => #throwException(ExecutionFailed, MSG) - ... - - rule [testapi-stopPrank]: hostCall ( "env" , "stopPrank" , [ .ValTypes ] -> [ .ValTypes ] ) => .K ... diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md index cf4d3365..8ce2f2f9 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md @@ -169,6 +169,8 @@ module MANBUFOPS 0 |-> ARG_IDX 1 |-> DEST_IDX ARGS requires #validArgIdx(ARG_IDX, ARGS) + [preserves-definedness] + // Preserving definedness: #validArgIdx(_) ensures Map {{ }} is defined // extern int32_t mBufferAppend(void* context, int32_t accumulatorHandle, int32_t dataHandle); rule hostCall("env", "mBufferAppend", [ i32 i32 .ValTypes ] -> [ i32 .ValTypes ] ) diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/smallIntOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/smallIntOps.md index dbfebbfa..643633bd 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/smallIntOps.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/smallIntOps.md @@ -57,6 +57,9 @@ module SMALLINTOPS ... 0 |-> VALUE + requires definedUnsigned(i64, VALUE) + [preserves-definedness] + // Preserving definedness: definedUnsigned(_) ensures #unsigned(_) is defined // extern void smallIntFinishSigned(void* context, long long value); rule hostCall("env", "smallIntFinishSigned", [ i64 .ValTypes ] -> [ .ValTypes ]) @@ -64,6 +67,10 @@ module SMALLINTOPS ... 0 |-> VALUE + requires definedSigned(i64, VALUE) + [preserves-definedness] + // Preserving definedness: definedSigned(_) ensures #signed(_) is defined + // extern int32_t smallIntStorageStoreUnsigned(void *context, int32_t keyOffset, int32_t keyLength, long long value); rule hostCall("env", "smallIntStorageStoreUnsigned", [ i32 i32 i64 .ValTypes ] -> [ i32 .ValTypes ]) diff --git a/package/version b/package/version index b9dbcf61..8c1c54a7 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.79 +0.1.80