Add ambiguity proof workflow for grammar verification

[TheLazyCat00]

Adds a workflow for ambiguity prove, the mode whose result carries no sentence-length bound. ambiguity-search.yml already covers the bounded search; the prover was reachable only by hand.

Not a pull request gate

"Not proven" is an expected, permanent possibility — unambiguity is undecidable, and the policy in docs/ambiguity.md explicitly allows tracked open obligations — so a required check on this would block merges for a verdict carrying no new information. The weekly run is the regression signal. Only a concrete ambiguous sentence fails the job, which is a real bug in the grammar.

The workflow

workflow_dispatch (ref, proof level K, concretization profile, timeout, strict) plus a Monday 04:00 UTC cron against the default branch. The env block is a verbatim copy of ambiguity-search.yml's, so both workflows take their memory, worker count and menhir path from the same configuration.

Two parameters are worth understanding before dispatching:

• Proof level K is precision, not effort. Stacks are abstracted to their top K states; cost grows exponentially in K while the chance of avoiding a spurious candidate grows with it. There is no K correct in general — 3 is what the README uses.
• Timeout bounds only the concretization search that runs after an abstract candidate. The abstract phase has no wall clock: it ends when the pair space is exhausted or the memory-derived pair limit is reached. The 60-minute job timeout is the real backstop for a level that turns out too high.

Reading the verdict

The verdict is read from the report text, not the exit status, and unrecognized output fails the job rather than passing it.

That is deliberate. ambiguity prove distinguishes four outcomes — proven, pair-limit overflow, an abstract candidate that would not concretize, and a concretized ambiguity — and at the time this branch was written the engine returned 0 for every one of them, including the last. A status-only check against such an engine reports a grammar with a found ambiguity as proven, which is the worst failure available here. The report text has always distinguished the outcomes, so that is what the verdict step reads.

#59 gives proof mode real exit statuses (0 proven, 1 ambiguous, 3 not proven, 2 a broken run). This branch is independent of it in either merge order: the run step treats the three verdict statuses as success and leaves the job result to the verdict step, so a "not proven" run does not fail the job, while the verdict logic keeps working against either engine. Once both have landed, the verdict script can be simplified to a case on $? — deliberately not done here, since it would be unsafe until #59 is in.

The job summary carries the verdict and its remediation, so a scheduled run is readable without opening the log. Reports upload as an artifact for 30 days.

Files

• .github/workflows/ambiguity-prove.yml
• .github/scripts/ambiguity-prove — runs the proof; env-driven with no arguments, because of the devbox run re-quoting hazard the sibling script documents
• .github/scripts/ambiguity-verdict — maps the report to a job result

Verification

The verdict script was exercised against fixtures reproducing the engine's exact output for all five paths (proven / overflow / unconcretized / concretized ambiguity / unrecognized), plus strict mode and a missing report; the runner's argument assembly was checked against a stub, including the empty-TOKENS branch and the missing-variable guards; and the real CLI accepts the exact argument list via --dry-run.

The workflow itself has not been dispatched — this session had no OCaml toolchain, since devbox installs nixpkgs from api.github.com and the sandbox egress policy blocks it. So the verdict the grammar actually produces, at which K, and how long the abstract phase takes are all unmeasured. Worth one manual dispatch before trusting the cron.

🤖 Generated with Claude Code

https://claude.ai/code/session_01N4KejxPN4Q9uQ67dHwUDgj

[coderabbitai]

Warning

Review limit reached

@TheLazyCat00, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 54 minutes

Limit details: You’ve used all 1 included review currently available under your plan.

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details

⚙️ Run configuration

Configuration used: Repository: zane-lang/coderabbit/.coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 94554bed-d94c-44e4-b19e-de7e55455cac

📥 Commits

Reviewing files that changed from the base of the PR and between 5d97d07 and 83341e4.

📒 Files selected for processing (3)

• .github/scripts/ambiguity-prove
• .github/scripts/ambiguity-verdict
• .github/workflows/ambiguity-prove.yml

---

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

• X
• Mastodon
• Reddit
• LinkedIn

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