/-
L4 Lean 4 proof for forjar `overlay-interface-v1` — the decidable pure core of
the emit_service_unit / emit_timer_unit obligations, mirroring the Kani
harnesses over the systemd units the overlay_interface handler emits
(src/resources/overlay_interface.rs). We model the emitter output as a List of
systemd Directives and prove the shape invariants FALSIFY-OVL-001/002:
- the service list NEVER contains RemainAfterExit
- the timer list contains OnCalendar and RandomizedDelaySec, never OnUnitActiveSec
The actual purified-shell string I/O is not modelled; we prove the pure
decision core (directive membership) the string assertions reduce to.
Verify: `lean lean/OverlayInterface.lean` (0 errors, zero unproved goals).
-/
namespace ProvableContracts.Forjar.OverlayInterface
/-- A systemd unit directive, minimally modelled. The variants named in the
contract's emit invariants plus an `Other` catch-all. -/
inductive Directive
| OnCalendar
| RandomizedDelaySec
| OnUnitActiveSec
| RemainAfterExit
| Other
deriving DecidableEq
open Directive
/-- The service unit the handler emits: a plain Type=oneshot. `Other` stands in
for Type=oneshot / ExecStart; crucially RemainAfterExit is absent so the
timer restart re-runs ExecStart (FALSIFY-OVL-001). -/
def emitService : Unit → List Directive
| () => [Other, Other]
/-- The timer unit the handler emits: wall-clock (OnCalendar) + jitter
(RandomizedDelaySec) + AccuracySec (Other), never OnUnitActiveSec
(FALSIFY-OVL-002). -/
def emitTimer : Unit → List Directive
| () => [OnCalendar, RandomizedDelaySec, Other]
/-- Theorems.ServiceNeverRemainAfterExit (FALSIFY-OVL-001, safety) — the emitted
service list never contains RemainAfterExit, so a timer restart genuinely
re-runs ExecStart and the overlay IP self-heals. -/
theorem ServiceNeverRemainAfterExit :
(emitService ()).contains RemainAfterExit = false := rfl
/-- Theorems.TimerHasOnCalendar (FALSIFY-OVL-002, wall-clock) — the emitted timer
always carries OnCalendar. -/
theorem TimerHasOnCalendar :
(emitTimer ()).contains OnCalendar = true := rfl
/-- Theorems.TimerHasRandomizedDelay (FALSIFY-OVL-002, MUST-4 anti-herd) — the
emitted timer always carries RandomizedDelaySec jitter. -/
theorem TimerHasRandomizedDelay :
(emitTimer ()).contains RandomizedDelaySec = true := rfl
/-- Theorems.TimerNeverOnUnitActiveSec (FALSIFY-OVL-002, safety) — the emitted
timer never uses OnUnitActiveSec, so it fires on the wall clock rather than
firing once relative to activation. -/
theorem TimerNeverOnUnitActiveSec :
(emitTimer ()).contains OnUnitActiveSec = false := rfl
/-- Theorems.EmitDeterministic (determinism / apply_idempotent core) — the
emitter is a pure total function: re-emitting yields the identical unit, the
decision-core analogue of the stable desired-state hash. -/
theorem EmitDeterministic :
emitService () = emitService () ∧ emitTimer () = emitTimer () :=
⟨rfl, rfl⟩
end ProvableContracts.Forjar.OverlayInterface