eukhe
Coding agent with a memory of all things
Star 0
Fork 0
Watch
eukhe docs tools.md
53 kB · 525 lines
Markdown
at bend/stackfix

Harness laws: tool surface #

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

S7. The tool surface #

The model can call: the roster tools, the tools behind dyn, the internal URLs, the shell.

  1. The roster is the tool list each request sends. It is fixed when the session opens, before its first request. After that, the harness rejects each roster change with the typed error RosterFixed:

    • an install or uninstall of an extension that changes the tools the model sees;
    • a configure of tools, modelTools or extensions;
    • an add_tools of a tool round.

    Each request sends the same roster, so the prompt cache stays valid.

  2. A later tool (an MCP server tool, a host tool that joins) does not go into the roster. The roster tool dyn reaches it:

    • dyn without name lists the dynamic tools;
    • dyn with name and arguments runs one;
    • mcp/<server>/<tool> is a tool of an MCP server the user configured; the kernel's MCP client runs it;
    • a host tool joins with ToolSurface::join and leaves with ToolSurface::quit. A tool that left is not reachable.

  3. Each schema the harness sends has the intent parameter i (optional, first) and a version of 1 or more: the annotation title: "v<n>" in the schema. Every wire API keeps it. At open the session builds every schema: it adds i if missing, keeps each declared parameter in its place, and sets the declared version (1 if none). Building a built schema changes nothing. codemode gets i and v1 this way.

  4. report_issue (behind dyn) is the AutoQA path. An agent reports a tool that failed or did not do what its description says, with the arguments tool and description. The session stores the report as a display-only row of custom type eukhe.tool_issue. The user sees the row; the model context does not get it.

  5. Internal URLs. The read tool (and the kernel read()) accepts scheme://path in place of a file path:

    URL Reads
    repo://<path> a file or directory under the workspace root (the session's working directory)
    skill://<name>/<path> a file under the directory of skill name
    skill://<name> its SKILL.md
    agent://<name|id> the whole chat of a subagent the conversation started
    memory:// the chat view
    memory://<id> message id whole (with its images)
    memory://<id>/<n> line id+n
    mcp://<server> the resource list of a server
    mcp://<server>/<uri> one resource (text; a binary part is a note with its size and MIME type), bounded like any read
    ssh://<host>/<path> one remote text file (rules: item 9)
    • A repo:// or skill:// read is a normal file read: [path#TAG] header, lines are edit anchors.
    • An mcp:// server must be one of the session's generic MCP servers.
    • An unknown scheme gets the rejection scheme.
    • glob rejects all schemes; grep does not find a scheme path.

  6. Confinement. A URL path is a list of /-separated segments under the root of its scheme. .. goes up one segment; . and an empty segment do not move.

    • A path above its root gets the rejection escapes. It is never clamped to the root.
    • A path that stays under its root resolves.
    • After this lexical check, a repo:// or skill:// read resolves the real path (follows symlinks) and requires it under the real path of the root. A symlink out of the root also gets escapes. This guard is against the filesystem; the model stays the lexical rule.
    • An ssh:// path has one of two roots on its host: the remote /, or the remote home when the first segment is exactly ~. eukhe cannot see the remote filesystem, so it does not check a remote symlink.
    • A plain file path is not confined (unchanged): absolute paths and .. from the working directory still read any file.
    • lexical_normalize keeps the filesystem rule (/.. is /) and is not used for URL paths.

  7. The shell and the approval gate. The bash tool (bash@1, extension eukhe.shell) is in the roster at open. It runs a script in process (crate eukhe-shell), not a system shell per script.

    • A script is a list of steps. A step is one simple command. Steps join with ;, newline, &&, ||, |.
    • Redirections per step: <, >, >>, 2>&1, &>.
    • Expansions: $NAME, ${NAME}, $?, a leading ~, the patterns *, ?, [...].
    • Built in: cat, ls, head, tail, wc, echo, pwd, mkdir, rm, rmdir, touch, cp, mv; grep on the ripgrep engine (grep-regex, grep-searcher). All other commands, and these with options the shell does not know, run as external processes.
    • Each external process gets its own process group and this environment: the daemon worker's environment, plus the session values (EUKHE_CODING_AGENT_DIR; EUKHE_CHAT_MEMORY in a chat-memory session), minus each credential (kernel::manager::local_env over durable::rlm::session_env).
    • A credential is a provider credential the provider code reads (eukhe_ai::env_api_keys::credential_env_vars, any case), or a name whose upper case contains API_KEY, APIKEY, TOKEN, SECRET, PASSWORD, PASSWD, PASSPHRASE, CREDENTIAL, PRIVATE_KEY or ACCESS_KEY.
    • A local kernel gets the same environment, but keeps the credentials the user's MCP config reads (a bearerTokenEnvVar, a stdio {"env": NAME} reference, an mcp:* key in auth.json that names a variable). It never keeps a provider credential. Runs as the compiled model bend/child_env.bend (kernel::manager::child_env calls entry bend/ffi_child_env.bend). Laws (G3): laws/child_env.bend.
    • Pipeline commands run at the same time, joined by OS pipes; the kernel pipe buffer limits each pipe. When a command stops, its input pipe closes, and the writer to that pipe stops too: an external process gets SIGPIPE, a shell command stops with status 141. Thus yes | head -n 3 stops.
    • A script with other syntax (control flow, functions, subshells, command substitution, here-documents, background jobs) is one exec step; bash -c runs it.
    • The tool obeys the S2 limits. Output goes through the call's Truncation as the steps write it: the result keeps output within the cap; the output_bounded diagnostic counts each dropped byte. With the opt-out, the result keeps all output.
    • A call blocks for the blocking budget (toolBlockingBudgetMs) at most. A longer script becomes a job (JobKind::Shell) in the session's JobTable; the call settles detached with the output so far and the job id. The script continues, and a gated step still asks the user. When the script ends, it settles its job and sends a JobSettled::Shell row ([job-settled job:ID status:S] and the bounded output) through the job-settled wake, as a detached cell does.
    • The job's kill stops the script and kills the process group of each running external process; the job settles killed.

  8. Each step has a set of effects: read, write, exec, net, outside, protected, secret. A table in eukhe-shell (effect.rs) gives a command's effects from its name, the git subcommand and some options. A command not in the table is exec.

    • Each redirection adds the effects of its target: a write inside the workspace is write; outside it, write and outside; to a protected path (S7 G1: eukhe's own settings and credentials, a .git directory, a directory on PATH, an ancestor of a protected or secret entry), write and protected. A read of a secret (ssh keys, credential stores) is read and secret.
    • Paths a step names add effects: a word that is or holds a secret (cat ~/.ssh/id_ed25519, grep -r KEY ~) adds secret. For a command that writes, a word outside the workspace adds outside; a protected word adds protected.
    • The working directory adds secret (when it holds one) only to a command that reads it because it names no path of its own: ls, du, find with no starting point, rg (the first operand is the pattern unless -e, -f, --regexp, --file or --files gives it), grep -r/-R (the same), git ls-files, and git grep with no pathspec after -- (an operand before -- may be a revision). An option whose value may be the next word takes it, so the path count errs low. In the home dir, echo hi, date or git -C repo log has no secret effect; ls or rg x has.
    • Every other table command reads only what it names or its input.
    • A script outside the grammar is one step with exec and every effect of every command it holds (subshells, command substitutions, pipelines inside control flow).

    A read step only reads. These rules make sure of that:

    • A program name with / (./cat, bin/stat, /usr/bin/rm) is exec: the shell runs that file, whatever its name.
    • A step with an assignment (PATH=./bin stat f, X=1) is exec, and export with an operand is exec. The environment can make a reading command run another program (PATH, LD_PRELOAD, LESSOPEN, GIT_*).
    • git: before the subcommand, only -C DIR and options that set no configuration and no program (--no-pager, -P, the pathspec options, --no-optional-locks, --no-replace-objects) are allowed. Any other (-c, --config-env, --exec-path, --git-dir, -p) is exec. Repository config can make git run a program (fsmonitor, hooks, pager, clean filters, external diff and textconv drivers, signature programs, ssh commands, credential helpers), so:
      • read subcommands: cat-file, count-objects, describe, for-each-ref, grep, log, ls-files, ls-tree, merge-base, name-rev, rev-list, rev-parse, shortlog, show, show-ref, version, diff --cached, and branch and symbolic-ref that only show;
      • write: branch, symbolic-ref, update-ref and init that change refs;
      • the shell runs each of these with GIT_UNTRUSTED_REPO_ARGS (eukhe-shell, also used by eukhe's own git probes: no fsmonitor, no hooks, no signature check, no pager, no fetch of missing objects), and diff, log, show with --no-ext-diff --no-textconv;
      • each of them is exec with --textconv, --ext-diff, --filters, a signature option or format (%G, signature, a pretty.<name> alias), describe --dirty/--broken, ls-files -m, grep -O, branch --edit-description;
      • every other subcommand is exec: status, work-tree diff, blame and add hash work-tree files through the clean filters, which no argument can switch off; commit, merge, rebase -x, bisect run, aliases run commands;
      • a subcommand that talks to a remote (clone, fetch, ls-remote, pull, push, submodule) is net and exec;
      • a read subcommand with --output is also write.
    • curl with an option that writes a file (-o, -O, -D, -c, -K, --output, ...) is net and write; wget is net and write.
    • sed: each script must be a known-safe form, else exec. Safe: only the commands p P d D q Q = n N g G h H x { }, s with the flags g i I m M p and a number, and y; addresses N, $, /regex/, and !. Allowed options: -n -E -r -s -u -z -e -i and their long forms. Any other option (-f) is exec. -i with safe scripts is write.
    • rg with --pre, --pre-glob or --hostname-bin is exec.
    • sort with --compress-program is exec; with -o or --output, write.
    • uniq and xxd with two operands are write (the second operand is the output file).
    • find with -exec, -execdir, -ok or -okdir is exec; with -delete, -fls, -fprint, -fprint0 or -fprintf, write.
    • less with a + command that has ! or | is exec; with -o, -O, --log-file or --LOG-FILE, write.
    • file with -C or --compile is write.
    • tree is not in the table (-o writes a file), so it is exec.
    • A long option can be an abbreviation (GNU getopt_long): the rules accept each prefix of the option name. An option letter in a short-option group (-uo) counts.

    The auto set:

    • A step runs immediately only when each of its effects is in the auto set.
    • The auto set is the Local cvar shell.autoEffects (S4): a list of effect names from read, write, exec, net, outside, protected. Default all six (law default_auto_is_grantable): nothing asks but a secret.
    • Secret is never in it: a step that reads or writes a secret always asks (law never_auto_is_routed). A user who narrows the auto set is asked about the steps it no longer holds.
    • A name other than the six is a typed error when the value is set.
    • The cvar is an execution gate, so an untrusted project cannot set it.

    The question (every other step, before it runs):

    • It shows the step exactly as it runs: each control or bidi character in a word is escaped ($'…'); the prompt keeps each line whole; Enter alone answers no.
    • The worker sends a shell_approval frame (effects: the names) to the attached clients. The first answer_shell_approval (approve or deny) is the answer.
    • When the session stops waiting on a question (a client answered it, its step ended or was cancelled, or every interactive client detached and it went elsewhere), the worker sends shell_approval_settled (requestId): every client drops it, shown or queued. An answer to a question no longer pending is refused with error code shell_approval_gone; the TUI shows one muted note, no error.
    • Who answers (phone gateway, no client, parent chain): G5. No answer is a denial.
    • The shell asks about the steps of a pipeline in order before any of them runs.
    • A denial stops the script at that step. Earlier steps ran and their changes stay. The denied step, the rest of its pipeline and all later steps do not run.
    • The result gives the output and exit status of each step that ran, and how the script ended: finished, exited, or refused at step N (denied, unanswered or gateway_refused).
    • One renderer (durable/shell.rs RefusalText) writes the text of a refused step, of a cell that did not run and of a document access that did not run: <what failed>. <next step>. Next steps:
      • Denied: do not try it again unless the user asks for it.
      • Unanswered: ask the user to attach a client, or to allow its effect in shell.autoEffects if that is not secret; or use read-only steps.
      • Gateway refused: ask the user to run it from the eukhe TUI or the dashboard.
    • Shell state (cd, export) lasts for one call only.

    The ipython tool is gated too. A cell is arbitrary Python: it can start any process (subprocess, os.system, the kernel bash()).

    • Each cell is one step with the effect exec. It runs immediately only when exec is in shell.autoEffects (the default).
    • Else the host asks with the same shell_approval frame: request id <call>:cell, step 0, the code as the command (control and bidi characters escaped), effects ["exec"]. It asks before it starts the kernel, a job or the blocking budget.
    • On a denial, no client, or no answer, the cell does not run; the model gets the refusal text (ipython did not run (exec): and the text above).
    • The bash() calls and host requests of a cell the gate let run do not ask again.

  9. Remote reads (ssh://). An ssh:// read is new outbound traffic, so it is off by default:

    1. The host must be in the setting ssh.hosts (list of strings; default empty). The setting is Global: eukhe reads it from the global settings.json only; a project cannot set it. The host must match an entry as written (box, me@box). With an empty list, each ssh:// read gets the rejection not_allowed, and the message names ssh.hosts.
    2. The host is letters, digits, ., -, _ and @, not starting with -. Other hosts get the rejection arguments. Put ports, users and options in ~/.ssh/config.
    3. Examples:
      ssh://box/etc/hosts       # reads /etc/hosts
ssh://box/~/notes/a.md    # reads notes/a.md under the remote home
ssh://box/~/../x          # rejection escapes (item 6)
ssh://box/../x            # rejection escapes (item 6)
    4. eukhe runs the user's ssh program with the user's ~/.ssh/config:
      ssh -T -o BatchMode=yes -o ConnectTimeout=<s> -o ClearAllForwardings=yes -- <host> "cat -- '<path>'"
      eukhe handles no key and no password. With BatchMode, a host that asks for a password or passphrase fails at once. The path goes to the remote shell as one single-quoted word (' becomes '\''), so no character of it is remote shell syntax. The remote login shell must be a POSIX shell.
    5. The call's output cap (S2) keeps the first bytes of the file. eukhe counts the rest; the reply's first line gives the number the cap dropped. The blocking budget (toolBlockingBudgetMs) ends the read: ssh runs in its own process group, and eukhe kills the group at the deadline. A read that did not fill the cap by the deadline gets the rejection timeout. A read that filled the cap gives its bytes, and the first line tells that the cap dropped that number of bytes or more.
    6. The read must run in a tool call. A kernel read() outside a tool call has no output cap, so it gets the rejection arguments.
    7. Typed rejections: host (unknown host, no connection, host key unknown or changed), auth (the host refused each key), not_found, is_directory, permission_denied, binary (not UTF-8 text, or a NUL byte), timeout, io (no ssh on PATH, or another failure).
    8. The read is of one whole file, as text: no [path#TAG] header, no selector, lines are not edit anchors.

Model: bend/tools.bend. Laws: laws/tools.bend (S7). Proofs: proof/tools/. Every input is free: any tools that join and quit, any schemas, any paths, any scripts, any auto set, any answers of the user.

Law Says
roster_fixed no event changes the roster; joiners go behind dyn (S7.1, S7.2)
roster_sent_fixed every request sends the starting roster (S7.1)
dyn_reaches_joined joined tool reachable via dyn (S7.2)
dyn_drops_quit quit tool unreachable via dyn (S7.2)
schema_has_intent every sent schema has i (S7.3)
schema_versioned every sent schema has version ≥ 1 (S7.3)
schema_keeps_params every declared parameter kept (S7.3)
schema_build_idempotent rebuild changes nothing (S7.3)
path_rejects_escape above root: rejected, never clamped (S7.6)
path_resolves_inside under root: resolves (S7.6)
gate_prefix steps that ran = first steps of the script, in order (S7.8)
gate_needs_yes gated steps run ≤ steps approved (S7.8)
gate_deny_stops denial: earlier steps ran; denied and later steps did not (S7.8)
gate_finish_runs_all finished script ran every step (S7.8)

Code: eukhe-durable/src/harness/registry.rs (Registry::fix_roster, RosterFixed, RosterChange, install/uninstall checks), harness/harness/conversation.rs Conversation::configure, harness/generation/round.rs (add_tools), eukhe-core/src/durable/registry.rs create_eukhe_registry (builds schemas, then fixes roster), durable/tool_contract.rs (parameters, build), durable/tool_surface/mod.rs (ToolSurface, dyn, report_issue), kernel/manager/mod.rs mcp_tool_call + mcp_call of the kernel MCP lane (eukhe-runtime/src/rlm/repl.py), eukhe-docs/src/url.rs (walk: sole URL path walker, under Url::names, Url::remote), eukhe-core/src/durable/documents/ssh.rs (SshRead: ssh.hosts check, ssh args, bounded read, typed errors), eukhe-core/src/durable/shell.rs (bash + approval), crate eukhe-shell (in-process shell, effect.rs, gate).

Ties:

  • Runs as the compiled core: entry bend/ffi_tool_surface.bend (id 51), Rust eukhe_bend::rules::tool_surface. tool_contract::build sends each schema's parameters as numbers (i is 0) and its declared version; the core answers the parameters in order and the version (build). ToolSurface keeps the registrations; which tools dyn reaches after each join and quit is the core's (step, dyn_call). Laws: laws/tool_surface.bend (tool_surface_ffi_exact, tool_surface_ffi_answers, tool_surface_ffi_left_over, tool_surface_ffi_example). The fixed roster stays the registry's own refusal (Registry::fix_roster, keep_roster: the installed tools compared whole), pinned by harness::tests::registry::a_fixed_roster_rejects_every_change_of_the_tools_the_model_sees.
  • Url::names and Url::remote walk a path with model resolve, run as the compiled core (entry bend/ffi_tools.bend, request laws tools_ffi_*; a name crosses as its segment's index).

Tests: harness::tests::registry::a_fixed_roster_rejects_every_change_of_the_tools_the_model_sees; durable::tool_surface::tests (two turns, same roster each request; late tool listed and run via dyn; report_issue row stored; install, configure rejected); daemon dyn_tool_e2e (stdio MCP tool listed and called via dyn; one tool loadout in transcript); url::tests::an_ssh_url_* (host, path rules); durable::documents::ssh::tests (fake ssh records args, plays hosts; shell-syntax path reads that file, runs nothing; each failure typed; cap counts dropped bytes; budget kills ssh).

Not modelled (tests tie them): wire form of the version annotation, MCP list and call via kernel, report row, remote side of ssh://.

G1. Path policy #

One path policy (eukhe_types::path_policy::PathPolicy) judges each path an agent tool reads or writes. The bash tool (S7 item 8) and the document tools (read, write, edit, grep, glob, the kernel fs.* requests) share it, so they cannot judge a path differently.

  1. The real path. The policy judges the real path, not the written path. resolve follows each symlink on the existing part of the path, dangling ones too (a write through it creates the target). . does not move. .. goes up from the real directory, not the written name. .. of / is /. The part that does not exist stays as written. Thus a symlink gets the class of its target. After 40 symlinks (MAX_LINKS, as Linux) the path loops: resolution stops following, and the policy does not trust the rest of the path.

  2. The classes. Each real path has one class; the first that applies wins:

    1. Secret: the path is a secret entry, or under one.
    2. Protected: a protected rule covers the path, or the path is an ancestor of a protected or secret entry (moving or removing the ancestor moves or removes the entry).
    3. Inside: the path is under a workspace root.
    4. Outside: all other paths.

    A path whose symlinks loop is never Inside: it is Outside, or Protected or Secret when one applies.

  3. The protected set comes from the settings loaders; there is no separate list (durable::path_policy::policy):

    • the agent dir and each entry directly in it (settings.json, config.cfg, subagent.cfg, models.json, auth.json, binds.cfg): a Dir rule;
    • the profile dir (agents/<agent>.cfg): a Tree rule;
    • the session's project config dir (<cwd>/.eukhe): a Tree rule; each .eukhe directory below the workspace root: a Named rule;
    • each settings file the session loads and rereads (EukheSettings::watched): a Tree rule;
    • each .git directory below the workspace root: a Named rule (its config and hooks name programs git runs);
    • each directory on PATH: a Dir rule (a file in it replaces a command).

    A Named rule looks at the part of the path below its workspace root (the whole path when no root holds it). The policy makes each entry real when it starts.

  4. The secret set: auth.json in the agent dir, the Prime CLI config, the credential stores of other programs in the home dir (.ssh, .aws, .azure, .config/gcloud, .config/gh, .docker/config.json, .kube, .gnupg, .password-store, .local/share/keyrings, .netrc, .git-credentials, .npmrc, .pypirc, .cargo/credentials, .cargo/credentials.toml), and the files named by AWS_SHARED_CREDENTIALS_FILE, AWS_CONFIG_FILE and CLOUDSDK_CONFIG.

  5. Effects of an access:

    Access Effects
    read or list read; of a Secret path, read and secret
    search (grep of a directory) of a path that is or holds a secret read and secret
    write Inside write
    write Outside write and outside
    write Protected write and protected
    write Secret write and secret

  6. The gate of the document tools (DocumentsGate). A document tool resolves each path once and gives that resolution (RealPath: the real path, and whether its symlinks looped) to the gate before the access. The access then occurs on that real path. The gate judges the resolution as given and does not resolve again: a second resolution can lose a loop. An access runs without a question only when the auto set (shell.autoEffects, S7 item 8) holds each of its effects; secret is never in it. Thus:

    • a write runs without a question when the auto set holds its effects, and never to a secret;
    • a read of a secret always asks;
    • each other access asks when the auto set does not hold all its effects.

    The question goes through the approval sink of a bash step: the shell_approval frame, with the verb and the real path as the command (write /path), and the effects.

    • Approve: the access runs.
    • Deny, no answer, or refused by the gateway rule (G5): the access does not run; the model gets the refusal text (S7 item 8), opened by the access's effects ((write+outside) it needs the user's approval, …).
    • No client can answer (no approval sink): the gate does not ask; each access that must ask does not run, and the model gets the unanswered refusal text, opened the same way.

  7. A write occurs on the real path. The writer locks the real path, then resolves the path again. If the real path changed (a symlink was made or moved), the write stops and writes nothing. A replaced file keeps its mode. A created file gets the default mode, with no execute bit.

Model: bend/path_policy.bend (alias Pp: real with max_links links of fuel, class, holds, effs, runs, asks, the store run and guarded). Laws: laws/path_policy.bend. Proofs: proof/path_policy/. Every input is free: any symlinks (loops too), any policy, any paths, any auto set, any answers.

Law Says
path_real_has_no_link no loop: no prefix of the real path is a symlink (G1.1)
path_secret_wins real path under a secret entry: Secret (G1.2)
path_inside_is_safe Inside only if: no loop, no secret covers it, no rule protects it, no ancestor of an entry, a root holds it (G1.2)
path_ancestor_guarded ancestor of a protected or secret entry: Protected or Secret (G1.2)
gate_write_auto_never_secret write without a yes: never to a secret (G1.6)
gate_secret_read_needs_yes secret read: only on a yes (G1.6)
gate_yes_runs a yes runs each access (G1.6)
gate_inside_write_runs write in auto set: Inside write runs unasked (G1.6)
secrets_need_yes no agent write sequence without a yes changes a secret (G1.6, G1.7)

Code: eukhe-types/src/path_policy.rs (resolve, RealPath, PathPolicy, PathRule, MAX_LINKS), eukhe-shell/src/paths.rs (judge: class and holds-a-secret of a resolved path, run as compiled model judge, entry bend/ffi_path_policy.bend, request laws path_policy_ffi_*; each path component crosses as an id), eukhe-core/src/durable/path_policy.rs (policy, session_policy, effects, DocumentsGate), eukhe-docs/src/gate.rs (AccessGate, Access), eukhe-docs/src/write.rs (write_file, LockedWriter), eukhe-shell/src/run.rs (step path effects: one judge_path per path).

Tests: durable::path_policy::tests::every_loader_file_is_guarded_and_a_project_file_is_inside, durable::path_policy::tests::a_write_whose_links_looped_asks_even_when_its_real_path_is_inside, path_policy::tests (eukhe-types).

Not modelled: filesystem change between gate and lock (the writer checks it), file modes.

G2. Shell classification #

A step's effects: every effect of every part (S7 item 8); auto set rules: S7 item 8. By default only a step with outside, protected or secret asks. A step has secret only when a part names a path that is or holds a secret (an operand, an option value, a redirection target, the working directory of a command that reads it because it names no path).

Model: bend/tools.bend part 4 (Step{id, effs}, grantable, within, join, Part{own, secret}, part.effs, parts.effs, parts.secret, exec). Laws: laws/tools.bend. Proofs: proof/tools/.

Law Says
step_holds_every_part step has every effect of every part
secret_needs_a_secret_path secret only if a part names a path that is or holds a secret
secret_path_gives_secret such a part gives its step secret
auto_needs_every_effect one effect outside the auto set, or ungrantable: asks
auto_never_sensitive secret: always asks, any auto set
composed_needs_every_part unasked only if every effect of every part is within the auto set
auto_runs_within within the auto set: runs, uses no answer
held_needs_a_yes not within: runs only on a yes; else the script stops there

Code: eukhe-types/src/shell.rs (ShellEffect, ShellEffects, AutoSet: the set the user allows), eukhe-shell/src/effect.rs (classify, GIT_UNTRUSTED_REPO_ARGS, reads_cwd), run.rs (Shell::parts: the facts of a step; parts of an out-of-grammar script from parse::parts), shown.rs (quote, visible), eukhe-tui/src/confirm.rs (ConfirmPanel::approval).

Runs as the compiled core: entry bend/ffi_shell.bend (id 50), Rust eukhe_bend::rules::shell. Rust gathers each step's parts (own codes from the command table and target classes, whether the part names a secret path); the core answers the step's effects (join of part.effs) and whether it runs unasked (within), whether a document tool's access runs unasked (within), and what an answer does (gate: a no stops the script at the step). Laws: laws/shell.bend (shell_ffi_exact: every input, the model's decision or exactly E shell: malformed request; shell_ffi_answers, shell_ffi_left_over, shell_ffi_example).

Tests: every_effect_of_a_step_must_be_allowed, only_a_step_that_reads_its_working_directory_reads_a_secret_in_it, effect::tests::a_command_reads_the_working_directory_only_when_it_names_no_path, effect::tests::a_git_step_that_can_run_a_repository_program_is_exec, a_git_step_that_is_not_exec_runs_with_the_untrusted_repository_arguments, shown::tests::a_hidden_character_is_escaped_and_bash_reads_the_word_back, confirm::tests::an_approval_answers_no_on_enter_and_keeps_every_line.

Not modelled: which paths a command reads or writes (every word counts; working dir only via reads_cwd); what an approved exec step does.

G4. Every runner of code goes through the gate #

A tool that runs code declares a Runner in its registration (extra): its caps (each effect its code can have) and how the gate covers it (EachStep: bash; EachCall: ipython). A tool with no Runner runs no code of its own. A Runner is always gated: Rust cannot write an ungated one.

Model: bend/runners.bend (registry, the tools a default session installs, in install order; cell, the gate of one call). Laws: laws/runners.bend. Proofs: proof/runners/.

Law Says
gate_covers_every_runner every registry tool whose caps hold exec is gated
ipython_gated_each_call ipython: caps exec, gate covers each call
cell_runs_only_within_or_approved gated call runs only if caps within the auto set or approved
cell_within_runs_unasked caps within: runs unasked
cell_approved_runs outside, approved: runs
cell_no_yes_stops outside, no approval (denial, no answer, no client): does not run
cell_exec_asks code that can run a program is never within an auto set without exec

Code: eukhe-core/src/durable/runner.rs (Runner, Gate), durable/rlm/tool.rs (ipython gate), durable/shell.rs (bash runner).

Runs as the compiled core: entry bend/ffi_runners.bend (id 52), Rust eukhe_bend::rules::runners. The ipython tool asks the core whether a cell runs unasked (within) and, after the session's approval sink answered (or with none attached), how the call ends (cell); Rust only picks the refusal text the answer names. Laws: laws/runners.bend section runners entry (runners_ffi_exact, runners_ffi_answers, runners_ffi_left_over, runners_ffi_example). durable::runner::tests::the_registry_is_its_model: every tool of an opened session (name, caps, gate), without and with chat memory, equals the core's registry.

Test: a_cell_runs_only_within_the_auto_set_or_approved.

Not modelled: dynamic tools behind dyn (MCP tools, kernel remote/<name> functions).

G5. A child's question reaches its root's user; the phone never waits #

A subagent session (an RLM child) runs in its own worker with no client of its own, so its gated steps (S7 item 8: bash steps, ipython cells) must ask the user of its root session.

  • A session whose question no client answers (none attached, or all detach without an answer) hands it to its parent session: daemon command relay_shell_approval (the parent's persisted session id, the request, and agent, the name of the asking subagent). The supervisor routes it to the parent's worker like a turn-long wait.
  • The parent asks its own clients with a shell_approval frame that carries agent, or hands the question on to its own parent.
  • The first session up the chain whose clients answer gives the answer ({"answer": "approve" | "deny" | "unanswered" | "gateway_refused"}). When the root has no client that answers, the answer is unanswered (a denial, with the usual message to the model).
  • The TUI prompt names the subagent (Subagent <name> asks: allow shell step N (<effects>)?), with the name's characters that a terminal hides or moves escaped. A frame without agent is the session's own question.

A client tells its kind when it attaches (clientKind: interactive, the default, or gateway). The phone gateway attaches as gateway: it shows no question, so a session never waits for its answer.

  • A session whose attached clients are all gateways asks no one and answers at once by the gateway rule: a step with protected (a write of eukhe's own config or credentials, a .git or .eukhe dir, a PATH dir) or secret is refused (gateway_refused); every other step runs.
  • The bash result, the ipython result and the document tools' error tell the model that the session runs only from the phone gateway and that the user must run the step from the TUI or the dashboard.
  • A subagent's question that reaches such a session gets the same answer.
  • When a TUI or the dashboard is attached beside the gateway, that client gets the question. If all of them detach without an answer while the gateway stays, the gateway rule answers.

The auto set comes first (gate; default: S7 item 8): a step within it runs unasked. Outside, protected and secret take the route above: a TUI or the dashboard is asked; from the phone alone, a write outside the workspace runs by the gateway rule, a protected write or a secret is refused.

Model: bend/approvals.bend (route, a chain of sessions from the one that asks up to its root: no client, clients that leave, clients that answer, the gateway alone, clients that leave while the gateway stays; fate, what becomes of a step with given effects; default_auto; gate, the auto set before the route). Laws: laws/approvals.bend, laws/tools.bend. Proofs: proof/approvals/.

Law Says
child_answered_by_root no session below the root answers: the root's clients get the question; their answer is the verdict
nearest_answer_wins first answering session up the chain decides, whatever is above
unanswered_only_when_quiet unanswered (a denial) only if no session in the chain answers
quiet_is_unanswered then unanswered; no session invents an answer
gateway_never_waits gateway-only session: no frame to any client, nothing up the chain, gateway rule answers at once
gateway_refuses_protected gateway rule refuses a protected write
gateway_refuses_secret gateway rule refuses a secret read or write
gateway_runs_the_rest gateway rule runs every other step unasked
left_to_the_gateway interactive clients leave it unanswered, gateway stays: gateway rule, not up the chain
gateway_rules_a_subagent subagent question reaching a gateway-only session: fares as that session's own step
default_auto_is_grantable no user setting: auto set = every effect but secret
never_auto_is_routed secret never runs unasked via the auto set; the question takes its route
never_auto_asks_the_client answering client (TUI, dashboard): it is asked; its answer decides
outside_runs_only_by_the_gateway phone only, auto set without outside: an outside write, not protected, no secret, runs, only by the gateway rule
guarded_refused_from_the_phone phone only: secret refused at once, any auto set

Code: eukhe-daemon/src/shell_approval.rs (ShellApprovals::ask, relay), worker.rs (relay over the supervisor link), worker/connection.rs (client kind at attach), supervisor/routing.rs (relay budget), eukhe-tui/src/session_ui/settings.rs (prompt), eukhe-gateway/src/link.rs (attaches as gateway), eukhe-core/src/settings/cvar/table.rs (SHELL_AUTO_EFFECTS, default auto set).

Runs as the compiled core: entry bend/ffi_approvals.bend (id 53), Rust eukhe_bend::rules::approvals, called by ShellApprovals::route at each session a question reaches: what the session does (next: show it to its interactive clients; end it by the gateway rule when its clients are all the phone gateway; relay it to its parent when no client is attached; no answer at a root), what its clients' answer makes of the step (answered), and the default auto set (default_auto). Laws: laws/approvals.bend section approvals entry (approvals_ffi_exact, approvals_ffi_answers, approvals_ffi_left_over, approvals_ffi_example). What stays in Rust is the interleaving (the relay over the supervisor, clients that detach, the first answer wins), checked by the bridge.

Ties:

  • shell_approval::bridge::the_approval_route_is_its_model vs bridge/bridge_approvals.bend (route): every chain of up to 3 sessions with a write, a program run, a protected write, a secret read, plus generated longer ones, on real ShellApprovals relaying through each parent's real handler; compares which sessions showed the question, whether each frame names the subagent, the end.
  • durable::shell::tests::the_default_auto_set_is_its_model: the real default auto set equals the core's default_auto.

Tests:

  • with_no_auto_set_a_write_outside_the_workspace_runs_unasked: no client; write, program run and outside write all run.
  • rlm_child_approval_e2e::a_subagent_step_runs_when_the_root_client_approves: real supervisor; root with attached client; subagent bash write under auto set read.
  • shell_approval_e2e::a_phone_only_session_runs_steps_unasked_and_refuses_a_protected_write: real supervisor, client attached as gateway, auto set read; write and program run run unasked by the gateway rule; .eukhe/settings.json write refused at once with the gateway message.

Not modelled: supervisor routing of the command (a parent whose worker is not resident is not asked; then unanswered); a client attaching while a question waits above it. The dashboard shows a subagent's question without its name.

S8. The documents tools #

The documents tools are read, edit, grep, glob and the kernel functions read(), write(), edit(), grep(), glob() (crate eukhe-docs). They share one edit store per session.

  1. An edit of many files is all or nothing for conflicts. The writer locks every path of the call, in one order, then checks each file: its bytes must be the bytes the edit was applied to, and an MV destination must not exist. If one check fails, no file is written. Then it writes the files in order and stops at the first failure. The reply names the files that landed (with new tags) and those that did not: "Applied to a; NOT applied to b, c". It never says nothing was written when a file landed. A rename that landed but whose directory sync failed, and a move whose source stays, are landed writes with a warning.
  2. A retry of a start or end insert with the old tag, after the insert landed, does not insert again: the result says the edit is already in the file.
  3. write() replaces an existing file only when its bytes on disk are a version this session saw (a read, a grep, or its own write or edit). Else it writes nothing and tells the model to read the file first. A new file is created. A replaced file keeps its BOM, line endings and mode; a warning tells when the content had other line endings, or when the old file was not UTF-8.
  4. MV never replaces a file. The destination gets the bytes through a hard link, which fails on a name that exists.
  5. A temporary file is .eukhe-tmp-<hash of the name>-<pid>-<n>, so a long name still fits. Its writer locks it. Each write of a target removes that target's temporary files that no writer locks (a crash left them). grep and glob do not show these names.
  6. A line ends at \n. A \r before \n is part of that line's CRLF ending; a lone \r is text. read, grep and edit share this line model. An edit keeps every byte outside its lines. A new or changed line gets the ending of the line before it (at file start: the file's first ending, else LF).
  7. The tag of a grep result is the hash of the bytes grep searched, not of a second read of the file.
  8. A line is seen only when its row reached the model, after the output bound cut the middle of a long result. An edit anchor on an unseen line is rejected; the rejection shows the line and marks it seen, so the same edit applies on a retry. After an edit lands, the lines seen before and the lines the edit wrote stay seen.
  9. grep and glob report each file they skip or cut, with the reason and the count: binary, unreadable, searched only in part, excluded directories, symlinks, walk errors, the match caps. A continuation (skip=N, a line range) gives the next results.
  10. One size limit (MAX_SNAPSHOT_FILE_BYTES, 4 MiB) applies everywhere. A larger file has no tag; the message tells the model to read it in ranges and change it with write() or bash. A non-UTF-8 file gets a message with its path and encoding.

Models: bend/doc_commit.bend, bend/doc_seen.bend, bend/doc_lines.bend, bend/doc_rows.bend, bend/doc_tags.bend, bend/doc_search.bend, bend/doc_glob.bend. Laws: laws/doc_seen.bend, laws/doc_search.bend, laws/doc_commit.bend, laws/doc_tags.bend, laws/doc_lines.bend, laws/doc_rows.bend, laws/doc_glob.bend. Proofs: proof/doc_seen/, proof/doc_search/, proof/doc_commit/, proof/doc_tags/, proof/doc_lines/, proof/doc_rows/ and proof/doc_glob/.

The writer's choices run as the compiled Bend core (bend/ffi_doc_commit.bend): the check of an edit (the first file that changed or whose MV destination exists stops it), what each publish did (landed, with which warning, or failed: stop), the reply of an edit (an error only when a publish failed and none landed; an untried file names the file that failed first), whether write() may replace its target, the seen versions (the last 8 digests), the temporary files' prefix and which of them a sweep removes. Rust locks, reads, compares bytes, hashes (xxh64 digests stay Rust), publishes and removes. Grep's tag choice for each shown file (tag a whole UTF-8 file with the searched text; no tag over the limit or for another encoding) runs as bend/ffi_doc_tags.bend. The walk's hiding of temporary names keeps the prefix as a constant (scope.rs, pinned by commit_prefix_spec).

Lines run as the compiled Bend core: Rust scans a file into its projection (text.rs Projection: the BOM flag, each line's length and own ending) and the core decides on it: the separators of an edit, the carry of a loaded file and what a whole-file write keeps (bend/ffi_doc_lines.bend), whether a read goes on and what it shows (bend/ffi_doc_rows.bend: lines counted, spans with context and gap markers, notices, tag). A selector's ranges reach the core sorted and merged (read/selector.rs: :5-6,1-2 reads 1-2 then 5-6; :1-5,3-8 reads 1-8 as one range); the core shows the ranges it gets in their order, with a gap marker before every span but the first that does not start right after the span before it.

Glob's ranking and pages run as the compiled Bend core (bend/ffi_doc_glob.bend, glob/ranking.rs). Rust walks, reads each matched path's time and spells a path only when the core asks for it. The core decides the page size (the limit, at most 200; default 200), the order (newest first, then by path), each path once at its newest time, which paths it keeps (the best skip + page + 1), the continuation (skip=N) and the past-the-end count. It asks for a path only while that path can still be on the page.

Law Says
edit_reports_what_landed reply says applied iff new content is on disk (S8.1)
edit_all_or_nothing_on_conflict one file changed since staging: no file lands (S8.1)
edit_lands_every_file no change, no failed write: every file lands (S8.1)
write_never_loses_unseen over an unseen version: refused, no change (S8.3)
write_writes_seen over no file or a seen version: written (S8.3)
move_never_overwrites to an existing name: refused, no change (S8.4)
move_moves to a free name: content moves (S8.4)
temp_sweep_never_held never removes a temp file a live writer locks (S8.5)
temp_sweep_only_own removes only its target's temp files (S8.5)
temp_sweep_removes_free removes every unlocked temp file of its target (S8.5)
load_persist_roundtrip load + write, no edit: same bytes (S8.6)
edit_keeps_untouched_bytes every byte outside the edited lines kept (S8.6)
edit_writes_new_lines an edit keeps the lines before, then exactly the new lines, then the lines after (S8.6)
grep_line_is_read_line grep and read: same text at the same line number (S8.6)
persist_weaves_carry edited file written line by line: each line but the last followed by its own ending, else the separator written before it (S8.6)
persist_plan_refines separator plan over runs of lines gives, line for line, that rule's separators (S8.6)
lines_entry_refines the plan's compiled entry reads every request back, answers the model's separators (S8.6)
lines_carry_is_first the carry decided from a file's projection is the first ending persist starts from (S8.6)
lines_write_keeps a whole-file write keeps the file's BOM and first ending, warns iff both texts have endings and they differ (S8.6)
lines_entry_answers the lines entry answers every request spelled from the wire primitives with the spelled decision (S8.6)
lines_entry_exact any input the lines entry does not refuse is the spelling of a request (S8.6)
rows_lines_are_read_rows the lines a read numbers are, in order and length, the model's read rows (S8.6)
rows_raw_lines_are_pieces a raw read counts every piece of the LF text (S8.6)
rows_gate_refuses a read that is not raw refuses a non-UTF-8 file, then a binary one (S8.10)
rows_view_shows a read shows the lines it counts, the spans with their context and gap markers, the notices and the tag of the read rule (S8.6, S8.10)
rows_gap_marks_every_jump the first span has no gap marker; every later span has one iff it does not start right after the span before (later, earlier or overlapping; raw: every later span) (S8.6)
rows_entry_answers the read entry answers every request spelled from the wire primitives with the spelled decision (S8.6)
rows_entry_exact any input the read entry does not refuse is the spelling of a request (S8.6)
tag_names_shown_text tag names the text its rows come from (S8.7)
edit_only_seen_lines applies only if every anchor is seen (S8.8)
edit_seen_applies all anchors seen: applies (S8.8)
reveal_then_retry rejected edit with ≤ 40 anchors applies on a straight retry iff every unseen anchor is a line of ≤ 512 characters (S8.8)
edit_marks_whole_reveal unseen anchors become seen iff the rejection showed them all whole: ≤ 40, each a line of ≤ 512 characters (S8.8)
reject_names_unseen rejection names exactly the unseen anchors, in order (S8.8)
reject_shows_lines rejection shows, of its first 40 unseen anchors, each that is a file line, cut to 512 characters when longer (S8.8)
reject_whole_exact rejection says it showed its anchors whole iff it did (S8.8)
reveal_bounds reveal cap: 40 anchors, 512 characters (S8.8)
seen_entry_refines the guard's compiled entry reads every request back, answers the model's verdict (S8.8)
grep_accounts_every_file each walked entry in exactly one class; classes sum to the walk (S8.9)
grep_notes_every_gap skipped, cut or unsearched class has a notice iff not empty (S8.9)
grep_notes_every_cut shown file with cut matches has its own notice (S8.9)
continuation_progresses continuation page not empty (S8.9)
continuation_contiguous continuation = next part of the list: none left out, none twice (S8.9)
continuation_disjoint page and continuation share no item (S8.9)
search_scope_answers scope: several files iff more than one root or a directory root; 20 matches a file and the skip asked, else 200 and no skip; page = match limit + 1 files, else 20 (S8.9)
grep_walk_spec, grep_keeps_spec, fetch_reaches each walked file's class, cut, kept matches and fetch are the spec's (S8.9)
page_is_window, next_is_more, past_is_beyond, grep_scope_pages, limit_round_robin, limit_cuts page, continuation, past-the-end notice, match limit: exactly the spec's (S8.9)
search_walk_runs, search_*_answers, search_*_refuses, search_shut_refuses grep's compiled entry and walk stepper answer each request with the rule's decision; malformed input gets the error form (S8.9)
glob_walk_runs, glob_events_answer glob's compiled entry answers a walk, and any events in any order, with the spec's page: newest first then by path, each path once, at most 200, the continuation and past-the-end count; no path that belongs on the page is declined (S8.9)
glob_open_refuses, glob_step_refuses, glob_shut_refuses malformed glob input gets the error form (S8.9)

Code: eukhe-docs/src/write.rs (LockedWriter::write_all, publish, write_file, sweep), hashline/mod.rs (apply_hashline, commit), hashline/patcher.rs, hashline/seen.rs (seen guard), hashline/apply.rs (line origins, persist), text.rs (scan, carry, write decision), read/mod.rs, read/view.rs (read gate and view), grep/, glob.rs, store.rs (saw_bytes), eukhe-core/src/durable/documents/tool.rs (bounded), requests.rs (Cut, Done::mark_seen).

Ties: write::tests (multi-file edit with injected faults and conflicts; write tool vs writes by another program; move; sweep with live locks; real files through the compiled core), text::tests::the_scan_is_the_projection (the scan is the projection the laws state), grep::bridge (read and grep show the same rows on random bytes with \r, \n, \r\n, BOM; file changes between search and record: the tag names the searched text), grep::decide::tests (grep's decisions come from the compiled core), glob::tests::the_page_comes_from_the_compiled_core (glob's page comes from the compiled core), durable::documents::bridge (long read cut by the output bound; edits at anchors in and around the cut).

Not modelled: notice text bytes; line model of a stale edit's rebase (maps lines through a line diff).