Skip to content

Revise unsafe Rust skill to V2 after V1 evaluation failures - #3522

Merged
joshlf merged 1 commit into
mainfrom
Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz
Sep 2, 2026
Merged

Revise unsafe Rust skill to V2 after V1 evaluation failures#3522
joshlf merged 1 commit into
mainfrom
Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz

Conversation

@joshlf

@joshlf joshlf commented Aug 3, 2026

Copy link
Copy Markdown
Member

Translate the V1 evaluation failures into general proof rules rather than
adding fixture-specific hazard trivia.

Require CONTRACT-BROKEN to have a valid UB-free falsifying execution. An
execution that contains UB may prove UNSOUND, but it cannot establish a defined
observation before or after the UB; without a separate UB-free witness, the
corresponding behavioral promise remains UNPROVED.

Require an explicit supported toolchain and configuration predicate, preserve
conflicting controlling policy sources, distinguish a conservative audit domain
from the project's unresolved support promise, and reject an earliest version,
CI sample, or convenient policy interpretation as proof of the whole domain.

Forbid promotion of one constructor, conversion, deserializer, or other
producer's precondition into a universal invariant of its output type. Require
an authoritative universal premise, enforced construction-and-preservation
closure, a verified theorem or explicit TCB premise, or a derivation specific
to the values actually consumed.

Strengthen literal-clause closure, full supported-domain composition, and
boundary and adversarial falsification before PROVED. Update the report
template and proof, configuration, API, and reporting references to carry the
same rules.

Agent-Authored-By: AI agent acting on Josh Liebow-Feeser's behalf


This PR is on branch codex/unsafe-rust-stack.

Latest Update: v11 — Compare vs v10

📚 Full Patch History

Links show the diff between the row version and the column version.

Version v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v11 v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v10 v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v9 v8 v7 v6 v5 v4 v3 v2 v1 Base
v8 v7 v6 v5 v4 v3 v2 v1 Base
v7 v6 v5 v4 v3 v2 v1 Base
v6 v5 v4 v3 v2 v1 Base
v5 v4 v3 v2 v1 Base
v4 v3 v2 v1 Base
v3 v2 v1 Base
v2 v1 Base
v1 Base
⬇️ Download this PR

Branch

git fetch origin refs/heads/Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz && git checkout -b pr-Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz FETCH_HEAD

Checkout

git fetch origin refs/heads/Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz && git checkout FETCH_HEAD

Cherry Pick

git fetch origin refs/heads/Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz && git cherry-pick FETCH_HEAD

Pull

git pull origin refs/heads/Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz

Stacked PRs enabled by GHerrit.

@codecov-commenter

codecov-commenter commented Aug 3, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 91.85%. Comparing base (1bfbbdf) to head (96bc345).

Additional details and impacted files
@@           Coverage Diff           @@
##             main    #3522   +/-   ##
=======================================
  Coverage   91.85%   91.85%           
=======================================
  Files          20       20           
  Lines        6093     6093           
=======================================
  Hits         5597     5597           
  Misses        496      496           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@joshlf
joshlf force-pushed the Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz branch from df5c1ef to cab951d Compare August 29, 2026 10:42
@joshlf
joshlf force-pushed the G3y45zv35fuuyeejc26bftqdd33lqz2oh branch from 5fa7e9e to 65a892d Compare August 29, 2026 11:11
@joshlf
joshlf force-pushed the Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz branch from cab951d to 20de26d Compare August 29, 2026 11:11
@joshlf
joshlf force-pushed the G3y45zv35fuuyeejc26bftqdd33lqz2oh branch from 65a892d to 792ff41 Compare September 1, 2026 22:15
@joshlf
joshlf force-pushed the Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz branch from 20de26d to 84438e4 Compare September 1, 2026 22:15
@joshlf
joshlf force-pushed the G3y45zv35fuuyeejc26bftqdd33lqz2oh branch from 405a8cb to c1b65d0 Compare September 2, 2026 21:51
@joshlf
joshlf force-pushed the Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz branch 2 times, most recently from 58f00bb to d0ce703 Compare September 2, 2026 22:28
@joshlf
joshlf force-pushed the G3y45zv35fuuyeejc26bftqdd33lqz2oh branch from c1b65d0 to 6c7a55f Compare September 2, 2026 22:28
Base automatically changed from G3y45zv35fuuyeejc26bftqdd33lqz2oh to main September 2, 2026 23:03
Translate the V1 evaluation failures into general proof rules rather than
adding fixture-specific hazard trivia.

Require CONTRACT-BROKEN to have a valid UB-free falsifying execution. An
execution that contains UB may prove UNSOUND, but it cannot establish a defined
observation before or after the UB; without a separate UB-free witness, the
corresponding behavioral promise remains UNPROVED.

Require an explicit supported toolchain and configuration predicate, preserve
conflicting controlling policy sources, distinguish a conservative audit domain
from the project's unresolved support promise, and reject an earliest version,
CI sample, or convenient policy interpretation as proof of the whole domain.

Forbid promotion of one constructor, conversion, deserializer, or other
producer's precondition into a universal invariant of its output type. Require
an authoritative universal premise, enforced construction-and-preservation
closure, a verified theorem or explicit TCB premise, or a derivation specific
to the values actually consumed.

Strengthen literal-clause closure, full supported-domain composition, and
boundary and adversarial falsification before PROVED. Update the report
template and proof, configuration, API, and reporting references to carry the
same rules.

gherrit-pr-id: Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz
Agent-Authored-By: AI agent acting on Josh Liebow-Feeser's behalf
@joshlf
joshlf force-pushed the Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz branch from d0ce703 to 96bc345 Compare September 2, 2026 23:04
@joshlf
joshlf enabled auto-merge September 2, 2026 23:05
@joshlf
joshlf added this pull request to the merge queue Sep 2, 2026
Merged via the queue into main with commit e51069e Sep 2, 2026
105 checks passed
@joshlf
joshlf deleted the Gxw7ewqzcrigbrgikdrjkmx2nnotda4uz branch September 2, 2026 23:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants