Skip to main content
Version: latest

Syntax & x07AST (JSON)

X07 uses a structured syntax called x07AST.

  • Humans can work with a pretty form.
  • Agents should operate directly on the JSON AST (no fragile text edits).

Why JSON AST?​

Text-based syntaxes (even simple ones) often fail under autonomous patching:

  • parentheses drift
  • braces drift
  • indentation drift
  • accidental truncation

A JSON AST:

  • is easy to validate,
  • is easy to patch with JSON Patch,
  • is easy to autoformat deterministically,
  • makes tooling (lint/repair) reliable.

Core expression model​

x07AST is an expression tree:

  • lists: ["head", arg1, arg2, ...]
  • identifiers: "std.bytes.len" (string)
  • integers: 123 (number)

The entrypoint expression returns bytes.

Boolean operators (i32)​

X07 represents booleans as i32 (0 = false, nonzero = true).

  • & / |: eager bitwise ops (both sides are evaluated).
  • && / ||: short-circuit logical ops (RHS is evaluated only when needed; result is 0 or 1).

Schema version​

The root JSON object must include schema_version.

Current schema version:

  • x07.x07ast@0.8.0

The toolchain also accepts legacy schema versions:

  • x07.x07ast@0.7.0 (programs with async protocol contracts but without function decreases)
  • x07.x07ast@0.6.0 (programs with loop contracts but without async protocol contracts)
  • x07.x07ast@0.5.0 (programs with function contracts but without loop contracts)
  • x07.x07ast@0.4.0 (programs without contracts)
  • x07.x07ast@0.3.0 (concrete-only programs)

Tooling (x07 ast init, x07 fmt, x07 lint) keeps the AST compatible with the current schema.

Generics (v0.4)​

x07AST v0.4 adds:

  • type_ref in signatures (either legacy concrete type tokens or structured type expressions)
  • type_params on defn / defasync
  • tapp at call sites
  • ty.* intrinsics for type-dependent ops inside generic bodies

See Generics.

Contracts (v0.5)​

x07AST v0.5 adds first-class function contracts:

  • Optional fields on defn / defasync declarations:
    • requires: array of preconditions
    • ensures: array of postconditions
    • invariant: array of function-level invariants
  • Each clause is an object:
    • id (optional string)
    • expr (expression; must typecheck to i32)
    • witness (optional array of expressions; evaluated only on failure)

Notes:

  • Contract expressions and witnesses must be contract-pure (no world.*, task.*, mutation forms, etc.).
  • __result is reserved and is only available inside ensures expressions.

Contract-pure allowlist​

Contract expressions and witnesses may only call contract-pure builtins/operators:

  • Operators: +, -, *, /, %, =, !=, <, <=, >, >=, <u, <=u, >u, >=u, <<u, >>u, &, |, ^, &&, ||.
  • Builtins: bytes.lit, bytes.view_lit, i32.lit, bytes.view, bytes.subview, bytes.len, bytes.get_u8, bytes.eq, bytes.cmp_range, view.len, view.get_u8, view.slice, view.to_bytes.
  • Also allowed: any builtin head with prefix option_* or result_*.

Module calls (like foo.bar) are not allowed in contracts.

Loop contracts (v0.6)​

x07AST v0.6 adds loop_contracts on defn declarations so proof mode can reason about for loops without widening the certifiable subset to recursion.

Each item points at a loop body by JSON Pointer and declares:

  • invariant[]: clauses that must hold at loop entry and every iteration
  • decreases[]: lexicographic rank terms used to prove termination

Minimal shape:

"loop_contracts": [
  {
    "ptr": "/decls/0/body/4",
    "invariant": [
      { "id": "i_nonneg", "expr": [">=", "i", 0] }
    ],
    "decreases": [
      { "expr": ["-", "n", "i"] }
    ]
  }
]

Use x07 verify --prove with loop_contracts when the certified surface needs loops; combine them with decreases on defn when the same pure core also uses self-recursion.

Function termination clauses (v0.8)​

x07AST v0.8 adds decreases on defn declarations so pure self-recursive functions can stay inside the certifiable proof subset.

decreases uses the same contract-clause object shape as requires / ensures / invariant and declares the lexicographic rank that must descend on recursive self-calls.

Minimal shape:

{
  "kind": "defn",
  "name": "main.count_down",
  "params": [{"name":"n","ty":"i32"}],
  "result": "i32",
  "requires": [{"id":"r0","expr":[">=","n",0]}],
  "decreases": [{"id":"d0","expr":"n"}],
  "body": ["if",["=","n",0],0,["main.count_down",["-","n",1]]]
}

Mutual recursion and recursive defasync targets remain outside the current certifiable subset.

Async protocol contracts (v0.7)​

x07AST v0.7 adds protocol on defasync declarations so async code can declare proof obligations across suspension points and task scopes.

protocol may include:

  • await_invariant[]
  • scope_invariant[]
  • cancellation_ensures[]

These clauses use the same contract-clause object shape as requires / ensures / invariant, and they must remain contract-pure.

Branded bytes annotations​

X07 can attach a nominal brand to bytes-like parameters and results to model “validated bytes of encoding X” (compile-time only).

In defn/defasync declarations:

  • params[] entries may include optional brand when ty is bytes-like.
  • result_brand may be provided when result is bytes-like.

Example:

{
  "kind": "defn",
  "name": "main.parse_x7sl",
  "params": [{"name":"b","ty":"bytes"}],
  "result": "result_bytes",
  "result_brand": "std.text.slices.x7sl_v1",
  "body": ["std.text.slices.cast_bytes_v1","b"]
}

Tooling​

For a full project skeleton (x07.json, lockfile, src/, tests/), use x07 init. The x07 ast subcommands are for working with individual *.x07.json files.

  • x07 ast init / x07 ast validate:
    • generates and validates *.x07.json skeletons
  • x07 fmt:
    • canonicalizes JSON (JCS) and ensures stable emission
  • x07 lint:
    • checks schema + semantic constraints
    • prints x07diag (machine-readable diagnostics)
  • x07 fix:
    • applies quickfixes (JSON Patch) and rewrites *.x07.json deterministically
  • x07 ast apply-patch:
    • applies RFC 6902 JSON Patch deterministically (agent-safe edits)
  • x07 ast schema:
    • emits the canonical JSON Schema for constrained/structured generation engines
  • x07 ast grammar --cfg:
    • emits GBNF variants plus semantic supplement for grammar-constrained decoding

Common mistakes (and the canonical fixes)​

1) Using multi-step logic where a single expression is required​

Fix: wrap with ["begin", ...].

2) Returning the wrong type from the entrypoint​

Fix: ensure the final expression is bytes.

3) Calling OS-only builtins in fixture worlds​

Fix: keep OS builtins behind OS adapters and world checks.