ci: make CI genuinely green — rust-ci toolchain pin (#39)

* abi: prove OneForOne restart invariant (Layer 2 semantic proof)

Add Otpiser.ABI.Semantics: a faithful Idris2 model of a one-for-one OTP
supervisor (children keyed by id, each Running/Failed) and a restart step,
with machine-checked proofs of the headline fault-tolerance invariant:

  - restartPreservesChildSet: restarting any child leaves the ordered set
    of supervised child ids unchanged (real propositional equality).
  - restartLeavesOthersUntouched: every sibling whose id differs from the
    target survives the restart byte-for-byte identical (Elem soundness).
  - restartHeadRuns / RestartedRunning: the targeted child is set Running.

Positive controls exhibit concrete witnesses over a 3-worker supervisor;
the negative control (negativeSiblingNotReset) refutes, by machine, the
OneForAll-style claim that a failed sibling is reset — establishing the
property is non-vacuous. No believe_me / postulate / assert_total.

Registered in otpiser-abi.ipkg; ABI builds clean with zero warnings.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* abi: add Layer-3 rest-for-one invariants (idempotence + prefix-untouched)

Add Otpiser.ABI.Invariants, a second machine-checked theorem distinct from
and deeper than the Layer-2 one-for-one flagship. Reuses the Semantics model
(Child/ChildStatus/Supervisor) and reasons about the rest_for_one transition:

  T1 IDEMPOTENCE (algebraic law): restForOne target . restForOne target
     = restForOne target  -- a genuine fixpoint, proven via a triggered-branch
     lemma; not a restatement of "siblings untouched".
  T2 child-id-set preservation across the rest-for-one transition.
  T3 prefix-untouched: children strictly before the target survive identically
     (the directional core of rest-for-one), via a BeforeTarget certificate.
  T4 sound+complete Dec (decIsTargetHead) + certifier.

Five positive controls (concrete witnesses incl. Refl-checked transition shape
and idempotence) and three negative/non-vacuity controls (Not-Elem refutation,
decision refutation, not-the-identity). No believe_me/postulate/assert_total;
%default total; SPDX MPL-2.0. Registered last in otpiser-abi.ipkg. Clean build
(0 warnings); adversarial false-equality check rejected.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* Add Layer 4 FfiSeam proof sealing the ABI<->FFI seam

Prove the FFI result-code/enum encoding is sound: distinct ABI outcomes
never collide on the C wire (injectivity) and the wire integer faithfully
round-trips back to the ABI value (lossless decode).

- intToResult decoder + resultRoundTrip (Refl per constructor)
- resultToIntInjective derived from the round-trip (justInjective + cong)
- same treatment for SupervisorStrategy (reuses Types.strategyRoundTrip)
  and ChildRestartType (new decoder + round-trip)
- positive controls (concrete decodes = Refl) and negative/non-vacuity
  controls (distinct codes have distinct wire ints, machine-checked)

Genuine total proofs: no believe_me/postulate/assert_total/etc.
%default total; zero build warnings.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* Add Layer-5 capstone: end-to-end ABI soundness certificate

Assemble the existing per-layer proofs into one inhabited value
`abiContractDischarged : ABISound`, tying manifest semantics ->
ABI proofs (flagship one-for-one + rest-for-one idempotence) ->
FFI seam injectivity into a single end-to-end soundness statement.

Fields reuse only already-exported witnesses/theorems:
- Layer 2 (Semantics): positiveTargetRunning, positiveSiblingUntouched
- Layer 3 (Invariants): restForOneIdempotent
- Layer 4 (FfiSeam): resultToIntInjective

The value typechecks iff every prior layer is sound. An adversarial
false certificate (bogus sibling witness) is rejected by the type
checker, confirming non-vacuity. No believe_me/postulate/assert_total.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* ci: make CI green — bump rust-ci to standards@8dc2bf0 (toolchain: stable 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

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/rust-ci.yml

@@ -14,4 +14,4 @@ permissions:
 
 jobs:
   rust-ci:
-    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236
+    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@8dc2bf039d1ff0372d650895c46bea7fbaec68ff