Skip to content

Commit 9f8812e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
Add proven-servers integration, Ephapax linear types, PanLL panels
proven-servers ABI bindings: - src/abi/ProvenFSM.idr — FSM types adapted for workflow state machine (MachineState→WorkflowStatus, TransitionResult, EventDisposition, ValidMachineTransition with impossibility proofs) - src/abi/ProvenQueue.idr — Queue connector types for HAR event consumption (QueueState, MessageState, DeliveryGuarantee, QueueOp with lifecycle proofs) Ephapax linear types (supplementary to Idris2, not authoritative): - src/abi/LinearDispatch.eph — linear ownership semantics: - RoutedEvent linear: events consumed exactly once (no double-dispatch) - WorkflowTransition linear: transitions atomic (old state invalidated) - QueueLease linear: handles explicitly released (no connection leaks) - withLease pattern for scoped queue access PanLL monitoring panels: - panels/fs-workflow/panel.json — workflow monitor (status, watch paths, rules, event timeline, action results, FSM state diagram, queue status) - panels/plugin-status/panel.json — plugin system monitor (loaded plugins, sandbox memory, execution log) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 8f2a66a commit 9f8812e

7 files changed

Lines changed: 923 additions & 6 deletions

File tree

‎.machine_readable/STATE.a2ml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,9 @@ milestone = "Phase 1.1 — Scaffolding"
1818
focus = "Multi-language scaffold, ABI/FFI layer, governance cleanup"
1919
rust-workspace = "done"
2020
abi-ffi-scaffold = "done"
21+
proven-fsm-bindings = "done"
22+
proven-queueconn-bindings = "done"
23+
ephapax-linear-types = "done"
2124
multi-lang-scaffold = "done"
2225
hypatia-workflow = "done"
2326

@@ -34,3 +37,4 @@ priority-5 = "Implement rpa-state persistence layer"
3437
[session-history]
3538
# 2026-03-16: Governance cleanup, license alignment, ABI/FFI scaffold, multi-lang scaffold
3639
# 2026-03-17: Doc cleanup, security fixes (wasmtime 36.0.6), SPDX alignment, Hypatia rules config, CodeQL matrix fix, cruft removal
40+
# 2026-03-16: proven-fsm bindings (ProvenFSM.idr), proven-queueconn bindings (ProvenQueue.idr), Ephapax linear types (LinearDispatch.eph)

‎ABI-FFI-README.md‎

Lines changed: 59 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -33,15 +33,18 @@ RPA Elysium uses the **hyperpolymath universal ABI/FFI standard**:
3333

3434
```
3535
src/abi/
36-
Types.idr — Core RPA types (Event, Action, Workflow, Error)
37-
Layout.idr — Memory layout proofs and alignment guarantees
38-
Foreign.idr — FFI function declarations and calling conventions
36+
Types.idr — Core RPA types (Event, Action, Workflow, Error)
37+
Layout.idr — Memory layout proofs and alignment guarantees
38+
Foreign.idr — FFI function declarations and calling conventions
39+
ProvenFSM.idr — proven-fsm bindings (workflow state machine)
40+
ProvenQueue.idr — proven-queueconn bindings (event queue interface)
41+
LinearDispatch.eph — Ephapax linear types (single-use event dispatch)
3942
4043
ffi/zig/
41-
build.zig — Zig build configuration (shared + static lib)
42-
src/main.zig — C-compatible FFI implementation stubs
44+
build.zig — Zig build configuration (shared + static lib)
45+
src/main.zig — C-compatible FFI implementation stubs
4346
44-
generated/abi/ — Auto-generated C headers (not yet implemented)
47+
generated/abi/ — Auto-generated C headers (not yet implemented)
4548
```
4649

4750
## Type Mapping
@@ -67,13 +70,63 @@ cd ffi/zig && zig build test
6770
cargo build --workspace
6871
```
6972

73+
## Proven-Servers Integration
74+
75+
RPA Elysium integrates with the **proven-servers** ecosystem for formally
76+
verified state machines and message queue interfaces:
77+
78+
### proven-fsm (ProvenFSM.idr)
79+
80+
Maps proven-fsm's linear finite state machine types onto RPA Elysium's
81+
workflow lifecycle:
82+
83+
| proven-fsm `MachineState` | RPA Elysium `WorkflowStatus` | Tag |
84+
|---------------------------|------------------------------|-----|
85+
| `Initial` | `Idle` | 0 |
86+
| `Running` | `Running` | 1 |
87+
| `Terminal` | `Stopped` | 2 |
88+
| `Faulted` | `Error` | 3 |
89+
90+
Additional types imported:
91+
- `TransitionResult` (Accepted/Rejected/Deferred) — workflow state change outcomes
92+
- `EventDisposition` (Consumed/Ignored/Queued/Dropped) — event processing results
93+
- `ValidMachineTransition` — proof-carrying type for legal state transitions
94+
95+
### proven-queueconn (ProvenQueue.idr)
96+
97+
Maps proven-queueconn's queue connector types onto RPA Elysium's event
98+
consumption layer (events routed from the Hybrid Automation Router):
99+
100+
- `QueueState` — subscription lifecycle (Disconnected/Connected/Consuming/Producing/Failed)
101+
- `MessageState` — individual event lifecycle (Pending/Delivered/Acknowledged/Rejected/DeadLettered/Expired)
102+
- `DeliveryGuarantee` — per-workflow delivery semantics (AtMostOnce/AtLeastOnce/ExactlyOnce)
103+
- `QueueOp` — queue operations (Publish/Subscribe/Acknowledge/Reject/Peek/Purge)
104+
- `ValidQueueTransition` — proof-carrying type for legal subscription state transitions
105+
106+
### Ephapax Linear Types (LinearDispatch.eph)
107+
108+
Defines linear types that enforce single-use semantics at compile time:
109+
110+
| Type | Guarantee |
111+
|------|-----------|
112+
| `RoutedEvent linear` | Event consumed exactly once — no duplication, no silent drop |
113+
| `WorkflowTransition linear` | Transition executed exactly once — no re-execution |
114+
| `QueueLease linear` | Subscription handle explicitly released — no resource leak |
115+
116+
Uses `let!` bindings to enforce that linear values are consumed exactly once
117+
within their scope. The `withLease` pattern provides automatic lease
118+
lifecycle management.
119+
70120
## Current Status
71121

72122
- [x] Idris2 ABI type definitions (scaffold)
73123
- [x] Idris2 layout proofs (scaffold)
74124
- [x] Idris2 FFI declarations (scaffold)
75125
- [x] Zig build configuration
76126
- [x] Zig FFI stubs with tests
127+
- [x] proven-fsm bindings (ProvenFSM.idr)
128+
- [x] proven-queueconn bindings (ProvenQueue.idr)
129+
- [x] Ephapax linear types (LinearDispatch.eph)
77130
- [ ] C header generation from Idris2
78131
- [ ] Wire FFI into Rust via `extern "C"` bindings
79132
- [ ] Integration tests (Rust <-> Zig via C ABI)

‎panels/fs-workflow/panel.json‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
{
2+
"$schema": "panll-panel/v1",
3+
"panel_id": "rpa-fs-workflow-monitor",
4+
"name": "Filesystem Workflow Monitor",
5+
"description": "Real-time monitoring panel for rpa-fs-workflow automation — watch paths, rule matches, action results",
6+
"version": "0.1.0",
7+
"category": "automation",
8+
"layout": {
9+
"type": "grid",
10+
"columns": 4,
11+
"rows": 5,
12+
"gap": "8px"
13+
},
14+
"widgets": [
15+
{
16+
"id": "workflow-status",
17+
"type": "status-indicator",
18+
"position": { "col": 1, "row": 1, "span_cols": 1 },
19+
"label": "Workflow Status",
20+
"data_source": "rpa-elysium://workflow/status",
21+
"states": {
22+
"idle": { "color": "#6b7280", "icon": "pause-circle" },
23+
"running": { "color": "#22c55e", "icon": "play-circle" },
24+
"paused": { "color": "#f59e0b", "icon": "pause" },
25+
"stopped": { "color": "#ef4444", "icon": "stop-circle" },
26+
"error": { "color": "#ef4444", "icon": "alert-circle" }
27+
}
28+
},
29+
{
30+
"id": "events-processed",
31+
"type": "counter",
32+
"position": { "col": 2, "row": 1, "span_cols": 1 },
33+
"label": "Events Processed",
34+
"data_source": "rpa-elysium://workflow/metrics/events_processed",
35+
"format": "number"
36+
},
37+
{
38+
"id": "actions-executed",
39+
"type": "counter",
40+
"position": { "col": 3, "row": 1, "span_cols": 1 },
41+
"label": "Actions Executed",
42+
"data_source": "rpa-elysium://workflow/metrics/actions_executed",
43+
"format": "number"
44+
},
45+
{
46+
"id": "error-count",
47+
"type": "counter",
48+
"position": { "col": 4, "row": 1, "span_cols": 1 },
49+
"label": "Errors",
50+
"data_source": "rpa-elysium://workflow/metrics/error_count",
51+
"format": "number",
52+
"thresholds": { "warning": 1, "critical": 5 }
53+
},
54+
{
55+
"id": "watch-paths",
56+
"type": "table",
57+
"position": { "col": 1, "row": 2, "span_cols": 2 },
58+
"label": "Watch Paths",
59+
"data_source": "rpa-elysium://workflow/watch_paths",
60+
"columns": [
61+
{ "key": "path", "label": "Path" },
62+
{ "key": "recursive", "label": "Recursive" },
63+
{ "key": "events_seen", "label": "Events" }
64+
]
65+
},
66+
{
67+
"id": "active-rules",
68+
"type": "table",
69+
"position": { "col": 3, "row": 2, "span_cols": 2 },
70+
"label": "Active Rules",
71+
"data_source": "rpa-elysium://workflow/rules",
72+
"columns": [
73+
{ "key": "name", "label": "Rule" },
74+
{ "key": "patterns", "label": "Patterns" },
75+
{ "key": "match_count", "label": "Matches" },
76+
{ "key": "enabled", "label": "Enabled" }
77+
]
78+
},
79+
{
80+
"id": "event-timeline",
81+
"type": "timeline",
82+
"position": { "col": 1, "row": 3, "span_cols": 4, "span_rows": 1 },
83+
"label": "Event Timeline",
84+
"data_source": "rpa-elysium://workflow/events/timeline",
85+
"time_range": "1h",
86+
"event_types": {
87+
"file_created": { "color": "#22c55e", "icon": "file-plus" },
88+
"file_modified": { "color": "#3b82f6", "icon": "file-edit" },
89+
"file_deleted": { "color": "#ef4444", "icon": "file-minus" },
90+
"file_renamed": { "color": "#8b5cf6", "icon": "file-arrow" }
91+
}
92+
},
93+
{
94+
"id": "action-results",
95+
"type": "event-log",
96+
"position": { "col": 1, "row": 4, "span_cols": 2, "span_rows": 2 },
97+
"label": "Action Results",
98+
"data_source": "rpa-elysium://workflow/actions/recent",
99+
"max_entries": 25,
100+
"show_timestamp": true,
101+
"columns": [
102+
{ "key": "action_type", "label": "Action" },
103+
{ "key": "success", "label": "OK" },
104+
{ "key": "message", "label": "Message" },
105+
{ "key": "affected_paths", "label": "Paths" }
106+
]
107+
},
108+
{
109+
"id": "fsm-state-diagram",
110+
"type": "state-diagram",
111+
"position": { "col": 3, "row": 4, "span_cols": 2 },
112+
"label": "Workflow FSM (proven-fsm)",
113+
"data_source": "rpa-elysium://workflow/fsm/state",
114+
"states": ["idle", "running", "paused", "stopped", "error"],
115+
"transitions": [
116+
{ "from": "idle", "to": "running", "label": "start" },
117+
{ "from": "running", "to": "stopped", "label": "stop" },
118+
{ "from": "running", "to": "error", "label": "fault" },
119+
{ "from": "error", "to": "idle", "label": "reset" }
120+
],
121+
"highlight_current": true
122+
},
123+
{
124+
"id": "queue-status",
125+
"type": "status-indicator",
126+
"position": { "col": 3, "row": 5, "span_cols": 2 },
127+
"label": "HAR Queue Connection (proven-queueconn)",
128+
"data_source": "rpa-elysium://queue/state",
129+
"states": {
130+
"disconnected": { "color": "#6b7280", "icon": "unlink" },
131+
"connected": { "color": "#22c55e", "icon": "link" },
132+
"consuming": { "color": "#3b82f6", "icon": "download" },
133+
"producing": { "color": "#8b5cf6", "icon": "upload" },
134+
"failed": { "color": "#ef4444", "icon": "alert-triangle" }
135+
}
136+
}
137+
],
138+
"refresh_interval_ms": 2000,
139+
"permissions": ["read:workflow", "read:events", "read:actions", "read:fsm", "read:queue"]
140+
}

‎panels/plugin-status/panel.json‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
{
2+
"$schema": "panll-panel/v1",
3+
"panel_id": "rpa-plugin-status",
4+
"name": "Plugin System Status",
5+
"description": "Monitoring panel for the WASM plugin sandbox system — loaded plugins, sandbox resources, execution stats",
6+
"version": "0.1.0",
7+
"category": "plugins",
8+
"layout": {
9+
"type": "grid",
10+
"columns": 3,
11+
"rows": 3,
12+
"gap": "8px"
13+
},
14+
"widgets": [
15+
{
16+
"id": "loaded-plugins",
17+
"type": "counter",
18+
"position": { "col": 1, "row": 1, "span_cols": 1 },
19+
"label": "Loaded Plugins",
20+
"data_source": "rpa-elysium://plugins/count"
21+
},
22+
{
23+
"id": "sandbox-memory",
24+
"type": "gauge",
25+
"position": { "col": 2, "row": 1, "span_cols": 1 },
26+
"label": "Sandbox Memory",
27+
"data_source": "rpa-elysium://plugins/sandbox/memory_usage",
28+
"min": 0,
29+
"max": 67108864,
30+
"format": "bytes",
31+
"thresholds": { "warning": 50331648, "critical": 62914560 }
32+
},
33+
{
34+
"id": "plugin-executions",
35+
"type": "counter",
36+
"position": { "col": 3, "row": 1, "span_cols": 1 },
37+
"label": "Executions",
38+
"data_source": "rpa-elysium://plugins/metrics/total_executions"
39+
},
40+
{
41+
"id": "plugin-list",
42+
"type": "table",
43+
"position": { "col": 1, "row": 2, "span_cols": 3 },
44+
"label": "Registered Plugins",
45+
"data_source": "rpa-elysium://plugins/list",
46+
"columns": [
47+
{ "key": "id", "label": "Plugin ID" },
48+
{ "key": "name", "label": "Name" },
49+
{ "key": "version", "label": "Version" },
50+
{ "key": "actions_count", "label": "Actions" },
51+
{ "key": "permissions", "label": "Permissions" },
52+
{ "key": "memory_limit", "label": "Mem Limit", "format": "bytes" }
53+
]
54+
},
55+
{
56+
"id": "plugin-logs",
57+
"type": "event-log",
58+
"position": { "col": 1, "row": 3, "span_cols": 3 },
59+
"label": "Plugin Execution Log",
60+
"data_source": "rpa-elysium://plugins/logs/recent",
61+
"max_entries": 20,
62+
"show_timestamp": true,
63+
"show_level": true
64+
}
65+
],
66+
"refresh_interval_ms": 5000,
67+
"permissions": ["read:plugins", "read:sandbox"]
68+
}

0 commit comments

Comments
 (0)