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 @deal.has(...) and a non-empty precondition. The prover lifts each precondition into a proof obligation at every call site.

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

import deal


@deal.pre(lambda channel, text: len(text) > 0, message="text must be non-empty")
@deal.has("send", "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


@deal.pre(lambda path, new_text: len(path) > 0, message="path must be non-empty")
@deal.has("edit", "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 the generic effect("send_message") and effect("edit_file") relations. Note that 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 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"
effects := trusted + "/effects.py"
prove := "uv run clauz3 prove --trusted-root " + trusted

test: lint cases

lint:
    uv run python -m deal lint {{effects}}

cases: length-at-most-pass length-at-most-fail length-at-least-pass length-at-least-fail length-between-pass length-between-branch-pass must-contain-pass must-contain-fail must-not-contain-pass must-not-contain-fail no-regex-metacharacters-pass no-regex-metacharacters-fail sends-at-most-pass sends-at-most-fail empty-text-precondition-fail text-no-guarantees-pass only-edit-under-pass only-edit-under-fail edit-length-at-most-pass edit-length-at-most-fail no-edits-pass no-edits-fail

length-at-most-pass:
    {{prove}} cases/length_at_most_pass.py

length-at-most-fail:
    if {{prove}} cases/length_at_most_fail.py; then exit 1; fi

length-at-least-pass:
    {{prove}} cases/length_at_least_pass.py

length-at-least-fail:
    if {{prove}} cases/length_at_least_fail.py; then exit 1; fi

length-between-pass:
    {{prove}} cases/length_between_pass.py

length-between-branch-pass:
    {{prove}} cases/length_between_branch_pass.py

must-contain-pass:
    {{prove}} cases/must_contain_pass.py

must-contain-fail:
    if {{prove}} cases/must_contain_fail.py; then exit 1; fi

must-not-contain-pass:
    {{prove}} cases/must_not_contain_pass.py

must-not-contain-fail:
    if {{prove}} cases/must_not_contain_fail.py; then exit 1; fi

no-regex-metacharacters-pass:
    {{prove}} cases/no_regex_metacharacters_pass.py

no-regex-metacharacters-fail:
    if {{prove}} cases/no_regex_metacharacters_fail.py; then exit 1; fi

sends-at-most-pass:
    {{prove}} cases/sends_at_most_pass.py

sends-at-most-fail:
    if {{prove}} cases/sends_at_most_fail.py; then exit 1; fi

empty-text-precondition-fail:
    if {{prove}} cases/empty_text_precondition_fail.py; then exit 1; fi

text-no-guarantees-pass:
    {{prove}} cases/text_no_guarantees_pass.py

only-edit-under-pass:
    {{prove}} cases/only_edit_under_pass.py

only-edit-under-fail:
    if {{prove}} cases/only_edit_under_fail.py; then exit 1; fi

edit-length-at-most-pass:
    {{prove}} cases/edit_length_at_most_pass.py

edit-length-at-most-fail:
    if {{prove}} cases/edit_length_at_most_fail.py; then exit 1; fi

no-edits-pass:
    {{prove}} cases/no_edits_pass.py

no-edits-fail:
    if {{prove}} cases/no_edits_fail.py; then exit 1; fi