📐modelcheck-undate

The groupant beside tools/modelcheck/src/undate.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

Components

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.

Model text

Descriptant

undate.rs implements mova-modelcheck undate REPO [--dry-run] NEW_REPORT. The main blocks of a groupant model.md state what is now; dated material and provenance (digests, concrete run paths under the data directory) live verbatim in one final ## History section. A section that a JSON record selects keeps its current substance: its dated sentences stay, mechanically rewritten without dates, while History keeps them verbatim; a selected section left heading-only gets its current body back from its newest History group. Mechanics only: no line is deleted, no model content is judged.

Forward

Inputs: Git-visible files of REPO (tracked and nonignored untracked). Targets are files named model.md inside a *.groupant/ directory. Protected names are every section value and every model.md#<Name> suffix in a tracked JSON string. The selection of a file is the set of its sections that some JSON record selects: path plus section in one object, or a file.md#Section value, resolved from the JSON file's directory.

1. Lines are classified outside code fences: blank, ATX heading, fenced, text. A heading block runs to the next heading of the same or a higher level (H1 lines end every block and never move). Text splits into units: a paragraph, one list item with its continuation, one table, one fenced block; a paragraph whose lines (except the last) each end a clause splits into record lines.
2. An epoch date is YYYY-MM-DD with year 2025 to 2029, not adjacent to digits; a toolchain build date (<hex commit> DATE) and a data snapshot date followed by run, dump, English dump or snapshot are not epoch dates. Provenance is a concrete path under the data directory variable (the variable followed by /, without a <placeholder>), a run of 40 or more lowercase hex digits that contains a digit, or seven or more such digits followed by ….
3. strip_line rewrites one line: a dated heading takes its undated name (Drop when nothing remains); an inline code span holding a date or provenance, a bare provenance token and a token in which a date is glued to an identifier become (see History); a date is removed with its frame ((D), ; D), (D, , a sentence-leading Epoch D (…): or D,, a preposition such as as of, on, since, or a separator such as , D, — D, D:), then spacing and punctuation are tidied and a sentence start is capitalized. A record line labelled Date:, Run root:, Commit: and similar, a History note, and a line left without letters or digits Drop. A heading holding provenance Fails. Fenced lines and lines without dates or provenance Keep unchanged.
4. Per H2 section: a unit with an epoch date or provenance goes to History; its key is its first date, else the date of the enclosing kept dated heading, else the last date seen earlier in the section, else Undated. In a selected section the unit also stays, rewritten line by line, when no line Fails and at least one line is kept. Otherwise it moves. A dated heading block moves whole, except the section lead: the first dated heading before any undated prose of the section stays in place under its undated name with a History note that quotes the original line. An undated block whose every unit moved moves whole, unless its name is a core block name (descriptant, domain, forward, reverse, invariant, cost, checks, tests, limits, limitations, composition, approximant); then only its units move and the heading stays. Code is neutral: it stays with a block that stays and moves with one that moves.
5. A dated H2 section moves whole unless protected. A dated H1 is renamed in place with a note.
6. Removal collapses the blank runs it leaves. History groups are ### <date> · <origin section>, sorted by date with Undated last, stable in document order, consecutive equal groups merged; a moved block's top heading is raised to H4. An existing History is parsed into its groups and new entries merge into it.
7. refill: every selected H2 section with nothing but blank lines and headings gets a body inserted after its heading. The History groups of that origin are tried newest first (dated keys descending, Undated last); the first whose restate is nonempty wins. restate passes every line of the group through strip_line; a unit with a Failing line or with nothing kept is left out, a fence follows only a kept paragraph, a heading only kept content. History is not changed. A selected section that no group restates is reported as residue.
8. Every changed file passes verify and a second run returns it unchanged. Then fresh hash-bound JSON references (path plus sha256 in one object) to changed files are rebound: a section's bytes for model.md#<S>, the whole file otherwise; JSON files changed by a rebind become targets of the next round until a fixpoint. Already stale bindings are reported and left stale. Without --dry-run all changed files are written. The report counts moved blocks and units, stripped units, refilled and residue sections.

Invariant

Nonblank lines are preserved as a multiset when headings are compared without their # level; the only missing lines are dated headings renamed in place, each quoted by a History note; the only added lines are ## History, group headings, notes, renamed headings and, inside selected sections of the main text, strip_line images of History lines (whose verbatim source History holds). Outside History and code fences no line carries an epoch date and no non-heading line carries provenance, except protected H2 headings. History is the single last H2 section. A second run is the identity. All maps are BTreeMap/BTreeSet, so two runs on the same tree give identical reports.

Cost

One git ls-files, one read of every tracked JSON file and every groupant model.md. Per file a linear scan of L lines, O(L log L) for the History sort and the multiset verification, one strip_line pass over the History lines for the derivable set, and one repeated run for idempotence. strip_line is linear in the line length times the number of dates removed (at most 64). Rebinding scans the literals of every JSON file once per round; rounds stop at the fixpoint (at most 16).

Tests

undate::tests: date detection with paper years, versions, seeds, toolchain build dates, data snapshot dates and invalid calendar values as non-dates; provenance digests and run paths, and the bare variable name as text; undated names; strip_line frames (parenthetical, sentence-leading epoch, preposition, separator, colon, code span, bare digest, run path, template path kept, glued run key, dated heading, record line and note dropped, heading with provenance failing, fenced line untouched); the A* fixture; protected and unprotected dated H2 sections; merging into an existing History; list items and tables; record lines against wrapped prose; a core heading kept; a selected section keeping its rewritten substance while an unselected one moves; refill of heading-only selected sections from the newest group (fence and sub-heading carried, older group ignored, Undated group used, record-only group left as residue, History unchanged); fresh, chained and stale hash bindings. Negative controls that verify must reject: a dropped line, a changed word, an invented line, a date left in the main text, a digest left in the main text, a rename without its note, a section after History, the untransformed dated text, a rewritten or refilled line outside a selected section, an invented refill line, and a refill line that keeps its date.

Behavior complement

It does not delete lines, reorder lines inside a unit, edit fenced code, touch Markdown outside groupant model.md files, rename H2 sections that JSON selects, refresh stale hashes, edit the external groupant store, rewrite manifest section fields or statuses, or decide whether a dated statement is still true. Outside selected sections a paragraph that mixes a current statement with a date moves whole. A refill takes only the newest restatable group of the origin section; older groups and partially emptied sections stay as they are.

Reverse reconstruction

Each History unit names its origin section in its group heading, and a moved block keeps its heading text, so the moved lines map back to their sections; a renamed heading maps back through its note. A rewritten or refilled main-text line maps back to its verbatim History line through strip_line, which is many-to-one (a removed date, frame or digest is not recoverable from the main text alone). Positions inside a section, blank-line spacing and the original heading levels of moved blocks are not recoverable from the output alone; Git history holds the exact former text.

Line preservation

verify(old, new, protected, selected) is the executable reverse check of the invariant above, run on every changed file before any write; the unit tests above are its negative controls.

Limits

Detection is lexical. A date written in another format, a digest shorter than 40 hex digits and not abbreviated with …, or a run path outside the data directory variable stays in the main text. strip_line removes frames by fixed patterns: a sentence may lose a parenthetical next to a leading date or read awkwardly after a removal; History holds the original. A section's lead is chosen by position, not meaning. Hash rebinding covers path/sha256 pairs in one JSON object only.

This page in Markdown → https://md.groupants.elamur.ai/free/en/mova/tools/modelcheck/src/undate.rs.groupant/