docs(soundness): TRUSTED: annotate 5 code_safety scanner fixtures#352
Merged
hyperpolymath merged 1 commit intoMay 27, 2026
Merged
Conversation
Each of the 5 fixture files under `test/soundness/fixtures/code_safety/` contains a deliberate soundness escape hatch (Admitted / sorry / postulate / believe_me / unsafeCoerce) so that the corresponding hypatia rule can be regression-tested in `test/soundness_test.exs`. Per the trusted-base reduction policy (hyperpolymath/standards#203, schema in docs/TRUSTED-BASE-REDUCTION-POLICY.adoc), every escape hatch must either be documented in docs/proof-debt.md (covered by #343) OR carry an inline `TRUSTED:` / `AXIOM:` leading comment. This commit adds the inline `TRUSTED:` annotation immediately above each marker, naming the rule whose regression test acts as the refutation budget. Content-safe: the comment lines do not remove the trigger pattern, so soundness_test.exs continues to fire on each fixture (this is checked by the same test). Cluster: 5 sites — single PR per Step B of the proof-debt P1 cleanup template. Classification: PROPERTY-TEST (§(b) BUDGETED). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 27, 2026
…ktree shadows (#355) [standards#223](hyperpolymath/standards#223) merged 2026-05-27 09:16Z, adding path-fragment exemption support to `check-trusted-base.sh`. ## What Adds `.trusted-base-ignore` with two entries: | Pattern | Reason | |---|---| | `test/soundness/fixtures/` | 5 scanner test fixtures (admitted.v / sorry.lean / agda_postulate.agda / believe_me.idr / unsafe_coerce.hs) that exist solely to verify the detector fires | | `.claude/worktrees/` | local agent worktree shadows that double-count the canonical tree (cf. hypatia#343 §(d) refresh noting 10 such shadows) | ## Why no pin bump needed `governance-reusable.yml` (current main) fetches scripts from `standards/main` at run-time (`ref: main` on the inner self-checkout, per standards#219). Since standards#223 is now on main, the next CI run on this repo will pick up the new exemption behaviour without bumping any SHA pin in hypatia's wrapper. ## Cleanup of redundant artifacts (deferred) The 5 inline `TRUSTED:` comments added by #352 and the 5/10 §(d) enumeration entries added by #343 become **redundant** after this lands but are kept for now to avoid stomping on those in-flight PRs. Follow-up PR will remove them once #352 and #343 settle. ## Closes hypatia#354. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
deleted the
claude/trusted-annotations-soundness-fixtures-2026-05-27
branch
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
TRUSTED:leading comments to the 5 deliberate scanner fixtures undertest/soundness/fixtures/code_safety/(admitted.v, sorry.lean, agda_postulate.agda, believe_me.idr, unsafe_coerce.hs).test/soundness_test.exscan regression-test that the correspondingcode_safety/*rule fires. The soundness test suite IS the refutation budget.Why this is content-safe
The added comments live above the trigger line. The marker pattern (
Admitted.,sorry,postulate,believe_me,unsafeCoerce) is preserved verbatim.test/soundness_test.exsstill fires on every fixture (verified by the existing test suite).Test plan
mix test --only soundnesscontinues to pass (every fixture still triggers its rule at the expected severity).bash /path/to/standards/scripts/check-trusted-base.sh .reports the 5 canonical sites as satisfied via inline annotation (no longer needs docs/proof-debt.md substring match to pass).Related
docs/proof-debt.md(count-correction revision pushed in parallel).check-trusted-base.shCI enforcement.🤖 Generated with Claude Code