File size: 2,848 Bytes
93c7565 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 | (* File: proofs/SafetyKernel.v
ProofBridge Liner — Formal Safety Kernel
-----------------------------------------
Structural formalisation of the circuit-breaker state machine in Coq.
The key theorem: UNAUTH actors can never reset a HALTED kernel.
This file can be compiled with: coqc proofs/SafetyKernel.v
*)
Require Import QArith.
(* ------------------------------------------------------------------ *)
(* Types *)
(* ------------------------------------------------------------------ *)
Inductive State := OPEN | HALTED.
Inductive Actor := AUTH | UNAUTH.
Record KernelInput := {
posterior : Q;
threshold : Q;
actor : Actor
}.
(* ------------------------------------------------------------------ *)
(* Transition Function *)
(* ------------------------------------------------------------------ *)
(** [step s i] computes the next state from current state [s] and
input [i]. The HALTED state is absorbing for UNAUTH actors. *)
Definition step (s : State) (i : KernelInput) : State :=
match s with
| OPEN =>
if Qle_bool i.(threshold) i.(posterior)
then HALTED
else OPEN
| HALTED =>
match i.(actor) with
| AUTH => OPEN
| UNAUTH => HALTED
end
end.
(* ------------------------------------------------------------------ *)
(* Theorems *)
(* ------------------------------------------------------------------ *)
(** Theorem 1 (Absorbing HALTED for UNAUTH):
An UNAUTH actor can never reset the circuit.
The HALTED state is absorbing when actor = UNAUTH. *)
Theorem unauthorized_halt_is_absorbing :
forall (i : KernelInput),
i.(actor) = UNAUTH ->
step HALTED i = HALTED.
Proof.
intros i H.
simpl.
rewrite H.
reflexivity.
Qed.
(** Theorem 2 (Monotone tripping):
If the posterior meets or exceeds the threshold,
the OPEN state transitions to HALTED. *)
Theorem posterior_above_threshold_trips :
forall (i : KernelInput),
Qle_bool i.(threshold) i.(posterior) = true ->
step OPEN i = HALTED.
Proof.
intros i H.
simpl.
rewrite H.
reflexivity.
Qed.
(** Theorem 3 (Safe below threshold):
If the posterior is strictly below the threshold, OPEN stays OPEN. *)
Theorem posterior_below_threshold_stays_open :
forall (i : KernelInput),
Qle_bool i.(threshold) i.(posterior) = false ->
step OPEN i = OPEN.
Proof.
intros i H.
simpl.
rewrite H.
reflexivity.
Qed.
(** Theorem 4 (AUTH can reset):
An AUTH actor always resets a HALTED kernel to OPEN. *)
Theorem auth_can_reset :
forall (i : KernelInput),
i.(actor) = AUTH ->
step HALTED i = OPEN.
Proof.
intros i H.
simpl.
rewrite H.
reflexivity.
Qed.
|