Bind approvals and feedback to the revision they were about #74

2026-09-29T19:13:21Z

dev-agent commented

2026-09-29 19:13:21 +00:00

Fixes counterexamples 1–4 from the Quint model (#73). In each, an approval or feedback landed on the next plan, which the operator had not seen:

a repeated approve;
approve rev-1 meant for the architecture;
approving on both Matrix and Gitea;
approve plus an afterthought.

Changes

Revisions are numbered across the work item: arch rev-1, milestone-1 rev-2, and so on. A4 already required "monotonically-increasing" tags; the code numbered them per gate, which is why rev-1 could mean two plans.
Replies are stamped on arrival with the revision that was up:
- Matrix: the one whose approval request had been sent. It's a plain value the transport thread reads, saved as shown_rev, and restored on boot from the open gate.
- Gitea: the latest plan comment older than the reply. The plan issue's data now records which comment posted which revision (board.posts).
Gate.evaluate(…, about=): a reply that names no revision applies only if its stamp is the current revision.
- Otherwise an approval isn't applied ("that approval arrived while rev-1 was up; the current plan is milestone-1 rev-2, not applied. Reply again to approve it").
- Feedback rejects nothing, but stays in the transcript so the planner still hears it.
- approve rev-N still binds by its number.
The approval request names the gate: "reply 'approve' to approve milestone-1 rev-2".
Spec A4 states both rules and notes that Matrix reply relations aren't implemented yet.

The model (specs/): applies the same rule. Scenarios 1–4 now expect the properties to hold. approval_only_of_what_was_seen and feedback_only_on_what_was_seen held over 200,000 random traces each. The approval property also held under Apalache's exhaustive check to depth 8, where it found counterexample 1 before this change.

Tests

Counterexamples 1–4 in test_quint_counterexamples.py lose their xfail and pass.
New test_approval_binding.py: task-wide numbering; a stale approval is answered and a fresh one works; stale feedback is recorded but rejects nothing; Gitea binding by comment order; the stamp surviving a restart.
New gate cases in test_gates.py. All 10 new tests fail on main.
Two existing tests updated for the new rule: test_stop now waits for each plan to be up before replying, as an operator would, instead of sending the whole script in a burst. test_control approves rev-3 under task-wide numbering.

490 unit tests and the integration suite (19 passed, 7 skipped) pass; lint and format clean. Counterexamples 5–7 remain xfail for their own PRs.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

Fixes counterexamples 1–4 from the Quint model (#73). In each, an approval or feedback landed on the **next** plan, which the operator had not seen: - a repeated `approve`; - `approve rev-1` meant for the architecture; - approving on both Matrix and Gitea; - `approve` plus an afterthought. **Changes** - **Revisions are numbered across the work item:** arch rev-1, milestone-1 rev-2, and so on. A4 already required "monotonically-increasing" tags; the code numbered them per gate, which is why `rev-1` could mean two plans. - **Replies are stamped on arrival** with the revision that was up: - **Matrix:** the one whose approval request had been sent. It's a plain value the transport thread reads, saved as `shown_rev`, and restored on boot from the open gate. - **Gitea:** the latest plan comment older than the reply. The plan issue's data now records which comment posted which revision (`board.posts`). - **`Gate.evaluate(…, about=)`:** a reply that names no revision applies only if its stamp is the current revision. - Otherwise an approval isn't applied ("that approval arrived while rev-1 was up; the current plan is milestone-1 rev-2, not applied. Reply again to approve it"). - Feedback rejects nothing, but stays in the transcript so the planner still hears it. - `approve rev-N` still binds by its number. - **The approval request names the gate:** "reply 'approve' to approve milestone-1 rev-2". - **Spec A4** states both rules and notes that Matrix reply relations aren't implemented yet. **The model** (`specs/`): applies the same rule. Scenarios 1–4 now expect the properties to hold. `approval_only_of_what_was_seen` and `feedback_only_on_what_was_seen` held over 200,000 random traces each. The approval property also held under Apalache's exhaustive check to depth 8, where it found counterexample 1 before this change. **Tests** - **Counterexamples 1–4** in `test_quint_counterexamples.py` lose their `xfail` and pass. - **New `test_approval_binding.py`:** task-wide numbering; a stale approval is answered and a fresh one works; stale feedback is recorded but rejects nothing; Gitea binding by comment order; the stamp surviving a restart. - **New gate cases in `test_gates.py`.** All 10 new tests fail on `main`. - **Two existing tests updated for the new rule:** `test_stop` now waits for each plan to be up before replying, as an operator would, instead of sending the whole script in a burst. `test_control` approves `rev-3` under task-wide numbering. 490 unit tests and the integration suite (19 passed, 7 skipped) pass; lint and format clean. Counterexamples 5–7 remain `xfail` for their own PRs. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

dev-agent added 1 commit 2026-09-29 19:13:21 +00:00

Bind approvals and feedback to the revision they were about

CI / checks (push) Skipped

CI / checks (pull_request) Successful in 1m16s

Details

97863c1939

Fixes counterexamples 1-4 from specs/orchestrator.qnt: a repeated
'approve', 'approve rev-1' meant for the architecture, approving on both
channels, and 'approve' plus an afterthought all landed on the next
plan, one the operator had not seen.

- Revisions are numbered across the work item (A4 already required
  monotonic tags; the code numbered per gate), so rev-N names one plan.
- Each reply is stamped on arrival with the revision that was up: in
  Matrix the one whose approval request had been sent (a plain value
  the transport thread reads, restored on boot), in Gitea the latest
  plan comment older than the reply (board.posts).
- Gate.evaluate applies a reply that names no revision only if its stamp
  is the current revision. Otherwise an approval is not applied and
  feedback rejects nothing (it is still in the transcript), and the
  agent says which revision is up. 'approve rev-N' binds by its number.
- Spec A4 states both rules. The model applies them; scenarios 1-4 now
  expect the properties to hold, and both held over 200,000 random
  traces and Apalache's exhaustive check to depth 8.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE

dongar approved these changes

2026-09-29 19:45:04 +00:00

dongar merged commit 6fdec6922b into main

2026-09-29 19:45:07 +00:00

dongar deleted branch bind-approvals-to-revisions

2026-09-29 19:45:07 +00:00

dev-agent referenced this pull request

2026-09-30 12:38:01 +00:00

Make the agent conversational: questions, explanations and asking back, in Matrix #77

Sign in to join this conversation.