Skip to content

Commit 89e7ae5

Browse files
Jonathan D.A. Jewellclaude
andcommitted
feat: add system-health example using linear types
Demonstrates ephapax linear discipline for real-world system monitoring. Health probes (memory, swap, thermal, disk, compositor, services) are encoded as linear values consumed exactly once through a threaded report. Includes host FFI declarations for Deno runtime integration. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent f1b95b9 commit 89e7ae5

1 file changed

Lines changed: 320 additions & 0 deletions

File tree

examples/system-health.eph

Lines changed: 320 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,320 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// system-health.eph - System dependability report in Ephapax linear
3+
//
4+
// Linear types guarantee each health probe is consumed exactly once,
5+
// preventing double-reads of stale data and ensuring every resource
6+
// handle (procfs, sysfs, service bus) is properly closed.
7+
//
8+
// Host FFI functions are imported from the Deno runtime.
9+
// Compile: just cli compile system-health.eph --mode linear --out system-health.wasm
10+
// Run: deno run --allow-read --allow-run system-health-host.ts
11+
12+
// ============================================================================
13+
// Status Encoding
14+
// ============================================================================
15+
16+
// Health status levels: OK < WARN < CRIT
17+
fn status_ok() -> i32 { 0 }
18+
fn status_warn() -> i32 { 1 }
19+
fn status_crit() -> i32 { 2 }
20+
21+
// Merge two statuses: take the worst (highest)
22+
fn status_merge(a: i32, b: i32) -> i32 {
23+
if a > b { a } else { b }
24+
}
25+
26+
fn status_name(s: i32) -> i32 {
27+
// 0 = "OK", 1 = "WARN", 2 = "CRIT" (host decodes)
28+
s
29+
}
30+
31+
// ============================================================================
32+
// Health Report Encoding
33+
// ============================================================================
34+
35+
// A HealthReport packs: (overall_status, check_count, issue_count)
36+
// Encoding: status * 10000 + check_count * 100 + issue_count
37+
// Linear: must be consumed exactly once (threaded through checks)
38+
39+
fn report_new() -> i32 {
40+
// status=OK(0), checks=0, issues=0
41+
0
42+
}
43+
44+
fn report_status(report: i32) -> i32 {
45+
report / 10000
46+
}
47+
48+
fn report_checks(report: i32) -> i32 {
49+
let remainder = report % 10000;
50+
remainder / 100
51+
}
52+
53+
fn report_issues(report: i32) -> i32 {
54+
report % 100
55+
}
56+
57+
fn report_add_check(report: i32, check_status: i32) -> i32 {
58+
let old_status = report_status(report);
59+
let old_checks = report_checks(report);
60+
let old_issues = report_issues(report);
61+
62+
let new_status = status_merge(old_status, check_status);
63+
let new_checks = old_checks + 1;
64+
let new_issues = if check_status > 0 { old_issues + 1 } else { old_issues };
65+
66+
let result = new_status * 10000 + new_checks * 100 + new_issues;
67+
result
68+
}
69+
70+
// ============================================================================
71+
// Probe Encoding
72+
// ============================================================================
73+
74+
// A Probe is a linear handle to a system metric reading.
75+
// Encoding: (source_tag * 1000000) + value
76+
// source_tag: 1=memory, 2=swap, 3=thermal, 4=disk, 5=compositor, 6=service
77+
// The value is metric-specific (percentage, temperature, boolean).
78+
// Linear: must be evaluated (consumed) exactly once.
79+
80+
fn probe_source(probe: i32) -> i32 {
81+
probe / 1000000
82+
}
83+
84+
fn probe_value(probe: i32) -> i32 {
85+
probe % 1000000
86+
}
87+
88+
fn mk_probe(source: i32, value: i32) -> i32 {
89+
source * 1000000 + value
90+
}
91+
92+
// Source tags
93+
fn src_memory() -> i32 { 1 }
94+
fn src_swap() -> i32 { 2 }
95+
fn src_thermal() -> i32 { 3 }
96+
fn src_disk() -> i32 { 4 }
97+
fn src_compositor() -> i32 { 5 }
98+
fn src_service() -> i32 { 6 }
99+
fn src_gpu() -> i32 { 7 }
100+
fn src_boot() -> i32 { 8 }
101+
102+
// ============================================================================
103+
// Threshold Evaluation
104+
// ============================================================================
105+
106+
// Evaluate a percentage probe against warn/crit thresholds
107+
fn eval_pct_probe(probe: i32, warn_thresh: i32, crit_thresh: i32) -> i32 {
108+
let value = probe_value(probe);
109+
// probe consumed here (linear - cannot reuse)
110+
if value >= crit_thresh {
111+
status_crit()
112+
} else {
113+
if value >= warn_thresh {
114+
status_warn()
115+
} else {
116+
status_ok()
117+
}
118+
}
119+
}
120+
121+
// Evaluate a temperature probe (skip bogus 127C readings)
122+
fn eval_temp_probe(probe: i32) -> i32 {
123+
let value = probe_value(probe);
124+
if value == 127 {
125+
// ACPI PCHZ bogus sensor - always skip
126+
status_ok()
127+
} else {
128+
if value >= 95 {
129+
status_crit()
130+
} else {
131+
if value >= 80 {
132+
status_warn()
133+
} else {
134+
status_ok()
135+
}
136+
}
137+
}
138+
}
139+
140+
// Evaluate a boolean probe (1=running/ok, 0=down/bad)
141+
fn eval_bool_probe(probe: i32) -> i32 {
142+
let value = probe_value(probe);
143+
if value == 1 {
144+
status_ok()
145+
} else {
146+
status_crit()
147+
}
148+
}
149+
150+
// Evaluate boot frequency probe (count of recent boots)
151+
fn eval_boot_probe(probe: i32) -> i32 {
152+
let value = probe_value(probe);
153+
if value > 10 {
154+
status_warn()
155+
} else {
156+
status_ok()
157+
}
158+
}
159+
160+
// ============================================================================
161+
// Host FFI Imports (provided by Deno runtime)
162+
// ============================================================================
163+
164+
// These functions are imported from the host environment.
165+
// Each returns a linear Probe that must be consumed exactly once.
166+
//
167+
// extern fn host_read_mem_pct() -> i32; // memory used %
168+
// extern fn host_read_swap_pct() -> i32; // swap used %
169+
// extern fn host_read_cpu_temp() -> i32; // CPU package temp (C)
170+
// extern fn host_read_gpu_temp() -> i32; // GPU temp (C)
171+
// extern fn host_read_disk_pct(id: i32) -> i32; // disk used % (0=var, 1=eclipse, 2=boot)
172+
// extern fn host_compositor_alive() -> i32; // 1=running, 0=dead
173+
// extern fn host_service_alive(id: i32) -> i32; // 1=active, 0=inactive
174+
// extern fn host_boot_count() -> i32; // boots in journal
175+
// extern fn host_emit_line(tag: i32, status: i32, value: i32) -> i32; // print a line
176+
177+
// ============================================================================
178+
// Individual Health Checks
179+
// ============================================================================
180+
181+
// Each check function consumes the report (linear), reads a probe (linear),
182+
// evaluates it, and produces a new report (linear). This threading ensures
183+
// no check is skipped and no data is read twice.
184+
185+
fn check_memory(report: i32, mem_pct: i32) -> i32 {
186+
let probe = mk_probe(src_memory(), mem_pct);
187+
let status = eval_pct_probe(probe, 80, 90);
188+
// probe is consumed by eval_pct_probe - cannot reuse
189+
let new_report = report_add_check(report, status);
190+
new_report
191+
}
192+
193+
fn check_swap(report: i32, swap_pct: i32) -> i32 {
194+
let probe = mk_probe(src_swap(), swap_pct);
195+
let status = eval_pct_probe(probe, 50, 80);
196+
let new_report = report_add_check(report, status);
197+
new_report
198+
}
199+
200+
fn check_thermal(report: i32, temp_c: i32) -> i32 {
201+
let probe = mk_probe(src_thermal(), temp_c);
202+
let status = eval_temp_probe(probe);
203+
let new_report = report_add_check(report, status);
204+
new_report
205+
}
206+
207+
fn check_gpu(report: i32, gpu_temp: i32) -> i32 {
208+
let probe = mk_probe(src_gpu(), gpu_temp);
209+
let status = eval_temp_probe(probe);
210+
let new_report = report_add_check(report, status);
211+
new_report
212+
}
213+
214+
fn check_disk(report: i32, disk_pct: i32) -> i32 {
215+
let probe = mk_probe(src_disk(), disk_pct);
216+
let status = eval_pct_probe(probe, 85, 95);
217+
let new_report = report_add_check(report, status);
218+
new_report
219+
}
220+
221+
fn check_compositor(report: i32, alive: i32) -> i32 {
222+
let probe = mk_probe(src_compositor(), alive);
223+
let status = eval_bool_probe(probe);
224+
let new_report = report_add_check(report, status);
225+
new_report
226+
}
227+
228+
fn check_service(report: i32, alive: i32) -> i32 {
229+
let probe = mk_probe(src_service(), alive);
230+
let status = eval_bool_probe(probe);
231+
let new_report = report_add_check(report, status);
232+
new_report
233+
}
234+
235+
fn check_boots(report: i32, boot_count: i32) -> i32 {
236+
let probe = mk_probe(src_boot(), boot_count);
237+
let status = eval_boot_probe(probe);
238+
let new_report = report_add_check(report, status);
239+
new_report
240+
}
241+
242+
// ============================================================================
243+
// Main: Thread the linear HealthReport through all checks
244+
// ============================================================================
245+
246+
fn main() -> i32 {
247+
// Create initial report (linear - must be consumed exactly once)
248+
let report = report_new();
249+
250+
// -- The host runtime calls us with sensor values via WASM imports.
251+
// -- For the compiled version, main() returns 0 (success) if the
252+
// -- type system itself is sound. The actual health check pipeline
253+
// -- runs in run_health_check() which the host invokes.
254+
255+
// Self-test: verify report encoding roundtrips
256+
let test_report = report_new();
257+
let test_r1 = report_add_check(test_report, status_ok());
258+
let test_r2 = report_add_check(test_r1, status_warn());
259+
let test_r3 = report_add_check(test_r2, status_crit());
260+
261+
let final_status = report_status(test_r3);
262+
let final_checks = report_checks(test_r3);
263+
let final_issues = report_issues(test_r3);
264+
265+
// Expected: status=2(CRIT), checks=3, issues=2
266+
let status_ok_v = final_status - 2;
267+
let checks_ok_v = final_checks - 3;
268+
let issues_ok_v = final_issues - 2;
269+
270+
// Consume the initial report (linear obligation)
271+
let consumed = report_status(report);
272+
273+
// Return 0 if all self-tests pass
274+
let err = status_ok_v * status_ok_v + checks_ok_v * checks_ok_v + issues_ok_v * issues_ok_v;
275+
err
276+
}
277+
278+
// ============================================================================
279+
// Exported: run_health_check - called by host with sensor readings
280+
// ============================================================================
281+
282+
// The host calls this with all sensor values packed into parameters.
283+
// Returns the final encoded report (linear - exactly one result).
284+
fn run_health_check(
285+
mem_pct: i32,
286+
swap_pct: i32,
287+
cpu_temp: i32,
288+
gpu_temp: i32,
289+
disk_var_pct: i32,
290+
disk_eclipse_pct: i32,
291+
disk_boot_pct: i32,
292+
compositor_alive: i32,
293+
svc_containerd: i32,
294+
svc_pipewire: i32,
295+
svc_watchdog: i32,
296+
svc_syncthing: i32,
297+
boot_count: i32
298+
) -> i32 {
299+
// Thread the linear report through every check in sequence.
300+
// Each step consumes the old report and produces a new one.
301+
// The type system guarantees no check is skipped or doubled.
302+
303+
let r0 = report_new();
304+
let r1 = check_memory(r0, mem_pct);
305+
let r2 = check_swap(r1, swap_pct);
306+
let r3 = check_thermal(r2, cpu_temp);
307+
let r4 = check_gpu(r3, gpu_temp);
308+
let r5 = check_disk(r4, disk_var_pct);
309+
let r6 = check_disk(r5, disk_eclipse_pct);
310+
let r7 = check_disk(r6, disk_boot_pct);
311+
let r8 = check_compositor(r7, compositor_alive);
312+
let r9 = check_service(r8, svc_containerd);
313+
let r10 = check_service(r9, svc_pipewire);
314+
let r11 = check_service(r10, svc_watchdog);
315+
let r12 = check_service(r11, svc_syncthing);
316+
let r13 = check_boots(r12, boot_count);
317+
318+
// r13 is the final report - consumed by returning it
319+
r13
320+
}

0 commit comments

Comments
 (0)