Skip to content

Commit bd0708d

Browse files
hyperpolymathhyperpolymath
committed
docs: substantive CRG C annotation (EXPLAINME.adoc)
1 parent 1e63263 commit bd0708d

1 file changed

Lines changed: 210 additions & 0 deletions

File tree

‎EXPLAINME.adoc‎

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= Session Sentinel — Show Me The Receipts
3+
:toc:
4+
:icons: font
5+
6+
The README makes claims. This file backs them up.
7+
8+
== Multi-AI Session Health Monitor
9+
10+
[quote, README]
11+
____
12+
Session Sentinel watches storage consumption across multiple AI tools (Claude,
13+
Copilot, Ollama, LM Studio, Continue.dev, Cursor, Aider, and custom providers),
14+
provides real-time health status via a KDE system tray icon, automatically cleans
15+
up stale sessions, and exposes a PanLL panel for fine-grained analysis and control.
16+
____
17+
18+
`src/core/scanner.as` enumerates known AI provider storage paths and accumulates
19+
byte totals per provider. `src/core/health.as` maps the total against four
20+
threshold bands (Green < 200 MB, Yellow < 500 MB, Red < 800 MB, Purple >= 800 MB)
21+
and emits a typed health zone. `src/core/healer.as` triggers pruning actions
22+
appropriate to the current zone: orphan removal for Yellow, stale-conversation
23+
pruning for Red, aggressive cleanup for Purple. Provider paths and thresholds
24+
are all configurable in `~/.config/session-sentinel/config.toml` (default:
25+
`config/session-sentinel.toml`).
26+
27+
**Caveat:** AffineScript core files (`src/core/*.as`) are the intended
28+
implementation. The PanLL panel manifest (`src/panels/manifest.json`) is
29+
specified in `README.adoc` but the `src/panels/` directory was not present at
30+
the time of this writing — it is pending wiring. The DBus interface is
31+
specified in `README.adoc` and implemented in the Zig FFI layer but requires
32+
a running KDE session to exercise.
33+
34+
- Scanner: `src/core/scanner.as`
35+
- Health model: `src/core/health.as`
36+
- Healer: `src/core/healer.as`
37+
- Monitor loop: `src/core/monitor.as`
38+
- Diagnostics: `src/core/diagnostics.as`
39+
- Config schema: `config/session-sentinel.toml`
40+
41+
== Idris2 ABI: Formally Verified Health State Machine
42+
43+
[quote, README]
44+
____
45+
ABI (Idris2): src/interface/abi/*.idr — Formally verified health state machine,
46+
monitor protocol, panel protocol. Dependent types prove threshold ordering and
47+
state transition validity.
48+
____
49+
50+
`src/interface/abi/HealthState.idr` defines the `HealthZone` dependent type
51+
with a proof that zone thresholds are strictly ordered (Green < Yellow < Red <
52+
Purple). `src/interface/abi/MonitorProtocol.idr` specifies the protocol between
53+
the scanner loop and the health emitter. `src/interface/abi/PanelProtocol.idr`
54+
specifies the DBus-level panel API. `src/interface/abi/Types.idr` provides
55+
shared type definitions. `src/interface/abi/Layout.idr` and `Foreign.idr`
56+
govern memory layout and FFI boundary types.
57+
https://idris2.readthedocs.io/en/latest/[Idris2 documentation]
58+
59+
**Caveat:** The Idris2 files exist and define the interface, but C header
60+
generation from these specs (the `generated/abi/` step in the standard ABI/FFI
61+
pipeline) has not been verified as passing in CI.
62+
63+
- ABI definitions: `src/interface/abi/HealthState.idr`, `MonitorProtocol.idr`, `PanelProtocol.idr`, `Types.idr`, `Layout.idr`, `Foreign.idr`
64+
- Learn more: https://github.com/hyperpolymath/rsr-template-repo/blob/main/ABI-FFI-README.md
65+
66+
== Zig FFI: System Tray, DBus, Watchdog
67+
68+
[quote, README]
69+
____
70+
FFI (Zig): src/interface/ffi/src/*.zig — Native KDE StatusNotifierItem via DBus,
71+
icon generation, watchdog, systemd integration. Zero runtime dependencies.
72+
____
73+
74+
`src/interface/ffi/src/` contains Zig source files implementing the KDE
75+
StatusNotifierItem D-Bus protocol (native StatusNotifier method dispatch),
76+
dynamic icon generation for each health zone, a watchdog that tracks consecutive
77+
scan failures and enters degraded mode after 3, and systemd notification
78+
integration (`sd_notify`). `src/interface/ffi/build.zig` is the Zig build
79+
definition. Integration tests live in `src/interface/ffi/test/`.
80+
https://ziglang.org/documentation/master/[Zig language reference]
81+
82+
**Caveat:** The D-Bus implementation is KDE-specific (StatusNotifierItem
83+
protocol). GNOME (AppIndicator) is not supported. Windows and macOS tray
84+
integration are not implemented.
85+
86+
- FFI source: `src/interface/ffi/src/`
87+
- Build: `src/interface/ffi/build.zig`
88+
- Tests: `src/interface/ffi/test/`
89+
90+
== Systemd User Service
91+
92+
[quote, README]
93+
____
94+
Boot activation: Systemd user service starts with graphical session, watchdog-integrated.
95+
____
96+
97+
`systemd/session-sentinel.service` is a systemd user unit with
98+
`WantedBy=graphical-session.target`. `systemd/install.sh` copies it to
99+
`~/.config/systemd/user/` and runs `systemctl --user daemon-reload`. The
100+
service invokes `session-sentinel-tray` which accepts `--once` for a manual
101+
single-scan and SIGHUP for config reload. The watchdog integration uses
102+
`WatchdogSec=` in the unit file and `sd_notify(WATCHDOG=1)` from the Zig layer.
103+
104+
**Caveat:** Requires a systemd user session (standard on Fedora/GNOME/KDE).
105+
Incompatible with pure musl/runit systems.
106+
107+
- Service file: `systemd/session-sentinel.service`
108+
- Installer: `systemd/install.sh`
109+
110+
== Verification and Safety Case
111+
112+
[quote, README]
113+
____
114+
Fault-tolerant: Watchdog monitors scan health; 3 consecutive failures enter
115+
degraded mode; automatic recovery with exponential backoff.
116+
____
117+
118+
`verification/` contains the formal verification artefacts: `proofs/` holds
119+
Idris2 proofs of protocol properties, `tests/` holds protocol conformance tests,
120+
`fuzzing/` holds fuzz driver inputs, `simulations/` holds model simulations,
121+
`benchmarks/` holds performance regression cases, `traceability/` maps
122+
requirements to proof obligations, and `safety_case/` contains the structured
123+
assurance case. `coverage/` tracks proof coverage metrics.
124+
125+
**Caveat:** The safety case is structured but not independently assessed.
126+
Fuzzing drivers require a supported fuzzer (AFL++, libFuzzer).
127+
128+
- Proofs: `verification/proofs/`
129+
- Safety case: `verification/safety_case/`
130+
- Traceability: `verification/traceability/`
131+
132+
== Stapeln Container Deployment
133+
134+
[quote, README]
135+
____
136+
container/ — Stapeln container ecosystem (for server deployments)
137+
____
138+
139+
`container/` provides Stapeln-compatible container definitions using a Chainguard
140+
base image. `container/Containerfile` is the Podman-compatible build file.
141+
`container/entrypoint.sh` bootstraps the service inside the container.
142+
`container/manifest.toml` declares the container manifest. `container/vordr.toml`
143+
configures the Vordr security policy. The compose example at
144+
`container/compose.example.toml` shows multi-container deployment.
145+
https://github.com/hyperpolymath/stapeln[Stapeln]
146+
147+
**Caveat:** Server-mode deployment via container is secondary to the primary
148+
systemd-user install path. Container mode does not have a system tray.
149+
150+
- Container: `container/Containerfile`, `container/manifest.toml`
151+
- Entry point: `container/entrypoint.sh`
152+
153+
== Dogfooded Across The Account
154+
155+
[cols="1,2"]
156+
|===
157+
| Technology | Also Used In
158+
159+
| **Idris2 ABI** | https://github.com/hyperpolymath/stapeln, https://github.com/hyperpolymath/groove
160+
| **Zig FFI** | https://github.com/hyperpolymath/airborne-submarine-squadron, https://github.com/hyperpolymath/burble
161+
| **AffineScript core** | https://github.com/hyperpolymath/airborne-submarine-squadron (game logic)
162+
| **KDE StatusNotifierItem** | https://github.com/hyperpolymath/ambientops (volumod tray)
163+
| **Stapeln containers** | https://github.com/hyperpolymath/stapeln (container standard)
164+
| **PanLL panels** | https://github.com/hyperpolymath/panll (panel framework)
165+
| **Deno runtime** | https://github.com/hyperpolymath/airborne-submarine-squadron
166+
|===
167+
168+
== File Map
169+
170+
[cols="1,2"]
171+
|===
172+
| Path | Proves
173+
174+
| `src/core/scanner.as` | Provider storage enumeration and byte accumulation
175+
| `src/core/health.as` | Threshold evaluation and health zone classification
176+
| `src/core/healer.as` | Zone-appropriate cleanup actions (prune, aggressive clean)
177+
| `src/core/monitor.as` | Main scan-and-notify loop with watchdog integration
178+
| `src/core/diagnostics.as` | Diagnostic log collection and export
179+
| `src/core/providers.as` | Known AI provider path registry
180+
| `src/core/config.as` | Config file loading and threshold binding
181+
| `src/interface/abi/HealthState.idr` | Dependent type proof of threshold ordering
182+
| `src/interface/abi/MonitorProtocol.idr` | Formally specified monitor ↔ health protocol
183+
| `src/interface/abi/PanelProtocol.idr` | DBus panel API specification
184+
| `src/interface/abi/Types.idr` | Shared ABI type definitions
185+
| `src/interface/abi/Layout.idr` | Memory layout proofs
186+
| `src/interface/abi/Foreign.idr` | FFI boundary type declarations
187+
| `src/interface/ffi/src/` | Zig implementations: tray, DBus, icons, watchdog, systemd
188+
| `src/interface/ffi/build.zig` | Zig build system entry point
189+
| `src/interface/ffi/test/` | FFI integration tests
190+
| `src/interface/generated/` | Auto-generated C headers from Idris2 ABI
191+
| `config/session-sentinel.toml` | Default config with all options documented
192+
| `systemd/session-sentinel.service` | Systemd user service unit
193+
| `systemd/install.sh` | Service installer script
194+
| `container/Containerfile` | Podman/Stapeln container definition (Chainguard base)
195+
| `container/manifest.toml` | Stapeln container manifest
196+
| `container/entrypoint.sh` | Container startup script
197+
| `verification/proofs/` | Idris2 proofs of protocol properties
198+
| `verification/safety_case/` | Structured assurance case
199+
| `verification/traceability/` | Requirements-to-proof traceability matrix
200+
| `verification/fuzzing/` | Fuzz driver inputs
201+
| `verification/benchmarks/` | Performance regression benchmarks
202+
| `features/` | BDD-style feature specifications
203+
| `tests/` | Test suite (Deno-based integration tests)
204+
| `examples/` | Example config files
205+
| `docs/` | Architecture and design documentation
206+
| `.machine_readable/` | A2ML state, meta, ecosystem files
207+
| `Justfile` | Task runner (build, install, test, clean)
208+
| `flake.nix` | Nix development shell
209+
| `guix.scm` | Guix package definition
210+
|===

0 commit comments

Comments
 (0)