feat: v0.1.0 — Bazel ruleset for ordeal certificate-checked SMT gates - #2
Merged
Conversation
Mirrors rules_verus's architecture (post-PR #21 fixed shape):
- ordeal/extensions.bzl: bzlmod module extension; per-platform download
repos + a hub repo declaring real per-platform toolchain() rules, so
register_toolchains("@ordeal_toolchains//:all") registers all platforms
and native resolution picks the host's.
- ordeal/private/repo.bzl: repository rule fetching
ordeal-v{version}-{triple}.tar.gz from pulseengine/ordeal releases,
sha256-verified against the release's SHA256SUMS.txt (all four v0.16.1
hashes pinned and re-verified locally), macOS quarantine stripped.
- ordeal/toolchain.bzl: OrdealToolchainInfo provider + toolchain rule.
- ordeal/defs.bzl: ordeal_check (gates on the verdict TEXT `unsat`,
because `ordeal check` exits 0 for cleanly decided `sat` too; failures
surface the actual verdict/stdout/stderr) and ordeal_verus_check
(discharges Verus `by (bit_vector)` logs; exit code authoritative;
optional --cert-out into test undeclared outputs). `--cert-out` is
verus-mode only — `ordeal check` takes no flags, so ordeal_check has
no cert_out attribute.
- examples/: consumer module via local_path_override, the CI oracle:
//:smoke (unsat gate passes), //:sat_must_fail (proves a sat query
FAILS the gate with the expected message), //:verus_obligations
(real Verus log fixture from ordeal's test suite, cert_out).
Verified green with the real downloaded v0.16.1 binary on
aarch64-apple-darwin.
- .github/workflows/ci.yml: bazel build //... + examples bazel test //...
on ubuntu-latest and macos-latest.
- Minimal rivet setup (rivet validate: PASS) + generated AGENTS/CLAUDE.
Trace: skip
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Builds the rules_ordeal Bazel ruleset, mirroring rules_verus's architecture (post-#21 fixed per-platform toolchain() hub shape).
What's in
ordeal/extensions.bzl):_KNOWN_VERSIONSpins all four v0.16.1 sha256s from the release'sSHA256SUMS.txt(re-verified locally against freshly downloaded assets); hub repo declares real per-platformtoolchain()rules soregister_toolchains("@ordeal_toolchains//:all")just works.ordeal/private/repo.bzl): downloadsordeal-v{version}-{triple}.tar.gz, sha256-verifies, chmod +x, strips macOS quarantine.ordeal/defs.bzl):ordeal_checkgates on the verdict textunsat(verified:ordeal checkexits 0 for cleanly decidedsattoo), surfacing the actual verdict/stdout/stderr on failure.ordeal_verus_checkdischarges Verusby (bit_vector)logs (exit code authoritative there; optionalcert_outdrops LRAT certs into test undeclared outputs).--cert-outverified to be verus-mode only, soordeal_checkhas no such attribute.local_path_override— the CI oracle.//:smoke(unsat passes),//:sat_must_fail(proves a sat query FAILS the gate with the expected message),//:verus_obligations(real Verus log fixture from ordeal's test suite).bazel build //...+cd examples && bazel test //...on ubuntu + macos.rivet validate: PASS) + generated AGENTS/CLAUDE.Verified locally (aarch64-apple-darwin, real v0.16.1 binary)
Direct negative check:
bazel test //:sat_gatefails withexpected verdict 'unsat', got 'sat' (exit 0).🤖 Generated with Claude Code
https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1