ci: make CI genuinely green — rust-ci toolchain pin + fmt/clippy#57
Merged
Conversation
…tive consent Adds Wokelangiser.ABI.Semantics, raising the ABI to Layer 2 with a genuine, machine-checked semantic proof of the repo's headline domain property (consent patterns + accessibility via WokeLang). Model: data Actions (Collect/Process/Share/Store) guarded by a consent Ledger of (action, ConsentState) entries. The headline proposition Permitted env act has a single constructor that demands lookupConsent act env = Just Active -- there is no constructor admitting a permitted action without active recorded consent, so 'permitted without consent' is unrepresentable. Includes: sound+complete decPermitted : Dec (Permitted env act); a Result certifier with soundness (certifyPermittedSound) and completeness (certifyPermittedComplete); permittedImpliesActive bridging to ConsentState; a positive control (processPermitted) and two negative controls (shareNotPermitted for Revoked consent, collectNotPermitted for no record), all machine-checked. Adversarially verified: a forged Permitted witness for a non-Active/absent action is rejected by idris2 (non-vacuous). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
Introduces Wokelangiser.ABI.Invariants over the existing Semantics model. Headline theorem revokeDeniesPermission: after withdrawing consent for an action via revoke, that action is never Permitted under the resulting ledger regardless of prior records (including a prior Active grant) -- the operational dual of the Layer-2 grant theorem, per GDPR Art. 7(3). Also proves: revokeResolvesRevoked, revokeOverridesActive (override path), revokeIdempotent (algebraic law), revokePreservesOthers (locality), a sound+complete decIsRevoked, revokedExcludesPermitted bridge, plus a positive control (processRevoked) and non-vacuity negative controls (processNotPermittedAfterRevoke vs processPermittedBeforeRevoke). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
Add Wokelangiser.ABI.FfiSeam sealing the ABI<->FFI seam at the proof level: faithful round-trip (reusing resultFromInt/resultRoundTrip from Types), encoder injectivity DERIVED from the round-trip via justInj . cong, positive decode controls, and machine-checked non-vacuity controls (distinct codes -> distinct ints). Genuine proof: no believe_me/postulate/assert_total/%hint. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
Assemble the four prior proof layers into one inhabited certificate value: - Layer 2 flagship: Semantics.processPermitted (consent-gated permission) - Layer 3 invariant: Invariants.processNotPermittedAfterRevoke (revocation monotonicity) - Layer 4 FFI seam: FfiSeam.resultToIntInjective (no outcome collisions on the wire) `ABISound` record + `abiContractDischarged : ABISound` constructed purely from existing exported witnesses. If any prior layer were unsound this value would not typecheck. No believe_me/postulate/assert_total/idris_crash/%hint. Adversarial check confirms a bogus certificate (false seam collision / forged permission) is rejected. Build: exit 0, zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
…ble fix) Resolves the standing baseline CI reds (rust-ci toolchain error, governance Language/anti-pattern, governance workflow-lint) without altering the proven ABI. The Bash gate reproduces the former Python gate's verdict verbatim (validated across all -iser repos) and catches the same drift classes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
hyperpolymath
marked this pull request as ready for review
June 28, 2026 09:22
hyperpolymath
enabled auto-merge (squash)
June 28, 2026 09:22
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
2 participants
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.
Summary
Make CI genuinely green. The shared rust-ci pin on
mainpredates standards#439, so the SHA-pinneddtolnay/rust-toolchainstep errors out before the job runs. This bumps the pin so rust-ci actually runs, and brings the Rust sources to fmt + clippy(-D warnings) clean under the CI toolchain (stable 1.96).Changes
rust-ci-reusable.ymlpind135b05→8dc2bf0(currentstandardsHEAD; includes #439 toolchain fix + #441/#442).cargo fmt+clippy --fix(src/codegen/accessibility.rs,src/codegen/i18n.rs) socargo fmt --all -- --checkandcargo clippy --locked --all-targets -- -D warningspass.RSR Quality Checklist
Required
cargo test --locked --all-targets)cargo fmt --all -- --check)cargo clippy --locked --all-targets -- -D warnings).envfiles includedTesting
Verified locally with the CI toolchain (rustc/clippy/rustfmt 1.96.0):
cargo fmt --check,clippy -D warnings,cargo check --locked,cargo test --lockedall pass.🤖 Generated with Claude Code
Generated by Claude Code