Skip to content

Text example

The text example shows the relation algebra's string side: length bounds, substring requirements, and prefix policies. Everything here compiles to Z3's string theory — len(...) becomes z3.Length, x in s becomes z3.Contains, and s.startswith(...) becomes z3.PrefixOf — so the prover reasons about the shape of text symbolically, across every reachable branch.

The trusted module exposes two side-effecting functions:

  • send_message(channel, text) — post text somewhere;
  • edit_file(path, new_text) — replace a file's contents.

The contract vocabulary then states policies an agent (or a user reviewing the permission request) cares about:

  • lengths within limits — length_at_most, length_at_least, length_between;
  • required or banned substrings — must_contain (e.g. a mandatory [automated] footer), must_not_contain (e.g. a banned token);
  • regex safety before sending — no_regex_metacharacters, which forbids every regular-expression metacharacter so agent- or user-influenced text cannot inject a pattern or trigger catastrophic backtracking (ReDoS) downstream;
  • bounded sends — sends_at_most;
  • file-edit policies — only_edit_under (a path-prefix sandbox), edit_length_at_most (bounded rewrites), and no_edits.

Trusted module

The trusted effects are stubs decorated with @clauz3.trusted and @clauz3.requires(...) preconditions on message text and file paths. The prover lifts each precondition into a proof obligation at every call site.

examples/text/tools/text/trusted/effects.py

import clauz3
from clauz3._path_safety import has_no_parent_segments


@clauz3.requires(lambda channel, text: len(text) > 0, message="text must be non-empty")
@clauz3.trusted
def send_message(channel: str, text: str) -> None:
    """Trusted text sender.

    Note: this is a mock function for testing; it won't *actually* post anything.

    Arguments:
      channel: where the text is posted.
      text: the body to send. Must be non-empty.
    """
    pass


@clauz3.requires(
    lambda path, new_text: has_no_parent_segments(path),
    message="path must not contain parent-directory segments",
)
@clauz3.requires(lambda path, new_text: len(path) > 0, message="path must be non-empty")
@clauz3.trusted
def edit_file(path: str, new_text: str) -> None:
    """Trusted file editor.

    Note: this is a mock function for testing; it won't *actually* edit a file.

    Arguments:
      path: file whose contents are replaced. Must be non-empty.
      new_text: the replacement contents.
    """
    pass

The contract module builds the string vocabulary on top of effect(send_message) and effect(edit_file), using the imported trusted functions. The length and substring checks live inside ordinary lambdas — the same relation language used elsewhere, just exercising its string operators.

examples/text/tools/text/trusted/contracts.py

"""String-manipulation predicates built from generic trusted effect facts.

Sent text is recorded under the ``send_message`` relation and file edits under
``edit_file`` (see ``effects.py``). These contracts let an agent state policies
about the *shape* of text it sends or writes:

- length bounds (``length_at_most`` / ``length_at_least`` / ``length_between``);
- required or banned substrings (``must_contain`` / ``must_not_contain``);
- freedom from regex metacharacters before text is fed to a pattern matcher
  (``no_regex_metacharacters``);
- where on disk an edit may land and how large it may be
  (``only_edit_under`` / ``edit_length_at_most``).

The length checks compile to ``z3.Length``, the substring checks to
``z3.Contains``, and the path-prefix checks to ``z3.PrefixOf`` via the
relation-lambda support in ``clauz3.spec``.
"""

from tools.text.trusted.effects import edit_file, send_message

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

Message = effect(send_message)
Edit = effect(edit_file)


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


@contract
def length_at_most(max_chars: int) -> ContractSpec:
    """Guarantee no sent text is longer than ``max_chars`` characters."""
    return Message.all(lambda e: len(e.text) <= max_chars)


@contract
def length_at_least(min_chars: int) -> ContractSpec:
    """Guarantee no sent text is shorter than ``min_chars`` characters."""
    return Message.all(lambda e: len(e.text) >= min_chars)


@contract
def length_between(min_chars: int, max_chars: int) -> ContractSpec:
    """Guarantee every sent text has length within ``[min_chars, max_chars]``."""
    return Message.all(lambda e: min_chars <= len(e.text) and len(e.text) <= max_chars)


@contract
def must_contain(substring: str) -> ContractSpec:
    """Guarantee every sent text contains ``substring`` (e.g. a required footer)."""
    return Message.all(lambda e: substring in e.text)


@contract
def must_not_contain(substring: str) -> ContractSpec:
    """Guarantee no sent text contains ``substring`` (e.g. a banned token)."""
    return Message.all(lambda e: substring not in e.text)


@contract
def no_regex_metacharacters() -> ContractSpec:
    """Guarantee no sent text contains a regular-expression metacharacter.

    Useful before passing agent- or user-influenced text into a system that
    treats it as (or interpolates it into) a regex: it rules out both pattern
    injection and pathological ``ReDoS`` constructs by construction.
    """
    return Message.all(
        lambda e: (
            "\\" not in e.text
            and "." not in e.text
            and "^" not in e.text
            and "$" not in e.text
            and "*" not in e.text
            and "+" not in e.text
            and "?" not in e.text
            and "(" not in e.text
            and ")" not in e.text
            and "[" not in e.text
            and "]" not in e.text
            and "{" not in e.text
            and "}" not in e.text
            and "|" not in e.text
        )
    )


@contract
def sends_at_most(count: int) -> ContractSpec:
    """Guarantee at most ``count`` messages are sent."""
    return Message.count() <= count


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


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


@contract
def edit_length_at_most(max_chars: int) -> ContractSpec:
    """Guarantee no file is rewritten with more than ``max_chars`` characters."""
    return Edit.all(lambda e: len(e.new_text) <= max_chars)

A passing case

Both messages are within the 20-character bound, so text.length_at_most(20) is discharged.

examples/text/cases/length_at_most_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.length_at_most(20))
def main() -> None:
    send_message("general", "ship it")
    send_message("alerts", "deploy finished ok")

A failing case

Text that will be fed to a pattern matcher must be metacharacter-free; the classic ReDoS pattern (a+)+$ violates text.no_regex_metacharacters() and the proof fails.

examples/text/cases/no_regex_metacharacters_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.no_regex_metacharacters())
def main() -> None:
    send_message("search", "(a+)+$")

All cases

Every file under cases/ is a small program plus its declared guarantee. Cases with the _pass suffix should prove; cases with _fail should be rejected. Browse the full set on the all-cases page.

How they run

The example Justfile invokes clauz3 prove against each case. _fail cases are wrapped so a non-zero exit is the expected outcome.

examples/text/Justfile

trusted := "tools/text/trusted"
prove := "uv run clauz3 prove --trusted-root " + trusted
# Proves each case in one process: *_pass.py must prove, *_fail.py must not.
prove-cases := "uv run python -m clauz3._prove_cases --trusted-root " + trusted

test: lint cases

lint:
    uv run clauz3 lint {{trusted}}/effects.py

cases:
    {{prove-cases}} cases/*_pass.py cases/*_fail.py