other

FINT

Lean spine source

Declarations: interrupt_separated_from_correction, interrupt_policy_invariant_from_correction_interface

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem interrupt_separated_from_correction :
    orseauNeutral interruptSeparationStep ∧
      ¬ channelPreserved interruptSeparationStep :=
  interrupt_neutral_not_channel_preserved

theorem interrupt_policy_invariant_from_correction_interface
    {State Corr Act : Type}
    (correctionState : InterruptBit → State → Corr)
    (choose : Corr → State → Act)
    (π : InterruptBit → State → Act)
    (hmed : CorrectionMediatedInterruptPolicy correctionState choose π)
    (hirrel : InterruptBitIrrelevantToCorrectionState correctionState) :
    InterruptInvariantPolicy π :=
  correction_mediated_policy_interrupt_invariant correctionState choose π hmed hirrel