docs(formal): generate PROFILES.md from the replay descriptors and shrink BEHAVIOR.md

formal/README.md

@@ -34,7 +34,7 @@ and generated artifacts; a reader should not need to open them to learn a rule.
 | [replay/](./replay/) | The shared replay coordinator, profile descriptors and witness classifiers every port executes | [replay/README.md](./replay/README.md) |
 | [tools/](./tools/) | The Node scripts behind the `make` targets: checks, generators, measurements and runners | [tools/README.md](./tools/README.md) |
 | [catalogs/](./catalogs/) | Hand-maintained manifests, evidence catalogs, ledgers, baselines and the fixed vector corpora | [catalogs/README.md](./catalogs/README.md) |
-| [generated/](./generated/) | Smoke traces, the fixtures lock and generated vectors; regenerated, never edited | [generated/README.md](./generated/README.md) |
+| [generated/](./generated/) | Smoke traces, the fixtures lock, generated vectors and the generated read views such as [PROFILES.md](./generated/PROFILES.md); regenerated, never edited | [generated/README.md](./generated/README.md) |
 
 ## How the specification connects to code
 

formal/catalogs/source-audit.json

@@ -1084,7 +1084,7 @@
   "reviewedGuides": [
     {
       "path": "formal/README.md",
-      "sha256": "cb6204391896e6c69ac5ab5e6195bc1c5f07261358220bb156433b9f5599b14a",
+      "sha256": "8042f90203465f6836322afa565479e36dcfdc6628a9a1d4140eea38093cd6f8",
       "entries": [
         {"title":"Executable DialCache specification"},
         {"title":"Start with your task"},
@@ -1102,7 +1102,7 @@
     },
     {
       "path": "formal/guides/AUTHORING.md",
-      "sha256": "728051bdcc8e1a7df19052aaa259ccdf8d7375647255325e514beafb9e22933b",
+      "sha256": "a8927a0580df5e67d795407d78040aa2a364e54cc20530c3d3db59507ce67d6f",
       "entries": [
         {"title":"Reading and extending the DialCache models"},
         {"title":"Reading a model"},
@@ -1124,22 +1124,22 @@
     },
     {
       "path": "formal/guides/BEHAVIOR.md",
-      "sha256": "6c835d7e3aecafce708b9ec7bf4b54d7c2d5daa4fa9c9a02ea71bbd5446b34a6",
+      "sha256": "7adc2ad8756d8df060b09c6d6c83c6d084e612c7b21afe2107029cb3c2ea2e99",
       "entries": [
-        {"title":"Portable behavioral scenarios and generated feature profiles"},
+        {"title":"Portable behavioral scenarios and generated profiles"},
         {"title":"Scenario format"},
         {"title":"Optional observed events"},
         {"title":"Fixture"},
         {"title":"Inputs and completion boundaries"},
-        {"title":"Additional composition profiles"},
         {"title":"Observations"},
         {"title":"Additional fixed-scenario inputs"},
-        {"title":"Generated pending-effect profile"},
-        {"title":"Generated feature profiles"},
-        {"title":"Generated independent-caller profile"},
-        {"title":"Generated layer-composition profile"},
-        {"title":"Generated request-scope profile"},
-        {"title":"Generated served-hit shadow admission profile"},
+        {"title":"Generated profiles"},
+        {"title":"Trace contract"},
+        {"title":"Value codes"},
+        {"title":"Observation channels"},
+        {"title":"Rules the profiles hold their drivers to"},
+        {"title":"Replaying generated traces"},
+        {"title":"Additional composition profiles"},
         {"title":"Port workflow and limits"}
       ],
       "review": {
@@ -1534,12 +1534,13 @@
     },
     {
       "path": "formal/guides/README.md",
-      "sha256": "2fb4e87fab1388f3c4bdce6ea41d865db52bb7edcade425630038013dca65b6a",
+      "sha256": "14d3ff0c562d1d2679d1127c050d266fda452cd27ce93d891adde8967b327137",
       "entries": [
         {"title":"Guides"},
         {"title":"Contract guides: what a port must preserve"},
         {"title":"Tooling guides: how to do the work"},
         {"title":"Coverage guides: what the evidence establishes"},
+        {"title":"Generated views: read, never edit"},
         {"title":"Historical evidence: what was measured, and when"}
       ],
       "review": {

formal/guides/AUTHORING.md

@@ -403,6 +403,14 @@ Formatting and deduplication improve reviewability; they do not increase the
 number of behavioral cases or justify a broader conformance claim. Changes to
 behavior, bounds, or claims should be reviewed separately from cleanup.
 
+The read views under `formal/generated/` ([PROFILES.md](../generated/PROFILES.md))
+are rendered from the replay descriptors and the catalogs; after a descriptor,
+`profiles.json`, `execution.json`, `coverage-witnesses.json` or a model's public runs
+(its replayed regressions) change, run
+`node formal/tools/generate-catalog-docs.mjs --write` and commit the result.
+`make audit` runs the `--check` form and fails on a stale view. Edit the
+descriptor or the catalog, never the view.
+
 ### Challenging every model
 
 `execution.json` also carries the model-property challenge catalog in its