Skip to content

Commit

Permalink
Drop . in favour of .K (#204)
Browse files Browse the repository at this point in the history 
* Drop . in favour of .K

* Set Version: 0.1.3

* Set Version: 0.1.4

---------

Co-authored-by: devops <[email protected]>
  • Loading branch information
@Baltoli
Baltoli and devops authored Feb 21, 2024
1 parent 183fefd commit fc55f10
Show file tree
Hide file tree
Showing 13 changed files with 183 additions and 183 deletions.
6 changes: 3 additions & 3 deletions auto-allocate.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ module WASM-AUTO-ALLOCATE
syntax Stmt ::= "newEmptyModule" WasmString
// -------------------------------------------
rule <instrs> newEmptyModule MODNAME => . ... </instrs>
rule <instrs> newEmptyModule MODNAME => .K ... </instrs>
<moduleRegistry> MR => MR [ MODNAME <- NEXT ] </moduleRegistry>
<nextModuleIdx> NEXT => NEXT +Int 1 </nextModuleIdx>
<moduleInstances> ( .Bag => <moduleInst> <modIdx> NEXT </modIdx> ... </moduleInst>) ... </moduleInstances>
Expand Down Expand Up @@ -50,7 +50,7 @@ It is treated purely as a key set -- the actual stored values are not used or st
syntax Instr ::= hostCall(String, String, FuncType)
// ---------------------------------------------------
rule <instrs> (. => allocfunc(HOSTMOD, NEXTADDR, TYPE, [ .ValTypes ], hostCall(wasmString2StringStripped(MOD), wasmString2StringStripped(NAME), TYPE) .Instrs, #meta(... id: String2Identifier("$auto-alloc:" +String #parseWasmString(MOD) +String ":" +String #parseWasmString(NAME) ), localIds: .Map )))
rule <instrs> (.K => allocfunc(HOSTMOD, NEXTADDR, TYPE, [ .ValTypes ], hostCall(wasmString2StringStripped(MOD), wasmString2StringStripped(NAME), TYPE) .Instrs, #meta(... id: String2Identifier("$auto-alloc:" +String #parseWasmString(MOD) +String ":" +String #parseWasmString(NAME) ), localIds: .Map )))
~> #import(MOD, NAME, #funcDesc(... type: TIDX))
...
</instrs>
Expand Down Expand Up @@ -81,4 +81,4 @@ It is treated purely as a key set -- the actual stored values are not used or st
rule #stripQuotes(S) => replaceAll(S, "\"", "")
endmodule
```
```
52 changes: 26 additions & 26 deletions elrond-config.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ module ELROND-CONFIG
requires 0 <=Int #signed(i32 , OFFSET)
andBool #signed(i32 , OFFSET) +Int lengthBytes(BS) >Int (SIZE *Int #pageSize())
rule <instrs> #memStore(OFFSET, BS) => . ... </instrs>
rule <instrs> #memStore(OFFSET, BS) => .K ... </instrs>
<contractModIdx> MODIDX:Int </contractModIdx>
<moduleInst>
<modIdx> MODIDX </modIdx>
Expand Down Expand Up @@ -100,7 +100,7 @@ module ELROND-CONFIG
requires #signed(i32 , LENGTH) <Int 0
rule [memLoad-zero-length]:
<instrs> #memLoad(_, 0) => . ... </instrs>
<instrs> #memLoad(_, 0) => .K ... </instrs>
<bytesStack> STACK => .Bytes : STACK </bytesStack>
rule [memLoad-bad-bounds]:
Expand All @@ -121,7 +121,7 @@ module ELROND-CONFIG
orBool #signed(i32 , OFFSET) +Int #signed(i32 , LENGTH) >Int (SIZE *Int #pageSize()))
rule [memLoad]:
<instrs> #memLoad(OFFSET, LENGTH) => . ... </instrs>
<instrs> #memLoad(OFFSET, LENGTH) => .K ... </instrs>
<bytesStack> STACK => #getBytesRange(DATA, OFFSET, LENGTH) : STACK </bytesStack>
<contractModIdx> MODIDX:Int </contractModIdx>
<moduleInst>
Expand Down Expand Up @@ -189,7 +189,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
syntax InternalInstr ::= #isReservedKey ( String )
// --------------------------------------------------
rule <instrs> #isReservedKey(KEY) => . ... </instrs>
rule <instrs> #isReservedKey(KEY) => .K ... </instrs>
requires notBool #hasPrefix(KEY, "ELROND")
rule <instrs> #isReservedKey(KEY)
Expand All @@ -205,7 +205,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
<callee> CALLEE </callee>
rule [storageLoadFromAddress]:
<instrs> #storageLoadFromAddress => . ... </instrs>
<instrs> #storageLoadFromAddress => .K ... </instrs>
<bytesStack> ADDR : KEY : STACK => #lookupStorage(STORAGE, KEY) : STACK </bytesStack>
<account>
<address> ADDR </address>
Expand Down Expand Up @@ -312,11 +312,11 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
syntax InternalInstr ::= "#appendToOutFromBytesStack"
| #appendToOut ( Bytes )
// -----------------------------------------------
rule <instrs> #appendToOutFromBytesStack => . ... </instrs>
rule <instrs> #appendToOutFromBytesStack => .K ... </instrs>
<bytesStack> OUT : STACK => STACK </bytesStack>
<out> ... (.ListBytes => ListItem(wrap(OUT))) </out>
rule <instrs> #appendToOut(OUT) => . ... </instrs>
rule <instrs> #appendToOut(OUT) => .K ... </instrs>
<out> ... (.ListBytes => ListItem(wrap(OUT))) </out>
```

Expand Down Expand Up @@ -393,7 +393,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
<bytesStack> DATA : STACK => STACK </bytesStack>
<valstack> <i32> NUMTOPICS : <i32> _ : VALSTACK => VALSTACK </valstack>
rule <instrs> #writeLogAux(1, TOPICS, DATA) => . ... </instrs>
rule <instrs> #writeLogAux(1, TOPICS, DATA) => .K ... </instrs>
<bytesStack> IDENTIFIER : STACK => STACK </bytesStack>
<callee> CALLEE </callee>
<logs> ... (.List => ListItem(logEntry(CALLEE, IDENTIFIER, TOPICS, DATA))) </logs>
Expand All @@ -415,16 +415,16 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
syntax InternalCmd ::= "#endWasm"
// ---------------------------------
rule <commands> #endWasm => popCallState ~> dropWorldState ... </commands>
<instrs> . </instrs>
<instrs> .K </instrs>
<out> OUT </out>
<logs> LOGS </logs>
<vmOutput> _ => VMOutput( OK , .Bytes , OUT , LOGS) </vmOutput>
[priority(60)]
syntax InternalCmd ::= "#waitWasm" [klabel(#waitWasm), symbol]
// ----------------------------------
rule <commands> #waitWasm => . ... </commands>
<instrs> . </instrs>
rule <commands> #waitWasm => .K ... </commands>
<instrs> .K </instrs>
[priority(60)]
```

Expand All @@ -441,7 +441,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
<vmOutput> .VMOutput => VMOutput( EC , MSG , .ListBytes , .List) </vmOutput>
rule [exception-skip]:
<commands> #exception(_,_) ~> (CMD:InternalCmd => . ) ... </commands>
<commands> #exception(_,_) ~> (CMD:InternalCmd => .K ) ... </commands>
requires CMD =/=K #endWasm
```
Expand All @@ -462,8 +462,8 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
</commands>
rule [throwExceptionBs]:
<instrs> (#throwExceptionBs( EC , MSG ) ~> _ ) => . </instrs>
<commands> (. => #exception(EC,MSG)) ... </commands>
<instrs> (#throwExceptionBs( EC , MSG ) ~> _ ) => .K </instrs>
<commands> (.K => #exception(EC,MSG)) ... </commands>
<logging> S => S +String " -- Exception: " +String Bytes2String(MSG) </logging>
rule [throwExceptionBs-cmd]:
<commands> (#throwExceptionBs( EC , MSG ) => #exception(EC,MSG)) ... </commands>
Expand All @@ -489,7 +489,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
// ------------------------------------------------------------------------------
// ignore if the account already exists
rule [createAccount-existing]:
<commands> createAccount(ADDR) => . ... </commands>
<commands> createAccount(ADDR) => .K ... </commands>
<account>
<address> ADDR </address>
...
Expand All @@ -498,7 +498,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
[priority(60)]
rule [createAccount-new]:
<commands> createAccount(ADDR) => . ... </commands>
<commands> createAccount(ADDR) => .K ... </commands>
<accounts>
( .Bag
=> <account>
Expand All @@ -516,7 +516,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
| setAccountOwner ( Bytes, Bytes )
// ---------------------------------------------------------------
rule [setAccountFields]:
<commands> setAccountFields(ADDR, NONCE, BALANCE, CODE, OWNER_ADDR, STORAGE) => . ... </commands>
<commands> setAccountFields(ADDR, NONCE, BALANCE, CODE, OWNER_ADDR, STORAGE) => .K ... </commands>
<account>
<address> ADDR </address>
<nonce> _ => NONCE </nonce>
Expand All @@ -529,15 +529,15 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
[priority(60)]
rule [setAccountCode]:
<commands> setAccountCode(ADDR, CODE) => . ... </commands>
<commands> setAccountCode(ADDR, CODE) => .K ... </commands>
<account>
<address> ADDR </address>
<code> _ => CODE </code>
...
</account>
[priority(60)]
rule <commands> setAccountOwner(ADDR, OWNER) => . ... </commands>
rule <commands> setAccountOwner(ADDR, OWNER) => .K ... </commands>
<account>
<address> ADDR </address>
<ownerAddress> _ => OWNER </ownerAddress>
Expand Down Expand Up @@ -603,8 +603,8 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
requires VALUE >Int ORIGFROM
[priority(60)]
rule <commands> #transferSuccess => . ... </commands>
<instrs> . </instrs>
rule <commands> #transferSuccess => .K ... </commands>
<instrs> .K </instrs>
```

## Calling Contract
Expand Down Expand Up @@ -706,7 +706,7 @@ Every contract call runs in its own Wasm instance initialized with the contract'
// clause.
rule [setContractModIdx]:
<commands> setContractModIdx => . ... </commands>
<commands> setContractModIdx => .K ... </commands>
<contractModIdx> _ => NEXTIDX -Int 1 </contractModIdx>
<nextModuleIdx> NEXTIDX </nextModuleIdx>
Expand All @@ -722,13 +722,13 @@ Initialize the call state and invoke the endpoint function:

```k
rule [mkCall]:
<commands> mkCall(TO, FUNCNAME:WasmStringToken, VMINPUT) => . ... </commands>
<commands> mkCall(TO, FUNCNAME:WasmStringToken, VMINPUT) => .K ... </commands>
<callState>
<callee> _ => TO </callee>
(_:VmInputCell => VMINPUT)
// executional
<wasm>
<instrs> . => ( invoke FUNCADDRS {{ FUNCIDX }} orDefault -1 ) </instrs>
<instrs> .K => ( invoke FUNCADDRS {{ FUNCIDX }} orDefault -1 ) </instrs>
<moduleInst>
<modIdx> MODIDX </modIdx>
<exports> ... FUNCNAME |-> FUNCIDX:Int </exports>
Expand All @@ -749,14 +749,14 @@ Initialize the call state and invoke the endpoint function:
[priority(60)]
rule [mkCall-func-not-found]:
<commands> mkCall(_TO, FUNCNAME:WasmStringToken, _VMINPUT) => . ... </commands>
<commands> mkCall(_TO, FUNCNAME:WasmStringToken, _VMINPUT) => .K ... </commands>
<contractModIdx> MODIDX:Int </contractModIdx>
<moduleInst>
<modIdx> MODIDX </modIdx>
<exports> EXPORTS </exports>
...
</moduleInst>
<instrs> . => #throwException(FunctionNotFound, "invalid function (not found)") </instrs>
<instrs> .K => #throwException(FunctionNotFound, "invalid function (not found)") </instrs>
<logging> S => S +String " -- callContract not found " +String #parseWasmString(FUNCNAME) </logging>
requires notBool( FUNCNAME in_keys(EXPORTS) )
[priority(60)]
Expand Down
26 changes: 13 additions & 13 deletions elrond-node.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,10 +137,10 @@ Storage maps byte arrays to byte arrays.
syntax BytesOp ::= #pushBytes ( Bytes )
| "#dropBytes"
// ---------------------------------------
rule <instrs> #pushBytes(BS) => . ... </instrs>
rule <instrs> #pushBytes(BS) => .K ... </instrs>
<bytesStack> STACK => BS : STACK </bytesStack>
rule <instrs> #dropBytes => . ... </instrs>
rule <instrs> #dropBytes => .K ... </instrs>
<bytesStack> _ : STACK => STACK </bytesStack>
syntax InternalInstr ::= "#returnLength"
Expand All @@ -163,23 +163,23 @@ The `<callStack>` cell stores a list of previous contract execution states. Thes
syntax InternalCmd ::= "pushCallState" [klabel(pushCallState), symbol]
// ---------------------------------------
rule [pushCallState]:
<commands> pushCallState => . ... </commands>
<commands> pushCallState => .K ... </commands>
<callStack> (.List => ListItem(CALLSTATE)) ... </callStack>
<callState> CALLSTATE </callState>
[priority(60)]
syntax InternalCmd ::= "popCallState" [klabel(popCallState), symbol]
// --------------------------------------
rule [popCallState]:
<commands> popCallState => . ... </commands>
<commands> popCallState => .K ... </commands>
<callStack> (ListItem(CALLSTATE) => .List) ... </callStack>
<callState> _ => CALLSTATE </callState>
[priority(60)]
syntax InternalCmd ::= "dropCallState" [klabel(dropCallState), symbol]
// ---------------------------------------
rule [dropCallState]:
<commands> dropCallState => . ... </commands>
<commands> dropCallState => .K ... </commands>
<callStack> (ListItem(_) => .List) ... </callStack>
[priority(60)]
```
Expand All @@ -195,23 +195,23 @@ The `<callStack>` cell stores a list of previous contract execution states. Thes
syntax InternalCmd ::= "pushWorldState" [klabel(pushWorldState), symbol]
// ---------------------------------------
rule [pushWorldState]:
<commands> pushWorldState => . ... </commands>
<commands> pushWorldState => .K ... </commands>
<interimStates> (.List => ListItem({ ACCTDATA })) ... </interimStates>
<accounts> ACCTDATA </accounts>
[priority(60)]
syntax InternalCmd ::= "popWorldState" [klabel(popWorldState), symbol]
// --------------------------------------
rule [popWorldState]:
<commands> popWorldState => . ... </commands>
<commands> popWorldState => .K ... </commands>
<interimStates> (ListItem({ ACCTDATA }) => .List) ... </interimStates>
<accounts> _ => ACCTDATA </accounts>
[priority(60)]
syntax InternalCmd ::= "dropWorldState" [klabel(dropWorldState), symbol]
// ---------------------------------------
rule [dropWorldState]:
<commands> dropWorldState => . ... </commands>
<commands> dropWorldState => .K ... </commands>
<interimStates> (ListItem(_) => .List) ... </interimStates>
[priority(60)]
```
Expand All @@ -224,7 +224,7 @@ The `<callStack>` cell stores a list of previous contract execution states. Thes
syntax InternalCmd ::= checkAccountExists( Bytes )
// ------------------------------------------------------
rule [checkAccountExists-pass]:
<commands> checkAccountExists(ADDR) => . ... </commands>
<commands> checkAccountExists(ADDR) => .K ... </commands>
<account>
<address> ADDR </address>
...
Expand Down Expand Up @@ -256,7 +256,7 @@ The `<callStack>` cell stores a list of previous contract execution states. Thes
syntax InternalCmd ::= checkBool(Bool, String) [klabel(checkBool), symbol]
// -----------------------------------------------------------------------------------
rule [checkBool-t]:
<commands> checkBool(true, _) => . ... </commands>
<commands> checkBool(true, _) => .K ... </commands>
rule [checkBool-f]:
<commands> checkBool(false, ERR) => #throwExceptionBs(ExecutionFailed, String2Bytes(ERR)) ... </commands>
Expand All @@ -267,8 +267,8 @@ The `<callStack>` cell stores a list of previous contract execution states. Thes
syntax InternalCmd ::= "resetCallstate" [klabel(resetCallState), symbol]
// ---------------------------------------------------------------------------
rule [resetCallstate]:
<commands> resetCallstate => . ... </commands>
(_:CallStateCell => <callState> <instrs> . </instrs> ... </callState>)
<commands> resetCallstate => .K ... </commands>
(_:CallStateCell => <callState> <instrs> .K </instrs> ... </callState>)
endmodule
```
```
12 changes: 6 additions & 6 deletions esdt.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ module ESDT
syntax InternalCmd ::= checkESDTBalance(account: Bytes, token: Bytes, value: Int)
// ------------------------------------------------------
rule [checkESDTBalance]:
<commands> checkESDTBalance(ACCT, TOKEN, VALUE) => . ... </commands>
<commands> checkESDTBalance(ACCT, TOKEN, VALUE) => .K ... </commands>
<account>
<address> ACCT </address>
<esdtData>
Expand All @@ -64,7 +64,7 @@ module ESDT
syntax InternalCmd ::= addToESDTBalance(account: Bytes, token: Bytes, delta: Int)
// ------------------------------------------------------
rule [addToESDTBalance]:
<commands> addToESDTBalance(ACCT, TOKEN, DELTA) => . ... </commands>
<commands> addToESDTBalance(ACCT, TOKEN, DELTA) => .K ... </commands>
<account>
<address> ACCT </address>
<esdtData>
Expand All @@ -77,7 +77,7 @@ module ESDT
[priority(60)]
rule [addToESDTBalance-new-esdtData]:
<commands> addToESDTBalance(ACCT, TOKEN, DELTA) => . ... </commands>
<commands> addToESDTBalance(ACCT, TOKEN, DELTA) => .K ... </commands>
<account>
<address> ACCT </address>
(.Bag => <esdtData>
Expand Down Expand Up @@ -222,7 +222,7 @@ module ESDT
rule [determineIsSCCallAfter-nocall]:
<commands> determineIsSCCallAfter(_SND, _DST, _FUNC, _VMINPUT)
=> . ...
=> .K ...
</commands>
[owise]
Expand Down Expand Up @@ -320,7 +320,7 @@ module ESDT
[klabel(checkAllowedToExecute), symbol]
// ----------------------------------------------------------------------------------------
rule [checkAllowedToExecute-pass]:
<commands> checkAllowedToExecute(ADDR, TOK, ROLE) => . ... </commands>
<commands> checkAllowedToExecute(ADDR, TOK, ROLE) => .K ... </commands>
<account>
<address> ADDR </address>
<esdtData>
Expand Down Expand Up @@ -356,4 +356,4 @@ module ESDT

```k
endmodule
```
```
2 changes: 1 addition & 1 deletion kmultiversx/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 = "kmultiversx"
version = "0.1.3"
version = "0.1.4"
description = "Python tools for Elrond semantics"
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
Loading

0 comments on commit fc55f10

Please sign in to comment.