diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index acbe5f1..f9eb5f6 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.kast.prelude.ml import mlEqualsTrue @@ -307,10 +307,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['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 5a24c63..812e118 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 d9b66db..cd1b3f6 100644 --- a/src/komet/kdist/soroban-semantics/configuration.md +++ b/src/komet/kdist/soroban-semantics/configuration.md @@ -256,7 +256,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 7bde93e..bf09856 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/src/komet/kdist/soroban-semantics/data.md @@ -104,47 +104,51 @@ 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 < #unparseWasmString("\"" +String S +String "\"") - // https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#tag-values - syntax Int ::= getTag(ScVal) [function, total] +// https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#tag-values + syntax Int ::= getTag(ScVal) [function, total, symbol(getTagScVal)] // ----------------------------------------------------- rule getTag(SCBool(false)) => 0 rule getTag(SCBool(true)) => 1 @@ -152,21 +156,21 @@ module HOST-OBJECT 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(U256(I)) => 12 requires I <=Int #maxU64small - rule getTag(U256(I)) => 70 requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width + rule getTag(U64(_) #as I) => 6 requires isSmall(I) + rule getTag(U64(_) #as I) => 64 requires notBool(isSmall(I)) + rule getTag(I64(_) #as I) => 7 requires isSmall(I) + rule getTag(I64(_) #as I) => 65 requires notBool(isSmall(I)) + rule getTag(U128(_) #as I) => 10 requires isSmall(I) + rule getTag(U128(_) #as I) => 68 requires notBool(isSmall(I)) + rule getTag(I128(_) #as I) => 11 requires isSmall(I) + rule getTag(I128(_) #as I) => 69 requires notBool(isSmall(I)) + rule getTag(U256(_) #as I) => 12 requires isSmall(I) + rule getTag(U256(_) #as I) => 70 requires notBool(isSmall(I)) 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(Symbol(_) #as S) => 14 requires isSmall(S) + rule getTag(Symbol(_) #as S) => 74 requires notBool(isSmall(S)) rule getTag(ScBytes(_)) => 72 rule getTag(ScString(_)) => 73 @@ -299,29 +303,39 @@ 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(U256(I)) => fromBodyAndTag(I, 12) requires I <=Int #maxU64small - 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(U256(I) #as X) => fromBodyAndTag(I, 12) 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 c2b9378..f6b8fb4 100644 --- a/src/komet/kdist/soroban-semantics/komet-lemmas.md +++ b/src/komet/kdist/soroban-semantics/komet-lemmas.md @@ -4,8 +4,6 @@ requires "data.md" module KSOROBAN-LEMMAS [symbolic] imports KWASM-LEMMAS - imports INT-BITWISE-LEMMAS - imports HOST-OBJECT-LEMMAS imports SOROBAN syntax InternalCmd ::= runLemma(ProofStep) | doneLemma(ProofStep) @@ -13,18 +11,7 @@ module KSOROBAN-LEMMAS [symbolic] rule runLemma(S) => doneLemma(S) ... -endmodule - -module INT-BITWISE-LEMMAS [symbolic] - imports INT - imports BOOL - - rule C |Int S => S |Int C [simplification, concrete(C), symbolic(S)] - rule X |Int 0 => X [simplification] - - rule A &Int B => B &Int A [simplification, concrete(A), symbolic(B)] - 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)] + /// Int Helpers syntax Bool ::= isPowerOf2(Int) [function, total] rule isPowerOf2(I:Int) => I ==Int 1 < (1 < 0 requires I <=Int 0 + syntax Bool ::= isTag(Int) [function, total, symbol(isTag)] + | isHostValInt(Int) [function, total, symbol(isHostValInt)] +//-------------------------------------------------------------------------- + rule isTag(TAG) => 0 <=Int TAG andBool TAG <=Int 255 + rule isHostValInt(I) => 0 <=Int I andBool I <=Int maxInt(i64, Unsigned) [concrete] + + /// Bitwise Lemmas + + rule C |Int S => S |Int C [simplification, concrete(C), symbolic(S)] + rule X |Int 0 => X [simplification] + + rule A &Int B => B &Int A [simplification, concrete(A), symbolic(B)] + 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)] + rule [modInt-to-bit-mask]: I modInt M => I &Int (M -Int 1) requires isPowerOf2(M) [simplification, concrete(M)] -endmodule + rule X &Int MASK => X + requires isFullMask(MASK) + andBool 0 <=Int X + andBool X <=Int MASK + [simplification] + + /// Integer Lemmas + + // From Wasm Semantics + // rule #signed(ITYPE, N) => N requires 0 <=Int N andBool N N -Int #pow(ITYPE) requires #pow1(ITYPE) <=Int N andBool N N +Int #pow(ITYPE) requires N N requires 0 <=Int N + + // #unsigned(T, A) is always nonnegative once definedUnsigned(T, A) holds + // (A may exceed T's signed max -- definedUnsigned allows up to T's unsigned max). + // - definedUnsigned(T, A): -#pow1(T) <= A < #pow(T) + // - 0 <= A: + // 1) 0 <= A -- branch condition + // 2) #unsigned(T, A) == A -- #unsigned's definition when 0 <= A + // 3) 0 <= #unsigned(T, A) -- substitute 2) into 1) + // - A < 0: + // 1) -#pow1(T) <= A -- definedUnsigned(T,A) + // 2) -#pow1(T) +Int #pow(T) <= A +Int #pow(T) -- add #pow(T) to both sides of 1) + // 3) #pow1(T) <= A +Int #pow(T) -- #pow(T) == 2 *Int #pow1(T) + // 4) #pow1(T) <= #unsigned(T, A) -- A +Int #pow(T) == #unsigned(T, A) since A < 0 + // 5) 0 <= #pow1(T) <= #unsigned(T, A) -- #pow1(T) >= 0 + rule [unsigned-is-nonnegative]: + 0 <=Int #unsigned(T, A) => true + requires definedUnsigned(T, A) + [simplification] + + // #unsigned(T, A) always stays below #pow(T) once definedUnsigned(T, A) holds. + // - definedUnsigned(T, A): -#pow1(T) <= A < #pow(T) + // - 0 <= A: + // 1) A < #pow(T) -- definedUnsigned(T,A) + // 2) #unsigned(T, A) == A -- #unsigned's definition when 0 <= A + // 3) #unsigned(T, A) < #pow(T) -- substitute 2) into 1) + // - A < 0: + // 1) A < 0 -- branch condition + // 2) A +Int #pow(T) < 0 +Int #pow(T) -- add #pow(T) to both sides of 1) + // 3) A +Int #pow(T) < #pow(T) -- 0 +Int #pow(T) == #pow(T) + // 4) #unsigned(T, A) < #pow(T) -- A +Int #pow(T) == #unsigned(T, A) since A < 0 + rule [unsigned-upper-bound]: + #unsigned(T, A) true + requires POW_T ==Int #pow(T) + andBool definedUnsigned(T, A) + [simplification] + + // Round-trip identity: #unsigned packs a signed A into T's unsigned range, + // #signed unpacks it back out. Only recovers A when A was already in T's + // signed range (-#pow1(T) <= A < #pow1(T), tighter than definedUnsigned): + // - 0 <= A (so 0 <= A < #pow1(T) from the requires bounds): + // 1) 0 <= A < #pow1(T) -- requires bounds, this branch + // 2) #unsigned(T, A) == A -- #unsigned's definition when 0 <= A + // 3) 0 <= #unsigned(T, A) < #pow1(T) -- substitute 2) into 1) + // 4) #signed(T, #unsigned(T, A)) == #unsigned(T, A) -- #signed's definition when 0 <= N < #pow1(T), via 3) + // 5) #signed(T, #unsigned(T, A)) == A -- substitute 2) into 4) + // - A < 0 (so -#pow1(T) <= A < 0 from the requires bounds): + // 1) -#pow1(T) <= A < 0 -- requires bounds, this branch + // 2) #unsigned(T, A) == A +Int #pow(T) -- #unsigned's definition when A < 0 + // 3) -#pow1(T) +Int #pow(T) <= A +Int #pow(T) < 0 +Int #pow(T) -- add #pow(T) to all sides of 1) + // 4) #pow1(T) <= A +Int #pow(T) < #pow(T) -- #pow(T) == 2 *Int #pow1(T) + // 5) #pow1(T) <= #unsigned(T, A) < #pow(T) -- substitute 2) into 4) + // 6) #signed(T, #unsigned(T, A)) == #unsigned(T, A) -Int #pow(T) -- #signed's definition when #pow1(T) <= N < #pow(T), via 5) + // 7) #signed(T, #unsigned(T, A)) == A +Int #pow(T) -Int #pow(T) -- substitute 2) into 6) + // 8) #signed(T, #unsigned(T, A)) == A -- simplify 7) + rule [signed-of-unsigned]: + #signed( T , #unsigned( T , A ) ) => A + requires 0 -Int #pow1(T) <=Int A + andBool A T &Int MASK - requires isFullMask(MASK) andBool SHIFT >=Int log2Int(MASK +Int 1) - [simplification, concrete(SHIFT, MASK)] + /// HostVal Lemmas - // #getRange(_,_,8)'s result always fits in 64-bit - rule #getRange(SB, ADDR, 8) &Int 18446744073709551615 => #getRange(SB, ADDR, 8) + rule [getBody-of-fromBodyAndTag]: + getBody(fromBodyAndTag(BODY, _TAG)) => BODY [simplification] + rule [getTag-of-fromBodyAndTag]: + getTag(fromBodyAndTag(_BODY, TAG)) => TAG + [simplification] - rule #getRange(#setRange(_BM, ADDR, VAL, WIDTH), ADDR', WIDTH') => #wrap(WIDTH', VAL) - requires 0 <=Int ADDR - andBool 0 MAJ [simplification] + rule [getMinor-of-fromMajorMinorAndTag]: + getMinor(fromMajorMinorAndTag(_MAJ, MIN, _TAG)) => MIN + [simplification] + + rule [getTag-of-fromMajorMinorAndTag]: + getTag(fromMajorMinorAndTag(_MAJ, _MIN, TAG)) => TAG + [simplification] + + + rule [bitwise-to-getTag]: + unwrap( HV:HostVal ) &Int 255 => getTag( HV ) + [simplification] + + rule I &Int 18446744073709551615 => I + requires isHostValInt(I) + [simplification] + + rule isHostValInt( unwrap(_:HostVal) ) => true [simplification] + + rule [shrs-to-getBody]: + i64 . shr_s unwrap(HV:HostVal) 8 => #extends(i64, i56, getBody(HV)) + [simplification] + + rule [shrs-skip-tag]: + i64 . shr_s unwrap(HV:HostVal) W => #applyIBinOpToVal( + i64 , shr_s, + i64 . shr_s unwrap(HV) 8, + (W -Int 8) + ) + requires 8 T . OP #get(X1) #get(X2) + rule #applyIBinOpToVal(_, _, _, _) => undefined [owise] + endmodule ``` diff --git a/src/komet/kdist/soroban-semantics/soroban.md b/src/komet/kdist/soroban-semantics/soroban.md index 0bda5a4..644c8c5 100644 --- a/src/komet/kdist/soroban-semantics/soroban.md +++ b/src/komet/kdist/soroban-semantics/soroban.md @@ -181,7 +181,7 @@ semantics. andBool (notBool isRelativeObjectHandle(VAL)) rule [push-HostVal]: - HostVal(I) => i64.const I ... + HV:HostVal => i64.const unwrap(HV) ... ```