Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,24 @@ body.
`deep-equality(coll, [])` and `equality(coll, [])` still resolve `insufficient-evidence` over the same
evidence where `count-tolerance(coll, 0, 0)` resolves `true`, because one totality covers a whole leaf
and exempting `equality` would also exempt a `{ literal: [] }` operand.
- Pre-flight's `seeded-faults-scoped` check no longer fails on a leg that is the fault leg's own
probe wearing a second label. The clean-leg set excluded the fault leg by leg id alone, so a
sensitivity witness leg spelling the manifestation witness's inputs was read as independent
evidence, the witness fired on it, and the check reported a scoping violation. A clean leg is now
dropped when it issued the fault leg's request and received the fault leg's answer. Both are
compared as canonical digests: the request with its correlation identifier neutralised, the
answer as the evidence a relation can address, which carries AD-11's projected body, so a field
the operation declares volatile is already out of it and a server-minted identifier stops being a
difference. Both halves are required. Answers alone would drop AD-10's own worked example of two
distinct nonexistent identifiers both returning 404, and requests alone cannot see that a system
answered one request two ways. The comparison lives in the reducer, where the answers are in
hand, beside the `state-reset` row that already compares two legs there.
- `seeded-faults-scoped` fails when no clean leg survives that comparison. It was satisfied before,
so a defect seeded against an operation with no other leg certified its own scoping from no
observation at all. A check that examined nothing has established nothing, which is the rule a
sensitivity relation resolving `insufficient-evidence` already follows. The note names the cause,
since an operation with no other leg and an operation every one of whose legs ran the fault leg's
probe are different authoring mistakes.

## [1.3.0] - 2026-09-09

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -570,6 +570,35 @@ Story 6.4's.
| `seeded-faults-scoped` | the defect's witness resolves non-`true` on every clean leg of its operation | it resolves `true` on any clean leg | never |
| `seeded-fault-fired` | the witness resolves `true` on its own fault leg | the witness is `null`, its leg has no observation, or the relation resolves `false` or `insufficient-evidence` | never |

>
> **Amended 2026-09-09, two rules.**
>
> 1. The row says "every clean leg of its operation", and the shipped reducer read "clean" as every
> other leg of that operation by leg id. A leg can run the fault leg's own probe under a second
> label, most often a sensitivity witness leg spelling the manifestation witness's inputs, and a
> witness firing there is the fault leg's own manifestation read a second time. The reducer now
> drops a clean leg that issued the fault leg's request and received the fault leg's answer.
> Both halves are required. Answers alone would drop AD-10's own worked example, two distinct
> nonexistent identifiers both returning 404, which are exactly the legs this check exists to
> read; requests alone are what the plan can see, and identical requests can still be answered
> differently. Both sides are canonical digests, the request with `probeId` neutralised and the
> answer as the leg's evidence with `observationId` neutralised. Evidence is the right side of
> the comparison because it is everything a relation can address, and it carries AD-11's
> projected body, so a field the operation declares volatile is already out of it. The comparison
> is in `reducePreflight` beside the `state-reset` row, which already compares two legs'
> projections there. An earlier revision of this change compared requests alone in
> `planPreflight` and narrowed the drop to `stateChangeMarker: false`, which left a defect seeded
> on `create-thing` failing the check whenever its witness posted a sensitivity leg's body. That
> case passes now: the answers decide it. Fixtures 126, 127, 128, 131, and 132.
> 2. An empty clean-leg set resolved `satisfied`, which certified scoping from no observation. It
> fails now, on the rule the `input-sensitivity` row already runs on: a check that examined
> nothing has established nothing. Emptiness is tested on the set that survives the drop, since
> the drop is what can empty it. Both causes are reachable and the note says which. An operation
> whose only leg is the fault leg reached it before this change. The drop adds AD-10's exemption
> case exactly: one keyless safe read whose two control-observe legs both send the empty inputs
> the operation admits, answered alike, so every leg the plan named is dropped. Fixtures 130 and
> 133.

**Anomalous** means `status >= 400`. The word is already the repository's: Story 6.1's conformance
suite asserts `probe/observe-anomalous-status`, and `ProbeObservation.status` is already bounded to
100–599 at the port, so nothing new is assumed about the protocol here.
Expand Down
12 changes: 12 additions & 0 deletions _bmad-output/project-knowledge/learning-path-step-by-step.md
Original file line number Diff line number Diff line change
Expand Up @@ -1801,6 +1801,18 @@ flowchart TD
- `clean-control` reads only the control legs. AD-10's own example is two 404s from a good fixture.
- The two seeded-fault checks are disjoint: one reads only clean legs, the other only the fault leg.
Fold them together and one answer maps to no outcome the schema can spell.
- A clean leg is one that asks a different question. The reducer drops a leg that issued the fault
leg's request and got the fault leg's answer, since that leg is the fault leg's own probe under a
second label. Both halves are needed: answers alone would drop two 404s from two distinct
nonexistent identifiers, which is AD-10's own example of a good fixture, and requests alone cannot
see that one request was answered two ways.
- The answer half compares the evidence, which is what a relation can address. It carries the
projected body, so a field the operation declares volatile is out of it already and a
server-minted id stops being a difference.
- An empty clean-leg set fails, and emptiness is tested on what survived the drop. The check
examined nothing, and a check that examined nothing has established nothing, which is the same
rule `insufficient-evidence` gets. The note says which cause emptied it: the operation had no
other leg, or every leg the plan named ran the fault leg's own probe.

**Watch out:**

Expand Down
2 changes: 1 addition & 1 deletion docs/reference/glossary.md
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ The six kinds a `PreflightVerdict` can carry.
| `state-reset` | Does the declared fixture reset return the system to a known state? |
| `clean-control` | Does the leg that should show nothing wrong in fact show nothing wrong? |
| `seeded-fault-fired` | Did the seeded fault manifest where it was supposed to? |
| `seeded-faults-scoped` | Did a manifestation witness fire on a clean leg, where it should not have? A leg with no observation cannot fire one, so a missing clean leg leaves this `satisfied`. |
| `seeded-faults-scoped` | Did a manifestation witness fire on a clean leg, where it should not have? A clean leg is one that asks a different question, so a leg that sent the fault leg's request and got back the fault leg's answer is left out. With no clean leg left to ask, this fails and says why. |

## Contract vocabulary

Expand Down
96 changes: 96 additions & 0 deletions src/core/preflight/reduce.ts
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,66 @@ const sameFixtureState = (
)
}

/**
* The canonical digest of one value, or `null` where the value holds something
* RFC 8785 cannot serialise. `JsonValue` admits an integer outside the safe
* range and a lone surrogate, and a 64-bit identifier in a query parameter is
* ordinary, so this is reachable from a contract that parses. A verdict is what
* this stage owes its caller, and `null` compares equal to nothing, so a value
* that cannot be digested leaves the two sides distinguishable and the check
* still reads the leg.
*/
const digestOrNull = (value: unknown): string | null => {
try {
return digestArtifact(value, PREFLIGHT_ARTIFACT_PATH)
} catch (error) {
if (error instanceof RuntimeFault) return null
throw error
}
}

/**
* Whether two legs issued one request and received one answer, which makes them
* one probe under two labels. A manifestation witness firing on such a leg is
* the fault leg's own manifestation read a second time, and it establishes
* nothing about where the defect is scoped.
*
* Both halves are required. Answers alone would drop AD-10's own worked example,
* two distinct nonexistent identifiers both returning 404: those legs ask
* different questions and are exactly the legs this check exists to read.
* Requests alone are what the plan can see, and identical requests can still be
* answered differently, which is why the comparison lives here where the
* answers are in hand.
*
* The answer half compares the evidence, which is everything a relation can
* address: two legs with equal evidence resolve one relation to one value. It
* carries AD-11's projected body, so a field the operation declares volatile is
* already out of it and a server-minted identifier stops being a difference,
* which is what makes the same request to a mutating operation comparable at
* all. The raw observation is the wrong side of this comparison for that exact
* reason: two writes to one collection differ on a minted id by design, and
* reading that as a difference puts the false failure this check just lost back
* one stage over.
*
* The correlation identifiers are neutralised on both sides, since they are the
* leg id and differ by construction. A digest that comes back `null` matches
* nothing, so a pair that cannot be compared stays a pair the check reads.
*/
const answeredAlike = (left: LegState, right: LegState): boolean => {
const request = (state: LegState): string | null =>
digestOrNull({ ...state.leg.request, probeId: '' })
const answer = (state: LegState): string | null =>
digestOrNull({ ...state.evidence, observationId: '' })
const leftRequest = request(left)
const leftAnswer = answer(left)
return (
leftRequest !== null &&
leftAnswer !== null &&
leftRequest === request(right) &&
leftAnswer === answer(right)
)
}

/**
* Resolves a manifestation witness against one leg. Returns `null` when that
* leg produced no observation, which the two seeded-fault rows read
Expand Down Expand Up @@ -307,7 +367,43 @@ export const reducePreflight: ReduceStage<
}
case 'seeded-faults-scoped': {
const { witness, defectId } = planned
const fault = states.get(witness.legId)
// The legs that answered a different question than the fault leg's, and
// the legs dropped for answering the same one.
const examined: string[] = []
const dropped: string[] = []
for (const legId of planned.cleanLegIds) {
const state = states.get(legId)
if (
state !== undefined &&
fault !== undefined &&
answeredAlike(state, fault)
) {
dropped.push(legId)
continue
}
examined.push(legId)
}
// Emptiness is tested on what survived the drop. A check over no clean
// leg examined nothing, and a check that examined nothing has
// established nothing, which is the rule the `input-sensitivity` row
// above already runs on. Satisfied here would certify scoping from zero
// evidence on the three contracts least able to afford it: one whose
// defect names the only leg its operation has, one whose every other leg
// repeats the fault leg's probe, and one where the plan named legs and
// the drop took all of them. The note says which.
if (examined.length === 0) {
const named = dropped.map((legId) => `"${legId}"`).join(', ')
return check(
planned.kind,
witness.operationId,
'failed',
dropped.length === 0
? `${defectId}: the operation has no leg besides the fault leg, so nothing here establishes that the defect is scoped to it`
: `${defectId}: every other leg of the operation issued the fault leg's own request and received its answer (${named}), so nothing here establishes that the defect is scoped to it`,
)
}
for (const legId of examined) {
const resolved = resolveAgainst(
witness,
states.get(legId),
Expand Down
59 changes: 59 additions & 0 deletions tests/preflight/fixtures/observations.ts
Original file line number Diff line number Diff line change
Expand Up @@ -478,6 +478,65 @@ export const cleanControlProbe: Probe = Probe.parse({
/** a deep copy of the seeded probe a test may mutate before parsing it back. */
export const probeDraft = (): any => structuredClone(seededProbe)

/**
* AD-10's exemption case as a whole contract: one safe read declaring no key in
* any channel. Its only legs are the two control-observe legs, and both carry
* the empty inputs the operation admits, so a defect seeded there has a
* manifestation witness that matches every leg of its own operation.
*/
export const keylessReadContract: EvalContract = EvalContract.parse({
...contractLiteral,
contractId: 'preflight-fixture-keyless',
permittedInterfaces: [
{
logicalId: 'thing-api',
kind: 'api',
operations: [
{
operationId: 'read-health',
method: 'GET',
pathTemplate: '/health',
stateChangeMarker: false,
requestShape: {
path: emptyChannel(),
query: emptyChannel(),
header: emptyChannel(),
body: emptyChannel(),
},
responseDescriptor: {
requiredKeys: [],
permittedKeys: ['ok'],
types: { ok: 'boolean' },
successIndicator: null,
channelRoles: null,
collectionLocations: null,
},
volatilePointers: [],
sensitivityWitness: null,
},
],
},
],
})

/** the seeded probe aimed at that contract's only operation. */
export const keylessDefectProbe: Probe = (() => {
const draft = probeDraft()
draft.probeId = 'P-003'
draft.defects[0].manifestationWitness.operationId = 'read-health'
draft.defects[0].manifestationWitness.inputs = inputsOf()
return Probe.parse(draft)
})()

/** the same probe aimed at an operation the plan gives no other leg. */
export const lonelyDefectProbe: Probe = (() => {
const draft = probeDraft()
draft.probeId = 'P-004'
draft.defects[0].manifestationWitness.operationId = 'reset-things'
draft.defects[0].manifestationWitness.inputs = inputsOf()
return Probe.parse(draft)
})()

export type ObservationPatch = {
readonly status?: number
readonly body?: ProbeObservedBody
Expand Down
Loading