diff --git a/elrond-config.md b/elrond-config.md index 989801b0..daae74e3 100644 --- a/elrond-config.md +++ b/elrond-config.md @@ -737,7 +737,7 @@ Initialize the call state and invoke the endpoint function: ... - _ => .Map + _ => .MapIntToInt _ => .MapIntToBytes _ => .BytesStack MODIDX:Int diff --git a/elrond-node.md b/elrond-node.md index 77f5147c..374b149b 100644 --- a/elrond-node.md +++ b/elrond-node.md @@ -32,7 +32,7 @@ module ELROND-NODE // executional // every contract call uses its own wasm module instance, managed data heaps, and bytesStack. - .Map + .MapIntToInt .MapIntToBytes .BytesStack .Int diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index 93bdc06e..204812b6 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.1" +version = "0.1.2" description = "Python tools for Elrond semantics" authors = [ "Runtime Verification, Inc. ", diff --git a/package/version b/package/version index 17e51c38..d917d3e2 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.1 +0.1.2 diff --git a/vmhooks/bigIntOps.md b/vmhooks/bigIntOps.md index 9bd40e8d..08eac39b 100644 --- a/vmhooks/bigIntOps.md +++ b/vmhooks/bigIntOps.md @@ -17,41 +17,43 @@ module BIGINT-HELPERS syntax IntResult ::= getBigInt(Int) [function, total] // ------------------------------------------------------- rule [[ getBigInt(IDX) => I ]] - ... IDX |-> I:Int ... + ... wrap(IDX) Int2Int|-> wrap(I) ... rule getBigInt(_) => Err("no bigInt under the given handle") [owise] syntax InternalInstr ::= #getBigInt ( idx : Int , Signedness ) // --------------------------------------------------------------- rule #getBigInt(BIGINT_IDX, SIGN) => . ... - STACK => Int2Bytes({HEAP[BIGINT_IDX]}:>Int, BE, SIGN) : STACK + STACK => Int2Bytes(HEAP {{ BIGINT_IDX }} orDefault 0, BE, SIGN) : STACK HEAP - requires #validIntId(BIGINT_IDX, HEAP) + requires BIGINT_IDX in_keys{{ HEAP }} [preserves-definedness] // Preserving definedness: // - Int2Bytes is total - // - {HEAP[BIGINT_IDX]}:>Int because of #validIntId(BIGINT_IDX, HEAP) - + // - in_keys is total + // - '_{{_}} orDefault' is total + rule #getBigInt(BIGINT_IDX, _SIGN) => #throwException(ExecutionFailed, "no bigInt under the given handle") ... HEAP - requires notBool #validIntId(BIGINT_IDX, HEAP) + requires notBool( BIGINT_IDX in_keys{{ HEAP }} ) syntax InternalInstr ::= #getBigIntOrCreate ( idx : Int , Signedness ) // --------------------------------------------------------------- rule [getBigIntOrCreate-get]: #getBigIntOrCreate(BIGINT_IDX, SIGN) => . ... - STACK => Int2Bytes({HEAP[BIGINT_IDX]}:>Int, BE, SIGN) : STACK + STACK => Int2Bytes(HEAP {{ BIGINT_IDX }} orDefault 0, BE, SIGN) : STACK HEAP - requires #validIntId(BIGINT_IDX, HEAP) + requires BIGINT_IDX in_keys{{ HEAP }} [preserves-definedness] // Preserving definedness: // - Int2Bytes is total - // - {HEAP[BIGINT_IDX]}:>Int because of #validIntId(BIGINT_IDX, HEAP) + // - in_keys is total + // - '_{{_}} orDefault' is total rule [getBigIntOrCreate-create]: #getBigIntOrCreate(BIGINT_IDX, SIGN) => #setBigIntValue(BIGINT_IDX, 0) ... STACK => Int2Bytes(0, BE, SIGN) : STACK HEAP - requires notBool #validIntId(BIGINT_IDX, HEAP) + requires notBool( BIGINT_IDX in_keys{{ HEAP }} ) syntax InternalInstr ::= #setBigIntFromBytesStack ( idx: Int , Signedness ) | #setBigInt ( idx: Int , value: Bytes , Signedness ) @@ -61,19 +63,17 @@ module BIGINT-HELPERS BS : _ rule #setBigInt(BIGINT_IDX, BS, SIGN) => . ... - HEAP => HEAP [BIGINT_IDX <- Bytes2Int(BS, BE, SIGN)] + HEAP => HEAP {{ BIGINT_IDX <- Bytes2Int(BS, BE, SIGN) }} rule #setBigIntValue(BIGINT_IDX, VALUE) => . ... - HEAP => HEAP [BIGINT_IDX <- VALUE] - - syntax Bool ::= #validIntId( Int , Map ) [function, total] - // ------------------------------------------------------------- - rule #validIntId( IDX , HEAP ) => IDX in_keys(HEAP) andBool isInt(HEAP[IDX] orDefault 0) + HEAP => HEAP {{ BIGINT_IDX <- VALUE }} syntax Int ::= #newKey(Map) [function, total] | #newKeyAux(Int, Map) [function, total] | #newKey(MapIntToBytes) [function, total] | #newKeyAux(Int, MapIntToBytes) [function, total] + | #newKey(MapIntToInt) [function, total] + | #newKeyAux(Int, MapIntToInt) [function, total] // ------------------------------------------------------- rule #newKey(M:Map) => #newKeyAux(size(M), M) rule #newKeyAux(I, M:Map) => I requires notBool(I in_keys(M)) @@ -83,6 +83,10 @@ module BIGINT-HELPERS rule #newKeyAux(I, M:MapIntToBytes) => I requires notBool(I in_keys{{M}}) rule #newKeyAux(I, M:MapIntToBytes) => #newKeyAux(I +Int 1, M) requires I in_keys{{M}} + rule #newKey(M:MapIntToInt) => #newKeyAux(size(M), M) + rule #newKeyAux(I, M:MapIntToInt) => I requires notBool(I in_keys{{M}}) + rule #newKeyAux(I, M:MapIntToInt) => #newKeyAux(I +Int 1, M) requires I in_keys{{M}} + // sqrtInt(X) = ⌊√X⌋ if X is non-negative // sqrtInt(X) = -1 if X is negative syntax Int ::= sqrtInt(Int) [function, total] @@ -126,11 +130,12 @@ module BIGINTOPS ... 0 |-> INITIAL - HEAP => HEAP[#newKey(HEAP) <- #signed(i64, INITIAL)] + HEAP => HEAP {{ #newKey(HEAP) <- #signed(i64, INITIAL) }} requires definedSigned(i64, INITIAL) [preserves-definedness] // Preserving definedness: // - #newKey is total + // - MapIntToInt{{Int <- Int}} is total // - we check that #signed(i64, INITIAL) is defined. // extern int32_t bigIntUnsignedByteLength(void* context, int32_t reference); @@ -158,7 +163,7 @@ module BIGINTOPS ... 0 |-> IDX - ... IDX |-> V ... + ... wrap(IDX) Int2Int|-> wrap(V) ... requires V <=Int maxSInt64 andBool minSInt64 <=Int V @@ -167,7 +172,7 @@ module BIGINTOPS => #throwException(ExecutionFailed, "big int cannot be represented as int64") ... 0 |-> IDX - ... IDX |-> V ... + ... wrap(IDX) Int2Int|-> wrap(V) ... requires V >Int maxSInt64 orBool minSInt64 >Int V @@ -179,7 +184,7 @@ module BIGINTOPS 0 |-> IDX HEAP - requires notBool #validIntId(IDX, HEAP) + requires notBool( IDX in_keys{{HEAP}}) // extern int32_t bigIntGetUnsignedBytes(void* context, int32_t reference, int32_t byteOffset); rule hostCall("env", "bigIntGetUnsignedBytes", [ i32 i32 .ValTypes ] -> [ i32 .ValTypes ]) @@ -234,14 +239,17 @@ module BIGINTOPS // extern void bigIntAdd(void* context, int32_t destination, int32_t op1, int32_t op2); rule hostCall("env", "bigIntAdd", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]) => . ... 0 |-> DST 1 |-> OP1_IDX 2 |-> OP2_IDX - HEAP => HEAP [DST <- {HEAP[OP1_IDX]}:>Int +Int {HEAP[OP2_IDX]}:>Int] - requires #validIntId(OP1_IDX, HEAP) - andBool #validIntId(OP2_IDX, HEAP) + HEAP + => HEAP {{ DST <- (HEAP{{OP1_IDX}} orDefault 0) +Int (HEAP{{OP2_IDX}} orDefault 0) }} + + requires OP1_IDX in_keys{{HEAP}} + andBool OP2_IDX in_keys{{HEAP}} [preserves-definedness] // Preserving definedness: - // - {HEAP[OP*_IDX]}:>Int is defined because #validIntId(OP*_IDX, HEAP) // - +Int is total - // - Map[Kitem <- KItem] is total + // - in_keys is total + // - _{{_ <- _}} is total + // - _{{_}} orDefault _ is total // TODO a lot of code duplication in the error cases. // use sth like #getBigInt that checks existence @@ -250,92 +258,99 @@ module BIGINTOPS 0 |-> _DST 1 |-> OP1_IDX 2 |-> OP2_IDX HEAP - requires notBool (#validIntId(OP1_IDX, HEAP)) - orBool notBool (#validIntId(OP2_IDX, HEAP)) + requires notBool (OP1_IDX in_keys{{HEAP}}) + orBool notBool (OP2_IDX in_keys{{HEAP}}) // extern void bigIntSub(void* context, int32_t destination, int32_t op1, int32_t op2); rule hostCall("env", "bigIntSub", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]) => . ... 0 |-> DST 1 |-> OP1_IDX 2 |-> OP2_IDX - HEAP => HEAP [DST <- {HEAP[OP1_IDX]}:>Int -Int {HEAP[OP2_IDX]}:>Int] - requires #validIntId(OP1_IDX, HEAP) - andBool #validIntId(OP2_IDX, HEAP) + HEAP + => HEAP {{ DST <- (HEAP{{OP1_IDX}} orDefault 0) -Int (HEAP{{OP2_IDX}} orDefault 0) }} + + requires OP1_IDX in_keys{{HEAP}} + andBool OP2_IDX in_keys{{HEAP}} [preserves-definedness] // Preserving definedness: - // - {HEAP[OP*_IDX]}:>Int is defined because #validIntId(OP*_IDX, HEAP) // - -Int is total - // - Map[Kitem <- KItem] is total + // - in_keys is total + // - _{{_ <- _}} is total + // - _{{_}} orDefault _ is total rule hostCall("env", "bigIntSub", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]) => #throwException(ExecutionFailed, "no bigInt under the given handle") ... 0 |-> _DST 1 |-> OP1_IDX 2 |-> OP2_IDX HEAP - requires notBool (#validIntId(OP1_IDX, HEAP)) - orBool notBool (#validIntId(OP2_IDX, HEAP)) + requires notBool (OP1_IDX in_keys{{HEAP}}) + orBool notBool (OP2_IDX in_keys{{HEAP}}) // extern void bigIntMul(void* context, int32_t destination, int32_t op1, int32_t op2); rule hostCall("env", "bigIntMul", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]) => . ... 0 |-> DST 1 |-> OP1_IDX 2 |-> OP2_IDX - HEAP => HEAP [DST <- {HEAP[OP1_IDX]}:>Int *Int {HEAP[OP2_IDX]}:>Int] - requires #validIntId(OP1_IDX, HEAP) - andBool #validIntId(OP2_IDX, HEAP) + HEAP + => HEAP {{ DST <- (HEAP{{OP1_IDX}} orDefault 0) *Int (HEAP{{OP2_IDX}} orDefault 0) }} + + requires OP1_IDX in_keys{{HEAP}} + andBool OP2_IDX in_keys{{HEAP}} [preserves-definedness] // Preserving definedness: - // - {HEAP[OP*_IDX]}:>Int is defined because #validIntId(OP*_IDX, HEAP) // - *Int is total - // - Map[Kitem <- KItem] is total + // - in_keys is total + // - _{{_ <- _}} is total + // - _{{_}} orDefault _ is total rule hostCall("env", "bigIntMul", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]) => #throwException(ExecutionFailed, "no bigInt under the given handle") ... 0 |-> _DST 1 |-> OP1_IDX 2 |-> OP2_IDX HEAP - requires notBool (#validIntId(OP1_IDX, HEAP)) - orBool notBool (#validIntId(OP2_IDX, HEAP)) + requires notBool (OP1_IDX in_keys{{HEAP}}) + orBool notBool (OP2_IDX in_keys{{HEAP}}) // extern void bigIntTDiv(void* context, int32_t destination, int32_t op1, int32_t op2); rule hostCall("env", "bigIntTDiv", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]) => . ... 0 |-> DST 1 |-> OP1_IDX 2 |-> OP2_IDX - HEAP => HEAP [DST <- {HEAP[OP1_IDX]}:>Int /Int {HEAP[OP2_IDX]}:>Int] - requires #validIntId(OP1_IDX, HEAP) - andBool #validIntId(OP2_IDX, HEAP) - andBool {HEAP[OP2_IDX]}:>Int =/=Int 0 + HEAP + => HEAP {{ DST <- (HEAP{{OP1_IDX}} orDefault 0) /Int (HEAP{{OP2_IDX}} orDefault 0) }} + + requires OP1_IDX in_keys{{HEAP}} + andBool OP2_IDX in_keys{{HEAP}} + andBool HEAP{{OP1_IDX}} orDefault 0 =/=Int 0 [preserves-definedness] // Preserving definedness: - // - {HEAP[OP*_IDX]}:>Int is defined because #validIntId(OP*_IDX, HEAP) // - we checked that /Int is defined - // - Map[Kitem <- KItem] is total + // - _{{_ <- _}} is total + // - _{{_}} orDefault _ is total rule hostCall("env", "bigIntTDiv", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]) => #throwException(ExecutionFailed, "no bigInt under the given handle") ... 0 |-> _DST 1 |-> OP1_IDX 2 |-> OP2_IDX HEAP - requires notBool (#validIntId(OP1_IDX, HEAP)) - orBool notBool (#validIntId(OP2_IDX, HEAP)) + requires notBool (OP1_IDX in_keys{{HEAP}}) + orBool notBool (OP2_IDX in_keys{{HEAP}}) rule hostCall("env", "bigIntTDiv", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ]) => #throwException(ExecutionFailed, "bigInt division by 0") ... 0 |-> _DST 1 |-> OP1_IDX 2 |-> OP2_IDX HEAP - requires #validIntId(OP1_IDX, HEAP) - andBool #validIntId(OP2_IDX, HEAP) - andBool {HEAP[OP2_IDX]}:>Int ==Int 0 + requires OP1_IDX in_keys{{HEAP}} + andBool OP2_IDX in_keys{{HEAP}} + andBool HEAP{{OP1_IDX}} orDefault 0 ==Int 0 // extern int32_t bigIntSign(void* context, int32_t op); rule hostCall("env", "bigIntSign", [ i32 .ValTypes ] -> [ i32 .ValTypes ]) - => i32.const #bigIntSign({HEAP[IDX]}:>Int) + => i32.const #bigIntSign(V) ... 0 |-> IDX - HEAP - requires #validIntId(IDX, HEAP) + ... wrap(IDX) Int2Int|-> wrap(V) [preserves-definedness] // Preserving definedness: - // - {HEAP[IDX]}:>Int is defined because #validIntId(IDX, HEAP) // - #bigIntSign is total - // - Map[Kitem <- KItem] is total + // - in_keys is total + // - _{{_ <- _}} is total rule hostCall("env", "bigIntSign", [ i32 .ValTypes ] -> [ i32 .ValTypes ]) => #throwException(ExecutionFailed, "no bigInt under the given handle") @@ -343,31 +358,32 @@ module BIGINTOPS 0 |-> IDX HEAP - requires notBool #validIntId(IDX, HEAP) + requires notBool (IDX in_keys{{HEAP}}) // extern int32_t bigIntCmp(void* context, int32_t op1, int32_t op2); rule hostCall("env", "bigIntCmp", [ i32 i32 .ValTypes ] -> [ i32 .ValTypes ]) - => i32.const #cmpInt({HEAP[IDX1]}:>Int, {HEAP[IDX2]}:>Int) + => i32.const #cmpInt(HEAP {{OP1_IDX}} orDefault 0, HEAP {{OP2_IDX}} orDefault 0) ... - 0 |-> IDX1 1 |-> IDX2 + 0 |-> OP1_IDX 1 |-> OP2_IDX HEAP - requires #validIntId(IDX1, HEAP) - andBool #validIntId(IDX2, HEAP) + requires OP1_IDX in_keys{{HEAP}} + andBool OP2_IDX in_keys{{HEAP}} [preserves-definedness] // Preserving definedness: - // - {HEAP[IDX*]}:>Int is defined because #validIntId(IDX*, HEAP) // - #cmpInt is total - // - Map[Kitem <- KItem] is total + // - in_keys is total + // - _{{_ <- _}} is total + // - _{{_}} orDefault _ is total rule hostCall("env", "bigIntCmp", [ i32 i32 .ValTypes ] -> [ i32 .ValTypes ]) => #throwException(ExecutionFailed, "no bigInt under the given handle") ... - 0 |-> IDX1 1 |-> IDX2 + 0 |-> OP1_IDX 1 |-> OP2_IDX HEAP - requires notBool #validIntId(IDX1, HEAP) - orBool notBool #validIntId(IDX2, HEAP) + requires notBool (OP1_IDX in_keys{{HEAP}}) + orBool notBool (OP2_IDX in_keys{{HEAP}}) // extern void bigIntFinishUnsigned(void* context, int32_t reference); rule hostCall("env", "bigIntFinishUnsigned", [ i32 .ValTypes ] -> [ .ValTypes ]) @@ -417,13 +433,14 @@ module BIGINTOPS rule hostCall("env", "bigIntGetUnsignedArgument", [ i32 i32 .ValTypes ] -> [ .ValTypes ]) => . ... 0 |-> ARG_IDX 1 |-> BIG_IDX ARGS - HEAP => HEAP [BIG_IDX <- Bytes2Int(ARGS {{ ARG_IDX }}, BE, Unsigned)] + HEAP => HEAP {{ BIG_IDX <- Bytes2Int(ARGS {{ ARG_IDX }}, BE, Unsigned) }} requires #validArgIdx(ARG_IDX, ARGS) [preserves-definedness] // Preserving definedness: // - ARGS {{ ARG_IDX }} is defined because #validArgIdx(ARG_IDX, ARGS) + // - #cmpInt is total // - Bytes2Int is total - // - Map[Kitem <- KItem] is total + // - _{{_ <- _}} is total // If ARG_IDX is invalid (out of bounds) just ignore // https://github.com/multiversx/mx-chain-vm-go/blob/ea3d78d34c35f7ef9c1a9ea4fce8288608763229/vmhost/vmhooks/bigIntOps.go#L68 @@ -436,13 +453,13 @@ module BIGINTOPS rule hostCall("env", "bigIntGetSignedArgument", [ i32 i32 .ValTypes ] -> [ .ValTypes ]) => . ... 0 |-> ARG_IDX 1 |-> BIG_IDX ARGS - HEAP => HEAP [BIG_IDX <- Bytes2Int(ARGS {{ ARG_IDX }}, BE, Signed)] + HEAP => HEAP {{ BIG_IDX <- Bytes2Int(ARGS {{ ARG_IDX }}, BE, Signed) }} requires #validArgIdx(ARG_IDX, ARGS) [preserves-definedness] // Preserving definedness: // - ARGS {{ ARG_IDX }} is defined because #validArgIdx(ARG_IDX, ARGS) // - Bytes2Int is total - // - Map[Kitem <- KItem] is total + // - _{{_ <- _}} is total rule hostCall("env", "bigIntGetSignedArgument", [ i32 i32 .ValTypes ] -> [ .ValTypes ]) => . ... 0 |-> ARG_IDX 1 |-> _BIG_IDX @@ -452,7 +469,7 @@ module BIGINTOPS // extern void bigIntGetCallValue(void *context, int32_t destination); rule hostCall("env", "bigIntGetCallValue", [ i32 .ValTypes ] -> [ .ValTypes ]) => . ... 0 |-> IDX - HEAP => HEAP[IDX <- VALUE] + HEAP => HEAP {{ IDX <- VALUE }} VALUE // extern void bigIntGetExternalBalance(void *context, int32_t addressOffset, int32_t result); @@ -521,7 +538,7 @@ module BIGINTOPS 0 |-> IDX HEAP - requires notBool (#validIntId(IDX, HEAP)) + requires notBool (IDX in_keys{{ HEAP }}) rule [bigIntIsInt64]: hostCall ( "env" , "bigIntIsInt64" , [ i32 .ValTypes ] -> [ i32 .ValTypes ] ) @@ -529,7 +546,7 @@ module BIGINTOPS ... 0 |-> IDX - ... IDX |-> V ... + ... wrap(IDX) Int2Int|-> wrap(V) ... // extern void bigIntSqrt(void* context, int32_t destinationHandle, int32_t opHandle); rule [bigIntSqrt-invalid-handle]: @@ -538,7 +555,7 @@ module BIGINTOPS 0 |-> _DEST 1 |-> IDX HEAP - requires notBool #validIntId(IDX, HEAP) + requires notBool (IDX in_keys{{ HEAP }}) rule [bigIntSqrt-neg]: hostCall ( "env" , "bigIntSqrt" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] ) @@ -546,7 +563,7 @@ module BIGINTOPS ... 0 |-> _DEST 1 |-> IDX - ... IDX |-> V ... + ... wrap(IDX) Int2Int|-> wrap(V) ... requires V 0 |-> DEST 1 |-> IDX - ... IDX |-> V ... + ... wrap(IDX) Int2Int|-> wrap(V) ... requires 0 <=Int V // extern void bigIntAbs(void* context, int32_t destinationHandle, int32_t opHandle); @@ -565,7 +582,7 @@ module BIGINTOPS 0 |-> _DEST 1 |-> IDX HEAP - requires notBool (#validIntId(IDX, HEAP)) + requires notBool (IDX in_keys{{ HEAP }}) rule [bigIntAbs]: hostCall ( "env" , "bigIntAbs" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] ) @@ -573,7 +590,7 @@ module BIGINTOPS ... 0 |-> DEST 1 |-> IDX - ... IDX |-> V ... + ... wrap(IDX) Int2Int|-> wrap(V) ... // extern void bigIntNeg(void* context, int32_t destinationHandle, int32_t opHandle); @@ -583,7 +600,7 @@ module BIGINTOPS 0 |-> _DEST 1 |-> IDX HEAP - requires notBool (#validIntId(IDX, HEAP)) + requires notBool (IDX in_keys{{ HEAP }}) rule [bigIntNeg]: hostCall ( "env" , "bigIntNeg" , [ i32 i32 .ValTypes ] -> [ .ValTypes ] ) @@ -591,7 +608,7 @@ module BIGINTOPS ... 0 |-> DEST 1 |-> IDX - ... IDX |-> V ... + ... wrap(IDX) Int2Int|-> wrap(V) ... endmodule