Skip to content

scratch: exercise the generated Rust proof gate on a runner (do not merge) - #231

Merged
hyperpolymath merged 1 commit into
mainfrom
proof-check-rust
Sep 24, 2026
Merged

hyperpolymath merged 1 commit into
mainfrom
proof-check-rust

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Throwaway PR. The tree on this branch is a project produced by main's own generator
(create-template.sh proofgateway -l rust), so .github/workflows/proof.yml executes exactly as
shipped.

Purpose: neither proof gate has ever run on a GitHub runner. This is that experiment. The branch
is closed and deleted once the run finishes.

Do not merge.

Scratch branch: the tree is a project produced by main's own generator, so
.github/workflows/proof.yml executes exactly as shipped. Not intended to merge.
@coderabbitai

coderabbitai Bot commented Sep 24, 2026 •

Copy link
Copy Markdown

Important

Review skipped

Too many files!

This PR contains 350 files, which is 250 over the limit of 100.

To get a review, reduce the PR to 100 files or fewer by splitting it into smaller PRs or changing its base branch.

Upgrade to a paid plan to raise the limit.

Usage-priced reviews support at most 300 files.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 39c61029-2c96-489b-99d1-76946ca9105f

📥 Commits

Reviewing files that changed from the base of the PR and between b5535f1 and 6dddd93.

⛔ Files ignored due to path filters (5)
  • .github/workflows/actions.lock is excluded by !**/*.lock
  • aletheia/Cargo.lock is excluded by !**/*.lock
  • aletheia/extraction/rhodibot/Cargo.lock is excluded by !**/*.lock
  • aletheia/extraction/rhodium-pipeline/Cargo.lock is excluded by !**/*.lock
  • aletheia/templates/common/.github/workflows/actions.lock is excluded by !**/*.lock
📒 Files selected for processing (350)
  • .claude/CLAUDE.md
  • .editorconfig
  • .gitattributes
  • .github/CODEOWNERS
  • .github/CONTRIBUTING.md
  • .github/FUNDING.yml
  • .github/copilot/coding-agent.yml
  • .github/dependabot.yml
  • .github/funding.yml
  • .github/hooks/validate-a2ml.sh
  • .github/hooks/validate-k9.sh
  • .github/label-classifier.json
  • .github/labels.json
  • .github/scripts/classify-issue.jq
  • .github/workflows/boj-build.yml
  • .github/workflows/casket-pages.yml
  • .github/workflows/changelog.yml
  • .github/workflows/ci.yml
  • .github/workflows/codeql.yml
  • .github/workflows/dogfood-gate.yml
  • .github/workflows/governance.yml
  • .github/workflows/hypatia-scan.yml
  • .github/workflows/instant-sync.yml
  • .github/workflows/label-triage.yml
  • .github/workflows/labels.yml
  • .github/workflows/mirror.yml
  • .github/workflows/pages.yml
  • .github/workflows/proof.yml
  • .github/workflows/push-email-notify.yml
  • .github/workflows/rust-ci.yml
  • .github/workflows/scorecard.yml
  • .github/workflows/secret-scanner.yml
  • .gitignore
  • .gitmodules
  • .hypatia-ignore
  • .hypatia/activity.jsonl
  • .hypatia/last-visit.json
  • .machine_readable/6a2/0-AI-MANIFEST.a2ml
  • .machine_readable/6a2/AGENTIC.a2ml
  • .machine_readable/6a2/ECOSYSTEM.a2ml
  • .machine_readable/6a2/META.a2ml
  • .machine_readable/6a2/NEUROSYM.a2ml
  • .machine_readable/6a2/PLAYBOOK.a2ml
  • .machine_readable/6a2/README.adoc
  • .machine_readable/6a2/STATE.a2ml
  • .machine_readable/6a2/anchor/0-AI-MANIFEST.a2ml
  • .machine_readable/6a2/anchor/ANCHOR.a2ml
  • .machine_readable/6a2/anchor/README.adoc
  • .machine_readable/CLADE.a2ml
  • .machine_readable/bot_directives/README.adoc
  • .machine_readable/bot_directives/coverage.a2ml
  • .machine_readable/bot_directives/debt.a2ml
  • .machine_readable/bot_directives/git-private-farm.a2ml
  • .machine_readable/bot_directives/gitbot-fleet.a2ml
  • .machine_readable/bot_directives/hypatia.a2ml
  • .machine_readable/bot_directives/methodology.a2ml
  • .machine_readable/contractiles/Adjustfile.a2ml
  • .machine_readable/contractiles/Bustfile.a2ml
  • .machine_readable/contractiles/Dustfile.a2ml
  • .machine_readable/contractiles/Intentfile.a2ml
  • .machine_readable/contractiles/Justfile
  • .machine_readable/contractiles/Mustfile.a2ml
  • .machine_readable/contractiles/Trustfile.a2ml
  • .machine_readable/integrations/feedback-o-tron.a2ml
  • .machine_readable/integrations/proven.a2ml
  • .machine_readable/integrations/verisimdb.a2ml
  • .machine_readable/integrations/vexometer.a2ml
  • .machine_readable/rsr-profile.a2ml
  • .machine_readable/self-validating/README.adoc
  • .machine_readable/self-validating/examples/ci-config.k9.ncl
  • .machine_readable/self-validating/examples/project-metadata.k9.ncl
  • .machine_readable/self-validating/examples/setup-repo.k9.ncl
  • .machine_readable/self-validating/template-hunt.k9.ncl
  • .machine_readable/self-validating/template-kennel.k9.ncl
  • .machine_readable/self-validating/template-yard.k9.ncl
  • .machine_readable/svc/README.adoc
  • .tool-versions
  • .well-known/ai.txt
  • .well-known/ai.txt
  • .well-known/humans.txt
  • .well-known/humans.txt
  • .well-known/security.txt
  • .well-known/security.txt
  • 0-AI-MANIFEST.a2ml
  • ARCHITECTURE.adoc
  • CHANGELOG.adoc
  • CHANGELOG.md
  • CODE_OF_CONDUCT.adoc
  • CONTRIBUTING.adoc
  • Cargo.toml
  • DELIVERY-186-197.md
  • EXPLAINME-new.adoc
  • EXPLAINME.adoc
  • GLOSSARY.adoc
  • GOVERNANCE.adoc
  • Justfile
  • LICENSE
  • LICENSES/AGPL-3.0-or-later.txt
  • MAINTAINERS
  • MAINTAINERS.adoc
  • Mustfile
  • NOTICE
  • PROOF-NEEDS.adoc
  • QUICKSTART-DEV.adoc
  • QUICKSTART-MAINTAINER.adoc
  • QUICKSTART-USER.adoc
  • README.adoc
  • ROADMAP.adoc
  • SECURITY.adoc
  • TEST-NEEDS.adoc
  • TOPOLOGY.adoc
  • absolute-zero
  • aletheia/.claude/CLAUDE.md
  • aletheia/.clippy.toml
  • aletheia/.clusterfuzzlite/Containerfile
  • aletheia/.clusterfuzzlite/build.sh
  • aletheia/.clusterfuzzlite/project.yaml
  • aletheia/.dockerignore
  • aletheia/.editorconfig
  • aletheia/.gitattributes
  • aletheia/.github/FUNDING.yml
  • aletheia/.github/ISSUE_TEMPLATE/bug_report.md
  • aletheia/.github/ISSUE_TEMPLATE/custom.md
  • aletheia/.github/ISSUE_TEMPLATE/documentation.md
  • aletheia/.github/ISSUE_TEMPLATE/feature_request.md
  • aletheia/.github/ISSUE_TEMPLATE/question.md
  • aletheia/.github/dependabot.yml
  • aletheia/.github/workflows/README.md
  • aletheia/.github/workflows/aletheia.yml
  • aletheia/.github/workflows/cflite_batch.yml
  • aletheia/.github/workflows/cflite_pr.yml
  • aletheia/.github/workflows/codeql.yml
  • aletheia/.github/workflows/generator-generic-ossf-slsa3-publish.yml
  • aletheia/.github/workflows/ghcr-publish.yml
  • aletheia/.github/workflows/governance.yml
  • aletheia/.github/workflows/hypatia-scan.yml
  • aletheia/.github/workflows/instant-sync.yml
  • aletheia/.github/workflows/jekyll-gh-pages.yml
  • aletheia/.github/workflows/mirror.yml
  • aletheia/.github/workflows/publish-container.yml
  • aletheia/.github/workflows/rust-ci.yml
  • aletheia/.github/workflows/scorecard-enforcer.yml
  • aletheia/.github/workflows/scorecard.yml
  • aletheia/.github/workflows/secret-scanner.yml
  • aletheia/.gitignore
  • aletheia/.gitlab-ci.yml
  • aletheia/.machine_readable/6a2/AGENTIC.a2ml
  • aletheia/.machine_readable/6a2/ECOSYSTEM.a2ml
  • aletheia/.machine_readable/6a2/META.a2ml
  • aletheia/.machine_readable/6a2/NEUROSYM.a2ml
  • aletheia/.machine_readable/6a2/PLAYBOOK.a2ml
  • aletheia/.machine_readable/6a2/STATE.a2ml
  • aletheia/.nojekyll
  • aletheia/.rustfmt.toml
  • aletheia/.well-known/ai.txt
  • aletheia/.well-known/humans.txt
  • aletheia/.well-known/security.txt
  • aletheia/ABI-FFI-README.adoc
  • aletheia/ALETHEIA-HANDOVER.adoc
  • aletheia/CHANGELOG.adoc
  • aletheia/CLAUDE.md
  • aletheia/CODE_OF_CONDUCT.adoc
  • aletheia/CONTRIBUTING.adoc
  • aletheia/CROSSREPO-HANDOVER.adoc
  • aletheia/Cargo.toml
  • aletheia/Containerfile
  • aletheia/FINAL_SUMMARY.adoc
  • aletheia/HANDOVER.scm
  • aletheia/Justfile
  • aletheia/LICENSE
  • aletheia/LICENSES/CC-BY-SA-4.0.txt
  • aletheia/LICENSES/PMPL-1.0-or-later.txt
  • aletheia/MAINTAINERS.adoc
  • aletheia/Mustfile
  • aletheia/PALIMPSEST.adoc
  • aletheia/PROJECT_STATUS.adoc
  • aletheia/QUICK_REFERENCE.adoc
  • aletheia/README.adoc
  • aletheia/ROADMAP.adoc
  • aletheia/RSR-CONFORMITY.adoc
  • aletheia/RSR_OUTLINE.adoc
  • aletheia/SECURITY.adoc
  • aletheia/benches/verification_benchmark.rs
  • aletheia/conformance/ECHIDNA-CONFORMANCE.adoc
  • aletheia/conformance/OIKOS-CONFORMANCE.adoc
  • aletheia/conformance/PALIMPSEST-CONFORMANCE.adoc
  • aletheia/conformance/README.adoc
  • aletheia/conformance/RSR-CONFORMANCE.adoc
  • aletheia/contractiles/README.adoc
  • aletheia/contractiles/dust/Dustfile
  • aletheia/contractiles/must/Mustfile
  • aletheia/docs/ARCHITECTURE.adoc
  • aletheia/docs/BADGES.adoc
  • aletheia/docs/CITATIONS.adoc
  • aletheia/docs/DEPLOYMENT.adoc
  • aletheia/docs/FAQ.adoc
  • aletheia/docs/MIGRATION-GUIDE.adoc
  • aletheia/docs/PRIORITIES.adoc
  • aletheia/docs/QUICK_START.adoc
  • aletheia/docs/RSR-SPECIFICATION.adoc
  • aletheia/docs/SILVER-LEVEL.adoc
  • aletheia/docs/VALUE-CHAIN-POLICY.adoc
  • aletheia/eclexiaiser.toml
  • aletheia/examples/simple_verification.rs
  • aletheia/examples/web-project-deno.json
  • aletheia/extraction/rhodibot/.github/workflows/ci.yml
  • aletheia/extraction/rhodibot/.gitlab-ci.yml
  • aletheia/extraction/rhodibot/.well-known/ai.txt
  • aletheia/extraction/rhodibot/.well-known/humans.txt
  • aletheia/extraction/rhodibot/.well-known/security.txt
  • aletheia/extraction/rhodibot/Cargo.toml
  • aletheia/extraction/rhodibot/Justfile
  • aletheia/extraction/rhodibot/README.adoc
  • aletheia/extraction/rhodibot/docs/VALUE-CHAIN-POLICY.adoc
  • aletheia/extraction/rhodibot/manifest.scm
  • aletheia/extraction/rhodibot/src/bot.rs
  • aletheia/extraction/rhodibot/src/lib.rs
  • aletheia/extraction/rhodibot/src/main.rs
  • aletheia/extraction/rhodibot/tests/integration_tests.rs
  • aletheia/extraction/rhodium-pipeline/Cargo.toml
  • aletheia/extraction/rhodium-pipeline/README.adoc
  • aletheia/extraction/rhodium-pipeline/docs/VALUE-CHAIN-POLICY.adoc
  • aletheia/extraction/rhodium-pipeline/src/lib.rs
  • aletheia/extraction/rhodium-pipeline/src/main.rs
  • aletheia/ffi/zig/build.zig
  • aletheia/ffi/zig/src/main.zig
  • aletheia/ffi/zig/test/integration_test.zig
  • aletheia/fuzz/Cargo.toml
  • aletheia/fuzz/fuzz_targets/fuzz_input.rs
  • aletheia/manifest.scm
  • aletheia/rust-toolchain.toml
  • aletheia/scripts/create-template.sh
  • aletheia/scripts/install.sh
  • aletheia/src/checks.rs
  • aletheia/src/config.rs
  • aletheia/src/main.rs
  • aletheia/src/output.rs
  • aletheia/src/types.rs
  • aletheia/templates/ada/.editorconfig
  • aletheia/templates/ada/.github/workflows/ci.yml
  • aletheia/templates/ada/.github/workflows/proof.yml
  • aletheia/templates/ada/.gitignore
  • aletheia/templates/ada/.machine_readable/rsr-profile.a2ml
  • aletheia/templates/ada/.tool-versions
  • aletheia/templates/ada/@@MOD_NAME@@.gpr
  • aletheia/templates/ada/Justfile
  • aletheia/templates/ada/README.adoc
  • aletheia/templates/ada/src/@@MOD_NAME@@.adb
  • aletheia/templates/ada/src/@@MOD_NAME@@.ads
  • aletheia/templates/ada/src/main.adb
  • aletheia/templates/ada/tests/run_tests.adb
  • aletheia/templates/ada/tests/tests.gpr
  • aletheia/templates/agda/.editorconfig
  • aletheia/templates/agda/.github/workflows/ci.yml
  • aletheia/templates/agda/.gitignore
  • aletheia/templates/agda/.machine_readable/rsr-profile.a2ml
  • aletheia/templates/agda/.tool-versions
  • aletheia/templates/agda/@@PROJECT_NAME@@.agda-lib
  • aletheia/templates/agda/Justfile
  • aletheia/templates/agda/README.adoc
  • aletheia/templates/agda/src/@@MOD_CAMEL@@.agda
  • aletheia/templates/agda/src/Properties.agda
  • aletheia/templates/common/.gitattributes
  • aletheia/templates/common/.github/workflows/governance.yml
  • aletheia/templates/common/.github/workflows/hypatia-scan.yml
  • aletheia/templates/common/.well-known/ai.txt
  • aletheia/templates/common/.well-known/humans.txt
  • aletheia/templates/common/.well-known/security.txt
  • aletheia/templates/common/0-AI-MANIFEST.a2ml
  • aletheia/templates/common/CHANGELOG.adoc
  • aletheia/templates/common/CODE_OF_CONDUCT.adoc
  • aletheia/templates/common/CONTRIBUTING.adoc
  • aletheia/templates/common/LICENSE
  • aletheia/templates/common/LICENSES/CC-BY-SA-4.0.txt
  • aletheia/templates/common/LICENSES/MPL-2.0.txt
  • aletheia/templates/common/MAINTAINERS.adoc
  • aletheia/templates/common/SECURITY.adoc
  • aletheia/templates/elixir/.editorconfig
  • aletheia/templates/elixir/.formatter.exs
  • aletheia/templates/elixir/.github/workflows/ci.yml
  • aletheia/templates/elixir/.gitignore
  • aletheia/templates/elixir/.machine_readable/rsr-profile.a2ml
  • aletheia/templates/elixir/.tool-versions
  • aletheia/templates/elixir/Justfile
  • aletheia/templates/elixir/README.adoc
  • aletheia/templates/elixir/lib/@@MOD_NAME@@.ex
  • aletheia/templates/elixir/lib/@@MOD_NAME@@/cli.ex
  • aletheia/templates/elixir/mix.exs
  • aletheia/templates/elixir/test/@@MOD_NAME@@_test.exs
  • aletheia/templates/elixir/test/test_helper.exs
  • aletheia/templates/haskell/.editorconfig
  • aletheia/templates/haskell/.github/workflows/ci.yml
  • aletheia/templates/haskell/.gitignore
  • aletheia/templates/haskell/.machine_readable/rsr-profile.a2ml
  • aletheia/templates/haskell/.tool-versions
  • aletheia/templates/haskell/@@PROJECT_NAME@@.cabal
  • aletheia/templates/haskell/Justfile
  • aletheia/templates/haskell/README.adoc
  • aletheia/templates/haskell/app/Main.hs
  • aletheia/templates/haskell/cabal.project
  • aletheia/templates/haskell/src/Core.hs
  • aletheia/templates/haskell/test/Main.hs
  • aletheia/templates/rust/.editorconfig
  • aletheia/templates/rust/.gitignore
  • aletheia/templates/rust/.machine_readable/rsr-profile.a2ml
  • aletheia/templates/rust/.tool-versions
  • aletheia/templates/rust/Justfile
  • aletheia/templates/rust/README.adoc
  • aletheia/templates/zig/.editorconfig
  • aletheia/templates/zig/.github/workflows/ci.yml
  • aletheia/templates/zig/.gitignore
  • aletheia/templates/zig/.machine_readable/rsr-profile.a2ml
  • aletheia/templates/zig/.tool-versions
  • aletheia/templates/zig/Justfile
  • aletheia/templates/zig/README.adoc
  • aletheia/templates/zig/build.zig
  • aletheia/templates/zig/src/main.zig
  • aletheia/templates/zig/src/root.zig
  • aletheia/templates/zig/test/integration_test.zig
  • aletheia/tests/integration_tests.rs
  • contractile.just
  • docs/STATE-OF-PLAY-2026-07-29.adoc
  • docs/architecture.adoc
  • docs/contributing.adoc
  • docs/decisions/0001-template.adoc
  • docs/proof-debt.adoc
  • docs/tech-debt-2026-05-26.adoc
  • docs/troubleshooting.adoc
  • docs/usage.adoc
  • llm-warmup-dev.adoc
  • llm-warmup-user.adoc
  • manifest.scm
  • mise.toml
  • setup.sh
  • src/impl.rs
  • src/lib.rs
  • src/main.rs
  • stapeln.toml
  • tests/aspect/security_test.rs
  • tests/e2e/brainfuck_e2e_test.rs
  • tests/fuzz/placeholder.txt
  • tests/integration_test.rs
  • tests/property_test.rs
  • verification/Cargo.toml
  • verification/README.adoc
  • verification/src/lib.rs
  • verification/why3find.json
  • www/.well-known/ai.txt
  • www/.well-known/humans.txt
  • www/.well-known/security.txt

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.


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.

@hyperpolymath
hyperpolymath marked this pull request as ready for review September 24, 2026 02:19
@hyperpolymath
hyperpolymath merged commit 5014068 into main Sep 24, 2026
18 of 21 checks passed
@hyperpolymath
hyperpolymath deleted the proof-check-rust branch September 24, 2026 02:19
hyperpolymath pushed a commit that referenced this pull request Sep 24, 2026
PR #231 was a proof exercise, not a change to the framework. Its tree was a
generator-produced Rust project, pushed only so that the generated
.github/workflows/proof.yml would resolve at the repository root and could be
executed on a GitHub runner. It was opened as a draft and was never meant to be
merged; it was squash-merged as 5014068, which replaced the entire repository
tree with that scaffold.

This commit restores the tree of b5535f1 exactly, so main is again the framework
plus the fixes that came before the exercise. Nothing from 5014068 is kept.
@hyperpolymath

Copy link
Copy Markdown
Owner Author

This PR was a proof exercise, not a change to the framework: its tree was a generator-produced Rust project, pushed so that the generated .github/workflows/proof.yml would resolve at the repository root and could be executed on a GitHub runner. It was opened as a draft and was not meant to be merged.

It was squash-merged ~100 s after the run went green, replacing the entire repository tree. That is reverted in 859b387, whose tree is identical to b5535f1. main's history keeps the accident and its correction on purpose.

Result of the exercise, now recorded in DELIVERY-186-197.md: Proof (Creusot) run 35946679306 finished green with Proved (2 files).

The route that does not risk this: both gates ship a workflow_dispatch: trigger, so a scratch branch can be exercised with POST /repos/{owner}/{repo}/actions/workflows/proof.yml/dispatches and no PR at all — which is how the Ada run (35947307833, 35/35 checks) was started.

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.

1 participant