Merge pull request 'E1/R7 assertion spec + arc status after Phases A and B (closes the Opus share)' (#118) from docs/e1-r7-assertion-spec into main
Reviewed-on: #118
This commit is contained in:
commit
bc8276d693
3 changed files with 299 additions and 6 deletions
|
|
@ -10,6 +10,50 @@ a memory or a chat instruction, the plan of record and `AGENTS.md` win.
|
|||
|
||||
---
|
||||
|
||||
## 0. Status at handoff — 2026-07-25, Opus units complete
|
||||
|
||||
The three Opus units are done and pushed. **Read the plan of record's AMENDED
|
||||
block first**: Phases A and B falsified four premises, one of which reorders the
|
||||
remaining work.
|
||||
|
||||
| Unit | Branch | State |
|
||||
|---|---|---|
|
||||
| A — negative-curriculum epistemology | `docs/adr-negative-curriculum` | ADR-0264, pushed. Proposed, awaiting ratification |
|
||||
| B — volume-honesty invariant | `test/volume-honesty-invariant` (stacked on A) | pushed. 13 tests, mutation-checked, in `smoke` |
|
||||
| E1 Opus half — the R7 assertion | `docs/e1-r7-assertion-spec` | this branch. `E1-R7-ASSERTION-SPEC.md` |
|
||||
|
||||
Merge order: **A, then B** (B is stacked on A), then E1's spec — merge-commit, not
|
||||
squash. E1's spec branch is independent of A/B and can merge in any order.
|
||||
|
||||
**What changed for the Sonnet units.** Three things, all of which make the
|
||||
remaining work different from §4 as originally written:
|
||||
|
||||
1. **A new implementation unit precedes everything: ADR-0264 R5–R7, query-scoped
|
||||
premise compilation.** `MAX_PREMISE_SENTENCES = 16` caps a family at 16 chains;
|
||||
at 17 the band declines every question, including ones that work today. Until
|
||||
this lands, no curriculum band can earn a license at any corpus size, so
|
||||
building Phase C first would produce a correct instrument reporting that every
|
||||
band is at its ceiling. R5 is fully specified and verified verdict-identical
|
||||
over 8,520 questions — it is a loud unit (the physics lane pins every verdict).
|
||||
2. **Phase F retargets to `philosophy_theology · modal`.** `physics · modal` has a
|
||||
hard ceiling of 480 against a 657 threshold. Do not author physics modal volume.
|
||||
3. **Phase C's producer must call the Phase B audit.** `AUDIT_SOURCES` in
|
||||
`tests/test_volume_honesty.py` carries a declared `None` for
|
||||
`curriculum_serve` that fails the moment its ledger exists. That is deliberate:
|
||||
it is the forcing function against repeating the deduction pattern.
|
||||
|
||||
**Standing "do not fix" — the deduction ledger exposure.** 21 of 25 ratified
|
||||
`deduction_serve` bands do not clear θ_SERVE on distinct evidence (worst: 28
|
||||
distinct cases inflated to 720 committed). It is measured, pinned in both
|
||||
directions, and **must not be repaired by any unit below.** The ledger is
|
||||
SHA-sealed, ratified, and gating a live flag; re-sealing it is Shay's ratification.
|
||||
If a unit's work makes `tests/test_volume_honesty.py` fail, that is a real signal
|
||||
— report it, do not update the inventory to match.
|
||||
|
||||
**Revised order: E2 → R5–R7 → C → D → E1(code) → parity.**
|
||||
|
||||
---
|
||||
|
||||
## 1. The tiering criterion — read this first, it is the whole rationale
|
||||
|
||||
Units are **not** assigned by difficulty, and not by model prestige. The evidence
|
||||
|
|
@ -49,11 +93,12 @@ and escalate (§6). That is not a failure — it is the mechanism working.
|
|||
|
||||
| Unit | Phase | Owner | Failure mode |
|
||||
|---|---|---|---|
|
||||
| Negative-curriculum epistemology ADR | A | **Opus** | silent |
|
||||
| Volume-honesty invariant (tests first) | B | **Opus** | silent |
|
||||
| R7 assertion — *what* to assert | E1 | **Opus** | silent |
|
||||
| Negative-curriculum epistemology ADR | A | **Opus** ✅ | silent |
|
||||
| Volume-honesty invariant (tests first) | B | **Opus** ✅ | silent |
|
||||
| R7 assertion — *what* to assert | E1 | **Opus** ✅ | silent |
|
||||
| Articulation feasibility study | §6 of plan | **Opus** | silent |
|
||||
| `assert_corpus_sound` rename | E2 | **Sonnet** | loud |
|
||||
| **Query-scoped premise compilation (R5–R7)** | **new, gates C/D/F** | **Sonnet** | loud |
|
||||
| Practice producer implementation | C | **Sonnet** | loud |
|
||||
| `core proposal-queue reseal` verb | D | **Sonnet** | loud |
|
||||
| R7 code move + suite registration | E1 | **Sonnet** | loud |
|
||||
|
|
@ -141,8 +186,37 @@ Every unit here has a loud failure mode. You are expected to iterate against the
|
|||
gate until it is green, not to re-derive design. If a unit seems to require a
|
||||
design decision, that is the signal in §6.
|
||||
|
||||
**Order: E2 → C → D → E1(code) → parity.** E2 first because Phase C adds a third
|
||||
`assert_corpus_sound` caller and renaming after that is strictly more work.
|
||||
**Order: E2 → R5–R7 → C → D → E1(code) → parity.** E2 first because Phase C adds a
|
||||
third `assert_corpus_sound` caller and renaming after that is strictly more work.
|
||||
R5–R7 second because nothing downstream can earn anything until it lands (§0).
|
||||
|
||||
### R5–R7. Query-scoped premise compilation — **do this before C and D**
|
||||
|
||||
`teaching/curriculum_premises.py::compile_premises` emits *every* chain in the
|
||||
family, and `read_verb_argument` refuses past `MAX_PREMISE_SENTENCES = 16`. So a
|
||||
17-chain family answers nothing. Three rules, all specified in ADR-0264 §2:
|
||||
|
||||
- **R5** — compile a scope that is a **superset of the query-atom rows** and a
|
||||
subset of the family. Default: **term incidence** (rows whose subject or object
|
||||
is one of the query's two terms). If that would still exceed the cap, narrow to
|
||||
the query-atom rows. Never truncate arbitrarily, and never refuse for size.
|
||||
- **R6** — an **empty scope is UNKNOWN**; only an empty *family* is the
|
||||
`empty_curriculum` refusal. Get this wrong and 8,463 of 8,520 questions flip
|
||||
from `unknown` to `declined`.
|
||||
- **R7 (curriculum)** — `premise_count` keeps reporting **family size**, because it
|
||||
is user-visible. Carry the compiled-scope size as a separate field. (Unrelated to
|
||||
audit-ledger R7 in E1 — same numeral, different register.)
|
||||
|
||||
**Why this is loud, and why it is not the ADR-0261 §5.1 premise-dropping sin.**
|
||||
Narrowing is verdict-*identical*, not merely sound: each compiled premise mints one
|
||||
independent propositional atom, so a scope containing the query atom decides the
|
||||
query exactly as the full family does. Verified over 8,520 routable questions with
|
||||
zero mismatches (`docs/research/curriculum-premise-scope-2026-07-25.md` probe 3).
|
||||
Gold is preserved: physics stays `entailed 14 / unknown 12 / declined 6`.
|
||||
|
||||
**Gate:** the `curriculum_serve` lane at `wrong=0`, and the 20 tests in
|
||||
`tests/test_curriculum_serve.py`. If any verdict moves, stop — the equivalence
|
||||
argument has a hole and that is escalation §6.3.
|
||||
|
||||
### E2. `assert_corpus_sound` rename
|
||||
Two functions, one name: `evals/deduction_serve/practice/gold.py:1163` (no args,
|
||||
|
|
@ -155,6 +229,18 @@ contract). Not a missing contract — a name collision, flagged in
|
|||
`evals/deduction_serve/practice/` topology **exactly**: producer in `evals/`,
|
||||
sealed artifact next to its reader in `chat/data/`.
|
||||
|
||||
> **Mirror the topology, NOT the volume strategy.** The deduction producer sets a
|
||||
> flat `CASES_PER_BAND = 720` and fills the quota by cycling a template ×
|
||||
> vocabulary space that is as small as 28 distinct instances — which is the
|
||||
> exposure Phase B measured. Follow the **`estimation`** producer instead
|
||||
> (`evals/determination_estimation`): 660 *distinct* cases per class, zero repeats,
|
||||
> chosen just above the 657 a perfect record needs. Emit at most one case per
|
||||
> distinct query atom (ADR-0264 R9) and let the count fall where the corpus puts
|
||||
> it. Then register the producer in `AUDIT_SOURCES`
|
||||
> (`tests/test_volume_honesty.py`) — the declared `None` there fails as soon as
|
||||
> `chat/data/curriculum_serve_ledger.json` exists, which is how this unit is
|
||||
> stopped from repeating the pattern.
|
||||
|
||||
**Reuse, do not rewrite** — this is why the unit is small:
|
||||
- `evals/curriculum_serve/oracle.py` — already an independent decision procedure;
|
||||
wrap as the gold tether.
|
||||
|
|
@ -241,7 +327,9 @@ available here.
|
|||
- Branch **and** worktree per unit; both deleted immediately after merge.
|
||||
- Pre-push gate in-worktree on canonical **Python 3.12.13** with
|
||||
`uv sync --locked`: `core test --suite smoke -q` then `--suite deductive -q`.
|
||||
Baselines at arc start: **smoke 555**, **deductive 285**.
|
||||
Baselines: **smoke 555 / deductive 285** at arc start; **smoke 569** after
|
||||
Phases A+B (+1 from ADR-0264 joining the derived ADR pin, +13 from
|
||||
`tests/test_volume_honesty.py`).
|
||||
- `[Verification]:` line in every PR description, naming the interpreter.
|
||||
- One PR per coherent unit. Compare-URL PRs; **Shay merges** — no merge
|
||||
automation, and green PRs sit until explicit authorization.
|
||||
|
|
|
|||
|
|
@ -0,0 +1,167 @@
|
|||
# E1 / audit-ledger R7 — the assertion spec
|
||||
|
||||
**Arc:** curriculum-license-loop Phase E1 · **Written:** 2026-07-25 · **By:** Opus 5
|
||||
**For:** the Sonnet unit "E1 (code half). R7" in `DIVISION-OF-WORK.md` §4
|
||||
**Read first:** `docs/specs/runtime_contracts.md` §"Open, tracked as audit-ledger R7"
|
||||
|
||||
The code move is specified — the contract already says *"defer the single sink
|
||||
emission to the pipeline serve boundary."* What was never specified is **what to
|
||||
assert**, and the default sink is `None`, so nothing exercises this path. A wrong
|
||||
move is therefore silent, which is why the assertion set is written here before
|
||||
any code moves. This is the same seam that regressed silently for two days in the
|
||||
#96 register-axis incident.
|
||||
|
||||
Do not improvise the assertions. If implementing reveals that one of them is
|
||||
wrong, that is escalation condition §6.3 — say so with the specifics rather than
|
||||
adjusting the assertion to match the implementation.
|
||||
|
||||
---
|
||||
|
||||
## 1. The defect, precisely
|
||||
|
||||
`ChatRuntime.chat` seals a `TurnEvent` and emits it to the sink inline
|
||||
(`chat/runtime.py:3157`, and the refusal-stub path at `:2490`).
|
||||
`CognitiveTurnPipeline` then applies the surface authority and the canonical
|
||||
`trace_hash` **after** `chat` returns, back-stamping both onto `turn_log[-1]`:
|
||||
|
||||
```
|
||||
core/cognition/pipeline.py:823 runtime.finalize_turn_trace_hash(trace_hash)
|
||||
core/cognition/pipeline.py:833 runtime.finalize_turn_surface(surface, articulation_surface)
|
||||
```
|
||||
|
||||
So `turn_log[-1]` ends up correct and **the durable telemetry stream does not**.
|
||||
The sink holds a stale `surface` and a stale `trace_hash`. `turn_log` is repaired;
|
||||
the thing that persists is not.
|
||||
|
||||
## 2. Mechanism — mirror `_pending_reboot_payload`, do not invent one
|
||||
|
||||
A stage-then-flush pattern already exists in this class: `_pending_reboot_payload`
|
||||
is buffered and flushed in `attach_telemetry_sink` (`chat/runtime.py:1486-1489`).
|
||||
Mirror its shape. Three rulings make the difference between mirroring it and
|
||||
reintroducing the bug:
|
||||
|
||||
**M1 — Stage an INDEX, not a copy of the event.** Stage the position in
|
||||
`turn_log`; at flush time, format `self.turn_log[idx]`. A captured `TurnEvent`
|
||||
object would be the pre-override snapshot, which is the defect with extra steps.
|
||||
Re-reading `turn_log` picks up both back-stamps for free and cannot go stale.
|
||||
|
||||
**M2 — `attach_telemetry_sink` must NOT flush a staged turn event.** This is the
|
||||
opposite of what it does for `_pending_reboot_payload`, and the asymmetry is
|
||||
load-bearing: the reboot payload is already final when buffered, whereas a staged
|
||||
turn event is *mid-flight* and may not yet be back-stamped. Flushing on attach
|
||||
would emit the pre-override event and silently restore R7. Leave the reboot flush
|
||||
exactly as it is.
|
||||
|
||||
**M3 — The runtime cannot detect whether a pipeline will run**, because
|
||||
`CognitiveTurnPipeline` wraps the runtime (`self.runtime`) rather than the reverse.
|
||||
So deferral must be **opt-in and explicit**: the pipeline tells the runtime it
|
||||
owns the emission, and the runtime emits inline otherwise. A runtime used directly
|
||||
(`ChatRuntime.chat` with no pipeline — which the eval and demo paths do) must
|
||||
behave byte-identically to today, including emission timing.
|
||||
|
||||
## 3. Invariants to assert
|
||||
|
||||
### I1 — Exactly once, on every path
|
||||
Each `TurnEvent` reaches the sink exactly once: never zero (a deferred event that
|
||||
nobody flushed), never twice (pipeline flush plus a fallback). Assert a count, not
|
||||
merely presence. Both emission sites are in scope — the main path (`:3157`) and
|
||||
the refusal-stub path (`:2490`).
|
||||
|
||||
### I2 — The emitted event is the POST-override event
|
||||
For a turn where the pipeline overrides the surface, the single emitted JSONL line
|
||||
must carry:
|
||||
|
||||
- `surface` == the pipeline's served surface (`pipeline.run().surface`)
|
||||
- `articulation_surface` == the pipeline's resolved articulation surface
|
||||
- `trace_hash` == the pipeline's computed `trace_hash` (non-empty)
|
||||
|
||||
Construct the test so the override actually fires — a turn where
|
||||
`TurnEvent.surface != pipeline.run().surface` under today's code. If the fixture
|
||||
does not produce a divergence, the test proves nothing; assert the divergence
|
||||
exists on the pre-fix code path, or pin a case that is known to decorate.
|
||||
|
||||
### I3 — `trace_hash` is verified by REPLAY, never by recomputation
|
||||
Assert the emitted `trace_hash` equals the `trace_hash` of a fresh pipeline replay
|
||||
of the same input. Do **not** rebuild it from the emitted record's fields — the
|
||||
contract states recomputation from a turn record is unsupported *and correct to be
|
||||
so*, because `TurnEvent` does not carry `hash_surface`. A test that recomputes
|
||||
would encode the opposite of the ruling.
|
||||
|
||||
### I4 — No pipeline, no change
|
||||
A `ChatRuntime` used directly emits exactly as it does today: same content, same
|
||||
timing relative to the `chat()` return. Assert against the current behaviour, not
|
||||
against the deferred behaviour.
|
||||
|
||||
### I5 — Exception safety
|
||||
If the pipeline raises between `chat()` returning and the serve boundary, the
|
||||
staged event must still reach the sink. Wrap the flush so it runs on the failure
|
||||
path (`try/finally` at the serve boundary), and test it with a fault injected
|
||||
after `chat()` — otherwise a pipeline error silently swallows a telemetry record,
|
||||
which is a worse failure than the one being fixed.
|
||||
|
||||
### I6 — Stream order stays monotone in turn number
|
||||
A durable stream's consumers may rely on order. Two specific orderings:
|
||||
|
||||
- turn events appear in turn order;
|
||||
- a correction event for turn *N* (`_emit_correction_event`,
|
||||
`chat/runtime.py:3261`) appears **after** turn *N*'s event. Note
|
||||
`_emit_correction_event` runs at `:3255` and then calls `self.chat(...)` at
|
||||
`:3259`, so the staged-event flush must be ordered against it deliberately
|
||||
rather than by accident.
|
||||
|
||||
### I7 — At most one event in flight
|
||||
Staging a second event while one is unflushed must flush the first, not drop it.
|
||||
This bounds the worst case to "the final turn of a session whose pipeline raised
|
||||
before the flush," which I5 already covers. Assert the two-turns-deferred case
|
||||
explicitly.
|
||||
|
||||
### I8 — Default deployment unaffected
|
||||
With `sink is None` (the default) nothing changes: no new work, no surface change,
|
||||
`turn_log` back-stamping identical. This is what makes the change safe to land
|
||||
without a flag.
|
||||
|
||||
## 4. Out of scope — do not fold these in
|
||||
|
||||
- **`hash_surface` on `TurnEvent`** (plan §5, decision 4C). R7 does **not** depend
|
||||
on it: R7 makes the stream carry the *pipeline's* `trace_hash`, which is a
|
||||
transport fix. Whether a consumer can recompute it is a separate ruling and is
|
||||
still open.
|
||||
- **The `trace_hash` / `finalize_turn_surface` divergence itself.** The contract
|
||||
says these serve different invariants and are correct to differ. R7 is only
|
||||
about which of the two the sink receives.
|
||||
- **Changing what `TurnEvent` contains.** Fields stay as they are.
|
||||
- **The discovery-candidate sink and the articulation sink.** Different sinks,
|
||||
different lifecycles. `_emit_discovery_candidates` already back-stamps via
|
||||
`finalize_turn_trace_hash`; leave it.
|
||||
|
||||
## 5. Definition of done
|
||||
|
||||
1. All eight invariants asserted in a new test module, registered in a **curated
|
||||
suite** in `core/cli_test.py` (§4 of `DIVISION-OF-WORK.md` — two files from
|
||||
PR #113 landed in no suite and ran only under `full`, which gates nothing).
|
||||
2. The seven existing sink test files still pass unchanged:
|
||||
`test_telemetry_sink.py`, `test_telemetry_fanout_and_summary.py`,
|
||||
`test_adr_0158_reboot_event.py`, `test_register_telemetry.py`,
|
||||
`test_anchor_lens_telemetry.py`, `test_correction_telemetry.py`,
|
||||
`test_workbench_operator_telemetry.py`. If one of them has to change, that is a
|
||||
behaviour change outside I1–I8 — stop and report it.
|
||||
3. `docs/specs/runtime_contracts.md` — the "**Open**, tracked as audit-ledger R7"
|
||||
paragraph becomes closed, naming the commit. Leave the surrounding
|
||||
`trace_hash`-vs-`finalize_turn_surface` explanation intact; only the R7
|
||||
paragraph is resolved.
|
||||
4. The `NOTE:` block in `finalize_turn_surface`'s docstring
|
||||
(`chat/runtime.py:1238-1244`) is removed, since it documents the limitation
|
||||
being fixed. `finalize_turn_trace_hash` carries the same limitation — check
|
||||
whether its docstring needs the same edit.
|
||||
5. Pre-push gate green in-worktree on canonical 3.12.13:
|
||||
`smoke` and `deductive`. Baselines at the time of writing: smoke **569**,
|
||||
deductive **285**.
|
||||
|
||||
## 6. Why this is an Opus-then-Sonnet split
|
||||
|
||||
Deciding M1–M3 and I5–I7 is where a mistake is invisible: a captured-event stage
|
||||
(M1), an attach-time flush (M2), or a missing `finally` (I5) all produce a green
|
||||
suite and a telemetry stream that is quietly wrong — which is precisely the
|
||||
original defect's failure mode. Once those are fixed in writing, the
|
||||
implementation has a red/green gate at every step, and iterating against it needs
|
||||
no design authority.
|
||||
|
|
@ -3,6 +3,44 @@
|
|||
**Date:** 2026-07-25 · **Status:** ACTIVE · **Base:** main @ `0a26787f`
|
||||
(post ADR-governance pin, PR #114)
|
||||
|
||||
> ## AMENDED 2026-07-25 after Phases A and B — read this before §1
|
||||
>
|
||||
> Phases A and B are complete (ADR-0264; `core/reliability_gate/evidence.py` +
|
||||
> `tests/test_volume_honesty.py`). Both falsified premises of the plan below. The
|
||||
> original text is preserved unchanged; this block is what supersedes it.
|
||||
>
|
||||
> **1. §3's first content target was wrong.** `physics · modal` was chosen for
|
||||
> having the most ratified chains (9). Chain count is not the constraint —
|
||||
> *taught vocabulary* is, because a question routes only if exactly one served
|
||||
> subject's vocabulary holds both terms. Physics has 16 lemmas, so that band's
|
||||
> entire question space is 480 — below the 657 threshold with every possible
|
||||
> question counted, and no amount of authoring raises it. **8 of 11 bands are
|
||||
> structurally unable to reach 657.** New target: **`philosophy_theology · modal`**
|
||||
> (149 exclusive lemmas ⇒ ceiling 44,104, same 8-chain start). ADR-0264 §4.2.
|
||||
>
|
||||
> **2. §1's "the build is modest" understates it, and §4's phase order is wrong.**
|
||||
> `MAX_PREMISE_SENTENCES = 16` caps a family at 16 chains — at 17 the band declines
|
||||
> *everything*, including questions that work today. So ADR-0262 §5.1's remedy
|
||||
> (author ≈219 relations) destroys the capability at row 17. A band therefore has
|
||||
> ≤16 entailed cases against a 657 threshold, and **no curriculum band can earn
|
||||
> SERVE until premise compilation is query-scoped.** A new implementation phase
|
||||
> (ADR-0264 R5–R7) precedes all content work. ADR-0264 §4.1.
|
||||
>
|
||||
> **3. Authoring a negative today serves a confident wrong "Yes."** Not UNKNOWN —
|
||||
> `polarity` is read by nothing, so the affirmative sentence is compiled. The
|
||||
> independent oracle ignores the field too, so gold agrees and `wrong=0` stays
|
||||
> green. ADR-0264 Fact 1 / R1–R4, R8.
|
||||
>
|
||||
> **4. §4's Phase B found the exposure already live elsewhere.** 21 of the 25
|
||||
> ratified `deduction_serve` bands do not clear θ_SERVE on *distinct* evidence;
|
||||
> three inflate 28 distinct cases into 720 committed, under a flag ratified ON.
|
||||
> Not repaired — the ledger is SHA-sealed and ratified, so re-sealing is Shay's
|
||||
> decision. `docs/research/distinct-evidence-audit-2026-07-25.md`.
|
||||
>
|
||||
> **Revised order:** E2 → **R5–R7 premise scope** → C → D → E1(code) → parity,
|
||||
> with Phase F retargeted and its volume recomputed. §7's "A gates B" held; what
|
||||
> it missed is that a scope fix gates C, D *and* F.
|
||||
|
||||
Successor to `generalization-arc-2026-07-24.md`, which closed its Tier F/O/S
|
||||
arc, and to the assessment-verification arc (PR #113). Division of work across
|
||||
tiers: `docs/handoff/curriculum-license-loop-2026-07/DIVISION-OF-WORK.md`
|
||||
|
|
|
|||
Loading…
Reference in a new issue