loop: review the unsafety moves the checker tolerates - #184
Conversation
The safety loop needs the agent's closing report to learn which target a step worked on and whether the agent considers the step finished, so run_rewrite now asks codex for its last message and returns it alongside the edited trees. run_review reads its report through the same output filter instead of assuming the last-message tree holds exactly one file, and yields an empty report when codex wrote none so the fail-closed gate sees it. Reasoning effort becomes a parameter so reviews and rewrites can run at different levels.
Reviews read a diff and argue about it; they do not need the rewrite tier. A separate models.agent_review setting lets them run on a cheaper model, and xhigh effort keeps the adversarial read thorough.
…rs the rules check-unsafe2 lets some per-function changes through with a warning when the crate-wide picture does not get worse: an operation relocated into another function, a qualifier flipped, an entry point that grew. Those are exactly the moves an agent can use to launder unsafety rather than remove it, so a second codex review now judges the warned lines under a written laundering rule set before a step is accepted. The same rule texts, together with a prose statement of the checker's gates, go into the worker prompt. Until now workers learned the gates from a two-sentence summary and were judged by rules they never saw.
|
Please stop having AI write PR/issue descriptions for you. It's always a puzzle trying to figure out what it's actually trying to say.
I think this is saying that check-unsafe2 allows individual metrics to increase as long as the crate-level
So this PR is adding a new review step similar to the existing FFI review (I assume that would be the "first" codex review), and updating the main rewrite prompt to tell it more about check-unsafe2 and this new review step (it doesn't make sense to use subagents for a review that's targeted to only a few lines, so "workers" must be the rewrite agents).
This sounds like a note for you as the author rather than for the PR reviewer. The two files in question do indeed contradict the whole premise of this PR. More importantly, I'm not sure if this is the right strategy. Trying to write an exhaustive list of "unsound things you shouldn't do" seems like a bit of a lost cause. One alternative might be having an adversarial agent whose job is to write a test case that triggers UB according to MIRI using only safe operations. This is trivial for common unsound helpers like |
2 participants
check-unsafe2 lets some per-function changes through with a warning when the crate-wide picture does not get worse. Those relocations and qualifier flips are the moves an agent can use to launder unsafety rather than remove it, so a second codex review now judges the warned lines under a written laundering rule set before a step is accepted. Workers get the same rule texts and a prose statement of the checker's gates.
Also: run_rewrite returns the agent's final message and takes an effort level, and reviews run on their own model (
models.agent_review) at xhigh effort. #182 builds on both.Worth a look: checker_rules.md and tolerated_unsafety_rules.md both say the checker does not downgrade regressions to warnings, yet this gate exists to review checker warnings. One of the two is stale.