diff --git a/docs/capabilities/invariants.md b/docs/capabilities/invariants.md new file mode 100644 index 0000000..fa06dcc --- /dev/null +++ b/docs/capabilities/invariants.md @@ -0,0 +1,281 @@ +# The cross-cutting rules the 51 capabilities imply + +Hand-written. The one file in this directory that is not generated. + +`docs/spec.md` states 51 capabilities one at a time. Twelve rules run across all +of them, and no capability's definition of done states any of these. A rule +broken here breaks many capabilities at once, which is why it does not show up +as one failing criterion. + +Each rule carries a mark. A rule split between what is written down and what +is not carries both, and says which half is which. + +| mark | meaning | +| --- | --- | +| `explicit` | a source states the rule and names its enforcement point | +| `implied` | capabilities depend on it, no source states it, and the code decides it case by case | +| `unresolved` | the sources do not answer it. A product question, not a defect | + +Nothing wanted is invented where the sources are silent. An `unresolved` rule +needs the owner, not a commit. + +Evidence is `docs/architecture/findings.md` for the code reading, +`docs/evals/2026-08-26-capability-baseline.md` for what ran, and the file itself +where the rule is written down. + +--- + +## 1. Continuity across turns and across reaches + +**Implied.** Continuity within one reach is built. Continuity across reaches is +not, and nothing states whether it should be. + +`dialogue.NewPersistentSessionStore` carries follow-up slots across turns and +across a restart. The clarify store is a per-reach stack and is deliberately not +persisted (`findings.md` 7.5, Vikunja #385). + +Across reaches there is no shared thread. `mavweb` hardcodes one conversation id +for the whole web reach, which is not continuity but the absence of separation: +a clarify parked by one probe was still parked for the next, and the first field +run had to be discarded for it (`docs/capabilities/README.md`, "Two things the +harness learned the hard way"). + +**What breaks:** a question asked by voice and answered on the web has no thread +to attach to. No capability's DoD asks for one, so nothing scores this. + +**The product question:** is a conversation per reach, or one conversation the +reaches are windows onto? + +## 2. Memory and correction semantics + +**Explicit for the row, implied for the namespace.** + +Supersede is written down and enforced: a correction points `voids_id` at the row +it replaces, and valid-time is the `ts` column (`internal/store/schema.sql`). +`CLAUDE.md` states the embedder contract, `EmbedQuery` and `EmbedPassage`, and +calling plain `Embed` on a note is named as a bug. + +Who may write a key is not written anywhere. `facts` has nine writers and no +owner, and two of them store things that are not observations: `crawl:hash:*` is +a fetch watermark and `cooldown:` is a tuning parameter (`findings.md` +1.1). The `source` column keeps them apart by convention, and the `CHECK` +constraint covers only `kind`. `notes` has six writers, one of them a LAN scan +whose records then compete by cosine similarity with things he said +(`findings.md` 1.2). + +**What breaks:** recall answers a question about him with a fetch watermark. +`queryFactByKey` reads the same table back as an answer. + +## 3. Current context and presence + +**Explicit and partly false at runtime.** + +Presence is one hysteresis bucket rewritten each tick (`state.presence_state`), +and the dispatcher's routing table is a pure function of severity and presence. + +One input is permanently wrong. `loop.State.CalendarBusy` reads +`facts(kind=env, source=caldav:*)` and `mavcaldav` is commented out of +`docker-compose.yml`, so the "do not nag mid-meeting" suppressor is always false +(`findings.md` 8.2). The compose file says so, which makes it a known gap. + +**What breaks:** every interruption decision that should have deferred to a +meeting. It fails open, toward interrupting. + +## 4. Proactive attention + +**Explicit, and the one prohibition is stated.** + +`CLAUDE.md`: no automatic attention-to-action path. Digestion may summarise +Praxis and may not call Hexis. At most one nudge candidate per tick, and the +restraint gate is a pure function over the rule set (`core.rules`). + +Restraint is decided twice on purpose (`findings.md` 2.3), and blocked candidates +are held durably in `digest_entries` rather than dropped. + +**What breaks:** nothing observed. This is the best-specified rule in the list. + +## 5. Interruption policy + +**Explicit for the choice, implied for the outcome.** + +`docs/handler-wiring.md` owns the dispatch decision, and the table over +(severity, presence) is pure. Delivery intent is recorded in +`delivery_attempts` before the external send, so a crash leaves a pending row +rather than a lost one. + +What is not stated is what a held nudge owes the user later. `digest_entries` +holds blocked candidates and two separate mechanisms carry the word digest +(`findings.md` 2.4). Nothing says when a held item expires instead of +resurfacing. + +**The product question:** does a held nudge have a shelf life? + +## 6. Clarification and follow-up ownership + +**Implied.** Who owns an open question, and for how long, is decided by three +components and stated by none. + +`runTurn` step 1 fires an expired-clarify notice, the clarify store is a +per-reach stack, and the pre-route ladder may claim the turn before routing +(`findings.md` 2.2). A restart drops a parked request silently, because the +notice path reads the store that is gone (`findings.md` 7.5). + +Measured: one park survived five consecutive turns, turns 9 through 13, and was +released by a path other than `отмена` +(`docs/evals/2026-08-26-capability-baseline.md`). + +**What breaks:** a question she asked stays open across unrelated turns, and +neither the ladder nor the store says whose job it is to close it. + +## 7. Degradation and honesty + +**Explicit as a rule, and the rule contradicts itself in practice.** + +`CLAUDE.md` states both halves. Fall back silently when the fallback would only +do the job better. Name the gap when the resident model cannot do the job at +all. `docs/spec.md` writes every v1 DoD at "voice-reachable and honest", where +honest means naming the gap and never filling it with a guess. + +Four silent degradations stack on one turn: workstation model to resident model, +CW2 to mavsttd, routing heads to LLM router to classifier, and search to Kiwix to +a named page to the model's own weights (`findings.md` 8.1). Each is argued +individually. Together a reply can be the resident model routing a worse +transcript with the classifier as a floor, answering from its weights, and +nothing in the reply distinguishes that from the best case. + +**What breaks:** the boundary between "only better" and "cannot do the job" is +not drawn anywhere, so the stack decides it by accident. + +**The product question:** at what depth of fallback does silence stop being +honest? + +## 8. Authority and confirmation + +**Unresolved, and this is the largest hole in the list.** + +Two systems each answer half and never meet. `internal/auth` answers who may +carry what authority and does not bind the reactive turn path at all +(`findings.md` 6.3). `internal/tool` answers what effect a capability has and +what proof it demands, runs on every act, and is not keyed on the reach +(`findings.md` 6.3b). Neither has the other's reach. + +Two representations of reach exist and both are ignored. +`internal/voice/server.go:198` defaults an empty `p.Surface` and a +client-asserted one survives to a handler that never reads it. `:148` hardcodes +`SurfacePCClient` for every connection. `req.Surface` is request payload on a +plaintext wire with no auth, so any client can claim `pc_client`. It must not +become an authorization input as it stands. + +One path has no gate at all. `praxisItemAction.handle` +(`cmd/mavend/ecosystem_acts.go:158`) reads `dec.Slots.Value` and calls straight +through. Acknowledge, resolve, ignore and pin are remote mutations that run on +first hearing, with no tier and no confirm turn. + +`CLAUDE.md` states the rule the code does not implement: LLM output is not +authorization, and a confirmation binds capability id, target entity, arguments, +requester and expiry. + +**What breaks:** no one can currently state the authority property of a Maven +turn. `origin × effect × evidence → permit` is the target shape and nothing +computes it. + +## 9. Privacy boundaries + +**Explicit, and it is the best-enforced rule here.** + +`CLAUDE.md`: the owner's data first, then the world. His notes and facts are +never search input, only the utterance leaves the box. The personal boundary is a +query source with `boundary: true`, and `queryWalk` reads +`Decision.SourceAnchored` for that source and no other. + +The exception is deliberate and recorded. The boundary guesses, so naming +`SourceWorld` drops it, and only a stage 0 grammar may do that (owner's call, +V-666). No component reads another component's database, and Praxis attention +comes over HTTP rather than from its SQLite file. + +**What breaks:** nothing observed. The one caveat is that `queryWalk` takes +sources out and moves none, which is the safety argument, and it holds only as +long as the table's order stays load-bearing. + +## 10. Learning from outcomes + +**Unresolved.** One loop exists, two are specified with no package, and nothing +says whether learning is a product goal. + +Built: `state.nudges` is the restraint memory and the only input to the tick +loop's autotune, which writes `cooldown:` back into `facts`. +`state.routing_labels` holds owner corrections of a route. + +Not built: `learning-the-style` and `learning-from-mistakes` have no package and +no component. `docs/spec.md` gives each a DoD written at what done would look +like. Both score `code_present: no`. + +One criterion passes by absence. "No model weights change and no training set is +built" is a negative, and nothing being built satisfies it. The generator reports +this as an anomaly rather than counting it as progress. + +**The product question:** is behavioural learning wanted, or is the negative +criterion the whole of the intent? + +## 11. Capability composition + +**Implied and absent.** Every capability is specified alone and the turn is +single-claim by construction. + +`core.action_table` dispatches one intent to one handler, and a handler returning +the empty string hands the turn on. `queryWalk` stops at the first source that +claims. Two independent arbitrations already decide one turn, with a third +running before both (`findings.md` 2.1, 2.2). + +`command-chaining` fails all three of its criteria with reason `wiring missing`. +The `chain` in `internal/router` is the world chain and the source chain, not +command chaining. + +`internal/claim` is the beginning of a vocabulary for this and is called by +nothing (`findings.md` 6.1). It carries a live defect: `Claim.Coverage` returns +1.0 for a claim that extracted nothing, because `claimSpans` includes +`Slots.Text` unconditionally and `fillSlots` backfills the raw utterance into +`Text` (`findings.md` 6.3d). + +**What breaks:** "напомни мне и запиши это" performs one of the two and says +nothing about the other. + +**The product question:** what is the single unit that competes for a turn. This +is one of the three the freeze was called to answer. + +## 12. Persistence across restart + +**Implied.** Four stores made four different choices and no source states the +rule. + +| state | survives a restart | evidence | +| --- | --- | --- | +| dialogue sessions | yes | `dialogue.NewPersistentSessionStore` | +| clarify store | no, deliberately | `findings.md` 7.5, Vikunja #385 | +| decision ring | no, in-memory bounded at 25 | `internal/decision/ring.go:11` | +| routing traces | yes, retained 14 days | `CLAUDE.md` | +| tick memo | no, in-process and argued for one field | `findings.md` 7.4 | +| surfaced items | no, and no TTL | `findings.md` 7.3 | + +Two of these are principled. The decision ring holds his words and is bounded on +purpose. The clarify store's reasoning is filed. The other four are not decided +anywhere. + +**What breaks:** less than it looks. `surfacedItems` has no TTL, and the source +comment argues that a stale ordinal resolves to an item Praxis reports as already +acknowledged, which is harmless because Praxis is the arbiter (`findings.md` +7.3). The cost is that the same absence of a written rule produced one argued +choice and three unargued ones. + +--- + +## What this file is for + +Session 2 step 2 of `docs/plans/26-capability-ledger-and-baseline.md`. It feeds +`docs/capabilities/gaps.md`, where every architecture concern must name the +capability or invariant it affects. + +Four rules are `unresolved` and they are the owner's, not a commit's: authority +and confirmation, learning from outcomes, capability composition, and the shelf +life of a held nudge. Two of the three questions the freeze was called to answer +appear here as invariant 8 and invariant 11.