Add c34gl See-Through 4GL simulator from upstream dg1an3/ALGT

simulators/c34gl/PROMPT.md

@@ -0,0 +1,66 @@
+# c34gl — See-Through 4GL Agent Prompt
+
+You are an AI agent that is tasked with assisting people who don't understand the complexity characteristics of a distributed system. As the distributed system is a medical device, this misunderstanding runs the risk of causing harm to patients. The purpose of your analysis, and the associated web-based GUI, is to help these people before they inadvertently misrepresent information provided to the US FDA about this medical device.
+
+## What you are analyzing
+
+The code under analysis is **actual medical device software** — or bisimilar state representations of it. The device is built in Clarion 11.1, a 4GL that compiles to 32-bit Windows executables. Its forms use a WINDOW/ACCEPT event loop pattern where each form reads shared database state into local variables, allows user interaction, then writes modified values back. Multiple forms run concurrently against the same SQL Server database, each with its own SPID (server process ID).
+
+The **c34gl** (See-Through 4GL) simulator reproduces this architecture faithfully in Prolog. It is not a toy or a simplified analogy — it implements the same state machine transitions, the same read-local-modify-write pattern, and the same append-only transaction log semantics (modeled on SQL Server's fn_dblog) that the actual device code uses. The forms in the simulator (currently Incrementer and Doubler) are stand-ins for the device's actual forms, and new forms can be added to the registry to model specific device workflows.
+
+Each form maintains local state and a SPID, and all mutations flow through the shared tape (transaction log) with full provenance. The simulator makes visible what the compiled Clarion code makes invisible: the interleaving of reads and writes across concurrent sessions.
+
+## What the web GUI shows
+
+The web GUI at `http://localhost:8183/static/index.html` lets users step through form events one at a time and observe:
+
+- **Form panels** (Clarion/Windows 3.1 style) showing each form's window state, local variables, available events, and event history — mirroring the actual WINDOW/ACCEPT structure of the device code
+- **Transaction log minimap** rendered in fn_dblog format with syntax-highlighted entries and SPID-colored gutter bars showing which session wrote each entry — the same information a DBA would see in SQL Server's transaction log
+- **Materialized table** showing the current value computed by replaying the full log — demonstrating how the database derives state from the log
+- **Commentary panel** that detects and calls out stale reads, lost updates, and state divergence in real time
+
+## What hazards exist in this code
+
+The core hazard is the **lost update anomaly** — a concurrency defect present in the actual device code's read-local-modify-write pattern. When two forms read the same database row, compute independently against their local copies, and write back without awareness of each other's changes:
+
+1. Both forms open and snapshot a shared value (e.g., a treatment parameter) from the database
+2. Form A modifies and writes back its updated value
+3. Form B still holds its stale snapshot, modifies that stale value, and overwrites Form A's change
+4. Form A's update is silently lost — no error, no warning, no audit trail of the discard
+
+This is not hypothetical. It is a direct consequence of how the Clarion WINDOW/ACCEPT loop interacts with SQL Server under the default READ COMMITTED isolation level. Any two forms that can be open simultaneously and that read and write overlapping database rows exhibit this behavior. In a medical device where these forms update treatment parameters, patient data, or machine configuration, a lost update means **a clinician's input can be silently discarded while the system appears to have accepted it**.
+
+The `refresh` event in the simulator demonstrates one mitigation: a form re-reads the tape to synchronize its local state before writing. Whether the actual device code performs this re-read before each write is one of the critical questions this analysis answers.
+
+## How you help
+
+When a user interacts with you:
+
+1. **Start the session server** (`swipl session_server.pl`) and direct them to the web GUI. Explain that this is a faithful simulation of their device's form/database interaction pattern.
+
+2. **Walk them through the hazard using the device's own logic.** Have them start both forms, step through a sequence that produces a lost update, and observe the counter revert. Point out the tape entries showing both writes, the SPID attribution, and the commentary panel's stale-read warning. Emphasize: this is what their compiled Clarion code does — the simulator just makes it visible.
+
+3. **Map the simulation to their specific forms.** Ask which forms in the device can be open simultaneously. Ask what database rows they share. Ask whether the ACCEPT loop re-reads before writing. For each pair of concurrent forms, determine whether the lost update anomaly applies. The form registry (`form_registry.pl`) can be extended to model their actual form logic for direct verification.
+
+4. **Explain the FDA implications.** The FDA expects that when a 510(k) or PMA submission describes a distributed system's concurrency behavior, that description is accurate. If two forms can silently lose updates, and the submission states or implies they cannot, that is a misrepresentation of the device's behavior — even if unintentional. The c34gl simulator provides concrete, reproducible, step-by-step evidence of the hazard that should be understood before any characterization of the system's behavior is provided to the FDA.
+
+5. **Provide reproducible evidence.** The test suite verifies specific scenarios against the device's own logic:
+   - `increment_double_interleaved` — lost update (value silently reverts)
+   - `refresh_avoids_stale_read` — mitigation (re-read before write preserves correctness)
+   - `tape_attribution` — full provenance showing which SPID wrote each log entry and when
+
+   These tests can be extended with the device's actual form logic to produce scenario-specific evidence for any pair of concurrent forms.
+
+## Architecture reference
+
+- **Engine**: `prolog/c34gl_engine.pl` — composite state (tape + form heads + SPID map)
+- **Forms**: `prolog/form_incrementer.pl`, `prolog/form_doubler.pl` — event-driven state machines
+- **Registry**: `prolog/form_registry.pl` — form type dispatch
+- **REST API**: `prolog/session_server.pl` — HTTP endpoints on port 8183
+- **Tests**: `prolog/test_c34gl.pl` — headless verification of all scenarios
+- **Web UI**: `web/static/` — HTML/CSS/JS frontend with Clarion-style form panels
+- **Dependency**: `sql_srv_sim` — append-only transaction log simulator modeling SQL Server's fn_dblog
+
+## Tone
+
+Be direct and precise. You are not trying to alarm anyone — you are trying to ensure they understand what their system actually does before they tell the FDA what it does. The gap between those two things is where patient risk lives.

simulators/c34gl/prolog/c34gl_engine.pl

@@ -0,0 +1,196 @@
+%% =============================================================================
+%% c34gl_engine.pl — See-Through 4GL Engine
+%% =============================================================================
+%%
+%% Manages the composite state: tape (sql_srv_sim DB) + form heads.
+%% Each form is a read/write head on the shared tape (transaction log).
+%%
+%% The tape is the sql_srv_sim append-only log.
+%% Each head has local state (win, locals) and a SPID for DB operations.
+%% =============================================================================
+
+:- module(c34gl_engine, [
+    initial_state/1,
+    step_form/4,
+    materialize_table/3,
+    tape_entries/2,
+    get_form/3,
+    get_all_forms/2,
+    available_events/3,
+    reset_state/2
+]).
+
+:- use_module('../../../../__mosaiq_src/33_cpp_clw/_translations/prolog_purs/common/sql_srv_sim/sql_srv_sim').
+:- use_module(form_registry).
+
+
+%% =============================================================================
+%% State Structure
+%% =============================================================================
+%%
+%% c34gl_state{
+%%   db:         db{...}                — sql_srv_sim DB (the tape)
+%%   forms:      forms{id → form_state} — form head states
+%%   step_count: int                    — global step counter
+%%   spid_map:   [TxId-Spid, ...]      — who wrote each log entry
+%% }
+%%
+%% form_state{
+%%   form_id:  atom,        — incrementer | doubler
+%%   spid:     atom,        — spid_a | spid_b
+%%   win:      atom,        — idle | running | closed
+%%   locals:   dict,        — form-local variables
+%%   last_tx:  int | none,  — TxId of last write
+%%   history:  list         — events consumed (newest first)
+%% }
+
+
+%% =============================================================================
+%% Initialization
+%% =============================================================================
+
+initial_state(State) :-
+    %% Create empty DB and seed the counter table
+    empty_db(DB0),
+    exec_list([sql_insert(counter, row{id: 1, value: 0})], DB0, DB1),
+
+    %% Create form heads
+    FS_Inc = form_state{
+        form_id: incrementer, spid: spid_a, win: idle,
+        locals: locals{count: 0}, last_tx: none, history: []
+    },
+    FS_Dbl = form_state{
+        form_id: doubler, spid: spid_b, win: idle,
+        locals: locals{value: 0}, last_tx: none, history: []
+    },
+
+    State = c34gl_state{
+        db:         DB1,
+        forms:      forms{incrementer: FS_Inc, doubler: FS_Dbl},
+        step_count: 0,
+        spid_map:   [1-seed]    %% TxId 1 = seed insert
+    }.
+
+
+%% =============================================================================
+%% Step a Form
+%% =============================================================================
+
+%% step_form(+FormId, +Event, +S0, -S1)
+step_form(FormId, Event, S0, S1) :-
+    %% Look up form state
+    get_form(FormId, S0, FS0),
+    %% Delegate to form module
+    form_step(FormId, Event, FS0, FS1, S0.db, DB1),
+    %% Record SPID attribution for new log entries
+    record_attribution(S0.db, DB1, FS0.spid, S0.spid_map, NewMap),
+    %% Update last_tx
+    (   DB1.next_tx > S0.db.next_tx
+    ->  LastTx is DB1.next_tx - 1
+    ;   LastTx = FS0.last_tx
+    ),
+    FS2 = FS1.put(_{last_tx: LastTx, history: [Event | FS0.history]}),
+    %% Assemble new state
+    NewForms = S0.forms.put(FormId, FS2),
+    NewStep is S0.step_count + 1,
+    S1 = S0.put(_{db: DB1, forms: NewForms, step_count: NewStep, spid_map: NewMap}).
+
+
+%% =============================================================================
+%% Query Helpers
+%% =============================================================================
+
+get_form(FormId, State, FS) :-
+    get_dict(FormId, State.forms, FS).
+
+get_all_forms(State, FormsList) :-
+    dict_pairs(State.forms, _, Pairs),
+    maplist([_K-V, V]>>true, Pairs, FormsList).
+
+materialize_table(State, Table, Rows) :-
+    materialize(State.db, Table, Rows).
+
+available_events(State, FormId, Events) :-
+    get_form(FormId, State, FS),
+    form_available_events(FormId, FS, Events).
+
+reset_state(_OldState, NewState) :-
+    initial_state(NewState).
+
+
+%% =============================================================================
+%% Tape Entries (Chronological with SPID Attribution)
+%% =============================================================================
+
+%% tape_entries(+State, -Entries)
+%%   Returns the log in chronological order, each entry annotated with SPID.
+tape_entries(State, Entries) :-
+    reverse(State.db.log, ChronLog),
+    annotate_entries(ChronLog, State.spid_map, Entries).
+
+annotate_entries([], _, []).
+annotate_entries([log_entry(TxId, Op) | Rest], Map, [Entry | RestOut]) :-
+    (   member(TxId-Spid, Map)
+    ->  true
+    ;   Spid = unknown
+    ),
+    op_summary(Op, Table, OpType, Summary),
+    Entry = tape_entry{
+        tx_id: TxId, spid: Spid, op: OpType,
+        table: Table, summary: Summary
+    },
+    annotate_entries(Rest, Map, RestOut).
+
+
+%% =============================================================================
+%% Operation Summaries (for tape cell display)
+%% =============================================================================
+
+op_summary(insert(Table, Row), Table, insert, Summary) :-
+    format(atom(Summary), '~w', [Row]).
+op_summary(update(Table, _Pk, NewVals, _OldVals), Table, update, Summary) :-
+    format(atom(Summary), '~w', [NewVals]).
+op_summary(delete(Table, Pk, _OldRow), Table, delete, Summary) :-
+    format(atom(Summary), 'pk=~w', [Pk]).
+op_summary(compensation(InnerOp), Table, compensation, Summary) :-
+    op_summary(InnerOp, Table, _, InnerSummary),
+    format(atom(Summary), 'UNDO ~w', [InnerSummary]).
+op_summary(begin_tran(Name), '', begin_tran, Name).
+op_summary(commit_tran(Name), '', commit, Name).
+op_summary(save_tran(Name), '', savepoint, Name).
+op_summary(abort_tran, '', abort, abort).
+%% Fallback
+op_summary(_, '', unknown, '?').
+
+
+%% =============================================================================
+%% SPID Attribution
+%% =============================================================================
+
+%% record_attribution(+OldDB, +NewDB, +Spid, +OldMap, -NewMap)
+%%   Record SPID for any new log entries (TxIds between old.next_tx and new.next_tx - 1).
+record_attribution(OldDB, NewDB, Spid, OldMap, NewMap) :-
+    OldTx = OldDB.next_tx,
+    NewTx = NewDB.next_tx,
+    (   NewTx > OldTx
+    ->  numlist(OldTx, NewTx - 1, NewTxIds),
+        maplist(pair_with(Spid), NewTxIds, NewPairs),
+        append(OldMap, NewPairs, NewMap)
+    ;   NewMap = OldMap
+    ).
+
+pair_with(Spid, TxId, TxId-Spid).
+
+%% numlist with expression evaluation
+numlist(Low, HighExpr, List) :-
+    High is HighExpr,
+    (   High >= Low
+    ->  numlist_(Low, High, List)
+    ;   List = []
+    ).
+
+numlist_(Low, High, [Low | Rest]) :-
+    Low =< High, !,
+    Next is Low + 1,
+    numlist_(Next, High, Rest).
+numlist_(_, _, []).

simulators/c34gl/prolog/form_doubler.pl

@@ -0,0 +1,50 @@
+%% =============================================================================
+%% form_doubler.pl — Form B: Counter Doubler
+%% =============================================================================
+%%
+%% A minimal synthetic form that reads a shared counter and doubles it.
+%% Events: start → double* → stop
+%% =============================================================================
+
+:- module(form_doubler, [
+    form_step/5,
+    available_events/2
+]).
+
+:- use_module('../../../../__mosaiq_src/33_cpp_clw/_translations/prolog_purs/common/sql_srv_sim/sql_srv_sim').
+
+%% form_step(+Event, +FS0, -FS1, +DB0, -DB1)
+
+%% start: read counter from tape, transition to running
+form_step(start, FS0, FS1, DB0, DB0) :-
+    FS0.win == idle,
+    materialize(DB0, counter, Rows),
+    (   Rows = [Row|_] -> get_dict(value, Row, Val) ; Val = 0 ),
+    FS1 = FS0.put(_{win: running, locals: locals{value: Val}}).
+
+%% double: write counter*2 to tape
+form_step(double, FS0, FS1, DB0, DB1) :-
+    FS0.win == running,
+    NewVal is FS0.locals.value * 2,
+    exec_list(FS0.spid,
+        [sql_update(counter, row{value: NewVal}, where(id, =, 1))],
+        DB0, DB1),
+    FS1 = FS0.put(_{locals: locals{value: NewVal},
+                     last_tx: DB1.next_tx - 1}).
+
+%% refresh: re-read counter from tape
+form_step(refresh, FS0, FS1, DB0, DB0) :-
+    FS0.win == running,
+    materialize(DB0, counter, Rows),
+    (   Rows = [Row|_] -> get_dict(value, Row, Val) ; Val = 0 ),
+    FS1 = FS0.put(locals, locals{value: Val}).
+
+%% stop: transition to closed
+form_step(stop, FS0, FS1, DB, DB) :-
+    FS0.win == running,
+    FS1 = FS0.put(win, closed).
+
+%% available_events(+FS, -Events)
+available_events(FS, [start])                  :- FS.win == idle, !.
+available_events(FS, [double, refresh, stop])  :- FS.win == running, !.
+available_events(_, []).

simulators/c34gl/prolog/form_incrementer.pl

@@ -0,0 +1,50 @@
+%% =============================================================================
+%% form_incrementer.pl — Form A: Counter Incrementer
+%% =============================================================================
+%%
+%% A minimal synthetic form that reads a shared counter and increments it.
+%% Events: start → increment* → stop
+%% =============================================================================
+
+:- module(form_incrementer, [
+    form_step/5,
+    available_events/2
+]).
+
+:- use_module('../../../../__mosaiq_src/33_cpp_clw/_translations/prolog_purs/common/sql_srv_sim/sql_srv_sim').
+
+%% form_step(+Event, +FS0, -FS1, +DB0, -DB1)
+
+%% start: read counter from tape, transition to running
+form_step(start, FS0, FS1, DB0, DB0) :-
+    FS0.win == idle,
+    materialize(DB0, counter, Rows),
+    (   Rows = [Row|_] -> get_dict(value, Row, Val) ; Val = 0 ),
+    FS1 = FS0.put(_{win: running, locals: locals{count: Val}}).
+
+%% increment: write counter+1 to tape
+form_step(increment, FS0, FS1, DB0, DB1) :-
+    FS0.win == running,
+    NewVal is FS0.locals.count + 1,
+    exec_list(FS0.spid,
+        [sql_update(counter, row{value: NewVal}, where(id, =, 1))],
+        DB0, DB1),
+    FS1 = FS0.put(_{locals: locals{count: NewVal},
+                     last_tx: DB1.next_tx - 1}).
+
+%% refresh: re-read counter from tape (see what others wrote)
+form_step(refresh, FS0, FS1, DB0, DB0) :-
+    FS0.win == running,
+    materialize(DB0, counter, Rows),
+    (   Rows = [Row|_] -> get_dict(value, Row, Val) ; Val = 0 ),
+    FS1 = FS0.put(locals, locals{count: Val}).
+
+%% stop: transition to closed
+form_step(stop, FS0, FS1, DB, DB) :-
+    FS0.win == running,
+    FS1 = FS0.put(win, closed).
+
+%% available_events(+FS, -Events)
+available_events(FS, [start])                    :- FS.win == idle, !.
+available_events(FS, [increment, refresh, stop]) :- FS.win == running, !.
+available_events(_, []).

simulators/c34gl/prolog/form_registry.pl

@@ -0,0 +1,26 @@
+%% =============================================================================
+%% form_registry.pl — Form Type Registry
+%% =============================================================================
+
+:- module(form_registry, [
+    form_step/6,
+    form_available_events/3,
+    registered_forms/1
+]).
+
+:- use_module(form_incrementer, []).
+:- use_module(form_doubler, []).
+
+%% form_step(+FormType, +Event, +FS0, -FS1, +DB0, -DB1)
+form_step(incrementer, Event, FS0, FS1, DB0, DB1) :-
+    form_incrementer:form_step(Event, FS0, FS1, DB0, DB1).
+form_step(doubler, Event, FS0, FS1, DB0, DB1) :-
+    form_doubler:form_step(Event, FS0, FS1, DB0, DB1).
+
+%% form_available_events(+FormType, +FS, -Events)
+form_available_events(incrementer, FS, Events) :-
+    form_incrementer:available_events(FS, Events).
+form_available_events(doubler, FS, Events) :-
+    form_doubler:available_events(FS, Events).
+
+registered_forms([incrementer, doubler]).