You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Owner decision, 2026-10-26: this change is agreed and queued for the next canon MAJOR. It is not to be cut on its own.
Change
Retire5.2.1 spark-ready ("Rust projects designed to admit SPARK/Ada modules") from 0-canon/rsr/rsr-criteria-v2.a2ml. It rests on the "Rust means Rust/SPARK" reading, which the proof-policy ruling of 2026-10-26 withdrew. Under 3-practice/PROOF-POLICY.adoc, Rust is verified with Creusot and SPARK belongs to Ada code.
Add a rhodium-tier creusot-ready criterion, gated on rust: the Rust code carries Creusot contracts for its load-bearing invariants (detect manual until a Hypatia rule exists).
Update the [weights-check].note headroom list, which names spark-ready.
Why it waits for a MAJOR
Under [versioning], removing a criterion is a MAJOR change (rule-major). A new rust-gated rhodium requirement is not additive-safe either, because it can make a conforming rust repo non-conforming at rhodium. That rules out a MINOR. canon.lock also needs two things for a MAJOR:
the 2.x criteria frozen under 0-canon/rsr/archive/;
the spine (rsr-template-repo) adopting the new hashes before the canon releases (Gate A).
That is too much ceremony for one rhodium criterion, so it rides the next era change.
Note on format
The criteria file is A2ML (legacy). If the 3.0.0 criteria have moved to a deed or k9 home by then, the new row goes there. Otherwise adding it needs explicit owner sign-off at that point.
Activity