18.12.25 Release

18.12.25 Release

fcf493b367d992fa19a0aeaa1971a98f61e531d2

Author: yoav-el-certora

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

@@ -3005,6 +3005,24 @@ object Config {
                 }"
         }
 
+        val retryOnLeafTimeout: ConfigType.BooleanCmdLine = object : ConfigType.BooleanCmdLine(
+            false,
+            Option(
+                "smt_retryOnLeafTimeout",
+                true,
+                "Reruns a timeouting leaf with a broader portfolio of solvers."
+            )
+        ), TransformationAgnosticConfig {}
+
+        val retryOnLeafTimeoutSolvers: ConfigType.SolverProgramCmdLine = object : ConfigType.SolverProgramCmdLine(
+            AllCommonAvailableSolversWithClOptions.toTypedArray(),
+            Option(
+                "smt_retryOnLeafTimeoutSolvers",
+                true,
+                "Solvers used for a rerun on timeouting leafs."
+            )
+        ), TransformationAgnosticConfig {}
+
         val NumOfUnsatCores: ConfigType.IntCmdLine = object : ConfigType.IntCmdLine(
             1,
             Option(

lib/Shared/src/main/kotlin/spec/cvlast/CVLRuleAndMethodChoiceValidation.kt

@@ -109,9 +109,27 @@ fun validateSimpleMethodChoices(knownFunctions: Set<String>): VoidResult<CVLErro
  * them, as this is a probable user input mistake.
  */
 fun validateRuleChoices(cvlAst: CVLAst) : VoidResult<CVLError> {
-    val allRules = cvlAst.rules.map { it.declarationId }.toSet() + cvlAst.invs.map { it.id }.toSet() +
+    val allRules = cvlAst.rules.mapToSet { it.declarationId } + cvlAst.invs.mapToSet { it.id } +
         cvlAst.useDeclarations.builtInRulesInUse.map { it.id }
-    return validateRuleChoices(allRules)
+    val validationResult = validateRuleChoices(allRules)
+    if(!validationResult.isResult()){
+        return validationResult
+    }
+
+    val invariantsNotInMainSpecFile = cvlAst.invs.filterNot { it.needsVerification }.mapToSet { it.id  }
+    /**
+     * With [config.Config.getNonPatternRuleChoices] we only match against explicit includes of invariants,
+     * once that do not include the wildcard (*). I.e. if one selects an invariant via --rule my_invariant*, and the main
+     * spec file contains a my_invariant_foo and an imported spec file contains my_invariant_bar, no typechecking error will occur,
+     * but my_invariant_bar is excluded.
+      */
+    val invariantsChosenFromImportedSpecs =  invariantsNotInMainSpecFile.filter { it in Config.getNonPatternRuleChoices().orEmpty() }
+    return if(invariantsChosenFromImportedSpecs.isNotEmpty()) {
+        CVLError.General(Range.Empty(), "A rule filter is applied (${Config.getNonPatternRuleChoices()}) and matches an invariant from an imported spec that is not used in the main spec. " +
+            "To include the invariant in verification, try adding the following statement(s) to your main spec file: \n${invariantsChosenFromImportedSpecs.joinToString("\n") { "use invariant $it;" }}").asError()
+    } else {
+        ok
+    }
 }
 
 fun validateRuleChoices(allRules: Set<String>) : VoidResult<CVLError> {

scripts/CertoraProver/certoraApp.py

@@ -23,6 +23,8 @@
 
 class CertoraApp(ABC):
     attr_class: Type[AttrUtil.Attributes] = Attrs.EvmProverAttributes
+    ecosystem: str = "EVM"
+    product: str = "PROVER"
 
 class EvmAppClass(CertoraApp):
     pass
@@ -38,15 +40,21 @@ class MoveAppClass(CertoraApp):
 
 class SolanaApp(RustAppClass):
     attr_class = Attrs.SolanaProverAttributes
+    ecosystem: str = "SOLANA"
+
 
 class SorobanApp(RustAppClass):
     attr_class = Attrs.SorobanProverAttributes
+    ecosystem: str = "SOROBAN"
 
 class RangerApp(EvmAppClass):
     attr_class = Attrs.RangerAttributes
+    product = "RANGER"
 
 class ConcordApp(EvmAppClass):
     attr_class = Attrs.ConcordAttributes
+    product = "CONCORD"
 
 class SuiApp(MoveAppClass):
     attr_class = Attrs.SuiProverAttributes
+    ecosystem: str = "SUI"

scripts/CertoraProver/certoraCloudIO.py

@@ -69,18 +69,6 @@
 
 FEATURES_REPORT_FILE = Path("featuresReport.json")
 
-class EcoEnum(Util.NoValEnum):
-    EVM = Util.auto()
-    SOROBAN = Util.auto()
-    SOLANA = Util.auto()
-    SUI = Util.auto()
-
-class ProductEnum(Util.NoValEnum):
-    PROVER = Util.auto()
-    RANGER = Util.auto()
-    CONCORD = Util.auto()
-
-
 class TimeError(Exception):
     """A custom exception used to report on time elapsed errors"""
 
@@ -648,21 +636,8 @@ def paths_in_source_dir(attr_values: List[str]) -> str:
 
         auth_data["useLatestFe"] = self.context.fe_version == str(Util.FeValue.LATEST)
 
-        if Attrs.is_solana_app():
-            auth_data["ecosystem"] = EcoEnum.SOLANA.name
-        elif Attrs.is_soroban_app():
-            auth_data["ecosystem"] = EcoEnum.SOROBAN.name
-        elif Attrs.is_sui_app():
-            auth_data["ecosystem"] = EcoEnum.SUI.name
-        else:
-            auth_data["ecosystem"] = EcoEnum.EVM.name
-
-        if Attrs.is_ranger_app():
-            auth_data["product"] = ProductEnum.RANGER.name
-        elif Attrs.is_concord_app():
-            auth_data["product"] = ProductEnum.CONCORD.name
-        else:
-            auth_data["product"] = ProductEnum.PROVER.name
+        auth_data["ecosystem"] = self.context.app.ecosystem
+        auth_data["product"] = self.context.app.product
 
         if Attrs.is_evm_app() and self.context.cache is not None:
             auth_data["toolSceneCacheKey"] = self.context.cache

scripts/CertoraProver/certoraCollectRunMetadata.py

@@ -74,6 +74,7 @@ class RunMetaData:
     conf_path -- the relative path form the cwd_relative to the configuration file
     group_id -- optional identifier for grouping this run
     java_version -- version of Java used during the run, if available
+    ecosystem -- the ecosystem of the current run (EVM, SOLANA, SOROBAN, SUI, etc)
     default_solc_version -- version of default solc version on current machine, if available
     python_version -- version of Python running the process
     certora_ci_client -- name of the CI client if available, derived from environment
@@ -84,7 +85,7 @@ class RunMetaData:
     """
     def __init__(self, raw_args: List[str], conf: Dict[str, Any], origin: str, revision: str,
                  branch: str, cwd_relative: Path, dirty: bool, main_spec: Optional[str],
-                 conf_path: Optional[Path], group_id: Optional[str], java_version: str):
+                 conf_path: Optional[Path], group_id: Optional[str], java_version: str, ecosystem: str):
         self.raw_args = raw_args
         self.conf = conf
         self.origin = origin
@@ -97,6 +98,7 @@ def __init__(self, raw_args: List[str], conf: Dict[str, Any], origin: str, revis
         self.group_id = group_id
         self.python_version = ".".join(str(x) for x in sys.version_info[:3])
         self.java_version = java_version
+        self.ecosystem = ecosystem
         self.default_solc_version = get_solc_version(self.conf)
         self.certora_ci_client = Utils.get_certora_ci_name()
         self.timestamp = str(datetime.now(timezone.utc).timestamp())
@@ -119,6 +121,7 @@ def __repr__(self) -> str:
             f" group_id: {self.group_id}\n"
             f" python_version: {self.python_version}\n"
             f" java_version: {self.java_version}\n"
+            f" ecosystem: {self.ecosystem}\n"
             f" default_solc_version: {self.default_solc_version}\n"
             f" CertoraCI client: {self.certora_ci_client}\n"
             f" jar_flag_info: {self.jar_flag_info}\n"
@@ -198,7 +201,8 @@ def collect_run_metadata(wd: Path, raw_args: List[str], context: CertoraContext)
                            main_spec=None,
                            conf_path=None,
                            group_id=None,
-                           java_version=context.java_version)
+                           java_version=context.java_version,
+                           ecosystem=context.app.ecosystem)
 
     # collect information about current git snapshot
     cwd_abs = wd.absolute()
@@ -227,7 +231,8 @@ def collect_run_metadata(wd: Path, raw_args: List[str], context: CertoraContext)
                            main_spec=get_main_spec(context),
                            conf_path=conf_path,
                            group_id=context.group_id,
-                           java_version=context.java_version)
+                           java_version=context.java_version,
+                           ecosystem=context.app.ecosystem)
 
     try:
         sha_out = subprocess.run(['git', 'rev-parse', 'HEAD'], cwd=wd,
@@ -263,7 +268,8 @@ def collect_run_metadata(wd: Path, raw_args: List[str], context: CertoraContext)
                            main_spec=get_main_spec(context),
                            conf_path=conf_path,
                            group_id=context.group_id,
-                           java_version=context.java_version)
+                           java_version=context.java_version,
+                           ecosystem=context.app.ecosystem)
 
         metadata_logger.debug(f' collected data:\n{str(data)}')
 
@@ -282,7 +288,8 @@ def collect_run_metadata(wd: Path, raw_args: List[str], context: CertoraContext)
                            main_spec=get_main_spec(context),
                            conf_path=conf_path,
                            group_id=context.group_id,
-                           java_version=context.java_version)
+                           java_version=context.java_version,
+                           ecosystem=context.app.ecosystem)
 
 
 def get_solc_version(conf: Dict[str, Any]) -> Optional[str]:

src/main/kotlin/verifier/LExpVCStats.kt

@@ -164,7 +164,7 @@ data class ResplitStatistic(
 @Serializable
 data class SplitStatistic(
     /** The location of the split in the split tree.  -1 indicates a failed split */
-    val address: List<Int>,
+    val address: String,
     /** splitName exactly as it is in Split<CoreTACProgram>.name. Also referred to as vcName */
     val splitName: String,
     val finalResult: String? = null,

src/main/kotlin/verifier/TACVerifier.kt

@@ -50,6 +50,7 @@ import smtlibutils.statistics.LearnedClausesFilterStatistics
 import smtlibutils.statistics.PreExecutionStatistics
 import solver.ConfigStatistics
 import solver.SMTCounterexampleModel
+import solver.SolverChoice
 import solver.SolverResult
 import spec.cvlast.CVLCmd
 import spec.cvlast.CVLExpDeclaredSymbolsCollector
@@ -184,7 +185,7 @@ class TACVerifier private constructor(
     ) {
         updateSplitStatistics(
             SplitStatistic(
-                address = address.asIntList,
+                address = address.name(),
                 vcFeatures = listOf(),
                 solvingEvent = ResplitStatistic(resplitTime),
                 timeToSolveSinceJarStart = TimeSinceStart(),
@@ -209,7 +210,7 @@ class TACVerifier private constructor(
 
         val splitStats = SplitStatistic(
             splitName = vcName,
-            address = address.asIntList,
+            address = address.name(),
             finalResult = LExpVCStatsLogger.getResultStr(checkerResult.satResult),
             timeout = timeout,
             smtSolvingWallTime = smtSolvingWallTime,
@@ -623,7 +624,7 @@ class TACVerifier private constructor(
                 vcGenStopWatch = MilliTimeElapserStopWatch(timeStatsRecorder, vcGenTimeTag),
                 solverStopWatch,
                 autoConfig,
-                localSettings
+                ((subProblem as? SplitTree.NodeWithInfo<*>)?.info as? LocalSettings) ?: localSettings
             )
             val finalResult = verifierResult.finalResult
             subProblem.setRunInfo(finalResult, verifierResult.elapsedTimeSeconds.seconds, timeout)
@@ -671,6 +672,24 @@ class TACVerifier private constructor(
                         problemQueue += subProblem.split(subProblemTAC)
                     }
                     continue
+                } else if (Config.Smt.retryOnLeafTimeout.get() && (subProblem.address !is SplitAddress.Rerun)) {
+                    val sub = LazySubProgram(
+                        splitTree,
+                        SplitAddress.Rerun(subProblem.lazySub.address)
+                    )
+                    val alreadyTried = smtFormulaCheckerResult.subResultsFlattened
+                        .mapNotNull { it.solverInstanceInfo?.solverConfig }
+                    val settings = localSettings.copy(
+                        solverProgramChoice = SolverChoice(
+                            Config.Smt.retryOnLeafTimeoutSolvers.get()
+                                .filter { it.solverInfo.getOptionForRandomSeed(1).isNotEmpty() }
+                                .flatMap { listOf(1, 2, 3).map { seed -> it.copy(randomSeed = seed) } }
+                                .filter { it !in alreadyTried }
+                                .map { it.copy(canBeSkipped = { _,_ -> false }) }
+                        )
+                    )
+                    logger.info { "Timed out on leaf ${sub.name}, rerunning with random seeds" }
+                    problemQueue.add(splitTree.NodeWithInfo(sub, subProblem.sideScore, settings))
                 } else {
                     // we dump timeouting leaves.
                     smtFormulaCheckerResult.let { last ->

src/main/kotlin/verifier/autoconfig/AutoConfigManager.kt

@@ -75,11 +75,11 @@ class AutoConfigManager(val ruleName: String) : Closeable {
      * their parent is also UNSAT. The propagation is recursive.
      */
     private fun propagateUNSAT(address: SplitAddress): Unit = synchronized(splitStatAndSolverConfigLock) {
-        if (address.asIntList.toString() !in stats.splitStatistics) {
+        if (address.name() !in stats.splitStatistics) {
             warn("The split with the address $address should be first added to ${::stats.name} before we propagate its unsat result")
             return
         }
-        if (!stats.splitStatistics[address.asIntList.toString()]!!.isEventuallyUNSAT()) {
+        if (!stats.splitStatistics[address.name()]!!.isEventuallyUNSAT()) {
             warn("Trying to propagate an unregistered UNSAT result of the split $address")
             return
         }
@@ -90,10 +90,10 @@ class AutoConfigManager(val ruleName: String) : Closeable {
         if (address !is SplitAddress.Block) {
             return
         }
-        val siblingAddressStr = address.sibling().toString()
+        val siblingAddressStr = address.sibling().name()
         if (stats.splitStatistics[siblingAddressStr]?.isEventuallyUNSAT() == true) {
             val parentAddress = address.parent
-            val parentAddressStr = parentAddress.toString()
+            val parentAddressStr = parentAddress?.name() ?: "null"
             if (parentAddressStr !in stats.splitStatistics) {
                 warn("The parent address $parentAddressStr is not registered in ${::stats.name}")
                 return
@@ -110,12 +110,12 @@ class AutoConfigManager(val ruleName: String) : Closeable {
      * Sets the [finalResult] and [solvers] of the stats of [address] based on the stats of [matchingUnsat].
      */
     private fun markMatchingUnsat(address: SplitAddress, matchingUnsat: BasicSplitStatistics) = synchronized(splitStatAndSolverConfigLock) {
-        if(address.asIntList.toString() !in stats.splitStatistics) {
+        if(address.name() !in stats.splitStatistics) {
             warn("Trying to mark an address UNSAT that is not in ${::stats.name}: $address")
             return
         }
-        stats.splitStatistics[address.asIntList.toString()] =
-            stats.splitStatistics[address.asIntList.toString()]!!.copy(
+        stats.splitStatistics[address.name()] =
+            stats.splitStatistics[address.name()]!!.copy(
                 finalResult = matchingUnsat.finalResult,
                 solvers = matchingUnsat.solvers
             )
@@ -126,27 +126,29 @@ class AutoConfigManager(val ruleName: String) : Closeable {
      * it gets computed and stored in [stats].
      */
     private fun getDigest(address: SplitAddress, prog: CoreTACProgram): String = synchronized(splitStatAndSolverConfigLock) {
-        require(address.asIntList.toString() in stats.splitStatistics) {
-            "Trying to store a digest for a split ${address.asIntList} that is not registered yet"
+        val addressName = address.name()
+        require(addressName in stats.splitStatistics) {
+            "Trying to store a digest for a split ${addressName} that is not registered yet"
         }
-        if (stats.splitStatistics[address.asIntList.toString()]!!.tacStats.digest == null) {
+        if (stats.splitStatistics[addressName]!!.tacStats.digest == null) {
             val digest = BasicTACStatistics.computeDigest(prog)
-            stats.splitStatistics[address.asIntList.toString()] =
-                stats.splitStatistics[address.asIntList.toString()]!!.let {
+            stats.splitStatistics[addressName] =
+                stats.splitStatistics[addressName]!!.let {
                     it.copy(tacStats = it.tacStats.copy(digest = digest))
                 }
         }
-        return stats.splitStatistics[address.asIntList.toString()]!!.tacStats.digest!!
+        return stats.splitStatistics[addressName]!!.tacStats.digest!!
     }
 
     /**
      * Register the given [subProblem] in [stats] (storing just address, split name, and basic TAC statistics).
      */
     fun registerSplit(address: SplitAddress, name: String, subProblemTAC: CoreTACProgram) = synchronized(splitStatAndSolverConfigLock) {
-        if (address.asIntList.toString() !in stats.splitStatistics.keys) {
-            info("registering split ${address.asIntList}")
-            stats.splitStatistics[address.asIntList.toString()] = BasicSplitStatistics(
-                address = address.asIntList.toString(),
+        val addressName = address.name()
+        if (addressName !in stats.splitStatistics.keys) {
+            info("registering split ${address.name()}")
+            stats.splitStatistics[addressName] = BasicSplitStatistics(
+                address = addressName,
                 splitName = name,
                 tacStats = BasicTACStatistics.fromCoreTACProgram(subProblemTAC, Config.AutoconfigUseDigests.get()),
             )
@@ -164,7 +166,7 @@ class AutoConfigManager(val ruleName: String) : Closeable {
         timeoutForSubProblem: Duration,
         solvingDuration: Duration,
     ) = synchronized(splitStatAndSolverConfigLock) {
-        val address = splitAddress.asIntList.toString()
+        val address = splitAddress.name()
         info("registering ${verifierResult.finalResult} result for split $address.")
         if(address !in stats.splitStatistics) {
             warn("Trying to register results for an unregistered split $address.")
@@ -262,7 +264,7 @@ class AutoConfigManager(val ruleName: String) : Closeable {
         val loadedMatches = loadedStats?.splitStatistics?.values?.filter { tacStats.match(it.tacStats) } ?: listOf()
         //Splits we have already solved in this CVT run and which are matching the current split.
         val newMatches: List<BasicSplitStatistics> = if (learnFromCurrent) {
-            val splitAddressStr = splitAddress.asIntList.toString()
+            val splitAddressStr = splitAddress.name()
             synchronized(splitStatAndSolverConfigLock) {
                 stats.splitStatistics.values.filter { tacStats.match(it.tacStats) && it.address != splitAddressStr }
             }