docs: seed docs/proof-debt.md for standards itself#213
Open
hyperpolymath wants to merge 1 commit into
Open
Conversation
Closes the self-referential loop: the trusted-base reduction policy (#203) and check-trusted-base CI script (#211) are published here, so standards itself must conform to its own schema. Enumerates the 11 undocumented Idris2 `partial` pragmas in a2ml/src/A2ML/Converters.idr and a2ml/src/A2ML/TypedCore.idr under §(d) DEBT. The remaining 4 markers (lol/proofs/theories/ information_theory.agda postulates and lol/src/abi/ partials) are already covered by the existing PROOF-NEEDS.md. These partial pragmas are not soundness breaks — they're Idris2 totality-checker waivers on mutually-recursive AST descents (Doc/Block/Section/Inline). Recommended disposition for each is either: - (a) discharge by fuel-indexed rewrite, OR - (b) re-classify as BUDGETED with a property test covering termination empirically. This file makes standards' own check-trusted-base CI gate pass (verified locally with the gate's script). Without it, every future PR to standards would fail CI once #211 lands. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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
docs/proof-debt.mdfor standards itself — the self-referential class.partialpragmas ina2ml/src/A2ML/Converters.idr+TypedCore.idrunder §(d) DEBT.PROOF-NEEDS.md.scripts/check-trusted-base.sh(feat(governance): add check-trusted-base CI enforcement #211) pass on standards itself — verified locally. Without this PR, every future PR to standards would fail the new CI gate once feat(governance): add check-trusted-base CI enforcement #211 merges.Companion
check-trusted-base.shCI gate (which this seed unblocks).Disposition notes
The 11
partialpragmas are NOT soundness breaks — they're Idris2 totality-checker waivers on mutually-recursiveDoc/Block/Section/InlineAST descents. Maintainer can triage each into §(a) discharge via fuel-indexed rewrite, or §(b) BUDGETED with a property test covering termination.🤖 Generated with Claude Code