Expand description
Structured read, edit and write tools of the experimental
--use-formal-ai mode (issue #258). Mirrors js/src/lib/formal-ai-files.js.
The bash tool runs only programs without shell syntax, and its write
programs (cp, mkdir, mv, rm, rmdir, touch) cannot change the text of a
file. These three tools are the guarded replacement primitive instead of an
interpreter: start itself reads and writes the one named workspace file,
byte for byte, so comments, whitespace and unrelated content survive.
- read: the exact UTF-8 text of a regular file, bounded by START_FORMAL_AI_MAX_FILE_BYTES, as the numbered frame Formal AI decodes back to that text (#261); it observes the file for later changes.
- edit: replaces one literal occurrence of old_string (or every one with replace_all) in a file read before, atomically, then reads it back.
- write: replaces an observed file, or creates one in an observed directory, atomically, then reads it back.
Paths follow the bash tool’s workspace policy (no absolute, escaping or symlinked-out paths), edit and write need START_FORMAL_AI_EFFECTS= workspace-write and an earlier observation of the target, and a file that changed since start read it is not overwritten.
Bounded typed source edits (issue #261): a change to an existing file is
bound to the complete bytes the read tool returned for it in this task
(listing it or cat is not enough), applied to exactly the matched regions
of those bytes, guarded against a change of the target until the new file
takes its place, and verified by reading it back: every matched region now
holds new_string and every other byte is unchanged and in place. The
mutation receipt (preimage, postimage and byte offsets of the matches) is
kept in the evidence and returned to Formal AI.
Structs§
- File
Args - Normalized arguments of a file tool call.
- File
Decision - Whether a file tool call may run (the effect policy of #255).
- File
Hooks - Test hooks: run just before the guard and just before the readback.
- File
Receipt - What an approved file call did.
- Match
- One matched region of a mutation receipt, in bytes of the preimage.
Constants§
Functions§
- describe_
file_ call - One-line rendering of a file call for notes and evidence.
- echoed_
by_ tool - Whether a tool result of the conversation already contained
text, as sent or as the file text of a read frame (whose lines carry numbers): an answer that only echoes file data back is not Formal AI’s own (#261). - evaluate_
file_ call - Decide whether a file tool call may run.
- file_
tool - The JSON schema of one file tool, as offered to Formal AI.
- normalize_
file_ args - Normalize the JSON arguments of a file tool call, or say what is wrong.
- read_
frame - The complete text of a read as the numbered frame Formal AI binds as a
whole-file Read (#261): one
NNNNN| lineper\n-separated line and a trailer with the line count. Formal AI decodes it back to exactlytext(lines joined with\n, so a missing or present final newline, CR bytes and Unicode survive); its OpenAI-compatible request parser drops any other metadata on a tool message, so the frame is the only binding it accepts. - read_
frame_ text - The exact text a read_frame() result frames, or None when it is not one.
- run_
file_ call - Run an approved file tool call.
- run_
file_ call_ with - run_file_call() with test hooks.
- sha256_
hex - Hex SHA-256 of some bytes.
- verify_
mutation - Check a readback against the mutation receipt, independently of how the new text was computed: every matched preimage region held exactly the old bytes, every other preimage byte is unchanged and in place, every replaced region holds exactly the new bytes, and nothing else was added.