---
title: "world-lang-lexing — Mova code model"
description: "Mova code model of world/src/lang.rs: components with their labels, obernants and the model text."
url: "https://groupants.elamur.ai/free/en/mova/world/src/lang.rs.groupant/lexing.groupant/"
---
Elamur: [Mova](https://md.mova.elamur.ai/free/en/) · [Dictionary](https://md.dictionary.elamur.ai/free/en/) · [Research](https://md.research.elamur.ai/free/en/) · **Groupants**

This page as HTML: <https://groupants.elamur.ai/free/en/mova/world/src/lang.rs.groupant/lexing.groupant/>

# world-lang-lexing

The groupant beside world/src/lang.rs in the Mova repository: what the code computes, what it never does, how to go back from its outputs, its invariants, cost and checks.

## Facts

- **kind:** groupant_fragment
- **status:** partial source derived instance
- **source:** [`world/src/lang.rs`](https://github.com/ElamurAI/mova-free/blob/main/world/src/lang.rs)
- **source SHA-256:** `9bcaf61d3d16dd69…`
- **covers:** Source bytes [11633,16968): lexing; the operation-specific contracts below define observation projections. (bytes 11633–16968)
- **part of:** [world-lang](https://md.groupants.elamur.ai/free/en/mova/world/src/lang.rs.groupant/)
- **repository folder:** [`world/src/lang.rs.groupant/lexing.groupant`](https://github.com/ElamurAI/mova-free/tree/main/world/src/lang.rs.groupant/lexing.groupant)
- **repository commit:** `855da7bd4a7b`

> **Implementation material.** A Mova code model describes this code at one source revision: partial models, finite checks and their stated scope. It is not a reviewed general exposition, and its labels are shown as written, never raised.

## Components

| component | label | where |
|---|---|---|
| **approximant** | partial | [Forward](#forward) |
| **ast** | partial | `../syntax.json` |
| **composition** | partial | [Composition](#composition) |
| **cost** | symbolic unmeasured | [Cost](#cost) |
| **descriptant** | present | `model.md` |
| **invariant** | partial | [Invariant](#invariant) |
| **tests** | bounded evidence | [tests](#tests) |

## Obernants

The typed relations around the forward model: the behaviour complement (what the code never does), the reverse reconstruction (every input compatible with an output) and specialised views.

| id | type | label | where |
|---|---|---|---|
| `nonbehavior` | behavior_complement | partial source derived model | [nonbehavior](#nonbehavior) |
| `antecedents` | reverse_reconstruction | partial source derived model | [antecedents](#antecedents) |
| `quotes_keys` | lexical_projection | partial source derived model | [quotes_keys](#quotes-keys) |
| `duplicate_order` | failure_precedence | partial source derived model | [duplicate_order](#duplicate-order) |
| `consumption` | state_transition | partial source derived model | [consumption](#consumption) |

## Model text


### descriptant

## world-lang-lexing

### Forward

tokens groups characters between literal double quotes and splits Unicode whitespace outside; there is no escape syntax. Args requires lowercase ASCII key names, splits the first '=', rejects repeated spellings and positions after any key, and validates complete outer quote pairs. text trims value edges; quote flags are enforced by ID/word consumers but intentionally ignored by some numeric/tag/text consumers. Args scans token order. Invalid key syntax precedes duplicate detection for that token; duplicate detection precedes quote validation. A malformed later command cannot override an earlier duplicate or positional-after-key error. Oracle checks unknown command plus duplicate keys. take removes the first matching key preserving order of remaining triples. Typed consumers propagate a first error; attrs consumes all remaining keys in order. done rejects first remaining position before first remaining key. Quote handling differs by consumer; there is no universal quoted-value ban.

Scope: Source bytes [11633,16968): lexing; the operation-specific contracts below define observation projections.

### Invariant

The parser is pure and never executes a command. IDs are syntax-checked and registry-filtered; their existence is not checked. Cmd projection may lose spelling, while Line retains trimmed raw and supplied no; FormatErr retains original raw. At most one success or error is produced per nonempty input line. Rejected lines do not suppress later parse_all lines.

### Composition

The root composes interfaces, tokenization/Args, scalar/collection validators, v1/v2 dispatch, narrative dispatch and line admission. Output of each stage is the exact next-stage input: quotes and consumed-key state cannot be independently reconstructed without matching the same original line. parse_line orders stages as trim, tokens, reverse-tail anchors, misplaced-anchor check, Args, command, unused arguments, fallback anchor. parse_all preserves input positions while partitioning successes/errors and skipping blank lines. Six scoped fragments bind concrete source ranges; the remaining parse_all and test regions are modeled at root. This hierarchy does not include executor or query semantics.

### Cost

For total input bytes N and line count L, a conservative whole-file time bound is O(N^2+L) under fixed closed vocabularies: duplicate-key/list scans and vector removals can be quadratic. Tokenization itself is O(N); accumulated output and peak retained parse storage are O(N+L) excluding caller-owned input and allocator overhead. No runtime speedup or finite error budget is claimed.

### Limits

Partial syn-2 projection binds the whole file; macros remain opaque and no name resolution, type inference, semantic AST or formal proof is supplied. types::* supplies Id parsing, Closed catalogs, field domains, value normalization and text limits; prag::schema::Act supplies speech acts. No state existence, reference resolution, world mutation, temporal consistency, truth of claims or query behavior is certified. No live commands, annotator, environment mutations, filesystem or external services are used in native tests. No useful approximate semantics or faster Rust surrogate is declared for these categorical gates.

### Epoch memory

2026-10-30 prospective model: relation endpoints must be characters, snapshot-looking C1@1 must fail ID parsing, repeated keys fail before command dispatch, quoted text groups whitespace, and explicit placement is exclusive. Complete bounded relation fibers use 784 strings and independent character-only expected antecedents. Current source admits ^s0 and duplicate anchors, allows distinct alias keys at/to to map to repeated Field::At values, and accepts numeric quantities through six digits (999999), despite num's 0-100000 comment. These are recorded behavior/policy gaps, not silently changed. An initial fixture used unsupported act=inform; corrected to the actual Act catalog's assert before final evidence. No production behavior was changed. Native measurements and the compiled endpoint mutant are recorded in evidence.json.

### catalog

## world-lang-lexing

Domain: Finite UTF-8 change-language lines with fixed types::* closed sets and prag::schema::Act; finite line numbers. Observation is Option<Line> or FormatErr. Inverse syntax fibers project to Cmd plus anchors and intentionally omit raw/no; full Line observations retain trimmed spelling and supplied line number. No world state or I/O is an input.

Scope: Source bytes [11633,16968): lexing; the operation-specific contracts below define observation projections.

Let U be admitted inputs paired with typed outputs for the named operation, R its fixed-source relation. Behavior complements below are candidate inner bounds of U minus R; source inspection and bounded witnesses do not prove global completeness. Reverse models retain all compatible antecedents in their declared domain, not one preferred spelling. No inverse recovers discarded whitespace unless raw text is observed.

### nonbehavior

Unclosed quote state cannot produce tokens; Args rejects non-lowercase key bytes, a duplicate exact key, a positional token after keys or a bare quoted text positional argument.

Domain and scope are fixed above. Evidence: tests.md names the independent finite native oracle; untested cases remain conditional source models. No semantic proof follows from a manifest.

### antecedents

Given Args.pos and ordered (key,value,quoted) triples, retain all whitespace-separated token strings with the same quote grouping. Prefix/suffix whitespace is unobserved by tokens; literal internal whitespace inside quoted values is preserved until a later text consumer trims it.

Domain and scope are fixed above. Evidence: tests.md names the independent finite native oracle; untested cases remain conditional source models. No semantic proof follows from a manifest.

### quotes_keys

tokens groups characters between literal double quotes and splits Unicode whitespace outside; there is no escape syntax. Args requires lowercase ASCII key names, splits the first '=', rejects repeated spellings and positions after any key, and validates complete outer quote pairs. text trims value edges; quote flags are enforced by ID/word consumers but intentionally ignored by some numeric/tag/text consumers.

Domain and scope are fixed above. Evidence: tests.md names the independent finite native oracle; untested cases remain conditional source models. No semantic proof follows from a manifest.

### duplicate_order

Args scans token order. Invalid key syntax precedes duplicate detection for that token; duplicate detection precedes quote validation. A malformed later command cannot override an earlier duplicate or positional-after-key error. Oracle checks unknown command plus duplicate keys.

Domain and scope are fixed above. Evidence: tests.md names the independent finite native oracle; untested cases remain conditional source models. No semantic proof follows from a manifest.

### consumption

take removes the first matching key preserving order of remaining triples. Typed consumers propagate a first error; attrs consumes all remaining keys in order. done rejects first remaining position before first remaining key. Quote handling differs by consumer; there is no universal quoted-value ban.

Domain and scope are fixed above. Evidence: tests.md names the independent finite native oracle; untested cases remain conditional source models. No semantic proof follows from a manifest.

### tests

#### Native bounded evidence

Six inline lang::bounded_models tests call pure parser/helpers only. Command inventory checks one fixture for all 25 variants and the six v3 names. Complete relation fibers exhaust 14 endpoint strings squared, two field orders and two separators: 784 strings, 16 admitted into four Cmd/anchor fibers and 768 rejected. The expected inverse sets are constructed from independent table indices, not parser outputs. The role matrix checks 5 roles against 9 registry prefixes; further fixtures check joint bounds, snapshots, malformed quotes, exact duplicate keys, first-error ordering, exclusive placement, cross-field gates, text limits, values and parse_all partition.

Run cargo test -p world --lib lang::bounded_models -- --test-threads=1, twice in debug and twice with --release. Normalize only these six named outcomes and compare. A compiled production mutant admits objects as the a endpoint of rel; the complete fiber assertion must fail, then restored source must pass. Generate mova-modelcheck syntax twice and compare. Reports and source/log hashes are in file-root evidence.json; raw logs live outside the repository under the named run directory. Existing tests elsewhere are not included. Finite evidence is not a full Rust proof or live executor test.