| Filename | Latest commit message | Latest commit date |
|---|---|---|
3645849e2d
Some checks failed
standards workspaces build + test / aac-rs (pull_request) Successful in 43s
joule-code conformance gate / Build + round-trip C1-C4 vectors (pull_request) Failing after 1m2s
standards workspaces build + test / joule-code-rs (pull_request) Successful in 57s
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 2s
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 42s
standards workspaces build + test / map-rs (pull_request) Successful in 34s
standards workspaces build + test / mesh-rs (pull_request) Successful in 37s
standards workspaces build + test / eoc-rs (pull_request) Successful in 1m45s
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m13s
standards workspaces build + test / openpay (pull_request) Successful in 1m36s
standards workspaces build + test / proof-rs (pull_request) Successful in 1m9s
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m1s
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 2m33s
standards workspaces build + test / arl-rs (pull_request) Successful in 11m38s
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 9m26s
standards workspaces build + test / jouledesk-rs (pull_request) Successful in 8m27s
standards workspaces build + test / joulehook-rs (pull_request) Successful in 8m29s
standards workspaces build + test / sense-rs (pull_request) Successful in 8m14s
`real_ladder()` was `[Propositional, Z3Smt, SmallModel, FrontierModel]`. The
first two are real; the last two are stand-ins that gate on `GoalKind` and
whose "artifact" is a hash of the goal restated. `FrontierModel` has no gate at
all — it proves any goal unconditionally.
So on a machine without `z3`, every goal came back Proved: the real rungs
declined, the router escalated, and T3 obliged. The receipt claimed
`closed_by: BigModel`, `provenance: Estimator`, `total_uj: 50_513_884` — the
energy was as invented as the proof. `run_z3`'s own doc says a missing solver
is read "as escalate, never as proof", but escalation *was* proof.
This is the second instance of one bug. The first — a refutation escalated into
a proof — was fixed by halting the router on `Verdict::Refuted`. The remaining
hole was known: `formal_fix.rs` hand-built `[Propositional, Z3Smt]` to dodge it,
noting "the stubs would still claim proved there". That workaround is now the
library's behaviour instead of one call site's.
* `Solver::is_decision_procedure()` — does this rung's `Proved` mean a
verifier would accept the artifact? Defaults to **false**, so a newly
written stand-in is excluded from the real ladders automatically and a real
solver must claim to be checkable. Real: Propositional, Z3Smt, Z3Server,
LeanVerifier.
* `real_ladder` / `resident_z3_ladder` hold decision procedures only.
Exhausting them yields Unproved — the honest answer to "nothing here could
decide this". There is no T2/T3 rung because no real one exists yet; a
missing rung must never be papered over with a stand-in, which converts
"we could not decide" into "we decided".
* `real_t0_ladder` → `reference_ladder_with_real_t0`. A mixed ladder under a
`real_` name is the confusion that produced this bug.
* `ladder_is_sound` asserts the split structurally;
`ladder_never_fabricates_a_proof_when_a_rung_is_absent` drives the real
router, because the defect lived in the composition of router and ladder,
not in either alone. It uses a goal `z3` cannot parse, so it asserts the
same thing whether or not a solver is installed.
The conformance vector pack is byte-identical: it is generated from
`reference_ladder`, which is unchanged and stays total by design — that is what
makes routing vectors deterministic, and why it is a fixture and never evidence.
What this was costing: `joule-code-release`'s pipeline already printed
"z3 absent — postcondition honestly unproved, never faked" while the stand-in
faked it, and certified releases on the result. It now reports gate=red and
refuses. `formal_fix` no longer says "z3 found a counter-model" when z3 never ran.
394 tests pass across proof-rs, joule-code and joulecontract, with and without
`z3` on PATH. CI keeps installing z3 — not for correctness now, but so the real
T1 rung is exercised rather than skipped.
Co-Authored-By: Claude Opus 5 <[email protected]>
|
||
| .. | ||
| joule-code-cargo | ||
| joule-code-cascade | ||
| joule-code-collab | ||
| joule-code-conformance | ||
| joule-code-identity | ||
| joule-code-jcp | ||
| joule-code-joulecontract | ||
| joule-code-receipt | ||
| joule-code-release | ||
| joule-code-remediate | ||
| joule-code-review | ||
| joule-code-reviewer | ||
| joule-code-schema | ||
| joule-code-spec | ||
| joule-moq | ||
| jwp | ||
| lockstep-quic | ||