Repository navigation
Open
Labels
choreRoutine maintenance with no behaviour changeRoutine maintenance with no behaviour changecicdCI/CD: workflows, actions, lockfiles, pins, runners, release gatesCI/CD: workflows, actions, lockfiles, pins, runners, release gatesgovernancePolicy, rulesets, standards, compliance, and their enforcementPolicy, rulesets, standards, compliance, and their enforcementlicensingLicences, SPDX headers, REUSE compliance, attributionLicences, SPDX headers, REUSE compliance, attribution
Description
Seven checks are red on every PR because of the state of main, not because of the PR's diff. They were measured on #228 (head abe7a34) and #229 (head bb82eeb). Four of them fail identically on main @ 8542e84.
| Check | Cause observed |
|---|---|
build (0.8.0) |
proven.ipkg builds 305/305, then idris2 --build tests.ipkg fails: tests/properties/SafeMathProps.idr references undefined names (safeNegate, safeAbs, detectOverflow, getValue, …) and has unelaboratable types (prop_addCommutative, prop_addIdentity, …) |
Aspect — Safety Invariants |
its grep finds the existing assert_total uses in src/ (about 20) |
Enforce Trustfile Policies |
"5 files have an SPDX header that is neither MPL-2.0 (code) nor CC-BY-SA-4.0 (docs)" |
scan / gitleaks |
also red on main @ 8542e84; not yet triaged |
governance / Workflow security linter |
also red on main; not yet triaged |
governance / Trusted-base reduction policy |
also red on main; not yet triaged |
governance / Validate Hypatia Baseline |
also red on main; not yet triaged |
Acceptance criteria
-
tests.ipkgbuilds: fixSafeMathPropsagainst the currentProven.SafeMathAPI, or remove the properties that test functions that no longer exist. - Each
assert_totalinsrc/is replaced with structural orsizeAccessiblerecursion, or the Aspect check whitelists it with a written justification. - The 5 SPDX headers are corrected. Relicensing is an owner decision.
- gitleaks, Workflow security linter, Trusted-base reduction policy and Hypatia Baseline are each triaged, then fixed or explicitly baselined.
- A PR that does not touch these areas is green on all seven.
Note: CodeRabbit's coding agent pushed commit 4f8d7fa ("replace assert_total with total recursion…, correct SPDX headers…") to the deleted-then-recreated branch fix/remove-false-runtime-assumptions. It is unreviewed, but may be a starting point.
Metadata
Metadata
Assignees
Labels
choreRoutine maintenance with no behaviour changeRoutine maintenance with no behaviour changecicdCI/CD: workflows, actions, lockfiles, pins, runners, release gatesCI/CD: workflows, actions, lockfiles, pins, runners, release gatesgovernancePolicy, rulesets, standards, compliance, and their enforcementPolicy, rulesets, standards, compliance, and their enforcementlicensingLicences, SPDX headers, REUSE compliance, attributionLicences, SPDX headers, REUSE compliance, attribution
Activity
hyperpolymath commentedon Oct 6, 2026
Triage (read-only, 2026-10-06; CI on #229 head bb82eeb, cross-checked against
main@ ced0ca5)Bottom line: 7 red checks, but only 3 underlying problems in this repo, plus 1 dead action pin and 1 bug in a shared standards script. No secret has leaked.
scan / gitleakssrc/Proven/SafeAPIKey/Proofs.idr:41,46(sk_live_abc123de…/sk_test_abc123de…, placeholder Stripe keys used indetectFormat … = StripeKeyproofs), andtests/unit/SafeJWTUnit.idr:37(the public jwt.io example token,sub 1234567890).gitleaksignoregovernance / Workflow security linterocaml/setup-ocaml@4462cc269f8d…in.github/workflows/ocaml-ci.yml:99,154. The API returns "No commit found for SHA"; reproduced locally withstandards/scripts/check-action-pins-resolve.sh(1 of 37). An unresolvableuses:means that job never runs.v3→93303b622b2522e4411e295f9e77411a24912ac7(resolved today), and updateactions.lockif presentAspect — Safety Invariantsassert_total/assert_smaller/believe_melines in 9src/files (SafeYAML/Parser ×6, SafeXML/Parser, SafeRegex/Matcher, SafeArgs/Parser, SafeTree, SafeTOML, and the SafeCORS, SafeJWT and SafeMathProofs)sizeAccessiblerecursion; 4f8d7fa (CodeRabbit agent, unreviewed) attempts thisgovernance / Trusted-base reduction policy.trusted-base-ignore, or enumerated indocs/proof-debt.adocTRUSTED:comment plus adocs/proof-debt.adocentry each, but the stopgap documents the debt rather than paying itEnforce Trustfile PoliciesSPDX-License-Identifier: Palimpsest-MPL-1.0(SafeYAML/Parser, SafeSQL/Builder, SafeRegex/Parser, SafeRegex/Matcher, SafeXML/Parser); the rest ofsrc/moved to MPL-2.0 in 0eb9709 (2026-05-22)MPL-2.0build (0.8.0)proven.ipkgbuilds 305/305.tests.ipkgthen fails with 13 errors intests/properties/SafeMathProps.idr: it callssafeAdd,safeSub,safeNegate,safeAbs,detectOverflowandgetValue, whichProven.SafeMathno longer exports. bdb1863 (2026-05-11, "align Safe* surface with idaptik #8") renamed them toaddChecked,subChecked,absSafe, … and the tests were not updatedgovernance / Validate Hypatia Baselineapply-baseline.sh: line 262: /usr/bin/jq: Argument list too long, exit 126.hyperpolymath/standardsscripts/apply-baseline.sh:187passes the whole findings file via--argjson findings "$FINDINGS_JSON", which overflows the per-argument limit (MAX_ARG_STRLEN, 128 KiB) once there are 298 findings--slurpfile/ stdin instead of--argjson. Then this repo must face 298 findings (critical=133, high=34, medium=107) against a 30-entry.hypatia-baseline.jsonSuggested order
proven.Horizon of this triage
tests.ipkgstops at its first failing module. The other 31 of its 32 modules are unobserved, so more breakage after SafeMathProps is likely; ci(antipattern): TS check reads .claude/CLAUDE.md exemption table #6's estimate assumes it.assert_totalcount comes fromgit greponmainexcluding--/|||comment lines, and matches the Aspect check's list. The Trusted-base count (30, of which 17 are undocumented) is the CI script's own figure.fix(SafeFiniteField): reject irreducibles not of degree n before redu…
chore(secrets): ignore three gitleaks test-fixture false positives (#231
docs: add AFFIRMATION.adoc anchored at 5360032 (#232)
docs: mark AFFIRMATION as agent-authored DRAFT, not owner-affirmed (#233