Skip to main content

Module formal_ai_files

Module formal_ai_files 

Source
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§

FileArgs
Normalized arguments of a file tool call.
FileDecision
Whether a file tool call may run (the effect policy of #255).
FileHooks
Test hooks: run just before the guard and just before the readback.
FileReceipt
What an approved file call did.
Match
One matched region of a mutation receipt, in bytes of the preimage.

Constants§

FILE_TOOL_NAMES

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| line per \n-separated line and a trailer with the line count. Formal AI decodes it back to exactly text (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.