Use one rule-selection type for conf scoping and run history by ericeil · Pull Request #259 · Certora/AutoProver

ericeil · 2026-10-02T19:34:25Z

Why there were two types

rules striping #177 (rule striping) added a TypedDict named RuleSelection (sort: "include" | "exclude", selector: list[str]) to composer/spec/source/prover.py. It recorded the rule subset a run covered, on ProverRunLog.rules, with None meaning every rule.
Add the Solana Prover preflight step #248 (Solana Prover preflight) included "prover: share conf infrastructure between CVL and Solana". That commit added a tagged union InheritRules | SelectRules | ExcludeRules to the new shared composer/prover/conf.py to scope a conf to a run's rules, and CVL and Solana confs both use it. It is the same idea as rules striping #177's TypedDict, and should have replaced it. Instead, a sloppy merge when Add the Solana Prover preflight step #248 landed kept both: rules striping #177's type was renamed to RuleSelectionRecord to avoid the name clash, and _scope_of was added to convert one into the other.

After that, the CVL prover code used both types. Run history and buffer jobs used RuleSelectionRecord. Conf building used RuleSelection. buffer_conf accepted either, through separate selection and rules parameters. submit_buffer parsed its arguments with its own _selection_of instead of the shared rule_selection, and keyed its job table on a string built by _selection_key.

What this changes

Removes RuleSelectionRecord, _selection_of, _scope_of and _selection_key. ProverRunLog.rules, _BufJob / _BufDone, _run_buffer_job and buffer_conf now all take a RuleSelection. A whole-buffer run records InheritRules() instead of None.
submit_buffer parses its arguments with rule_selection, and keys its job table on (buffer name, selection) directly.
SelectRules / ExcludeRules store names as a sorted tuple. Sorting keeps the duplicate-submit check ignoring name order, as _selection_key did. The tuple conversion is needed because ProverRunLog is saved in checkpoints, and restoring a checkpoint turns tuples into lists; without it, a restored selection doesn't compare equal to a fresh one and can't be hashed. A new test checks the round trip.
A new _checked_rules(selection, declared) in prover.py works out which declared rules a run under a selection checks. The stuck-rule tracking (_executed_rules) and submit_buffer's check for a selection that would run no rule both use it. It stays out of conf.py because it assumes InheritRules means every rule, which holds for the CVL pipeline's base confs, not for every conf. An include selection now counts only rules the buffer declares; before, its names were returned as given.
No cvlr code changes: the cvlr code only ever used the union.

Testing

pytest tests/ -m "not expensive": 1655 passed
pyright: 0 errors

🤖 Generated with Claude Code

RuleSelectionRecord (a TypedDict recorded on ProverRunLog and carried by buffer jobs) duplicated RuleSelection (the InheritRules | SelectRules | ExcludeRules union in composer/prover/conf.py), with _selection_of and _scope_of converting between them. Use RuleSelection throughout: the run log, the job records, buffer_conf, and submit_buffer, which now parses its arguments with rule_selection. A whole-buffer run records InheritRules() rather than None. The checkpoint serializer restores tuples as lists, so SelectRules and ExcludeRules coerce names back to a tuple; otherwise a restored selection compares unequal to a fresh one and is unhashable. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Selection key and checked-rules logic move from free functions in prover.py to key() / checked_among() methods on each RuleSelection variant, beside apply_to. The tuple coercion moves into each __post_init__, dropping the _freeze_names helper. Test run-log constructors that still passed rules=None now pass InheritRules(), and a harness comment no longer describes a whole-buffer run as rules=None. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Drop RuleSelection.key() and checked_among(). SelectRules and ExcludeRules now sort their names on construction, so selections naming the same rules compare equal and buffer_jobs is keyed on (name, selection) directly instead of on an encoded string. Which declared rules a selection checks is a run-history question with a CVL-pipeline assumption (InheritRules means every rule), so it moves out of the ecosystem-neutral conf module into _checked_rules in prover.py. An include selection now counts only declared rules rather than echoing its names back. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

jtoman

approving with nits

jtoman · 2026-10-02T22:44:30Z

+    def __post_init__(self) -> None:
+        # Sorted so that selections naming the same rules compare equal. Coerced to a tuple
+        # because checkpointed graph state records selections, and the checkpoint serializer
+        # restores tuples as lists.
+        object.__setattr__(self, "names", tuple(sorted(self.names)))


I absolutely hate this, but researching it seems to be the "way to do this". This language dude.

jtoman · 2026-10-02T22:45:30Z

    prover_results: list[tuple[RulePath, StatusCodes]]
    spec_digest: str
-    rules: RuleSelectionRecord | None
+    rules: RuleSelection


We're sure dataclasses round trip through a checkpointer okay? I vaguely remember seeing code to that effect when I've poked at it, but my distrust of the checkpointer led me to choose typeddicts to begin with.

That wouldn't have occurred to me to check! I just had Claude build a little program to make sure this works, and it looks like it does.

jtoman · 2026-10-02T22:48:04Z

+def _checked_rules(selection: RuleSelection, declared: Iterable[str]) -> list[str]:
+    """The ``declared`` rules a run under ``selection`` checks. ``InheritRules`` counts as every
+    rule: the source pipeline's base confs select none of their own. Names match exactly, which
+    holds because ``submit_buffer`` admits only names the buffer declares, never patterns."""
+    match selection:
+        case InheritRules():
+            return list(declared)
+        case SelectRules(names):
+            selected = set(names)
+            return [r for r in declared if r in selected]
+        case ExcludeRules(names):
+            excluded = set(names)
+            return [r for r in declared if r not in excluded]


see my comment from another commit; it's very possible to define a def selected(self, declared: Iterable[str]) on each inhabitant of RuleSelection pyright will handle that.

Adding a comment explaining why this is here, and not a public method on the selection types.

jtoman · 2026-10-02T22:48:25Z

    msg: str = "",
-    selection: RuleSelectionRecord | None = None,
-    rules: RuleSelection | None = None,
+    rules: RuleSelection = InheritRules(),


remember kids, this is okay only because these are immutable.

jtoman · 2026-10-02T22:49:31Z

+            match selection:
+                case InheritRules():
+                    sel_desc = ""
+                case SelectRules(names):
+                    sel_desc = f" (rules {list(names)})"
+                case ExcludeRules(names):
+                    sel_desc = f" (excluding {list(names)})"


State that the checked-rules computation is not a general property of a RuleSelection: it relies on the source pipeline's base confs selecting no rules and on submit_buffer admitting only exact declared names. Also update a test comment that still described a whole-buffer run as rules=None. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

ericeil and others added 3 commits October 2, 2026 12:34

ericeil requested a review from jtoman October 2, 2026 20:08

ericeil marked this pull request as ready for review October 2, 2026 20:08

jtoman approved these changes Oct 2, 2026

View reviewed changes

ericeil and others added 2 commits October 2, 2026 16:41

Merge branch 'master' into eric/unify-rule-selection

5dc1e65

ericeil enabled auto-merge (squash) October 2, 2026 23:43

ericeil merged commit 709293a into master Oct 2, 2026
2 checks passed

ericeil deleted the eric/unify-rule-selection branch October 2, 2026 23:44

Navigation Menu

Use one rule-selection type for conf scoping and run history - #259

Use one rule-selection type for conf scoping and run history#259
ericeil merged 5 commits into
masterfrom
eric/unify-rule-selection

ericeil commented Oct 2, 2026 •

edited

Loading

Uh oh!

jtoman left a comment

Uh oh!

jtoman Oct 2, 2026

Uh oh!

ericeil Oct 2, 2026

Uh oh!

jtoman Oct 2, 2026

Uh oh!

ericeil Oct 2, 2026

Uh oh!

jtoman Oct 2, 2026

Uh oh!

ericeil Oct 2, 2026

Uh oh!

jtoman Oct 2, 2026

Uh oh!

jtoman Oct 2, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

ericeil commented Oct 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Why there were two types

What this changes

Testing

Uh oh!

jtoman left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

ericeil commented Oct 2, 2026 •

edited

Loading