diff --git a/package/version b/package/version index 920c3bd5..61671068 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.57 +0.1.58 diff --git a/pyproject.toml b/pyproject.toml index 2d515d22..b56ee96f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.57" +version = "0.1.58" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 3b86ada0..ae3c0ce4 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -10,7 +10,7 @@ from hypothesis import strategies from pyk.cterm import CTerm, cterm_build_claim -from pyk.kast.inner import KSort, KVariable +from pyk.kast.inner import KSequence, KSort, KVariable from pyk.kast.manip import Subst, split_config_from from pyk.kast.outer import KClaim from pyk.konvert import kast_to_kore, kore_to_kast @@ -284,11 +284,12 @@ def make_steps(*args: KInner) -> KInner: lhs_subst['ALWAYSALLOCATE_CELL'] = token(always_allocate) lhs = CTerm(Subst(lhs_subst).apply(conf), [mlEqualsTrue(c) for c in ctrs]) - rhs_subst = subst.copy() - rhs_subst['PROGRAM_CELL'] = STEPS_TERMINATOR - rhs_subst['EXITCODE_CELL'] = token(0) - del rhs_subst['LOGGING_CELL'] - del rhs_subst['ALWAYSALLOCATE_CELL'] + # Expect the root contract call to terminate successfully while allowing changes to the blockchain state + rhs_subst = { + 'PROGRAM_CELL': STEPS_TERMINATOR, + 'EXITCODE_CELL': token(0), + 'K_CELL': KSequence(), + } rhs = CTerm(Subst(rhs_subst).apply(conf)) claim, _ = cterm_build_claim(name, lhs, rhs) diff --git a/src/komet/kdist/soroban-semantics/auto-allocate.md b/src/komet/kdist/soroban-semantics/auto-allocate.md index df6f126e..2f668aca 100644 --- a/src/komet/kdist/soroban-semantics/auto-allocate.md +++ b/src/komet/kdist/soroban-semantics/auto-allocate.md @@ -18,10 +18,19 @@ module WASM-AUTO-ALLOCATE syntax Stmt ::= "newEmptyModule" WasmString // ------------------------------------------- - rule newEmptyModule MODNAME => .K ... + + rule [newEmptyModule-trap]: + newEmptyModule _MODNAME => trap ... + NEXT + NEXT ... + [priority(10)] + + rule [newEmptyModule]: + newEmptyModule MODNAME => .K ... MR => MR [ MODNAME <- NEXT ] NEXT => NEXT +Int 1 ( .Bag => NEXT ... ) ... + [preserves-definedness] syntax Stmts ::= autoAllocModules ( ModuleDecl, Map ) [function] | #autoAllocModules ( Defns , Map ) [function] diff --git a/src/komet/kdist/soroban-semantics/configuration.md b/src/komet/kdist/soroban-semantics/configuration.md index 9c64337c..40c27a31 100644 --- a/src/komet/kdist/soroban-semantics/configuration.md +++ b/src/komet/kdist/soroban-semantics/configuration.md @@ -242,7 +242,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly STACK => toSmall(SCV) : STACK ALWAYS_ALLOCATE requires alwaysSmall(SCV) - orBool ( toSmallValid(SCV) andBool notBool ALWAYS_ALLOCATE ) + orBool ( isSmall(SCV) andBool notBool ALWAYS_ALLOCATE ) // recursively allocate vector items rule [allocObject-vec]: diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md index 01c2f486..65335116 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/src/komet/kdist/soroban-semantics/data.md @@ -102,40 +102,44 @@ module HOST-OBJECT imports HOST-OBJECT-SYNTAX imports WASM + syntax Int ::= unwrap(HostVal) [function, total, symbol(HostVal:unwrap)] + // --------------------------------------------------- + rule unwrap(HostVal(I)) => I + syntax Int ::= getMajor(HostVal) [function, total, symbol(getMajor)] | getMinor(HostVal) [function, total, symbol(getMinor)] | getTag(HostVal) [function, total, symbol(getTag)] | getBody(HostVal) [function, total, symbol(getBody)] // ----------------------------------------------------------------------- - rule getMajor(HostVal(I)) => I >>Int 32 - rule getMinor(HostVal(I)) => (I &Int (#pow(i32) -Int 1)) >>Int 8 - rule getTag(HostVal(I)) => I &Int 255 - rule getBody(HostVal(I)) => I >>Int 8 + rule getMajor(HostVal(I)) => I >>Int 32 [concrete] + rule getMinor(HostVal(I)) => (I &Int (#pow(i32) -Int 1)) >>Int 8 [concrete] + rule getTag(HostVal(I)) => I &Int 255 [concrete] + rule getBody(HostVal(I)) => I >>Int 8 [concrete] syntax Bool ::= isObject(HostVal) [function, total, symbol(isObject)] | isObjectTag(Int) [function, total, symbol(isObjectTag)] | isRelativeObjectHandle(HostVal) [function, total, symbol(isRelativeObjectHandle)] // -------------------------------------------------------------------------------- rule isObject(V) => isObjectTag(getTag(V)) - rule isObjectTag(TAG) => 64 <=Int TAG andBool TAG <=Int 77 + rule isObjectTag(TAG) => 64 <=Int TAG andBool TAG <=Int 77 [concrete] rule isRelativeObjectHandle(V) => getMajor(V) &Int 1 ==Int 0 syntax Int ::= indexToHandle(Int, Bool) [function, total, symbol(indexToHandle)] // -------------------------------------------------------------------------------- - rule indexToHandle(I, false) => (I < I < (I < I < getMajor(V) >>Int 1 + rule getIndex(V) => getMajor(V) >>Int 1 [concrete] syntax HostVal ::= fromHandleAndTag(Int, Int) [function, total, symbol(fromHandleAndTag)] | fromMajorMinorAndTag(Int, Int, Int) [function, total, symbol(fromMajorMinorAndTag)] | fromBodyAndTag(Int, Int) [function, total, symbol(fromBodyAndTag)] // -------------------------------------------------------------------------------- rule fromHandleAndTag(H, T) => fromMajorMinorAndTag(H, 0, T) - rule fromMajorMinorAndTag(MAJ, MIN, TAG) => fromBodyAndTag((MAJ < HostVal((BODY < fromBodyAndTag((MAJ < HostVal((BODY < 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(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 - rule getTag(Symbol(BS)) => 14 requires lengthString(BS) <=Int 9 - rule getTag(Symbol(BS)) => 74 requires lengthString(BS) >Int 9 - rule getTag(ScBytes(_)) => 72 + 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(_) #as X) => 6 requires isSmall(X) + rule getTag(U64(_) #as X) => 64 requires notBool isSmall(X) + rule getTag(I64(_) #as X) => 7 requires isSmall(X) + rule getTag(I64(_) #as X) => 65 requires notBool isSmall(X) + rule getTag(U128(_) #as X) => 10 requires isSmall(X) + rule getTag(U128(_) #as X) => 68 requires notBool isSmall(X) + rule getTag(I128(_) #as X) => 11 requires isSmall(X) + rule getTag(I128(_) #as X) => 69 requires notBool isSmall(X) + rule getTag(ScVec(_)) => 75 + rule getTag(ScMap(_)) => 76 + rule getTag(ScAddress(_)) => 77 + rule getTag(Symbol(_) #as X) => 14 requires isSmall(X) + rule getTag(Symbol(_) #as X) => 74 requires notBool isSmall(X) + rule getTag(ScBytes(_)) => 72 syntax Int ::= getTagWithFlag(alwaysAllocate: Bool, ScVal) [function, total] // ------------------------------------------------------------------------------- @@ -173,7 +177,7 @@ module HOST-OBJECT rule getTagWithFlag(true, I128(_)) => 69 rule getTagWithFlag(true, Symbol(_)) => 74 rule getTagWithFlag(_, SCV) => getTag(SCV) [owise] - + // 64-bit integers that fit in 56 bits syntax Int ::= "#maxU64small" [macro] | "#maxI64small" [macro] @@ -273,28 +277,38 @@ module HOST-OBJECT syntax HostVal ::= toSmall(ScVal) [function, total, symbol(toSmall)] // --------------------------------------------------------------------------------- - rule toSmall(SCBool(false)) => fromMajorMinorAndTag(0, 0, 0) - rule toSmall(SCBool(true)) => fromMajorMinorAndTag(0, 0, 1) - rule toSmall(Void) => fromMajorMinorAndTag(0, 0, 2) - rule toSmall(Error(TYP, I)) => fromMajorMinorAndTag(I, ErrorType2Int(TYP), 3) - rule toSmall(U32(I)) => fromMajorMinorAndTag(I, 0, 4) - rule toSmall(I32(I)) => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5) + rule toSmall(SCBool(false)) => fromMajorMinorAndTag(0, 0, 0) + rule toSmall(SCBool(true)) => fromMajorMinorAndTag(0, 0, 1) + rule toSmall(Void) => fromMajorMinorAndTag(0, 0, 2) + rule toSmall(Error(TYP, I)) => fromMajorMinorAndTag(I, ErrorType2Int(TYP), 3) + rule toSmall(U32(I)) => fromMajorMinorAndTag(I, 0, 4) + 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] - - syntax Bool ::= toSmallValid(ScVal) - [function, total, symbol(toSmallValid)] - // --------------------------------------------------------------------------------- - rule toSmallValid(VAL) => toSmall(VAL) =/=K HostVal(-1) + rule toSmall(U64(I) #as X) => fromBodyAndTag(I, 6) requires isSmall(X) + rule toSmall(I64(I) #as X) => fromBodyAndTag(#unsigned(i56, I), 7) requires isSmall(X) + rule toSmall(U128(I) #as X) => fromBodyAndTag(I, 10) requires isSmall(X) + rule toSmall(I128(I) #as X) => fromBodyAndTag(#unsigned(i56, I), 11) requires isSmall(X) + rule toSmall(Symbol(S) #as X) => fromBodyAndTag(encode6bit(S), 14) requires isSmall(X) + rule toSmall(_) => HostVal(-1) [owise] + + syntax Bool ::= isSmall(ScVal) [function, total, symbol(isSmall)] + // ----------------------------------------------------------------------- + rule isSmall(SCBool(_)) => true + rule isSmall(Void) => true + rule isSmall(Error(_, _)) => true + rule isSmall(U32(_)) => true + rule isSmall(I32(_)) => true + rule isSmall(U64(I)) => isSmallInt(Unsigned, I) + rule isSmall(I64(I)) => isSmallInt(Signed, I) + rule isSmall(U128(I)) => isSmallInt(Unsigned, I) + rule isSmall(I128(I)) => isSmallInt(Signed, I) + rule isSmall(Symbol(S)) => lengthString(S) <=Int 9 + rule isSmall(_) => false [owise] + + syntax Bool ::= isSmallInt(Signedness, Int) [function, total, symbol(isSmallInt)] + // ------------------------------------------------------------------------ + rule isSmallInt(Unsigned, I) => 0 <=Int I andBool I 0 -Int #pow1(i56) <=Int I andBool I returnHostVal => i64.const I ... - HostVal(I) : S => S + returnHostVal => HV ... + HV:HostVal : S => S rule [hostfun-obj-to-u64]: hostCall ( "i" , "0" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) diff --git a/src/komet/kdist/soroban-semantics/komet-lemmas.md b/src/komet/kdist/soroban-semantics/komet-lemmas.md index c2b93787..d429cfd0 100644 --- a/src/komet/kdist/soroban-semantics/komet-lemmas.md +++ b/src/komet/kdist/soroban-semantics/komet-lemmas.md @@ -7,9 +7,10 @@ module KSOROBAN-LEMMAS [symbolic] imports INT-BITWISE-LEMMAS imports HOST-OBJECT-LEMMAS imports SOROBAN + imports MAP-SYMBOLIC syntax InternalCmd ::= runLemma(ProofStep) | doneLemma(ProofStep) - syntax ProofStep ::= HostVal | ScVal | Int | Bool + syntax ProofStep ::= HostVal | ScVal | Int | Bool | Val rule runLemma(S) => doneLemma(S) ... @@ -26,35 +27,48 @@ module INT-BITWISE-LEMMAS [symbolic] rule (A &Int B) &Int C => A &Int (B &Int C) [simplification, concrete(B, C)] rule A &Int (B &Int C) => (A &Int B) &Int C [simplification, symbolic(A, B)] - syntax Bool ::= isPowerOf2(Int) [function, total] + syntax Bool ::= isPowerOf2(Int) [function, total, symbol(isPowerOf2)] rule isPowerOf2(I:Int) => I ==Int 1 < false requires I <=Int 0 - syntax Bool ::= isFullMask(Int) [function, total] + syntax Bool ::= isFullMask(Int) [function, total, symbol(isFullMask)] rule isFullMask(I:Int) => I ==Int fullMask(log2Int(I) +Int 1) requires 0 false requires I <=Int 0 - syntax Int ::= fullMask(Int) [function, total] + syntax Int ::= fullMask(Int) [function, total, symbol(fullMask)] rule fullMask(I:Int) => (1 < 0 requires I <=Int 0 rule [modInt-to-bit-mask]: - I modInt M => I &Int (M -Int 1) requires isPowerOf2(M) - [simplification, concrete(M)] + I modInt M => I &Int (M -Int 1) requires isPowerOf2(M) andBool 0 <=Int I + [simplification, concrete(M), preserves-definedness] endmodule -module HOST-OBJECT-LEMMAS [symbolic] +module HOST-OBJECT-LEMMA-HELPERS [symbolic] imports HOST-OBJECT imports INT-BITWISE-LEMMAS + syntax Bool ::= isTag(Int) [function, total, symbol(isTag)] + | isPayload(Int) [function, total, symbol(isPayload)] +//----------------------------------------------------------------- + rule isTag(TAG) => 0 <=Int TAG andBool TAG <=Int 255 + // A payload is a 64-bit unsigned integer + rule isPayload(P) => 0 <=Int P andBool P T &Int MASK requires isFullMask(MASK) andBool SHIFT >=Int log2Int(MASK +Int 1) [simplification, concrete(SHIFT, MASK)] - // #getRange(_,_,8)'s result always fits in 64-bit - rule #getRange(SB, ADDR, 8) &Int 18446744073709551615 => #getRange(SB, ADDR, 8) + rule [64bit-fullmask-of-payload]: + X &Int 18446744073709551615 => X + requires isPayload(X) [simplification] @@ -66,5 +80,75 @@ module HOST-OBJECT-LEMMAS [symbolic] andBool WIDTH' <=Int WIDTH [simplification] + rule [shrs-to-getBody]: + i64 . shr_s unwrap(HV:HostVal) 8 => getBody(HV) + [simplification] + + rule [shift-to-getBody]: + unwrap(HV) >>Int 8 => getBody(HV) + [simplification] + + rule [defined-unsigned-is-non-negative]: + 0 <=Int #unsigned(T, I) => true + requires definedUnsigned(T, I) + [simplification, preserves-definedness] + + rule [and-255-of-unwrap]: + unwrap(HV:HostVal) &Int 255 => getTag(HV) [simplification] + + rule [getTag-of-fromMajorMinorAndTag]: + getTag(fromMajorMinorAndTag(MAJ, MIN, TAG)) => TAG + requires 0 <=Int MAJ + andBool 0 <=Int MIN + andBool isTag(TAG) + [simplification] + + rule [getBody-of-fromBodyAndTag]: + getBody(fromBodyAndTag(BODY, TAG)) => BODY + requires 0 <=Int BODY + andBool isTag(TAG) + [simplification] + + rule [getTag-of-fromBodyAndTag]: + getTag(fromBodyAndTag(BODY, TAG)) => TAG + requires 0 <=Int BODY + andBool isTag(TAG) + [simplification] + + rule [unwrap-is-payload]: + isPayload(unwrap(_:HostVal)) => true + [simplification] + + rule [unwrap-is-non-negative]: + 0 <=Int unwrap(_:HostVal) => true + [simplification] + + // #getRange(_,_,8)'s result always fits in 64-bit + rule [getRange-8-is-payload]: + isPayload(#getRange(_, _, 8)) => true + [simplification] + + + rule [getBody-of-unwrapped-small-i64]: + #signed( + i64, + unwrap( + fromBodyAndTag( #unsigned ( i56 , I:Int ) , 7 ) + ) + ) >>Int 8 + => I + requires isSmallInt(Signed, I) + [simplification] + + rule [shift-of-nonneg-is-nonneg]: + 0 <=Int I < true + requires 0 <=Int I andBool 0 <=Int S + [simplification] + + rule [or-of-nonnegs-is-nonneg]: + 0 <=Int X |Int Y => true + requires 0 <=Int X andBool 0 <=Int Y + [simplification] + endmodule ``` diff --git a/src/komet/kdist/soroban-semantics/soroban.md b/src/komet/kdist/soroban-semantics/soroban.md index 731252fb..f56dfbc2 100644 --- a/src/komet/kdist/soroban-semantics/soroban.md +++ b/src/komet/kdist/soroban-semantics/soroban.md @@ -160,7 +160,7 @@ module SOROBAN andBool (notBool isRelativeObjectHandle(VAL)) rule [push-HostVal]: - HostVal(I) => i64.const I ... + HV:HostVal => i64.const unwrap(HV) ... ``` diff --git a/src/tests/lemmas/specs/int-bitwise-spec.k b/src/tests/lemmas/specs/int-bitwise-spec.k index 90ac2486..266ae794 100644 --- a/src/tests/lemmas/specs/int-bitwise-spec.k +++ b/src/tests/lemmas/specs/int-bitwise-spec.k @@ -9,4 +9,12 @@ module INT-BITWISE-SPEC ( (I < + 4 + requires 0 <=Int I + endmodule diff --git a/src/tests/lemmas/specs/test-spec.k b/src/tests/lemmas/specs/test-spec.k index 5e32c44c..ae9efb25 100644 --- a/src/tests/lemmas/specs/test-spec.k +++ b/src/tests/lemmas/specs/test-spec.k @@ -1,12 +1,59 @@ module TEST-SPEC imports KASMER + + // Tested lemmas: + // - and-255-of-unwrap + claim [test-bitwise-gettag-of-u32]: + unwrap(toSmall(U32(I))) &Int 255 => 4 + requires 0 <=Int I + // Tested lemmas: - // - bitwise-mk-hostval-then-mask - claim [test-bitwise-mk-hostval-then-mask]: - ( (I < - 4 + // - getTag-of-fromMajorMinorAndTag + claim [test-getTag-of-u32]: + getTag(toSmall(U32(I))) => 4 requires 0 <=Int I + // Tested lemmas: + // - getTag-of-fromBodyAndTag + // - defined-unsigned-is-non-negative + claim [getTag-of-small-i64]: + .Steps + .K + + runLemma( getTag(toSmall(I64(I))) ) + => + doneLemma( 7 ) + + requires isSmallInt(Signed, I) + + + // Tested lemmas: + // - modInt-to-bit-mask-64 + // - unwrap-fits-in-64-bits + claim [modInt-of-unwrap-unsigned]: + .Steps + .K + + runLemma( unwrap ( fromBodyAndTag ( #unsigned ( i56 , I ) , 7 )) modInt 18446744073709551616 ) + => + doneLemma( unwrap ( fromBodyAndTag ( #unsigned ( i56 , I ) , 7 )) ) + + requires isSmallInt(Signed, I) + + // Tested lemmas: + // - modInt-to-bit-mask-64 + // - unwrap-fits-in-64-bits + // - shrs-to-getBody + // - getBody-of-fromBodyAndTag + claim [shrs-of-unwrap-unsigned]: + .Steps + .K + + runLemma( i64 . shr_s unwrap ( fromBodyAndTag ( #unsigned ( i56 , I ) , 7 )) modInt 18446744073709551616 8 ) + => + doneLemma( #unsigned ( i64 , I ) ) + + requires isSmallInt(Signed, I) + endmodule