chore(secrets): ignore three gitleaks test-fixture false positives by hyperpolymath · Pull Request #231 · hyperpolymath/proven

hyperpolymath · 2026-10-06T19:32:34Z

Summary

Adds a .gitleaksignore for the three test fixtures that turn scan / gitleaks red. None of them is a credential:

src/Proven/SafeAPIKey/Proofs.idr:41 and :46 are placeholder Stripe-prefixed strings with the body abc123def456. They exist only to prove that detectFormat returns StripeKey.
tests/unit/SafeJWTUnit.idr:37 is the public jwt.io example token (sub 1234567890, "John Doe"). It has been on main since 0863498 (2026-01-12).

Each entry is pinned by its exact file:rule:line fingerprint, so any new finding still fails, and so does a fixture that moves to another line. This is item 1 of the triage on #230.

Refs #230

Type of change

🐛 Bug fix: no, the scanner is behaving correctly; these are fixtures
✨ New feature: no
💥 Breaking change: no
🕳️ Soundness fix: no
📖 Documentation: no
🧹 Refactor / tech debt: no
⚡ Performance: no
🔧 Build / CI / tooling

📌 New pins

Head SHA: 60ff489

None. This PR changes no action uses:, actions.lock, lockfile or container digest.

How has this been verified?

I ran gitleaks 8.18.4, the version the reusable pins, exactly as secret-scanner-reusable.yml@571cc734 runs it: detect --source . --no-git --redact --config <estate-baseline.toml at 571cc734> --exit-code 1.

Run	Expected	Got
`main` (`a32c3b6`), no ignore file	rc=1, the 3 CI fingerprints	rc=1, the same 3
This branch	rc=0	rc=0
Planted control: a random real-format `sk_live_` key in a new file	rc=1	rc=1, `zz-planted.idr:stripe-access-token:1`
Planted control: `Proofs.idr` shifted down one line	rc=1	rc=1

The first draft of the file quoted the placeholder strings in a comment, and gitleaks flagged the ignore file itself (.gitleaksignore:stripe-access-token:8). The comment now describes the strings without quoting them.

Checklist

My commits are signed (git log --format=%G? → G).
I ran the project's own checks locally: the gitleaks scan above. No Idris source changed, so I did not rebuild.
New files carry the correct SPDX-License-Identifier: .gitleaksignore is config, so MPL-2.0. No existing file was relicensed.
Docs: no docs make claims about secret scanning, so none needed updating.
No soundness hole: no .idr file is touched.

Notes for reviewers

Pre-existing red checks, deferred to #230 (they are red on main and this PR does not touch them):

Enforce Trustfile Policies: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230 (licence headers, item 5)
governance / Trusted-base reduction policy: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230 (escape hatches, item 4)
governance / Workflow security linter: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230 (dead OCaml pin, item 2)
Aspect — Safety Invariants, build (0.8.0), governance / Validate Hypatia Baseline: deferred to CI: seven checks red on main independent of PR content (tests.ipkg, assert_total, SPDX, 4 governance/scan) #230 (items 3, 6, 7), if they finish red
GitGuardian also flagged the jwt.io token, at commit 4f8d7fa. That commit was pushed by coderabbitai[bot] to the leftover branch fix/remove-false-runtime-assumptions. Nothing needs rotating. The GitGuardian incident has to be dismissed as a test credential in the GitGuardian dashboard, because this file does not configure GitGuardian.
That leftover branch should be deleted; its PR, fix(soundness): remove false postulates in SafeFiniteField, SafePipe, SafeTerminal #228, already merged.
There are no required checks on main, so automerge is deliberately not armed, because it would merge instantly. This waits for a human merge.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HZc76cZKg5tUgduxXGLQkD

The gating scan flags placeholder Stripe-prefixed strings in SafeAPIKey/Proofs.idr (lines 41, 46) and the public jwt.io example token in tests/unit/SafeJWTUnit.idr (line 37). None is a credential. Pin each by file:rule:line fingerprint so any new finding, or a moved fixture, still fails the scan. Refs #230 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HZc76cZKg5tUgduxXGLQkD

coderabbitai · 2026-10-06T19:32:52Z

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: 1840f9e0-a4cb-4299-9b36-1e3bb9d790cb

📥 Commits

Reviewing files that changed from the base of the PR and between a32c3b6 and 60ff489.

📒 Files selected for processing (1)

.gitleaksignore

 __________________________________________________________________________________________________
< Estimate to avoid surprises. Estimate before you start. You'll spot potential problems up front. >
 --------------------------------------------------------------------------------------------------
  \
   \   (\__/)
       (•ㅅ•)
       / 　 づ

Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

_{Comment @coderabbitai help to get the list of available commands.}

sonarqubecloud · 2026-10-06T19:33:07Z

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

coderabbitai · 2026-10-06T19:45:02Z

Add Carrot credits or activate Agent usage billing to use Autopilot

## Summary Adds `AFFIRMATION.adoc`, the third file of the README / EXPLAINME / AFFIRMATION trio. It is a dated snapshot, open to refutation, of what proven can honestly claim at `main` **53600326**. It also lists what proven does **not** claim. - **Affirmed:** - `proven.ipkg` builds 305/305 modules in CI; - `proof-check (0.8.0)` passes; - there is no `believe_me` or `idris_crash` in code; - the false postulates are gone (#228, #229); - gitleaks is clean (#231). - **Not claimed:** - the README's "Mathematically proven" (PROOF-NEEDS samples about 3%); - the bodyless declarations that act as postulates; - 22 escape hatches; - the stubbed hash FFI; - `tests.ipkg` (it does not build); - about 79 unbuilt modules; - the weak or empty theorems; - the red checks on #230; - a pinned CI image. Where the README says more than this file, this file wins. Refs #230 ## Type of change - [ ] 🐛 Bug fix: no - [ ] ✨ New feature: no - [ ] 💥 Breaking change: no - [ ] 🕳️ Soundness fix: no - [x] 📖 Documentation - [ ] 🧹 Refactor / tech debt: no - [ ] ⚡ Performance: no - [ ] 🔧 Build / CI / tooling: no ## 📌 New pins Head SHA: **c25c3b5e302b9d66e1ae945ad47c72053c7d7234** None. This PR changes no action `uses:`, `actions.lock`, lockfile or container digest. ## How has this been verified? Every claim cites its evidence in the file: - **The build:** CI job `verify-idris-build` (id 112464109461) at 5360032 ends with `305/305: Building Proven`. - **The test build:** `idris2-ci.yml` at a32c3b6 gave proof-check success and build failure. The failure comes from the `tests.ipkg` renames in bdb1863. - **The escape-hatch counts:** `grep -rnw --include=*.idr <word> src`, with comment and doc-comment lines removed: - `believe_me` 0 (the 48 raw matches are all comments); - `idris_crash` 0; - `assert_total` 20; - `assert_smaller` 2. - **The hash stubs:** `Hash.idr` has 9 `%foreign` lines, all commented out. - **The recon figures** (383 bodyless, 79 unbuilt, 52 warnings, 71 `()` theorems) are labelled as measured at 8542e84 and not re-counted here. - **The 3%** is quoted from `PROOF-NEEDS.adoc` (1 of 32 sampled modules). - **Placeholder check:** the file contains no `{{`, `TODO: update`, `<PROJECT` or `example.com`. It has 103 substantive lines. ## Checklist - [x] My commits are **signed** (`git log --format=%G?` → `G`). - [x] I ran the project's own checks: no Idris source changed, so there was nothing to rebuild. The evidence is CI's at the anchor. - [x] New files carry the correct `SPDX-License-Identifier`: `CC-BY-SA-4.0`, as for the repo's other `.adoc` docs, with the attribution line from `.claude/CLAUDE.md`. - [x] Docs: this *is* the docs change. Correcting the README overclaim is item C4 of the follow-up and is not done here. - [x] No soundness hole: no `.idr` file is touched. ## Notes for reviewers - The anchor is the **parent** of this commit. A squash merge changes the commit SHA but keeps 5360032 as the parent, so the anchor stays valid only if nothing else lands on `main` first. If something does, rebase this branch and re-check the anchor row. **Pre-existing red checks** (red on `main` too; this PR does not touch them): - `governance / Workflow security linter`: deferred to #230 (dead OCaml pin) - `governance / Trusted-base reduction policy`: deferred to #230 (undocumented escape hatches) - `governance / Validate Hypatia Baseline`: deferred to #230 (`--argjson` crash in standards) - `Enforce Trustfile Policies`: deferred to #230 (Palimpsest licence headers) - `Aspect — Safety Invariants`: deferred to #230 - **Emerged, not yet on #230:** `GitHub Pages / build` is blocked by the action allowlist on `actions/upload-artifact@v4`. The `mirror-*` ×3 jobs have an empty host variable. Both are recorded in `dev-notes/inbox/findings.md`. - There are no required checks on `main`, so automerge is deliberately **not** armed. This waits for a human squash merge. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01HZc76cZKg5tUgduxXGLQkD Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

hyperpolymath merged commit 5360032 into main Oct 6, 2026
35 of 40 checks passed

hyperpolymath deleted the fix/gitleaks-fixture-ignores branch October 6, 2026 19:37

hyperpolymath mentioned this pull request Oct 7, 2026

docs: add AFFIRMATION.adoc anchored at 53600326 #232

Merged

6 of 13 tasks

Navigation Menu

Repository navigation

chore(secrets): ignore three gitleaks test-fixture false positives - #231

chore(secrets): ignore three gitleaks test-fixture false positives#231
hyperpolymath merged 1 commit into
mainfrom
fix/gitleaks-fixture-ignores

hyperpolymath commented Oct 6, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot commented Oct 6, 2026 •

edited by hyperpolymath

Loading

Uh oh!

sonarqubecloud Bot commented Oct 6, 2026

Uh oh!

Uh oh!

coderabbitai Bot commented Oct 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented Oct 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Type of change

📌 New pins

How has this been verified?

Checklist

Notes for reviewers

Uh oh!

coderabbitai Bot commented Oct 6, 2026 • edited by hyperpolymath Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sonarqubecloud Bot commented Oct 6, 2026

Quality Gate passed

Uh oh!

Uh oh!

coderabbitai Bot commented Oct 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

hyperpolymath commented Oct 6, 2026 •

edited

Loading

coderabbitai Bot commented Oct 6, 2026 •

edited by hyperpolymath

Loading