Update dependency: deps/kmir_release

deps/kmir_release

@@ -1 +1 @@
-0.4.185
+0.4.186

package/version

@@ -1 +1 @@
-0.1.15
+0.1.16

pyproject.toml

@@ -4,19 +4,19 @@ 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]]
 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"

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
 

src/kompass/kdist/kompass/spl-token.md

@@ -205,23 +205,21 @@ 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(
            Aggregate(variantIdx(0),
              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)
     </k>
@@ -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]
 ```
 

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<Self, ProgramError> {
         if data.len() < Self::LEN {

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)