editor

A trusted clauz3 layer for in-place file editing — edit_file (full replace) and append_file (append) — with path-prefix policies and content-substring guards an agent can prove before any disk write.

Unlike the layers under examples/, these effects are real, not mocks: edit_file actually overwrites and append_file actually appends. The prover never runs their bodies — it records each call as a fact and proves the contract. The bodies run only under clauz3 run, after a program is proved and approved.

Install

clauz3 install stdlib:editor

Effects

Import with from tools.editor.trusted.effects import edit_file, append_file:

• edit_file(path: str, new_text: str) -> None — overwrite a UTF-8 file. Precondition: path is non-empty. Recorded under the edit and write markers.
• append_file(path: str, text: str) -> None — append UTF-8 text. Precondition: path is non-empty. Recorded under the edit and write markers.

Both create parent directories as needed.

Because both effects also carry the write marker, filesystem write policies from stdlib:filesystem (e.g. only_write_under, writes_at_most) also apply to edits — installing both layers gives you stacked enforcement without redeclaring constraints.

Contracts

Import with from tools.editor.trusted import contracts as ed:

• ed.no_guarantees() — explicit null contract.
• ed.no_edits() — no edit (replace or append) is performed.
• ed.no_appends() — no append is performed.
• ed.only_edit_under(root) — every edit path is under root.
• ed.never_edit_under(prefix) — no edit path is under prefix.
• ed.edits_at_most(count) — at most count edits occur.
• ed.replace_length_at_most(max_chars) — every full-replace fits in max_chars.
• ed.append_length_at_most(max_chars) — every append chunk fits in max_chars.
• ed.must_not_replace(substring) — no full-replace contains substring.
• ed.must_not_append(substring) — no append contains substring.

The must_not_* contracts are useful as secrets / banned-token guards before content reaches disk.

Example

import clauz3
from tools.editor.trusted import contracts as ed
from tools.editor.trusted.effects import append_file, edit_file


@clauz3.guarantee(ed.only_edit_under("/repo/build"))
@clauz3.guarantee(ed.must_not_replace("BEGIN PRIVATE KEY"))
@clauz3.guarantee(ed.edits_at_most(10))
def main() -> None:
    edit_file("/repo/build/manifest.json", '{"version": "1.0"}')
    append_file("/repo/build/log.txt", "build complete\n")

Tests

clauz3 test stdlib:editor

tests/cases/*_pass.py must prove; tests/cases/*_fail.py must not.

Source

src/clauz3/stdlib/editor/tools/editor/trusted/effects.py

"""Trusted editor effects: in-place file modification.

Both ``edit_file`` (full-content replace) and ``append_file`` are real
non-mock implementations. They both carry the ``edit`` marker so a
single ``Edit = effect("edit")`` relation in the contract layer covers
all in-place mutation.

This is intentionally a separate stdlib tool from ``filesystem``:

- the ``edit`` marker is distinct from ``write``, so a project can
  permit reads + edits while still forbidding from-scratch writes
  (or vice versa);
- ``append_file`` is genuinely a different operation from ``write_file``
  (preserves prior content), so the contract layer can talk about both
  shapes;
- the content-substring contracts (``must_not_write_text``) are unique
  to the editor surface — useful as exfil / secrets / banned-token guards
  before any text reaches disk.
"""

from pathlib import Path

import deal


@deal.pre(lambda path, new_text: len(path) > 0, message="path must be non-empty")
@deal.has("edit", "write", "trusted")
def edit_file(path: str, new_text: str) -> None:
    """Replace the UTF-8 contents of ``path`` with ``new_text``.

    Creates parent directories as needed; overwrites any existing file.
    Recorded under the ``edit`` marker.
    """
    target = Path(path)
    target.parent.mkdir(parents=True, exist_ok=True)
    target.write_text(new_text, encoding="utf-8")


@deal.pre(lambda path, text: len(path) > 0, message="path must be non-empty")
@deal.has("edit", "write", "trusted")
def append_file(path: str, text: str) -> None:
    """Append ``text`` to the UTF-8 contents of ``path``.

    Creates parent directories and the file as needed. Recorded under
    the ``edit`` marker, with field name ``text`` (not ``new_text``).
    """
    target = Path(path)
    target.parent.mkdir(parents=True, exist_ok=True)
    with target.open("a", encoding="utf-8") as fh:
        fh.write(text)

src/clauz3/stdlib/editor/tools/editor/trusted/contracts.py

"""Editor path and content policies built from generic trusted effect facts.

Edits (both full-replace and append) are recorded under the ``edit`` marker.
These contracts let an agent state where on the filesystem it may edit, how
many edits it may make, and constraints on the content written.
"""

from clauz3.spec import ContractSpec, contract, effect
from clauz3.spec import no_guarantees as core_no_guarantees

Edit = effect("edit")
EditFile = effect("edit_file")
AppendFile = effect("append_file")


@contract
def no_guarantees() -> ContractSpec:
    """Make no guarantees about editor effects."""
    return core_no_guarantees()


@contract
def no_edits() -> ContractSpec:
    """Guarantee the program performs no edits (replace or append)."""
    return Edit.empty()


@contract
def no_appends() -> ContractSpec:
    """Guarantee the program performs no appends."""
    return AppendFile.empty()


@contract
def only_edit_under(root: str) -> ContractSpec:
    """Guarantee every edit (replace or append) has a path under ``root``."""
    return Edit.all(lambda e: e.path.startswith(root))


@contract
def never_edit_under(prefix: str) -> ContractSpec:
    """Guarantee no edit has a path under ``prefix``."""
    return Edit.all(lambda e: not e.path.startswith(prefix))


@contract
def edits_at_most(count: int) -> ContractSpec:
    """Guarantee at most ``count`` edits occur."""
    return Edit.count() <= count


@contract
def replace_length_at_most(max_chars: int) -> ContractSpec:
    """Guarantee every ``edit_file`` replacement is at most ``max_chars`` long.

    Bounds full-content replacements; ``append_file`` is unaffected and uses
    ``append_length_at_most`` for the corresponding bound.
    """
    return EditFile.all(lambda e: len(e.new_text) <= max_chars)


@contract
def append_length_at_most(max_chars: int) -> ContractSpec:
    """Guarantee every ``append_file`` chunk is at most ``max_chars`` long."""
    return AppendFile.all(lambda e: len(e.text) <= max_chars)


@contract
def must_not_replace(substring: str) -> ContractSpec:
    """Guarantee no full-replace contains ``substring`` (e.g. a banned token).

    Useful as a secrets / banned-content guard before content reaches disk.
    Applies to ``edit_file`` only; the append-side guard is ``must_not_append``.
    """
    return EditFile.all(lambda e: substring not in e.new_text)


@contract
def must_not_append(substring: str) -> ContractSpec:
    """Guarantee no append chunk contains ``substring``."""
    return AppendFile.all(lambda e: substring not in e.text)

All cases

Browse the full set on the all-cases page.