Skip to content

docs: seed docs/proof-debt.md index per trusted-base policy#37

Closed
hyperpolymath wants to merge 1 commit into
mainfrom
claude/seed-proof-debt-2026-05-26
Closed

docs: seed docs/proof-debt.md index per trusted-base policy#37
hyperpolymath wants to merge 1 commit into
mainfrom
claude/seed-proof-debt-2026-05-26

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

What this PR does NOT do

Migrate the substantive content out of PROOF-NEEDS.md. That file remains canonical; this file just makes the schema-conformant filename exist for the check-trusted-base.sh CI gate.

🤖 Generated with Claude Code

Per the trusted-base reduction policy (hyperpolymath/standards#203),
adds a schema-conformant index at docs/proof-debt.md that references
PROOF-NEEDS.md as the source of truth.

This repo already has substantive proof-debt documentation in
PROOF-NEEDS.md — this PR doesn't duplicate that content, just adds the
schema bridge so the check-trusted-base CI gate (standards#211) finds
docs/proof-debt.md at the canonical filename and recognises this repo
as documented.

Marker count detected by check-trusted-base.sh: 3.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath enabled auto-merge (squash) May 26, 2026 16:52
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 55 issues detected

Severity Count
🔴 Critical 9
🟠 High 18
🟡 Medium 28

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Merge artifact in root",
    "type": "stale",
    "file": "SPEC.core.scm.orig",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No permissions declaration -- add permissions: read-all",
    "type": "missing_permissions",
    "file": "comprehensive-quality.yml",
    "action": "add_permissions",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/main.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/probability.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/ternary.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/test/probability_test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/test/ternary_test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/examples/uncertainty.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "Atom creation from untrusted input may exhaust atom table (1 occurrences, CWE-400)",
    "type": "erlang_atom_from_untrusted",
    "file": "/home/runner/work/betlang/betlang/lsp/bet-lsp/build/packages/thoas/src/thoas_decode.erl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath
Copy link
Copy Markdown
Owner Author

Superseded by #39, which corrects the marker count (3 → 1) and substantively classifies substTop_preserves_typing as §(c) NECESSARY AXIOM per the standards#203 schema.

auto-merge was automatically disabled May 27, 2026 07:45

Pull request was closed

hyperpolymath added a commit that referenced this pull request May 27, 2026
…39)

## Summary

Replaces the thin index in
[#37](#37) with a
substantive classification under the
[standards#203](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc)
trusted-base reduction policy schema.

**Corrects the marker count** (#37 said "3 escape hatches"; actual is
**1**). Classifies the single hatch:

- **(a) DISCHARGED**: none
- **(b) BUDGETED**: none
- **(c) NECESSARY AXIOM**: `proofs/BetLang.lean:392`
`substTop_preserves_typing` — classical substitution lemma over de
Bruijn substitution. Cited from Pierce TAPL Ch. 6 + Software Foundations
Vol 2 + Programming Language Foundations in Agda. Promotion path
documented per [PR
#27](#27).
- **(d) DEBT**: none

The repo has **zero `sorry`** declarations. The author's in-file framing
at `BetLang.lean:387-391` already distinguishes this as an explicit
axiom rather than a proof hole; the (c) classification formalises that
disposition under the estate-wide policy schema.

## Why supersede #37

PR #37's index says "3 escape hatches" (wrong — only 1 axiom), and
defers all classification to a stub `PROOF-NEEDS.md` pointer without
actually doing the work. This PR does the substantive classification per
the policy schema.

After this PR merges,
[#37](#37) should be closed
as superseded.

## Format choice

`.adoc` per estate-wide convention ("All docs must be `.adoc` except
GitHub-required files" — standards CLAUDE.md). The policy itself allows
`.md` or `.adoc`.

## Test plan

- [x] AsciiDoc renders on GitHub
- [x] GPG-signed commit (key `4A03639C…2867091E`, noreply email)
- [x] Auto-merge SQUASH enabled
- [ ] CI baseline-rot (Test on Racket 8.11/8.12/current, Code Quality,
governance/Workflow-security-linter, governance/Language-anti-pattern)
is pre-existing on `main` — same failures present on `#37` and on
`main`'s latest commit `6702d2d`. Not introduced by this PR.

🤖 Generated with [Claude Code](https://claude.com/claude-code)
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.

1 participant