Express the source-tool read filter as a predicate

[shellygr]

Addresses @jtoman's review on #119. Same behavioural goal, expressed the way he asked for
rather than as a regex. #119 is left open for now; this branch is the replacement for its
composer/spec/util.py change.

Stacked on Certora/graphcore#29 — the graphcore submodule here is pinned to that
PR's head commit, which is not merged yet. Needs a re-pin to the merge commit before this
leaves draft.

Why

The rule the pipeline needs is "withhold these trees, but never withhold Solidity".
As a regex that is a lookahead guarding an alternation, plus (?:.*/)?d/.* for every
directory that can nest:

(?!.*\.sol\Z)(?:(?:.*/)?node_modules/.*|(?:.*/)?lib/.*|…)|(?:.*/)?\.certora_internal.*|…

graphcore's own type-alias comment already said why this is the wrong tool — "node_modules" in p.parts versus (?:.*/)?node_modules/.*.

Change

FS_FORBIDDEN_READ (a regex string) becomes fs_forbidden_read, a predicate over the
path, and the four rule classes get names instead of being inlined into one alternation:

	withheld	Solidity carve-out
_WITHHELD_WHOLE_DIRS	.git, .certora_internal, any depth	no
_REPORT_DIR_PREFIX	emv-*, root only	no
_NON_SOLIDITY_DIRS	node_modules, lib, test, dist, any depth	yes
generated files	.json / .map / .dat, *.min.js, *.bundle.js	yes

Withheld-whole is tested before the carve-out — that ordering is what makes prover
working directories the deliberate exception to "never withhold Solidity". Their .sol is
a verbatim copy of a contract already readable at its canonical path (each certoraRun
materializes another inputs/.certora_sources/**), and the analyzer reaches a specific
report's copy through a VFS scoped to that report.

The filter's type widens to GlobalExcludeArg everywhere it flows, so --forbidden-read
still takes a regex from the command line while the default is the predicate.

Testing

tests/test_fs_forbidden_read.py is carried over from #119 unchanged except for its
harness — it now calls the predicate instead of re.fullmatch. The assertions are the
behavioural spec, so 6/6 green is the evidence that dropping the regex changed nothing it
covered.

Measured against the source bundle of the dev run that motivated this:

	master	this PR
grep-visible files	914 (209.1 MB)	662 (9.5 MB)
visible .sol	597 / 597	597 / 597
longest visible line	4,802,095 B	6,406 B
the grep_files call that overflowed	2.53 MB	1.5 KB

Deliberate behaviour deltas vs master, beyond the intended ones:

• .gitignore becomes readable. The old (?:.*/)?\.git.* matched it by prefix; the
  predicate matches .git as an exact path component. Real .git content is still
  withheld here and by graphcore's floor.
• x_bundle.js becomes withheld (new generated-file rule); a hand-written bundle.js stays
  readable.

Also: 15 passed across test_fs_forbidden_read.py + test_design_doc_finder.py (the other
FS_FORBIDDEN_READ consumer), and pyright composer/ analyzer sanity_analyzer certora_autosetup is clean — 0 errors, with one pre-existing FormT warning in
composer/pipeline/core.py unchanged.

🤖 Generated with Claude Code

[jtoman]

worth computing this cartesian product ahead of time imo.

[shellygr]

Claude answers: done in 6f7e236. Built the six pairings once at import and let str.endswith take the tuple, which also collapses the helper to a single expression:

_BUNDLE_STEM_SUFFIXES = tuple(
    sep + marker for sep in (".", "-", "_") for marker in ("min", "bundle")
)
# ('.min', '.bundle', '-min', '-bundle', '_min', '_bundle')

def _is_generated_bundle(path: PurePath) -> bool:
    return path.suffix == ".js" and path.stem.endswith(_BUNDLE_STEM_SUFFIXES)

Tests unchanged and still green.