Repository navigation
docs(formal): generate PROFILES.md from the replay descriptors and shrink BEHAVIOR.md - #233
Merged
Merged
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #233 +/- ##
==========================================
- Coverage 93.73% 93.73% -0.01%
==========================================
Files 78 78
Lines 11357 11357
Branches 656 656
==========================================
- Hits 10646 10645 -1
- Misses 641 642 +1
Partials 70 70
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
This was referenced Oct 15, 2026
lan17
added a commit
that referenced
this pull request
Oct 15, 2026
Phase 3 of #220, item B1. One commit, base `main`. Independent of #233. ## What `node formal/tools/check-style.mjs --report` prints the readability measurements #220 tracks, computed from the sources so progress is reproducible: | Measure | Value today | | --- | --- | | Quint files under formal/models | 82 | | Lines over 120 characters (models / kernel / fixtures) | 658 (171 / 180 / 307) | | Module header comment lines, total / longest / over 25 | 805 / 32 / 2 | | Quint comment sentences, count / over 40 / over 60 / over 100 words / longest / average | 1793 / 210 / 88 / 32 / 277 / 24.6 | | Guide sentences, count / over 40 / over 60 / over 100 words / longest / average | 2226 / 93 / 23 / 5 / 161 / 17.4 | | Definitions, count / six or more parameters (models / kernel / fixtures) | 854 / 45 (0 / 45 / 0) | | Definitions taking two or more boolean parameters | 7 (cache-rules.qnt:sourceMayWarmLocal, fixtures/kernel/markers.qnt:initial, fixtures/kernel/markers.qnt:initialize, kernel/remote-io.qnt:startLoader, kernel/serving.qnt:authority, kernel/serving.qnt:judgeReleaseUnder, kernel/shadow.qnt:newJob) | | Free-text exclusion reasons in execution.json | 531 | Those are reported, not enforced; the editorial guidance for them stays in AUTHORING "Writing conventions". Without arguments the tool enforces the two rules guidance alone did not hold (AUTHORING already asked for lines without horizontal scrolling, and the Quint sources broke that 658 times): a Quint line is at most 120 characters and a module header is at most 25 comment lines. The header is the `//` comment block beside the `module` line, before it or after it, up to the first import or definition, so the kernel fixtures' headers written above `module` count too. Enforcement covers every `.qnt` under `formal/models` not named for that rule in `formal/catalogs/style-allowlist.json`. The allowlist names the 60 files that break the line cap today and the two fixtures (`held-remote.qnt`, `payload-classes.qnt`) whose headers exceed 25 lines; it carries no counts and may only shrink: an entry whose file has become clean fails the check, so cleaning a file means deleting its line, and adding one is a reviewed exception. The check runs in `make audit`. ## Why now #231 brought every kernel header under the cap; without an enforced rule that regresses the first time someone pastes a paragraph. The line cap starts as a ratchet over 22 clean files and tightens as files are wrapped (Quint 0.32.0 has no formatter, so wrapping stays manual and is separate work). Review follow-up (second commit): the header is counted on both sides of the `module` line, banner lines no longer inflate the sentence metric, boolean parameters are counted anywhere in a signature with actions included, and the report carries the over 60 and over 100 columns #220 tracked. ## Tests `formal-style.test.ts`: on a fake tree, an unlisted long line fails naming `path:line`, an unlisted tall header fails whether written before or after `module`, a stale entry for either rule and a file outside the scope fail, a file listed for one rule and offending the other reports both, header counting stops at the first import or definition, definitions are scanned to the matching parenthesis, and the report renders every row; on the committed tree the check passes, exactly two headers exceed the cap (both allowlisted), and the audit plan contains the step. ## Verification `make audit` green with the new step; `vitest run test/formal-style test/formal-validation` pass; `tsc --noEmit` clean; `node scripts/check-docs.mjs` green. AUTHORING re-keyed with `--refresh`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
…k BEHAVIOR.md Six sections of BEHAVIOR.md (6,600 of its 9,600 words) restated the replay descriptors in formal/replay/features.mjs, effects.mjs, local-clock.mjs and profiles/*.mjs: each profile's fixture, setup, actions and the driver commands their choices decode into. Those facts are now rendered from the descriptors and the catalogs into formal/generated/PROFILES.md by formal/tools/generate-catalog-docs.mjs. Per profile: model, version and input encoding, smoke trace, the ports claiming it, the generation bounds and counts from execution.json, the required witness count, the fixture (per init choice where it varies), the setup commands, every action with its choice range and the decoded driver commands (long ranges show the first six and last two), and the observation channels the coordinator compares. A decoder that reads the observation or the environment is evaluated against probes and the page says which keys it reads. The view lives under formal/generated/ rather than guides/ because generated text is not reviewed by hand: the source audit scans every guide, and a view that changes with its sources would need a ledger re-key on every regeneration, which is the ripple #220 removes. `--check` runs in the audit lane; `--write` is documented in AUTHORING. BEHAVIOR.md keeps what the tables cannot state, condensed into one "Generated profiles" section: the trace contract, the value codes (effects.mjs cites them), the meaning of each observation channel, the rules each profile holds its drivers to, and how to replay a generated trace. It goes from 9,597 words to 4,920; the composition-profile summary now follows it and links the view. Tests: formal-catalog-docs.test.ts pins the committed view to the renderer, determinism, coverage of every profile and action, the probe decoding and the declared channels. Ledger: BEHAVIOR, AUTHORING, the two indexes re-keyed; parity inputs re-pinned.
…condensation lost Review follow-up on the generated profile view and the shrunk BEHAVIOR.md. The view renders each profile's setup commands from the same function the coordinator uses: bindings.mjs now exports fixtureFor and setupFor, so the effects profile's init-dependent initial policy (empty, a 30 ms read budget or a null reply) appears per init choice instead of nowhere. The effects channel lists the fields the parser compares, writeTtls included. A decoder that reads the observation or the environment is annotated per choice and per probe kind (a count shown with one so far; the wall clock shown as 0) instead of one note claiming every choice assumes one. Only a counter walking up (consecutive decodings differing in one numeric field) is abbreviated; a payload class or an overlay per choice is shown in full, so the 26 policy overlays and the recovery-read frame seeds are readable again. The scope profile's diagnostics say no age event is selected rather than naming a `none` event. The observation probe has the shared record's shape and rejects an unknown field; a decoder failure names its profile and action; the view header names the Quint models among its inputs, since a model's public runs are its replayed regressions. BEHAVIOR.md restores every normative statement the condensation dropped: the effects setup and bounds, the observer-fault isolation, the ms-to-s conversion and the one-byte scalar, the policy overlay consequences (choices 10 to 25), the scope trail rules and the AsyncLocalStorage disclaimer, the nested-context ownership rule, the admission readmission, 600 ms bound, 32-effect bound and smoke description, the independent bounds and settlement boundary, the layers two-slot rationale and operation variants, the shadow C1 identity, reencode, advanceWall and timer rules, the JSON warning obligation, the failing-replay diagnostics, and what each profile leaves to others. It also corrects two channel attributions: effects asserts s.o, s.io and s.events only, and shadow-read-deadlines carries s.io. Five model comments that cited the removed headings now point at the view and the new section; the fixtures lock follows. AUTHORING and the generated README name the models and both regeneration commands.
lan17
force-pushed
the
claude/formal-profiles-doc
branch
from
October 15, 2026 02:00
807d90f to
5df88f1
Compare
lan17
added a commit
that referenced
this pull request
Oct 15, 2026
…ere.mjs (#235) Phase 3 of #220, item D1, reshaped after review. One commit, stacked on #233 until it lands, then retargeted to `main`. ## What changed since the first version The first version mirrored the challenge and mutant catalogs into 8,190 lines of Markdown. That earned its lines badly: a 345 KB mirror is no easier to read than the JSON it copies, it costs a regeneration on every catalog edit, and it is worse for an agent, which parses JSON fine. What a reader needs is a skimmable list and one entry at a time. ## What this does now - **`formal/generated/CHALLENGES.md`** (91 lines) and **`MUTANTS.md`** (76 lines): one row per challenge (contract, source, invariant, native mutant, reproducer run, detected and excluded counts) and per mutant (case, description, detections per port, challenges mapped to it). Generated by the same `--write`, checked by the same `--check` in the audit lane. - **`where.mjs` reads an entry in full on demand:** `node formal/tools/where.mjs recovery-inclusive-maximum` prints the edit, the invariant, the mapping with its cross-contract note and evidence checkpoint, the reproducer and every exclusion with its reason; `node formal/tools/where.mjs M01` prints the rationale, the edits per port including the Rust mirror, the required detections and the challenges mapped to it. Net: +167 generated lines instead of +8,190, no new reading surface, and the lookup the mirror was really for. ## Tests `formal-catalog-docs.test.ts` pins all three views to the renderers and checks that every challenge and every mutant has one row and that the indexes stay within a few lines of the entry count. `formal-where.test.ts` covers the challenge and mutant lookups and their error paths. ## Verification `make audit` green; `vitest run test/formal-catalog-docs test/formal-where` pass; `tsc --noEmit` clean; `node scripts/check-docs.mjs` green (32 pages). Indexes and AUTHORING re-keyed with `--refresh`; parity inputs re-pinned. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Phase 3 of #220, item A4. One commit, base
main.What
Six sections of
BEHAVIOR.md(6,600 of its 9,600 words) restated the replay descriptors informal/replay/features.mjs,effects.mjs,local-clock.mjsandprofiles/*.mjs: each profile's fixture, setup, actions and the driver commands their choices decode into. Those facts are now generated intoformal/generated/PROFILES.mdbynode formal/tools/generate-catalog-docs.mjs --write, andmake auditfails when the view is stale (--check).Per profile the view gives: model, version and input encoding, smoke trace, the ports claiming it, the generation bounds and counts from
execution.json, the required witness count, the fixture (per init choice where it varies), the setup commands, every action with its choice range and the decoded driver commands, and the observation channels the coordinator compares. A decoder that reads the observation or the environment (the "release the latest effect" actions, the wall-clock-stamped seeds) is evaluated against probes and the page says which keys it reads. Only a counter walking up (consecutive decodings differing in one numeric field) is abbreviated; a payload class or an overlay per choice is shown in full. The fixture and the setup come frombindings.mjs, the same functions the coordinator uses, so the view cannot drift from what the drivers receive. 17 profiles, 169 actions, 773 lines.BEHAVIOR.mdkeeps what tables cannot state, condensed into one "Generated profiles" section: the trace contract, the value codes (whicheffects.mjscites), the meaning of each observation channel (io,d,events,markers,compression,policyErrors), the rules each profile holds its drivers to, and how to replay a generated trace. The composition-profile summary now follows it and links the view.BEHAVIOR.mdwordsTwo decisions to flag
guides/PROFILES.md. The view lives underformal/generated/instead, because generated text is not reviewed by hand: the source audit scans every guide, and a view that changes with its sources would need a ledger re-key on every regeneration, which is exactly the ripple Formal: readability and change-cost plan for the Quint tree (glossary, kernel docs, naming, catalog prose, ledger churn) #220 removes.generated/README.md, the guides index and the formal README's directory table point at it.BEHAVIOR.md. The result is 5,563: the six sections carried about 2,500 words of normative rules that are stated nowhere else in prose (the effects reply classes and bounds, the diagnostics attribution rules, the scope closure rules, the admission ownership rules, the policy overlay consequences, the shadow payload andsourceWorkMsrules, what each profile leaves to others). I kept them, condensed into one bulleted section, rather than drop contract content to hit a number. An independent review of the first commit found rules the condensation had dropped and two wrong channel attributions; the second commit restores every one and fixes both.Verification
make auditgreen with the new "Check the generated read views" step.vitest run test/formal-catalog-docs test/formal-validation test/formal-exploration test/formal-source-audit test/formal-go-parity: all pass (the Rust prerequisite probe test fails locally only because Docker is not running here; it does not touch this change).tsc --noEmitclean;node scripts/check-docs.mjsgreen (30 pages, every link in the generated view resolves).BEHAVIOR.md,AUTHORING.md,guides/README.mdandformal/README.mdre-keyed with--refresh; parity inputs re-pinned.🤖 Generated with Claude Code