---
title: "modelcheck-sections — Mova code model"
description: "Mova code model of tools/modelcheck/src/sections.rs: components with their labels, obernants and the model text."
url: "https://groupants.elamur.ai/free/en/mova/tools/modelcheck/src/sections.rs.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/tools/modelcheck/src/sections.rs.groupant/>

# modelcheck-sections

The groupant beside tools/modelcheck/src/sections.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
- **status:** partial source derived
- **source:** [`tools/modelcheck/src/sections.rs`](https://github.com/ElamurAI/mova-free/blob/main/tools/modelcheck/src/sections.rs)
- **source SHA-256:** `c05b5d875d6fffdd…`
- **repository folder:** [`tools/modelcheck/src/sections.rs.groupant`](https://github.com/ElamurAI/mova-free/tree/main/tools/modelcheck/src/sections.rs.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** | source derived | [Forward](#forward) |
| **ast** | partial | `syntax.json` |
| **composition** | partial | [Composition](#composition) |
| **cost** | symbolic unmeasured | [Cost](#cost) |
| **descriptant** | present | [Descriptant](#descriptant) |
| **invariant** | source derived | [Invariant](#invariant) |
| **tests** | bounded executed | [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 |
|---|---|---|---|
| `behavior_complement` | behavior_complement | partial source derived | [behavior_complement](#behavior-complement) |
| `reverse_reconstruction` | reverse_reconstruction | partial source derived | [reverse_reconstruction](#reverse-reconstruction) |

## Parts

- [modelcheck-library-section-fences](https://md.groupants.elamur.ai/free/en/mova/tools/modelcheck/src/sections.rs.groupant/section-fences.groupant/)

## Model text


### Descriptant

`sections.rs` holds the narrow Markdown section grammar that groupant references and the one-file consolidation share: line splitting with fence state, plain H2 headings, section byte selection, `file#Section` splitting, GitHub-style anchors and heading demotion. It is not a Markdown renderer: no setext headings, HTML blocks, lists, containers or inline markup.

Epoch 2026-11-04 (source revision in the manifest): created when each groupant became one `model.md` with blocks. The fence automaton moved here from `lib.rs`; its fragment is `section-fences.groupant`.

### Forward

For text T split at `\n` (CRLF terminators stripped from the line text, kept in spans):

- `lines(T)`: per line the text, byte span and `fenced`, true for fence delimiters and every line inside a fence. A fence opens on 0–3 spaces then ≥3 backticks or tildes (a backtick info string has no backtick) and closes on the same marker, at least as long, followed only by spaces or tabs. An unclosed fence marks every remaining line.
- `h2_names(T)`: rest of each unfenced line starting with `## `; `heading_count(T,S)`: number of unfenced lines equal to `## S`.
- `section_bytes(T,S)`: when `heading_count=1`, the bytes from the heading line start to the end of the last nonblank line before the next unfenced `## ` line (or end of text), without its terminator; otherwise none.
- `split_reference(r)`: `(file, Some(section))` at the first `#`, else `(r, None)`.
- `anchor(name)`: trimmed, lowercased; spaces become `-`; only alphanumerics, `-` and `_` stay.
- `heading_level(line)`: ATX level 1–6 after 0–3 spaces, followed by end, space or tab. `min_heading_level(T)` over unfenced lines.
- `demote(T,k)`: adds k `#` after the indent of every unfenced ATX heading line; other bytes unchanged. Returns the count of headings pushed past level 6.

### Invariant

Only unfenced exact `## S` lines select sections; a missing or duplicate heading never yields bytes. `section_bytes` is a substring of T that starts with `## S`. `demote` changes only unfenced heading lines and only by inserting `#` characters, so removing the same k characters from those lines restores T. Fence state after a closed fence equals the initial state.

### Cost

O(B) time over the B bytes of T for each call, O(L) line records for L lines; `section_bytes` scans twice (count, then selection). No allocation beyond the line vector, the heading string and the demoted output.

### Composition

`lib.rs` uses `heading_count`, `split_reference` and `section_bytes` (through `reference_bytes`) for component sections and hash-bound section references. `consolidate.rs` uses all of the module: verbatim/wrapped decisions, collision anchors, demotion, unclosed-fence refusal and section rebinding. `mova-correspondence` uses `split_reference` and `section_bytes` for catalogue model bindings. The child `section-fences.groupant` refines the fence automaton range.

### Tests

`sections::tests::sections_follow_the_plain_h2_grammar` (fenced heading ignored, duplicates rejected, unclosed fence detected, split and anchor) and `sections::tests::demotion_is_reversible_and_skips_fences` (fenced lines, non-headings and overflow). Integration: `consolidate::tests` and the groupant validation controls in `lib.rs`.

### behavior_complement

The module never selects a section for zero or several matching headings, never treats a fenced, indented (≥4 spaces), padded or `##`-without-space line as a heading, never rewrites non-heading lines in `demote`, and never resolves paths, reads files or interprets inline Markdown, HTML or setext headings.

### reverse_reconstruction

Given `section_bytes(T,S)=X`, every T whose unique `## S` section has exactly those bytes is compatible; the other sections, the preamble and trailing blank lines are unconstrained. Given `demote(T,k)=D` with known k, T is unique (remove k `#` from each unfenced heading line of D); with unknown k, every k with all heading levels of D above k is compatible. Given `anchor(n)=a`, all names differing only in case, removed punctuation or surrounding whitespace are compatible.