Theorem document schema

A .theorem file is a UTF-8 text file containing one or more YAML (YAML Ain't Markup Language) documents. Multiple documents within a single file are separated by ---. Each document describes one theorem.

Use theoremc::schema::load_theorem_docs to parse a .theorem file's contents into a vector of TheoremDoc structs:

use theoremc::schema::load_theorem_docs;

let yaml = std::fs::read_to_string("theorems/my_theorem.theorem")?;
let docs = load_theorem_docs(&yaml)?;

The function:

• Deserializes one or more YAML documents from the input string.
• Rejects unknown keys (any key not defined in the schema causes an error).
• Validates theorem identifiers and Forall keys against the identifier rules (see below).
• Validates Forall and Actions type strings as Rust types, rejecting free named lifetimes such as &'a T.
• Enforces non-empty constraints on string fields (see below).
• Returns Err(SchemaError) with an actionable message on failure.

When a concrete source path is available (for example, a fixture path or project file path), prefer load_theorem_docs_with_source so diagnostics include that source identifier:

use theoremc::schema::{SourceId, load_theorem_docs_with_source};

let source = "theorems/my_theorem.theorem";
let yaml = std::fs::read_to_string(source)?;
let docs = load_theorem_docs_with_source(&SourceId::new(source), &yaml)?;

Every theorem document is a YAML mapping with the following fields. Keys use TitleCase canonically, but lowercase aliases are also accepted (e.g., Theorem or theorem).

Theorem names and Forall map keys must satisfy:

• Match the ASCII pattern ^[A-Za-z_][A-Za-z0-9_]*$.
• Must not be a Rust reserved keyword (fn, let, match, type, self, Self, async, yield, etc.).

Invalid identifiers produce an InvalidIdentifier error with a message explaining why the identifier was rejected.

All string fields that carry semantic content must be non-empty after trimming (leading and trailing whitespace removed using Unicode-aware str::trim()). The loader rejects documents where any of the following fields are empty or contain only whitespace:

• About
• Assumption.expr and Assumption.because
• Assertion.assert and Assertion.because
• WitnessCheck.cover and WitnessCheck.because
• KaniEvidence.vacuity_because (when present)

The loader also enforces these structural constraints:

• The Prove section requires at least one assertion.
• Evidence.kani.unwind accepts only positive integers (> 0).
• At least one Witness entry is required when allow_vacuous is omitted or explicitly false.
• allow_vacuous: true is accepted only with a non-empty vacuity_because rationale.

The expression fields Assumption.expr, Assertion.assert, and WitnessCheck.cover must contain syntactically valid Rust expressions. The loader parses each expression using syn::Expr and rejects any expression that is not a single, value-producing form.

Accepted forms include comparisons, function and method calls, boolean literals, identifiers, arithmetic, if expressions, match expressions, closures, field access, and other standard Rust expressions:

Assume:
  - expr: "amount <= (u64::MAX - balance)"
    because: prevent overflow
Prove:
  - assert: "result.is_valid()"
    because: account invariants hold
Witness:
  - cover: "if x > 0 { x } else { 1 }"
    because: positive branch is exercised

Rejected forms include statement blocks, loops (for, while, loop), let bindings, unsafe/async/const blocks, assignments, and flow-control statements (return, break, continue):

# These will be rejected:
Assume:
  - expr: "{ let x = 1; x > 0 }"    # block expression
  - expr: "for i in 0..10 { }"       # for loop
  - expr: "x = 5"                    # assignment

The loader validates the structural constraints of Let bindings and Do steps:

• Every ActionCall.action field (in both Let bindings and Do steps) must be non-empty after trimming. Blank action names are rejected.
• Every non-blank ActionCall.action must follow canonical action-name grammar: Segment ("." Segment)+ (at least one . separator).
• Each canonical action-name segment must match ^[A-Za-z_][A-Za-z0-9_]*$ and must not be a Rust reserved keyword.
• Every MaybeBlock.because field must be non-empty after trimming.
• Every MaybeBlock.do list must contain at least one step (an empty maybe block is meaningless).
• Validation recurses into nested maybe blocks. A maybe containing another maybe with a blank because is caught with a full path context (e.g., "Do step 2: maybe.do step 1: maybe.because must be non-empty").
• Let bindings accept only call or must variants. A maybe block inside Let is rejected at the deserialization level.

Assumption: a constraint on symbolic inputs. Both expr and because are required and must be non-empty after trimming.

Assume:
  - expr: "amount <= u64::MAX"
    because: "prevent overflow"

Assertion: a proof obligation. Both assert and because are required and must be non-empty after trimming.

Prove:
  - assert: "balance == expected"
    because: "deposit adds to balance"

WitnessCheck: a non-vacuity witness. Both cover and because are required and must be non-empty after trimming.

Witness:
  - cover: "amount == 50"
    because: "mid-range deposit is exercised"

LetBinding: a named value binding. Must be one of call or must.

Let:
  params:
    must:
      action: account.params
      args: { max_balance: 1000 }
  result:
    call:
      action: account.deposit
      args: { account: { ref: a }, amount: { ref: amount } }

Step: an element of the Do sequence. Must be one of call, must, or maybe.

Do:
  - call:
      action: account.deposit
      args: { account: { ref: a }, amount: 100 }
  - must:
      action: account.validate
      args: { account: { ref: result } }
  - maybe:
      because: "optional second deposit"
      do:
        - call:
            action: account.deposit
            args: { account: { ref: result }, amount: 10 }

ActionCall: an invocation of a theorem action.

• action (required): dot-separated action name (e.g., account.deposit).
• action must use canonical grammar (Segment ("." Segment)+), where each segment is an ASCII identifier and not a Rust reserved keyword.
• args (required): mapping of parameter name to value.
• as (optional): binding name for the return value.

Evidence: backend configuration. Currently, supports kani, with verus and stateright as placeholders. The Evidence section is required for every theorem document, and theorem_file! requires an Evidence.kani entry so it can generate the Kani proof harness. Omitting Evidence.kani causes macro expansion to fail with MissingKaniEvidence.

Evidence:
  kani:
    unwind: 10
    expect: SUCCESS

KaniEvidence fields:

• unwind (required): positive integer, must be > 0 (loop unwinding bound).
• expect (required): one of SUCCESS, FAILURE, UNREACHABLE, or UNDETERMINED.
• allow_vacuous (optional, default false): whether vacuous success is permitted. When omitted, behaviour is identical to allow_vacuous: false.
• vacuity_because (required when allow_vacuous is true): human-readable justification. Must be non-empty after trimming.

After YAML deserialization, each action argument value is decoded into an ArgValue that distinguishes literals from variable references. This encoding ensures that plain YAML strings are unconditionally treated as string literals and variable references require the explicit { ref: <name> } wrapper.

• ArgValue::Literal(LiteralValue::Bool(b)) — a YAML boolean (true/false).
• ArgValue::Literal(LiteralValue::Integer(n)) — a YAML integer.
• ArgValue::Literal(LiteralValue::Float(f)) — a YAML float.
• ArgValue::Literal(LiteralValue::String(s)) — a plain YAML string. Plain strings are always string literals, regardless of whether a Let binding with the same name exists in the same theorem.
• ArgValue::Reference(name) — an explicit variable reference via { ref: <name> }. The name must be a valid ASCII identifier (^[A-Za-z_][A-Za-z0-9_]*$) and must not be a Rust reserved keyword.
• ArgValue::RawSequence(values) — a YAML sequence. During proof harness generation (Phase 3), sequences are recursively lowered to vec![...] macro expressions. Nested sequences, scalars, and references are supported.
• ArgValue::RawMap(map) — any YAML map that is not a single-key sentinel wrapper. During proof harness generation (Phase 3), maps are lowered to struct literals using the expected parameter type name. Field values are lowered recursively. Multi-key maps are never treated as wrappers, even when one of their keys is ref or literal.

Semantic stability invariant: adding a new Let binding can never silently change the meaning of an existing argument that was previously a plain string. A plain string "x" always decodes as ArgValue::Literal(String("x")), even if a binding named x exists. To reference a binding, use { ref: x }.

args:
  name: "hello"              # → ArgValue::Literal(String("hello"))
  count: 42                  # → ArgValue::Literal(Integer(42))
  enabled: true              # → ArgValue::Literal(Bool(true))
  graph_ref: { ref: graph }  # → ArgValue::Reference("graph")
  label: { literal: "graph" }  # → ArgValue::Literal(String("graph"))
  opts: { timeout: 30 }     # → ArgValue::RawMap (future: struct literal)

Invalid reference targets produce actionable error messages:

• { ref: "" } — "ref value must not be empty"
• { ref: fn } — "ref value 'fn' is a Rust reserved keyword"
• { ref: 123bad } — "ref value '123bad' is not a valid identifier"
• { ref: 42 } — "ref value must be a string identifier, not an integer"

Explicit literal wrappers produce string literals when the value is a string. Non-string values are rejected:

• { literal: "graph" } — ArgValue::Literal(LiteralValue::String("graph")).
• { literal: "" } — ArgValue::Literal(LiteralValue::String("")) (empty string is valid).
• { literal: 42 } — "literal value must be a string, not an integer".
• { literal: true } — "literal value must be a string, not a boolean".

Lowering limitations (current implementation):

• Nested maps within composite values (maps inside lists, or maps as field values within other maps) are not yet supported because field type information requires Phase 3 compile-time type probes. Attempts to lower nested maps produce a clear error directing users to use explicit let-bindings for nested struct construction. Top-level map arguments and lists of scalars/references are fully supported.
• Type shape restrictions: Only simple type paths (MyStruct, module::Type) are supported as expected parameter types. Generic types, references, and tuple types require explicit handling and may produce unsupported type errors during lowering.

Supported YAML value forms (summary):

• YAML booleans → Rust boolean literals (true, false).
• YAML integers → Rust unsuffixed integer literals (42, not 42i64).
• YAML floats → Rust unsuffixed float literals (99.5, not 99.5f64).
• YAML strings → Rust string literals ("hello"). Plain strings are always literals.
• YAML lists → vec![...] macro expressions (lowered recursively during Phase 3 harness generation). Nested lists, scalars, and references are supported. Empty lists are allowed (vec![]).
• YAML maps → Rust struct literals (lowered during Phase 3 harness generation using the expected parameter type name). Field values are lowered recursively. Unknown fields, missing fields, and type mismatches surface as Rust compilation errors, not theoremc validation errors.
• Single-key sentinel wrappers: { ref: name } → ArgValue::Reference, { literal: "text" } → ArgValue::Literal. All other YAML maps (including multi-key maps such as { literal: "x", other: 1 }) pass through as ArgValue::RawMap for struct-literal lowering.

load_theorem_docs and load_theorem_docs_with_source return Result<Vec<TheoremDoc>, SchemaError>, where SchemaError has six variants:

• Deserialize { message, diagnostic } — YAML parsing or schema mismatch error.
• InvalidIdentifier { identifier, reason } — identifier validation failure.
• InvalidActionName { action, reason } — action name grammar or keyword validation failure.
• ValidationFailed { theorem, reason, diagnostic, source } — structural constraint violation (e.g., empty Prove section or no Evidence backend), or a raw-to-public decode failure with its original source error preserved.
• MangledIdentifierCollision { message } — two or more different canonical action names produce the same mangled Rust identifier.
• DuplicateTheoremKey { theorem_key, collisions, diagnostic } — two theorem documents loaded from the same source produce the same literal theorem key {P}#{T}, with structured collision diagnostics for each duplicate key.

For parse failures, validation failures, and duplicate theorem-key failures, diagnostic includes structured location metadata when available:

• stable code (schema.parse_failure or schema.validation_failure),
• source identifier,
• line and column,
• deterministic fallback message.

Use SchemaError::diagnostic() to access this payload for custom rendering, snapshot assertions, or editor integration. For duplicate theorem-key errors, callers can also inspect SchemaError::DuplicateTheoremKey { theorem_key, collisions, diagnostic } directly to enumerate every colliding theorem key in stable order.

All variants produce actionable error messages suitable for display to theorem authors.