ci: make CI genuinely green — rust-ci toolchain pin#36
Merged
Conversation
Flagship semantic proof: totalCost (xs ++ ys) = totalCost xs + totalCost ys (conservation, by induction), plus a decidable WithinBudget proposition with sound+complete Dec, certifier soundness, and positive + negative controls (an over-budget ledger is provably rejected). Verified with idris2 0.7.0 (build clean, zero warnings) + adversarial rejection. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
Add Eclexiaiser.ABI.Invariants, a second, deeper machine-checked theorem distinct from the Layer-2 conservation (additivity) proof. Reuses the existing Semantics model (Ledger, totalCost, WithinBudget) without redefining datatypes, and proves the ordering structure of cost accounting: - prefixMonotone / costMonotoneAppend: appending work never decreases total cost (an LTE inequality, derived via additivity + lteAddRight) — not the Layer-2 equality. - budgetWeakening: budget compliance is downward-closed in the budget (WithinBudget b l -> LTE b b2 -> WithinBudget b2 l), via hand-proven LTE transitivity. - decBudgetLE: sound+complete decision for the ordering side condition. - Positive controls (concrete monotone step, prefix split, weakened witness) plus non-vacuity controls (Not on a false equality and on a false ordering), all machine-checked. Builds with exit 0 and zero warnings; adversarial false-statement checks are rejected by the type-checker. Registered last in the .ipkg. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
Add Eclexiaiser.ABI.FfiSeam proving the on-the-wire encoding resultToInt : Result -> Bits32 is sound: - resultRoundTrip: faithful/lossless — a decoder intToResult round-trips every Result through its C integer back to itself. - resultToIntInjective: distinct ABI outcomes never collide on the wire, DERIVED from the round-trip via a local justInj + cong/trans/sym. - Positive controls (concrete decodes = Refl) and two non-vacuity controls (distinct codes -> distinct ints, machine-checked). Genuine proof: no believe_me/postulate/assert_total/sorry. Builds with zero warnings; adversarial false claim (resultToInt Ok = resultToInt Error) is rejected by the checker. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
Introduce Eclexiaiser.ABI.Capstone: a single end-to-end ABI soundness certificate that composes the existing prior-layer proofs into one inhabited value. - ABISound record bundles three proven facts, one per layer: * flagship — Layer-2 budget-compliance witness (Semantics.withinEx) * invariant — Layer-3 monotonicity bound (Invariants.monotoneStepEx) * ffiSeam — Layer-4 seam injectivity (FfiSeam.resultToIntInjective) - abiContractDischarged : ABISound is built solely from those real exported witnesses; it typechecks iff all layers are sound together. Genuine composition only (no believe_me/postulate/etc.). An adversarial false certificate (bogus over-budget flagship witness) was confirmed to be rejected by the typechecker. Build is clean with 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
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. The Rust sources are already 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).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