26.11.25 Release

26.11.25 Release

2fa67951d2cfc4bb92805e5e22057f33b5203efd

Author: yoav-el-certora

Public/TestEVM/Builtin/SafeCasting/Default.conf

@@ -4,4 +4,5 @@
     ],
     verify: "C:C.spec",
     "solc": "solc8.28",
+    "safe_casting_builtin": true
 }

Public/TestEVM/Builtin/SafeCasting/expectedDefault.json

@@ -3,6 +3,7 @@
 		"safeCasting": {
 			"FAIL": [
 				"complex(int8,int8)",
+				"narrow(int64)",
 				"noWidth(uint256)"
 			],
 			"SUCCESS": [

Public/TestSolana/CpisTest/Default.conf

@@ -1,6 +1,6 @@
 {
     "build_script": "./certora_build.sh",
-    "java_args": ["-Dlevel.cpi=info"],
+    "java_args": ["-Dlevel.sbf.cpi=info"],
     "rule": [
         "rule_transfer_token_transfers_same_wallet_0",
         "rule_transfer_token_transfers_same_wallet_1",

Public/TestSolana/CpisTest/src/processor.rs

@@ -5,9 +5,9 @@ use solana_program::{
     program_error::ProgramError,
     pubkey::Pubkey,
 };
-
 use spl_token::instruction::{burn, close_account, mint_to, transfer};
 
+
 const SEED1: &[u8] = b"seed1";
 const SEED2: &[u8] = b"seed2";
 const SEED3: &[u8] = b"seed3";
@@ -29,6 +29,7 @@ pub fn process_transfer_token<const N_SIGNERS: usize>(
     Ok(())
 }
 
+#[cvlr::early_panic]
 fn invoke_transfer_token<'a, const N_SIGNERS: usize>(
     token_program: &AccountInfo<'a>,
     from: &AccountInfo<'a>,
@@ -87,6 +88,7 @@ pub fn process_mint_token<const N_SIGNERS: usize>(
     Ok(())
 }
 
+#[cvlr::early_panic]
 fn invoke_mint_token<'a, const N_SIGNERS: usize>(
     token_program: &AccountInfo<'a>,
     mint: &AccountInfo<'a>,
@@ -146,6 +148,7 @@ pub fn process_burn_token<const N_SIGNERS: usize>(
     Ok(())
 }
 
+#[cvlr::early_panic]
 fn invoke_burn_token<'a, const N_SIGNERS: usize>(
     token_program: &AccountInfo<'a>,
     source: &AccountInfo<'a>,
@@ -198,6 +201,7 @@ pub fn process_close_account<const N_SIGNERS: usize>(
     Ok(())
 }
 
+#[cvlr::early_panic]
 fn invoke_close_account<'a, const N_SIGNERS: usize>(
     token_program: &AccountInfo<'a>,
     account: &AccountInfo<'a>,
@@ -241,6 +245,7 @@ pub fn process_unknown_program(
     Ok(())
 }
 
+#[cvlr::early_panic]
 fn invoke_unknown_program<'a>(
     acc1: &AccountInfo<'a>,
     acc2: &AccountInfo<'a>,

lib/Shared/src/main/kotlin/config/Config.kt

@@ -2267,6 +2267,15 @@ object Config {
         )
     ) {}
 
+    val extraSolanaPatterns = object : ConfigType.BooleanCmdLine(
+        true,
+        Option(
+            "extraSolanaPatterns",
+            true,
+            "Apply some extra solana rewrite pattern [default=true]"
+        )
+    ) {}
+
     val globalInliner = object : ConfigType.IntCmdLine(
         default = 1,
         option = Option(
@@ -2487,6 +2496,15 @@ object Config {
         )
     ) {}
 
+    val SafeCastingBuiltin: ConfigType.BooleanCmdLine = object : ConfigType.BooleanCmdLine(
+        false,
+        Option(
+            "safeCastingBuiltin", true,
+            "Used to signal that the python side instrumented the safeCasting builtin rule [default: false]"
+        ),
+        pythonName = "--safe_casting_builtin"
+    ) {}
+
     val CallTraceHardFail = object : ConfigType.HardFailCmdLine(
         HardFailMode.OFF,
         Option(

lib/Shared/src/main/kotlin/log/Logger.kt

@@ -129,8 +129,18 @@ enum class LoggerTypes : LoggerName {
     CALLTRACE_STORAGE,
     REPORT_UTILS,
     SBF,
-    SBF_SCALAR_ANALYSIS,
     SBF_BACKWARD_SCALAR_ANALYSIS,
+    SBF_CPI,
+    SBF_MEMORY_ANALYSIS,
+    SBF_PTA_UNIFY,
+    SBF_PTA_UNIFY2,
+    SBF_PTA_COLLAPSES,
+    SBF_PTA_CELL_RECONSTRUCT,
+    SBF_PTA_JOIN,
+    SBF_PTA_LEQ,
+    SBF_PTA_MEM_TRANSFER,
+    SBF_SCALAR_ANALYSIS,
+    SBF_SCALAR_WITH_PREDS_ANALYSIS,
     WASM,
     WASM_ANALYSIS,
     CVLR,
@@ -140,7 +150,6 @@ enum class LoggerTypes : LoggerName {
     TWOSTAGE,
     FOUNDRY,
     DEBUG_SYMBOLS,
-    CPI,
     EQUIVALENCE,
     OVERFLOW_PATTERN_REWRITER,
     BOUNDED_MODEL_CHECKER,

scripts/CertoraProver/certoraBuild.py

@@ -3339,14 +3339,14 @@ def instrument_auto_finders(self, build_arg_contract_file: str, i: int,
         else:
             added_source_finders = {}
 
-        try:
-            casting_instrumentations, casting_types = generate_casting_instrumentation(self.asts, build_arg_contract_file, sdc_pre_finder)
-        except Exception as e:
-            instrumentation_logger.warning(
-                f"Computing casting instrumentation failed for {build_arg_contract_file}: {e}", exc_info=True)
-            casting_instrumentations, casting_types = {}, {}
-
-        instr = CertoraBuildGenerator.merge_dicts_instrumentation(instr, casting_instrumentations)
+        if self.context.safe_casting_builtin:
+            try:
+                casting_instrumentations, casting_types = generate_casting_instrumentation(self.asts, build_arg_contract_file, sdc_pre_finder)
+            except Exception as e:
+                instrumentation_logger.warning(
+                    f"Computing casting instrumentation failed for {build_arg_contract_file}: {e}", exc_info=True)
+                casting_instrumentations, casting_types = {}, {}
+            instr = CertoraBuildGenerator.merge_dicts_instrumentation(instr, casting_instrumentations)
 
         abs_build_arg_contract_file = Util.abs_posix_path(build_arg_contract_file)
         if abs_build_arg_contract_file not in instr:
@@ -3401,12 +3401,13 @@ def instrument_auto_finders(self, build_arg_contract_file: str, i: int,
                         read_so_far += amt + 1 + to_skip
                     output.write(in_file.read(-1))
 
-                    library_name, funcs = casting_types.get(contract_file, ("", list()))
-                    if len(funcs) > 0:
-                        output.write(bytes(f"\nlibrary {library_name}" + "{\n", "utf8"))
-                        for f in funcs:
-                            output.write(bytes(f, "utf8"))
-                        output.write(bytes("}\n", "utf8"))
+                    if self.context.safe_casting_builtin:
+                        library_name, funcs = casting_types.get(contract_file, ("", list()))
+                        if len(funcs) > 0:
+                            output.write(bytes(f"\nlibrary {library_name}" + "{\n", "utf8"))
+                            for f in funcs:
+                                output.write(bytes(f, "utf8"))
+                            output.write(bytes("}\n", "utf8"))
 
         new_file = self.to_autofinder_file(build_arg_contract_file)
         self.context.file_to_contract[new_file] = self.context.file_to_contract[

scripts/CertoraProver/certoraContextAttributes.py

@@ -1202,6 +1202,19 @@ class EvmAttributes(AttrUtil.Attributes):
         disables_build_cache=False,
     )
 
+    SAFE_CASTING_BUILTIN = AttrUtil.AttributeDefinition(
+        arg_type=AttrUtil.AttrArgType.BOOLEAN,
+        help_msg="This needs to be set to true for the safeCasting builtin to work",
+        default_desc="This needs to be set to true for the safeCasting builtin to work",
+        jar_flag='-safeCastingBuiltin',
+        argparse_args={
+            'action': AttrUtil.STORE_TRUE,
+            'default': False
+        },
+        affects_build_cache_key=True,
+        disables_build_cache=False,
+    )
+
     @classmethod
     def hide_attributes(cls) -> List[str]:
         # do not show these attributes in the help message

scripts/CertoraProver/certoraContextValidator.py

@@ -238,7 +238,8 @@ def __default_path() -> Path:
         check_rule(context)
 
         if context.split_rules and (context.build_only or context.compilation_steps_only):
-            raise Util.CertoraUserInputError("cannot use 'compilation_steps_only' or 'build_only' with 'split_rules'")
+            validation_logger.warning("When running with 'compilation_steps_only' or 'build_only', "
+                                      "'split_rules' attribute has no effect and will be ignored.")
 
         if context.compilation_steps_only and context.build_only:
             raise Util.CertoraUserInputError("cannot use both 'compilation_steps_only' and 'build_only'")

scripts/certoraRun.py

@@ -74,7 +74,7 @@ def run_certora(args: List[str], app: Type[App.CertoraApp] = App.EvmApp,
     # Collect and dump configuration layout
     collect_and_dump_config_layout(context)
 
-    if context.split_rules:
+    if context.split_rules and not (context.build_only or context.compilation_steps_only):
         context.build_only = True
         build(context)
         context.build_only = False