Skip to content

charon-ml, aeneas: declare GithubRepo provenance — both were UNSCANNED - #574

Merged
twitchyliquid64 merged 1 commit into
mainfrom
bryan/gitlab-provenance-backfill
Aug 10, 2026
Merged

charon-ml, aeneas: declare GithubRepo provenance — both were UNSCANNED#574
twitchyliquid64 merged 1 commit into
mainfrom
bryan/gitlab-provenance-backfill

Conversation

@bryan-minimal

@bryan-minimal bryan-minimal commented Aug 5, 2026

Copy link
Copy Markdown
Member

The nightly scan's second warning line — the one below the CPE-coverage line I've been chasing — reports:

35 package(s) emitted NO vuln query (no OSV ecosystem, no GitHub repo, not GnuProject/Sourceforge) — UNSCANNED, reported as 0 findings

That's a strictly worse class than "queried, found nothing": these were never asked. charon-ml and aeneas are on that list, and both have a plain GitHub upstream that simply was never declared.

package upstream license
charon-ml AeneasVerif/charon Apache-2.0 (confirmed via API)
aeneas AeneasVerif/aeneas Apache-2.0 (confirmed via API)

Both sources are gs://-mirrored, and Provenance::from_url deliberately declines gs:// — so nothing could infer these; they had to be declared.

Neither resolves any advisory today (OSV GIT query returns 0 for both repos, checked). That's the point — a queried zero is an answer, an unqueried zero is not. From here they ride the OSV GIT / GHSA path like every other GithubRepo package.

Verified with pkgmgr check-onboarding against this branch: 80 gaps → 78, and neither package appears in the output any more.


The other three couldn't be fixed, and the reason is the interesting part

menhir, visitors and unionfind are also on the unscanned list. All three are fpottier projects on gitlab.inria.fr, and each build.ncl header already says so:

"no Gitlab provenance category yet — minimal-supply-chain#347"

That category has since shipped on the tooling side (sc#347/#348 + pm#511): Provenance::Gitlab { host, owner, repo } exists in the Rust parser and scan.rs routes it. But the minimal stdlib contract never got it. From attr_classes.ncl in the stdlib actually in use, the accepted set is exactly:

'GithubRepo   'GnuProject   'Sourceforge   'Website

Declaring 'Gitlab under | Attrs fails the contract outright — and not gracefully. minimal dump aborts with failed to validate source_provenance and the whole package set fails to evaluate, not just that package. I hit exactly this and it silently turned a check-onboarding run into "0 packages evaluated successfully", which reads as a pass.

psmisc looks like a counter-example. It isn't.

psmisc ships category = 'Gitlab on main today — but its attrs block carries no | Attrs annotation, so it is never contract-checked. That's an accident rather than a pattern to copy, and it means we currently have one package whose provenance the contract has never validated.

So the pkgs half wasn't forgotten — it wasn't expressible

Raising the stdlib gap is a minimal-side decision, so this PR stops at the two packages that can land today rather than working around a contract. Flagging it here so the next person doesn't rediscover it the same way.

Remaining on the unscanned list after this: 33, including the X11 stack (libdrm, xorgproto, xtrans, xcb-proto, libxau, libx*, atk, at-spi2-core), ghc/ghc-bootstrap, and several vendor CLIs.

Summary by CodeRabbit

  • Chores
    • Added source repository metadata for Aeneas.
    • Added source repository metadata for Charon.

The nightly scan's second warning line (below the CPE-coverage one) reports:

    ⚠ 35 package(s) emitted NO vuln query (no OSV ecosystem, no GitHub repo,
      not GnuProject/Sourceforge) — UNSCANNED, reported as 0 findings

That is a strictly worse class than "queried, found nothing": these packages
were never asked. charon-ml and aeneas are on that list, and both have a plain
GitHub upstream that just was never declared.

  charon-ml → AeneasVerif/charon   (Apache-2.0, confirmed via API)
  aeneas    → AeneasVerif/aeneas   (Apache-2.0, confirmed via API)

Both sources are gs://-mirrored, and `Provenance::from_url` deliberately
declines gs:// — so nothing could infer these; they had to be declared.

Neither currently resolves any advisory (OSV GIT query returns 0 for both
repos, checked today), so this changes no finding today. That is the point: a
queried zero is an answer, an unqueried zero is not. From here they ride the
OSV GIT / GHSA path like every other GithubRepo package.

Verified with `pkgmgr check-onboarding` against this branch: 80 gaps -> 78, and
neither package appears in the output any more.

## The other three could NOT be fixed, and the reason matters

menhir, visitors and unionfind are also on the unscanned list. All three are
fpottier projects on gitlab.inria.fr, and each build.ncl header already says:

    "no `Gitlab` provenance category yet — minimal-supply-chain#347"

That category HAS since shipped on the tooling side (sc#347/#348 + pm#511):
`Provenance::Gitlab { host, owner, repo }` exists in the Rust parser and
scan.rs routes it. But the minimal STDLIB contract never got it. From the
stdlib in use (`attr_classes.ncl`), the accepted set is exactly:

    'GithubRepo   'GnuProject   'Sourceforge   'Website

Declaring 'Gitlab under `| Attrs` therefore fails the contract outright —
`minimal dump` aborts with "failed to validate source_provenance" and the WHOLE
package set fails to evaluate, not just that package.

psmisc appears to contradict this: it ships `category = 'Gitlab` on main today.
It does not — psmisc's attrs block carries NO `| Attrs` annotation, so it is
never contract-checked. That is an accident, not a pattern to copy, and it means
we currently have one package whose provenance the contract has never seen.

So the pkgs half of the GitLab provenance work was never merely forgotten — it
was not expressible. Raising the stdlib gap is a minimal-side decision, so this
PR stops at the two packages that can land today rather than working around a
contract.
@coderabbitai

coderabbitai Bot commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Review Change Stack

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: CHILL

Plan: Pro

Run ID: 94af3e2d-d1b3-40e4-9c88-4056b3d122c0

📥 Commits

Reviewing files that changed from the base of the PR and between 9b504de and 28fd79a.

📒 Files selected for processing (2)
  • packages/aeneas/build.ncl
  • packages/charon-ml/build.ncl

📝 Walkthrough

Walkthrough

The package declarations for Aeneas and Charon now include GitHub source provenance metadata. The metadata identifies each repository by source category, owner, and repository name.

Changes

Source provenance

Layer / File(s) Summary
Package source provenance metadata
packages/aeneas/build.ncl, packages/charon-ml/build.ncl
Added source_provenance declarations for the AeneasVerif/aeneas and AeneasVerif/charon GitHub repositories.

Estimated code review effort: 1 (Trivial) | ~5 minutes

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title clearly identifies both packages and the main change: declaring GitHub repository provenance to address their unscanned status.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.
✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch bryan/gitlab-provenance-backfill

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

@twitchyliquid64
twitchyliquid64 marked this pull request as ready for review August 10, 2026 22:05
@twitchyliquid64
twitchyliquid64 added this pull request to the merge queue Aug 10, 2026
Merged via the queue into main with commit b12c91c Aug 10, 2026
10 checks passed
@twitchyliquid64
twitchyliquid64 deleted the bryan/gitlab-provenance-backfill branch August 10, 2026 22:16
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.

2 participants