docs: roll-up projection contract revision 3 (terra re-review residuals)
ci/woodpecker/pr/ci Pipeline was successful
ci/woodpecker/pr/ci Pipeline was successful
F2: partial-scope witnesses reconstructed at platform-project and estate sibling levels, where chain grants can differ; the workspace-sibling construction is stated non-constructible under contract 1 grant targets. F3: section 2.5 defines one field-exact recursive roll-up node record (id/type/name/totals/children at every depth, required children array, empty at workspaces, ascending-id ordering, no wrapper); whole-result rules moved to section 2.6 at section scope; section 6.7 witness asserts the recursive shape. F6: fixture assigns workspaces to named platform-projects; grant-level cases limited to the three levels contract 1 defines, workspace access covered by membership with the no-workspace-grant fact stated.
This commit is contained in:
@@ -33,6 +33,21 @@ and explicit company-, estate-, project-grant, and membership cases
|
|||||||
(F6). The §5.3 legacy-row exclusion and pre-rank no-obligation rules
|
(F6). The §5.3 legacy-row exclusion and pre-rank no-obligation rules
|
||||||
are disclosed as drafting additions (F7).
|
are disclosed as drafting additions (F7).
|
||||||
|
|
||||||
|
Revision 3 (terra re-review residuals): the partial-scope witnesses are
|
||||||
|
reconstructed at levels where chain grants can actually differ —
|
||||||
|
platform-project siblings under one estate and estate siblings under
|
||||||
|
one company — because contract 1 §3.1/§3.4 defines no workspace-level
|
||||||
|
grant target, so no reader can hold a chain grant on two of three
|
||||||
|
sibling workspaces (F2). §2.5 now defines one field-exact recursive
|
||||||
|
record — every node, including the queried node and every leaf, is the
|
||||||
|
same five-field shape with a required, deterministically ordered
|
||||||
|
`children` array that is empty at workspaces — and the whole-result
|
||||||
|
rules (no optional fields, denial envelope, wire faithfulness) are
|
||||||
|
their own §2.6 at section scope (F3). The fixture assigns workspaces
|
||||||
|
to named platform-projects, and §6.1's grant-level cases are the three
|
||||||
|
levels contract 1 defines, with workspace-level access covered by the
|
||||||
|
membership case and stated as having no direct chain grant (F6).
|
||||||
|
|
||||||
This contract binds the projection semantics (§2), reader authorization
|
This contract binds the projection semantics (§2), reader authorization
|
||||||
semantics (§3), read-only enforcement (§4), dependencies and phase
|
semantics (§3), read-only enforcement (§4), dependencies and phase
|
||||||
timing (§5), witnesses (§6), and disclosed drafting additions (§7). It
|
timing (§5), witnesses (§6), and disclosed drafting additions (§7). It
|
||||||
@@ -94,24 +109,40 @@ row with contract 5 (`tool-gateway-mapping.md`).
|
|||||||
is never imported, persisted as authoritative state, or used to
|
is never imported, persisted as authoritative state, or used to
|
||||||
gate or deny work (witness §6.8 — both the write-path and the
|
gate or deny work (witness §6.8 — both the write-path and the
|
||||||
decision-path prohibitions are witnessed).
|
decision-path prohibitions are witnessed).
|
||||||
5. **Closed semantic schema.** The successful result consists of
|
5. **Closed semantic schema.** The successful result is exactly one
|
||||||
exactly these semantic fields, and no others:
|
**roll-up node record**, a single recursive shape used at every
|
||||||
- `node`: the queried node — exactly `id`, `type` (one of the four
|
depth. A roll-up node record consists of exactly these five
|
||||||
contract 1 levels), `name`.
|
fields, and no others:
|
||||||
|
- `id`: the node's identifier.
|
||||||
|
- `type`: one of the four contract 1 levels.
|
||||||
|
- `name`: the node's name.
|
||||||
- `totals`: one entry per status value of the typed lifecycle —
|
- `totals`: one entry per status value of the typed lifecycle —
|
||||||
every status key present, a count of zero represented explicitly
|
every status key present, a count of zero represented explicitly
|
||||||
as `0`, never by key absence.
|
as `0`, never by key absence. At a workspace node, `totals` is
|
||||||
- `children`: the reader-visible (§3.2) child nodes of `node`,
|
that workspace's own counts; at any other node, `totals` is the
|
||||||
each carrying exactly the same `id`/`type`/`name`/`totals`
|
sum over the node's aggregation scope (§2.2). This is how §2.1's
|
||||||
shape, recursively down to the workspaces in the reader's
|
"per workspace and as subtree totals" content is carried:
|
||||||
aggregation scope. A node outside §3.2 visibility never appears
|
per-workspace counts are the leaf records' `totals`, subtree
|
||||||
at any depth.
|
totals are the interior records' `totals`.
|
||||||
There are no optional result fields. The denial/nonexistent
|
- `children`: a required array, present on EVERY node record. Its
|
||||||
response is the contract 5 §4.2 not-found-class error envelope
|
elements are the reader-visible (§3.2) child nodes of this node,
|
||||||
with no fields beyond that envelope. The wire DTO is expressed
|
each itself a complete roll-up node record, recursing down to
|
||||||
under contract 5 §4.1, and MUST be a faithful serialization of
|
the workspaces in the reader's aggregation scope. At a workspace
|
||||||
exactly this semantic field set: a wire field with no
|
node the array is exactly `[]` — a workspace record never has
|
||||||
corresponding semantic field above is a conformance defect.
|
children. The array is ordered deterministically, ascending by
|
||||||
|
`id`; the implementing PR asserts that ordering. A node outside
|
||||||
|
§3.2 visibility never appears at any depth.
|
||||||
|
|
||||||
|
The queried node's record IS the whole result — there is no
|
||||||
|
wrapper field around it.
|
||||||
|
|
||||||
|
6. **Whole-result rules.** There are no optional result fields at any
|
||||||
|
depth. The denial/nonexistent response is the contract 5 §4.2
|
||||||
|
not-found-class error envelope with no fields beyond that
|
||||||
|
envelope. The wire DTO is expressed under contract 5 §4.1, and
|
||||||
|
MUST be a faithful serialization of exactly the §2.5 recursive
|
||||||
|
record: a wire field with no corresponding semantic field is a
|
||||||
|
conformance defect.
|
||||||
|
|
||||||
## 3. Reader authorization semantics
|
## 3. Reader authorization semantics
|
||||||
|
|
||||||
@@ -191,9 +222,10 @@ Binding on the implementing PRs. Every witness names, in its
|
|||||||
implementation, the exact endpoints/tools, tables, and fixtures it
|
implementation, the exact endpoints/tools, tables, and fixtures it
|
||||||
exercises. The base fixture seeds two companies; under company A **two
|
exercises. The base fixture seeds two companies; under company A **two
|
||||||
estates with distinct, non-identical count profiles**: estate A1 with
|
estates with distinct, non-identical count profiles**: estate A1 with
|
||||||
two platform-projects and three workspaces, estate A2 with one
|
two platform-projects — P1 holding workspaces W1 and W2, P2 holding
|
||||||
platform-project and one workspace, all with known task counts across
|
workspace W3 — and estate A2 with one platform-project P3 holding one
|
||||||
at least three statuses; under company B one workspace.
|
workspace W4, all with known task counts across at least three
|
||||||
|
statuses; under company B one workspace.
|
||||||
|
|
||||||
1. **Correctness witnesses:** for a reader holding a direct company-A
|
1. **Correctness witnesses:** for a reader holding a direct company-A
|
||||||
grant, roll-up totals at every level equal the seeded sums — each
|
grant, roll-up totals at every level equal the seeded sums — each
|
||||||
@@ -203,28 +235,40 @@ at least three statuses; under company B one workspace.
|
|||||||
with no double count across the chain. For a reader holding a
|
with no double count across the chain. For a reader holding a
|
||||||
direct estate-A1 grant, the estate-A1 result equals the A1 sum and
|
direct estate-A1 grant, the estate-A1 result equals the A1 sum and
|
||||||
a company-A query returns company A with exactly A1's contribution
|
a company-A query returns company A with exactly A1's contribution
|
||||||
(estate A2 invisible). Each of the four grant levels — company,
|
(estate A2 invisible). Each of the three chain grant levels
|
||||||
estate, platform-project (below), workspace — has an explicit
|
contract 1 §3.1 defines — company, estate, platform-project
|
||||||
case; none is simulated by unioning workspace access.
|
(below, §6.2) — has an explicit direct-grant case, none simulated
|
||||||
2. **Scope witnesses:** a reader with a direct grant on one
|
by unioning lower access. Workspace-level access has NO direct
|
||||||
platform-project sees exactly its subtree's counts at every
|
chain grant (contract 1 §3.1/§3.4 define no workspace grant
|
||||||
queryable level; for a reader authorized on two of three sibling
|
target) and is covered by the §6.2 membership case.
|
||||||
workspaces, the parent totals equal the two readable workspaces'
|
2. **Scope witnesses:** a reader with a direct grant on
|
||||||
sum. **Membership locality (§1.4):** a member-only reader queries
|
platform-project P1 only sees exactly P1's subtree counts
|
||||||
|
(W1+W2): a P1 query returns W1+W2; an estate-A1 query returns the
|
||||||
|
estate node with exactly P1's contribution, sibling project P2 and
|
||||||
|
its workspace W3 absent at every depth; a company-A query likewise
|
||||||
|
carries only P1's contribution. An estate-sibling case: a reader
|
||||||
|
with a direct grant on estate A1 only queries company A and
|
||||||
|
receives exactly A1's contribution, estate A2 absent. (Chain
|
||||||
|
grants exist only at company, estate, and platform-project —
|
||||||
|
contract 1 §3.1 — so partial scope among SIBLING WORKSPACES of
|
||||||
|
one project is not constructible by grants and is not witnessed;
|
||||||
|
the constructible partial-scope cases are the project- and
|
||||||
|
estate-sibling ones above.) **Membership locality (§1.4):** a member-only reader queries
|
||||||
the workspace directly and receives its counts; the same reader
|
the workspace directly and receives its counts; the same reader
|
||||||
querying the workspace's parent (or any ancestor) receives the
|
querying the workspace's parent (or any ancestor) receives the
|
||||||
§3.4-equivalent nonexistent-node response, and no ancestor
|
§3.4-equivalent nonexistent-node response, and no ancestor
|
||||||
response for any other reader changes because of that membership.
|
response for any other reader changes because of that membership.
|
||||||
3. **No-oracle witnesses:** the sibling-workspace response above
|
3. **No-oracle witnesses:** the P1-only reader's estate-A1 response
|
||||||
contains no field disclosing the third workspace's existence
|
above contains no field disclosing P2's or W3's existence
|
||||||
(closed-schema comparison against a reader authorized on all
|
(closed-schema comparison against an estate-A1-granted reader's
|
||||||
three: identical field set, differing only in counts and visible
|
response: identical field set, differing only in counts and
|
||||||
nodes). **Partial-scope hidden node:** the reader who sees the
|
visible nodes). **Partial-scope hidden node:** the P1-only reader
|
||||||
parent and two siblings queries the hidden third workspace by its
|
— who sees estate A1 and the P1 subtree — queries hidden sibling
|
||||||
real id — the response satisfies the §3.4 equivalence predicate
|
project P2 by its real id, and separately hidden workspace W3 by
|
||||||
against the same query naming a nonexistent id, under one fixed
|
its real id; each response satisfies the §3.4 equivalence
|
||||||
request context with the declared volatile-field normalization.
|
predicate against the same query naming a nonexistent id, under
|
||||||
**Cross-tenant:** an unauthorized reader naming company B receives
|
one fixed request context with the declared volatile-field
|
||||||
|
normalization. **Cross-tenant:** an unauthorized reader naming company B receives
|
||||||
a response §3.4-equivalent to naming a nonexistent id. Each
|
a response §3.4-equivalent to naming a nonexistent id. Each
|
||||||
equivalence check is executable byte comparison after the declared
|
equivalence check is executable byte comparison after the declared
|
||||||
normalization, not a shape judgment.
|
normalization, not a shape judgment.
|
||||||
@@ -251,12 +295,14 @@ at least three statuses; under company B one workspace.
|
|||||||
workspace tables and the hierarchy tables (contract 1 §6.7's
|
workspace tables and the hierarchy tables (contract 1 §6.7's
|
||||||
both-table zero-write assertion).
|
both-table zero-write assertion).
|
||||||
7. **Closed-schema witness:** the response is asserted field-exact
|
7. **Closed-schema witness:** the response is asserted field-exact
|
||||||
against the §2.5 enumeration — `node` (id/type/name), `totals`
|
against the §2.5 recursive record at every depth — exactly
|
||||||
(every typed status present, explicit zeros), `children`
|
`id`/`type`/`name`/`totals`/`children` on every node, every typed
|
||||||
(recursive, visible only) — and a response carrying any field
|
status present with explicit zeros, `children: []` at every
|
||||||
outside the enumeration fails the assertion (carve-out boundary,
|
workspace record, the declared ascending-`id` ordering, no
|
||||||
|
wrapper field — and a response carrying any field outside the
|
||||||
|
record at any depth fails the assertion (carve-out boundary,
|
||||||
§2.3). The denial envelope is asserted field-exact against
|
§2.3). The denial envelope is asserted field-exact against
|
||||||
contract 5 §4.2's envelope.
|
contract 5 §4.2's envelope (§2.6).
|
||||||
8. **Non-authoritative and never-gate witnesses:** (a) a static
|
8. **Non-authoritative and never-gate witnesses:** (a) a static
|
||||||
production import-graph inventory (hierarchy contract §6.3 style,
|
production import-graph inventory (hierarchy contract §6.3 style,
|
||||||
production code over `apps/` and `packages/`, tests excluded)
|
production code over `apps/` and `packages/`, tests excluded)
|
||||||
|
|||||||
Reference in New Issue
Block a user