| Filename | Latest commit message | Latest commit date |
|---|---|---|
6b03da3883
Some checks failed
wai cross-architecture byte-equality / windows-x86_64 (pull_request) Successful in 27s
standards workspaces build + test / aac-rs (pull_request) Successful in 53s
joule-code conformance gate / Build + round-trip C1-C4 vectors (pull_request) Failing after 1m4s
standards workspaces build + test / joule-code-rs (pull_request) Successful in 50s
WAI conformance / cargo-class corpora · windows (pull_request) Successful in 1m18s
jouleclaw public surface must stay documented / Public-surface audit (jouleclaw-rs) (pull_request) Successful in 57s
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 3s
WAI conformance / cross-arch byte-equality · windows (pull_request) Successful in 22s
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 45s
standards workspaces build + test / map-rs (pull_request) Successful in 33s
standards workspaces build + test / mesh-rs (pull_request) Successful in 30s
standards workspaces build + test / eoc-rs (pull_request) Successful in 1m48s
standards workspaces build + test / openpay (pull_request) Successful in 1m30s
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m14s
wai cross-architecture byte-equality / linux-aarch64 (pull_request) Successful in 19s
WAI conformance / cargo-class corpora · linux-arm64 (pull_request) Successful in 38s
standards workspaces build + test / proof-rs (pull_request) Successful in 1m13s
WAI conformance / cross-arch byte-equality · linux-arm64 (pull_request) Successful in 19s
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m1s
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 2m34s
wai cross-architecture byte-equality / linux-x86_64 (pull_request) Successful in 16s
WAI conformance / cargo-class corpora · linux (pull_request) Successful in 30s
WAI conformance / cross-arch byte-equality · linux (pull_request) Successful in 13s
WAI neural decoders end-to-end / synthetic fixtures → Rust decode → reference (±4) (pull_request) Failing after 1m4s
standards workspaces build + test / arl-rs (pull_request) Successful in 16m0s
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 11m35s
standards workspaces build + test / jouledesk-rs (pull_request) Successful in 11m23s
standards workspaces build + test / joulehook-rs (pull_request) Successful in 11m3s
standards workspaces build + test / sense-rs (pull_request) Successful in 10m46s
wai cross-architecture byte-equality / macos-arm64 (reference) (pull_request) Successful in 35s
WAI conformance / cargo-class corpora · macos (pull_request) Successful in 1m48s
WAI conformance / cross-arch byte-equality · macos (pull_request) Successful in 39s
The first full matrix run surfaced a real defect, which this commit does NOT
fix — it only lets CI exercise the intended path.
`joulecontract-proof`'s `a_real_postcondition_discharges_through_z3` fails on a
runner because the image has no z3. The test is written to handle that: its
solver-absent branch asserts
// no solver present: the SMT rung returns Unproved, never a fake pass
assert!(matches!(entry.status, DischargeStatus::Unproved(_)));
and that assertion is what fails. Reproduced in the exact runner image
(catthehacker/ubuntu:act-22.04, arm64), the ladder returns:
status Proved · closed_by Some(BigModel) · provenance Estimator
attempts: Automation(false) → Smt(false) → SmallModel(false) → BigModel(TRUE)
`real_ladder()` is [Propositional, Z3Smt, SmallModel, FrontierModel]. The first
two are real; proof-solvers' own docs call the model rungs "honest stand-ins",
and FrontierModel returns `proved(goal)` unconditionally for its goal kind. So
with no solver installed, a stand-in closes the goal and reports Proved with 50 J
of estimated cost attached. The same module states the contract it breaks: "A
solver returns Proved only when a verifier would accept the artifact."
The test is right and the ladder does not honour it.
This is left unfixed on purpose. The stand-ins are load-bearing in proof-cascade
and proof-conformance, and proof-conformance ships a published vector pack —
changing whether a stand-in may close a goal would invalidate it. That is a
deliberate call for the proof standard's owner, not a side effect of a CI fix.
So: install z3 where it is needed, and record the defect where whoever picks it
up will find it. Both z3 jobs are pinned to Linux runners because the macOS
runner is a host executor with no apt; proof-rs moved from macos to linux for
that reason.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
|
||
| .. | ||
| workflows | ||