Replace per-edit unsafety ratchet with reviewed net-decrease policy by thedataking · Pull Request #167 · GaloisInc/Tractor-Crisp

thedataking · 2026-07-25T11:23:59Z

check-unsafe2 enforced a ratchet per function and per metric: no unsafety metric could increase anywhere, even when the crate-wide result improved. That rule could not distinguish adding unsafe code from relocating it into a smaller, explicit boundary, so legitimate decompositions were rejected in flight and the rewriter often spent its budget reverting them or landing no-ops.

The new policy judges the bounded net effect, reviews what counting cannot decide, and gives stalled runs an honest way to stop:

Functions free of unsafe remain protected. Existing unsafe functions, and new named implementation functions created as part of a relocation, may absorb unsafe operations only when the crate-wide total does not increase. Raw-pointer fields, int-to-pointer casts, new foreign-function uses, and calls into FFI entry points remain hard errors. Pointer-bearing signature increases are permitted on unsafe fn, while a new or newly-safe function must have a pointer-free signature.
Every checker-tolerated per-function increase is sent to a dedicated review with an anti-laundering rubric. FFI entry-point changes retain their separate review, and the checker now warns immediately when work grows inside a count-exempt wrapper. Hard checker failures run before expensive tests or reviews.
The adversarial corpus covers net increases, unsafe relocation into new helpers, reference-oracle laundering, raw-pointer signature flips, unsafe helpers used for decomposition, and implementation work stuffed into FFI wrappers.
The loop can accept a net-neutral preparatory step or a final BLOCKED: result instead of pressuring the rewriter into cosmetic or rule-breaking edits. Dead-end notes must cite the exact checker diagnostic, review finding, or failing test, and oversized plans can be compacted without changing their remaining work.
Near the end of a stalled run, a read-only adjudicator can waive residual operations only when they are sound, minimal, and inherent to the FFI boundary. Planning, adjudication, and review have separate model and effort settings, and a run whose remaining operations are all covered ends explicitly as "completed with residual unsafe."

Each case is a rewrite that lowers or preserves the unsafe count without making the code safer: laundering helpers, count compression, export-set edits, closure rekeying, and similar shapes. Several were observed from the rewriter during safety-loop runs; the rest close channels found by review.

… inventory A crate with no baseline JSON is held to an all-zero inventory rather than skipped, so unsafe code can't be hidden in a newly added crate.

… set Only a per-function entry-point boolean was recorded, so deleting an exported fn or static, demoting it, or editing an #[export_name] value was invisible to the checker. The exported symbol set is the ABI contract; record each item's symbol and reject any change.

Entry points are exempt from the unsafety metrics, so routing work through an exported wrapper hides unsafe code behind the exemption. The FFI rules already forbid such calls; tracking them per function lets the checker reject the move deterministically instead of relying on the LLM review to notice.

Inline asm can access arbitrary memory but fed no metric, so rewriting unsafe operations into asm! blocks would lower the count without making anything safer.

An `unsafe impl` (e.g. `unsafe impl Send`) is a zero-code soundness assertion no body metric sees, so a rewrite could trade counted unsafety for an uncounted promise. c2rust never emits one, so any occurrence was added by refactoring; reject new ones until a review-gated relaxation exists.

rustc reports closures as synthetic function entries. Treating those entries as independent baseline items caused safety-preserving zlib rewrites to be rejected: closures introduced inside FFI entry points did not inherit the entry-point exemption, and raw-pointer types in local closure signatures were treated as new named signature surface. Fold closure-like entries into their enclosing named item before comparison. Sum body-derived metrics (derefs, unsafe calls, asm, uses, and casts), so moving unsafe operations into a closure does not hide them. Keep declaration properties (qualifiers, signature pointer counts, and export status) from the enclosing item only. This lets closures inside FFI entry points inherit their exemption and avoids charging local closure signatures as named API surface.

casts_int_to_ptr only counted `as` casts, so the same usize round-trip spelled as with_exposed_provenance() and friends went uncounted. Charge the std APIs that materialize a pointer from an address the same as the cast they replace.

…natures sig_contains_raw_ptr is non-increasing, so wrapping a pointer in a local struct and passing that would zero the count with no real progress. Descend local Adts (and charge NonNull directly); std types are not descended since they reach NonNull internally without being the function's own unsafety surface.

Rejected-review findings previously lived only in process memory, so a restarted run repeated attempts the reviewer had already rejected. Rebuild the sticky reminder list from FAIL reviews in the op_history reflog at startup, and record the deterministic pre-gate's rejections the same way, so both kinds of rejection are equally durable.

…al cap

…oint All 30 FFI-review rejections in the 2026-08-06 zlib run were one move: unsafe work relocated into an exported wrapper, where the count exemption hides it. The review catches this only after the full step is spent (agent run, tests, review: ~3.5 min discarded each time). The relocation is mechanically visible in the metrics, so say so at check time: the agent runs check-unsafe2 mid-turn and can self-correct before the step is judged. Warning only -- legitimate refactors also grow wrapper conversion code -- and phrased to not match the tolerated-warning regexes in crisp, so it alerts the agent without also triggering a tolerated-move review; the FFI review stays the judge.

…oints Charging every new function for struct-carried pointer signatures (3cd5cde) made the grouped raw-free state migration a serial prerequisite for all decomposition: 25 of run 6's 34 blocked steps cite it, and throughput fell to ~54 ops/h against run 3's ~300 at the same count depth. An unsafe fn self-counts, so letting it carry raw-pointer signatures cannot create a terminal hiding place; requiring a pointer-free signature to create a safe fn or drop an unsafe qualifier closes the create-then-flip laundering route that a plain revert would reopen. Revert if the next run does not at least double ops/attempt.

The step prompt names only the crate-wide total; the per-function inventory sits in the sandbox JSON, which the zlib run-7 agent consulted once in 430 iterations. Its final 20 iterations all worked a gzip cluster holding 78 of 2139 remaining operations while 95% of them sat in four files it never opened. Summarize per-file totals and the largest functions into the prompt so each iteration's target choice starts from the mass distribution rather than the plan's current fixation.

A failure streak means the agent's own target choice is not working: zlib run 7 ended with twenty consecutive no-progress iterations inside a 78-op gzip cluster because the plan's dead-end notes had fenced off everything else, while 95% of the remaining operations sat in files the agent never opened. After retarget_after consecutive failures, override plan-driven choice with an explicit target: the largest function in the file carrying the most unsafe operations. Ranking files before functions matters because unsafety mass and function size diverge: deflate.rs holds the most remaining operations (947) spread across many mid-size functions (largest 186), and a per-function argmax would starve it indefinitely behind inflate::inflate (503). The file is also the unit where reductions compound -- helpers and slice views built for one function are reused by its neighbors -- so successive retargets should land in one neighborhood rather than chase the momentary biggest function across files. An accepted reduction resets the streak and returns the choice to the agent; waived functions are settled and never targeted.

The stall suffix offers a net-neutral preparatory step as the fallback, and the loop counts such steps as failures; in zlib run 7 the agent farmed that escape hatch for 16 of the 20 green, reviewed, accepted iterations that ended the run. Preparation is the right call early in a streak, so allow neutral_steps_per_streak of them; past that the suffix withdraws the invitation and demands a removal or an explicit BLOCKED, so a genuine dead end surfaces in a few iterations instead of grinding to the stop.

zlib run 7's plan merged four clusters into one prohibition -- do not make helpers over ABI-shaped state safe -- although the checker had only rejected specific gz_state/z_stream probes, and the hygiene rewrite preserved the overreach while the plan's four identically worded Next rows never moved. Require dead-end notes to stay scoped to the functions and types their gate actually fired on, at both the step that writes them and the rewrite that merges them, and give the hygiene rewriter the current inventory so remaining work is reordered by where the operations are.

thedataking · 2026-09-05T00:35:56Z

Superseded by #182, stacked on the cleaned-up #171. The replacement carries the current safety-loop work and uses the checker policy on main; the relaxed checker policy and residual-unsafety waiver experiments from this PR are not included.

thedataking changed the title ~~Replace the per-edit unsafety ratchet with a reviewed net-decrease policy~~ Replace per-edit unsafety ratchet with reviewed net-decrease policy Jul 25, 2026

thedataking force-pushed the perl/optimize-agent-loop branch from 23e8371 to af680f2 Compare July 29, 2026 11:42

thedataking changed the base branch from main to perl/find-unsafe2-hardening July 29, 2026 11:42

thedataking force-pushed the perl/optimize-agent-loop branch from af680f2 to 4552934 Compare July 29, 2026 12:03

thedataking changed the base branch from perl/find-unsafe2-hardening to perl/ffi-pregate-recovery July 29, 2026 12:16

thedataking added 9 commits August 5, 2026 01:30

find_unsafe2: check crates missing from the baseline against an empty…

84ba4af

… inventory A crate with no baseline JSON is held to an all-zero inventory rather than skipped, so unsafe code can't be hidden in a newly added crate.

find_unsafe2: charge inline asm as an unsafety metric

bc7fa85

Inline asm can access arbitrary memory but fed no metric, so rewriting unsafe operations into asm! blocks would lower the count without making anything safer.

thedataking force-pushed the perl/ffi-pregate-recovery branch from a935a7f to e2478e5 Compare August 5, 2026 09:14

thedataking force-pushed the perl/optimize-agent-loop branch from 4552934 to 774b4ca Compare August 5, 2026 09:23

thedataking force-pushed the perl/optimize-agent-loop branch from 774b4ca to 7f18616 Compare August 6, 2026 09:59

thedataking force-pushed the perl/ffi-pregate-recovery branch from e2478e5 to 17eb005 Compare August 6, 2026 09:59

thedataking added 9 commits August 7, 2026 00:59

check-unsafe2: allow unsafety to move between unsafe fns under a glob…

7e0ccd0

…al cap

workflow: review checker-tolerated unsafety before acceptance

40fa80b

check-unsafe2: tolerate relocated unsafety in new functions under review

0b8bd55

workflow: adjudicate terminal unsafe operations with waivers

106b515

workflow: let stalled agents prepare, explain, or declare BLOCKED

85c4d38

workflow: configure models and effort for planning and reviews

b6ddb94

loop: rewrite a bloated or stall-implicated plan into a compact guide

c789fba

thedataking force-pushed the perl/optimize-agent-loop branch from 7f18616 to 25500fb Compare August 7, 2026 08:05

thedataking added 3 commits August 8, 2026 22:23

thedataking force-pushed the perl/ffi-pregate-recovery branch from 17eb005 to 2bf487a Compare September 5, 2026 00:35

thedataking mentioned this pull request Sep 5, 2026

Simplify safety steps and retain target feedback #182

Open

thedataking closed this Sep 5, 2026

Navigation Menu

Uh oh!

Replace per-edit unsafety ratchet with reviewed net-decrease policy - #167

Replace per-edit unsafety ratchet with reviewed net-decrease policy#167
thedataking wants to merge 23 commits into
perl/ffi-pregate-recoveryfrom
perl/optimize-agent-loop

thedataking commented Jul 25, 2026 •

edited

Loading

Uh oh!

thedataking commented Sep 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

thedataking commented Jul 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thedataking commented Sep 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

thedataking commented Jul 25, 2026 •

edited

Loading