proof-solvers: a time limit on every z3 goal, and a deadline on its I/O #239

Merged

dcharlot merged 1 commit from fix/z3-goal-deadline into main 2026-10-13 09:32:22 -04:00

Conversation 0 Commits 1 Files changed 1 +282 -40

dcharlot commented 2026-10-13 03:11:15 -04:00

Owner

Copy link

What was wrong

The resident z3 session had no time limit. If z3 could not decide a goal, that one goal held the session for as long as z3 kept working on it. Every goal queued behind it waited too. The one-shot z3 had the same problem.

The fix

Every goal now has two limits, on both the resident session and the one-shot rung.

• Soft limit. z3 stops on its own at -t: (GOAL_TIMEOUT, 60 s by default, set with Z3Server::with_goal_timeout). At the limit, (check-sat) answers unknown. The goal counts as undecided, never proved, and the session goes on to the next goal.
• Hard deadline. A goal can lift z3's limit for itself with (set-option :timeout …). So the write and the read both give up GOAL_DEADLINE_GRACE (5 s) past the soft limit. At that point:
  • the one-shot z3 is killed;
  • the resident session is broken and replaced, and the goal stays undecided.

z3 reads its input only as it reaches each command. A goal can contain its own (check-sat) followed by more than a pipe buffer of text. Such a goal blocked the write on the calling thread for as long as that check ran, where no read deadline could stop it. So both ends of the pipe are now on threads of their own:

• in the session, a writer thread fed by a channel and a reader thread;
• in the one-shot rung, output_within.

Checked

z3 behaviour. Checked on Homebrew z3 5.1.0 (build host) and on Ubuntu's 4.8.12, the version the CI image installs:

• unknown comes at the soft limit;
• a goal's :timeout lifts that limit, even after (reset);
• the session decides on after an unknown;
• a 426 KB write blocks behind the goal's own (check-sat).

Tests. Five new tests, on a goal z3 cannot decide in seconds (32-bit factors of a 64-bit semiprime):

• a_goal_past_its_limit_is_unknown_and_the_session_decides_on
• a_goal_that_lifts_its_limit_is_cut_off_at_the_deadline: the session's z3 is gone after the drop
• a_goal_too_long_to_write_is_cut_off_at_the_deadline
• a_one_shot_z3_is_killed_at_the_deadline: both ends, and the pid is checked
• the_server_keeps_its_goal_limit_across_sessions: the builder, and the replacement session keeps the limit

Mutation checks. Each mutation fails at least one of the new tests:

• no -t:;
• no read deadline in the session;
• no read deadline in the one-shot rung;
• the one-shot write on the calling thread;
• no kill at the deadline;
• the builder not restarting the resident;
• the retire path dropping the limit.

Build host. cargo test --workspace (proof-rs) passes. clippy -p proof-solvers --all-targets -D warnings is clean. proof-conformance passes all checks. gen-vectors output is byte-identical to proof/conformance/v1; the conformance ladder holds no z3.

🤖 Generated with Claude Code

## What was wrong The resident `z3` session had no time limit. If z3 could not decide a goal, that one goal held the session for as long as z3 kept working on it. Every goal queued behind it waited too. The one-shot z3 had the same problem. ## The fix Every goal now has two limits, on both the resident session and the one-shot rung. - **Soft limit.** z3 stops on its own at `-t:` (`GOAL_TIMEOUT`, 60 s by default, set with `Z3Server::with_goal_timeout`). At the limit, `(check-sat)` answers `unknown`. The goal counts as undecided, never proved, and the session goes on to the next goal. - **Hard deadline.** A goal can lift z3's limit for itself with `(set-option :timeout …)`. So the write and the read both give up `GOAL_DEADLINE_GRACE` (5 s) past the soft limit. At that point: - the one-shot z3 is killed; - the resident session is broken and replaced, and the goal stays undecided. z3 reads its input only as it reaches each command. A goal can contain its own `(check-sat)` followed by more than a pipe buffer of text. Such a goal blocked the write on the calling thread for as long as that check ran, where no read deadline could stop it. So both ends of the pipe are now on threads of their own: - in the session, a writer thread fed by a channel and a reader thread; - in the one-shot rung, `output_within`. ## Checked **z3 behaviour.** Checked on Homebrew z3 5.1.0 (build host) and on Ubuntu's 4.8.12, the version the CI image installs: - `unknown` comes at the soft limit; - a goal's `:timeout` lifts that limit, even after `(reset)`; - the session decides on after an `unknown`; - a 426 KB write blocks behind the goal's own `(check-sat)`. **Tests.** Five new tests, on a goal z3 cannot decide in seconds (32-bit factors of a 64-bit semiprime): - `a_goal_past_its_limit_is_unknown_and_the_session_decides_on` - `a_goal_that_lifts_its_limit_is_cut_off_at_the_deadline`: the session's z3 is gone after the drop - `a_goal_too_long_to_write_is_cut_off_at_the_deadline` - `a_one_shot_z3_is_killed_at_the_deadline`: both ends, and the pid is checked - `the_server_keeps_its_goal_limit_across_sessions`: the builder, and the replacement session keeps the limit **Mutation checks.** Each mutation fails at least one of the new tests: - no `-t:`; - no read deadline in the session; - no read deadline in the one-shot rung; - the one-shot write on the calling thread; - no kill at the deadline; - the builder not restarting the resident; - the retire path dropping the limit. **Build host.** `cargo test --workspace` (proof-rs) passes. `clippy -p proof-solvers --all-targets -D warnings` is clean. `proof-conformance` passes all checks. `gen-vectors` output is byte-identical to `proof/conformance/v1`; the conformance ladder holds no z3. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-10-13 03:11:15 -04:00

proof-solvers: a time limit on every z3 goal, and a deadline on its I/O ... 4a137b3cdd

The resident z3 session had no limit. One goal z3 could not decide held the
session, and every goal queued behind it, for as long as z3 kept at it.

Two guards now close that, in the resident session and the one-shot z3 alike:

- z3's own soft limit (`-t:`, GOAL_TIMEOUT = 60 s by default;
  Z3Server::with_goal_timeout). At the limit `(check-sat)` answers
  `unknown`, which counts as undecided, and the session decides on.
- A deadline GOAL_DEADLINE_GRACE (5 s) past that limit, on both the write
  and the read. A goal can lift z3's limit for itself with
  `(set-option :timeout ...)`. Past the deadline the one-shot z3 is killed,
  and the resident session is broken and replaced.

z3 reads its input only as it reaches each command. So a goal with a
`(check-sat)` of its own and more than a pipe's worth of text after it
blocked the write on the calling thread for as long as that check ran.
Both ends of the pipe are now on threads of their own.

Checked on Homebrew z3 (build host) and on Ubuntu's 4.8.12 (the CI
image's version): unknown at the soft limit, the limit lifted by a goal's
:timeout even after (reset), and a 426 KB write that blocks behind the
goal's own check.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

dcharlot merged commit 8b7a83053b into main 2026-10-13 09:32:22 -04:00

dcharlot referenced this pull request from a commit 2026-10-13 09:32:23 -04:00

Merge pull request 'proof-solvers: a time limit on every z3 goal, and a deadline on its I/O' (#239) from fix/z3-goal-deadline into main

dcharlot referenced this pull request from a commit 2026-10-13 22:40:05 -04:00

Merge origin/main (at 1ec8f447, with #233, #234, #236, #238, #239, #240) into wai/d2c-decoders-on-ops

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!239

No description provided.