diff --git a/deps/kmir_release b/deps/kmir_release index fc9d7b3..5e5d9c3 100644 --- a/deps/kmir_release +++ b/deps/kmir_release @@ -1 +1 @@ -0.4.185 +0.4.186 diff --git a/package/version b/package/version index c34958a..e8e277f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.15 +0.1.16 diff --git a/pyproject.toml b/pyproject.toml index 3ce1dac..c2d6e9d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,11 +4,11 @@ build-backend = "hatchling.build" [project] name = "kompass" -version = "0.1.15" +version = "0.1.16" description = "K Semantics for the Solana ecosystem" requires-python = "~=3.10" dependencies = [ - "kmir@git+https://github.com/runtimeverification/mir-semantics.git@v0.4.185#subdirectory=kmir", + "kmir@git+https://github.com/runtimeverification/mir-semantics.git@v0.4.186#subdirectory=kmir", ] [[project.authors]] @@ -16,7 +16,7 @@ name = "Runtime Verification, Inc." email = "contact@runtimeverification.com" [tool.uv.sources] -kmir = { git = "https://github.com/runtimeverification/mir-semantics.git", rev = "v0.4.185", subdirectory = "kmir" } +kmir = { git = "https://github.com/runtimeverification/mir-semantics.git", rev = "v0.4.186", subdirectory = "kmir" } [project.scripts] kompass = "kompass.__main__:main" diff --git a/src/kompass/__main__.py b/src/kompass/__main__.py index 9314a0e..ba32e72 100644 --- a/src/kompass/__main__.py +++ b/src/kompass/__main__.py @@ -8,7 +8,9 @@ from kmir.__main__ import _arg_parser as kmir_arg_parser from kmir.__main__ import _parse_args as kmir_parse_args from kmir.cargo import CargoProject -from kmir.options import KMirOpts, ProveRSOpts, PruneOpts, RunOpts +from kmir.options import KMirOpts +from kmir.options import ProveOpts as KMirProveOpts +from kmir.options import PruneOpts, RunOpts from kmir.options import ShowOpts as KMirShowOpts from kmir.options import ViewOpts as KMirViewOpts from kmir.smir import SMIRInfo @@ -44,9 +46,9 @@ def _kompass_run(opts: RunOpts) -> None: print(kompass.kore_to_pretty(result)) -def _kompass_prove_rs(opts: ProveRSOpts) -> None: +def _kompass_prove(opts: KMirProveOpts) -> None: kompass = Kompass(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report) - proof = kompass.prove_rs(opts) + proof = kompass.prove_program(opts) print(str(proof.summary)) if not proof.passed: sys.exit(1) @@ -106,7 +108,7 @@ def _run_prove(opts: ProveOpts) -> bool: kompass = Kompass(HASKELL_DEF_DIR, LLVM_LIB_DIR, bug_report=opts.bug_report) - prove_rs_opts = ProveRSOpts( + prove_opts = KMirProveOpts( rs_file=smir, proof_dir=opts.proof_dir if opts.proof_dir is not None else target_dir / 'proofs', haskell_target='kompass.haskell', @@ -119,7 +121,7 @@ def _run_prove(opts: ProveOpts) -> bool: smir=True, start_symbol=opts.start_symbol, ) - proof = kompass.prove_rs(prove_rs_opts) + proof = kompass.prove_program(prove_opts) print(str(proof.summary)) return proof.passed @@ -205,8 +207,8 @@ def kompass(args: Sequence[str]) -> None: _kompass_show(opts) case PruneOpts(): _kompass_prune(opts) - case ProveRSOpts(): - _kompass_prove_rs(opts) + case KMirProveOpts(): + _kompass_prove(opts) case _: raise AssertionError diff --git a/src/kompass/kdist/kompass/spl-token.md b/src/kompass/kdist/kompass/spl-token.md index a2243ea..e3b78e3 100644 --- a/src/kompass/kdist/kompass/spl-token.md +++ b/src/kompass/kdist/kompass/spl-token.md @@ -205,7 +205,7 @@ module KMIR-SPL-TOKEN => dynamicSize(17) [priority(30)] - // Multisig data buffer length (Multisig::LEN = 355) + // Multisig data buffer length (runtime-verification Multisig::LEN = 99) rule #maybeDynamicSize( dynamicSize(_), SPLDataBuffer( @@ -213,15 +213,13 @@ module KMIR-SPL-TOKEN ListItem(Integer(_, 8, false)) // m ListItem(Integer(_, 8, false)) // n ListItem(BoolVal(_)) // is_initialized - ListItem(Range( // signers: [Pubkey; 11] - ListItem(_) ListItem(_) ListItem(_) ListItem(_) ListItem(_) - ListItem(_) ListItem(_) ListItem(_) ListItem(_) ListItem(_) - ListItem(_) + ListItem(Range( // signers: [Pubkey; 3] + ListItem(_) ListItem(_) ListItem(_) )) ) ) ) - => dynamicSize(355) + => dynamicSize(99) [priority(30)] ``` @@ -446,25 +444,17 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami ListItem(Integer(?SplMultisigM:Int, 8, false)) // m: u8 ListItem(Integer(?SplMultisigN:Int, 8, false)) // n: u8 ListItem(BoolVal(?_SplMultisigInitialised:Bool)) // is_initialized: bool - ListItem(Range( // signers: [Pubkey; 11] + ListItem(Range( // signers: [Pubkey; 3] ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner0:List)))) ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner1:List)))) ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner2:List)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner3:List)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner4:List)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner5:List)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner6:List)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner7:List)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner8:List)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner9:List)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner10:List)))) )) ) ) ) ~> #forceSetPlaceValue( place(LOCAL, appendP(PROJS, REFCELL_PROJS)), // navigate to RefCell for borrow init - #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, REFCELL_PROJS))), 355) + #initBorrow(operandCopy(place(LOCAL, appendP(PROJS, REFCELL_PROJS))), 99) ) ~> #continueAt(TARGET) @@ -475,14 +465,6 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami andBool #isSplPubkey(?SplSigner0) andBool #isSplPubkey(?SplSigner1) andBool #isSplPubkey(?SplSigner2) - andBool #isSplPubkey(?SplSigner3) - andBool #isSplPubkey(?SplSigner4) - andBool #isSplPubkey(?SplSigner5) - andBool #isSplPubkey(?SplSigner6) - andBool #isSplPubkey(?SplSigner7) - andBool #isSplPubkey(?SplSigner8) - andBool #isSplPubkey(?SplSigner9) - andBool #isSplPubkey(?SplSigner10) [priority(30), preserves-definedness] ``` diff --git a/src/tests/integration/data/token/spl-token/spl-multisig-signer-index.rs b/src/tests/integration/data/token/spl-token/spl-multisig-signer-index.rs index 01c23f0..d56fa0d 100644 --- a/src/tests/integration/data/token/spl-token/spl-multisig-signer-index.rs +++ b/src/tests/integration/data/token/spl-token/spl-multisig-signer-index.rs @@ -45,7 +45,7 @@ enum ProgramError { InvalidAccountData, } -const MAX_SIGNERS: usize = 11; +const MAX_SIGNERS: usize = 3; #[derive(Clone, Debug)] struct Multisig { @@ -56,7 +56,7 @@ struct Multisig { } impl Multisig { - const LEN: usize = 355; + const LEN: usize = 99; fn unpack_from_slice(data: &[u8]) -> Result { if data.len() < Self::LEN { diff --git a/src/tests/integration/test_token.py b/src/tests/integration/test_token.py index 6cd270b..7b77dcc 100644 --- a/src/tests/integration/test_token.py +++ b/src/tests/integration/test_token.py @@ -4,7 +4,8 @@ import pytest from kmir.kmir import KMIR, KMIRAPRNodePrinter -from kmir.options import ProveRSOpts, ShowOpts +from kmir.options import ProveOpts as KMirProveOpts +from kmir.options import ShowOpts from kmir.testing.fixtures import assert_or_update_show_output from pyk.cterm.show import CTermShow from pyk.kast.pretty import PrettyPrinter @@ -46,13 +47,13 @@ def test_token_prove_rs(rs_file: Path, kmir: KMIR, update_expected_output: bool) start_symbols = START_SYMBOLS.get(rs_file.stem, ['main']) for start_symbol in start_symbols: - prove_rs_opts = ProveRSOpts( + prove_opts = KMirProveOpts( rs_file, start_symbol=start_symbol, haskell_target='kompass.haskell', llvm_lib_target='kompass.llvm-library', ) - apr_proof = KMIR.prove_rs(prove_rs_opts) + apr_proof = KMIR.prove_program(prove_opts) if should_show: printer = PrettyPrinter(kmir.definition) diff --git a/uv.lock b/uv.lock index 099c64b..48699fb 100644 --- a/uv.lock +++ b/uv.lock @@ -562,8 +562,8 @@ wheels = [ [[package]] name = "kmir" -version = "0.4.185" -source = { git = "https://github.com/runtimeverification/mir-semantics.git?subdirectory=kmir&rev=v0.4.185#612177d09eff707066c594d4939da3567a2d4b2a" } +version = "0.4.186" +source = { git = "https://github.com/runtimeverification/mir-semantics.git?subdirectory=kmir&rev=v0.4.186#fae1058f0887db88daf25dca834f75efd222ca70" } dependencies = [ { name = "kframework" }, { name = "rust-demangler" }, @@ -571,7 +571,7 @@ dependencies = [ [[package]] name = "kompass" -version = "0.1.15" +version = "0.1.16" source = { editable = "." } dependencies = [ { name = "kmir" }, @@ -597,7 +597,7 @@ dev = [ ] [package.metadata] -requires-dist = [{ name = "kmir", git = "https://github.com/runtimeverification/mir-semantics.git?subdirectory=kmir&rev=v0.4.185" }] +requires-dist = [{ name = "kmir", git = "https://github.com/runtimeverification/mir-semantics.git?subdirectory=kmir&rev=v0.4.186" }] [package.metadata.requires-dev] dev = [