diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 810184a..90e84bd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -85,6 +85,50 @@ jobs: name: compile-commands path: build/compile_commands.json + # ── TLA+ formal verification (TLC model checking) ──────────────────────────── + # Independent of the C++ build (tla/*.tla model the safety-relevant state + # machines rcp/lifecycle.hpp and rcp/e2e.hpp implement, not the C++ code + # itself), so this job carries no `needs:` on build-and-test, matching + # c-RCP's own identically-named formal-verification job. Each spec's + # like-named .cfg file in tla/ supplies TLC's CONSTANTS/SPECIFICATION/ + # INVARIANTS/PROPERTIES — TLC loads it automatically when invoked without + # -config (see FORMAL_VERIFICATION.md). TLC itself exits non-zero on any + # invariant/property violation or deadlock, so a plain `java -jar ...` per + # spec is already a real pass/fail gate — no output-scraping needed. + formal-verification: + name: formal verification (TLC model checking) + runs-on: ubuntu-22.04 + steps: + - uses: actions/checkout@v4 + + - uses: actions/setup-java@v4 + with: + distribution: temurin + java-version: '21' + + - name: Download TLC (tla2tools.jar) + run: curl -sSL -o "$RUNNER_TEMP/tla2tools.jar" https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar + + - name: Model-check WatchdogSafeState.tla + working-directory: tla + run: java -jar "$RUNNER_TEMP/tla2tools.jar" -workers 4 WatchdogSafeState.tla + + - name: Model-check RxSequenceGuard.tla + working-directory: tla + run: java -jar "$RUNNER_TEMP/tla2tools.jar" -workers 4 RxSequenceGuard.tla + + - name: Model-check CrcSafeStateLatch.tla + working-directory: tla + run: java -jar "$RUNNER_TEMP/tla2tools.jar" -workers 4 CrcSafeStateLatch.tla + + - name: Model-check LifecycleStateMachine.tla + working-directory: tla + run: java -jar "$RUNNER_TEMP/tla2tools.jar" -workers 4 LifecycleStateMachine.tla + + - name: Model-check E2ESafePoint.tla + working-directory: tla + run: java -jar "$RUNNER_TEMP/tla2tools.jar" -workers 4 E2ESafePoint.tla + # ── rcp/l2.hpp real-socket round trip (Linux, needs CAP_NET_RAW/root) ──────── # Exercises rcp::l2::Server/Client over a real veth pair — real AF_PACKET # sockets, a real Linux network interface pair, real Ethernet frames. This diff --git a/tla/E2ESafePoint.cfg b/tla/E2ESafePoint.cfg new file mode 100644 index 0000000..ea0720b --- /dev/null +++ b/tla/E2ESafePoint.cfg @@ -0,0 +1,17 @@ +\* TLC model-checking configuration for E2ESafePoint.tla. +CONSTANTS + s1 = s1 + s2 = s2 + Streams = {s1, s2} + SafestateEnabled = {s1} + WatchdogEnabled = {s1, s2} + +SPECIFICATION FairSpec + +INVARIANTS + TypeOK + +PROPERTIES + SafetyRequestsSurvivePurge + NoUnsafeSafetyExecution + EventuallySafetyExecutes diff --git a/tla/E2ESafePoint.tla b/tla/E2ESafePoint.tla new file mode 100644 index 0000000..050ead3 --- /dev/null +++ b/tla/E2ESafePoint.tla @@ -0,0 +1,215 @@ +---- MODULE E2ESafePoint ---- +(* + * Formal specification of the per-request-stream watchdog and safety-tagged- + * request execution gate rcp::e2e.hpp provides (rcp::e2e::RxWatchdog, + * apply_watchdog_overflow(), endpoint_in_configured_safe_state(), + * may_execute_now()). + * + * Ported from c-RCP's tla/E2ESafePoint.tla (Phase 7, cpp-RCP issue #129) + * against these same primitives, confirmed by direct comparison against + * c-RCP's rcp_e2e_wd_evaluate()/rcp_e2e_watchdog_purge_should_keep()/ + * rcp_e2e_endpoint_in_safe_state() (src/e2e.c) during this port to be + * behaviorally identical for the two properties this spec establishes: a + * watchdog-overflow purge never discards a pending safety-tagged request, + * and a safety-tagged request only ever executes once its endpoint has + * reached its configured safe state. rcp/e2e.hpp additionally exposes + * apply_queue_overflow() (a request-queue-overrun trigger, distinct from + * watchdog expiry, gated on rx_ovrflw_safestate_enable) that this spec does + * not separately model, matching c-RCP's own spec's scope -- both triggers + * share the identical purge-normal/retain-safety consequence Miss(s) below + * already captures once its own safe-state-enable input is set, so a second, + * differently-named copy of the identical action would add no new coverage. + * + * This models one request stream's rx_wd_enable/rx_wd_timeout_interval/ + * rx_wd_safestate_enable watchdog (RxWatchdog::overflowed(), + * apply_watchdog_overflow()), its pending-request queue split into a + * safety-tagged and a normal component (request::RequestRecord::is_safety, + * request::RequestLedger::cancel_all(non_safestate_only)), and the + * safety-tagged execution admission rule (may_execute_now()) against a + * polled endpoint_in_safe_state measurement + * (endpoint_in_configured_safe_state()). CRC32 well-formedness itself + * (wrap()/unwrap()) is a pure per-frame computation with no interesting + * state-transition behavior to model checking, and is covered by + * tests/test_e2e.cpp instead -- same scope split as the c-RCP original. + * The watchdog's own timeout-vs-latch mechanics (kick()/overflowed()'s own + * elapsed-time behavior) are separately covered by tla/WatchdogSafeState.tla + * -- this spec's own Kick/Miss actions below model only the timing- + * independent, purge-relevant consequence of an overflow, abstracting away + * the elapsed-time comparison WatchdogSafeState.tla already verifies in + * full, so the two specs are complementary, not duplicates. + * + * Safety property (SP1): a watchdog-overflow purge with + * rx_wd_safestate_enable set never discards a pending safety-tagged + * request -- only normal-tagged requests are purged. + * Safety property (SP2): a safety-tagged request only ever transitions + * from pending to executed while its endpoint reports it has reached + * the configured safe state. + * + * Liveness property (LP1): a safety-tagged request that becomes pending + * eventually executes, given per-stream fair scheduling of ExecuteSafety and + * an endpoint safe-state signal that eventually settles and stays true. The + * naive stronger wording -- "a pending safety-tagged request is eventually + * either executed or purged, never stuck pending forever" -- is false by + * construction against this spec's own SP1 above: Miss(s) (the only purge + * event) never touches safety_pending by design, so "purged" is never a + * live alternative for a safety-tagged request, and a property requiring + * "executed or purged" is unprovable as stated (TLC finds a trivial + * submit-and-never-purge counterexample). LP1 below is the corrected, + * narrower claim this spec can actually make and TLC confirms holds. TLC's + * default no-successor-state deadlock check passes (every state in the + * model has at least one enabled successor). LP1 is a related but strictly + * stronger claim: per-stream progress/livelock-freedom under fairness, not + * mere deadlock-freedom. The fairness-minimality result (WF suffices, SF + * buys nothing extra) was re-confirmed against real TLC runs during this + * port and carries over unchanged from c-RCP's own original derivation -- + * the underlying action structure is unchanged. + *) + +EXTENDS TLC + +CONSTANTS Streams, \* set of request-stream identifiers + SafestateEnabled, \* streams with rx_wd_safestate_enable set + WatchdogEnabled \* streams with rx_wd_enable set + +ASSUME SafestateEnabled \subseteq Streams +ASSUME WatchdogEnabled \subseteq Streams + +VARIABLES overflowed, \* Stream -> BOOLEAN: RxWatchdog::overflowed() verdict + endpoint_in_safe_state, \* Stream -> BOOLEAN: polled safe-state measurement + \* (endpoint_in_configured_safe_state()) + safety_pending, \* Stream -> BOOLEAN: a safety-tagged request is queued + normal_pending \* Stream -> BOOLEAN: a normal-tagged request is queued + +vars == <> + +TypeOK == + /\ overflowed \in [Streams -> BOOLEAN] + /\ endpoint_in_safe_state \in [Streams -> BOOLEAN] + /\ safety_pending \in [Streams -> BOOLEAN] + /\ normal_pending \in [Streams -> BOOLEAN] + +Init == + /\ overflowed = [s \in Streams |-> FALSE] + /\ endpoint_in_safe_state \in [Streams -> BOOLEAN] + /\ safety_pending = [s \in Streams |-> FALSE] + /\ normal_pending = [s \in Streams |-> FALSE] + +(* RxWatchdog::kick()-equivalent: resets a stream's elapsed-since-last-kick + * clock, clearing any overflow verdict. *) +Kick(s) == + /\ overflowed' = [overflowed EXCEPT ![s] = FALSE] + /\ UNCHANGED <> + +(* RxWatchdog::overflowed() reporting TRUE once elapsed exceeds + * rx_wd_timeout_interval -- only possible while the watchdog is enabled for + * this stream (a disabled watchdog never overflows, RxWatchdog::overflowed()'s + * own !cfg.rx_wd_enable guard). When rx_wd_safestate_enable is also set, + * this is exactly apply_watchdog_overflow()'s own purge event: every + * pending normal-tagged request is discarded + * (request::RequestLedger::cancel_all(/*non_safestate_only=*/true)), but a + * pending safety-tagged request survives untouched. *) +Miss(s) == + /\ s \in WatchdogEnabled + /\ overflowed[s] = FALSE + /\ overflowed' = [overflowed EXCEPT ![s] = TRUE] + /\ IF s \in SafestateEnabled + THEN normal_pending' = [normal_pending EXCEPT ![s] = FALSE] + ELSE UNCHANGED normal_pending + /\ UNCHANGED <> + +(* A caller submits a safety-tagged (RequestRecord::is_safety, wire 0x8x) + * request; may_execute_now() only ever governs *execution*, not admission + * into the queue, so submission itself is unconditional. *) +SubmitSafety(s) == + /\ safety_pending' = [safety_pending EXCEPT ![s] = TRUE] + /\ UNCHANGED <> + +SubmitNormal(s) == + /\ normal_pending' = [normal_pending EXCEPT ![s] = TRUE] + /\ UNCHANGED <> + +(* may_execute_now(): a safety-tagged request executes only once the + * endpoint reports it has reached its configured safe state + * (endpoint_in_configured_safe_state()). *) +ExecuteSafety(s) == + /\ safety_pending[s] + /\ endpoint_in_safe_state[s] + /\ safety_pending' = [safety_pending EXCEPT ![s] = FALSE] + /\ UNCHANGED <> + +(* A non-safety-tagged request is never gated by endpoint_in_safe_state + * (may_execute_now()'s own !rec.is_safety short-circuit). *) +ExecuteNormal(s) == + /\ normal_pending[s] + /\ normal_pending' = [normal_pending EXCEPT ![s] = FALSE] + /\ UNCHANGED <> + +(* endpoint_in_configured_safe_state()'s own polled measurement changing -- + * e.g. the ForceHighImpedance strategy's external boolean flipping, or the + * RunSafeSequencer strategy's tracked sequencer state reaching (or leaving) + * cfg.rx_safe_sequencer_state as the physical endpoint moves. *) +ObserveSafeState(s) == + /\ endpoint_in_safe_state' \in [Streams -> BOOLEAN] + /\ UNCHANGED <> + +Next == + \E s \in Streams : + \/ Kick(s) + \/ Miss(s) + \/ SubmitSafety(s) + \/ SubmitNormal(s) + \/ ExecuteSafety(s) + \/ ExecuteNormal(s) + \/ ObserveSafeState(s) + +Spec == Init /\ [][Next]_<> + +(* FairSpec adds weak fairness, per stream, on ExecuteSafety(s) -- and only + * weak fairness. Re-confirmed against real TLC runs during this port: + * nothing in this spec can clear safety_pending[s] except ExecuteSafety(s) + * itself (Miss(s) leaves it untouched by SP1), so once safety_pending[s] + * holds and endpoint_in_safe_state[s] holds continuously, ExecuteSafety(s) + * stays continuously enabled until it is taken -- exactly the condition WF + * acts on. Strong fairness buys nothing extra here; TLC confirms a WF-only + * variant already suffices once LP1's antecedent below holds. *) +FairSpec == Spec /\ (\A s \in Streams : WF_vars(ExecuteSafety(s))) + +(* LP1's antecedent, per stream: the endpoint's polled safe-state signal + * eventually settles and stays TRUE. Without this, ObserveSafeState + * (deliberately left unfair, matching its role as an unconstrained polled + * environment measurement) could keep flipping endpoint_in_safe_state[s] + * forever, which would repeatedly disable ExecuteSafety(s) right as it + * becomes enabled -- WF only acts on an action that is *continuously* + * enabled, and TLC confirms dropping this antecedent produces exactly that + * flapping-endpoint counterexample. *) +EndpointEventuallyStable(s) == <>[](endpoint_in_safe_state[s]) + +(* LP1: for every stream, given its endpoint signal eventually settling true + * and fair (WF) scheduling of that stream's ExecuteSafety, a safety-tagged + * request that becomes pending on that stream eventually executes. *) +EventuallySafetyExecutes == + \A s \in Streams : + EndpointEventuallyStable(s) => [](safety_pending[s] => <>~safety_pending[s]) + +(* SP1: a watchdog-overflow purge (safestate-enabled Miss) never clears a + * pending safety-tagged request -- only Miss can purge, and Miss leaves + * safety_pending entirely unchanged by construction; this property confirms + * that guarantee holds for every reachable step, not just by inspection of + * the action definition. *) +SafetyRequestsSurvivePurge == + [][\A s \in Streams : + (overflowed[s] = FALSE /\ overflowed'[s] = TRUE /\ s \in SafestateEnabled /\ safety_pending[s]) + => safety_pending'[s]]_<> + +(* SP2: a safety-tagged request only ever transitions from pending to + * not-pending while its endpoint was reporting safe state -- i.e. the only + * way safety_pending[s] goes TRUE -> FALSE is ExecuteSafety(s), whose own + * guard requires endpoint_in_safe_state[s]. *) +NoUnsafeSafetyExecution == + [][\A s \in Streams : + (safety_pending[s] /\ ~safety_pending'[s]) => endpoint_in_safe_state[s]]_<> + +THEOREM Spec => TypeOK /\ SafetyRequestsSurvivePurge /\ NoUnsafeSafetyExecution +THEOREM FairSpec => EventuallySafetyExecutes + +==== diff --git a/tla/LifecycleStateMachine.cfg b/tla/LifecycleStateMachine.cfg new file mode 100644 index 0000000..9e9f280 --- /dev/null +++ b/tla/LifecycleStateMachine.cfg @@ -0,0 +1,10 @@ +\* TLC model-checking configuration for LifecycleStateMachine.tla. +SPECIFICATION FairSpec + +INVARIANTS + TypeOK + +PROPERTIES + NoSkipConfiguration + FieldLockMonotonicWhileConfigured + EventuallyRcpConfigured diff --git a/tla/LifecycleStateMachine.tla b/tla/LifecycleStateMachine.tla new file mode 100644 index 0000000..85c50eb --- /dev/null +++ b/tla/LifecycleStateMachine.tla @@ -0,0 +1,229 @@ +---- MODULE LifecycleStateMachine ---- +(* + * Formal specification of rcp::lifecycle::ServerLifecycle (rcp/lifecycle.hpp), + * the 3-state HW_UNCONFIGURED / HW_CONFIGURED / RCP_CONFIGURED progression an + * OPEN Alliance TC18 Remote Control Protocol Specification v0.5.1_RC server + * advances through as it gets configured, plus the plausibility checks and + * register-locking behavior tied to that progression. + * + * Ported from c-RCP's tla/LifecycleStateMachine.tla (Phase 7, cpp-RCP issue + * #129) against ServerLifecycle::transition()/check_hw_cfg()/check_rcp_cfg() + * — confirmed, by direct comparison against c-RCP's rcp_lifecycle_transition() + * (src/lifecycle.c) during this port, to be a field-for-field match: same + * from/target state pairs, same plausibility guards, same writer- + * authorization structure. This spec deliberately abstracts writer + * authorization and idleness-gating out of scope, same as the c-RCP original + * it is ported from — every promote/demote action below is modelled as + * enabled whenever its plausibility guard passes, without a `writer`/ + * `all_other_eps_idle` input, since neither this spec's safety properties + * (state/field-lock shape) nor its liveness property depend on who initiated + * a transition or whether other endpoints were idle at the time. See "Known + * abstraction gap" below for what this simplification leaves out of scope, + * and rcp/lifecycle.hpp's own ServerLifecycle::transition() doc comment for + * the full writer/idle-gated topology this spec does not model in full. + * + * ServerLifecycle also exposes a second, simpler entry point — advance()/ + * deconfigure() — predating transition() and kept alongside it for its own + * existing callers (see ServerLifecycle's class doc comment, "Why advance() + * and transition() both exist"). advance()'s forward steps and + * transition()'s guarded promotions enforce the identical hw_cfg/rcp_cfg + * plausibility gates on the identical state pairs, so PromoteToHwConfigured/ + * PromoteToRcpConfigured below model both entry points at once; this spec + * does not separately model advance()'s "repeat of the current state is + * invalid_transition" rule, since it manifests no differently, from this + * spec's own state/field-lock/liveness properties' point of view, than + * transition()'s "repeat of the current state is a no-op" rule — both leave + * every variable this spec tracks unchanged. + * + * Known abstraction gap (present already in c-RCP's own spec, not introduced + * by this port): transition() additionally supports a partial demotion, + * RcpConfigured -> HwConfigured (guarded by a narrower writer authorization + * plus idleness, TC18 Figure 17's own explicit arrow) — a transition neither + * this spec nor c-RCP's original models at all. field_writable()'s locking + * rules (FieldKind::FunctionalWStar in particular) are, in the real + * implementation, a PURE FUNCTION of the current ServerState — "permanently + * locked once RcpConfigured is reached" literally means "locked while + * state = RcpConfigured", re-evaluated on every query, not a persistent + * latch bit — so demoting via that unmodelled transition would, in the real + * implementation, make a FunctionalWStar field writable again immediately, + * without going all the way back through HwUnconfigured. `field_lock` below + * instead models locking as a separate, sticky variable that only clears via + * FullReset (mirroring c-RCP's own choice), which is faithful to the real + * implementation only as long as this unmodelled demotion is never taken — + * true within this spec's own Next relation (it is not one of the actions + * below), but not a claim about ServerLifecycle::transition()'s full + * behavior. Left as-is, matching c-RCP's own spec's scope, rather than + * silently narrowing what SP2 below actually establishes; re-deriving this + * spec to add that demotion and re-model field_lock as the real state- + * function it is would be a distinct formal-modeling task, not a port. + * + * Safety property (SP1): the server can never reach RcpConfigured + * directly from HwUnconfigured -- every upward transition passes through + * HwConfigured. + * Safety property (SP2): once a field class is locked while the server + * is RcpConfigured, it never becomes unlocked again while the server + * remains RcpConfigured (a lock can only be cleared by demoting all the + * way back to HwUnconfigured -- a full reset). + * + * Liveness property (LP1): given HW/RCP configuration inputs that eventually + * settle and stay consistent, the server eventually reaches RcpConfigured + * under fair scheduling -- i.e. this is not merely a state the server *can* + * reach (SP1/SP2 already establish what happens if it does), it is a state + * fair scheduling *guarantees* it reaches. TLC's default no-successor-state + * deadlock check passes (every state in the model has at least one enabled + * successor). LP1 is a related but strictly stronger claim: progress/ + * livelock-freedom under fairness, not mere deadlock-freedom. The fairness + * conditions below were re-derived and confirmed against real TLC runs + * during this port (WF vs. SF, both re-run), matching c-RCP's own original + * derivation exactly -- the fairness-minimality result carries over + * unchanged because the underlying action structure is unchanged. + *) + +EXTENDS TLC + +HwUnconfigured == "HwUnconfigured" +HwConfigured == "HwConfigured" +RcpConfigured == "RcpConfigured" + +LifecycleStates == {HwUnconfigured, HwConfigured, RcpConfigured} + +Unlocked == "Unlocked" +Locked == "Locked" +LockStates == {Unlocked, Locked} + +VARIABLES state, \* current lifecycle state (ServerLifecycle::state_) + hw_cfg_consistent, \* check_hw_cfg()'s current verdict + rcp_cfg_consistent, \* check_rcp_cfg()'s current verdict + field_lock \* FieldKind::FunctionalWStar field lock state (see "Known + \* abstraction gap" above) + +vars == <> + +TypeOK == + /\ state \in LifecycleStates + /\ hw_cfg_consistent \in BOOLEAN + /\ rcp_cfg_consistent \in BOOLEAN + /\ field_lock \in LockStates + +Init == + /\ state = HwUnconfigured + /\ hw_cfg_consistent \in BOOLEAN + /\ rcp_cfg_consistent \in BOOLEAN + /\ field_lock = Unlocked + +(* The PlausibilitySnapshot check_hw_cfg()/check_rcp_cfg() are evaluated + * against may change between transition attempts -- their verdicts are + * re-evaluated each time advance()/transition() runs, not cached once and + * for all. *) +ReviseHwConsistency == + /\ hw_cfg_consistent' \in BOOLEAN + /\ UNCHANGED <> + +ReviseRcpConsistency == + /\ rcp_cfg_consistent' \in BOOLEAN + /\ UNCHANGED <> + +(* HW_UNCONFIGURED -> HW_CONFIGURED, gated by check_hw_cfg(). *) +PromoteToHwConfigured == + /\ state = HwUnconfigured + /\ hw_cfg_consistent + /\ state' = HwConfigured + /\ UNCHANGED <> + +(* HW_CONFIGURED -> RCP_CONFIGURED, gated by check_rcp_cfg(). HwGeneric + * fields become read-only and FunctionalWStar fields become permanently + * locked (see field_writable()) for the remainder of this configured + * session on this same transition. *) +PromoteToRcpConfigured == + /\ state = HwConfigured + /\ rcp_cfg_consistent + /\ state' = RcpConfigured + /\ field_lock' = Locked + /\ UNCHANGED <> + +(* HW_CONFIGURED -> HW_UNCONFIGURED demotion, modelled unconditional (writer + * authorization/idleness abstracted out of scope; see this spec's own + * top-of-file note). *) +DemoteToHwUnconfigured == + /\ state = HwConfigured + /\ state' = HwUnconfigured + /\ UNCHANGED <> + +(* RCP_CONFIGURED -> HW_UNCONFIGURED full-reset demotion, modelled + * unconditional (writer authorization/idleness abstracted out of scope) and + * the only way this spec clears a field lock -- a full reset re-opens + * hardware configuration from scratch, so whatever FunctionalWStar fields + * were locked for the just-ended configured session no longer apply to the + * next one. This is a modelling assumption, not a literal reading of any + * single rcp/lifecycle.hpp doc comment; see this spec's own "Known + * abstraction gap" note above. *) +FullReset == + /\ state = RcpConfigured + /\ state' = HwUnconfigured + /\ field_lock' = Unlocked + /\ UNCHANGED <> + +Next == + \/ ReviseHwConsistency + \/ ReviseRcpConsistency + \/ PromoteToHwConfigured + \/ PromoteToRcpConfigured + \/ DemoteToHwUnconfigured + \/ FullReset + +Spec == Init /\ [][Next]_<> + +(* FairSpec adds the minimum fairness each promote action genuinely needs to + * guarantee LP1, re-confirmed against real TLC runs during this port: + * + * - WF_vars(PromoteToHwConfigured): weak fairness suffices. Once + * hw_cfg_consistent holds continuously and state = HwUnconfigured holds + * continuously, nothing else can disable PromoteToHwConfigured before it + * fires -- no other action changes state away from HwUnconfigured. TLC + * confirms a WF-only variant already gets the server past HwUnconfigured + * on its own. + * + * - SF_vars(PromoteToRcpConfigured): strong fairness is required, and WF is + * provably insufficient here. DemoteToHwUnconfigured is unconditionally + * enabled at state = HwConfigured and can race PromoteToRcpConfigured back + * to HwUnconfigured every time before it fires, so PromoteToRcpConfigured + * is never *continuously* enabled -- only *infinitely often* enabled -- + * which WF does not act on but SF does. TLC confirms a WF-only variant on + * this action finds a concrete Promote/Demote lasso counterexample that + * never leaves {HwUnconfigured, HwConfigured}. + *) +FairSpec == Spec + /\ WF_vars(PromoteToHwConfigured) + /\ SF_vars(PromoteToRcpConfigured) + +(* LP1's antecedent: check_hw_cfg()/check_rcp_cfg()'s inputs eventually + * settle and stay consistent (become permanently TRUE) -- without this, + * ReviseHwConsistency/ReviseRcpConsistency (deliberately left unfair, + * matching their role as an unconstrained environment input) could keep an + * input flapping forever and no fairness on the promote actions could + * compensate, since neither promote action is ever enabled while its + * gating input is FALSE. *) +InputsEventuallyConsistent == <>[](hw_cfg_consistent /\ rcp_cfg_consistent) + +(* LP1: given eventually-consistent inputs and fair scheduling of the two + * promote actions (at the minimum fairness level each genuinely needs, + * above), the server eventually reaches RcpConfigured. *) +EventuallyRcpConfigured == InputsEventuallyConsistent => <>(state = RcpConfigured) + +(* SP1: No skip-configuration transition -- RcpConfigured is only ever + * reached from HwConfigured, never directly from HwUnconfigured. *) +NoSkipConfiguration == + [][state = HwUnconfigured => state' # RcpConfigured]_<> + +(* SP2: A field lock, once set while RcpConfigured, is never cleared except + * by the full-reset transition back to HwUnconfigured -- i.e. it never + * silently reverts to Unlocked while the server remains RcpConfigured + * (subject to this spec's own "Known abstraction gap" note above). *) +FieldLockMonotonicWhileConfigured == + [][ (state = RcpConfigured /\ field_lock = Locked /\ state' = RcpConfigured) + => field_lock' = Locked ]_<> + +THEOREM Spec => TypeOK /\ NoSkipConfiguration /\ FieldLockMonotonicWhileConfigured +THEOREM FairSpec => EventuallyRcpConfigured + +====