Skip to content

Lemmas and symbolic execution improvements #67

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
bbyalcinkaya wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

Lemmas and symbolic execution improvements #67

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
a17f289
add `preserves-definedness` to `newEmptyModule`
bbyalcinkaya Feb 12, 2025
05425ef
allow blockchain state changes in post-execution check
bbyalcinkaya Jul 21, 2026
5fd2143
make bitwise rules concrete
bbyalcinkaya Jul 21, 2026
98de848
refactor `toSmallValid`/`getTag`
bbyalcinkaya Jul 21, 2026
fee3acf
add lemmas
bbyalcinkaya Aug 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions src/komet/kasmer.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
11 changes: 10 additions & 1 deletion src/komet/kdist/soroban-semantics/auto-allocate.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,19 @@ module WASM-AUTO-ALLOCATE

syntax Stmt ::= "newEmptyModule" WasmString
// -------------------------------------------
rule <instrs> newEmptyModule MODNAME => .K ... </instrs>

rule [newEmptyModule-trap]:
<instrs> newEmptyModule _MODNAME => trap ... </instrs>
<nextModuleIdx> NEXT </nextModuleIdx>
<moduleInst> <modIdx> NEXT </modIdx> ... </moduleInst>
[priority(10)]

rule [newEmptyModule]:
<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>
[preserves-definedness]

syntax Stmts ::= autoAllocModules ( ModuleDecl, Map ) [function]
| #autoAllocModules ( Defns , Map ) [function]
Expand Down
2 changes: 1 addition & 1 deletion src/komet/kdist/soroban-semantics/configuration.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
<hostStack> STACK => toSmall(SCV) : STACK </hostStack>
<alwaysAllocate> ALWAYS_ALLOCATE </alwaysAllocate>
requires alwaysSmall(SCV)
orBool ( toSmallValid(SCV) andBool notBool ALWAYS_ALLOCATE )
orBool ( isSmall(SCV) andBool notBool ALWAYS_ALLOCATE )

// recursively allocate vector items
rule [allocObject-vec]:
Expand Down
106 changes: 60 additions & 46 deletions src/komet/kdist/soroban-semantics/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,69 +104,73 @@ 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 <<Int 1) |Int 1
rule indexToHandle(I, true) => I <<Int 1
rule indexToHandle(I, false) => (I <<Int 1) |Int 1 [concrete]
rule indexToHandle(I, true) => I <<Int 1 [concrete]

syntax Int ::= getIndex(HostVal) [function, total, symbol(getIndex)]
// ----------------------------------------------------------------------------
rule getIndex(V) => 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 <<Int 24) |Int MIN, TAG)
rule fromBodyAndTag(BODY, TAG) => HostVal((BODY <<Int 8) |Int TAG)
rule fromMajorMinorAndTag(MAJ, MIN, TAG) => fromBodyAndTag((MAJ <<Int 24) |Int MIN, TAG) [concrete]
rule fromBodyAndTag(BODY, TAG) => HostVal((BODY <<Int 8) |Int TAG) [concrete]

syntax WasmStringToken ::= #unparseWasmString ( String ) [function, total, hook(STRING.string2token)]
| #quoteUnparseWasmString ( String ) [function, total]
rule #quoteUnparseWasmString(S) => #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
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(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

Expand Down Expand Up @@ -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 <Int #pow(i56)
rule isSmallInt(Signed, I) => 0 -Int #pow1(i56) <=Int I andBool I <Int #pow1(i56)

syntax Bool ::= alwaysSmall(ScVal)
[function, total, symbol(alwaysSmall)]
Expand Down
4 changes: 2 additions & 2 deletions src/komet/kdist/soroban-semantics/host/integer.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ module HOST-INTEGER
[preserves-definedness] // definedness of '#unsigned(,)' is checked

rule [returnHostVal]:
<instrs> returnHostVal => i64.const I ... </instrs>
<hostStack> HostVal(I) : S => S </hostStack>
<instrs> returnHostVal => HV ... </instrs>
<hostStack> HV:HostVal : S => S </hostStack>

rule [hostfun-obj-to-u64]:
<instrs> hostCall ( "i" , "0" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
Expand Down
Loading
Loading