# Harness laws: session state

Shared rules (what a law secures, adversary, H1 to H6): [harness.md](harness.md).

### S1. The session tree

One tree holds a session's state. Node: id, parent, value. Node id > parent id. Root (id `0`) parents the top nodes; the root is not a node.

1. A record changes the tree. `Do` holds one checked change: `Put` sets a node; `Del` removes a node and its subtree. Rejected: `Put` whose parent is not root or a node; `Del` of the root. A rejected record changes nothing.
2. `Rewind` holds exact changes back to an earlier tree. Rejected if the result is not a sound tree.
3. The journal keeps every record in order. Replay of the journal = live tree; replay of a prefix = snapshot. Cursor = number of records.
4. A rewind plan compares live tree and snapshot: stops each node that goes, starts each node that comes back, restores each node that changes.

The state tree is the session tree made by the storage's commits. Disk format unchanged: the tree comes from the commits in `main.jsonl`.

1. Each stored record is a node: conversation, entry, task, submission, document. Conversation: under the conversation of its owning task, else of its fork source, else root. Entry, task, submission: under their conversation. Session document: root. Conversation document: its conversation. Task document: its task's conversation.
2. So each parent is root or a conversation; no commit deletes a conversation. History drops early states of a terminal task, yet each node finds its parent: a build from history first learns each task's conversation.
3. Each change of a commit is one `Do`: new or changed record `Put`; retired document `Del`; copied document `Put`. Changes come unordered: a `Put` waits for its parent.
4. A change whose parent or node is missing is a typed error (`StateError`): tree unchanged, session logs it. Nothing dropped silently.
5. Value: conversation, task, submission = record as JSON. Entry = kind, conversation, head, task. Document = kind, key, scope, creating commit, last changing commit.
6. Ids go in first-seen order. A commit at or before the tree's last commit counts once.
7. On open, storage keeps its replayed history; a background task builds the tree from it, then records each Harness commit. The commit listener only queues, so no commit waits for the tree. Open and attach do not wait for the build; a read does. A panic in build or record stops the tree: it ends its commit subscription; reads get an error.
8. Ids and cursor hold for one worker. A rebuild can see records in another order; after a worker restart a client reads a new snapshot.

Wire: one-shot read, opt-in subscription.

1. `get_state_tree`: snapshot (with cursor), or records after cursor `since`. `get_state_rewind_plan`: effects of a rewind to a cursor.
2. `subscribe_state_tree`: same reply. The supervisor adds the connection to the session's state tree subscribers before the worker reads the tree; then each commit that adds records sends a `state_tree_update` frame (`from`, `cursor`, records). Frames cover every record after the reply's cursor.
3. Frames can repeat reply records. Client skips a frame with `cursor` <= its own; else applies records from its own cursor. `from` > client cursor = loss: subscribe again.
4. `unsubscribe_state_tree` or a closed connection ends it. Non-subscribers never get the frame. The frame is not a session event: no event sequence, so other clients' replay cursors are unchanged. A direct session client of the worker never gets it.

Model: `bend/tree.bend`. Laws: `laws/tree.bend` (S1). Proofs: `proof/tree/`. All laws universal: any record (any put, valid or not, any delete, any rewind ops).

| Law | Says |
| --- | --- |
| `tree_apply_sound` | Sound tree stays sound: ids ordered, no orphan, no cycle (S1.1, S1.2). |
| `tree_replay_sound` | Any journal → sound tree (S1.3). |
| `tree_snapshot` | Prefix snapshot + later records = whole-journal tree (= live tree for a client) (S1.3). |
| `tree_rewind_reaches` | Rewind by diff live→target = target exactly (S1.2, S1.4). |
| `tree_rewind_still` | Rewind to live = no changes (S1.4). |
| `tree_rewind_minimal` | Rewind touches only nodes differing between live and target (S1.4). |
| `tree_delete_removes` | Delete removes its node (S1.1). |
| `tree_delete_only_below` | Delete removes only its subtree (S1.1). |
| `tree_delete_within` | Delete changes no kept node (S1.1). |
| `tree_put_sets` | Put under root or a node sets it (S1.1). |
| `tree_put_keeps_others` | Put changes no other node (S1.1). |
| `tree_core_tree` | Compiled core's tree after any journal (key map, splits halve the key range) = the journal's tree (S1.3). |
| `tree_core_answer` | After any journal, the core answers each record as the model decides: taken or kept; a delete cuts exactly the nodes it removes (S1.1, S1.2). |
| `tree_core_note` | A record steps the core to the core of the journal with that record appended, so core laws hold for the live core (S1.3). |
| `tree_core_plan` | Core's rewind plan to the tree after the first n records = what the live→that-tree diff does to each node's work (S1.4). |
| `tree_core_snap` | Core's snapshot after the first n records = their replay (S1.3). |
| `tree_core_plan_keeps`, `tree_core_snap_keeps` | Rewind plan and snapshot leave the core unchanged. |
| `tree_ffi_ask_round_trip` | Every record and question the Rust journal writes reads back in the core's entry (`bend/ffi_tree.bend`). |
| `tree_ffi_step` | An entry step answers the core's answer, keeps the core's next state. |
| `tree_ffi_open` | The entry opens the empty core with the halves the journal sends. |
| `tree_ffi_malformed`, `tree_ffi_trailing`, `tree_ffi_refused`, `tree_ffi_open_malformed`, `tree_ffi_open_trailing` | Any other input answers the wire's error form, never a default; a step keeps the core. |
| `tree_ffi_example` | Tags and field order Rust writes and reads. |

Code: `eukhe-durable/src/tree/mod.rs` `SessionTree`, `TreeRecord`, `TreeOp`; `tree/journal.rs` `Journal` (`push`, `snapshot_at`, `rewind_plan`: shell over a stepper of the compiled Bend core, `bend/ffi_tree.bend` through `eukhe-bend`; equal values share one value index); `tree/state.rs` `StateTree` (`record`, `from_history`, `record_writes`, `records_since`, `snapshot_at`, `rewind_plan`); `storage/jsonl/storage.rs` `CommitHistory`, `JsonlStorage::take_history`; `eukhe-core/src/durable/state_tree.rs` `LiveStateTree`; `eukhe-daemon/src/worker/state_tree.rs` (`get_state_tree`, `subscribe_state_tree`, `get_state_rewind_plan`, `state_tree_update`); `supervisor/clients.rs` (subscription, `state_tree_subscribers`); `supervisor/supervision.rs` (frame routing); `peer.rs` `ConnectionRole::streams`; `eukhe-cli/src/daemon_command.rs` `run_state` (`eukhe state`, `--follow`, `rewind-plan`).

Tie: the journal decides every record, rewind plan and snapshot by one step of its stepper (the compiled model), whose state is the live tree and the journal; a record costs its change and a lookup (a delete walks only its node and nodes with a parent of its key or more), not the tree.

Tests (glue around the core): `tree::journal::tests::the_live_tree_follows_the_core`, `tree::state::tests::commits_build_the_tree_with_parents_first`, `storage_writes_build_the_same_journal_as_publications`, `a_rewind_plan_stops_starts_and_restores`, `a_history_gives_every_node_its_conversation`, `an_unknown_parent_or_node_is_an_error`; `jsonl_storage::keeps_the_replayed_and_later_commits_until_the_history_is_taken`; `durable::open::tests::the_state_tree_follows_the_history_and_the_live_commits`; daemon `get_state_tree_answers_the_sessions_tree`, `subscribe_state_tree_streams_records_to_its_connection_only`; `peer::tests::peer_session_attach_gates_event_stream`.

Not modelled: commit→record map (S1, second list); tested.

### D2. Storage and cron

Storage = a directory with one commit log, `main.jsonl`; opened with fsync on in each worker.

1. Commit: append one line to `main.jsonl`, flush the file. First commit after open also flushes the storage directory (entry of `main.jsonl`); open flushes the parent directory (entry of the storage directory). Only then is the commit acknowledged.
2. A crash can come at any step: keeps flushed bytes and any prefix of unflushed bytes; can lose unflushed directory entries.
3. Open reads complete lines only; cuts a torn tail (bytes after the last newline), never read as a commit.

A new storage (legacy import, fork) builds in a staging directory beside its place: `.<name>.import-<uuid>` or `.<name>.fork-<uuid>`.

1. The builder creates `<staging>.lock` first and holds an exclusive lock until the build ends.
2. Publish renames staging into place only if no entry has the name (`RENAME_NOREPLACE`). An existing entry, even an empty directory, stays; the build fails with "exists".
3. Sweep: at boot and every 5 minutes, every depth of the sessions directory and `session-artifacts`; never enters a storage, symlink or leftover. Removes a staging directory, delete tombstone, or lock file without its directory, when no live process holds its lock and it is untouched for a day.

Listing shows storage directories (not hidden, with `main.jsonl` and a readable cwd) and legacy files `<stem>.jsonl`. A legacy file lists under its stem (the storage name every open imports it into), only while no directory has that name. So a session lists once, before and after import.

Models: `bend/log.bend`, `bend/staging.bend`. Laws: `laws/log.bend`, `laws/staging.bend`. Proofs: `proof/log/` and `proof/staging/`. The commit log's rules run as compiled Bend (`bend/log.bend` section "The rules", entry `bend/ffi_log.bend`, id 33): what an open does with a file (`tail`, from its length and last newline), and the plan of steps at open and per commit (`Store.open`, `Store.commit`, a stepper); `JsonlStorage` reads the facts and does the steps (`storage/jsonl/plan.rs`).

| Law | Says |
| --- | --- |
| `log_reads_lines` | Open reads exactly the complete lines, in order; never a torn tail. |
| `log_ack_durable` | Post-crash log = old log + all acked commits + maybe more. |
| `log_only_commits` | Post-crash log = old log + prefix of tried commits. |
| `log_open_cuts_the_torn_tail`, `log_open_keeps_the_complete_lines`, `log_open_refuses_odd_facts` | An open keeps a file whose bytes are all in complete lines, cuts any other to exactly the bytes of the lines open reads (`Lg.recover`); refuses facts no file has. |
| `log_plan_runs_the_model`, `log_plan_ack_durable`, `log_plan_only_commits` | The plan of an fsync open and its commits, cut after any step, is the model's epoch (`Lg.run`): acked commits survive, only a prefix of commits is read. |
| `log_commit_plan`, `log_open_plan` | Every commit's plan for every storage and sidecar list: records, (fsync) their flushes and a directory flush while an entry is new, marker, (fsync) its flush and a directory flush while main.jsonl's entry is new, ack. |
| `log_ffi_*`, `log_stepper_*` | The entry answers the requests Rust writes with the rule's decisions, the error form to anything else; a refused step keeps the state. |
| `publish_never_overwrites` | Taken name: publish fails, no change. |
| `publish_moves` | Free name: publish moves the storage. |
| `sweep_never_live` | Never removes a live-locked entry. |
| `sweep_never_young` | Never removes an entry touched within the day. |
| `sweep_stays_out` | Never removes an unreached entry. |
| `sweep_reaches_every_depth` | Removes every free, stale, reached leftover. |
| `list_one_location` | No name listed as both storage and legacy file. |
| `list_import_lists_storage` | After import, the stem lists as storage. |
| `list_import_keeps_others` | Import changes no other listing. |
| `publish_settles`, `publish_settle_refines` | The real publish verdict: taken exactly when the rename without replacement met an entry; the model's publish. |
| `meet_exact`, `meet_minted_*`, `sweep_stays_out_real` | What the sweep does with each entry of a listing (enter, keep, judge a leftover or an orphan lock file), by name and type. |
| `judge_exact`, `judge_refines`, `sweep_never_live_real`, `sweep_never_young_real`, `sweep_takes_stale_free_real` | The plan for a judged entry from its lock probe and times (a day, to the nanosecond); the model's `removes`. |
| `scan_*` (`laws/listing.bend`) | Which entry of the sessions directory is a session, under which id; one location per id; imports. |
| `rows_*` | The listing: every candidate with a cwd and a file, once, as its entry, newest first, then by id, then by place; unread facts of skipped entries ignored. |
| `staging_entry_*` | The entry answers the requests Rust writes with the rule's decisions, the error form to anything else. |

Code: `eukhe-durable/src/storage/jsonl/storage.rs` (`JsonlStorage::open`, `run_plan`, commit path, `read_lines`), `storage/jsonl/plan.rs` (the calls of the compiled core); `eukhe-core/src/durable/staging.rs` (`lock_staging`, `publish`, `sweep_stale_staging_dirs`: the facts and the steps), `durable/staging/rule.rs` (the calls of the compiled core, entry `bend/ffi_staging.bend`); `platform/fs.rs` `rename_no_replace`; `durable/discovery.rs` `list_sessions`; `eukhe-daemon/src/session_archive.rs` (sweep loop).

Crash test of the commit log's IO shell: `storage::jsonl::crash::a_crash_at_any_step_keeps_the_acknowledged_commits_and_only_commits` (real `JsonlStorage` over a file system that loses power after any step, every crash point of a three-commit epoch, 120 random histories: the log after is the log before, the acked commits, then only a prefix of the commits).

Tests: `durable::staging::tests::publish_never_replaces_an_entry_at_the_target`, `a_held_staging_dir_is_never_swept`, `sweeps_leftovers_at_every_depth_it_owns`.

#### The cron store

All processes of an agent directory share the cron jobs file (`cron-jobs.json`, or a session's `scheduled-jobs.json`). `AgentCronJobStore` (crates/eukhe-core/src/cron/store/):

1. A claim belongs to its owner. Each dispatch record names its claiming process (pid and start identity, `ProcessIdentity`). Recovery clears a claim only if it is this process's and its run is no longer live (pass unwound), or its owner is dead. Another process's live claim stays.
2. A one-shot job completes only by its run's finish step, or by recovery of a claim whose run ended. A claim never completes it.
3. Nothing dropped. Unparseable job or claim records, and unknown top-level keys, stay as they are. A file that exists but cannot be read or parsed is never overwritten: the next update moves it to `<name>.corrupt-<ms>-<id>` and starts empty. Only a missing file reads as empty.
4. A failing job stops. Each failure delays the next run by 2, 4, 8, 16, 32, then 60 minutes (never before schedule); the pause never shrinks in a streak. After `FAILURE_STOP_AFTER` (8) failures in a row: paused with its error; cron list shows `paused`, `failures=8`, the error. Only a user action restarts it (resume sets the count to 0). A good run sets the count to 0. Failure 8 comes about three hours after failure 1; the last two pauses are one hour each: a cause that lasts this long is not a short outage.

Model: `bend/cron.bend`. Laws: `laws/cron.bend` (`cron_fires_once`, `cron_once_finished_after_end`, `cron_never_drops`, `cron_claim_owned`, `cron_backoff_bounded`). Proofs: `proof/cron/`.

Bridge: `cron::store::bridge::the_rust_cron_store_equals_the_bend_model`: 3 simulated processes (own store, owner identity, liveness seam, fake clock), one file, byte-equal to `bridge/bridge_cron.bend`. Not modelled: cron expressions (model: one-shot, interval); freshness merge of whole-list writes (bridge steps one at a time).

Tests (`cron::store::jobs::tests`): `a_pass_of_another_process_keeps_a_live_claim`, `a_one_shot_is_not_completed_while_it_runs`, `an_unread_job_survives_a_create`, `a_corrupt_file_is_moved_aside`, `a_failing_job_stops_after_the_cap`.