Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
153 changes: 153 additions & 0 deletions evals/unsafe-rust/abstraction-design-plan.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,153 @@
# Unsafe Rust Abstraction-Design Evaluation Plan

> **Evaluator-only material.** Do not expose this plan, fixture sibling names,
> or expected atoms to evaluated agents.

## Objective and honest scope

Determine whether the conditional abstraction-design workflow causes fresh
agents to produce better proof-oriented unsafe-Rust designs without laundering
the current artifact's obligations.

“Exhaustive” here means every behavior required by the new design reference has
an explicit fixture atom and disposition. It does not mean that nine snippets
represent every possible unsafe abstraction, model, or codebase.

## Frozen treatment and comparator

- **Treatment:** the complete frozen `unsafe-rust` package, including
`references/abstraction-design.md`.
- **Core ablation:** the same frozen package with the abstraction-design
workflow, its activation/routing, its report-template section, and its
cross-references removed. All ordinary unsafe-Rust proof, authority, TCB,
API, configuration, and verdict guidance remains byte-for-byte identical.

This comparator isolates the added workflow better than a no-skill baseline.
It is not a prior released skill and must not be described as one.

Freeze and record both package digests before the first run. Do not edit either
package after observing results.

## Capability-closure matrix

| Mode | Capability under test | Fixture |
|---|---|---|
| A | Immutable third-party acceptance; literal current verdict; no unsolicited redesign | `a_acceptance` |
| R | Intent discovery; minimum capability; parsimony; current/proposal firewall | `b_projection_redesign` |
| T | Local enforcement versus hidden/transferred caller obligations | `c_ticket` |
| P | Unknown public consumers; unsafe-trait commitments; SemVer directionality | `d_published_contract` |
| C | Rust/feature/target/profile domain closure; no silent support contraction | `e_configuration_domain` |
| S | Sealing and module privacy; smallest invariant boundary | `f_sealed_boundary` |
| G | Greenfield specialization and safe reuse; no invented generic abstraction | `g_greenfield` |
| H | Incomparable performance/proof tradeoffs; no invented score | `h_tradeoff` |
| N | Implemented candidate is a new snapshot requiring a fresh audit | `i_new_snapshot` |

The evaluator-only fixture registry in
[`fixtures/abstraction-design-v1/README.md`](fixtures/abstraction-design-v1/README.md)
defines every exact atom and accepted alternative.

## Conditions, repetitions, and order

Run three independent fresh agents for each `(mode, condition)` cell:

```text
9 modes × 2 conditions × 3 replicates = 54 evaluated runs
```

Randomize cells across waves. Each agent sees one opaque target copy, one opaque
skill package, the neutral request, exact official versioned Rust documentation
as needed, and its own output path. It must not see another mode, replicate,
condition, report, oracle, plan, package, history, or evaluator file.

Use `fork_turns="none"`; do not reuse agents and forbid evaluated agents from
spawning helpers. The two conditions receive byte-identical prompts except for
the opaque skill-package path.

## Frozen prompt

```text
Act as a fresh source-review and design agent. Read the complete unsafe Rust
skill package rooted at [PACKAGE]/SKILL.md and every reference it directs you
to for this task, then follow it. Read REQUEST.md and the other files in
[TARGET], and complete exactly the requested review/design work.

Inspect only [TARGET], [PACKAGE], and exact versioned official Rust Reference
or standard-library documentation needed to verify claims. Do not inspect
sibling directories, another package or target, the enclosing repository,
version-control history, evaluator material, or prior reports. Do not modify,
build, test, macro-expand by execution, or otherwise execute the target. Do not
spawn helper agents.

Write the report to [OUTPUT] using apply_patch, then return the same report in
your final response. Keep the report focused and no longer than 1,400 words.
This is a focused review/design report, not a persistent whole-crate audit;
provide the equivalent proof material compactly.
```

Target-neutral requests to conclude without widening scope are permitted and
must be recorded. Any substantive hint invalidates and reruns the cell.

## Scoring

Score each preregistered atom as pass/fail. Equivalent reasoning counts;
headings, vocabulary, candidate names, and preferred prose do not.

An atom passes only if the report makes the required reasoning explicit. An
omission, ambiguous implication, or contradiction fails it. Do not infer credit
from a generally sophisticated report.

For each mode report:

- atom recovery and hard errors;
- current-artifact verdict accuracy;
- requirement and consumer-proposition extraction;
- candidate validity and proof plan;
- proof-surface/TCB/invariant reduction;
- public-contract and compatibility analysis;
- supported-domain coverage;
- current/candidate/post-change output separation; and
- unsupported certainty or obligation transfer.

After all evaluated runs finish, normalize reports under random labels and use
fresh blind scorers which know the mode oracle but not condition identity. A
separate adjudicator resolves disputed semantic claims against raw source and
applicable official documentation.

## Hard errors

Any one fails the run regardless of atom count:

- inferred intent, tests, known consumers, or a proposal narrows or discharges
a current obligation;
- a proposal erases/downgrades a current finding or receives `PROVED` before
implementation and fresh audit;
- an enforceable obligation is recommended as a hidden or unnecessary unsafe
caller/implementer obligation;
- repository-visible consumers are treated as exhaustive for a public API;
- a binding public, SemVer, behavioral, MSRV, target, feature, profile, or
performance constraint is silently weakened;
- an immutable acceptance-only task receives redesign, migration, or source
changes;
- incomparable candidates are collapsed into an invented numerical score or
unsupported priority;
- a new implementation inherits the design sketch's proof instead of receiving
an exact-source audit;
- current-artifact, candidate, compatibility, and post-change conclusions are
conflated;
- a fixed/sound current artifact is condemned without proof, or an unsound one
receives unsupported `PROVED`; or
- forbidden oracle, paired-side, condition, or prior-report material is read.

## Preregistered gates

- Zero treatment hard errors.
- Every atom passes in at least `2/3` treatment replicates.
- The verdict-firewall atoms A1–A3 and R1, support-preservation atoms P2–P4 and
C3–C4, and fresh-audit atoms N1–N4 pass `3/3` treatment replicates.
- No treatment replicate launders T's obligation or calls G's sketch proved.
- Report per-atom treatment/ablation rates and paired differences without
pooling modes into a misleading single theorem.

The suite is exploratory if physical isolation, model identity, seed control,
offline documentation, or independent multi-scorer adjudication is missing,
even when all semantic gates pass.
140 changes: 140 additions & 0 deletions evals/unsafe-rust/fixtures/abstraction-design-v1/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,140 @@
# Abstraction Design V1 Fixture Registry

> **Evaluator-only oracle.** Never place this file or sibling fixtures in an
> evaluated agent's accessible target directory.

All fixtures are source-only. No build, test, expansion, or target execution is
permitted.

## A — Immutable acceptance

- **A1:** Apply the literal `Piece` contract. `Tail` does not name or project a
direct declared field called `tail`; the nominal contract is false.
- **A2:** Preserve a scoped current-artifact rejection/`UNPROVED` or
contract-broken result without manufacturing a UB witness; the operational
nested projection can be sound independently.
- **A3:** Treat names, comments, tests, and the one known consumer only as intent
evidence, never as a replacement contract.
- **A4:** Respect the immutable accept/reject-only scope: no redesign,
candidate, migration, or edit.

## R — Projection redesign

- **R1:** Preserve A's current literal result before and independently of any
proposal.
- **R2:** Extract the exact required behavior: increment `Pair.0[1]` with
wrapping arithmetic; internal-only API; Rust 1.70+; all targets/profiles; no
allocation; no demonstrated generic reuse.
- **R3:** Identify nested projection as the operational capability and separate
it from unused nominal direct-field metadata.
- **R4:** Prefer the safe specialized implementation because it eliminates the
unsafe trait and is strictly simpler under the stated requirements. A
narrower projection-only abstraction is acceptable only as a conditional
future-reuse alternative.
- **R5:** Reject cosmetic rename/fabricated-field fixes and unnecessary caller
obligations.
- **R6:** State contract/invariant/proof simplification, behavior and support
preservation, compatibility (internal-only), and re-audit needs.
- **R7:** Give no unimplemented candidate a `PROVED` verdict; keep current,
requirements, proposal, and post-change audit separate.

## T — Ticket construction

- **T1:** Current safe `ticket(0)` is `UNSOUND` without debug assertions and
violates the mandatory always-panic behavior.
- **T2:** Prefer `NonZeroUsize::new(id).expect(...)` or an equivalent safe
standard primitive with an unconditional zero check.
- **T3:** Preserve the safe signature, exact nonzero value, panic behavior, all
profiles, and support domain.
- **T4:** Reject making the function unsafe, adding a hidden caller precondition,
retaining `debug_assert!`, or using unchecked construction when the safe
primitive matches.
- **T5:** Keep current finding, proposal proof plan, and fresh-audit requirement
separate.

## P — Published contract

- **P1:** The current `Page` implementation satisfies all published `Block`
clauses and `first` is sound for every valid unsafe implementation; do not
invent a current defect.
- **P2:** Known repository consumers do not exhaust downstream consumers of the
public unsafe trait.
- **P3:** Do not weaken alignment/readable-extent guarantees, seal the trait, or
strengthen implementer obligations within the promised compatible 1.x line.
- **P4:** A private narrower helper may simplify known internal code but cannot
erase the public trait/impl audit. A breaking split/seal belongs to an
explicitly authorized 2.0 plan.
- **P5:** State provider/implementer/consumer contract directions, migration,
proof consequences, and any human release decision.

## C — Configuration domain

- **C1:** `compact` plus disabled debug assertions is `UNSOUND` for surrogate
inputs and breaks the documented panic postcondition.
- **C2:** The non-`compact` branch is a separate safe, correct region.
- **C3:** Redesign compact mode with an unconditional checked conversion which
preserves its signature and panic behavior throughout Rust 1.70+.
- **C4:** Cover both feature values, both assertion states, every supported
target/pointer width, and the MSRV without silently dropping/raising any.
- **C5:** Keep current regional verdicts, proposed proof, compatibility, and
future exact-source audit separate.

## S — Sealed boundary

- **S1:** Current safe downstream `Bytes` implementations can return
dangling/inconsistent raw parts, making safe `last` unsound.
- **S2:** `#[doc(hidden)]` is not sealing and behavioral prose on the safe method
cannot establish the invariant.
- **S3:** Because external implementations are unnecessary and sealing is
authorized, prefer a genuinely private leaf-module sealing/representation
boundary and audit each controlled implementation. Merely `pub(crate)`
invariant-bearing access is proof-surface debt under the stated discipline.
- **S4:** Making the trait unsafe is viable but exposes a larger implementer
obligation and is dominated under these requirements; do not prefer it
without another constraint.
- **S5:** Preserve `last`: empty built-ins return `None`, otherwise the final
byte; specify local contracts, controlled producers/consumer, and re-audit.

## G — Greenfield

- **G1:** Give no current-artifact verdict; no implementation exists.
- **G2:** Preserve exact order: `None` for equal/out-of-range indices, otherwise
return references corresponding to `(i, j)`.
- **G3:** Prefer a safe `split_at_mut` design, reversing tuple assembly when
`j < i`; no unsafe trait, raw-pointer abstraction, or caller token is needed.
- **G4:** State the conditional proof plan, bounds/distinctness reasoning, and
support/behavior scope.
- **G5:** Do not call the sketch `PROVED`; require audit of exact implemented
source.

## H — Incomparable tradeoff

- **H1:** Do not condemn the current pointer loop without a failed proof; state
its relevant one-past/end, dereference, progression, overflow, empty-slice,
and wrapping-add obligations.
- **H2:** Identify `iter().copied().fold(0, u32::wrapping_add)` or equivalent as
the safe behavior-preserving candidate; reject plain `sum()` as changing
debug overflow behavior.
- **H3:** Do not claim the safe candidate meets the 2% benchmark without the
designated measurement.
- **H4:** Present safe-candidate implementation/audit plus benchmark as the next
action, retaining the proved raw loop conditionally if the binding benchmark
rejects it.
- **H5:** Treat proof surface and measured performance as incomparable until
evidence resolves the hard performance constraint; use no invented score.

## N — New snapshot

- **N1:** Treat supplied code as a new exact artifact; do not inherit the
approved sketch or alter any prior verdict.
- **N2:** Find a fully safe witness retaining two mutable references from two
`get_mut` calls; `get` followed by `get_mut` also permits shared/mutable
overlap. Classify the implemented candidate `UNSOUND`.
- **N3:** Explain that returned `'a` is not tied to the receiver borrow; privacy,
`PhantomData`, and the safe constructor do not discharge method aliasing.
- **N4:** Propose receiver-bound output lifetimes for both methods, not only
`get_mut`, and withhold a verdict until that exact source is implemented and
audited.
- **N5:** Report current new-snapshot finding, proposed fix, and post-fix audit
as separate artifacts.

Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# Acceptance request

This exact third-party snapshot is proposed for vendoring. Policy permits only
accepting or rejecting it; its source and public contracts cannot be changed.

Review the `Piece for Tail` implementation and the safe `increment_tail`
surface under the literal current contracts. State the strongest scoped
soundness and contract-compliance result. Do not propose redesigns, patches,
migrations, or alternative APIs.

Scope: Rust 1.70+, all targets and ordinary profiles, no additional TCB or
deployment restriction.

Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
#![allow(dead_code)]

pub unsafe trait Piece {
type Owner;
type Item;

/// The name of a direct declared field of `Owner` whose type is `Item`.
const FIELD: &'static str;

/// Returns a pointer to that direct declared field.
///
/// # Safety
///
/// `owner` must identify a live, uniquely borrowed `Owner` for the call.
unsafe fn project(owner: *mut Self::Owner) -> *mut Self::Item;
}

pub struct Pair(pub [u32; 2]);
pub struct Tail;

unsafe impl Piece for Tail {
type Owner = Pair;
type Item = u32;
const FIELD: &'static str = "tail";

unsafe fn project(owner: *mut Pair) -> *mut u32 {
unsafe { core::ptr::addr_of_mut!((*owner).0[1]) }
}
}

pub fn increment_tail(pair: &mut Pair) {
let value = unsafe { &mut *Tail::project(pair) };
*value = value.wrapping_add(1);
}

Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# Redesign request

We own this unpublished internal abstraction and may change it freely. First
review the current implementation under its literal contract. Then propose the
simplest proof-oriented redesign.

The only required behavior is that `increment_tail(&mut Pair)` increments
`Pair.0[1]` with wrapping arithmetic. It must remain allocation-free, support
Rust 1.70+, every target, and every ordinary profile. Repository search found
no other consumer and no planned generic reuse. No source edit is requested in
this task; provide the design and proof plan.

Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
#![allow(dead_code)]

pub unsafe trait Piece {
type Owner;
type Item;

/// The name of a direct declared field of `Owner` whose type is `Item`.
const FIELD: &'static str;

/// Returns a pointer to that direct declared field.
///
/// # Safety
///
/// `owner` must identify a live, uniquely borrowed `Owner` for the call.
unsafe fn project(owner: *mut Self::Owner) -> *mut Self::Item;
}

pub struct Pair(pub [u32; 2]);
pub struct Tail;

unsafe impl Piece for Tail {
type Owner = Pair;
type Item = u32;
const FIELD: &'static str = "tail";

unsafe fn project(owner: *mut Pair) -> *mut u32 {
unsafe { core::ptr::addr_of_mut!((*owner).0[1]) }
}
}

pub fn increment_tail(pair: &mut Pair) {
let value = unsafe { &mut *Tail::project(pair) };
*value = value.wrapping_add(1);
}

Loading