diff --git a/formal/README.md b/formal/README.md
index 7627bced..3022fb58 100644
--- a/formal/README.md
+++ b/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
diff --git a/formal/catalogs/source-audit.json b/formal/catalogs/source-audit.json
index 1b2ac7ee..ba9d3f7c 100644
--- a/formal/catalogs/source-audit.json
+++ b/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": {
diff --git a/formal/generated/PROFILES.md b/formal/generated/PROFILES.md
new file mode 100644
index 00000000..283dafed
--- /dev/null
+++ b/formal/generated/PROFILES.md
@@ -0,0 +1,773 @@
+# Conformance profiles
+
+Generated by `node formal/tools/generate-catalog-docs.mjs --write` from
+[profiles.json](../catalogs/profiles.json), [execution.json](../catalogs/execution.json),
+[coverage-witnesses.json](../catalogs/coverage-witnesses.json), the replay descriptors under
+[../replay/](../replay/README.md) (the fixture and setup through `bindings.mjs`, the shared record
+through `observation.mjs`) and the public runs of each Quint model, which are its replayed
+regressions. Do not edit; `make audit` fails when this page is stale.
+
+One section per profile: what the drivers are configured with, which commands each recorded
+action decodes into, and which observation channels the coordinator compares. A choice is the
+integer the Quint action records in `input.choice`; the driver command is what the coordinator
+sends for it. [BEHAVIOR.md](../guides/BEHAVIOR.md) explains the scenario format, the fixture
+fields and the observation record; [PORTING.md](../guides/PORTING.md) explains what a driver does with them.
+
+| Profile | Model | Actions | Sampled histories | Replayed regressions | Required witnesses |
+| --- | --- | --- | --- | --- | --- |
+| [core](#core) | [dialcache-conformance.qnt](../models/dialcache-conformance.qnt) | 8 | 32 | 5 | 0 |
+| [effects](#effects) | [dialcache-effects-conformance.qnt](../models/dialcache-effects-conformance.qnt) | 21 | 512 | 51 | 95 |
+| [scope](#scope) | [dialcache-scope-conformance.qnt](../models/dialcache-scope-conformance.qnt) | 7 | 256 | 14 | 26 |
+| [recovery](#recovery) | [dialcache-recovery-conformance.qnt](../models/dialcache-recovery-conformance.qnt) | 14 | 512 | 31 | 47 |
+| [policy](#policy) | [dialcache-policy-conformance.qnt](../models/dialcache-policy-conformance.qnt) | 12 | 512 | 33 | 51 |
+| [shadow](#shadow) | [dialcache-shadow-conformance.qnt](../models/dialcache-shadow-conformance.qnt) | 20 | 1024 | 40 | 77 |
+| [admission](#admission) | [dialcache-admission-conformance.qnt](../models/dialcache-admission-conformance.qnt) | 8 | 128 | 9 | 19 |
+| [layers](#layers) | [dialcache-layers-conformance.qnt](../models/dialcache-layers-conformance.qnt) | 8 | 512 | 17 | 27 |
+| [independent](#independent) | [dialcache-independent-conformance.qnt](../models/dialcache-independent-conformance.qnt) | 11 | 512 | 15 | 18 |
+| [recovery-read](#recovery-read) | [dialcache-recovery-read-conformance.qnt](../models/dialcache-recovery-read-conformance.qnt) | 12 | 256 | 34 | 26 |
+| [local-failure](#local-failure) | [dialcache-local-failure-conformance.qnt](../models/dialcache-local-failure-conformance.qnt) | 6 | 128 | 5 | 4 |
+| [runtime-boundaries](#runtime-boundaries) | [dialcache-runtime-boundaries-conformance.qnt](../models/dialcache-runtime-boundaries-conformance.qnt) | 5 | 256 | 29 | 22 |
+| [shadow-layers](#shadow-layers) | [dialcache-shadow-layers-conformance.qnt](../models/dialcache-shadow-layers-conformance.qnt) | 9 | 256 | 26 | 22 |
+| [local-clock](#local-clock) | [dialcache-local-clock-conformance.qnt](../models/dialcache-local-clock-conformance.qnt) | 3 | 128 | 4 | 2 |
+| [source-budgets](#source-budgets) | [dialcache-source-budgets-conformance.qnt](../models/dialcache-source-budgets-conformance.qnt) | 5 | 256 | 10 | 7 |
+| [dark-layers](#dark-layers) | [dialcache-dark-layers-conformance.qnt](../models/dialcache-dark-layers-conformance.qnt) | 18 | 256 | 29 | 48 |
+| [shadow-read-deadlines](#shadow-read-deadlines) | [dialcache-shadow-read-deadlines-conformance.qnt](../models/dialcache-shadow-read-deadlines-conformance.qnt) | 10 | 128 | 6 | 6 |
+
+## core
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-conformance.qnt](../models/dialcache-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [conformance-smoke.itf.json](./conformance-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 32 sampled histories of at most 30 steps from 256 samples; 4 scheduled invariants; 5 exported regressions |
+| Required witnesses | 0 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+The coordinator sends an empty fixture; see [core.mjs](../replay/core.mjs) for what the driver constructs.
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `bumpSource` | none | `[{"op":"advanceWall","ms":1},{"op":"bumpSource"}]` |
+| `outsideCall` | none | `[{"op":"advanceWall","ms":1},{"op":"call","identity":{"keyType":"user_id","id":"123","useCase":"ConformanceOutside","tracked":false},"policy":{"ttlSec":{"local":60},"ramp":{"local":100}},"mode":"outside","counter":"outsideLoaderCalls","readFailure":false}]` |
+| `requestLocalPair` | none | `[{"op":"advanceWall","ms":1},{"op":"call","identity":{"keyType":"user_id","id":"123","useCase":"ConformanceRequest","tracked":false},"policy":{"requestLocal":true},"mode":"request-pair","counter":"requestLoaderCalls","readFailure":false}]` |
+| `localCall` | none | `[{"op":"advanceWall","ms":1},{"op":"call","identity":{"keyType":"user_id","id":"123","useCase":"ConformanceLocal","tracked":false},"policy":{"ttlSec":{"local":60},"ramp":{"local":100}},"mode":"single","counter":"localLoaderCalls","readFailure":false}]` |
+| `coalescedLocalPair` | none | `[{"op":"advanceWall","ms":1},{"op":"call","identity":{"keyType":"user_id","id":"123","useCase":"ConformanceCoalesced","tracked":false},"policy":{"ttlSec":{"local":60},"ramp":{"local":100}},"mode":"coalesced-pair","counter":"coalescedLoaderCalls","readFailure":false}]` |
+| `remoteCall` | none | `[{"op":"advanceWall","ms":1},{"op":"call","identity":{"keyType":"user_id","id":"123","useCase":"ConformanceRemote","tracked":true},"policy":{"ttlSec":{"remote":60},"ramp":{"remote":100}},"mode":"single","counter":"remoteLoaderCalls","readFailure":false}]` |
+| `invalidateRemote` | none | `[{"op":"advanceWall","ms":1},{"op":"invalidate","identity":{"keyType":"user_id","id":"123","useCase":"ConformanceRemote","tracked":true}}]` |
+| `remoteReadFailureCall` | none | `[{"op":"advanceWall","ms":1},{"op":"call","identity":{"keyType":"user_id","id":"123","useCase":"ConformanceRemote","tracked":true},"policy":{"ttlSec":{"remote":60},"ramp":{"remote":100}},"mode":"single","counter":"remoteLoaderCalls","readFailure":true}]` |
+
+### Observation channels
+
+- `o`: `sourceVersion`, `lastResult`, `outsideLoaderCalls`, `requestLoaderCalls`, `localLoaderCalls`, `coalescedLoaderCalls`, `remoteLoaderCalls`, `redisReads`, `redisWrites`; the model fields observable through the public API.
+
+## effects
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-effects-conformance.qnt](../models/dialcache-effects-conformance.qnt) |
+| Version | 3, inputs `explicit-v1` |
+| Smoke trace | [effects-smoke.itf.json](./effects-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 512 sampled histories of at most 60 steps from 4096 samples; 11 scheduled invariants; 51 exported regressions |
+| Required witnesses | 95 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture, by init choice
+
+| Init choice | Fixture |
+| --- | --- |
+| 0 | `{"policy":{"ttlSec":{"remote":60}},"tracked":true,"readTimeoutMs":"default","observe":["readContext","readAbort","request","disabled","miss","error","coalesced","invalidation","get","fallback","serialization","futureOffset","size","storedSize","writeDispatch"]}` |
+| 1 | `{"policy":{"ttlSec":{"remote":60}},"tracked":true,"readTimeoutMs":20,"observe":["readContext","readAbort","request","disabled","miss","error","coalesced","invalidation","get","fallback","serialization","futureOffset","size","storedSize","writeDispatch"]}` |
+| 2 | `{"policy":{"ttlSec":{"remote":60},"remoteReadTimeoutMs":10},"tracked":true,"readTimeoutMs":20,"observe":["readContext","readAbort","request","disabled","miss","error","coalesced","invalidation","get","fallback","serialization","futureOffset","size","storedSize","writeDispatch"]}` |
+| 3 | `{"policy":{"ttlSec":{"remote":60},"remoteReadTimeoutMs":10},"tracked":true,"readTimeoutMs":20,"observe":["readContext","readAbort","request","disabled","miss","error","coalesced","invalidation","get","fallback","serialization","futureOffset","size","storedSize","writeDispatch"]}` |
+| 4 | `{"policy":{"ttlSec":{"remote":60},"remoteReadTimeoutMs":10},"tracked":true,"readTimeoutMs":20,"observe":["readContext","readAbort","request","disabled","miss","error","coalesced","invalidation","get","fallback","serialization","futureOffset","size","storedSize","writeDispatch"]}` |
+| 5 | `{"policy":{"ttlSec":{"remote":60},"remoteReadTimeoutMs":10},"tracked":false,"readTimeoutMs":20,"observe":["readContext","readAbort","request","disabled","miss","error","coalesced","invalidation","get","fallback","serialization","futureOffset","size","storedSize","writeDispatch"]}` |
+
+### Setup commands, by init choice
+
+| Init choice | Setup |
+| --- | --- |
+| 0 | `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
`{"op":"policy","value":{}}` |
+| 1 | `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
`{"op":"policy","value":{}}` |
+| 2 | `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
`{"op":"policy","value":{}}` |
+| 3 | `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
`{"op":"policy","value":{"remoteReadTimeoutMs":30}}` |
+| 4 | `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
`{"op":"policy","value":null}` |
+| 5 | `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
`{"op":"policy","value":{}}` |
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | none | `[{"op":"begin"}]` |
+| `resolveLoader` | any read or loader index | 0 → `[{"op":"resolve","loader":0,"value":1}]` |
+| `rejectLoader` | any read or loader index | 0 → `[{"op":"reject","loader":0}]` |
+| `releaseRead` | any read or loader index | 0 → `[{"op":"faults","value":{"read":false}},{"op":"release","effect":"read","index":0},{"op":"faults","value":{"read":false}}]` |
+| `failRead` | any read or loader index | 0 → `[{"op":"faults","value":{"read":true}},{"op":"release","effect":"read","index":0},{"op":"faults","value":{"read":false}}]` |
+| `releaseLoad` | none | `[{"op":"faults","value":{"load":false}},{"op":"release","effect":"load","index":0},{"op":"faults","value":{"load":false}}]`
every decoding reads `observation.loads` (the count so far at the step; shown with one so far) |
+| `failLoad` | none | `[{"op":"faults","value":{"load":true}},{"op":"release","effect":"load","index":0},{"op":"faults","value":{"load":false}}]`
every decoding reads `observation.loads` (the count so far at the step; shown with one so far) |
+| `releaseDump` | none | `[{"op":"faults","value":{"dump":false}},{"op":"release","effect":"dump","index":0},{"op":"faults","value":{"dump":false}}]`
every decoding reads `observation.dumps` (the count so far at the step; shown with one so far) |
+| `failDump` | none | `[{"op":"faults","value":{"dump":true}},{"op":"release","effect":"dump","index":0},{"op":"faults","value":{"dump":false}}]`
every decoding reads `observation.dumps` (the count so far at the step; shown with one so far) |
+| `releaseWrite` | none | `[{"op":"faults","value":{"write":false}},{"op":"release","effect":"write","index":0},{"op":"faults","value":{"write":false}}]`
every decoding reads `observation.writes` (the count so far at the step; shown with one so far) |
+| `failWrite` | none | `[{"op":"faults","value":{"write":true}},{"op":"release","effect":"write","index":0},{"op":"faults","value":{"write":false}}]`
every decoding reads `observation.writes` (the count so far at the step; shown with one so far) |
+| `seedRemote` | none | `[{"op":"seed","value":1}]` |
+| `tick` | none | `[{"op":"advance","ms":10}]` |
+| `jumpClock` | none | `[{"op":"advance","ms":10,"deliverTimers":false}]` |
+| `rollbackWall` | none | `[{"op":"shiftWall","ms":-1000}]` |
+| `advanceWall` | 1, 59999, 60000 | 1 → `[{"op":"shiftWall","ms":1}]`
59999 → `[{"op":"shiftWall","ms":59999}]`
60000 → `[{"op":"shiftWall","ms":60000}]` |
+| `observerFault` | 0, 1 | 0 → `[{"op":"faults","value":{"observer":false}}]`
1 → `[{"op":"faults","value":{"observer":true}}]` |
+| `readBudgetPolicy` | 0..4 | 0 → `[{"op":"policy","value":{}}]`
1 → `[{"op":"policy","value":{"remoteReadTimeoutMs":10}}]`
2 → `[{"op":"policy","value":{"remoteReadTimeoutMs":20}}]`
3 → `[{"op":"policy","value":{"remoteReadTimeoutMs":30}}]`
4 → `[{"op":"policy","value":{"remoteReadTimeoutMs":50}}]` |
+| `adapterReply` | 1..16 | 1 → `[{"op":"adapterReply","value":null}]`
2 → `[{"op":"adapterReply","value":42}]`
3 → `[{"op":"adapterReply","value":{"kind":"watermark_miss","observedWatermarkMs":20}}]`
4 → `[{"op":"adapterReply","value":{"reason":"value_absent"}}]`
5 → `[{"op":"adapterReply","value":{"kind":"miss"}}]`
6 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"invented"}}]`
7 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"invented","observedWatermarkMs":20}}]`
8 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"watermark_fenced"}}]`
9 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"watermark_fenced","observedWatermarkMs":-1}}]`
10 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"value_absent","observedWatermarkMs":1.5}}]`
11 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"value_absent","observedWatermarkMs":9007199254740992}}]`
12 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"value_absent","observedWatermarkMs":20}}]`
13 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"expired","observedWatermarkMs":0}}]`
14 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"value_absent","payload":"1","createdAtMs":0}}]`
15 → `[{"op":"adapterReply","value":{"reason":"watermark_fenced","observedWatermarkMs":20,"payload":"1","createdAtMs":0}}]`
16 → `[{"op":"adapterReply","value":{"kind":"miss","reason":"watermark_fenced","observedWatermarkMs":20}}]`
every decoding reads `environment.wallMs` (the environment value at the step; shown as 0) |
+| `invalidate` | none | `[{"op":"invalidate"}]` |
+| `futureFence` | none | `[{"op":"invalidate","futureBufferMs":20}]` |
+
+### Observation channels
+
+- `o`: `loaders`, `reads`, `writes`, `invalidations`, `loads`, `dumps`, `policyCalls`, `calls`, `writeTtls`, `events`, `readContexts`, `readAborts`; the effects record the parser compares: counters, caller codes, physical write TTLs, the ordered event trail, read contexts and aborts.
+
+## scope
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-scope-conformance.qnt](../models/dialcache-scope-conformance.qnt) |
+| Version | 2, inputs `explicit-v1` |
+| Smoke trace | [scope-smoke.itf.json](./scope-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 256 sampled histories of at most 60 steps from 1024 samples; 6 scheduled invariants; 14 exported regressions |
+| Required witnesses | 26 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+`{"policy":{"requestLocal":true},"remote":false,"fallbackTimeoutMs":null,"probeSourceScope":true,"observe":["coalesced","error"]}`
+
+### Setup commands
+
+- `{"op":"openScope","id":"0"}`
+- `{"op":"faults","value":{"holdPolicies":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `openScope` | 1..4 | 1 → `{"op":"openScope","id":"1"}`
2 → `{"op":"openScope","id":"2","parent":"0"}`
3 → `{"op":"openScope","id":"3","parent":"0","disabled":true}`
4 → `{"op":"openScope","id":"4","parent":"3"}` |
+| `closeScope` | 0..4 | 0 → `{"op":"closeScope","id":"0"}`
1 → `{"op":"closeScope","id":"1"}`
2 → `{"op":"closeScope","id":"2"}`
3 → `{"op":"closeScope","id":"3"}`
4 → `{"op":"closeScope","id":"4"}` |
+| `beginCall` | 0..5 | 0 → `{"op":"begin","scope":"0"}`
1 → `{"op":"begin","scope":"1"}`
2 → `{"op":"begin","scope":"2"}`
3 → `{"op":"begin","scope":"3"}`
4 → `{"op":"begin","scope":"4"}`
5 → `{"op":"begin","outside":true}` |
+| `releasePolicy` | none | `{"op":"release","effect":"policy","index":0}`
every decoding reads `observation.policyCalls` (the count so far at the step; shown with one so far) |
+| `resolveLoader` | 1..112 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":0}`
4 → `{"op":"resolve","loader":0,"value":null}`
5 → `{"op":"resolve","loader":0,"value":false}`
6 → `{"op":"resolve","loader":0,"value":0}`
7 → `{"op":"resolve","loader":0,"value":""}`
8 → `{"op":"resolve","loader":1,"value":1}`
9 → `{"op":"resolve","loader":1,"value":2}`
10 → `{"op":"resolve","loader":1}`
11 → `{"op":"resolve","loader":1,"value":null}`
12 → `{"op":"resolve","loader":1,"value":false}`
13 → `{"op":"resolve","loader":1,"value":0}`
14 → `{"op":"resolve","loader":1,"value":""}`
15 → `{"op":"resolve","loader":2,"value":1}`
16 → `{"op":"resolve","loader":2,"value":2}`
17 → `{"op":"resolve","loader":2}`
18 → `{"op":"resolve","loader":2,"value":null}`
19 → `{"op":"resolve","loader":2,"value":false}`
20 → `{"op":"resolve","loader":2,"value":0}`
21 → `{"op":"resolve","loader":2,"value":""}`
22 → `{"op":"resolve","loader":3,"value":1}`
23 → `{"op":"resolve","loader":3,"value":2}`
24 → `{"op":"resolve","loader":3}`
25 → `{"op":"resolve","loader":3,"value":null}`
26 → `{"op":"resolve","loader":3,"value":false}`
27 → `{"op":"resolve","loader":3,"value":0}`
28 → `{"op":"resolve","loader":3,"value":""}`
29 → `{"op":"resolve","loader":4,"value":1}`
30 → `{"op":"resolve","loader":4,"value":2}`
31 → `{"op":"resolve","loader":4}`
32 → `{"op":"resolve","loader":4,"value":null}`
33 → `{"op":"resolve","loader":4,"value":false}`
34 → `{"op":"resolve","loader":4,"value":0}`
35 → `{"op":"resolve","loader":4,"value":""}`
36 → `{"op":"resolve","loader":5,"value":1}`
37 → `{"op":"resolve","loader":5,"value":2}`
38 → `{"op":"resolve","loader":5}`
39 → `{"op":"resolve","loader":5,"value":null}`
40 → `{"op":"resolve","loader":5,"value":false}`
41 → `{"op":"resolve","loader":5,"value":0}`
42 → `{"op":"resolve","loader":5,"value":""}`
43 → `{"op":"resolve","loader":6,"value":1}`
44 → `{"op":"resolve","loader":6,"value":2}`
45 → `{"op":"resolve","loader":6}`
46 → `{"op":"resolve","loader":6,"value":null}`
47 → `{"op":"resolve","loader":6,"value":false}`
48 → `{"op":"resolve","loader":6,"value":0}`
49 → `{"op":"resolve","loader":6,"value":""}`
50 → `{"op":"resolve","loader":7,"value":1}`
51 → `{"op":"resolve","loader":7,"value":2}`
52 → `{"op":"resolve","loader":7}`
53 → `{"op":"resolve","loader":7,"value":null}`
54 → `{"op":"resolve","loader":7,"value":false}`
55 → `{"op":"resolve","loader":7,"value":0}`
56 → `{"op":"resolve","loader":7,"value":""}`
57 → `{"op":"resolve","loader":8,"value":1}`
58 → `{"op":"resolve","loader":8,"value":2}`
59 → `{"op":"resolve","loader":8}`
60 → `{"op":"resolve","loader":8,"value":null}`
61 → `{"op":"resolve","loader":8,"value":false}`
62 → `{"op":"resolve","loader":8,"value":0}`
63 → `{"op":"resolve","loader":8,"value":""}`
64 → `{"op":"resolve","loader":9,"value":1}`
65 → `{"op":"resolve","loader":9,"value":2}`
66 → `{"op":"resolve","loader":9}`
67 → `{"op":"resolve","loader":9,"value":null}`
68 → `{"op":"resolve","loader":9,"value":false}`
69 → `{"op":"resolve","loader":9,"value":0}`
70 → `{"op":"resolve","loader":9,"value":""}`
71 → `{"op":"resolve","loader":10,"value":1}`
72 → `{"op":"resolve","loader":10,"value":2}`
73 → `{"op":"resolve","loader":10}`
74 → `{"op":"resolve","loader":10,"value":null}`
75 → `{"op":"resolve","loader":10,"value":false}`
76 → `{"op":"resolve","loader":10,"value":0}`
77 → `{"op":"resolve","loader":10,"value":""}`
78 → `{"op":"resolve","loader":11,"value":1}`
79 → `{"op":"resolve","loader":11,"value":2}`
80 → `{"op":"resolve","loader":11}`
81 → `{"op":"resolve","loader":11,"value":null}`
82 → `{"op":"resolve","loader":11,"value":false}`
83 → `{"op":"resolve","loader":11,"value":0}`
84 → `{"op":"resolve","loader":11,"value":""}`
85 → `{"op":"resolve","loader":12,"value":1}`
86 → `{"op":"resolve","loader":12,"value":2}`
87 → `{"op":"resolve","loader":12}`
88 → `{"op":"resolve","loader":12,"value":null}`
89 → `{"op":"resolve","loader":12,"value":false}`
90 → `{"op":"resolve","loader":12,"value":0}`
91 → `{"op":"resolve","loader":12,"value":""}`
92 → `{"op":"resolve","loader":13,"value":1}`
93 → `{"op":"resolve","loader":13,"value":2}`
94 → `{"op":"resolve","loader":13}`
95 → `{"op":"resolve","loader":13,"value":null}`
96 → `{"op":"resolve","loader":13,"value":false}`
97 → `{"op":"resolve","loader":13,"value":0}`
98 → `{"op":"resolve","loader":13,"value":""}`
99 → `{"op":"resolve","loader":14,"value":1}`
100 → `{"op":"resolve","loader":14,"value":2}`
101 → `{"op":"resolve","loader":14}`
102 → `{"op":"resolve","loader":14,"value":null}`
103 → `{"op":"resolve","loader":14,"value":false}`
104 → `{"op":"resolve","loader":14,"value":0}`
105 → `{"op":"resolve","loader":14,"value":""}`
106 → `{"op":"resolve","loader":15,"value":1}`
107 → `{"op":"resolve","loader":15,"value":2}`
108 → `{"op":"resolve","loader":15}`
109 → `{"op":"resolve","loader":15,"value":null}`
110 → `{"op":"resolve","loader":15,"value":false}`
111 → `{"op":"resolve","loader":15,"value":0}`
112 → `{"op":"resolve","loader":15,"value":""}` |
+| `rejectLoader` | 0..15 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
… one more per choice …
14 → `{"op":"reject","loader":14}`
15 → `{"op":"reject","loader":15}` |
+| `policy` | 0..2 | 0 → `{"op":"policy","value":{}}`
1 → `{"op":"policy","value":{"requestLocal":false}}`
2 → `{"op":"policy","value":{"coalesce":false}}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+- `d`: `ages`, `coalesced`, `fallbackErrors`, `warnings`; diagnostics; no age events are selected.
+
+## recovery
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-recovery-conformance.qnt](../models/dialcache-recovery-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [recovery-smoke.itf.json](./recovery-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 512 sampled histories of at most 60 steps from 4096 samples; 10 scheduled invariants; 31 exported regressions |
+| Required witnesses | 47 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture, by init choice
+
+| Init choice | Fixture |
+| --- | --- |
+| 0 | `{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"requestLocal":false},"tracked":true,"fallbackTimeoutMs":10,"recovery":"default","observe":["recoveryAge","coalesced","error"]}` |
+| 1 | `{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"requestLocal":false},"tracked":true,"fallbackTimeoutMs":10,"recovery":"allow","observe":["recoveryAge","coalesced","error"]}` |
+| 2 | `{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"requestLocal":false},"tracked":true,"fallbackTimeoutMs":10,"recovery":"deny","observe":["recoveryAge","coalesced","error"]}` |
+| 3 | `{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"requestLocal":false},"tracked":true,"fallbackTimeoutMs":10,"recovery":"error","observe":["recoveryAge","coalesced","error"]}` |
+| 4 | `{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"requestLocal":true},"tracked":true,"fallbackTimeoutMs":10,"recovery":"default","observe":["recoveryAge","coalesced","error"]}` |
+| 5 | `{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"requestLocal":true},"tracked":true,"fallbackTimeoutMs":10,"recovery":"allow","observe":["recoveryAge","coalesced","error"]}` |
+| 6 | `{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"requestLocal":true},"tracked":true,"fallbackTimeoutMs":10,"recovery":"deny","observe":["recoveryAge","coalesced","error"]}` |
+| 7 | `{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"requestLocal":true},"tracked":true,"fallbackTimeoutMs":10,"recovery":"error","observe":["recoveryAge","coalesced","error"]}` |
+
+### Setup commands
+
+- `{"op":"openScope","id":"0"}`
+- `{"op":"openScope","id":"1"}`
+- `{"op":"seed","value":1,"ageMs":1000}`
+- `{"op":"faults","value":{"holdLoads":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0..7 | 0 → `{"op":"begin","scope":"0","recovery":"allow"}`
1 → `{"op":"begin","scope":"0","recovery":"deny"}`
2 → `{"op":"begin","scope":"0","recovery":"error"}`
3 → `{"op":"begin","scope":"0"}`
4 → `{"op":"begin","scope":"1","recovery":"allow"}`
5 → `{"op":"begin","scope":"1","recovery":"deny"}`
6 → `{"op":"begin","scope":"1","recovery":"error"}`
7 → `{"op":"begin","scope":"1"}` |
+| `joinCall` | 0, 1 | 0 → `{"op":"begin","scope":"0"}`
1 → `{"op":"begin","scope":"1"}` |
+| `closeScope` | 0, 1 | 0 → `{"op":"closeScope","id":"0"}`
1 → `{"op":"closeScope","id":"1"}` |
+| `resolveLoader` | 0..7 | 0 → `{"op":"resolve","loader":0,"value":2}`
1 → `{"op":"resolve","loader":1,"value":2}`
2 → `{"op":"resolve","loader":2,"value":2}`
3 → `{"op":"resolve","loader":3,"value":2}`
4 → `{"op":"resolve","loader":4,"value":2}`
5 → `{"op":"resolve","loader":5,"value":2}`
6 → `{"op":"resolve","loader":6,"value":2}`
7 → `{"op":"resolve","loader":7,"value":2}` |
+| `rejectLoader` | 0..7 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
6 → `{"op":"reject","loader":6}`
7 → `{"op":"reject","loader":7}` |
+| `rejectTimeout` | 0..7 | 0 → `{"op":"reject","loader":0,"error":"timeout"}`
1 → `{"op":"reject","loader":1,"error":"timeout"}`
2 → `{"op":"reject","loader":2,"error":"timeout"}`
3 → `{"op":"reject","loader":3,"error":"timeout"}`
4 → `{"op":"reject","loader":4,"error":"timeout"}`
5 → `{"op":"reject","loader":5,"error":"timeout"}`
6 → `{"op":"reject","loader":6,"error":"timeout"}`
7 → `{"op":"reject","loader":7,"error":"timeout"}` |
+| `releaseLoad` | none | `{"op":"release","effect":"load","index":0}`
every decoding reads `observation.loads` (the count so far at the step; shown with one so far) |
+| `seed` | 0..6 | 0 → `{"op":"seed","value":1,"ageMs":0}`
1 → `{"op":"seed","value":1,"ageMs":999}`
2 → `{"op":"seed","value":1,"ageMs":1000}`
3 → `{"op":"seed","value":1,"ageMs":4999}`
4 → `{"op":"seed","value":1,"ageMs":5000}`
5 → `{"op":"seed","value":1,"ageMs":-1}`
6 → `{"op":"seed","value":2,"ageMs":1000}` |
+| `advance` | 1, 10, 1000, 4000 | 1 → `{"op":"advance","ms":1}`
10 → `{"op":"advance","ms":10}`
1000 → `{"op":"advance","ms":1000}`
4000 → `{"op":"advance","ms":4000}` |
+| `rollbackWall` | none | `{"op":"shiftWall","ms":-1000}` |
+| `invalidate` | none | `{"op":"invalidate"}` |
+| `policy` | 2000, 5000 | 2000 → `{"op":"policy","value":{"staleOnErrorMaxAgeSec":2}}`
5000 → `{"op":"policy","value":{"staleOnErrorMaxAgeSec":5}}` |
+| `readFault` | 0, 1 | 0 → `{"op":"faults","value":{"read":false}}`
1 → `{"op":"faults","value":{"read":true}}` |
+| `loadFault` | 0, 1 | 0 → `{"op":"faults","value":{"load":false}}`
1 → `{"op":"faults","value":{"load":true}}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+- `d`: `ages`, `coalesced`, `fallbackErrors`, `warnings`; diagnostics; ages are the `recoveryAge` events.
+
+## policy
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-policy-conformance.qnt](../models/dialcache-policy-conformance.qnt) |
+| Version | 3, inputs `explicit-v1` |
+| Smoke trace | [policy-smoke.itf.json](./policy-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 512 sampled histories of at most 60 steps from 2048 samples; 12 scheduled invariants; 33 exported regressions |
+| Required witnesses | 51 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+`{"policy":{"ttlSec":{"local":1,"remote":1},"staleOnErrorMaxAgeSec":5},"localMaxSize":1,"fallbackTimeoutMs":null,"observe":["error"]}`
+
+### Setup commands
+
+- `{"op":"faults","value":{"holdPolicies":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0, 1 | 0 → `{"op":"begin","key":"0"}`
1 → `{"op":"begin","key":"1"}` |
+| `releasePolicy` | none | `{"op":"release","effect":"policy","index":0}`
every decoding reads `observation.policyCalls` (the count so far at the step; shown with one so far) |
+| `resolveLoader` | 1..84 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":0}`
4 → `{"op":"resolve","loader":0,"value":null}`
5 → `{"op":"resolve","loader":0,"value":false}`
6 → `{"op":"resolve","loader":0,"value":0}`
7 → `{"op":"resolve","loader":0,"value":""}`
8 → `{"op":"resolve","loader":1,"value":1}`
9 → `{"op":"resolve","loader":1,"value":2}`
10 → `{"op":"resolve","loader":1}`
11 → `{"op":"resolve","loader":1,"value":null}`
12 → `{"op":"resolve","loader":1,"value":false}`
13 → `{"op":"resolve","loader":1,"value":0}`
14 → `{"op":"resolve","loader":1,"value":""}`
15 → `{"op":"resolve","loader":2,"value":1}`
16 → `{"op":"resolve","loader":2,"value":2}`
17 → `{"op":"resolve","loader":2}`
18 → `{"op":"resolve","loader":2,"value":null}`
19 → `{"op":"resolve","loader":2,"value":false}`
20 → `{"op":"resolve","loader":2,"value":0}`
21 → `{"op":"resolve","loader":2,"value":""}`
22 → `{"op":"resolve","loader":3,"value":1}`
23 → `{"op":"resolve","loader":3,"value":2}`
24 → `{"op":"resolve","loader":3}`
25 → `{"op":"resolve","loader":3,"value":null}`
26 → `{"op":"resolve","loader":3,"value":false}`
27 → `{"op":"resolve","loader":3,"value":0}`
28 → `{"op":"resolve","loader":3,"value":""}`
29 → `{"op":"resolve","loader":4,"value":1}`
30 → `{"op":"resolve","loader":4,"value":2}`
31 → `{"op":"resolve","loader":4}`
32 → `{"op":"resolve","loader":4,"value":null}`
33 → `{"op":"resolve","loader":4,"value":false}`
34 → `{"op":"resolve","loader":4,"value":0}`
35 → `{"op":"resolve","loader":4,"value":""}`
36 → `{"op":"resolve","loader":5,"value":1}`
37 → `{"op":"resolve","loader":5,"value":2}`
38 → `{"op":"resolve","loader":5}`
39 → `{"op":"resolve","loader":5,"value":null}`
40 → `{"op":"resolve","loader":5,"value":false}`
41 → `{"op":"resolve","loader":5,"value":0}`
42 → `{"op":"resolve","loader":5,"value":""}`
43 → `{"op":"resolve","loader":6,"value":1}`
44 → `{"op":"resolve","loader":6,"value":2}`
45 → `{"op":"resolve","loader":6}`
46 → `{"op":"resolve","loader":6,"value":null}`
47 → `{"op":"resolve","loader":6,"value":false}`
48 → `{"op":"resolve","loader":6,"value":0}`
49 → `{"op":"resolve","loader":6,"value":""}`
50 → `{"op":"resolve","loader":7,"value":1}`
51 → `{"op":"resolve","loader":7,"value":2}`
52 → `{"op":"resolve","loader":7}`
53 → `{"op":"resolve","loader":7,"value":null}`
54 → `{"op":"resolve","loader":7,"value":false}`
55 → `{"op":"resolve","loader":7,"value":0}`
56 → `{"op":"resolve","loader":7,"value":""}`
57 → `{"op":"resolve","loader":8,"value":1}`
58 → `{"op":"resolve","loader":8,"value":2}`
59 → `{"op":"resolve","loader":8}`
60 → `{"op":"resolve","loader":8,"value":null}`
61 → `{"op":"resolve","loader":8,"value":false}`
62 → `{"op":"resolve","loader":8,"value":0}`
63 → `{"op":"resolve","loader":8,"value":""}`
64 → `{"op":"resolve","loader":9,"value":1}`
65 → `{"op":"resolve","loader":9,"value":2}`
66 → `{"op":"resolve","loader":9}`
67 → `{"op":"resolve","loader":9,"value":null}`
68 → `{"op":"resolve","loader":9,"value":false}`
69 → `{"op":"resolve","loader":9,"value":0}`
70 → `{"op":"resolve","loader":9,"value":""}`
71 → `{"op":"resolve","loader":10,"value":1}`
72 → `{"op":"resolve","loader":10,"value":2}`
73 → `{"op":"resolve","loader":10}`
74 → `{"op":"resolve","loader":10,"value":null}`
75 → `{"op":"resolve","loader":10,"value":false}`
76 → `{"op":"resolve","loader":10,"value":0}`
77 → `{"op":"resolve","loader":10,"value":""}`
78 → `{"op":"resolve","loader":11,"value":1}`
79 → `{"op":"resolve","loader":11,"value":2}`
80 → `{"op":"resolve","loader":11}`
81 → `{"op":"resolve","loader":11,"value":null}`
82 → `{"op":"resolve","loader":11,"value":false}`
83 → `{"op":"resolve","loader":11,"value":0}`
84 → `{"op":"resolve","loader":11,"value":""}` |
+| `rejectLoader` | 0..11 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
6 → `{"op":"reject","loader":6}`
7 → `{"op":"reject","loader":7}`
8 → `{"op":"reject","loader":8}`
9 → `{"op":"reject","loader":9}`
10 → `{"op":"reject","loader":10}`
11 → `{"op":"reject","loader":11}` |
+| `seed` | 0..3 | 0 → `{"op":"seed","key":"0","value":1,"ttlMs":5000}`
1 → `{"op":"seed","key":"0","value":2,"ttlMs":5000}`
2 → `{"op":"seed","key":"1","value":1,"ttlMs":5000}`
3 → `{"op":"seed","key":"1","value":2,"ttlMs":5000}` |
+| `policy` | 0..25 | 0 → `{"op":"policy","value":{}}`
1 → `{"op":"policy","value":{"ttlSec":{"local":2}}}`
2 → `{"op":"policy","value":{"ttlSec":{"remote":2}}}`
3 → `{"op":"policy","value":{"ramp":{"local":0}}}`
4 → `{"op":"policy","value":{"ramp":{"remote":0}}}`
5 → `{"op":"policy","value":{"ttlSec":{"local":-1}}}`
6 → `{"op":"policy","value":{"ttlSec":{"remote":-1}}}`
7 → `{"op":"policy","value":{"staleOnErrorMaxAgeSec":2}}`
8 → `{"op":"policy","value":{"ramp":{"local":0,"remote":0}}}`
9 → `{"op":"policy","value":{"ttlSec":{"remote":4},"staleOnErrorMaxAgeSec":0}}`
10 → `{"op":"policy","value":{"coalesce":false}}`
11 → `{"op":"policy","value":{"ttlSec":{"local":2},"coalesce":false}}`
12 → `{"op":"policy","value":{"ttlSec":{"remote":2},"coalesce":false}}`
13 → `{"op":"policy","value":{"ramp":{"local":0},"coalesce":false}}`
14 → `{"op":"policy","value":{"ramp":{"remote":0},"coalesce":false}}`
15 → `{"op":"policy","value":{"ttlSec":{"local":-1},"coalesce":false}}`
16 → `{"op":"policy","value":{"ttlSec":{"remote":-1},"coalesce":false}}`
17 → `{"op":"policy","value":{"staleOnErrorMaxAgeSec":2,"coalesce":false}}`
18 → `{"op":"policy","value":{"ramp":{"local":0,"remote":0},"coalesce":false}}`
19 → `{"op":"policy","value":{"ttlSec":{"remote":4},"staleOnErrorMaxAgeSec":0,"coalesce":false}}`
20 → `{"op":"policy","value":{"remoteReadTimeoutMs":0}}`
21 → `{"op":"policy","value":{"ramp":{"local":101}}}`
22 → `{"op":"policy","value":{"ramp":{"remote":101}}}`
23 → `{"op":"policy","value":{"staleOnErrorMaxAgeSec":1}}`
24 → `{"op":"policy","value":{"staleOnErrorMaxAgeSec":-1}}`
25 → `{"op":"policy","value":{"shadow":{"ramp":101}}}` |
+| `advance` | 1, 500, 1000, 2000, 5000 | 1 → `{"op":"advance","ms":1}`
500 → `{"op":"advance","ms":500}`
1000 → `{"op":"advance","ms":1000}`
2000 → `{"op":"advance","ms":2000}`
5000 → `{"op":"advance","ms":5000}` |
+| `rollbackWall` | none | `{"op":"shiftWall","ms":-1000}` |
+| `providerFault` | 0, 1 | 0 → `{"op":"faults","value":{"policy":false}}`
1 → `{"op":"faults","value":{"policy":true}}` |
+| `readFault` | 0, 1 | 0 → `{"op":"faults","value":{"read":false}}`
1 → `{"op":"faults","value":{"read":true}}` |
+| `dumpFault` | 0, 1 | 0 → `{"op":"faults","value":{"dump":false}}`
1 → `{"op":"faults","value":{"dump":true}}` |
+| `writeFault` | 0, 1 | 0 → `{"op":"faults","value":{"write":false}}`
1 → `{"op":"faults","value":{"write":true}}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+- `policyErrors`: `layer`, `errorType`; one record per configuration error.
+
+## shadow
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-shadow-conformance.qnt](../models/dialcache-shadow-conformance.qnt) |
+| Version | 3, inputs `explicit-v1` |
+| Smoke trace | [shadow-smoke.itf.json](./shadow-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 1024 sampled histories of at most 60 steps from 4096 samples; 14 scheduled invariants; 40 exported regressions |
+| Required witnesses | 77 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture, by init choice
+
+| Init choice | Fixture |
+| --- | --- |
+| 0 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":true,"observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 1 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":true,"comparator":"equal","observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 2 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":true,"comparator":"unequal","observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 3 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":true,"comparator":"error","observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 4 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100,"logMismatches":true}},"tracked":true,"shadowHook":true,"observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 5 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100,"logMismatches":true}},"tracked":true,"shadowHook":true,"comparator":"equal","observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 6 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100,"logMismatches":true}},"tracked":true,"shadowHook":true,"comparator":"unequal","observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 7 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100,"logMismatches":true}},"tracked":true,"shadowHook":true,"comparator":"error","observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 8 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":false,"observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 9 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":true,"comparator":"equal","comparisonMs":10,"observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 10 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":true,"comparator":"error","comparisonMs":10,"observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 11 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":true,"sourceWorkMs":9,"observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+| 12 | `{"policy":{"ttlSec":{"remote":60},"ramp":{"remote":0},"shadow":{"ramp":100}},"tracked":true,"shadowHook":true,"sourceWorkMs":10,"observe":["shadowAge","mismatchWarning","coalesced","error","futureOffset"]}` |
+
+### Setup commands
+
+- `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | none | `{"op":"begin"}` |
+| `resolveLoader` | 1, 2 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
every decoding reads `observation.loaders` (the count so far at the step; shown with one so far) |
+| `rejectLoader` | none | `{"op":"reject","loader":0}`
every decoding reads `observation.loaders` (the count so far at the step; shown with one so far) |
+| `releaseRead` | none | `{"op":"release","effect":"read","index":0}`
every decoding reads `observation.reads` (the count so far at the step; shown with one so far) |
+| `releaseLoad` | none | `{"op":"release","effect":"load","index":0}`
every decoding reads `observation.loads` (the count so far at the step; shown with one so far) |
+| `releaseDump` | none | `{"op":"release","effect":"dump","index":0}`
every decoding reads `observation.dumps` (the count so far at the step; shown with one so far) |
+| `releaseWrite` | none | `{"op":"release","effect":"write","index":0}`
every decoding reads `observation.writes` (the count so far at the step; shown with one so far) |
+| `advance` | 1, 10 | 1 → `{"op":"advance","ms":1}`
10 → `{"op":"advance","ms":10}` |
+| `seed` | 1..8 | 1 → `{"op":"seed","value":1}`
2 → `{"op":"seed","value":2}`
3 → `{"op":"seed","payloadHex":"31"}`
4 → `{"op":"seed","payloadHex":"32"}`
5 → `{"op":"seed","payloadHex":"2031"}`
6 → `{"op":"seed","payloadText":" 1"}`
7 → `{"op":"seed","payloadText":"\"café\""}`
8 → `{"op":"seed","payloadHex":"22636166c3a922"}` |
+| `reencode` | 1..8 | 1 → `{"op":"seed","value":1}`
2 → `{"op":"seed","value":2}`
3 → `{"op":"seed","payloadHex":"31"}`
4 → `{"op":"seed","payloadHex":"32"}`
5 → `{"op":"seed","payloadHex":"2031"}`
6 → `{"op":"seed","payloadText":" 1"}`
7 → `{"op":"seed","payloadText":"\"café\""}`
8 → `{"op":"seed","payloadHex":"22636166c3a922"}` |
+| `seedUnicode` | 7, 8 | 7 → `{"op":"seed","payloadText":"\"café\""}`
8 → `{"op":"seed","payloadHex":"22636166c3a922"}` |
+| `invalidate` | 0, 20 | 0 → `{"op":"invalidate","futureBufferMs":0}`
20 → `{"op":"invalidate","futureBufferMs":20}` |
+| `readFault` | 0, 1 | 0 → `{"op":"faults","value":{"read":false}}`
1 → `{"op":"faults","value":{"read":true}}` |
+| `loadFault` | 0, 1 | 0 → `{"op":"faults","value":{"load":false}}`
1 → `{"op":"faults","value":{"load":true}}` |
+| `dumpFault` | 0, 1 | 0 → `{"op":"faults","value":{"dump":false}}`
1 → `{"op":"faults","value":{"dump":true}}` |
+| `writeFault` | 0, 1 | 0 → `{"op":"faults","value":{"write":false}}`
1 → `{"op":"faults","value":{"write":true}}` |
+| `rollbackWall` | none | `{"op":"shiftWall","ms":-1000}` |
+| `advanceWall` | 1, 60000 | 1 → `{"op":"shiftWall","ms":1}`
60000 → `{"op":"shiftWall","ms":60000}` |
+| `shadowPolicy` | 0..2 | 0 → `{"op":"policy","value":{"shadow":{"ramp":100}}}`
1 → `{"op":"policy","value":{"shadow":{"ramp":0}}}`
2 → `{"op":"policy","value":{"shadow":{"ramp":101}}}` |
+| `logPolicy` | 0..2 | 0 → `{"op":"policy","value":{"shadow":{"logMismatches":false}}}`
1 → `{"op":"policy","value":{"shadow":{"logMismatches":true}}}`
2 → `{"op":"policy","value":{"shadow":{"logMismatches":"invalid"}}}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+- `d`: `ages`, `coalesced`, `fallbackErrors`, `warnings`, `configErrors`, `futureOffsets`; diagnostics; ages are the `shadowAge` events.
+
+## admission
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-admission-conformance.qnt](../models/dialcache-admission-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [admission-smoke.itf.json](./admission-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 128 sampled histories of at most 60 steps from 1024 samples; 10 scheduled invariants; 9 exported regressions |
+| Required witnesses | 19 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+`{"policy":{"ttlSec":{"remote":60},"shadow":{"ramp":100}},"tracked":true,"shadowMaxInFlight":2,"readTimeoutMs":1000,"probeSourceScope":true}`
+
+### Setup commands
+
+- `{"op":"seed","key":"0","value":1}`
+- `{"op":"seed","key":"1","value":1}`
+- `{"op":"seed","key":"2","value":1}`
+- `{"op":"faults","value":{"holdReads":true,"holdLoads":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0..5 | 0 → `{"op":"begin","key":"0","instance":"0"}`
1 → `{"op":"begin","key":"1","instance":"0"}`
2 → `{"op":"begin","key":"2","instance":"0"}`
3 → `{"op":"begin","key":"0","instance":"1"}`
4 → `{"op":"begin","key":"1","instance":"1"}`
5 → `{"op":"begin","key":"2","instance":"1"}` |
+| `releaseRead` | 0..31 | 0 → `{"op":"release","effect":"read","index":0}`
1 → `{"op":"release","effect":"read","index":1}`
2 → `{"op":"release","effect":"read","index":2}`
3 → `{"op":"release","effect":"read","index":3}`
4 → `{"op":"release","effect":"read","index":4}`
5 → `{"op":"release","effect":"read","index":5}`
… one more per choice …
30 → `{"op":"release","effect":"read","index":30}`
31 → `{"op":"release","effect":"read","index":31}` |
+| `releaseLoad` | 0..31 | 0 → `{"op":"release","effect":"load","index":0}`
1 → `{"op":"release","effect":"load","index":1}`
2 → `{"op":"release","effect":"load","index":2}`
3 → `{"op":"release","effect":"load","index":3}`
4 → `{"op":"release","effect":"load","index":4}`
5 → `{"op":"release","effect":"load","index":5}`
… one more per choice …
30 → `{"op":"release","effect":"load","index":30}`
31 → `{"op":"release","effect":"load","index":31}` |
+| `resolveLoader` | 1..32 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":1,"value":1}`
4 → `{"op":"resolve","loader":1,"value":2}`
5 → `{"op":"resolve","loader":2,"value":1}`
6 → `{"op":"resolve","loader":2,"value":2}`
7 → `{"op":"resolve","loader":3,"value":1}`
8 → `{"op":"resolve","loader":3,"value":2}`
9 → `{"op":"resolve","loader":4,"value":1}`
10 → `{"op":"resolve","loader":4,"value":2}`
11 → `{"op":"resolve","loader":5,"value":1}`
12 → `{"op":"resolve","loader":5,"value":2}`
13 → `{"op":"resolve","loader":6,"value":1}`
14 → `{"op":"resolve","loader":6,"value":2}`
15 → `{"op":"resolve","loader":7,"value":1}`
16 → `{"op":"resolve","loader":7,"value":2}`
17 → `{"op":"resolve","loader":8,"value":1}`
18 → `{"op":"resolve","loader":8,"value":2}`
19 → `{"op":"resolve","loader":9,"value":1}`
20 → `{"op":"resolve","loader":9,"value":2}`
21 → `{"op":"resolve","loader":10,"value":1}`
22 → `{"op":"resolve","loader":10,"value":2}`
23 → `{"op":"resolve","loader":11,"value":1}`
24 → `{"op":"resolve","loader":11,"value":2}`
25 → `{"op":"resolve","loader":12,"value":1}`
26 → `{"op":"resolve","loader":12,"value":2}`
27 → `{"op":"resolve","loader":13,"value":1}`
28 → `{"op":"resolve","loader":13,"value":2}`
29 → `{"op":"resolve","loader":14,"value":1}`
30 → `{"op":"resolve","loader":14,"value":2}`
31 → `{"op":"resolve","loader":15,"value":1}`
32 → `{"op":"resolve","loader":15,"value":2}` |
+| `rejectLoader` | 0..15 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
… one more per choice …
14 → `{"op":"reject","loader":14}`
15 → `{"op":"reject","loader":15}` |
+| `seed` | 0..5 | 0 → `{"op":"seed","key":"0","value":1}`
1 → `{"op":"seed","key":"0","value":2}`
2 → `{"op":"seed","key":"1","value":1}`
3 → `{"op":"seed","key":"1","value":2}`
4 → `{"op":"seed","key":"2","value":1}`
5 → `{"op":"seed","key":"2","value":2}` |
+| `advance` | 1, 10 | 1 → `{"op":"advance","ms":1}`
10 → `{"op":"advance","ms":10}` |
+| `policy` | 0..3 | 0 → `{"op":"policy","value":{"shadow":{"ramp":100},"coalesce":true}}`
1 → `{"op":"policy","value":{"shadow":{"ramp":0},"coalesce":true}}`
2 → `{"op":"policy","value":{"shadow":{"ramp":100},"coalesce":false}}`
3 → `{"op":"policy","value":{"shadow":{"ramp":0},"coalesce":false}}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+
+## layers
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-layers-conformance.qnt](../models/dialcache-layers-conformance.qnt) |
+| Version | 2, inputs `explicit-v1` |
+| Smoke trace | [layers-smoke.itf.json](./layers-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 512 sampled histories of at most 80 steps from 2048 samples; 10 scheduled invariants; 17 exported regressions |
+| Required witnesses | 27 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture, by init choice
+
+| Init choice | Fixture |
+| --- | --- |
+| 0 | `{"policy":{"requestLocal":true,"ttlSec":{"local":60,"remote":60}},"tracked":false,"remote":true,"localMaxSize":2,"fallbackTimeoutMs":null}` |
+| 1 | `{"policy":{"requestLocal":true,"ttlSec":{"local":60,"remote":60}},"tracked":true,"remote":true,"localMaxSize":2,"fallbackTimeoutMs":null}` |
+| 2 | `{"policy":{"requestLocal":true,"ttlSec":{"local":60,"remote":60}},"tracked":false,"remote":true,"localMaxSize":0,"fallbackTimeoutMs":null}` |
+| 3 | `{"policy":{"requestLocal":true,"ttlSec":{"local":60,"remote":60}},"tracked":true,"remote":true,"localMaxSize":0,"fallbackTimeoutMs":null}` |
+| 4 | `{"policy":{"requestLocal":true,"ttlSec":{"local":60,"remote":60}},"tracked":false,"remote":false,"localMaxSize":2,"fallbackTimeoutMs":null}` |
+| 5 | `{"policy":{"requestLocal":true,"ttlSec":{"local":60,"remote":60}},"tracked":true,"remote":false,"localMaxSize":2,"fallbackTimeoutMs":null}` |
+
+### Setup commands
+
+- `{"op":"openScope","id":"0","instance":"0"}`
+- `{"op":"openScope","id":"1","instance":"0"}`
+- `{"op":"openScope","id":"2","instance":"1"}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0..19 | 0 → `{"op":"begin","key":"0","useCase":"Layers0","scope":"0"}`
1 → `{"op":"begin","key":"0","useCase":"Layers1","scope":"0"}`
2 → `{"op":"begin","key":"1","useCase":"Layers0","scope":"0"}`
3 → `{"op":"begin","key":"1","useCase":"Layers1","scope":"0"}`
4 → `{"op":"begin","key":"0","useCase":"Layers0","scope":"1"}`
5 → `{"op":"begin","key":"0","useCase":"Layers1","scope":"1"}`
6 → `{"op":"begin","key":"1","useCase":"Layers0","scope":"1"}`
7 → `{"op":"begin","key":"1","useCase":"Layers1","scope":"1"}`
8 → `{"op":"begin","key":"0","useCase":"Layers0","scope":"2"}`
9 → `{"op":"begin","key":"0","useCase":"Layers1","scope":"2"}`
10 → `{"op":"begin","key":"1","useCase":"Layers0","scope":"2"}`
11 → `{"op":"begin","key":"1","useCase":"Layers1","scope":"2"}`
12 → `{"op":"begin","key":"0","useCase":"Layers0","instance":"0"}`
13 → `{"op":"begin","key":"0","useCase":"Layers1","instance":"0"}`
14 → `{"op":"begin","key":"1","useCase":"Layers0","instance":"0"}`
15 → `{"op":"begin","key":"1","useCase":"Layers1","instance":"0"}`
16 → `{"op":"begin","key":"0","useCase":"Layers0","instance":"1"}`
17 → `{"op":"begin","key":"0","useCase":"Layers1","instance":"1"}`
18 → `{"op":"begin","key":"1","useCase":"Layers0","instance":"1"}`
19 → `{"op":"begin","key":"1","useCase":"Layers1","instance":"1"}` |
+| `resolveLoader` | 1..40 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":1,"value":1}`
4 → `{"op":"resolve","loader":1,"value":2}`
5 → `{"op":"resolve","loader":2,"value":1}`
6 → `{"op":"resolve","loader":2,"value":2}`
7 → `{"op":"resolve","loader":3,"value":1}`
8 → `{"op":"resolve","loader":3,"value":2}`
9 → `{"op":"resolve","loader":4,"value":1}`
10 → `{"op":"resolve","loader":4,"value":2}`
11 → `{"op":"resolve","loader":5,"value":1}`
12 → `{"op":"resolve","loader":5,"value":2}`
13 → `{"op":"resolve","loader":6,"value":1}`
14 → `{"op":"resolve","loader":6,"value":2}`
15 → `{"op":"resolve","loader":7,"value":1}`
16 → `{"op":"resolve","loader":7,"value":2}`
17 → `{"op":"resolve","loader":8,"value":1}`
18 → `{"op":"resolve","loader":8,"value":2}`
19 → `{"op":"resolve","loader":9,"value":1}`
20 → `{"op":"resolve","loader":9,"value":2}`
21 → `{"op":"resolve","loader":10,"value":1}`
22 → `{"op":"resolve","loader":10,"value":2}`
23 → `{"op":"resolve","loader":11,"value":1}`
24 → `{"op":"resolve","loader":11,"value":2}`
25 → `{"op":"resolve","loader":12,"value":1}`
26 → `{"op":"resolve","loader":12,"value":2}`
27 → `{"op":"resolve","loader":13,"value":1}`
28 → `{"op":"resolve","loader":13,"value":2}`
29 → `{"op":"resolve","loader":14,"value":1}`
30 → `{"op":"resolve","loader":14,"value":2}`
31 → `{"op":"resolve","loader":15,"value":1}`
32 → `{"op":"resolve","loader":15,"value":2}`
33 → `{"op":"resolve","loader":16,"value":1}`
34 → `{"op":"resolve","loader":16,"value":2}`
35 → `{"op":"resolve","loader":17,"value":1}`
36 → `{"op":"resolve","loader":17,"value":2}`
37 → `{"op":"resolve","loader":18,"value":1}`
38 → `{"op":"resolve","loader":18,"value":2}`
39 → `{"op":"resolve","loader":19,"value":1}`
40 → `{"op":"resolve","loader":19,"value":2}` |
+| `rejectLoader` | 0..19 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
… one more per choice …
18 → `{"op":"reject","loader":18}`
19 → `{"op":"reject","loader":19}` |
+| `closeScope` | 0..2 | 0 → `{"op":"closeScope","id":"0"}`
1 → `{"op":"closeScope","id":"1"}`
2 → `{"op":"closeScope","id":"2"}` |
+| `policy` | 0..5 | 0 → `{"op":"policy","value":{}}`
1 → `{"op":"policy","value":{"requestLocal":false}}`
2 → `{"op":"policy","value":{"ramp":{"local":0}}}`
3 → `{"op":"policy","value":{"ramp":{"remote":0}}}`
4 → `{"op":"policy","value":{"ramp":{"local":0,"remote":0}}}`
5 → `{"op":"policy","value":{"requestLocal":false,"ramp":{"local":0,"remote":0}}}` |
+| `seed` | 0..7 | 0 → `{"op":"seed","key":"0","useCase":"Layers0","value":1}`
1 → `{"op":"seed","key":"0","useCase":"Layers0","value":2}`
2 → `{"op":"seed","key":"0","useCase":"Layers1","value":1}`
3 → `{"op":"seed","key":"0","useCase":"Layers1","value":2}`
4 → `{"op":"seed","key":"1","useCase":"Layers0","value":1}`
5 → `{"op":"seed","key":"1","useCase":"Layers0","value":2}`
6 → `{"op":"seed","key":"1","useCase":"Layers1","value":1}`
7 → `{"op":"seed","key":"1","useCase":"Layers1","value":2}` |
+| `invalidate` | 0, 1 | 0 → `{"op":"invalidate","key":"0"}`
1 → `{"op":"invalidate","key":"1"}` |
+| `tick` | none | `{"op":"advance","ms":1}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+
+## independent
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-independent-conformance.qnt](../models/dialcache-independent-conformance.qnt) |
+| Version | 2, inputs `explicit-v1` |
+| Smoke trace | [independent-smoke.itf.json](./independent-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 512 sampled histories of at most 60 steps from 2048 samples; 7 scheduled invariants; 15 exported regressions |
+| Required witnesses | 18 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+`{"policy":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5,"coalesce":false},"tracked":true,"readTimeoutMs":5,"fallbackTimeoutMs":10,"recovery":"allow","observe":["readContext","readAbort"]}`
+
+### Setup commands
+
+- `{"op":"seed","value":1,"ageMs":1000}`
+- `{"op":"faults","value":{"holdReads":true,"holdLoads":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | none | `{"op":"begin"}` |
+| `releaseRead` | 0..5 | 0 → `{"op":"release","effect":"read","index":0,"fail":false}`
1 → `{"op":"release","effect":"read","index":1,"fail":false}`
2 → `{"op":"release","effect":"read","index":2,"fail":false}`
3 → `{"op":"release","effect":"read","index":3,"fail":false}`
4 → `{"op":"release","effect":"read","index":4,"fail":false}`
5 → `{"op":"release","effect":"read","index":5,"fail":false}` |
+| `failRead` | 0..5 | 0 → `{"op":"release","effect":"read","index":0,"fail":true}`
1 → `{"op":"release","effect":"read","index":1,"fail":true}`
2 → `{"op":"release","effect":"read","index":2,"fail":true}`
3 → `{"op":"release","effect":"read","index":3,"fail":true}`
4 → `{"op":"release","effect":"read","index":4,"fail":true}`
5 → `{"op":"release","effect":"read","index":5,"fail":true}` |
+| `releaseLoad` | 0..5 | 0 → `{"op":"release","effect":"load","index":0,"fail":false}`
1 → `{"op":"release","effect":"load","index":1,"fail":false}`
2 → `{"op":"release","effect":"load","index":2,"fail":false}`
3 → `{"op":"release","effect":"load","index":3,"fail":false}`
4 → `{"op":"release","effect":"load","index":4,"fail":false}`
5 → `{"op":"release","effect":"load","index":5,"fail":false}` |
+| `failLoad` | 0..5 | 0 → `{"op":"release","effect":"load","index":0,"fail":true}`
1 → `{"op":"release","effect":"load","index":1,"fail":true}`
2 → `{"op":"release","effect":"load","index":2,"fail":true}`
3 → `{"op":"release","effect":"load","index":3,"fail":true}`
4 → `{"op":"release","effect":"load","index":4,"fail":true}`
5 → `{"op":"release","effect":"load","index":5,"fail":true}` |
+| `resolveLoader` | 1..12 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":1,"value":1}`
4 → `{"op":"resolve","loader":1,"value":2}`
5 → `{"op":"resolve","loader":2,"value":1}`
6 → `{"op":"resolve","loader":2,"value":2}`
7 → `{"op":"resolve","loader":3,"value":1}`
8 → `{"op":"resolve","loader":3,"value":2}`
9 → `{"op":"resolve","loader":4,"value":1}`
10 → `{"op":"resolve","loader":4,"value":2}`
11 → `{"op":"resolve","loader":5,"value":1}`
12 → `{"op":"resolve","loader":5,"value":2}` |
+| `rejectLoader` | 0..5 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}` |
+| `advance` | 1, 5, 10, 1000 | 1 → `{"op":"advance","ms":1}`
5 → `{"op":"advance","ms":5}`
10 → `{"op":"advance","ms":10}`
1000 → `{"op":"advance","ms":1000}` |
+| `seed` | 0..5 | 0 → `{"op":"seed","value":1,"ageMs":0}`
1 → `{"op":"seed","value":1,"ageMs":1000}`
2 → `{"op":"seed","value":2,"ageMs":1000}`
3 → `{"op":"seed","value":1,"ageMs":4999}`
4 → `{"op":"seed","value":2,"ageMs":0}`
5 → `{"op":"seed","value":1,"ageMs":1999}` |
+| `invalidate` | none | `{"op":"invalidate"}` |
+| `policy` | 0..3 | 0 → `{"op":"policy","value":{"remoteReadTimeoutMs":5,"staleOnErrorMaxAgeSec":5}}`
1 → `{"op":"policy","value":{"remoteReadTimeoutMs":10,"staleOnErrorMaxAgeSec":5}}`
2 → `{"op":"policy","value":{"remoteReadTimeoutMs":5,"staleOnErrorMaxAgeSec":2}}`
3 → `{"op":"policy","value":{"remoteReadTimeoutMs":10,"staleOnErrorMaxAgeSec":2}}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+- `io`: `budgets`, `aborted`, `sourceErrors`; read budgets in dispatch order, aborted read indices, each caller's source-error identity.
+
+## recovery-read
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-recovery-read-conformance.qnt](../models/dialcache-recovery-read-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [recovery-read-smoke.itf.json](./recovery-read-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 256 sampled histories of at most 60 steps from 1024 samples; 8 scheduled invariants; 34 exported regressions |
+| Required witnesses | 26 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture, by init choice
+
+| Init choice | Fixture |
+| --- | --- |
+| 0 | `{"policy":{"requestLocal":true,"ttlSec":{"local":1,"remote":1},"staleOnErrorMaxAgeSec":5},"tracked":false,"recovery":"allow","fallbackTimeoutMs":null,"readTimeoutMs":30000000,"observe":["readContext","readAbort","marker","compression"]}` |
+| 1 | `{"policy":{"requestLocal":true,"ttlSec":{"local":1,"remote":1},"staleOnErrorMaxAgeSec":5},"tracked":true,"recovery":"allow","fallbackTimeoutMs":null,"readTimeoutMs":30000000,"observe":["readContext","readAbort","marker","compression"]}` |
+| 2 | `{"policy":{"requestLocal":true,"ttlSec":{"local":1,"remote":1},"staleOnErrorMaxAgeSec":5,"shadow":{"ramp":100}},"tracked":true,"recovery":"allow","fallbackTimeoutMs":null,"readTimeoutMs":30000000,"observe":["readContext","readAbort","marker","compression"]}` |
+
+### Setup commands
+
+- `{"op":"openScope","id":"0"}`
+- `{"op":"openScope","id":"1"}`
+- `{"op":"faults","value":{"holdReads":true,"holdLoads":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0..2 | 0 → `{"op":"begin","scope":"0"}`
1 → `{"op":"begin","scope":"1"}`
2 → `{"op":"begin"}` |
+| `releaseRead` | none | `{"op":"release","effect":"read","index":0}`
every decoding reads `observation.reads` (the count so far at the step; shown with one so far) |
+| `releaseLoad` | none | `{"op":"release","effect":"load","index":0}`
every decoding reads `observation.loads` (the count so far at the step; shown with one so far) |
+| `rejectLoader` | none | `{"op":"reject","loader":0}`
every decoding reads `observation.loaders` (the count so far at the step; shown with one so far) |
+| `resolveLoader` | none | `{"op":"resolve","loader":0,"value":2}`
every decoding reads `observation.loaders` (the count so far at the step; shown with one so far) |
+| `seed` | 0..18 | 0 → `{"op":"seed","ageMs":0,"ttlMs":60000,"value":1}`
1 → `{"op":"seed","ageMs":999,"ttlMs":60000,"value":1}`
2 → `{"op":"seed","ageMs":1000,"ttlMs":60000,"value":1}`
3 → `{"op":"seed","ageMs":4999,"ttlMs":60000,"value":1}`
4 → `{"op":"seed","ageMs":5000,"ttlMs":60000,"value":1}`
5 → `{"op":"seed","ageMs":3600001,"ttlMs":60000,"value":1}`
6 → `{"op":"seed","ageMs":7200000,"ttlMs":60000,"value":1}`
7 → `{"op":"seed","ageMs":0,"ttlMs":60000,"value":2}`
8 → `{"op":"seed","ageMs":1000,"ttlMs":60000,"payloadHex":"0128b52ffd200109000031"}`
9 → `{"op":"seed","ageMs":1000,"ttlMs":60000,"payloadHex":"016e6f742061207a737464206672616d65"}`
10 → `{"op":"seed","ageMs":0,"ttlMs":60000,"frameHex":"010000000000000000ff31"}`
11 → `{"op":"seed","ageMs":0,"ttlMs":1000,"value":1}`
12 → `{"op":"seed","ageMs":4999,"ttlMs":60000,"payloadHex":"0128b52ffd200109000031"}`
13 → `{"op":"seed","ageMs":0,"ttlMs":60000,"payloadHex":"0128b52ffd200109000031"}`
14 → `{"op":"seed","ageMs":0,"ttlMs":60000,"payloadHex":"016e6f742061207a737464206672616d65"}`
15 → `{"op":"seed","ageMs":1000,"ttlMs":1000,"value":1}`
16 → `{"op":"seed","ageMs":0,"ttlMs":60000,"frameHex":"0100200000000000010031"}`
17 → `{"op":"seed","ageMs":0,"ttlMs":60000,"frameHex":"0200000000000000000031"}`
18 → `{"op":"seed","ageMs":1000,"ttlMs":60000}`
choices 10, 17 read `environment.wallMs` (the environment value at the step; shown as 0) |
+| `advance` | 1, 999, 1000, 4000, 60000, 3600000 | 1 → `{"op":"advance","ms":1}`
999 → `{"op":"advance","ms":999}`
1000 → `{"op":"advance","ms":1000}`
4000 → `{"op":"advance","ms":4000}`
60000 → `{"op":"advance","ms":60000}`
3600000 → `{"op":"advance","ms":3600000}` |
+| `policy` | 0..2 | 0 → `{"op":"policy","value":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":5}}`
1 → `{"op":"policy","value":{"ttlSec":{"remote":1},"staleOnErrorMaxAgeSec":7200}}`
2 → `{"op":"policy","value":{"ttlSec":{"remote":7200},"staleOnErrorMaxAgeSec":14400}}` |
+| `closeScope` | 0, 1 | 0 → `{"op":"closeScope","id":"0"}`
1 → `{"op":"closeScope","id":"1"}` |
+| `invalidate` | none | `{"op":"invalidate"}` |
+| `observeMarker` | none | `{"op":"observeMarker"}` |
+| `writeFault` | 0, 1 | 0 → `{"op":"faults","value":{"write":false}}`
1 → `{"op":"faults","value":{"write":true}}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+- `io`: `budgets`, `aborted`, `sourceErrors`; read budgets in dispatch order, aborted read indices, each caller's source-error identity.
+- `markers`: `cutoffMs`, `ttlMs`; one record per observed invalidation marker.
+- `compression`: `decompressed`, `fallback_raw`; one outcome per decode.
+
+## local-failure
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-local-failure-conformance.qnt](../models/dialcache-local-failure-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [local-failure-smoke.itf.json](./local-failure-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 128 sampled histories of at most 40 steps from 512 samples; 6 scheduled invariants; 5 exported regressions |
+| Required witnesses | 4 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+`{"policy":{"requestLocal":true,"ttlSec":{"local":60,"remote":60}},"fallbackTimeoutMs":null,"localFaultInjection":true}`
+
+### Setup commands
+
+- `{"op":"openScope","id":"0"}`
+- `{"op":"openScope","id":"1"}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0..2 | 0 → `{"op":"begin","scope":"0"}`
1 → `{"op":"begin","scope":"1"}`
2 → `{"op":"begin"}` |
+| `resolveLoader` | 1, 2 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
every decoding reads `observation.loaders` (the count so far at the step; shown with one so far) |
+| `rejectLoader` | none | `{"op":"reject","loader":0}`
every decoding reads `observation.loaders` (the count so far at the step; shown with one so far) |
+| `localFault` | 0, 1 | 0 → `{"op":"faults","value":{"localStorage":false}}`
1 → `{"op":"faults","value":{"localStorage":true}}` |
+| `policy` | 0, 1 | 0 → `{"op":"policy","value":{"ramp":{"remote":0}}}`
1 → `{"op":"policy","value":{"ramp":{"remote":100}}}` |
+| `seed` | 1, 2 | 1 → `{"op":"seed","value":1}`
2 → `{"op":"seed","value":2}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+
+## runtime-boundaries
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-runtime-boundaries-conformance.qnt](../models/dialcache-runtime-boundaries-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [runtime-boundaries-smoke.itf.json](./runtime-boundaries-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 256 sampled histories of at most 60 steps from 1024 samples; 7 scheduled invariants; 29 exported regressions |
+| Required witnesses | 22 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture, by init choice
+
+| Init choice | Fixture |
+| --- | --- |
+| 0 | `{"policy":{"coalesce":false,"requestLocal":true},"remote":false,"fallbackTimeoutMs":null}` |
+| 1 | `{"policy":{"coalesce":false,"ttlSec":{"local":60}},"remote":false,"fallbackTimeoutMs":null}` |
+| 2 | `{"policy":{"coalesce":false,"ttlSec":{"remote":60}},"remote":true,"fallbackTimeoutMs":null}` |
+| 3 | `{"policy":{"requestLocal":true},"remote":false,"fallbackTimeoutMs":null}` |
+| 4 | `{"policy":{"ttlSec":{"local":60}},"remote":false,"fallbackTimeoutMs":null}` |
+| 5 | `{"policy":{"ttlSec":{"remote":60}},"remote":true,"fallbackTimeoutMs":null}` |
+| 6 | `{"policy":{},"remote":false,"fallbackTimeoutMs":null}` |
+| 7 | `{"policy":{},"remote":true,"fallbackTimeoutMs":null}` |
+| 8 | `{"policy":{"requestLocal":false,"ramp":{"local":0,"remote":0},"staleOnErrorMaxAgeSec":0,"shadow":{"ramp":0}},"remote":false,"fallbackTimeoutMs":null}` |
+| 9 | `{"policy":{"requestLocal":true,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":100}},"remote":true,"fallbackTimeoutMs":null}` |
+
+### Setup commands
+
+- `{"op":"openScope","id":"0"}`
+- `{"op":"faults","value":{"holdPolicies":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | none | `{"op":"begin","scope":"0"}` |
+| `releasePolicy` | none | `{"op":"release","effect":"policy","index":0}`
every decoding reads `observation.policyCalls` (the count so far at the step; shown with one so far) |
+| `closeScope` | none | `{"op":"closeScope","id":"0"}` |
+| `policy` | 0..21 | 0 → `{"op":"policy","value":{"ramp":{"local":99.95154615025967,"remote":23.72337388806045}}}`
1 → `{"op":"policy","value":{"coalesce":false,"ramp":{"local":99.95154615025967,"remote":23.72337388806045}}}`
2 → `{"op":"policy","value":{"coalesce":true,"ramp":{"local":99.95154615025967,"remote":23.72337388806045}}}`
3 → `{"op":"policy","value":{"ramp":{"local":99.95154617354274,"remote":23.723373911343515}}}`
4 → `{"op":"policy","value":{"coalesce":false,"ramp":{"local":99.95154617354274,"remote":23.723373911343515}}}`
5 → `{"op":"policy","value":{"coalesce":true,"ramp":{"local":99.95154617354274,"remote":23.723373911343515}}}`
6 → `{"op":"policy","value":{"ramp":{"local":99.9515461968258,"remote":23.72337393462658}}}`
7 → `{"op":"policy","value":{"coalesce":false,"ramp":{"local":99.9515461968258,"remote":23.72337393462658}}}`
8 → `{"op":"policy","value":{"coalesce":true,"ramp":{"local":99.9515461968258,"remote":23.72337393462658}}}`
9 → `{"op":"policy","value":{}}`
10 → `{"op":"policy","value":{"coalesce":false}}`
11 → `{"op":"policy","value":{"coalesce":true}}`
12 → `{"op":"policy","value":null}`
13 → `{"op":"policy","value":{"requestLocal":false}}`
14 → `{"op":"policy","value":{"coalesce":"invalid"}}`
15 → `{"op":"policy","value":{"requestLocal":"invalid"}}`
16 → `{"op":"policy","value":{"coalesce":null}}`
17 → `{"op":"policy","value":{"requestLocal":null}}`
18 → `{"op":"policy","value":{"ttlSec":{"local":60}}}`
19 → `{"op":"policy","value":{"ttlSec":{"remote":60}}}`
20 → `{"op":"policy","value":{"ttlSec":{"local":60},"ramp":{"local":100}}}`
21 → `{"op":"policy","value":{"requestLocal":false,"ramp":{"local":0,"remote":0},"staleOnErrorMaxAgeSec":0,"shadow":{"ramp":0}}}` |
+| `resolveLoader` | 0..63 | 0 → `{"op":"resolve","loader":0,"value":1}`
1 → `{"op":"resolve","loader":0,"value":2}`
2 → `{"op":"resolve","loader":0}`
3 → `{"op":"resolve","loader":0,"value":"undefined"}`
4 → `{"op":"resolve","loader":0,"value":null}`
5 → `{"op":"resolve","loader":0,"value":false}`
6 → `{"op":"resolve","loader":0,"value":0}`
7 → `{"op":"resolve","loader":0,"value":""}`
8 → `{"op":"resolve","loader":1,"value":1}`
9 → `{"op":"resolve","loader":1,"value":2}`
10 → `{"op":"resolve","loader":1}`
11 → `{"op":"resolve","loader":1,"value":"undefined"}`
12 → `{"op":"resolve","loader":1,"value":null}`
13 → `{"op":"resolve","loader":1,"value":false}`
14 → `{"op":"resolve","loader":1,"value":0}`
15 → `{"op":"resolve","loader":1,"value":""}`
16 → `{"op":"resolve","loader":2,"value":1}`
17 → `{"op":"resolve","loader":2,"value":2}`
18 → `{"op":"resolve","loader":2}`
19 → `{"op":"resolve","loader":2,"value":"undefined"}`
20 → `{"op":"resolve","loader":2,"value":null}`
21 → `{"op":"resolve","loader":2,"value":false}`
22 → `{"op":"resolve","loader":2,"value":0}`
23 → `{"op":"resolve","loader":2,"value":""}`
24 → `{"op":"resolve","loader":3,"value":1}`
25 → `{"op":"resolve","loader":3,"value":2}`
26 → `{"op":"resolve","loader":3}`
27 → `{"op":"resolve","loader":3,"value":"undefined"}`
28 → `{"op":"resolve","loader":3,"value":null}`
29 → `{"op":"resolve","loader":3,"value":false}`
30 → `{"op":"resolve","loader":3,"value":0}`
31 → `{"op":"resolve","loader":3,"value":""}`
32 → `{"op":"resolve","loader":4,"value":1}`
33 → `{"op":"resolve","loader":4,"value":2}`
34 → `{"op":"resolve","loader":4}`
35 → `{"op":"resolve","loader":4,"value":"undefined"}`
36 → `{"op":"resolve","loader":4,"value":null}`
37 → `{"op":"resolve","loader":4,"value":false}`
38 → `{"op":"resolve","loader":4,"value":0}`
39 → `{"op":"resolve","loader":4,"value":""}`
40 → `{"op":"resolve","loader":5,"value":1}`
41 → `{"op":"resolve","loader":5,"value":2}`
42 → `{"op":"resolve","loader":5}`
43 → `{"op":"resolve","loader":5,"value":"undefined"}`
44 → `{"op":"resolve","loader":5,"value":null}`
45 → `{"op":"resolve","loader":5,"value":false}`
46 → `{"op":"resolve","loader":5,"value":0}`
47 → `{"op":"resolve","loader":5,"value":""}`
48 → `{"op":"resolve","loader":6,"value":1}`
49 → `{"op":"resolve","loader":6,"value":2}`
50 → `{"op":"resolve","loader":6}`
51 → `{"op":"resolve","loader":6,"value":"undefined"}`
52 → `{"op":"resolve","loader":6,"value":null}`
53 → `{"op":"resolve","loader":6,"value":false}`
54 → `{"op":"resolve","loader":6,"value":0}`
55 → `{"op":"resolve","loader":6,"value":""}`
56 → `{"op":"resolve","loader":7,"value":1}`
57 → `{"op":"resolve","loader":7,"value":2}`
58 → `{"op":"resolve","loader":7}`
59 → `{"op":"resolve","loader":7,"value":"undefined"}`
60 → `{"op":"resolve","loader":7,"value":null}`
61 → `{"op":"resolve","loader":7,"value":false}`
62 → `{"op":"resolve","loader":7,"value":0}`
63 → `{"op":"resolve","loader":7,"value":""}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+
+## shadow-layers
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-shadow-layers-conformance.qnt](../models/dialcache-shadow-layers-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [shadow-layers-smoke.itf.json](./shadow-layers-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 256 sampled histories of at most 60 steps from 1024 samples; 13 scheduled invariants; 26 exported regressions |
+| Required witnesses | 22 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+`{"policy":{"requestLocal":true,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":100,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":100}},"tracked":true,"fallbackTimeoutMs":null,"readTimeoutMs":120000,"shadowMaxInFlight":2,"recovery":"allow","probeSourceScope":true}`
+
+### Setup commands
+
+- `{"op":"openScope","id":"0","instance":"0"}`
+- `{"op":"openScope","id":"1","instance":"0"}`
+- `{"op":"openScope","id":"2","instance":"1"}`
+- `{"op":"faults","value":{"holdDumps":true,"holdWrites":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0..14 | 0 → `{"op":"begin","key":"0","useCase":"ShadowLayers","scope":"0"}`
1 → `{"op":"begin","key":"1","useCase":"ShadowLayers","scope":"0"}`
2 → `{"op":"begin","key":"2","useCase":"ShadowLayers","scope":"0"}`
3 → `{"op":"begin","key":"0","useCase":"ShadowLayers","scope":"1"}`
4 → `{"op":"begin","key":"1","useCase":"ShadowLayers","scope":"1"}`
5 → `{"op":"begin","key":"2","useCase":"ShadowLayers","scope":"1"}`
6 → `{"op":"begin","key":"0","useCase":"ShadowLayers","scope":"2"}`
7 → `{"op":"begin","key":"1","useCase":"ShadowLayers","scope":"2"}`
8 → `{"op":"begin","key":"2","useCase":"ShadowLayers","scope":"2"}`
9 → `{"op":"begin","key":"0","useCase":"ShadowLayers","instance":"0"}`
10 → `{"op":"begin","key":"1","useCase":"ShadowLayers","instance":"0"}`
11 → `{"op":"begin","key":"2","useCase":"ShadowLayers","instance":"0"}`
12 → `{"op":"begin","key":"0","useCase":"ShadowLayers","instance":"1"}`
13 → `{"op":"begin","key":"1","useCase":"ShadowLayers","instance":"1"}`
14 → `{"op":"begin","key":"2","useCase":"ShadowLayers","instance":"1"}` |
+| `resolveLoader` | 1..48 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":1,"value":1}`
4 → `{"op":"resolve","loader":1,"value":2}`
5 → `{"op":"resolve","loader":2,"value":1}`
6 → `{"op":"resolve","loader":2,"value":2}`
7 → `{"op":"resolve","loader":3,"value":1}`
8 → `{"op":"resolve","loader":3,"value":2}`
9 → `{"op":"resolve","loader":4,"value":1}`
10 → `{"op":"resolve","loader":4,"value":2}`
11 → `{"op":"resolve","loader":5,"value":1}`
12 → `{"op":"resolve","loader":5,"value":2}`
13 → `{"op":"resolve","loader":6,"value":1}`
14 → `{"op":"resolve","loader":6,"value":2}`
15 → `{"op":"resolve","loader":7,"value":1}`
16 → `{"op":"resolve","loader":7,"value":2}`
17 → `{"op":"resolve","loader":8,"value":1}`
18 → `{"op":"resolve","loader":8,"value":2}`
19 → `{"op":"resolve","loader":9,"value":1}`
20 → `{"op":"resolve","loader":9,"value":2}`
21 → `{"op":"resolve","loader":10,"value":1}`
22 → `{"op":"resolve","loader":10,"value":2}`
23 → `{"op":"resolve","loader":11,"value":1}`
24 → `{"op":"resolve","loader":11,"value":2}`
25 → `{"op":"resolve","loader":12,"value":1}`
26 → `{"op":"resolve","loader":12,"value":2}`
27 → `{"op":"resolve","loader":13,"value":1}`
28 → `{"op":"resolve","loader":13,"value":2}`
29 → `{"op":"resolve","loader":14,"value":1}`
30 → `{"op":"resolve","loader":14,"value":2}`
31 → `{"op":"resolve","loader":15,"value":1}`
32 → `{"op":"resolve","loader":15,"value":2}`
33 → `{"op":"resolve","loader":16,"value":1}`
34 → `{"op":"resolve","loader":16,"value":2}`
35 → `{"op":"resolve","loader":17,"value":1}`
36 → `{"op":"resolve","loader":17,"value":2}`
37 → `{"op":"resolve","loader":18,"value":1}`
38 → `{"op":"resolve","loader":18,"value":2}`
39 → `{"op":"resolve","loader":19,"value":1}`
40 → `{"op":"resolve","loader":19,"value":2}`
41 → `{"op":"resolve","loader":20,"value":1}`
42 → `{"op":"resolve","loader":20,"value":2}`
43 → `{"op":"resolve","loader":21,"value":1}`
44 → `{"op":"resolve","loader":21,"value":2}`
45 → `{"op":"resolve","loader":22,"value":1}`
46 → `{"op":"resolve","loader":22,"value":2}`
47 → `{"op":"resolve","loader":23,"value":1}`
48 → `{"op":"resolve","loader":23,"value":2}` |
+| `rejectLoader` | 0..23 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
… one more per choice …
22 → `{"op":"reject","loader":22}`
23 → `{"op":"reject","loader":23}` |
+| `rejectTimeout` | 0..23 | 0 → `{"op":"reject","loader":0,"error":"timeout"}`
1 → `{"op":"reject","loader":1,"error":"timeout"}`
2 → `{"op":"reject","loader":2,"error":"timeout"}`
3 → `{"op":"reject","loader":3,"error":"timeout"}`
4 → `{"op":"reject","loader":4,"error":"timeout"}`
5 → `{"op":"reject","loader":5,"error":"timeout"}`
… one more per choice …
22 → `{"op":"reject","loader":22,"error":"timeout"}`
23 → `{"op":"reject","loader":23,"error":"timeout"}` |
+| `releaseDump` | 0..23 | 0 → `{"op":"release","effect":"dump","index":0}`
1 → `{"op":"release","effect":"dump","index":1}`
2 → `{"op":"release","effect":"dump","index":2}`
3 → `{"op":"release","effect":"dump","index":3}`
4 → `{"op":"release","effect":"dump","index":4}`
5 → `{"op":"release","effect":"dump","index":5}`
… one more per choice …
22 → `{"op":"release","effect":"dump","index":22}`
23 → `{"op":"release","effect":"dump","index":23}` |
+| `releaseWrite` | 0..23 | 0 → `{"op":"release","effect":"write","index":0}`
1 → `{"op":"release","effect":"write","index":1}`
2 → `{"op":"release","effect":"write","index":2}`
3 → `{"op":"release","effect":"write","index":3}`
4 → `{"op":"release","effect":"write","index":4}`
5 → `{"op":"release","effect":"write","index":5}`
… one more per choice …
22 → `{"op":"release","effect":"write","index":22}`
23 → `{"op":"release","effect":"write","index":23}` |
+| `advance` | 1, 60000, 120000 | 1 → `{"op":"advance","ms":1}`
60000 → `{"op":"advance","ms":60000}`
120000 → `{"op":"advance","ms":120000}` |
+| `policy` | 0..13 | 0 → `{"op":"policy","value":{"requestLocal":true,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":100,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":100}}}`
1 → `{"op":"policy","value":{"requestLocal":true,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":100}}}`
2 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":100,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":100}}}`
3 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":100}}}`
4 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":100},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":100}}}`
5 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":100},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":0}}}`
6 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":0}}}`
7 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":100,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":101}}}`
8 → `{"op":"policy","value":{"requestLocal":true,"coalesce":false,"ttlSec":{"local":60,"remote":120},"ramp":{"local":100,"remote":0},"staleOnErrorMaxAgeSec":180,"shadow":{"ramp":100}}}`
9 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":74.59508266765624}}}`
10 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":74.59508269093931}}}`
11 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":0},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":74.59508271422237}}}`
12 → `{"op":"policy","value":{"requestLocal":true,"coalesce":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":100,"remote":100},"staleOnErrorMaxAgeSec":120,"shadow":{"ramp":100}}}`
13 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":120},"ramp":{"local":0,"remote":100},"staleOnErrorMaxAgeSec":180,"shadow":{"ramp":0}}}` |
+| `seed` | 0..11 | 0 → `{"op":"seed","key":"0","useCase":"ShadowLayers","value":1,"ageMs":0,"ttlMs":180000}`
1 → `{"op":"seed","key":"0","useCase":"ShadowLayers","value":2,"ageMs":0,"ttlMs":180000}`
2 → `{"op":"seed","key":"0","useCase":"ShadowLayers","value":1,"ageMs":59999,"ttlMs":180000}`
3 → `{"op":"seed","key":"0","useCase":"ShadowLayers","value":1,"ageMs":60000,"ttlMs":180000}`
4 → `{"op":"seed","key":"1","useCase":"ShadowLayers","value":1,"ageMs":0,"ttlMs":180000}`
5 → `{"op":"seed","key":"1","useCase":"ShadowLayers","value":2,"ageMs":0,"ttlMs":180000}`
6 → `{"op":"seed","key":"1","useCase":"ShadowLayers","value":1,"ageMs":59999,"ttlMs":180000}`
7 → `{"op":"seed","key":"1","useCase":"ShadowLayers","value":1,"ageMs":60000,"ttlMs":180000}`
8 → `{"op":"seed","key":"2","useCase":"ShadowLayers","value":1,"ageMs":0,"ttlMs":180000}`
9 → `{"op":"seed","key":"2","useCase":"ShadowLayers","value":2,"ageMs":0,"ttlMs":180000}`
10 → `{"op":"seed","key":"2","useCase":"ShadowLayers","value":1,"ageMs":59999,"ttlMs":180000}`
11 → `{"op":"seed","key":"2","useCase":"ShadowLayers","value":1,"ageMs":60000,"ttlMs":180000}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+
+## local-clock
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-local-clock-conformance.qnt](../models/dialcache-local-clock-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [local-clock-smoke.itf.json](./local-clock-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 128 sampled histories of at most 40 steps from 512 samples; 4 scheduled invariants; 4 exported regressions |
+| Required witnesses | 2 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+The coordinator sends an empty fixture; see [local-clock.mjs](../replay/local-clock.mjs) for what the driver constructs.
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `constructInstance` | 0, 1 | 0 → `[{"op":"constructInstance","instance":0}]`
1 → `[{"op":"constructInstance","instance":1}]` |
+| `advanceTicks` | 1, 100, 300, 400, 700, 999200, 999999, 1000000 | 1 → `[{"op":"advanceTicks","ticks":1}]`
100 → `[{"op":"advanceTicks","ticks":100}]`
300 → `[{"op":"advanceTicks","ticks":300}]`
400 → `[{"op":"advanceTicks","ticks":400}]`
700 → `[{"op":"advanceTicks","ticks":700}]`
999200 → `[{"op":"advanceTicks","ticks":999200}]`
999999 → `[{"op":"advanceTicks","ticks":999999}]`
1000000 → `[{"op":"advanceTicks","ticks":1000000}]` |
+| `call` | 0..3 | 0 → `[{"op":"call","instance":0,"offered":1}]`
1 → `[{"op":"call","instance":0,"offered":2}]`
2 → `[{"op":"call","instance":1,"offered":1}]`
3 → `[{"op":"call","instance":1,"offered":2}]` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+
+## source-budgets
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-source-budgets-conformance.qnt](../models/dialcache-source-budgets-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [source-budgets-smoke.itf.json](./source-budgets-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 256 sampled histories of at most 60 steps from 1024 samples; 6 scheduled invariants; 10 exported regressions |
+| Required witnesses | 7 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture, by init choice
+
+| Init choice | Fixture |
+| --- | --- |
+| 0 | `{"policy":{"ttlSec":{"local":1}},"tracked":true,"remote":false,"fallbackTimeoutMs":"default"}` |
+| 1 | `{"policy":{"ttlSec":{"local":1}},"tracked":true,"remote":false,"fallbackTimeoutMs":null}` |
+| 2 | `{"policy":{"ttlSec":{"local":1}},"tracked":true,"remote":false,"fallbackTimeoutMs":10}` |
+
+### Setup commands
+
+- `{"op":"faults","value":{"holdPolicies":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0..3 | 0 → `{"op":"begin"}`
1 → `{"op":"begin","outside":true}`
2 → `{"op":"begin","key":"{invalid}"}`
3 → `{"op":"begin","outside":true,"key":"{invalid}"}` |
+| `releasePolicy` | 0..7 | 0 → `{"op":"release","effect":"policy","index":0}`
1 → `{"op":"release","effect":"policy","index":1}`
2 → `{"op":"release","effect":"policy","index":2}`
3 → `{"op":"release","effect":"policy","index":3}`
4 → `{"op":"release","effect":"policy","index":4}`
5 → `{"op":"release","effect":"policy","index":5}`
6 → `{"op":"release","effect":"policy","index":6}`
7 → `{"op":"release","effect":"policy","index":7}` |
+| `resolveLoader` | 1..16 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":1,"value":1}`
4 → `{"op":"resolve","loader":1,"value":2}`
5 → `{"op":"resolve","loader":2,"value":1}`
6 → `{"op":"resolve","loader":2,"value":2}`
7 → `{"op":"resolve","loader":3,"value":1}`
8 → `{"op":"resolve","loader":3,"value":2}`
9 → `{"op":"resolve","loader":4,"value":1}`
10 → `{"op":"resolve","loader":4,"value":2}`
11 → `{"op":"resolve","loader":5,"value":1}`
12 → `{"op":"resolve","loader":5,"value":2}`
13 → `{"op":"resolve","loader":6,"value":1}`
14 → `{"op":"resolve","loader":6,"value":2}`
15 → `{"op":"resolve","loader":7,"value":1}`
16 → `{"op":"resolve","loader":7,"value":2}` |
+| `rejectLoader` | 0..7 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
6 → `{"op":"reject","loader":6}`
7 → `{"op":"reject","loader":7}` |
+| `advance` | 1, 3, 6, 9, 10, 100, 59999, 60001 | 1 → `{"op":"advance","ms":1}`
3 → `{"op":"advance","ms":3}`
6 → `{"op":"advance","ms":6}`
9 → `{"op":"advance","ms":9}`
10 → `{"op":"advance","ms":10}`
100 → `{"op":"advance","ms":100}`
59999 → `{"op":"advance","ms":59999}`
60001 → `{"op":"advance","ms":60001}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+
+## dark-layers
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-dark-layers-conformance.qnt](../models/dialcache-dark-layers-conformance.qnt) |
+| Version | 2, inputs `explicit-v1` |
+| Smoke trace | [dark-layers-smoke.itf.json](./dark-layers-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 256 sampled histories of at most 60 steps from 1024 samples; 24 scheduled invariants; 29 exported regressions |
+| Required witnesses | 48 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+`{"policy":{"requestLocal":true,"coalesce":true,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"ramp":{"local":100,"remote":0},"shadow":{"ramp":100}},"tracked":true,"fallbackTimeoutMs":10,"readTimeoutMs":30000000,"shadowMaxInFlight":1,"recovery":"allow","probeSourceScope":true,"observe":["shadowAge","futureOffset","coalesced","error","coalescingState"]}`
+
+### Setup commands
+
+- `{"op":"openScope","id":"0","instance":"0"}`
+- `{"op":"openScope","id":"1","instance":"0"}`
+- `{"op":"openScope","id":"2","instance":"1"}`
+- `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0..9 | 0 → `{"op":"begin","key":"0","useCase":"DarkLayers","scope":"0"}`
1 → `{"op":"begin","key":"1","useCase":"DarkLayers","scope":"0"}`
2 → `{"op":"begin","key":"0","useCase":"DarkLayers","scope":"1"}`
3 → `{"op":"begin","key":"1","useCase":"DarkLayers","scope":"1"}`
4 → `{"op":"begin","key":"0","useCase":"DarkLayers","scope":"2"}`
5 → `{"op":"begin","key":"1","useCase":"DarkLayers","scope":"2"}`
6 → `{"op":"begin","key":"0","useCase":"DarkLayers","instance":"0"}`
7 → `{"op":"begin","key":"1","useCase":"DarkLayers","instance":"0"}`
8 → `{"op":"begin","key":"0","useCase":"DarkLayers","instance":"1"}`
9 → `{"op":"begin","key":"1","useCase":"DarkLayers","instance":"1"}` |
+| `resolveLoader` | 1..24 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":1,"value":1}`
4 → `{"op":"resolve","loader":1,"value":2}`
5 → `{"op":"resolve","loader":2,"value":1}`
6 → `{"op":"resolve","loader":2,"value":2}`
7 → `{"op":"resolve","loader":3,"value":1}`
8 → `{"op":"resolve","loader":3,"value":2}`
9 → `{"op":"resolve","loader":4,"value":1}`
10 → `{"op":"resolve","loader":4,"value":2}`
11 → `{"op":"resolve","loader":5,"value":1}`
12 → `{"op":"resolve","loader":5,"value":2}`
13 → `{"op":"resolve","loader":6,"value":1}`
14 → `{"op":"resolve","loader":6,"value":2}`
15 → `{"op":"resolve","loader":7,"value":1}`
16 → `{"op":"resolve","loader":7,"value":2}`
17 → `{"op":"resolve","loader":8,"value":1}`
18 → `{"op":"resolve","loader":8,"value":2}`
19 → `{"op":"resolve","loader":9,"value":1}`
20 → `{"op":"resolve","loader":9,"value":2}`
21 → `{"op":"resolve","loader":10,"value":1}`
22 → `{"op":"resolve","loader":10,"value":2}`
23 → `{"op":"resolve","loader":11,"value":1}`
24 → `{"op":"resolve","loader":11,"value":2}` |
+| `rejectLoader` | 0..11 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
6 → `{"op":"reject","loader":6}`
7 → `{"op":"reject","loader":7}`
8 → `{"op":"reject","loader":8}`
9 → `{"op":"reject","loader":9}`
10 → `{"op":"reject","loader":10}`
11 → `{"op":"reject","loader":11}` |
+| `releaseRead` | 0..23 | 0 → `{"op":"release","effect":"read","index":0}`
1 → `{"op":"release","effect":"read","index":1}`
2 → `{"op":"release","effect":"read","index":2}`
3 → `{"op":"release","effect":"read","index":3}`
4 → `{"op":"release","effect":"read","index":4}`
5 → `{"op":"release","effect":"read","index":5}`
… one more per choice …
22 → `{"op":"release","effect":"read","index":22}`
23 → `{"op":"release","effect":"read","index":23}` |
+| `releaseLoad` | 0..23 | 0 → `{"op":"release","effect":"load","index":0}`
1 → `{"op":"release","effect":"load","index":1}`
2 → `{"op":"release","effect":"load","index":2}`
3 → `{"op":"release","effect":"load","index":3}`
4 → `{"op":"release","effect":"load","index":4}`
5 → `{"op":"release","effect":"load","index":5}`
… one more per choice …
22 → `{"op":"release","effect":"load","index":22}`
23 → `{"op":"release","effect":"load","index":23}` |
+| `releaseDump` | 0..23 | 0 → `{"op":"release","effect":"dump","index":0}`
1 → `{"op":"release","effect":"dump","index":1}`
2 → `{"op":"release","effect":"dump","index":2}`
3 → `{"op":"release","effect":"dump","index":3}`
4 → `{"op":"release","effect":"dump","index":4}`
5 → `{"op":"release","effect":"dump","index":5}`
… one more per choice …
22 → `{"op":"release","effect":"dump","index":22}`
23 → `{"op":"release","effect":"dump","index":23}` |
+| `releaseWrite` | 0..23 | 0 → `{"op":"release","effect":"write","index":0}`
1 → `{"op":"release","effect":"write","index":1}`
2 → `{"op":"release","effect":"write","index":2}`
3 → `{"op":"release","effect":"write","index":3}`
4 → `{"op":"release","effect":"write","index":4}`
5 → `{"op":"release","effect":"write","index":5}`
… one more per choice …
22 → `{"op":"release","effect":"write","index":22}`
23 → `{"op":"release","effect":"write","index":23}` |
+| `advance` | 1, 10, 60000 | 1 → `{"op":"advance","ms":1}`
10 → `{"op":"advance","ms":10}`
60000 → `{"op":"advance","ms":60000}` |
+| `policy` | 0..8 | 0 → `{"op":"policy","value":{"requestLocal":true,"coalesce":true,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"ramp":{"local":100,"remote":0},"shadow":{"ramp":100}}}`
1 → `{"op":"policy","value":{"requestLocal":true,"coalesce":true,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"ramp":{"local":0,"remote":0},"shadow":{"ramp":100}}}`
2 → `{"op":"policy","value":{"requestLocal":false,"coalesce":true,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"ramp":{"local":100,"remote":0},"shadow":{"ramp":100}}}`
3 → `{"op":"policy","value":{"requestLocal":false,"coalesce":true,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"ramp":{"local":0,"remote":0},"shadow":{"ramp":100}}}`
4 → `{"op":"policy","value":{"requestLocal":true,"coalesce":false,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"ramp":{"local":100,"remote":0},"shadow":{"ramp":100}}}`
5 → `{"op":"policy","value":{"requestLocal":false,"coalesce":false,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"ramp":{"local":100,"remote":0},"shadow":{"ramp":100}}}`
6 → `{"op":"policy","value":{"requestLocal":true,"coalesce":true,"ttlSec":{"local":60,"remote":60},"staleOnErrorMaxAgeSec":120,"ramp":{"local":100,"remote":0},"shadow":{"ramp":0}}}`
7 → `{"op":"policy","value":{"requestLocal":true,"coalesce":true,"ttlSec":{"local":60,"remote":120},"staleOnErrorMaxAgeSec":180,"ramp":{"local":100,"remote":0},"shadow":{"ramp":100}}}`
8 → `{"op":"policy","value":{"requestLocal":false,"coalesce":true,"ttlSec":{"local":60,"remote":120},"staleOnErrorMaxAgeSec":180,"ramp":{"local":0,"remote":0},"shadow":{"ramp":100}}}` |
+| `seed` | 0..11 | 0 → `{"op":"seed","key":"0","useCase":"DarkLayers","ageMs":0,"ttlMs":180000,"value":1}`
1 → `{"op":"seed","key":"0","useCase":"DarkLayers","ageMs":0,"ttlMs":180000,"value":2}`
2 → `{"op":"seed","key":"0","useCase":"DarkLayers","ageMs":59999,"ttlMs":180000,"value":1}`
3 → `{"op":"seed","key":"0","useCase":"DarkLayers","ageMs":60000,"ttlMs":180000,"value":1}`
4 → `{"op":"seed","key":"0","useCase":"DarkLayers","ageMs":0,"ttlMs":180000,"payloadHex":"016e6f742061207a737464206672616d65"}`
5 → `{"op":"seed","key":"0","useCase":"DarkLayers","ageMs":0,"ttlMs":180000,"frameHex":"010000000000000000ff31"}`
6 → `{"op":"seed","key":"1","useCase":"DarkLayers","ageMs":0,"ttlMs":180000,"value":1}`
7 → `{"op":"seed","key":"1","useCase":"DarkLayers","ageMs":0,"ttlMs":180000,"value":2}`
8 → `{"op":"seed","key":"1","useCase":"DarkLayers","ageMs":59999,"ttlMs":180000,"value":1}`
9 → `{"op":"seed","key":"1","useCase":"DarkLayers","ageMs":60000,"ttlMs":180000,"value":1}`
10 → `{"op":"seed","key":"1","useCase":"DarkLayers","ageMs":0,"ttlMs":180000,"payloadHex":"016e6f742061207a737464206672616d65"}`
11 → `{"op":"seed","key":"1","useCase":"DarkLayers","ageMs":0,"ttlMs":180000,"frameHex":"010000000000000000ff31"}`
choices 5, 11 read `environment.wallMs` (the environment value at the step; shown as 0) |
+| `invalidate` | 0..3 | 0 → `{"op":"invalidate","key":"0","futureBufferMs":0}`
1 → `{"op":"invalidate","key":"0","futureBufferMs":20}`
2 → `{"op":"invalidate","key":"1","futureBufferMs":0}`
3 → `{"op":"invalidate","key":"1","futureBufferMs":20}` |
+| `closeScope` | 0..2 | 0 → `{"op":"closeScope","id":"0"}`
1 → `{"op":"closeScope","id":"1"}`
2 → `{"op":"closeScope","id":"2"}` |
+| `inspect` | 0, 1 | 0 → `{"op":"inspectCoalescing","instance":"0"}`
1 → `{"op":"inspectCoalescing","instance":"1"}` |
+| `rollbackWall` | none | `{"op":"shiftWall","ms":-1000}` |
+| `readFault` | 0, 1 | 0 → `{"op":"faults","value":{"read":false}}`
1 → `{"op":"faults","value":{"read":true}}` |
+| `loadFault` | 0, 1 | 0 → `{"op":"faults","value":{"load":false}}`
1 → `{"op":"faults","value":{"load":true}}` |
+| `dumpFault` | 0, 1 | 0 → `{"op":"faults","value":{"dump":false}}`
1 → `{"op":"faults","value":{"dump":true}}` |
+| `writeFault` | 0, 1 | 0 → `{"op":"faults","value":{"write":false}}`
1 → `{"op":"faults","value":{"write":true}}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+- `d`: `ages`, `coalesced`, `fallbackErrors`, `warnings`, `configErrors`, `futureOffsets`, `inspections`; diagnostics; ages are the `shadowAge` events.
+
+## shadow-read-deadlines
+
+| | |
+| --- | --- |
+| Model | [formal/models/dialcache-shadow-read-deadlines-conformance.qnt](../models/dialcache-shadow-read-deadlines-conformance.qnt) |
+| Version | 1, inputs `explicit-v1` |
+| Smoke trace | [shadow-read-deadlines-smoke.itf.json](./shadow-read-deadlines-smoke.itf.json) |
+| Ports claiming it | typescript, go, rust, python |
+| Generation | 128 sampled histories of at most 40 steps from 1024 samples; 6 scheduled invariants; 6 exported regressions |
+| Required witnesses | 6 labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |
+
+### Fixture
+
+`{"policy":{"requestLocal":false,"ttlSec":{"local":60,"remote":60},"ramp":{"local":0,"remote":0},"shadow":{"ramp":100}},"tracked":true,"fallbackTimeoutMs":10,"readTimeoutMs":5,"shadowMaxInFlight":1,"probeSourceScope":true,"observe":["shadowAge","futureOffset","coalesced","error","readContext","readAbort"]}`
+
+### Setup commands
+
+- `{"op":"faults","value":{"holdReads":true,"holdLoads":true,"holdDumps":true,"holdWrites":true}}`
+
+### Actions
+
+| Action | Choices | Driver commands |
+| --- | --- | --- |
+| `beginCall` | 0, 1 | 0 → `{"op":"begin","key":"0"}`
1 → `{"op":"begin","key":"1"}` |
+| `resolveLoader` | 1..16 | 1 → `{"op":"resolve","loader":0,"value":1}`
2 → `{"op":"resolve","loader":0,"value":2}`
3 → `{"op":"resolve","loader":1,"value":1}`
4 → `{"op":"resolve","loader":1,"value":2}`
5 → `{"op":"resolve","loader":2,"value":1}`
6 → `{"op":"resolve","loader":2,"value":2}`
7 → `{"op":"resolve","loader":3,"value":1}`
8 → `{"op":"resolve","loader":3,"value":2}`
9 → `{"op":"resolve","loader":4,"value":1}`
10 → `{"op":"resolve","loader":4,"value":2}`
11 → `{"op":"resolve","loader":5,"value":1}`
12 → `{"op":"resolve","loader":5,"value":2}`
13 → `{"op":"resolve","loader":6,"value":1}`
14 → `{"op":"resolve","loader":6,"value":2}`
15 → `{"op":"resolve","loader":7,"value":1}`
16 → `{"op":"resolve","loader":7,"value":2}` |
+| `rejectLoader` | 0..7 | 0 → `{"op":"reject","loader":0}`
1 → `{"op":"reject","loader":1}`
2 → `{"op":"reject","loader":2}`
3 → `{"op":"reject","loader":3}`
4 → `{"op":"reject","loader":4}`
5 → `{"op":"reject","loader":5}`
6 → `{"op":"reject","loader":6}`
7 → `{"op":"reject","loader":7}` |
+| `releaseRead` | 0..15 | 0 → `{"op":"release","effect":"read","index":0}`
1 → `{"op":"release","effect":"read","index":1}`
2 → `{"op":"release","effect":"read","index":2}`
3 → `{"op":"release","effect":"read","index":3}`
4 → `{"op":"release","effect":"read","index":4}`
5 → `{"op":"release","effect":"read","index":5}`
… one more per choice …
14 → `{"op":"release","effect":"read","index":14}`
15 → `{"op":"release","effect":"read","index":15}` |
+| `releaseLoad` | 0..15 | 0 → `{"op":"release","effect":"load","index":0}`
1 → `{"op":"release","effect":"load","index":1}`
2 → `{"op":"release","effect":"load","index":2}`
3 → `{"op":"release","effect":"load","index":3}`
4 → `{"op":"release","effect":"load","index":4}`
5 → `{"op":"release","effect":"load","index":5}`
… one more per choice …
14 → `{"op":"release","effect":"load","index":14}`
15 → `{"op":"release","effect":"load","index":15}` |
+| `releaseDump` | 0..15 | 0 → `{"op":"release","effect":"dump","index":0}`
1 → `{"op":"release","effect":"dump","index":1}`
2 → `{"op":"release","effect":"dump","index":2}`
3 → `{"op":"release","effect":"dump","index":3}`
4 → `{"op":"release","effect":"dump","index":4}`
5 → `{"op":"release","effect":"dump","index":5}`
… one more per choice …
14 → `{"op":"release","effect":"dump","index":14}`
15 → `{"op":"release","effect":"dump","index":15}` |
+| `releaseWrite` | 0..15 | 0 → `{"op":"release","effect":"write","index":0}`
1 → `{"op":"release","effect":"write","index":1}`
2 → `{"op":"release","effect":"write","index":2}`
3 → `{"op":"release","effect":"write","index":3}`
4 → `{"op":"release","effect":"write","index":4}`
5 → `{"op":"release","effect":"write","index":5}`
… one more per choice …
14 → `{"op":"release","effect":"write","index":14}`
15 → `{"op":"release","effect":"write","index":15}` |
+| `advance` | 1, 4, 5, 10, 20 | 1 → `{"op":"advance","ms":1}`
4 → `{"op":"advance","ms":4}`
5 → `{"op":"advance","ms":5}`
10 → `{"op":"advance","ms":10}`
20 → `{"op":"advance","ms":20}` |
+| `policy` | 5, 20 | 5 → `{"op":"policy","value":{"remoteReadTimeoutMs":5}}`
20 → `{"op":"policy","value":{"remoteReadTimeoutMs":20}}` |
+| `seed` | 0..3 | 0 → `{"op":"seed","key":"0","value":1,"ttlMs":60000}`
1 → `{"op":"seed","key":"0","value":2,"ttlMs":60000}`
2 → `{"op":"seed","key":"1","value":1,"ttlMs":60000}`
3 → `{"op":"seed","key":"1","value":2,"ttlMs":60000}` |
+
+### Observation channels
+
+- `o`: `calls`, `loaders`, `reads`, `writes`, `invalidations`, `maintenance`, `loads`, `dumps`, `policyCalls`, `classifications`, `comparisons`, `sourceScopes`, `writeTtls`, `shadow`, `recovery`; the shared observation record.
+- `io`: `budgets`, `aborted`, `sourceErrors`; read budgets in dispatch order, aborted read indices, each caller's source-error identity.
+- `d`: `ages`, `coalesced`, `fallbackErrors`, `warnings`, `configErrors`, `futureOffsets`; diagnostics; ages are the `shadowAge` events.
diff --git a/formal/generated/README.md b/formal/generated/README.md
index 2d79d8de..5fe83730 100644
--- a/formal/generated/README.md
+++ b/formal/generated/README.md
@@ -6,16 +6,20 @@ Never edit a file in this directory; regenerate it.
- `-smoke.itf.json` (17 files): one named history per conformance profile, the committed smoke trace every port's smoke lane replays; written by `generated-fixtures.mjs` from [../catalogs/fixture-recipes.json](../catalogs/fixture-recipes.json).
- `generated-fixtures.lock.json`: the pinned input hashes (models, recipes, generators) and output hashes of every committed fixture, including the witness fixtures under `typescript/test/fixtures/`; written in the same pass.
- `quint-key-vectors.json`, `quint-frame-vectors.json`, `quint-envelope-vectors.json`, `quint-invalidation-vectors.json`: the generated wire vectors, one per wire model, with the generator's own source hash in their provenance; written by the `generate-*-vectors.mjs` scripts.
+- `PROFILES.md`: the read view of every conformance profile (fixture, setup, each action's choice decodings into driver commands, observation channels), rendered from the replay descriptors, the catalogs and each model's public runs by `node formal/tools/generate-catalog-docs.mjs --write`; `make audit` fails when it is stale.
-Regenerate everything with Quint 0.32.0 on `PATH`:
+Regenerate the Quint artifacts (traces, lock, vectors) with Quint 0.32.0 on
+`PATH`, and the read views without Quint:
```sh
node formal/tools/generate-artifacts.mjs --write
+node formal/tools/generate-catalog-docs.mjs --write
```
`make fixtures-check` (`node formal/tools/generate-artifacts.mjs --check`)
-recomputes every artifact and fails on any difference; the ordinary TypeScript
-suite also verifies the lock against the committed files without Quint. The
-pull request lane regenerates these files only when an input they declare
-changed (`.github/scripts/fixture-scope.mjs`). GitHub renders the directory as
+recomputes every Quint artifact and fails on any difference; the ordinary
+TypeScript suite also verifies the lock against the committed files without
+Quint. `make audit` checks the read views the same way. The pull request lane
+regenerates the Quint artifacts only when an input they declare changed
+(`.github/scripts/fixture-scope.mjs`). GitHub renders the directory as
generated.
diff --git a/formal/generated/generated-fixtures.lock.json b/formal/generated/generated-fixtures.lock.json
index d0635252..3e63853c 100644
--- a/formal/generated/generated-fixtures.lock.json
+++ b/formal/generated/generated-fixtures.lock.json
@@ -11,20 +11,20 @@
"formal/models/cache-rules.qnt": "ae2a1748e911402c6818e8294265764e06d18d050a89219df7d55faa83fb06e5",
"formal/models/cohort-boundaries.qnt": "700f0b9ee734f2511b3c7f10138b9636cef93bc1045b653479a05be1766e3407",
"formal/models/conformance-observations.qnt": "76e26fb0c5802a13c63f0819071b5326b1586cab187c73d8b204ec7da70f5c2f",
- "formal/models/dialcache-admission-conformance.qnt": "928b8bd5d566d39c656bfdd3e7e9af0dae975f1b840b67d2ada76d2ccd39c10c",
+ "formal/models/dialcache-admission-conformance.qnt": "08ca435b9f3c200c2386a2ce2da7fd0651bd0f8d24f02083242f3674e1db60de",
"formal/models/dialcache-conformance.qnt": "3e91cad0afa6ba44353d651078fdf6284df0354ca82de0e3712dfe4f243244d7",
"formal/models/dialcache-dark-layers-conformance.qnt": "e9ffc9133a6a1b641aff31123b48799273d64bd5596f0c504879d3eb085a2e12",
- "formal/models/dialcache-effects-conformance.qnt": "a47ad34f9e985749e2658bd7c2da00f6995e65a94e51febd0ad0b6ff1f3fc074",
- "formal/models/dialcache-independent-conformance.qnt": "dd8734b02512a8dc0c65a0604b3dad10bed3d0f2a91e0246d5379c3807191639",
+ "formal/models/dialcache-effects-conformance.qnt": "34f7b08029304a0a499219bb8dbc3fc19982c0d5ba9f073cfc806e1c73aba24c",
+ "formal/models/dialcache-independent-conformance.qnt": "948dda299145fd5afd179f2ce6b98c17aa3796a88ff90dc7c44da8f437c1ca50",
"formal/models/dialcache-layers-conformance.qnt": "c596ae3e8d4a10d4eb9b696ad8ed93b4d4f7f9bbf234ad7ab29016d411a8538e",
"formal/models/dialcache-local-clock-conformance.qnt": "ed326ad6e5a8701e5b3eeb5cb313e429517f54c58e3d1fc5aecc3cada508dfaa",
"formal/models/dialcache-local-failure-conformance.qnt": "ae1152dd94f4355bebe9b2c000d9b74ef46b86c3052cc9ddf221a4b550e3e24b",
"formal/models/dialcache-policy-conformance.qnt": "423fcfae91e0adbe2a18e968ddd1d30569a63077cc2bd283092ebe921954ff7c",
- "formal/models/dialcache-recovery-conformance.qnt": "efe86fa2358e5843f015ebbcdeb7444b5c4ce489f870acbaac29f454b84329c4",
+ "formal/models/dialcache-recovery-conformance.qnt": "f15dec6366ce622d175fcf9cc8506b34197c06353fc5cbc8967668002ac33424",
"formal/models/dialcache-recovery-read-conformance.qnt": "199bc6c93d74d228c4df500eda8d838970670cb038ba396838d9ba59690d7434",
"formal/models/dialcache-runtime-boundaries-conformance.qnt": "dc761bf9cf65b91382477ead6d2596582089512c0405300e813ab6c909079c96",
"formal/models/dialcache-scope-conformance.qnt": "1f8817b882b5f8c4d37aecf82d2b4ae1f87f1dc5fd55bfdd94bf4841b6b1fddd",
- "formal/models/dialcache-shadow-conformance.qnt": "32158eb0d6cc81901d1107b553aeab56baeebe767e5e1c3099790b3f3fdca4ac",
+ "formal/models/dialcache-shadow-conformance.qnt": "8fcb59b1012f203f8248cdab095cfc3c25f0860715b1b44c3fc0ffbfed4510a6",
"formal/models/dialcache-shadow-layers-conformance.qnt": "d778c8e4efd2f62e33de17e8739bf3d49d426b8b47e2a129056d8a485db9aff7",
"formal/models/dialcache-shadow-read-deadlines-conformance.qnt": "b43373789a9cbfd907b50c5ebb49dec738e3621eab8132d16a4101634ed0d9f2",
"formal/models/dialcache-source-budgets-conformance.qnt": "d2e01cc2cf6caed229e289c727a2bbc7e99b7d9557a9e94223cc399732dd20b1",
diff --git a/formal/guides/AUTHORING.md b/formal/guides/AUTHORING.md
index 9f44293e..8dc4fd00 100644
--- a/formal/guides/AUTHORING.md
+++ b/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
diff --git a/formal/guides/BEHAVIOR.md b/formal/guides/BEHAVIOR.md
index 3d0b36bf..575c6c52 100644
--- a/formal/guides/BEHAVIOR.md
+++ b/formal/guides/BEHAVIOR.md
@@ -1,8 +1,8 @@
-# Portable behavioral scenarios and generated feature profiles
+# Portable behavioral scenarios and generated profiles
[`behavioral-scenarios.json`](../catalogs/behavioral-scenarios.json) specifies deterministic feature scenarios independently of TypeScript. [`dialcache-effects-conformance.qnt`](../models/dialcache-effects-conformance.qnt) generates additional races using the same driver operations. Together with the [core profile](./CONFORMANCE.md) and [protocol vectors](../catalogs/protocol-vectors.json), these are executable contracts for implementation tests and language ports. The core profile is the introductory one and stays uncomposed from the kernel library: its drivers read the model's private state fields as their observation, so composing it is a driver-contract change in both ports.
-The deterministic corpus currently contains 244 scenarios across 12 behavior families. It includes request-scope lifetime, coalescing, both read and fallback deadlines, local TTL/LRU, runtime snapshots, layer precedence, cache failures, tracked invalidation, frame age/retention, stale recovery, and shadow validation. These scenarios are test-derived contracts, **not Quint-generated traces**. The effects model generates interleavings of calls, loader settlement, clock observations, native writes, and invalidation. Recovery, policy, and shadow models generate further feature schedules through the same driver; their bounds and action mappings appear below. Keeping these complementary forms avoids a single model containing every feature combination. The [feature map](./FEATURE-COVERAGE.md) relates the scenarios to the full reviewed behavioral, protocol, and native inventory.
+The deterministic corpus currently contains 244 scenarios across 12 behavior families. It includes request-scope lifetime, coalescing, both read and fallback deadlines, local TTL/LRU, runtime snapshots, layer precedence, cache failures, tracked invalidation, frame age/retention, stale recovery, and shadow validation. These scenarios are test-derived contracts, **not Quint-generated traces**. The effects model generates interleavings of calls, loader settlement, clock observations, native writes, and invalidation. Recovery, policy, and shadow models generate further feature schedules through the same driver; their bounds and action mappings are generated into [PROFILES.md](../generated/PROFILES.md). Keeping these complementary forms avoids a single model containing every feature combination. The [feature map](./FEATURE-COVERAGE.md) relates the scenarios to the full reviewed behavioral, protocol, and native inventory.
The corpus includes interaction regressions for scope closure during recovery, runtime coalescing changes during an active flight, independent retained snapshots, recovery/shadow exclusion, local insertion TTL after an aging remote hit, and shadow capacity ownership. These are fixed portable schedules: they extend implementation conformance without claiming that the generated profiles explore those combinations. The [behavioral evidence map](./TEST-MAP.md#behavioral-map) connects these obligations to implementation tests and the current generated profiles.
@@ -81,12 +81,280 @@ Wall time starts at `2026-09-08T12:00:00Z`; monotonic time starts at zero. Elaps
Only unresolved external operations are gated. A port can use its own executor and explicit request-context handles. It must not reproduce Node Promise turns. The TypeScript driver captures its execution context inside public enable/disable calls; it does not read DialCache's context internals.
+## Observations
+
+- `calls`: every caller, in start order, is `{"status":"pending"}`, `{"status":"value","value":1}`, or `{"status":"error","error":"source:0"}` / `"timeout:0"`. Source IDs identify the original loader error; timeout IDs identify distinct timeout outcomes in observation order. Coalesced followers must receive the same error identity. Ports can compare a shared logical error token without adopting JavaScript object identity.
+- `loaders`, `reads`, `writes`, `invalidations`, `loads`, `dumps`, `policyCalls`: cumulative actual loader, adapter, serializer, and provider invocations. Failed and still-pending attempts count. Value writes and invalidations are separate.
+- `classifications`, `comparisons`: actual invocations of the fixture-owned classifier/comparator. Built-in defaults are not instrumented.
+- `sourceScopes`: actual source-entry enablement observations when the explicit scope probe is enabled; otherwise empty.
+- `writeTtls`: actual requested physical write TTLs in milliseconds, in dispatch order.
+- `maintenance`: public invalidation outcomes, `ok`, `mutation_error`, or `missing_remote`. The last category records the actual public error; a port need not reproduce its native class or text.
+- `shadow`, `recovery`: terminal outcomes from the public diagnostic hooks, in observed order. Exact telemetry timing and ordinary metrics are not asserted.
+
+A returned cache value, loader invocation, or acknowledged write does not prove publication. Subsequent calls test cache retention and invalidation. Negative harness tests deliberately remove recovery, local storage, and acknowledged invalidation and require a later observable divergence.
+
+### Additional fixed-scenario inputs
+
+`adapterReply` stages one JSON-shaped semantic adapter result for the next successful raw-read settlement. Only one result may be staged at a time. The driver supplies it to the real cache at the adapter boundary; it neither decodes it on behalf of DialCache nor records a predicted miss/hit. Existing held reads and read failures remain independent. Tests use invalid replies to check the core's normalization; ports whose adapter type cannot represent malformed replies can enforce that boundary when decoding external input.
+
+`seed.payloadText` supplies exact UTF-8 text serializer bytes; `seed.payloadHex` supplies raw binary serializer/envelope bytes, framed with the current wall timestamp minus `ageMs`. `seed.frameHex` remains a complete frame, including header; ordinary `seed.value` still uses the scalar fixture codec. These inputs change only the fake Redis environment.
+
+## Generated profiles
+
+Every profile is a Quint model whose public actions decode into driver commands;
+the drivers replay its sampled histories and exported regressions, and all but
+`core` compose the kernel library. What a profile's drivers are configured with,
+which commands each recorded action and choice decode into, and which observation
+channels the coordinator compares are generated from the replay descriptors into
+[PROFILES.md](../generated/PROFILES.md), one section per profile. This section keeps
+what those tables do not state: the trace contract, the value codes, the meaning of
+each observation channel, the rules a profile holds its drivers to, what each
+profile leaves to others, and how to replay a generated trace.
+
+### Trace contract
+
+Each ITF state carries the authoritative `input.name` and `input.choice` beside the
+expected state `s`. The choice is a nonnegative ITF integer on actions that have
+choices and `-1` otherwise; optional `mbt::actionTaken` and `mbt::nondetPicks.choice`
+annotations must agree with it, and raw regression exports carry no annotations
+([trace contract](./PORTING.md#trace-and-observation-contract)). The parser rejects
+unknown actions, unsupported choices, missing observation fields and integer
+precision loss. `s.o` and the channels a profile declares (`s.io`, `s.d`, `s.markers`,
+`s.compression`, `s.policyErrors`, the effects `s.events`) are the asserted channels;
+the rest of `s` is the model's private prediction and never enters execution or the
+implementation projection. A driver selects explicit choices for source indices and
+uses its own invocation counts for actions that target the latest effect; it never
+reads expected counters, phases, cached values or fences to select an input or to
+fabricate an observation. Failure actions set a fixture fault, release the selected
+external gate, drain runnable work and restore the fault. A failing replay reports the
+trace, the step, the action and both observations.
+
+### Value codes
+
+Caller observations encode pending as 0, fixture values 1 and 2 as 1 and 2, a source
+error as 3 and a deadline error as 4. Codes 5 to 9 are the absent, `null`, `false`,
+zero and empty-string values the scope and policy profiles generate; 11 is the text
+`"undefined"`, distinct from absent; 10 is invalid. Other outcomes fail replay. The
+generated profiles compare error categories; the fixed scenarios compare logical
+error identity. The effects model keeps the version-2 codes of its own contract, 0
+pending, 1 value, 2 source error and 3 timeout; its composed text records the shared
+codes in `s.o.calls` and the parser maps them, so that observation schema is
+unchanged. Version 3 of effects added the explicit wall-advance domain and the
+last-fresh and exact-expiry adapter-frame histories; the differential records that
+as an intended input-domain expansion.
+
+### Observation channels
+
+- `s.io = { budgets, aborted, sourceErrors }` (independent, recovery-read,
+ shadow-read-deadlines): `budgets` are the actual adapter read budgets in read
+ invocation order, `aborted` the cooperative cancellation indices in delivery order,
+ and `sourceErrors` one entry per caller, zero unless the caller returned its
+ source's ordinary error, otherwise the one-based actual source identity. The driver
+ projects adapter callbacks and returned error tokens; model-private ownership never
+ enters execution. The effects profile asserts `s.o`, `s.io` and `s.events` only,
+ its `io` carrying budgets and aborted reads; asserting `io` with source errors or
+ `d` beside `events` under the shared codes would be a separate observation-schema
+ change.
+- `s.d = { warnings, ages, coalesced, fallbackErrors }` (scope, recovery, shadow,
+ dark-layers, shadow-read-deadlines), with `configErrors` where the profile counts
+ `config_resolution` events carrying the remote, non-fallback labels, `futureOffsets`
+ where it records them, and `inspections` for dark-layers' public process snapshots.
+ Ages are integer milliseconds in Quint and compared with actual callback seconds
+ after unit conversion. Recovery records an age only after a successful retained
+ decode; shadow records the original C0 age at a match or confirmed-mismatch
+ verdict, clamped to zero after a wall rollback, and warns only for a confirmed
+ mismatch whose admitted policy enabled logging. `coalesced` records request or
+ process scope labels; `fallbackErrors` records the layer a failed source is
+ attributed to, failures later recovered as stale included. Scope fixtures assert one
+ trail for shared failures and no cache-error trail for disabled pass-through work.
+ An active local layer attributes its failed source to `local` even inside a request
+ memo; without a shared layer a transient request attributes it to `request_local`;
+ a request that closes while policy is pending attributes to `noop`, and
+ admission-time attribution survives later closure. Exact native JSON warning
+ formatting remains a binding obligation.
+- `s.events` (effects) records `{ event, location, detail, amount }` in order:
+ location is a reached layer or coalescing scope; amount is an integer millisecond
+ measurement (get, fallback, serialization, future offset), a byte size, a
+ write-dispatch index or zero. Replay converts model milliseconds to callback seconds
+ and compares the ordered events, their labels and source-error attribution. A
+ follower emits its coalescing event without repeating the leader's trail; fresh
+ decoding counts in the remote-get duration; source duration ends at accepted
+ settlement or deadline; a dump has its own duration; late sources do not repeat
+ failures; size events precede adapter dispatch even when the write stays pending.
+ Scalar value 1 has one serialized byte here; Unicode and binary byte accounting is
+ covered by the protocol vectors and the fixed scenarios.
+- `s.markers` and `s.compression` (recovery-read) record each observed invalidation
+ marker as `{ cutoffMs, ttlMs }` and each decode's outcome, `decompressed` or
+ `fallback_raw`.
+- `s.policyErrors` (policy) records each configuration error as
+ `{ layer: "noop", errorType: "config_resolution" }`.
+
+### Rules the profiles hold their drivers to
+
+- **effects.** Each history has at most eight callers and eight sources; successful
+ values are 1; no local cache, recovery, shadow work or physical expiry is enabled.
+ Monotonic time and application wall time are separate; `tick` and `jumpClock`
+ advance 10 ms with and without timer delivery, and clock jumps without delivery
+ are generated during 10 ms reads and source-owned phases; read budgets are
+ multiples of the 10 ms step and a budget change affects later reads while followers
+ keep their leader's budget. An `observerFault` fails the diagnostic callbacks and
+ leaves cache outcomes unchanged. A read deadline starts a fresh source budget and
+ suppresses refill; a successful raw read clears that budget before decoding; a
+ failed fresh decode permits refill; an accepted serialization or write outlives the
+ source budget, with the observed fence checked again after preparation. The queued
+ adapter reply classes are, by choice: 1 null, 2 primitive, 3 legacy watermark shape,
+ 4 kindless metadata, 5 missing miss reason, 6 unknown reason, 7 unknown reason with a
+ valid future fence, 8 fenced reason without a fence, 9 negative fence, 10 fractional
+ fence, 11 unsafe fence, 12 absent reason with a future fence, 13 expired reason with
+ a zero fence, 14 miss with stray frame fields, 15 valid frame with stray miss
+ metadata, 16 fenced reason with a valid future fence; future fences are the input
+ wall clock plus 20 ms. A successful raw completion consumes the reply even when
+ DialCache abandoned that read; an adapter failure leaves it queued. A port with typed
+ replies may normalize these encodings at its boundary but must preserve the
+ resulting miss and refill behavior.
+- **recovery.** Contexts 0 and 1 are open in every fixture; request misses may join
+ one process flight, after which each attached open context memoizes the result; a
+ same-request follower records request coalescing, a new request process coalescing,
+ and a `joinCall` into pending shared work can still be won by a preexisting request
+ memo.
+ Recovered values are never published to shared storage. Closing a context clears
+ its memo and prevents late recovery from populating it. Recovery starts at a source
+ deadline reached inside a larger elapsed-time step, and its held decode may
+ complete later; the retained snapshot and source-error identity survive late
+ settlement. Init choices 0 to 3 select the timeout-only default or an instance
+ classifier that allows, denies or throws; 4 to 7 add request-local caching; a
+ call's recovery choice 3 inherits the instance policy and 0 to 2 override it.
+- **policy.** Another invocation is admitted once the preceding provider reply is
+ released, even while its source is pending; sources settle in any order; same-key
+ followers join only while the current policy permits sharing; a shared leader stays
+ registered when an independent source publishes or fails. An overlay replaces the
+ whole runtime overlay and omitted leaves inherit the fixture; choices 10 to 19 are
+ choices 0 to 9 with `coalesce: false`; an invalid remote read budget of 0 bypasses
+ all caching for the invocation; an invalid local or remote ramp of 101 disables
+ that layer and preserves the other; an invalid recovery maximum age of 1 or -1 s
+ leaves normal serving active and writes with the ordinary 1 s retention; an invalid
+ shadow ramp of 101 leaves normal fresh serving active. In policy and recovery, wall
+ time and elapsed time are separate: a local hit survives a rollback before its TTL
+ and expires at that TTL despite it, a future-dated frame is rejected, a retained
+ candidate that a rollback makes future-dated is rejected, physical Redis expiry is
+ independent, and invalidation never lowers a watermark.
+- **shadow.** Payload choices make text and binary share exact UTF-8 bytes while
+ different byte spellings decode to the same value; comparison uses decoded values,
+ confirmation uses bytes, and C1 compares the retained payload identity even when
+ the replacement's timestamp is future-dated; `reencode` replaces the stored bytes
+ with an alternate text or binary form during C1 and records it as an explicit
+ choice, so a driver never consults expected storage; `advanceWall` moves only the
+ application wall clock while C1 is pending, elapsed deadlines and physical Redis
+ expiry standing still. Another call is admitted once the preceding source and owned
+ job work have settled. Fixtures 11 and 12 advance elapsed and wall time by
+ `sourceWorkMs` without delivering timers while the source begins: at 9 ms the dark
+ job still dispatches C0, at exactly 10 ms the job reports timeout without a Redis
+ read while the caller stays pending, and the caller's later settlement or timer
+ gives its deadline error; these fixtures observe after overdue timers are
+ delivered, and intermediate native timer ordering is outside their bounds. Timer
+ delivery is not required for elapsed-time rejection. Malformed logging keeps
+ comparison active with warnings disabled, and a job admitted under it records a
+ configuration error and captures logging off; later runtime changes do not rewrite
+ an admitted job's policy.
+- **admission.** Caller reads and all decoding are held; a successful read acquires
+ C0 and completing its decode considers shadow admission under the flight's accepted
+ policy; coalesced followers share one admission; a detached source runs with caching
+ disabled; an unequal comparison triggers a held C1 read; no shadow action changes a
+ caller result or writes cache values. A whole-job timeout emits one outcome but keeps
+ the slot until its pending source, decode or confirmation read settles; later
+ completion starts no new work and emits no replacement verdict, and once the owned
+ work drains a later hit may admit another job. Two instances with two slots each
+ make a duplicate drop distinguishable from a full instance. At most sixteen calls
+ and sixteen admitted jobs give at most 32 read and 32 decode effects, and elapsed
+ time is bounded to 600 ms so serving reads stay fresh and below their separate
+ deadline. The committed smoke trace keeps the actions, choices and observation
+ records of the first 57 states of a generated history with the model-private fields
+ omitted; the parser replays both forms without special handling.
+- **independent.** Six callers can each own one read, one source and one decode;
+ only raw reads and decoding are held, and accepted publication completes at the
+ source-settlement boundary. Each call captures its own read budget and recovery
+ policy; a read failure or timeout cannot borrow another call's refill authority;
+ each recovery chain retains its own candidate and source error; invalidation cannot
+ revoke an acquired decode or candidate, though recovery still rechecks age around
+ the decode; late settlement of one call never affects another. Deadlines are
+ delivered in time order, registration order at equal instants, new deadlines reached
+ within the advance included; other runtimes need not use the same timer
+ implementation.
+- **layers.** Fixture modes 4 and 5 omit the Redis adapter, so an explicit
+ invalidation reports `missing_remote` and dispatches nothing. Two instances share
+ Redis but own their local capacity and process flights; contexts 0 and 1 belong to
+ instance 0, context 2 to instance 1, and contexts 3 and 4 are fresh invocation
+ scopes on each instance. Twenty calls and eighty steps keep entries fresh, so TTL
+ boundaries stay in the policy profile and the scenarios; four logical identities
+ over a two-slot local cache show promotion and eviction while request storage can
+ exceed that capacity. A completed source publishes only to participating eligible
+ layers; tracked remote fallback skips direct local publication while an
+ authoritative hit may warm local; invalidation of an entity fences later remote
+ reads of both tracked operation variants while acquired request and local values
+ survive; a policy change preserves an admitted source's publication decision.
+- **scope.** `openScope` opens contexts 1 to 4 at most once each, nested ones only
+ while outer 0 lives and 4 only after 3; `closeScope` closes any opened unfinished
+ context after the first call; closing 0 or 1 clears that lifetime's memo and flights,
+ closing a nested context does not end the outer lifetime, a closed outer context is
+ pass-through, and a completed nested context still belongs to its live outer
+ lifetime. These are context ownership rules; a port need not reproduce
+ AsyncLocalStorage or Promise scheduling. Enabled calls wait for `releasePolicy`;
+ disabled, detached and outside calls start their own source with no provider
+ invocation; at most one provider reply is held while accepted sources may overlap.
+ A late source returns to its original caller after closure but cannot populate a
+ replacement memo; coalescing admission precedes reading a memo another accepted
+ source populated.
+- **dark-layers.** The `inspect` action takes a public process snapshot of either
+ instance into `s.d.inspections` (instance, leader and follower counts, oldest
+ monotonic leader age; the model records an idle age as -1, the native projection as
+ `null`). Served shadow work and a caller's held write beside its held read are
+ outside this profile.
+
+The remaining composed profiles (recovery-read, local-failure, runtime-boundaries,
+shadow-layers, source-budgets, shadow-read-deadlines, local-clock) are summarized in
+the next section; their rules live in the kernel module headers the profiles compose.
+
+Each profile leaves the rest to others. Independent does not combine coalesced
+recovery, scope lifetimes, wall rollback or held publication. Layers leaves larger
+capacities, more scopes and instances, mixed deadline, recovery and shadow
+combinations and expiry during LRU ordering outside its bounds. Scope leaves request
+deadlines, recovery, shared-process flights, arbitrary context trees and more than
+two outer lifetimes to other profiles. Admission leaves ordinary misses, read and
+decode faults, separate read timeouts, shadow fill writes, custom comparator
+failures, local and request layers and fractional cohort selection to other
+profiles, the scenarios and the vectors. Every generated profile establishes
+occurrence of its witnesses, not fairness, exhaustive interleavings or wider claims.
+
+### Replaying generated traces
+
+`typescript/test/formal-features.test.ts` replays the feature traces and checks the
+parser and assertion trust boundaries; the committed smoke traces under
+`formal/generated/` run without Quint in the fast checks, and full validation replays
+every generated trace in every port. To replay one downloaded trace or a whole corpus:
+
+```sh
+DIALCACHE_FEATURE_TRACE_FILE=.formal-traces/features/recovery/trace_0.itf.json \
+ corepack pnpm --dir typescript exec vitest run test/formal-features.test.ts --coverage.enabled=false
+DIALCACHE_FEATURE_TRACE_DIR=.formal-traces/features \
+ corepack pnpm --dir typescript exec vitest run test/formal-features.test.ts --coverage.enabled=false
+```
+
+The parent directory (`recovery/`, `policy/`, `shadow/` and so on) identifies the
+fixture; keep a failing trace with its profile directory when copying it. The witnesses
+each profile's corpus must reach are listed per profile in
+[coverage-witnesses.json](../catalogs/coverage-witnesses.json); the witness checks
+establish occurrence only, and a corpus that misses a promised path fails them. Ports
+must select the specification revision that matches the traces they replay and reject
+unsupported actions or choices.
+
## Additional composition profiles
The following profiles extend the existing ownership models. Their exact bounds,
-checked properties and replayed regressions are registered in `execution.json`.
-Each records explicit public inputs as described in `AUTHORING.md`; expected
-observations never select a command, effect index or source result.
+checked properties and replayed regressions are registered in `execution.json`, and
+their fixtures, setup, action decodings and observation channels are generated into
+[PROFILES.md](../generated/PROFILES.md). Each records explicit public inputs as
+described in `AUTHORING.md`; expected observations never select a command, effect
+index or source result.
| Profile | Boundary and distinguishing public observations | Executable mapping |
| --- | --- | --- |
@@ -135,285 +403,6 @@ reply values and only their delivered replies determine policy.
Calls may remain pending at a scenario's end. Drivers release fixture-owned work during cleanup; cleanup effects are outside the trace and cannot satisfy its assertions. Unknown operations, missing effects, and repeated settlement fail replay.
-## Observations
-
-- `calls`: every caller, in start order, is `{"status":"pending"}`, `{"status":"value","value":1}`, or `{"status":"error","error":"source:0"}` / `"timeout:0"`. Source IDs identify the original loader error; timeout IDs identify distinct timeout outcomes in observation order. Coalesced followers must receive the same error identity. Ports can compare a shared logical error token without adopting JavaScript object identity.
-- `loaders`, `reads`, `writes`, `invalidations`, `loads`, `dumps`, `policyCalls`: cumulative actual loader, adapter, serializer, and provider invocations. Failed and still-pending attempts count. Value writes and invalidations are separate.
-- `classifications`, `comparisons`: actual invocations of the fixture-owned classifier/comparator. Built-in defaults are not instrumented.
-- `sourceScopes`: actual source-entry enablement observations when the explicit scope probe is enabled; otherwise empty.
-- `writeTtls`: actual requested physical write TTLs in milliseconds, in dispatch order.
-- `maintenance`: public invalidation outcomes, `ok`, `mutation_error`, or `missing_remote`. The last category records the actual public error; a port need not reproduce its native class or text.
-- `shadow`, `recovery`: terminal outcomes from the public diagnostic hooks, in observed order. Exact telemetry timing and ordinary metrics are not asserted.
-
-A returned cache value, loader invocation, or acknowledged write does not prove publication. Subsequent calls test cache retention and invalidation. Negative harness tests deliberately remove recovery, local storage, and acknowledged invalidation and require a later observable divergence.
-
-### Additional fixed-scenario inputs
-
-`adapterReply` stages one JSON-shaped semantic adapter result for the next successful raw-read settlement. Only one result may be staged at a time. The driver supplies it to the real cache at the adapter boundary; it neither decodes it on behalf of DialCache nor records a predicted miss/hit. Existing held reads and read failures remain independent. Tests use invalid replies to check the core's normalization; ports whose adapter type cannot represent malformed replies can enforce that boundary when decoding external input.
-
-`seed.payloadText` supplies exact UTF-8 text serializer bytes; `seed.payloadHex` supplies raw binary serializer/envelope bytes, framed with the current wall timestamp minus `ageMs`. `seed.frameHex` remains a complete frame, including header; ordinary `seed.value` still uses the scalar fixture codec. These inputs change only the fake Redis environment.
-
-## Generated pending-effect profile
-
-The effects model fixes remote-only policy to 60 seconds, a 10 ms source deadline and separately configured read budgets, and held read/decode/serialize/write effects. It bounds each trace to eight callers and eight sources; successful values are 1. Model monotonic time and application wall time are separate. No local cache, recovery, shadow work, or physical expiry is enabled in this profile. The model is composed from the kernel library: the held remote traversal under the budgeted lifecycle with its refills held, the queued adapter reply, and the metric events the drivers compare.
-
-| Quint action | Driver input |
-| --- | --- |
-| `init` | Choice 0..5 configures the fresh fixture and initial policy; hold reads, loads, dumps, and writes; observe budgets, cancellation, dispatch, and portable diagnostic events |
-| `beginCall` | `begin` |
-| `resolveLoader` / `rejectLoader` | Resolve with value 1 / reject, using explicit source index `choice` |
-| `releaseRead` / `failRead` | Release the explicitly selected raw read with success / failure |
-| `releaseLoad/Dump/Write` / `failLoad/Dump/Write` | Settle the latest corresponding actual effect with success / failure |
-| `seedRemote` | Seed value 1 at the current application wall time |
-| `tick` / `jumpClock` | Advance 10 ms with / without timer delivery |
-| `rollbackWall` | Move application wall time back 1,000 ms, preserving monotonic time and Redis physical expiry |
-| `advanceWall` | Version 3: move application wall time forward by explicit choice 1/59999/60000 ms; preserve monotonic time, deadlines and physical expiry |
-| `invalidate` / `futureFence` | Invalidate with a 0 / 20 ms future buffer |
-| `observerFault` | Choice 0/1 restores / fails diagnostic callbacks; cache outcomes remain unchanged |
-| `adapterReply` | Choice 1..16 supplies one next raw adapter reply; a second cannot be queued until the first is consumed |
-| `readBudgetPolicy` | Choice 0 inherits the operation/instance budget; choices 1..4 supply runtime budgets 10/20/30/50 ms |
-
-Initial choices 0..4 use tracked keys; choice 5 checks untracked reply/fence behavior. The effects initial input selects these precedence cases. Budget changes affect later reads; followers retain the registered leader's budget. Read budgets are multiples of the 10 ms clock step. Clock jumps without timer delivery are generated during 10 ms reads and source/application-owned phases; larger reads use delivered timer steps.
-
-| Initial choice | Instance | Operation default | Initial runtime | Effective read budget |
-| --- | --- | --- | --- | --- |
-| 0 | Omitted | Omitted | Inherit | Library 50 ms |
-| 1 | 20 ms | Omitted | Inherit | 20 ms |
-| 2 | 20 ms | 10 ms | Inherit | 10 ms |
-| 3 | 20 ms | 10 ms | 30 ms | 30 ms |
-| 4 | 20 ms | 10 ms | Provider returns null | 10 ms |
-| 5 | 20 ms | 10 ms | Inherit; untracked key | 10 ms |
-
-Each ITF state contains authoritative `input.name` and `input.choice`, plus
-expected state `s`. Choices are ITF integers: read/source settlement records an
-actual effect index; `observerFault` records 0/1; `init` records 0..5,
-`readBudgetPolicy` records 0..4, `adapterReply` records 1..16, and
-`advanceWall` records 1, 59999 or 60000 milliseconds. Actions without
-an external choice use `-1`. Optional MBT compatibility annotations must agree
-with the explicit input; raw regression exports need no annotations. See the
-[trace contract](./PORTING.md#trace-and-observation-contract).
-The parser rejects missing, unexpected, or unsafe choices. Failure actions set a fixture fault, release the selected external gate, drain runnable work, and restore the fault. `s.o`, `s.io` and `s.events` are the asserted channels; the rest of `s` is the model's private prediction and never enters execution or implementation projection.
-
-After every step, replay compares actual caller outcomes, loader/read/write/invalidation/serializer/provider counts, physical write TTLs, actual raw-read context budgets/initial cancellation state, and ordered cancellation IDs. Model caller codes are 0 pending, 1 value 1, 2 original source error, 3 timeout; the composed text records the shared conformance codes in `s.o.calls` (3 source error, 4 deadline error) and the parser maps them to these, so the observation schema introduced by version 2 is unchanged. Version 3 adds the explicit wall-advance domain and exported last-fresh/exact-expiry adapter-frame histories; the differential records this intended input-domain expansion. Asserting `io` and `d` beside `events` under the shared codes, as the feature profiles do, would be a separate observation-schema change. Fixed scenarios additionally compare logical error identity. A read deadline starts a fresh source budget and suppresses refill; successful raw-read completion clears that budget before application-owned decoding. Failed fresh decoding permits refill. Accepted serialization/write outlives the source budget, with the observed fence checked again after preparation.
-
-Full validation exports 512 traces from 4,096 samples, up to 60 transitions, and requires all actions plus 95 witnesses covering abandoned source/read settlement, independent budgets, late settlement guards, application-owned phases, acquired snapshots across invalidation, failure-specific publication, clock rollback at the second fence check, and observer failure isolation. Scheduled deterministic regressions anchor their declared boundaries; [execution.json](../catalogs/execution.json) distinguishes model checks from exported replays. Sampling favors the narrow rollback-during-publication boundary as well as unrestricted clock changes; it does not restrict that behavior to the favored schedule.
-
-Full validation runs all profiles in `execution.json` through TypeScript and Go. PR checks run the committed subset alongside ordinary tests. Committed ITF smokes run without Quint. Failure diagnostics include trace, step, action, and both observations. The effects choice/state schema and scope/policy value choices changed with this specification revision; ports must select a matching revision and reject unsupported actions or choices. Behavioral scenario schema 2 is unchanged.
-
-The queued adapter choices are: 1 null, 2 primitive, 3 legacy watermark shape, 4 kindless metadata, 5 missing miss reason, 6 unknown reason, 7 unknown reason with valid future fence, 8 fenced reason without fence, 9 negative fence, 10 fractional fence, 11 unsafe fence, 12 absent reason with future fence, 13 expired reason with zero fence, 14 miss with stray frame fields, 15 valid frame with stray miss metadata, and 16 fenced reason with valid future fence. Future fences are the input wall clock plus 20 ms. Successful raw completion consumes the reply even when DialCache has abandoned that read; adapter failure leaves it queued. Ports with strongly typed replies may normalize these encodings at their input boundary, but must preserve the resulting miss/refill behavior.
-
-`s.events` records `{ event, location, detail, amount }`. Location identifies a reached layer or coalescing scope. Amount is an integer millisecond measurement (get, fallback, serialization, future offset), a byte size, a write-dispatch index, or zero. Replay converts model milliseconds to callback seconds and compares actual ordered events, their labels, and source-error attribution. A follower emits its coalescing event without repeating the leader's read/source trail. Fresh decoding is included in remote-get duration; source duration ends at accepted settlement/deadline; dump has its own duration. Late sources do not repeat failures. Size events precede actual adapter dispatch, including when that write remains pending. Scalar value 1 has one serialized byte here; Unicode/binary byte accounting remains covered by protocol vectors and fixed scenarios.
-
-The profile requires 95 witnesses, listed in [coverage-witnesses.json](../catalogs/coverage-witnesses.json): fixture and race boundaries, every reply class consumed by an active read, untracked fence demotion, normalized fences blocking publication, every selected event kind, error/miss categories, and nonzero held load/dump durations. Its 51 exported public regressions, the model's public-only runs, anchor normalization, phase timing, late-failure suppression, and the sampled boundaries that random generation reaches only rarely, so a fresh seed cannot lose them. Missing/corrupted diagnostic observations fail the harness.
-
-## Generated feature profiles
-
-The generated feature models share the existing driver and a common [observation record](../models/conformance-observations.qnt). Their ITF states contain authoritative `input.name` and `input.choice`, with `s.o` as the expected observation. State outside `s.o` and the optional diagnostic record `s.d` is model-private prediction, not an implementation observation. The explicit choice is a nonnegative ITF integer on actions with choices below, or `-1` otherwise. Optional `mbt::actionTaken` and `mbt::nondetPicks.choice` annotations must agree with it. Reject unknown actions, unsupported choices, missing observation fields, and integer precision loss.
-
-Call observations encode pending as 0, fixture values 1/2 as 1/2, source errors as 3, and deadline errors as 4. Success codes 5..9 represent absent, null, false, zero, and empty string respectively; scope/policy generate these values. Other outcomes fail replay. These profiles compare error categories; the fixed scenarios compare logical error identity. All other observation fields use the scenario vocabulary directly, including zero/empty fields. A driver must use explicit action choices for selected source indices and its actual invocation counts for actions targeting the latest effect. It must never use expected counters, phases, cached values, or fences to select an input or fabricate an observation.
-
-| Profile | Fixture and bounds | Generated coverage |
-| --- | --- | --- |
-| [Independent](../models/dialcache-independent-conformance.qnt) | Tracked same-key calls, coalescing disabled, six callers, independent read/source/decode gates, read budgets 5/10 ms, F=1 s and captured M=2/5 s | Per-call cancellation, late effects, refill authority, recovery snapshots/policy and original source-error identities |
-| [Layers](../models/dialcache-layers-conformance.qnt) | Two instances, three persistent contexts, four identities, tracked/untracked and capacity 0/2 fixtures, twenty calls | Request/process sharing, layer precedence, LRU promotion/eviction, per-instance capacity, tracked local warming and operation-group invalidation |
-| [Admission](../models/dialcache-admission-conformance.qnt) | Tracked served remote hits, three keys, two instances, two shadow slots per instance, held reads/decodes, 10 ms job deadline, up to sixteen callers | Same-key deduplication, capacity drops, instance isolation, coalesced hits, policy snapshots, disabled detached sources, match/mismatch/supersession, capacity retained through timed-out source/decode/C1 work. Composed from the kernel library: the held remote traversal (`remote_io`) with the shadow module's held served-job lifecycle and its budgets |
-| [Scope](../models/dialcache-scope-conformance.qnt) | Request-only, one key, two outer lifetimes, three nested contexts, one held provider reply, independently settled sources, no deadline, up to sixteen callers | Scope isolation/closure/replacement; nested and disabled contexts; reenablement; pending policy at closure; shared rejection/retry; request/coalescing policy changes; late source settlement |
-| [Recovery](../models/dialcache-recovery-conformance.qnt) | Tracked remote with optional request memoization in two contexts, F=1 s, M initially 5 s, 10 ms source deadline, held decoding, up to eight callers | Fresh/stale/future frames; F/M boundaries; allow/deny/failing classifier; coalesced followers; source success versus rejection/deadline; default timeout-only classification and explicit overrides; abandoned source settlement; age checks around decode; invalidation/replacement; read/decode failures; captured recovery policy. Composed from the kernel library: the held remote traversal with its recovery snapshots under the budgeted lifecycle, the read settled at admission, and the diagnosed variants that record the coalesced scope, the failed layer and the recovery age |
-| [Policy](../models/dialcache-policy-conformance.qnt) | Untracked local+remote, both TTLs initially 1 s, M=5 s, local capacity one, two keys, one held provider reply, independently settled sources, no source deadline, up to twelve callers | Runtime coalescing on/off, per-source policy snapshots, shared versus independent same-key work, cross-key overlap and reverse settlement; independent runtime leaves; invalid local/remote TTL; provider/read/dump/write failure; policy acquisition and pending publication; local eviction/insertion TTL; logical Redis freshness versus physical retention |
-| [Shadow](../models/dialcache-shadow-conformance.qnt) | Tracked remote TTL=60 s, serving ramp=0, shadow ramp initially 100 (runtime 0/100/invalid), optional outcome hook, caller/job deadline=10 ms, all read/load/dump/write effects held, up to eight callers | Independent dark C0/source settlement; captured payload decode; match/mismatch/C1 supersession; confirmation failure; conditional fills; source/read/decode/dump/write failure; deadline during held effects; late work cannot change emitted outcomes. Composed from the kernel library: the dark arm of the shadow module's held lifecycle (the job's C0 read, decode and confirmation read held and released by ordinal) over the diagnosed budgeted held remote traversal, with the held fill and the buffered invalidation |
-| [Dark layers](../models/dialcache-dark-layers-conformance.qnt) | Two instances, two keys, three persistent scopes and two transient contexts; twelve callers, one dark job per instance, 10 ms source/job budget, 60 s local TTL; held read/load/dump/write effects | Request/process followers, independent publication, source-error retry, captured fill retention, strict read/write fences, buffered invalidation, wall rollback, payload faults and failure-layer diagnostics |
-| [Shadow read deadlines](../models/dialcache-shadow-read-deadlines-conformance.qnt) | Two keys, one instance, one shadow slot, eight callers; 10 ms source/job budget, 5 or 20 ms read budgets; held effects and a 100 ms elapsed-time bound | C0/C1 errors at their own read deadlines, raw ownership and readmission, independent job timeout, captured C1 budget and dispatch-relative timing |
-
-Dark-layers inputs use explicit effect ordinals and source indices. `beginCall` choices 0..9 encode key modulo two and context divided by two; `resolveLoader` choices 1..24 encode source index and value 1/2. Policy choices 0..8 select request/local layers, coalescing and dark-shadow admission, with remote serving always off. Seeds 0..11 select two keys and six frame classes; invalidation 0..3 selects a key and a 0/20 ms future buffer. `advance` accepts 1, 10 or 60000 ms, `rollbackWall` shifts wall time back 1000 ms, and each read/load/dump/write fault toggles 0/1. Version 2 adds `inspect` choices 0/1 for public process snapshots of either instance and `s.d.inspections`. The snapshot records instance, leader/follower counts, and oldest monotonic leader age; the model uses -1 for an idle age and the native projection uses null. Five exported histories require live counts, request/process follower separation, oldest-leader replacement, instance isolation, wall rollback independence, cleanup on success/error/timeout, and exclusion of unfinished shadow or abandoned raw work. Served shadow work and the caller's own held write beside its held read remain outside this profile.
-
-The dark-layers native replay settled one diagnostics rule against the TypeScript reference: an active local layer attributes its failed source to `local` even inside a request memo; without a shared layer, a transient request attributes it to `request_local`. Named public histories pin both cases in TypeScript and Go.
-
-Recovery opens contexts 0 and 1 in every fixture. New calls use open contexts; the separate scope profile covers detached calls after closure. Request misses may join the same process flight, after which each attached open context memoizes its result. A same-request follower records request coalescing; a new request records process coalescing. Recovered values have no shared-cache publication. Closing a context clears its memo and prevents late recovery from populating it. Four required witnesses include a recovered memo hit, later probes of both requests after shared recovery, a new read after closed-scope recovery, and request followers sharing recovery work. Three deterministic regressions anchor these cases.
-
-Policy and recovery separate wall timestamps from elapsed time. Generated public probes require local hits to survive a rollback before their original TTL, expiry at that TTL despite rollback, remote future-frame rejection, and retained recovery rejection when rollback makes its candidate future-dated. Physical Redis expiry remains independent. Invalidation never lowers an existing watermark. Four deterministic regressions anchor these clock rules.
-
-Recovery begins with value 1 seeded at age 1,000 ms. Policy and shadow begin with empty storage. Every trace gets a fresh fixture. The shadow profile permits another call once its preceding source and owned job work have settled. The separate admission and shadow-layers profiles exercise cross-key capacity/drop and mixed ownership boundaries alongside fixed scenarios. Recovery advances through a source deadline before the end of a larger elapsed-time step; recovery starts at that deadline and its held decode may complete later. The retained snapshot and source-error identity survive late source settlement. Recovery initial input 0/1/2/3 selects the timeout-only library default or an instance classifier that allows, denies, or throws; 4..7 selects the same classifier with request-local caching enabled. Operation choice 3 inherits that instance policy; 0/1/2 replaces it with allow/deny/error. Full validation requires all eight initial fixtures, both directions of operation override, instance allow on ordinary source errors, instance denial on source deadline, and classifier-error preservation of the source failure. Policy admits another invocation after the preceding provider reply is released, even while its source remains pending. Sources can settle in any order; same-key followers join only while their current policy permits sharing. A shared leader remains registered when an independent source publishes or fails. Request scopes have their own generated profile; held publication remains outside this policy profile.
-
-Common actions reuse the scenario inputs: `releaseRead/Load/Dump/Write/Policy` releases the most recently observed corresponding external effect in scope/recovery/policy/shadow; admission and independent instead select explicit pending read/load indices; `readFault/loadFault/dumpFault/writeFault/providerFault` sets that failure flag from choice 0/1 (provider uses `faults.policy`). Shadow `rejectLoader` rejects the latest actual loader; recovery/scope/policy/admission/independent settlement selects an explicit source index. No action reads or mutates the cache's internal state.
-
-| Profile/action | Input mapping and allowed choices |
-| --- | --- |
-| Recovery `closeScope` | Close context choice 0/1; late work can finish but cannot memoize into the closed context |
-| Recovery `beginCall` | Choice 0..7: context `floor(choice / 4)` and operation classifier `choice % 4` (allow/deny/error/inherit) |
-| Recovery `joinCall` | Begin in context choice 0/1 while shared work is pending; a preexisting request memo can still win |
-| Recovery `resolveLoader` / `rejectLoader` / `rejectTimeout` | Choice 0..7 selects an unsettled source; resolve with value 2 / reject with ordinary error / reject with a propagated timeout error |
-| Recovery `seed` | Choices 0..6 give ages `[0,999,1000,4999,5000,-1,1000]` ms; value 1 except choice 6 gives value 2 |
-| Recovery `advance` | Elapsed time choice 1, 10, 1000, or 4000 ms, with timers delivered |
-| Recovery / Policy `rollbackWall` | Move only the application wall clock back 1,000 ms; local deadlines and physical expiry retain elapsed time |
-| Recovery `invalidate` | Public invalidation with zero future buffer |
-| Recovery `policy` | Set `staleOnErrorMaxAgeSec` to choice 2000/5000 divided by 1000 |
-| Policy `beginCall` | Key is string `"0"` or `"1"` from choice 0/1 |
-| Policy `resolveLoader` | Choice 1..84 encodes source index `floor((choice - 1) / 7)` and the value at `(choice - 1) % 7` in `[1,2,absent,null,false,0,""]`; only pending sources are generated |
-| Policy `rejectLoader` | Reject the explicitly selected source index, choice 0..11; only pending sources are generated |
-| Policy `seed` | Choice 0..3 supplies key `floor(choice/2)` with value `1 + choice%2`, current wall stamp, and 5 s physical TTL |
-| Policy `advance` | Elapsed time choice 1, 500, 1000, 2000, or 5000 ms |
-| Policy `policy` | Replace overlay using the numbered table below |
-| Shadow `init` | Choice 0..3 selects default/equal/unequal/error comparison; 4..7 selects the same comparison with mismatch logging enabled; 8 omits the outcome hook; 9/10 supplies equal/error comparison consuming 10 ms; 11/12 uses default comparison and consumes 9/10 ms of external source work before deferred job dispatch. Logging is initially off for 8..12 |
-| Shadow `rollbackWall` | Move the wall clock back 1,000 ms without changing elapsed time |
-| Shadow `logPolicy` | Choice 0/1 disables/enables logging; choice 2 supplies the malformed string `"invalid"`. Newly admitted eligible jobs record a configuration error and capture logging off for choice 2; omitted ramp inherits the fixture default |
-| Shadow `shadowPolicy` | Choice 0/1/2 replaces the runtime overlay with shadow ramp 100/0/101; omitted logging inherits the fixture default |
-| Shadow `beginCall` | Plain `begin` |
-| Shadow `resolveLoader` | Resolve latest loader with choice 1/2 |
-| Shadow `seed` / `reencode` | Store the explicit payload choice below at current wall time; `reencode` chooses the alternate text/binary form of the currently stored bytes during C1 |
-| Shadow `seedUnicode` | Store text/binary multibyte JSON using choice 7/8; this extra environment branch increases representation-boundary sampling while ordinary `seed` retains all payloads |
-| Shadow `advance` | Elapsed time choice 1/10 ms, delivering due timers; blocked-source fixtures 11/12 use only 10 ms windows |
-| Shadow `advanceWall` | Move only the application wall clock forward by choice 1/60000 ms while C1 confirmation is pending; elapsed deadlines and physical Redis TTL do not advance |
-| Shadow `invalidate` | Public invalidation with future buffer choice 0/20 ms |
-
-Shadow payload choices 1/2 are text JSON `1`/`2`; 3/4 are binary hex `31`/`32`; 5 is binary `2031`; 6 is text ` 1`; 7 is text JSON `"café"`; 8 is binary `22636166c3a922`. Thus text and binary may share exact UTF-8 bytes, while different byte spellings may decode to the same value. Comparison uses decoded values; confirmation uses bytes. `reencode` records the replacement payload as an explicit choice, so a driver never consults expected storage. Required witnesses include both Unicode text/binary confirmation directions, equal decoded values superseded by different bytes, binary C0 decoding, and successful/failing comparison exhausting the deadline. Timer delivery is not required for elapsed-time rejection.
-
-Policy overlay choices replace the entire runtime overlay; omitted leaves inherit the fixture's defaults:
-
-| Choice | Overlay |
-| --- | --- |
-| 0 | Empty/inherit |
-| 1 | Local TTL 2 s |
-| 2 | Remote TTL 2 s |
-| 3 | Local serving ramp 0 |
-| 4 | Remote serving ramp 0 |
-| 5 | Invalid local TTL -1 s |
-| 6 | Invalid remote TTL -1 s |
-| 7 | Recovery maximum age 2 s |
-| 8 | Both serving ramps 0 |
-| 9 | Remote TTL 4 s, recovery disabled (maximum age 0) |
-| 10..19 | Same overlay as choice minus 10, with `coalesce: false`; other choices inherit default sharing |
-| 20 | Invalid remote read budget 0: bypass all caching for the invocation |
-| 21 / 22 | Invalid local / remote ramp 101: disable that layer while preserving the other |
-| 23 / 24 | Invalid recovery maximum age 1 / -1 s: normal serving remains active, writes use ordinary 1 s retention |
-| 25 | Invalid shadow ramp 101: normal fresh serving remains active |
-
-Five deterministic policy regressions anchor invalid budget, per-layer ramp, optional recovery retention, and fresh-hit shadow-policy behavior. The generated sample requires each boundary, including a Redis hit under invalid shadow policy and both invalid recovery retention cases. Independent Redis seeding makes external replacement/read scenarios reachable.
-
-Generation exports 512 recovery traces from 4,096 samples, and 512 policy traces from 2,048 samples and 1,024 shadow traces from 4,096 samples, at most 60 transitions each. Actions are sampled in progress/environment groups so repeated environmental changes do not crowd out useful completion paths; C1 favors completion and logging changes while retaining replacement, fencing, read failure, time, and admission-policy changes. This changes exploration frequency, not the allowed transition semantics.
-
-Full validation requires every named action, all three recovery outcomes, recovery across invalidation, coalesced recovery, age-out during decoding, local/remote hits, changed-policy publication, physical TTLs of 1/2/4/5 seconds, both C0/source orders, all twelve modeled shadow outcomes, and a write completing after shadow timeout. These witness checks fail if a configured corpus misses its promised paths. They establish occurrence only. The separate verification models still reason about wider abstractions such as shadow admission, and the portable fixed corpus covers additional binding-independent boundaries.
-
-Scope and recovery expose `s.d = { warnings, ages, coalesced, fallbackErrors }`. Shadow profile version 2 adds `configErrors`, counting actual `config_resolution` events with remote/non-fallback labels. Other profile diagnostic schemas are unchanged. Ages are integer milliseconds in Quint and compared to actual callback seconds after unit conversion. The driver obtains this projection only from observed callbacks; it checks their operation/outcome labels and retains their order. Recovery records age only after successful retained decode. Shadow records original-C0 age at match/confirmed-mismatch verdict, clamped to zero after wall rollback; it emits a warning only for a confirmed mismatch whose admitted policy enabled logging. Later runtime changes do not rewrite that policy. Malformed logging leaves comparison active and warnings disabled. C1 compares retained payload identity even when a replacement timestamp is future-dated. Exact native JSON warning formatting remains a binding obligation.
-
-`coalesced` records actual request/process scope labels; `fallbackErrors` records the source-failure layer, including failures later recovered as stale. Scope fixtures assert one trail for shared failures, no cache-error trail for disabled pass-through work, and `noop` attribution if the request closes while policy is pending. Admission-time attribution survives later scope closure. Three deterministic scope regressions and five diagnostic witnesses anchor these consequences. Other cache/maintenance errors are outside this feature diagnostic projection and remain checked by effects and fixed scenarios.
-
-Thirteen shadow fixtures, both custom comparison overrides, comparison failure, both captured-logging directions, logging on/off, malformed logging at a completed mismatch, no warning for match/supersession, clamped age, and positive verdict age are required witnesses. Thirty-nine deterministic shadow regressions, every one an exported public schedule, anchor these rules. Required witnesses also cover no job without the outcome hook, disabled/invalid policy skipping new jobs, and an admitted job completing under its original policy. Missing or corrupted diagnostic expectations must fail harness checks.
-
-Fixtures 11/12 use the existing external `sourceWorkMs` input, advancing elapsed and wall time without delivering timers while the source begins. At 9 ms, the dark job still dispatches C0 and an immediately settled source can succeed. At exactly 10 ms, the deferred job reports timeout without a Redis read, while the caller remains pending. Subsequent source resolution or rejection produces the caller's deadline error when settlement checks elapsed time; delivering its timer may produce that error first. These fixtures advance in full 10 ms windows after the blocked work, observing after overdue timers are delivered; intermediate native timer ordering is outside their bounds. This distinguishes job abandonment from source timer delivery. Generated witnesses require both boundaries and both late settlement outcomes. The `expiredSourceWorkSkipsRedis` invariant independently forbids reads in the exhausted-work fixture; warning authorization is checked against captured valid policy separately from verdict emission.
-
-`typescript/test/formal-features.test.ts` replays these traces and checks parser/assertion trust boundaries. Fast PR checks use the committed `recovery-smoke.itf.json`, `policy-smoke.itf.json`, and `shadow-smoke.itf.json` without Quint. Full validation replays every generated trace. To replay a downloaded artifact:
-
-```sh
-DIALCACHE_FEATURE_TRACE_FILE=.formal-traces/features/recovery/trace_0.itf.json \
- corepack pnpm --dir typescript exec vitest run test/formal-features.test.ts --coverage.enabled=false
-```
-
-Full policy validation requires six additional concurrency witnesses: cross-key overlap, uncoalesced same-key overlap, a join after policy changes, reverse source settlement, one source settling multiple callers, and publication while another provider reply is held. Its committed smoke is a generated prefix containing a shared rejection and a later independent settlement; it also runs without Quint. Policy settlement choices changed with the concurrent profile, so replay these traces with the matching specification revision.
-
-The parent `independent/`, `layers/`, `scope/`, `recovery/`, `policy/`, `shadow/`, or `admission/` directory identifies the fixture. To replay a whole generated feature corpus, set `DIALCACHE_FEATURE_TRACE_DIR=.formal-traces/features` instead. Keep a failing trace with its profile directory when copying it.
-
-## Generated independent-caller profile
-
-[`dialcache-independent-conformance.qnt`](../models/dialcache-independent-conformance.qnt) tests the same key with coalescing disabled. The single registered-flight models cannot express independent acquired reads and recovery chains; this companion reuses the existing driver and effect vocabulary. Six callers can each own one read, one source, and one decode. Tracked remote freshness is 1 s, initial recovery maximum age is 5 s, read budget is 5 ms, and source budget is 10 ms. Recovery classification allows ordinary errors and timeouts. Value 1 initially has age 1,000 ms and physical TTL 60,000 ms. Only raw reads and decoding are held; accepted publication completes at the source-settlement boundary.
-
-| Action | Environment/public input |
-| --- | --- |
-| `beginCall` | Begin another independent same-key call |
-| `releaseRead` / `failRead`, `releaseLoad` / `failLoad` | Complete or reject the explicitly selected actual read/decode index, 0..5 |
-| `resolveLoader` | Choice 1..12: source `floor((choice - 1) / 2)`, value `1 + (choice - 1) % 2` |
-| `rejectLoader` | Reject source index 0..5 with that source's logical error |
-| `advance` | Advance 1, 5, 10, or 1,000 ms and deliver due deadlines |
-| `seed` | Choice 0..5: values `[1,1,2,1,2,1]`, ages `[0,1000,1000,4999,0,1999]` ms, physical TTL 60,000 ms |
-| `invalidate` | Public invalidation with zero future buffer |
-| `policy` | Choice 0..3: read budget 5 ms for even choices, 10 ms for odd; recovery maximum age 5 s for 0/1, 2 s for 2/3 |
-
-Each call captures its read budget and recovery policy. Read failure or timeout cannot borrow another call's refill authority. Each recovery chain retains its own eligible bytes and original source error. Later invalidation cannot revoke an already acquired fresh decode or stale candidate; recovery still rechecks age around decode. Late raw read/source settlement cannot affect another call. The environment delivers deadlines in time order, using registration order for equal instants, including new source deadlines reached within one advance. This is the supplied schedule; other runtimes need not use the same timer implementation.
-
-Besides the common `s.o`, replay requires `s.io = { budgets, aborted, sourceErrors }`. `budgets` records actual adapter read budgets in read invocation order; `aborted` records actual cooperative cancellation indices in delivery order. `sourceErrors` has one entry per caller: zero unless the caller returned its source's ordinary error, otherwise the one-based actual source identity. The driver projects actual adapter callbacks and returned error tokens; model-private ownership records never enter execution. Parser and corrupted-budget tests protect that boundary.
-
-Full validation emits 512 traces from 2,048 samples, up to 60 steps, and requires every action plus the witnesses listed for it in [coverage-witnesses.json](../catalogs/coverage-witnesses.json), covering separate budgets/deadlines, distinct recovery values/errors, captured age policy, failed-read refill suppression, acquired observations across invalidation, and late completion isolation. The profile's deterministic regressions, the runs its model declares, anchor these rules. The committed `independent-smoke.itf.json` replays without Quint. Coalesced recovery, scope lifetimes, wall rollback, and held publication retain separate profile coverage; this model does not combine every feature.
-
-## Generated layer-composition profile
-
-[`dialcache-layers-conformance.qnt`](../models/dialcache-layers-conformance.qnt) connects request memoization, process flights, local storage, Redis, and source publication. The separate scope and policy profiles isolate lifetime and policy history; composition is needed to test a request miss joining a process flight, per-instance storage shared across operations, and the publication consequences of tracked reads.
-
-The initial **input choice**, never expected model state, selects the fresh fixture:
-
-| `init` choice | Identity and Redis adapter | Local capacity per instance |
-| --- | --- | --- |
-| 0 | Untracked, adapter present | 2 |
-| 1 | Tracked, adapter present | 2 |
-| 2 | Untracked, adapter present | 0 |
-| 3 | Tracked, adapter present | 0 |
-| 4 | Untracked, adapter absent | 2 |
-| 5 | Tracked, adapter absent | 2 |
-
-Modes 4 and 5 omit the Redis adapter and require public local-hit reuse after explicit invalidation reports `missing_remote`; no adapter mutation is dispatched. All modes enable request-local caching and 60-second local/remote TTLs, with no source deadline. Sources are held independently; other external effects settle at their action boundary. Two instances share Redis but own their local capacity and process flights. Persistent contexts 0 and 1 belong to instance 0; context 2 belongs to instance 1. Contexts 3 and 4 mean a fresh invocation scope on instance 0 and 1 respectively. This is an input-level fixture description, not a requirement to reproduce any host context API.
-
-| Action | Input mapping |
-| --- | --- |
-| `beginCall` | Choice 0..19: context `floor(choice/4)`, identity `choice%4`; identity maps to entity `floor(identity/2)` and operation `Layers0`/`Layers1` from `identity%2` |
-| `resolveLoader` | Choice 1..40 selects source `floor((choice-1)/2)` and value `1+(choice-1)%2` |
-| `rejectLoader` | Explicit pending source index 0..19 |
-| `closeScope` | Persistent context 0..2; captured handles remain usable for detached calls |
-| `policy` | 0 all layers; 1 disable request; 2 disable local; 3 disable remote; 4 request only; 5 no serving layers |
-| `seed` | Choice 0..7 selects identity `floor(choice/2)` and value `1+choice%2` |
-| `invalidate` | Entity 0/1, affecting both tracked operation variants |
-| `tick` | Advance 1 ms |
-
-At most twenty calls and eighty steps keep entries fresh throughout this profile; TTL boundaries remain in policy/scenario coverage. There are four logical identities, so a two-slot local cache can demonstrate read promotion and eviction, while request storage can exceed that capacity. Successful source completion publishes only to participating eligible layers. Tracked remote fallback skips direct local publication; an authoritative hit can warm local. Invalidation fences subsequent remote reads while acquired request/local values survive. Policy changes preserve admitted sources' publication decisions.
-
-Full validation exports 512 traces from 2,048 samples. Required witnesses include all six fixtures and local reuse without Redis before and after a surfaced maintenance error, cross-request process sharing, zero-capacity sharing/reload, uncapped request memoization, LRU promotion/eviction with later public probes, per-instance capacity, tracked read warming, local survival across invalidation, both operation variants fenced, and untracked reads ignoring markers. Private model records select reachability witnesses only; storage-related witnesses require actual replayed calls that probe their predictions. They never control the adapter or become implementation observations. Scheduled deterministic regressions anchor these boundaries, and a committed generated smoke runs without Quint. The current regression inventory is the model's runs; the witness inventory is in [coverage-witnesses.json](../catalogs/coverage-witnesses.json).
-
-This profile uses the same observations and public/environment inputs as the other feature profiles. It adds initial fixture choices; drivers must reject unsupported choices. Larger capacities, more scopes/instances, mixed deadline/recovery/shadow combinations, and expiry during LRU ordering are outside its generated bounds.
-
-## Generated request-scope profile
-
-The scope profile reuses the same `openScope`, `closeScope`, `begin`, policy, and source-settlement inputs. It adds no public API or driver mechanism. It starts with enabled outer context `0`, held provider replies, request-local caching on, no shared storage, and the source-scope probe enabled. Its single key isolates request-lifetime semantics from the storage/TTL state in the policy profile.
-
-| Context choice | Meaning |
-| --- | --- |
-| 0 | Initially open outer request |
-| 1 | A separately opened outer request; it may overlap or replace 0 |
-| 2 | Enabled context nested under 0 |
-| 3 | Disabled context nested under 0 |
-| 4 | Enabled context nested under 3, reusing 0's live memo lifetime |
-| 5 | Outside every request; only usable by `beginCall` |
-
-`openScope` chooses 1..4, each at most once. Nested contexts open only while outer 0 is live, and 4 requires 3 to exist. `closeScope` chooses any opened, unfinished context 0..4 after the first call. Closing 0/1 clears that lifetime's memo and registered flights. Closing nested contexts does not end the outer lifetime. Captured contexts remain usable by later calls: closed outer contexts are pass-through, while completed nested contexts still belong to a live outer lifetime. These are context ownership rules; ports need not reproduce AsyncLocalStorage or Promise scheduling.
-
-`beginCall` chooses context 0..5. Enabled calls wait for `releasePolicy`; disabled/detached/outside calls immediately start their own source without a provider invocation. At most one provider response is held, but any accepted sources may overlap. `policy` choice 0 inherits request caching and coalescing; 1 sets `requestLocal: false`; 2 sets `coalesce: false` while retaining memoization. Settlements select actual loader indices: `resolveLoader` choice 1..112 encodes index `floor((choice - 1) / 7)` and the value at `(choice - 1) % 7` in `[1,2,absent,null,false,0,""]`; `rejectLoader` chooses index 0..15. Only pending sources are generated.
-
-The model predicts memo lifetime and flight ownership. Replay observes actual caller values/errors, source enablement, and provider/source invocations; subsequent calls establish hits or misses. A late source may return to its original caller after closure, but cannot populate a replacement memo. Coalescing admission precedes reading a memo populated by another independently accepted source.
-
-Generation exports 256 traces from 1,024 samples, up to 60 transitions, with at most sixteen calls. Sampling keeps closure reachable while favoring useful call progress; no fairness or exhaustive context-tree claim is made. Full validation requires every action plus the cataloged witnesses, including disabled/detached bypass, policy reply after closure, rejection/retry, shared rejection, source settlement after closure, replacement miss after that settlement, independent scope overlap, uncoalesced same-scope overlap, memo hits, nested/reenabled hits, memo reuse after nested closure, memo reuse after policy bypass, memo hits for all five empty/falsy/absent values, and five failure-attribution/shared-trail witnesses. Deterministic model regressions anchor closure, replacement, nested/disabled reuse, rejection/retry, and error attribution.
-
-The committed `scope-smoke.itf.json` is a generated schedule including absent-value reuse and request closure. It runs without Quint in fast PR checks. Request deadlines, recovery, shared-process flights, arbitrary context trees, and more than two outer lifetimes remain covered separately or outside this generated profile.
-
-## Generated served-hit shadow admission profile
-
-[`dialcache-admission-conformance.qnt`](../models/dialcache-admission-conformance.qnt) reuses the existing public driver and observation schema. It separates admission and resource ownership from the dark C0/fill protocol. Three shared Redis keys initially contain value 1, with tracked serving and shadow ramps at 100%. Two cache instances each have two shadow slots. This makes a duplicate drop distinguishable from a full instance, and permits checking another instance while the first is full.
-
-Caller reads and all decoding are held. A successful caller read acquires C0; completing its decode returns that value and considers shadow admission using the caller flight's accepted policy. Coalesced followers share this one admission. Independently accepted calls can each attempt admission. An admitted detached source runs with caching disabled. Shadow comparison uses its retained C0 and source result; unequal values trigger a held C1 read. No shadow action changes a caller result or writes cache values. Every rule is a kernel transition: the held remote traversal with immediate replies (`remote_io`) through the shadow module's held served-job lifecycle, which captures the cohort selection when the caller's read is dispatched and consults it when the decode completes the hit, with the job budgets kept by `deadlines`; the profile owns the bounded state, the input decoding and the guards.
-
-| Quint action | Portable input and choice |
-| --- | --- |
-| `beginCall` | Choice 0..5 selects instance `floor(choice / 3)` and key `choice % 3`, both decimal strings |
-| `releaseRead` / `releaseLoad` | Release the explicitly chosen actual effect index, 0..31 |
-| `resolveLoader` | Choice 1..32 selects source index `floor((choice - 1) / 2)` and value `1 + (choice - 1) % 2` |
-| `rejectLoader` | Reject the chosen actual source index, 0..15 |
-| `seed` | Choice 0..5 replaces key `floor(choice / 2)` with value `1 + choice % 2`; both instances observe the shared environment |
-| `policy` | Choice 0 inherits enabled shadow/coalescing; 1 disables shadow; 2 disables coalescing; 3 disables both. Only new caller flights acquire the changed policy |
-| `advance` | Advance 1 or 10 ms and deliver timers, bounded to 600 ms total elapsed time |
-
-Only pending effects/sources may settle. There are at most sixteen calls and sixteen admitted jobs, giving at most 32 read and 32 decode effects. Redis TTL is 60 seconds, each shadow job's deadline is 10 ms, and the read deadline is 1,000 ms. The elapsed-time bound keeps serving reads fresh and below their separate deadline. Ordinary misses, read/decode faults, separate read timeouts, shadow fill writes, custom comparator failures, local/request layers, and fractional cohort selection retain coverage in other profiles, scenarios, or vectors.
-
-A whole-job timeout emits one diagnostic outcome but keeps the slot until its pending source, decode, or confirmation read settles. Later completion cannot start another decode/read or emit a replacement verdict. Once the owned work drains, a subsequent hit may admit another job. This models resource ownership rather than cancellation or language executor turns.
-
-Full validation exports 128 traces from 1,024 samples, up to 60 transitions, and requires every action plus the cataloged witnesses, including six terminal outcomes (match, mismatch, superseded, source_error, timeout, dropped), one admission for coalesced hits, uncoalesced hit overlap, accepted shadow policy after a change, unselected hits, duplicate drops while capacity is available, full-capacity drops, admission while the other instance is full, per-instance deduplication, capacity retained by each of the three timed-out phases, and readmission after expired work drains. Deterministic model regressions anchor coalesced admission, duplicate drops, per-instance capacity, all three timeout ownership phases, the shadow selection captured with the read across a policy change, and an uncoalesced caller's own read beside the registered leader.
-
-The committed `admission-smoke.itf.json` retains actions, choices, and observation records from the first 57 states of a generated trace. Model-private prediction fields are omitted to keep it compact. It contains a timed-out decode, a blocked duplicate, completion of the raw decode, and subsequent admission for that key. Full generated ITF states remain in the full workflow artifacts. The existing parser replays both forms without special handling or expected-state input to the driver.
-
## Port workflow and limits
1. Implement the protocol/key/normalization/envelope vectors and the invalidation-transition vectors against the actual remote adapter/protocol.
diff --git a/formal/guides/README.md b/formal/guides/README.md
index 02dae0cf..0edce5e4 100644
--- a/formal/guides/README.md
+++ b/formal/guides/README.md
@@ -30,6 +30,10 @@ by-task view; this index is the by-kind view it lacks. Read
- [TEST-MAP.md](./TEST-MAP.md): the map from contracts to implementation evidence.
- [TEST-AUDIT.md](./TEST-AUDIT.md): keeping the docs and test audit ledger current.
+## Generated views: read, never edit
+
+- [../generated/PROFILES.md](../generated/PROFILES.md): every conformance profile's fixture, setup, action decodings and observation channels, rendered from the replay descriptors; [BEHAVIOR.md](./BEHAVIOR.md) keeps the rules behind them.
+
## Historical evidence: what was measured, and when
- [HISTORY.md](./HISTORY.md): the composition records of each profile's rewrite over the kernel library, and the PR #161 validation baseline, at the revisions they were measured.
diff --git a/formal/models/dialcache-admission-conformance.qnt b/formal/models/dialcache-admission-conformance.qnt
index 04ce6013..06d1fb6a 100644
--- a/formal/models/dialcache-admission-conformance.qnt
+++ b/formal/models/dialcache-admission-conformance.qnt
@@ -18,7 +18,7 @@ module dialcache_admission_conformance {
// explicit source settlements and elapsed clock steps. Bounds: three keys,
// two instances, two job slots each, sixteen callers; elapsed time stays
// below read deadlines and physical Redis expiration.
- // See BEHAVIOR.md "Generated served-hit shadow admission profile" for the
+ // See formal/generated/PROFILES.md (admission) and BEHAVIOR.md "Generated profiles" for the
// drivers' input table.
// Every rule is a kernel transition (formal/models/kernel): the held remote
// traversal with immediate replies (remote_io, through the shadow module's
diff --git a/formal/models/dialcache-effects-conformance.qnt b/formal/models/dialcache-effects-conformance.qnt
index 3363f73d..d3c58f97 100644
--- a/formal/models/dialcache-effects-conformance.qnt
+++ b/formal/models/dialcache-effects-conformance.qnt
@@ -20,7 +20,7 @@ module dialcache_effects_conformance {
// One registered remote-only execution, plus up to eight callers and late
// external sources/reads. Selected aspects of C23-C28 cover budgets and
// accepted publication; C33-C36 cover fences/snapshots; C55-C59 cover effects.
- // See BEHAVIOR.md: "Generated pending-effect profile" for the driver mapping.
+ // See formal/generated/PROFILES.md (effects) for the driver mapping and BEHAVIOR.md "Generated profiles".
// No local storage, recovery, shadow work, or physical expiry participates.
// Every rule is a kernel transition (formal/models/kernel): the held remote
// traversal (remote_io) under the budgeted held lifecycle (deadlines) with
diff --git a/formal/models/dialcache-independent-conformance.qnt b/formal/models/dialcache-independent-conformance.qnt
index 29a6c154..a9959111 100644
--- a/formal/models/dialcache-independent-conformance.qnt
+++ b/formal/models/dialcache-independent-conformance.qnt
@@ -15,7 +15,7 @@ module dialcache_independent_conformance {
// C24/C56: each owns its read and source deadline. Read failure denies only
// that caller's refill (C28); recovery keeps its captured policy, snapshot,
// and original error (selected aspects of C36/C40-C46/C58).
- // See BEHAVIOR.md: "Generated feature profiles" and its independent input table.
+ // See formal/generated/PROFILES.md (independent) for the input table and BEHAVIOR.md "Generated profiles".
// No local/request storage, shadow work, or publication failures participate.
// Every rule is a kernel transition (formal/models/kernel): the held remote
// traversal (remote_io) with its recovery snapshots (recovery) under the
diff --git a/formal/models/dialcache-recovery-conformance.qnt b/formal/models/dialcache-recovery-conformance.qnt
index b721d2a9..5b78c3f0 100644
--- a/formal/models/dialcache-recovery-conformance.qnt
+++ b/formal/models/dialcache-recovery-conformance.qnt
@@ -16,7 +16,7 @@ module dialcache_recovery_conformance {
// One registered tracked remote flight, with coalesced callers in two optional
// request lifetimes. Selected aspects of C40-C46 cover retained recovery;
// C03/C43 cover request publication; C57/C58 cover age and error observations.
- // See BEHAVIOR.md: "Generated feature profiles" and its recovery input table.
+ // See formal/generated/PROFILES.md (recovery) for the input table and BEHAVIOR.md "Generated profiles".
// Reads and publication settle at action boundaries; decoding and sources may
// wait. No local storage, independent same-key flights or shadow work
// participates. Every rule is a kernel transition (formal/models/kernel): the held
diff --git a/formal/models/dialcache-shadow-conformance.qnt b/formal/models/dialcache-shadow-conformance.qnt
index 55913768..9983e6e7 100644
--- a/formal/models/dialcache-shadow-conformance.qnt
+++ b/formal/models/dialcache-shadow-conformance.qnt
@@ -19,7 +19,7 @@ module dialcache_shadow_conformance {
// One ramped-down caller source and its selected dark C0/source/C1 job.
// Selected rules from C47/C49-C54 govern admission, comparison, fill authority,
// and timeout ownership; C57/C60 cover snapshot age and captured logging.
- // See BEHAVIOR.md: "Generated feature profiles" for fixtures and payloads.
+ // See formal/generated/PROFILES.md (shadow) for fixtures and payloads and BEHAVIOR.md "Generated profiles".
// Each source/read/decode/serialize/write can remain externally pending. This
// profile excludes serving hits, request/local storage, and overlapping jobs.
// `now` is elapsed milliseconds; the wall clock is `now` plus a skew the
diff --git a/formal/replay/bindings.mjs b/formal/replay/bindings.mjs
index e540441c..63c99e05 100644
--- a/formal/replay/bindings.mjs
+++ b/formal/replay/bindings.mjs
@@ -26,15 +26,34 @@ export function profileActions() {
// observation; "wallClock" for core, whose commands are awaited
// request/response but whose wall clock the schedule controls; "none" for
// local-clock, which reports the real process clock that no rule constrains.
+// The fixture and the setup commands a profile's drivers receive before the
+// first step, from the init choice: the one place that knows them, read by
+// the bindings below and by the generated profile view.
+export function fixtureFor(name, initChoice) {
+ if (Object.hasOwn(profiles, name)) {
+ const profile = profiles[name];
+ return typeof profile.fixture === "function" ? profile.fixture(initChoice) : profile.fixture;
+ }
+ if (name === "effects") return effects.fixtureFor(initChoice);
+ return {};
+}
+export function setupFor(name, initChoice) {
+ if (Object.hasOwn(profiles, name)) return profiles[name].setup;
+ if (name === "effects") {
+ return [
+ { op: "faults", value: { holdReads: true, holdLoads: true, holdDumps: true, holdWrites: true } },
+ ...effects.inputsFor({ action: "init", choice: initChoice }, emptyObservation(effects.fixtureFor(initChoice)), { wallMs: 0 }),
+ ];
+ }
+ return [];
+}
+
export function bindTrace(name, raw, path) {
if (Object.hasOwn(profiles, name)) {
const profile = profiles[name];
const trace = parseTrace(raw, path, profile);
- const fixture = typeof profile.fixture === "function"
- ? profile.fixture(trace.steps[0].choice)
- : profile.fixture;
return {
- trace, fixture, setup: profile.setup, observation: "behaviorObservation", settlement: "receipt",
+ trace, fixture: fixtureFor(name, trace.steps[0].choice), setup: setupFor(name), observation: "behaviorObservation", settlement: "receipt",
commands(index, observed, environment) {
const { action, choice } = trace.steps[index];
return action === "init" ? [] : [featureInput(profile, action, choice, observed, environment)];
@@ -72,15 +91,9 @@ export function bindTrace(name, raw, path) {
}
if (name === "effects") {
const trace = effects.parseTrace(raw, path);
- const fixture = effects.fixtureFor(trace.steps[0].choice);
const expected = effects.expectedObservations(trace);
- const initialInput = { action: "init", choice: trace.steps[0].choice };
return {
- trace, fixture, observation: "behaviorObservation", settlement: "receipt",
- setup: [
- { op: "faults", value: { holdReads: true, holdLoads: true, holdDumps: true, holdWrites: true } },
- ...effects.inputsFor(initialInput, emptyObservation(fixture), { wallMs: 0 }),
- ],
+ trace, fixture: fixtureFor(name, trace.steps[0].choice), setup: setupFor(name, trace.steps[0].choice), observation: "behaviorObservation", settlement: "receipt",
commands(index, observed, environment) {
const { action, choice } = trace.steps[index];
const input = { action, ...(choice === undefined ? {} : { choice }) };
diff --git a/formal/tools/README.md b/formal/tools/README.md
index c7b90787..f14c73a7 100644
--- a/formal/tools/README.md
+++ b/formal/tools/README.md
@@ -38,6 +38,7 @@ generated-fixture verification; `validation.mjs` is the list of record.
- [generate-artifacts.mjs](./generate-artifacts.mjs): regenerates every committed artifact (`--write`) or verifies it (`--check`).
- [generated-fixtures.mjs](./generated-fixtures.mjs): the smoke traces, witness fixtures and the lock from `fixture-recipes.json`.
- [generate-key-vectors.mjs](./generate-key-vectors.mjs), [generate-frame-vectors.mjs](./generate-frame-vectors.mjs), [generate-envelope-vectors.mjs](./generate-envelope-vectors.mjs), [generate-invalidation-vectors.mjs](./generate-invalidation-vectors.mjs): one generated vector file each.
+- [generate-catalog-docs.mjs](./generate-catalog-docs.mjs): the generated read views under `formal/generated/` (`PROFILES.md`) from the replay descriptors and the catalogs; `--check` runs in the `audit` lane.
- [witnesses.mjs](./witnesses.mjs): language-neutral witness evaluation over the generated corpus and its baseline.
- [replay-inputs.mjs](./replay-inputs.mjs): adds replay annotations to exported regressions from their explicit input record.
- [explore.mjs](./explore.mjs): a fresh-seed exploration in an isolated source snapshot (`make explore`); `--replay` reproduces a saved run.
diff --git a/formal/tools/generate-catalog-docs.mjs b/formal/tools/generate-catalog-docs.mjs
new file mode 100644
index 00000000..1c04ed3c
--- /dev/null
+++ b/formal/tools/generate-catalog-docs.mjs
@@ -0,0 +1,208 @@
+// Generated read views of the catalogs and the replay descriptors. The JSON
+// catalogs and the descriptor modules stay the source of truth; these pages
+// exist so a reader can see what a profile's drivers do without opening the
+// JavaScript, and so an agent gets the same facts in one file. `--write`
+// regenerates every view under formal/generated/, `--check` fails when a
+// committed view differs from what the sources render (the `audit` lane).
+import { readFileSync, writeFileSync } from 'node:fs';
+import { resolve } from 'node:path';
+import { fileURLToPath } from 'node:url';
+import { profiles as featureProfiles } from '../replay/features.mjs';
+import { effectsDescriptor, inputsFor as effectsInputs, observedFields as effectsObservedFields, project as projectEffects } from '../replay/effects.mjs';
+import { localClockDescriptor, localClockInput } from '../replay/local-clock.mjs';
+import { actionNames as coreActionNames, coreCommands, observationFields as coreObservationFields } from '../replay/core.mjs';
+import { fixtureFor, setupFor } from '../replay/bindings.mjs';
+import { emptyObservation } from '../replay/observation.mjs';
+import { scheduleExecution } from './execution.mjs';
+
+export const root = fileURLToPath(new URL('../../', import.meta.url));
+export const views = { profiles: 'formal/generated/PROFILES.md' };
+const json = (path, directory = root) => JSON.parse(readFileSync(resolve(directory, path), 'utf8'));
+const code = value => `\`${JSON.stringify(value)}\``;
+const text = value => String(value).replaceAll('|', '\\|');
+
+// The replay descriptor of each profile, in one shape: the fixture and the
+// setup commands by init choice (from bindings.mjs, the same functions the
+// coordinator uses), the actions, each decoding a recorded choice into the
+// driver commands for that step, and the observation channels the parser
+// compares.
+export function describeProfile(id) {
+ const effectsRecord = Object.keys(projectEffects({ ...Object.fromEntries(effectsObservedFields.map(field => [field, 0])), calls: [], writeTtls: [], events: [] }));
+ if (id === 'core') {
+ return { kind: 'core', initChoices: undefined, fixture: () => fixtureFor(id), setup: () => setupFor(id),
+ actions: Object.fromEntries(coreActionNames.filter(name => name !== 'init').map(name => [name, { decode: () => coreCommands(name) }])),
+ channels: [{ name: 'o', fields: coreObservationFields, note: 'the model fields observable through the public API' }] };
+ }
+ if (id === 'effects') {
+ return { kind: 'effects', initChoices: [0, 1, 2, 3, 4, 5], fixture: choice => fixtureFor(id, choice), setup: choice => setupFor(id, choice),
+ actions: Object.fromEntries(Object.entries(effectsDescriptor.actions).map(([name, action]) => [name,
+ { choices: action.choices, decode: (choice, observed, environment) => effectsInputs({ action: name, choice }, observed, environment) }])),
+ channels: [{ name: 'o', fields: effectsRecord, note: 'the effects record the parser compares: counters, caller codes, physical write TTLs, the ordered event trail, read contexts and aborts' }] };
+ }
+ if (id === 'local-clock') {
+ return { kind: 'local-clock', initChoices: undefined, fixture: () => fixtureFor(id), setup: () => setupFor(id),
+ actions: Object.fromEntries(Object.entries(localClockDescriptor.actions).map(([name, action]) => [name, { choices: action.choices, decode: choice => localClockInput(name, choice) }])),
+ channels: [{ name: 'o', fields: Object.keys(emptyObservation()), note: 'the shared observation record' }] };
+ }
+ const descriptor = featureProfiles[id];
+ if (!descriptor) throw new Error(`No replay descriptor for profile ${id}`);
+ const channels = [{ name: 'o', fields: Object.keys(emptyObservation()), note: 'the shared observation record' }];
+ if (descriptor.readIO) channels.push({ name: 'io', fields: ['budgets', 'aborted', 'sourceErrors'], note: 'read budgets in dispatch order, aborted read indices, each caller\'s source-error identity' });
+ if (descriptor.diagnosticAge !== undefined) {
+ const ages = descriptor.diagnosticAge === 'none' ? 'no age events are selected' : `ages are the \`${descriptor.diagnosticAge}\` events`;
+ channels.push({ name: 'd', fields: ['ages', 'coalesced', 'fallbackErrors', 'warnings', ...(descriptor.diagnosticConfigErrors ? ['configErrors'] : []), ...(descriptor.diagnosticFutureOffsets ? ['futureOffsets'] : []), ...(descriptor.diagnosticInspections ? ['inspections'] : [])], note: `diagnostics; ${ages}` });
+ }
+ if (descriptor.markerIO) channels.push({ name: 'markers', fields: ['cutoffMs', 'ttlMs'], note: 'one record per observed invalidation marker' });
+ if (descriptor.compressionIO) channels.push({ name: 'compression', fields: ['decompressed', 'fallback_raw'], note: 'one outcome per decode' });
+ if (descriptor.policyErrorIO) channels.push({ name: 'policyErrors', fields: ['layer', 'errorType'], note: 'one record per configuration error' });
+ return { kind: 'features', initChoices: descriptor.initChoices, fixture: choice => fixtureFor(id, choice), setup: choice => setupFor(id, choice),
+ actions: Object.fromEntries(Object.entries(descriptor.actions).map(([name, action]) => [name, { choices: action.choices, decode: (choice, observed, environment) => action.input(choice, observed, environment) }])),
+ channels };
+}
+
+// Decode a choice with probes standing in for the observation and the
+// environment. The observation probe has the shape of the shared record:
+// every counter reads as 1 (one effect so far), every list as empty, and an
+// unknown field is an error; the environment probe reads the wall clock as
+// 0. The keys a decoder touches are reported per choice, so the page can say
+// which decodings depend on the step.
+export function decodeWithProbes(decode, choice) {
+ const touched = new Set();
+ const shape = emptyObservation();
+ const observed = new Proxy({}, { get: (_, key) => {
+ if (typeof key !== 'string') return undefined;
+ if (!Object.hasOwn(shape, key)) throw new Error(`decoder reads an unknown observation field: ${key}`);
+ touched.add(`observation.${key}`);
+ return Array.isArray(shape[key]) ? [] : 1;
+ } });
+ const environment = new Proxy({}, { get: (_, key) => { if (typeof key === 'string') touched.add(`environment.${key}`); return 0; } });
+ const input = decode(choice, observed, environment);
+ return { input, touched: [...touched] };
+}
+
+const range = choices => {
+ if (choices === 'index') return 'any read or loader index';
+ if (!choices?.length) return 'none';
+ const contiguous = choices.every((value, index) => index === 0 || value === choices[index - 1] + 1);
+ return contiguous && choices.length > 2 ? `${choices[0]}..${choices.at(-1)}` : choices.join(', ');
+};
+
+// Consecutive decodings that differ in exactly one numeric field are a
+// counter walking up (an effect index, a loader index); only such a run is
+// abbreviated. Anything else, a payload class per choice or an overlay per
+// choice, is shown in full, because the page is where those are read.
+function singleNumericStep(a, b) {
+ if (typeof a !== 'object' || typeof b !== 'object' || a === null || b === null) return false;
+ const keys = new Set([...Object.keys(a), ...Object.keys(b)]);
+ let differing = 0;
+ for (const key of keys) {
+ if (JSON.stringify(a[key]) === JSON.stringify(b[key])) continue;
+ if (typeof a[key] !== 'number' || typeof b[key] !== 'number') return false;
+ differing++;
+ }
+ return differing === 1;
+}
+
+function renderAction(profile, name, action) {
+ const choices = action.choices === 'index' ? [0] : action.choices ?? [undefined];
+ const examples = choices.map(choice => {
+ try { return { choice, ...decodeWithProbes(action.decode, choice) }; }
+ catch (error) { throw new Error(`${profile}.${name} choice ${choice}: ${error.message}`); }
+ });
+ const show = example => text(example.choice === undefined ? code(example.input) : `${example.choice} → ${code(example.input)}`);
+ const counterWalk = examples.length > 12 && examples.every((example, index) => index === 0 || singleNumericStep(examples[index - 1].input, example.input));
+ let cell = counterWalk ? [...examples.slice(0, 6).map(show), '… one more per choice …', ...examples.slice(-2).map(show)].join('
') : examples.map(show).join('
');
+ const byKey = new Map();
+ for (const example of examples) for (const key of example.touched) byKey.set(key, [...(byKey.get(key) ?? []), example.choice]);
+ for (const [key, keyChoices] of byKey) {
+ const which = keyChoices.length === examples.length ? 'every decoding' : `choice${keyChoices.length === 1 ? '' : 's'} ${keyChoices.join(', ')}`;
+ const meaning = key.startsWith('environment.') ? 'the environment value at the step; shown as 0' : 'the count so far at the step; shown with one so far';
+ cell += `
${which} ${keyChoices.length === 1 || keyChoices.length === examples.length ? 'reads' : 'read'} \`${key}\` (${meaning})`;
+ }
+ return `| \`${name}\` | ${range(action.choices)} | ${cell} |`;
+}
+
+export function renderProfiles({ directory = root } = {}) {
+ const registry = json('formal/catalogs/profiles.json', directory);
+ const execution = scheduleExecution(json('formal/catalogs/execution.json', directory));
+ const witnesses = json('formal/catalogs/coverage-witnesses.json', directory);
+ const implementations = registry.implementations ?? [];
+ const lines = ['# Conformance profiles', '',
+ 'Generated by `node formal/tools/generate-catalog-docs.mjs --write` from',
+ '[profiles.json](../catalogs/profiles.json), [execution.json](../catalogs/execution.json),',
+ '[coverage-witnesses.json](../catalogs/coverage-witnesses.json), the replay descriptors under',
+ '[../replay/](../replay/README.md) (the fixture and setup through `bindings.mjs`, the shared record',
+ 'through `observation.mjs`) and the public runs of each Quint model, which are its replayed',
+ 'regressions. Do not edit; `make audit` fails when this page is stale.', '',
+ 'One section per profile: what the drivers are configured with, which commands each recorded',
+ 'action decodes into, and which observation channels the coordinator compares. A choice is the',
+ 'integer the Quint action records in `input.choice`; the driver command is what the coordinator',
+ 'sends for it. [BEHAVIOR.md](../guides/BEHAVIOR.md) explains the scenario format, the fixture',
+ 'fields and the observation record; [PORTING.md](../guides/PORTING.md) explains what a driver does with them.', ''];
+ lines.push('| Profile | Model | Actions | Sampled histories | Replayed regressions | Required witnesses |', '| --- | --- | --- | --- | --- | --- |');
+ const rows = registry.profiles.map(profile => {
+ const model = execution.models.find(entry => entry.profile === profile.id);
+ const description = describeProfile(profile.id);
+ return { profile, model, description };
+ });
+ for (const { profile, model, description } of rows) {
+ lines.push(`| [${profile.id}](#${profile.id.replace(/[^a-z0-9-]/g, '')}) | [${profile.model.split('/').pop()}](../models/${profile.model.split('/').pop()}) | ${Object.keys(description.actions).length} | ${model?.generate?.traces ?? '-'} | ${model?.replayRegressions?.length ?? 0} | ${(witnesses[profile.id] ?? []).length} |`);
+ }
+ lines.push('');
+ for (const { profile, model, description } of rows) {
+ const claims = implementations.filter(port => port.profiles.includes(profile.id)).map(port => port.id);
+ lines.push(`## ${profile.id}`, '', '| | |', '| --- | --- |',
+ `| Model | [${profile.model}](../models/${profile.model.split('/').pop()}) |`,
+ `| Version | ${profile.version}, inputs \`${profile.inputEncoding}\` |`,
+ `| Smoke trace | [${profile.smoke.split('/').pop()}](./${profile.smoke.split('/').pop()}) |`,
+ `| Ports claiming it | ${claims.join(', ') || 'none'} |`,
+ `| Generation | ${model ? `${model.generate.traces} sampled histories of at most ${model.generate.maxSteps} steps from ${model.generate.maxSamples} samples; ${model.invariants.length} scheduled invariants; ${model.replayRegressions?.length ?? 0} exported regressions` : 'not scheduled'} |`,
+ `| Required witnesses | ${(witnesses[profile.id] ?? []).length} labels in [coverage-witnesses.json](../catalogs/coverage-witnesses.json) |`, '');
+ const initChoices = description.initChoices ?? [undefined];
+ const fixtures = initChoices.map(choice => ({ choice, fixture: description.fixture(choice), setup: description.setup(choice) }));
+ const varies = key => new Set(fixtures.map(entry => JSON.stringify(entry[key]))).size > 1;
+ if (varies('fixture')) {
+ lines.push('### Fixture, by init choice', '', '| Init choice | Fixture |', '| --- | --- |');
+ for (const entry of fixtures) lines.push(`| ${entry.choice} | ${text(code(entry.fixture))} |`);
+ lines.push('');
+ } else {
+ lines.push('### Fixture', '', Object.keys(fixtures[0].fixture ?? {}).length ? text(code(fixtures[0].fixture)) : `The coordinator sends an empty fixture; see [${description.kind}.mjs](../replay/${description.kind}.mjs) for what the driver constructs.`, '');
+ }
+ if (varies('setup')) {
+ lines.push('### Setup commands, by init choice', '', '| Init choice | Setup |', '| --- | --- |');
+ for (const entry of fixtures) lines.push(`| ${entry.choice} | ${entry.setup.map(command => text(code(command))).join('
')} |`);
+ lines.push('');
+ } else if (fixtures[0].setup.length) lines.push('### Setup commands', '', ...fixtures[0].setup.map(command => `- ${text(code(command))}`), '');
+ lines.push('### Actions', '', '| Action | Choices | Driver commands |', '| --- | --- | --- |');
+ for (const [name, action] of Object.entries(description.actions)) lines.push(renderAction(profile.id, name, action));
+ lines.push('', '### Observation channels', '');
+ for (const channel of description.channels) lines.push(`- \`${channel.name}\`: ${channel.fields.map(field => `\`${field}\``).join(', ')}; ${channel.note}.`);
+ lines.push('');
+ }
+ return lines.join('\n').trimEnd() + '\n';
+}
+
+export function checkCatalogDocs({ directory = root } = {}) {
+ const stale = [];
+ for (const [name, path] of Object.entries(views)) {
+ const rendered = name === 'profiles' ? renderProfiles({ directory }) : undefined;
+ let committed;
+ try { committed = readFileSync(resolve(directory, path), 'utf8'); } catch { committed = undefined; }
+ if (committed !== rendered) stale.push(path);
+ }
+ if (stale.length) throw new Error(`Generated views are stale; run node formal/tools/generate-catalog-docs.mjs --write: ${stale.join(', ')}`);
+ return { views: Object.keys(views).length };
+}
+
+export function writeCatalogDocs({ directory = root } = {}) {
+ writeFileSync(resolve(directory, views.profiles), renderProfiles({ directory }));
+ return { views: Object.keys(views).length };
+}
+
+if (process.argv[1] === fileURLToPath(import.meta.url)) {
+ const mode = process.argv[2];
+ if (process.argv.length !== 3 || !['--write', '--check'].includes(mode)) {
+ console.error('Usage: node formal/tools/generate-catalog-docs.mjs --write|--check');
+ process.exitCode = 2;
+ } else console.log(mode === '--write' ? writeCatalogDocs() : checkCatalogDocs());
+}
diff --git a/formal/tools/validation.mjs b/formal/tools/validation.mjs
index 6b89c362..fa9fc37f 100644
--- a/formal/tools/validation.mjs
+++ b/formal/tools/validation.mjs
@@ -21,7 +21,7 @@ export const targetDescriptions = {
'check-rust': 'Rust formatting check, clippy with warnings denied and default tests including the smoke conformance run',
'check-python': 'Python native, protocol, scenario and committed smoke tests with coverage (coverage/python/native.lcov)',
docs: 'Check shared examples and links; generate native API references and the documentation site (Go, Rust and Python required)',
- audit: 'Check source, behavior, feature, Go and generated-fixture freshness inventories and the Quint style caps',
+ audit: 'Check source, behavior, feature, Go, generated-fixture and generated-view freshness inventories and the Quint style caps',
smoke: 'Replay committed Quint-derived fixtures in TypeScript, Go, Rust and Python; no full completion claim',
formal: 'Check every scheduled Quint model, generate the complete corpus and shared witness evidence, then replay TypeScript, Go, Rust and Python',
'formal-check': 'Typecheck and run every scheduled Quint model, its public regressions and the model mutation challenges',
@@ -196,6 +196,7 @@ export function validationPlan(target, { directory = root, environment = process
.map(name => node(`Check ${name}`, `formal/tools/${name}.mjs`))
.concat(node('Verify committed fixture fingerprints', 'formal/tools/generated-fixtures.mjs', '--verify'),
node('Check the Quint style caps', 'formal/tools/check-style.mjs'),
+ node('Check the generated read views', 'formal/tools/generate-catalog-docs.mjs', '--check'),
node('Check conditional fixture regeneration scope', '--test', '.github/scripts/fixture-scope.test.mjs')),
smoke: [tsReplay(false), nativeGo(false), nativeRust(false),
python('Replay committed Python fixtures and scenarios', '-m', 'pytest', 'python/tests/test_conformance.py')],
diff --git a/typescript/test/formal-catalog-docs.test.ts b/typescript/test/formal-catalog-docs.test.ts
new file mode 100644
index 00000000..ec37884c
--- /dev/null
+++ b/typescript/test/formal-catalog-docs.test.ts
@@ -0,0 +1,44 @@
+import { readFileSync } from "node:fs";
+import { describe, expect, it } from "vitest";
+
+const { renderProfiles, describeProfile, decodeWithProbes, checkCatalogDocs, views } = await import(
+ new URL("../../formal/tools/generate-catalog-docs.mjs", import.meta.url).href,
+) as {
+ renderProfiles(options?: { directory?: string }): string;
+ describeProfile(id: string): { actions: Record unknown }>; channels: Array<{ name: string }> };
+ decodeWithProbes(decode: (choice: number, observed: unknown, environment: unknown) => unknown, choice: number): { input: unknown; touched: string[] };
+ checkCatalogDocs(options?: { directory?: string }): { views: number };
+ views: Record;
+};
+const registry = JSON.parse(readFileSync(new URL("../../formal/catalogs/profiles.json", import.meta.url), "utf8")) as { profiles: Array<{ id: string }> };
+
+describe("generated catalog views", () => {
+ it("renders the committed PROFILES.md exactly, so the audit lane can check freshness without Quint", () => {
+ const committed = readFileSync(new URL(`../../${views.profiles}`, import.meta.url), "utf8");
+ expect(renderProfiles()).toBe(committed);
+ expect(checkCatalogDocs()).toEqual({ views: 1 });
+ });
+
+ it("is deterministic and covers every registered profile and every descriptor action", () => {
+ const rendered = renderProfiles();
+ expect(renderProfiles()).toBe(rendered);
+ for (const { id } of registry.profiles) {
+ expect(rendered, id).toContain(`\n## ${id}\n`);
+ for (const action of Object.keys(describeProfile(id).actions)) expect(rendered, `${id}.${action}`).toContain(`| \`${action}\` |`);
+ }
+ });
+
+ it("decodes with probes that report what a decoder reads at the step", () => {
+ const { actions } = describeProfile("recovery");
+ expect(decodeWithProbes(actions.releaseLoad!.decode, 0)).toEqual({ input: { op: "release", effect: "load", index: 0 }, touched: ["observation.loads"] });
+ expect(decodeWithProbes(actions.advance!.decode, 1000)).toEqual({ input: { op: "advance", ms: 1000 }, touched: [] });
+ const recoveryRead = describeProfile("recovery-read");
+ expect(decodeWithProbes(recoveryRead.actions.seed!.decode, 17).touched).toEqual(["environment.wallMs"]);
+ });
+
+ it("lists the observation channels a profile's descriptor declares", () => {
+ expect(describeProfile("recovery-read").channels.map(channel => channel.name)).toEqual(["o", "io", "markers", "compression"]);
+ expect(describeProfile("policy").channels.map(channel => channel.name)).toEqual(["o", "policyErrors"]);
+ expect(describeProfile("core").channels.map(channel => channel.name)).toEqual(["o"]);
+ });
+});