From e5b74028b5e39a9b2e8be44ce3c3f26cd87a67c5 Mon Sep 17 00:00:00 2001 From: Swung0x48 Date: Fri, 18 Sep 2026 12:33:04 -0400 Subject: [PATCH] [Docs] (Disaggregated): P5e ID-120 - contract amendment 8's sticky-forward clause is marked UNLANDED - CONTRACT-P5E section 8 item 8 says GetBufferBindingPointCount's sticky forward becomes FATAL under split. It is not in the code and must not be put there this phase: FieldOwnership.def:147 (field row) and :179 (forward row) both say BARRIER_PULLED, and the generator refuses a field/forward pair that disagrees - pinned by FieldOwnershipTest.TheSevenStickyForwardsAgreeWithTheirFieldRows. - Landing it as written would either trip the generator or drag the FIELD row to FATAL with it, and that second reading moves 23 pairs of the derived admitted set: the row's retiring phase is "P7/P13", which is exactly what admits it on every stamped verb under ID-125, and a FATAL row is admitted nowhere - so 23 reads this phase never promised to migrate would start aborting. - MEASURED, NOT INHERITED: ID-120 said 10 pairs; that count predates ID-125's retiring-phase disjunct. `--print-admitted | grep -c '^GetBufferBindingPointCount@'` says 23 on this head, and the note records the command as well as the number. - Annotated in place, struck through with the phase that lands it (P7/P13), for ID-105's reason: a contract clause that is arithmetically impossible against the code is a clause that changes, and the divergence is better stated than discovered from a red gate two phases from now. --- MobileGL/MG_Remote/CONTRACT-P5E.md | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/MobileGL/MG_Remote/CONTRACT-P5E.md b/MobileGL/MG_Remote/CONTRACT-P5E.md index 635f833e..36a3dac0 100644 --- a/MobileGL/MG_Remote/CONTRACT-P5E.md +++ b/MobileGL/MG_Remote/CONTRACT-P5E.md @@ -539,9 +539,29 @@ both backends. re-derived as `MGPipeBarriered`. 7. **§3.3's state note** is retired by fb (§5.4). 8. **`FieldOwnership.def`**: `GetBoundVertexArray`, `GetTextureUnitObject`, `GetImageTextureBinding`, `GetFramebufferBindingSlot`, `GetProgramForDraw/Dispatch`, `GetBufferBindingPoint` gain retiring - phase "P5e (Espryt unbarriered), P7 (Magma)"; `GetBufferBindingPointCount`'s forward → FATAL under - split; `GetTransformFeedbackProgram`, `GetProgramObject`, `GetTextureObject`, `ValidateProgramName`, - `HasOpenTransformFeedbackSpan`, `RecordError` keep their rows (barriered-only readers). + phase "P5e (Espryt unbarriered), P7 (Magma)"; ~~`GetBufferBindingPointCount`'s forward → FATAL under + split~~ (**UNLANDED — see below**); `GetTransformFeedbackProgram`, `GetProgramObject`, + `GetTextureObject`, `ValidateProgramName`, `HasOpenTransformFeedbackSpan`, `RecordError` keep + their rows (barriered-only readers). + + > **UNLANDED, and deliberately so (P5e gl, ruling ID-120). Lands with P7/P13.** The clause + > "`GetBufferBindingPointCount`'s forward → FATAL under split" is NOT in the code and must not + > be put there this phase. `FieldOwnership.def:147` (the field row) and `:179` (the forward row) + > both say `BARRIER_PULLED`, and the generator refuses a field/forward pair that disagrees — + > pinned by `FieldOwnershipTest.TheSevenStickyForwardsAgreeWithTheirFieldRows`. So landing the + > clause as written would either trip the generator or drag the FIELD row to FATAL with it, and + > that second reading changes **23 pairs** of the derived admitted set (§7, measured with + > `--print-admitted | grep -c '^GetBufferBindingPointCount@'`; ID-120 said 10, which was + > counted before ID-125's retiring-phase disjunct widened the set). The row's retiring phase is + > "P7/P13", which is exactly what admits it on every stamped verb today; a FATAL row is + > admitted nowhere, so those reads would start aborting on a migration this phase never + > promised. + > + > The divergence is STATED HERE rather than discovered from a red gate, for ID-105's reason: + > when a contract clause is arithmetically impossible against the code, the contract is what + > changes. The phase that retires the buffer-binding-point family (P7 for the Magma half, P13 + > for the transfer half) lands the field row and its forward TOGETHER, in one commit, and + > deletes this note. 9. **Table 1** gains `set_program_bindings` (80), appended; `set_shader_buffers` (38) gains its route, sink and emitter (`PipeCatalogueTest.cpp:170-171, 242-243` invert). **Table 0** gains §1's thirteen rows. **Table 3** gains `IpcTable::RunAhead/PresentCredit`.